Add regression from #1978. (#5552)

This PR adds a regression from #1978 that has been fixed in the meantime.
Closes #1978 .

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index ef00b11b09e259087d286faf6a79016dd01654c5..590c2fef2eb12126c49f58f1ffa61c879620c2f9 100644 (file)
--- 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 (file)
index 0000000..1ad26cb
--- /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 c2f0a58ad84b1c941966b8651643675668333a4c..8d854f47f246115c12405d9f4043c5763ebb5ad4 100644 (file)
--- 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 bb4e9794cef99abf70a39694a3931a288c06cac3..947c368d1d7bd66e83f0a8e97c7cb81f9437b957 100644 (file)
--- 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)))