From d288f52dd82fe6590950758289e86ebcb039350d Mon Sep 17 00:00:00 2001 From: Mathias Preiner Date: Wed, 30 Jun 2021 15:07:47 -0700 Subject: 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. --- test/regress/regress0/issue6738.smt2 | 12 ++++++++++++ 1 file changed, 12 insertions(+) create mode 100644 test/regress/regress0/issue6738.smt2 (limited to 'test/regress/regress0/issue6738.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) + -- cgit v1.2.3