diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2021-06-30 15:07:47 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-06-30 22:07:47 +0000 |
commit | d288f52dd82fe6590950758289e86ebcb039350d (patch) | |
tree | f025c84989cc7e096ae365b9671bef267da546c8 /test/regress | |
parent | 46c994963ef764101409d55d77e0e15db704827b (diff) |
Use SAT context level for --bv-assert-input instead of decision level. (#6758)
The decision level as previously implemented was not accurate since it
did not consider the user context level. This resulted in facts being
incorrectly recognized as input assertions, which happened for
incremental benchmarks.
Diffstat (limited to 'test/regress')
-rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
-rw-r--r-- | test/regress/regress0/issue6738.smt2 | 12 |
2 files changed, 13 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index fe49d8b39..e2e216567 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -674,6 +674,7 @@ set(regress_0_tests regress0/issue5743.smt2 regress0/issue5947.smt2 regress0/issue6605-2-abd-triv.smt2 + regress0/issue6738.smt2 regress0/issue6741.smt2 regress0/ite_arith.smt2 regress0/ite_real_int_type.smtv1.smt2 diff --git a/test/regress/regress0/issue6738.smt2 b/test/regress/regress0/issue6738.smt2 new file mode 100644 index 000000000..905ae823c --- /dev/null +++ b/test/regress/regress0/issue6738.smt2 @@ -0,0 +1,12 @@ +; COMMAND-LINE: -i --bv-solver=bitblast --bv-assert-input +(set-logic QF_BV) +(declare-fun N () Bool) +(assert (not (= (_ bv1 1) (bvnot (ite N (_ bv1 1) (_ bv0 1)))))) +(push 1) +(assert (not N)) +(set-info :status unsat) +(check-sat) +(pop 1) +(set-info :status sat) +(check-sat) + |