diff options
-rw-r--r-- | src/theory/theory_engine.cpp | 12 |
1 files changed, 8 insertions, 4 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index aa897b244..5ef7480e8 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -590,10 +590,14 @@ void TheoryEngine::propagate(TNode literal, theory::TheoryId theory) { if (Theory::setContains(currentTheory, lhsNotified) && Theory::setContains(currentTheory, rhsNotified)) { // Normalize the equality Node equality = Rewriter::rewriteEquality(currentTheory, atom); - // The assertion - Node assertion = negated ? equality.notNode() : equality; - // Remember it to assert later - d_propagatedEqualities.push_back(SharedEquality(assertion, literal, theory, currentTheory)); + if (equality.getKind() != kind::CONST_BOOLEAN) { + // The assertion + Node assertion = negated ? equality.notNode() : equality; + // Remember it to assert later + d_propagatedEqualities.push_back(SharedEquality(assertion, literal, theory, currentTheory)); + } else { + Assert(negated || equality.getConst<bool>()); + } } } } |