diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-10-26 12:10:50 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-10-26 17:10:50 +0000 |
| commit | 58e710b299aaf46d480085fb98c77cd3b60de04a (patch) | |
| tree | ba38689b1f9188f669784712f558be1ba3f630b3 | |
| parent | aa09c24adf024eee0a72ba5b5d9119c71e17d2a0 (diff) | |
Add regressions for fixed issues (#7495)
Fixes #4656. Fixes #5234. These do not occur on master.
| -rw-r--r-- | test/regress/CMakeLists.txt | 2 | ||||
| -rw-r--r-- | test/regress/regress0/cores/issue5234-uc-ua.smt2 | 12 | ||||
| -rw-r--r-- | test/regress/regress0/unconstrained/issue4656-bool-term-vars.smt2 | 12 |
3 files changed, 26 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 8263152dd..299261284 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -449,6 +449,7 @@ set(regress_0_tests regress0/cores/issue4971-2.smt2 regress0/cores/issue4971-3.smt2 regress0/cores/issue5079.smt2 + regress0/cores/issue5234-uc-ua.smt2 regress0/cores/issue5238.smt2 regress0/cores/issue5902.smt2 regress0/cores/issue5908.smt2 @@ -1453,6 +1454,7 @@ set(regress_0_tests regress0/unconstrained/geq.smt2 regress0/unconstrained/gt.smt2 regress0/unconstrained/issue4644.smt2 + regress0/unconstrained/issue4656-bool-term-vars.smt2 regress0/unconstrained/ite.smt2 regress0/unconstrained/leq.smt2 regress0/unconstrained/lt.smt2 diff --git a/test/regress/regress0/cores/issue5234-uc-ua.smt2 b/test/regress/regress0/cores/issue5234-uc-ua.smt2 new file mode 100644 index 000000000..ab31ec71f --- /dev/null +++ b/test/regress/regress0/cores/issue5234-uc-ua.smt2 @@ -0,0 +1,12 @@ +; EXPECT: unsat +; EXPECT: () +(set-option :incremental true) +(set-option :check-unsat-cores true) +(set-option :produce-unsat-assumptions true) +(set-logic ALL) +(declare-const a Bool) +(declare-const b Bool) +(declare-const c Bool) +(assert (distinct a b c)) +(check-sat-assuming (c)) +(get-unsat-assumptions) diff --git a/test/regress/regress0/unconstrained/issue4656-bool-term-vars.smt2 b/test/regress/regress0/unconstrained/issue4656-bool-term-vars.smt2 new file mode 100644 index 000000000..cd6154464 --- /dev/null +++ b/test/regress/regress0/unconstrained/issue4656-bool-term-vars.smt2 @@ -0,0 +1,12 @@ +(set-logic QF_AUFBVLIA) +(set-info :status unsat) +(declare-fun a (Bool) Bool) +(declare-fun b (Bool) Bool) +(declare-fun c (Bool) Bool) +(declare-fun d () Bool) +(declare-fun e () Bool) +(declare-fun f () Bool) +(assert (distinct (a d) (a e))) +(assert (distinct (b e) (b f))) +(assert (distinct (c f) (c d))) +(check-sat) |