From 885f2f6f43460a024491390d78fe4c0cd838cafe Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Tue, 8 Dec 2020 21:48:21 +0100 Subject: [PATCH] Add regression from #1978. (#5552) This PR adds a regression from #1978 that has been fixed in the meantime. Closes #1978 . --- test/regress/CMakeLists.txt | 1 + test/regress/regress0/bool/issue1978.smt2 | 13 +++++++++++++ .../regress0/issue4707-bv-to-bool-small.smt2 | 1 + .../regress2/issue4707-bv-to-bool-large.smt2 | 1 + 4 files changed, 16 insertions(+) create mode 100644 test/regress/regress0/bool/issue1978.smt2 diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index ef00b11b0..590c2fef2 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -144,6 +144,7 @@ set(regress_0_tests regress0/auflia/fuzz04.smtv1.smt2 regress0/auflia/fuzz05.smtv1.smt2 regress0/auflia/x2.smtv1.smt2 + regress0/bool/issue1978.smt2 regress0/boolean-prec.cvc regress0/boolean-terms-bug-array.smt2 regress0/boolean-terms-kernel1.smt2 diff --git a/test/regress/regress0/bool/issue1978.smt2 b/test/regress/regress0/bool/issue1978.smt2 new file mode 100644 index 000000000..1ad26cbf7 --- /dev/null +++ b/test/regress/regress0/bool/issue1978.smt2 @@ -0,0 +1,13 @@ +; COMMAND-LINE: --incremental +; EXPECT: sat +; EXPECT: unsat +(set-logic ALL) +(declare-fun _substvar_29_ () Bool) +(declare-fun _substvar_30_ () Bool) +(declare-fun _substvar_36_ () Bool) +(assert (= false (and _substvar_29_ _substvar_30_))) +(check-sat) +(assert false) +(push 1) +(assert _substvar_36_) +(check-sat) \ No newline at end of file diff --git a/test/regress/regress0/issue4707-bv-to-bool-small.smt2 b/test/regress/regress0/issue4707-bv-to-bool-small.smt2 index c2f0a58ad..8d854f47f 100644 --- a/test/regress/regress0/issue4707-bv-to-bool-small.smt2 +++ b/test/regress/regress0/issue4707-bv-to-bool-small.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --bv-to-bool ; EXPECT: sat (set-logic ALL) (declare-fun b () (Array (_ BitVec 10) (_ BitVec 1))) diff --git a/test/regress/regress2/issue4707-bv-to-bool-large.smt2 b/test/regress/regress2/issue4707-bv-to-bool-large.smt2 index bb4e9794c..947c368d1 100644 --- a/test/regress/regress2/issue4707-bv-to-bool-large.smt2 +++ b/test/regress/regress2/issue4707-bv-to-bool-large.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --bv-to-bool ; EXPECT: sat (set-logic ALL) (declare-fun a () (Array (_ BitVec 32) (_ BitVec 8))) -- 2.30.2