From: Dejan Jovanović <dejan.jovanovic@gmail.com>
Date: Sat, 10 Dec 2011 08:34:41 +0000 (+0000)
Subject: adding additional checks for theories propagating literals that already have a value
X-Git-Tag: cvc5-1.0.0~8360
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=933a1ea506fd553e756be942087ef82154b6f959;p=cvc5.git

adding additional checks for theories propagating literals that already have a value
---

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]);