From 3fd65ea9f5b5cdb2fe4b511b76abcad89e1cd71d Mon Sep 17 00:00:00 2001 From: =?utf8?q?Dejan=20Jovanovi=C4=87?= Date: Sat, 10 Dec 2011 07:02:21 +0000 Subject: [PATCH] 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. --- src/theory/theory_engine.cpp | 12 ++++++++---- 1 file 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()); + } } } } -- 2.30.2