diff options
| author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2021-07-07 17:53:20 -0300 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-07-07 20:53:20 +0000 |
| commit | 299b9e0cee11e2b3da1aad5ffbd2f6a8b949d3fe (patch) | |
| tree | 1626294ba8a81c519ff469171850b7840d8a2a87 /test | |
| parent | 75e56930987398a02d1c90c723b4f18ea7c0d7c4 (diff) | |
[unsat cores] Adding regressions from #4971 (#6852)
Adds remaining regressions from issue #4791, which we can handle with the different new unsat-core modes. Note that issue4971-1.smt2 requires the sat-proof mode for unsat cores.
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/CMakeLists.txt | 3 | ||||
| -rw-r--r-- | test/regress/regress0/cores/issue4971-0.smt2 | 18 | ||||
| -rw-r--r-- | test/regress/regress0/cores/issue4971-1.smt2 | 15 | ||||
| -rw-r--r-- | test/regress/regress0/cores/issue4971-2.smt2 | 6 |
4 files changed, 42 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 18e9d9864..ea78096dc 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -439,6 +439,9 @@ set(regress_0_tests regress0/cores/issue3455.smt2 regress0/cores/issue3651.smt2 regress0/cores/issue4925.smt2 + regress0/cores/issue4971-0.smt2 + regress0/cores/issue4971-1.smt2 + regress0/cores/issue4971-2.smt2 regress0/cores/issue4971-3.smt2 regress0/cores/issue5079.smt2 regress0/cores/issue5238.smt2 diff --git a/test/regress/regress0/cores/issue4971-0.smt2 b/test/regress/regress0/cores/issue4971-0.smt2 new file mode 100644 index 000000000..75878183c --- /dev/null +++ b/test/regress/regress0/cores/issue4971-0.smt2 @@ -0,0 +1,18 @@ +; COMMAND-LINE: --incremental -q --check-unsat-cores +; EXPECT: unknown +; EXPECT: unsat +; EXPECT: ( +; EXPECT: IP_1 +; EXPECT: ) +(declare-const v1 Bool) +(declare-const v9 Bool) +(declare-const v14 Bool) +(declare-const i4 Int) +(declare-const v16 Bool) +(assert (! (forall ((q0 Bool) (q1 Bool) (q2 (_ BitVec 10)) (q3 Bool) (q4 (_ BitVec 10))) (=> (distinct (_ bv827 10) q2 q4) (xor q1 q0))) :named IP_1)) +(declare-const v21 Bool) +(assert (! (or v9 v21 v16) :named IP_33)) +(assert (! (or (< (abs 404) i4) v14 v1) :named IP_51)) +(check-sat) +(check-sat-assuming (IP_33 IP_51)) +(get-unsat-core)
\ No newline at end of file diff --git a/test/regress/regress0/cores/issue4971-1.smt2 b/test/regress/regress0/cores/issue4971-1.smt2 new file mode 100644 index 000000000..9bb4f3e84 --- /dev/null +++ b/test/regress/regress0/cores/issue4971-1.smt2 @@ -0,0 +1,15 @@ +; COMMAND-LINE: --incremental -q --check-unsat-cores --unsat-cores-mode=sat-proof +; EXPECT: sat +; EXPECT: sat +(declare-const i2 Int) +(declare-const i5 Int) +(declare-fun st2 () (Set Int)) +(declare-fun st4 () (Set Int)) +(declare-fun st9 () (Set Int)) +(declare-const v6 Bool) +(assert (! (forall ((q12 Int) (q13 Bool)) (xor false true true false true true v6 (<= 5 i5 93 417 i2) true (subset st2 st4) true)) :named IP_4)) +(declare-const i11 Int) +(assert (< (card st9) i11)) +(assert (! (not (<= 5 i5 93 417 i2)) :named IP_46)) +(check-sat) +(check-sat-assuming ((! (or v6 v6 v6) :named IP_12) (! (or false v6 v6) :named IP_56)))
\ No newline at end of file diff --git a/test/regress/regress0/cores/issue4971-2.smt2 b/test/regress/regress0/cores/issue4971-2.smt2 new file mode 100644 index 000000000..ac9de97d2 --- /dev/null +++ b/test/regress/regress0/cores/issue4971-2.smt2 @@ -0,0 +1,6 @@ +; COMMAND-LINE: --incremental --check-unsat-cores +; EXPECT: sat +(set-logic QF_SLIA) +(assert false) +(reset-assertions) +(check-sat)
\ No newline at end of file |