a bit more changes, when propagting equalities/dis-equalities don't assert them to...

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index aa897b24439a2b1d14d12cb91d11aef1583cd1aa..5ef7480e8f51eab8c9bf46b6e9e75fa95bae666f 100644 (file)
--- 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>());
+          }
         }
       }
     }