a bit more changes, when propagting equalities/dis-equalities don't assert them to theories that rewrite them to true. for example, 1 != 0 rewrites to true, so it shouldn't get propagated to arithmetic.

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>());
+          }
         }
       }
     }