From 933a1ea506fd553e756be942087ef82154b6f959 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Dejan=20Jovanovi=C4=87?= Date: Sat, 10 Dec 2011 08:34:41 +0000 Subject: [PATCH] adding additional checks for theories propagating literals that already have a value --- src/theory/theory_engine.cpp | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 5ef7480e8..4c289b5c1 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -573,7 +573,14 @@ void TheoryEngine::propagate(TNode literal, theory::TheoryId theory) { Node normalizedEquality = Rewriter::rewrite(literal); if (d_propEngine->isSatLiteral(normalizedEquality)) { // If there is a literal, just enqueue it, same as above - d_propagatedLiterals.push_back(normalizedEquality); + bool value; + if (d_propEngine->hasValue(normalizedEquality, value)) { + // if we are propagting something that already has a sat value we better be the same + Debug("theory") << "literal " << literal << " (" << normalizedEquality << ") propagated by " << theory << " but already has a sat value" << std::endl; + Assert((value && (literal.getKind() != kind::NOT)) || (!value && literal.getKind() == kind::NOT)); + } else { + d_propagatedLiterals.push_back(normalizedEquality); + } } // Otherwise, we assert it to all interested theories Theory::Set lhsNotified = d_sharedTerms.getNotifiedTheories(atom[0]); -- 2.30.2