diff options
| author | Mathias Preiner <mathias.preiner@gmail.com> | 2021-07-02 15:13:17 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-07-02 22:13:17 +0000 |
| commit | de0401e53e4baab30a5e78d5bd51048348b1e1ce (patch) | |
| tree | 0f1697a82a4c839b5fd7a365ce3c5777c741c70f /test/regress | |
| parent | f83a753ad62a005085c47a7c0f4ba2e406d9acd7 (diff) | |
Fix bv assert input reset assertions (#6820)
If reset-assertions was called it will now reset the SAT solver and the
CNF stream if clauses were permanently added to the SAT solver via
option --bv-assert-input.
Diffstat (limited to 'test/regress')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress0/bv/reset-assertions-assert-input.smt2 | 18 |
2 files changed, 19 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 6cf5c76c1..00a50a69c 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -429,6 +429,7 @@ set(regress_0_tests regress0/bv/mult-pow2-negative.smt2 regress0/bv/pr4993-bvugt-bvurem-a.smt2 regress0/bv/pr4993-bvugt-bvurem-b.smt2 + regress0/bv/reset-assertions-assert-input.smt2 regress0/bv/sizecheck.cvc regress0/bv/smtcompbug.smtv1.smt2 regress0/bv/test-bv_intro_pow2.smt2 diff --git a/test/regress/regress0/bv/reset-assertions-assert-input.smt2 b/test/regress/regress0/bv/reset-assertions-assert-input.smt2 new file mode 100644 index 000000000..6a77ae078 --- /dev/null +++ b/test/regress/regress0/bv/reset-assertions-assert-input.smt2 @@ -0,0 +1,18 @@ +; COMMAND-LINE: -i --bv-solver=bitblast --bv-assert-input +(set-logic QF_BV) +(set-option :global-declarations true) + +(declare-const a (_ BitVec 8)) +(declare-const b (_ BitVec 8)) +(declare-const c (_ BitVec 8)) +(declare-const d (_ BitVec 8)) + +(assert (distinct (bvadd a d) (bvadd b c))) +(set-info :status sat) +(check-sat) + +(reset-assertions) + +(assert (= (bvadd a d) (bvadd b c))) +(set-info :status sat) +(check-sat) |