From: Dejan Jovanović <dejan.jovanovic@gmail.com>
Date: Sat, 10 Dec 2011 07:02:21 +0000 (+0000)
Subject: a bit more changes, when propagting equalities/dis-equalities don't assert them to... 
X-Git-Tag: cvc5-1.0.0~8361
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3fd65ea9f5b5cdb2fe4b511b76abcad89e1cd71d;p=cvc5.git

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.
---

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