diff options
| author | Gereon Kremer <nafur42@gmail.com> | 2020-12-08 21:48:21 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-12-08 14:48:21 -0600 |
| commit | 885f2f6f43460a024491390d78fe4c0cd838cafe (patch) | |
| tree | be8d526d1e34d3d74b277568dd780e8727315c51 | |
| parent | 3255e4335f25f35318a41f174ec15a28b0f0520d (diff) | |
Add regression from #1978. (#5552)
This PR adds a regression from #1978 that has been fixed in the meantime.
Closes #1978 .
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress0/bool/issue1978.smt2 | 13 | ||||
| -rw-r--r-- | test/regress/regress0/issue4707-bv-to-bool-small.smt2 | 1 | ||||
| -rw-r--r-- | test/regress/regress2/issue4707-bv-to-bool-large.smt2 | 1 |
4 files changed, 16 insertions, 0 deletions
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))) |