From dec5c322b84e45659e3683d16b42a4b6d648b172 Mon Sep 17 00:00:00 2001 From: lianah Date: Tue, 26 Feb 2013 15:50:37 -0500 Subject: [PATCH] fix for bv crash in incremental mode; this is a temporary fix for bug 493 --- src/theory/bv/theory_bv.cpp | 5 ++- test/regress/regress0/aufbv/bug493.smt | 54 ++++++++++++++++++++++++++ 2 files changed, 58 insertions(+), 1 deletion(-) create mode 100644 test/regress/regress0/aufbv/bug493.smt diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 7acb93cc2..8baa31a4b 100644 --- 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 index 000000000..d7ae495af --- /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)))))))))))))) +) -- 2.30.2