[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.

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 18e9d9864be61cffc653c714451794e68e55d2a9..ea78096dcc3f444a06cc2935039d07c3bcc43fc0 100644 (file)
--- 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 (file)
index 0000000..7587818
--- /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 (file)
index 0000000..9bb4f3e
--- /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 (file)
index 0000000..ac9de97
--- /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