fix for bv crash in incremental mode; this is a temporary fix for bug 493

diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 7acb93cc2c4b01fb2749fed0ffa84e639a06a4ed..8baa31a4b6931ee6f5f8ba5de2cae2abeda411b5 100644 (file)
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -148,7 +148,10 @@ void TheoryBV::propagate(Effort e) {
   bool ok = true;
   for (; d_literalsToPropagateIndex < d_literalsToPropagate.size() && ok; d_literalsToPropagateIndex = d_literalsToPropagateIndex + 1) {
     TNode literal = d_literalsToPropagate[d_literalsToPropagateIndex];
-    ok = d_out->propagate(literal);
+    // temporary fix for incremental bit-blasting 
+    if (d_valuation.isSatLiteral(literal)) {
+      ok = d_out->propagate(literal);
+    }
   }
 
   if (!ok) {

diff --git a/test/regress/regress0/aufbv/bug493.smt b/test/regress/regress0/aufbv/bug493.smt
new file mode 100644 (file)
index 0000000..d7ae495
--- /dev/null
+++ b/test/regress/regress0/aufbv/bug493.smt
@@ -0,0 +1,54 @@
+(benchmark B_
+  :source {
+Source unknown
+}
+  :status unknown
+  :category { unknown }
+  :logic QF_AUFBV
+  :extrafuns ((m Array[8:8]))
+  :extrafuns ((regionSize Array[8:8]))
+  :extrafuns ((m_0 Array[8:8]))
+  :extrafuns ((regionSize_0 Array[8:8]))
+  :extrafuns ((addr_of_j BitVec[8]))
+  :extrafuns ((m_1 Array[8:8]))
+  :extrafuns ((regionSize_1 Array[8:8]))
+  :extrafuns ((m_2 Array[8:8]))
+  :extrafuns ((regionSize_2 Array[8:8]))
+  :extrafuns ((addr_of_a BitVec[8]))
+  :extrafuns ((m_3 Array[8:8]))
+  :extrafuns ((regionSize_3 Array[8:8]))
+  :extrafuns ((m_4 Array[8:8]))
+  :extrafuns ((regionSize_4 Array[8:8]))
+  :extrafuns ((m_5 Array[8:8]))
+  :extrafuns ((regionSize_5 Array[8:8]))
+  :extrafuns ((m_6 Array[8:8]))
+  :extrafuns ((regionSize_6 Array[8:8]))
+  :extrafuns ((addr_of_i BitVec[8]))
+  :extrafuns ((m_7 Array[8:8]))
+  :extrafuns ((regionSize_7 Array[8:8]))
+  :extrafuns ((m_8 Array[8:8]))
+  :extrafuns ((regionSize_8 Array[8:8]))
+  :formula (let (?v_3 (bvadd addr_of_a (select (store regionSize addr_of_a (bvmul bv8[8] bv1[8])) addr_of_a))) (let (?v_0 (store m addr_of_j bv0[8])) (let (?v_1 (store ?v_0 addr_of_j (bvadd (select ?v_0 addr_of_j) bv2[8]))) (let (?v_2 (bvadd addr_of_a (bvmul (select (store ?v_1 addr_of_i (bvadd (select ?v_1 addr_of_j) bv2[8])) addr_of_i) bv1[8]))) (not (implies (if_then_else true (and (bvule addr_of_a ?v_3) (and (bvult addr_of_j addr_of_a) (bvult addr_of_i addr_of_j))) false) (and (bvule addr_of_a ?v_2) (bvult ?v_2 ?v_3))))))))
+  :extrafuns ((m_9 Array[8:8]))
+  :extrafuns ((regionSize_9 Array[8:8]))
+  :extrafuns ((m_10 Array[8:8]))
+  :extrafuns ((regionSize_10 Array[8:8]))
+  :extrafuns ((m_11 Array[8:8]))
+  :extrafuns ((regionSize_11 Array[8:8]))
+  :extrafuns ((addr_of_TEST_VAR_0 BitVec[8]))
+  :extrafuns ((m_12 Array[8:8]))
+  :extrafuns ((regionSize_12 Array[8:8]))
+  :extrafuns ((m_13 Array[8:8]))
+  :extrafuns ((regionSize_13 Array[8:8]))
+  :extrafuns ((m_14 Array[8:8]))
+  :extrafuns ((regionSize_14 Array[8:8]))
+  :extrafuns ((m_15 Array[8:8]))
+  :extrafuns ((regionSize_15 Array[8:8]))
+  :extrafuns ((m_16 Array[8:8]))
+  :extrafuns ((regionSize_16 Array[8:8]))
+  :extrafuns ((m_17 Array[8:8]))
+  :extrafuns ((regionSize_17 Array[8:8]))
+  :extrafuns ((m_18 Array[8:8]))
+  :extrafuns ((regionSize_18 Array[8:8]))
+  :formula (let (?v_9 (bvadd addr_of_a (select (store regionSize addr_of_a (bvmul bv8[8] bv1[8])) addr_of_a))) (flet ($v_4 (bvule addr_of_a ?v_9)) (flet ($v_5 (bvult addr_of_i addr_of_j)) (let (?v_0 (store m addr_of_j bv0[8])) (let (?v_1 (store ?v_0 addr_of_j (bvadd (select ?v_0 addr_of_j) bv2[8]))) (let (?v_2 (store ?v_1 addr_of_i (bvadd (select ?v_1 addr_of_j) bv2[8]))) (let (?v_3 (store ?v_2 (bvadd addr_of_a (bvmul (select ?v_2 addr_of_i) bv1[8])) bv0[8])) (let (?v_6 (store ?v_3 addr_of_TEST_VAR_0 (ite (bvult (select ?v_3 addr_of_j) bv8[8]) bv1[8] bv0[8]))) (let (?v_7 (store ?v_6 addr_of_j (bvadd (select ?v_6 addr_of_j) bv2[8]))) (let (?v_8 (bvadd addr_of_a (bvmul (select (store ?v_7 addr_of_i (bvadd (select ?v_7 addr_of_j) bv2[8])) addr_of_i) bv1[8]))) (not (implies (if_then_else (if_then_else (if_then_else true (and $v_4 (and (bvult addr_of_j addr_of_a) $v_5)) false) (not (= (select ?v_6 addr_of_TEST_VAR_0) bv0[8])) false) (and $v_4 (and (bvult addr_of_TEST_VAR_0 addr_of_a) (and (bvult addr_of_j addr_of_TEST_VAR_0) $v_5))) false) (and (bvule addr_of_a ?v_8) (bvult ?v_8 ?v_9))))))))))))))
+)