diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/theory_engine.cpp | 14 |
1 files changed, 11 insertions, 3 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 63fc1ae65..a81b38fe9 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -931,8 +931,10 @@ void TheoryEngine::assertToTheory(TNode assertion, TNode originalAssertion, theo if (fromTheoryId == THEORY_SAT_SOLVER) { // We know that this is normalized, so just send it off to the theory if (markPropagation(assertion, originalAssertion, toTheoryId, fromTheoryId)) { - // We assert it, and we know it's preregistereed coming from the SAT solver directly - theoryOf(toTheoryId)->assertFact(assertion, assertion == originalAssertion); + // Is it preregistered + bool preregistered = d_propEngine->isSatLiteral(assertion) && Theory::theoryOf(assertion) == toTheoryId; + // We assert it + theoryOf(toTheoryId)->assertFact(assertion, preregistered); // Mark that we have more information d_factsAsserted = true; } @@ -1211,6 +1213,9 @@ void TheoryEngine::ensureLemmaAtoms(const std::vector<TNode>& atoms, theory::The // Rewrite the equality Node eqNormalized = Rewriter::rewrite(atoms[i]); + + Debug("theory::atoms") << "TheoryEngine::ensureLemmaAtoms(): " << eq << " with nf " << eqNormalized << std::endl; + // If the equality is a boolean constant, we send immediately if (eqNormalized.isConst()) { if (eqNormalized.getConst<bool>()) { @@ -1221,8 +1226,11 @@ void TheoryEngine::ensureLemmaAtoms(const std::vector<TNode>& atoms, theory::The continue; } + Assert(eqNormalized.getKind() == kind::EQUAL); + + // If the normalization did the just flips, keep the flip - if (eqNormalized[0] == eq[1]) { + if (eqNormalized[0] == eq[1] && eqNormalized[1] == eq[0]) { eq = eqNormalized; } |