From: Gereon Kremer <nafur42@gmail.com>
Date: Tue, 8 Dec 2020 20:48:21 +0000 (+0100)
Subject: Add regression from #1978. (#5552)
X-Git-Tag: cvc5-1.0.0~2478
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=885f2f6f43460a024491390d78fe4c0cd838cafe;p=cvc5.git

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 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)))