From: Dejan Jovanović <dejan.jovanovic@gmail.com>
Date: Sun, 10 Jul 2011 12:05:47 +0000 (+0000)
Subject: another bugfix for uf
X-Git-Tag: cvc5-1.0.0~8515
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4b77b48b0069aa5b75163b0ca92d1a066c1f6ebd;p=cvc5.git

another bugfix for uf
---

diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 7688379d9..438854a9a 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -97,15 +97,20 @@ void TheoryUF::propagate(Effort level) {
       if (!d_valuation.hasSatValue(literal, satValue)) {
         d_out->propagate(literal);
       } else {
-        std::vector<TNode> assumptions;
-        if (literal != d_false) {
-          TNode negatedLiteral = literal.getKind() == kind::NOT ? literal[0] : (TNode) literal.notNode();
-          assumptions.push_back(negatedLiteral);
+        if (!satValue) {
+          Debug("uf") << "TheoryUF::propagate(): in conflict" << std::endl;
+          std::vector<TNode> assumptions;
+          if (literal != d_false) {
+            TNode negatedLiteral = literal.getKind() == kind::NOT ? literal[0] : (TNode) literal.notNode();
+            assumptions.push_back(negatedLiteral);
+          }
+          explain(literal, assumptions);
+          d_conflictNode = mkAnd(assumptions);
+          d_conflict = true;
+          break;
+        } else {
+          Debug("uf") << "TheoryUF::propagate(): already asserted" << std::endl;
         }
-        explain(literal, assumptions);
-        d_conflictNode = mkAnd(assumptions);
-        d_conflict = true;
-        break;
       }
     }
   }