From 4b77b48b0069aa5b75163b0ca92d1a066c1f6ebd Mon Sep 17 00:00:00 2001
From: =?utf8?q?Dejan=20Jovanovi=C4=87?= <dejan.jovanovic@gmail.com>
Date: Sun, 10 Jul 2011 12:05:47 +0000
Subject: [PATCH] another bugfix for uf

---
 src/theory/uf/theory_uf.cpp | 21 +++++++++++++--------
 1 file changed, 13 insertions(+), 8 deletions(-)

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;
       }
     }
   }
-- 
2.30.2