From 299b9e0cee11e2b3da1aad5ffbd2f6a8b949d3fe Mon Sep 17 00:00:00 2001
From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Wed, 7 Jul 2021 17:53:20 -0300
Subject: [PATCH] [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.
---
 test/regress/CMakeLists.txt                  |  3 +++
 test/regress/regress0/cores/issue4971-0.smt2 | 18 ++++++++++++++++++
 test/regress/regress0/cores/issue4971-1.smt2 | 15 +++++++++++++++
 test/regress/regress0/cores/issue4971-2.smt2 |  6 ++++++
 4 files changed, 42 insertions(+)
 create mode 100644 test/regress/regress0/cores/issue4971-0.smt2
 create mode 100644 test/regress/regress0/cores/issue4971-1.smt2
 create mode 100644 test/regress/regress0/cores/issue4971-2.smt2

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