fix for clark's bug

imporant: theories SHOULD NOT use getSatValue at all, otherwise they might create a conflict with a literal they didn't get()  

3 files changed, 48 insertions, 19 deletions

diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 811600ad4..273b406e6 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -225,27 +225,20 @@ bool TheoryBV::storePropagation(TNode literal, SubTheory subtheory)
     d_propagatedBy[literal] = subtheory;
   }
 
-  // See if the literal has been asserted already
-  bool satValue = false;
-  bool hasSatValue = d_valuation.hasSatValue(literal, satValue);
-
-  // If asserted, we might be in conflict
-  if (hasSatValue && !satValue) {
-    Debug("bitvector::propagate") << indent() << "TheoryBV::storePropagation(" << literal << ", " << subtheory << ") => conflict" << std::endl;
-    std::vector<TNode> assumptions;
-    Node negatedLiteral = literal.getKind() == kind::NOT ? (Node) literal[0] : literal.notNode();
-    assumptions.push_back(negatedLiteral);
-    explain(literal, assumptions);
-    setConflict(mkAnd(assumptions)); 
-    return false;
+  // Propagate differs depending on the subtheory
+  // * bitblaster needs to be left alone until it's done, otherwise it doesn't know how to explain
+  // * equality engine can propagate eagerly
+  bool ok = true;
+  if (subtheory == SUB_EQUALITY) {
+    d_out->propagate(literal);
+    if (!ok) {
+      setConflict();
+    }
+  } else {
+    d_literalsToPropagate.push_back(literal);
   }
+  return ok;
 
-  // Nothing, just enqueue it for propagation and mark it as asserted already
-  Debug("bitvector::propagate") << indent() << "TheoryBV::storePropagation(" << literal << ", " << subtheory << ") => enqueuing for propagation" << std::endl;
-  d_literalsToPropagate.push_back(literal);
-
-  // No conflict
-  return true;
 }/* TheoryBV::propagate(TNode) */
 
 
diff --git a/test/regress/regress0/bv/Makefile.am b/test/regress/regress0/bv/Makefile.am
index 481a19ef3..a21c772b1 100644
--- a/test/regress/regress0/bv/Makefile.am
+++ b/test/regress/regress0/bv/Makefile.am
@@ -34,6 +34,7 @@ SMT_TESTS = \
 	fuzz17.delta01.smt \
 	fuzz18.delta01.smt \
 	fuzz18.delta02.smt \
+	fuzz18.delta03.smt \
 	fuzz18.smt \
 	fuzz19.delta01.smt \
 	fuzz19.smt \
diff --git a/test/regress/regress0/bv/fuzz18.delta03.smt b/test/regress/regress0/bv/fuzz18.delta03.smt
new file mode 100644
index 000000000..685f5c153
--- /dev/null
+++ b/test/regress/regress0/bv/fuzz18.delta03.smt
@@ -0,0 +1,35 @@
+(benchmark fuzzsmt
+:logic QF_BV
+:extrafuns ((v4 BitVec[4]))
+:extrafuns ((v2 BitVec[4]))
+:extrafuns ((v6 BitVec[4]))
+:status sat
+:formula
+(flet ($n1 true)
+(let (?n2 bv1[1])
+(let (?n3 (sign_extend[3] ?n2))
+(flet ($n4 (bvuge v6 ?n3))
+(let (?n5 bv0[1])
+(let (?n6 (ite $n4 ?n2 ?n5))
+(let (?n7 (zero_extend[3] ?n6))
+(let (?n8 bv1[4])
+(flet ($n9 (bvugt ?n7 ?n8))
+(let (?n10 (ite $n9 ?n2 ?n5))
+(let (?n11 (sign_extend[3] ?n10))
+(let (?n12 (bvlshr v2 v4))
+(let (?n13 (bvashr ?n12 v6))
+(flet ($n14 (bvult ?n11 ?n13))
+(let (?n15 bv0[4])
+(flet ($n16 (distinct v4 ?n15))
+(flet ($n17 (bvslt ?n15 ?n12))
+(let (?n18 (ite $n17 ?n2 ?n5))
+(let (?n19 (zero_extend[3] ?n18))
+(flet ($n20 (bvugt ?n8 ?n19))
+(let (?n21 (ite $n20 ?n2 ?n5))
+(let (?n22 (sign_extend[3] ?n21))
+(flet ($n23 (bvslt ?n15 ?n22))
+(let (?n24 (ite $n23 ?n2 ?n5))
+(flet ($n25 (bvsle ?n5 ?n24))
+(flet ($n26 (and $n14 $n16 $n25))
+$n26
+)))))))))))))))))))))))))))