From 1c0a94f3797c0746c760009975012cfd0a247583 Mon Sep 17 00:00:00 2001
From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Wed, 19 May 2021 18:05:07 -0300
Subject: [PATCH] Adding regressions that failed on old unsat cores (#6574)

We can thus close #3455, #3651, #4925, #5079, #5238, #5902, #5908, and #5604.
---
 test/regress/CMakeLists.txt                  |  9 +++++
 test/regress/regress0/cores/issue3455.smt2   | 16 +++++++++
 test/regress/regress0/cores/issue3651.smt2   | 21 +++++++++++
 test/regress/regress0/cores/issue4925.smt2   | 16 +++++++++
 test/regress/regress0/cores/issue4971-3.smt2 | 38 ++++++++++++++++++++
 test/regress/regress0/cores/issue5079.smt2   | 16 +++++++++
 test/regress/regress0/cores/issue5238.smt2   | 14 ++++++++
 test/regress/regress0/cores/issue5902.smt2   |  3 ++
 test/regress/regress0/cores/issue5908.smt2   | 22 ++++++++++++
 test/regress/regress1/cores/issue5604.smt2   |  8 +++++
 10 files changed, 163 insertions(+)
 create mode 100644 test/regress/regress0/cores/issue3455.smt2
 create mode 100644 test/regress/regress0/cores/issue3651.smt2
 create mode 100644 test/regress/regress0/cores/issue4925.smt2
 create mode 100644 test/regress/regress0/cores/issue4971-3.smt2
 create mode 100644 test/regress/regress0/cores/issue5079.smt2
 create mode 100644 test/regress/regress0/cores/issue5238.smt2
 create mode 100644 test/regress/regress0/cores/issue5902.smt2
 create mode 100644 test/regress/regress0/cores/issue5908.smt2
 create mode 100644 test/regress/regress1/cores/issue5604.smt2

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 21a9f04b8..1478ae072 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -432,6 +432,14 @@ set(regress_0_tests
   regress0/bv/unsound1-reduced.smt2
   regress0/chained-equality.smt2
   regress0/constant-rewrite.smtv1.smt2
+  regress0/cores/issue3455.smt2
+  regress0/cores/issue3651.smt2
+  regress0/cores/issue4925.smt2
+  regress0/cores/issue4971-3.smt2
+  regress0/cores/issue5079.smt2
+  regress0/cores/issue5238.smt2
+  regress0/cores/issue5902.smt2
+  regress0/cores/issue5908.smt2
   regress0/cvc-rerror-print.cvc
   regress0/cvc3-bug15.cvc
   regress0/cvc3.userdoc.01.cvc
@@ -1487,6 +1495,7 @@ set(regress_1_tests
   regress1/bvdiv2.smt2
   regress1/constarr3.cvc
   regress1/constarr3.smt2
+  regress1/cores/issue5604.smt2
   regress1/datatypes/acyclicity-sr-ground096.smt2
   regress1/datatypes/dt-color-2.6.smt2
   regress1/datatypes/dt-param-card4-unsat.smt2
diff --git a/test/regress/regress0/cores/issue3455.smt2 b/test/regress/regress0/cores/issue3455.smt2
new file mode 100644
index 000000000..ec72daa32
--- /dev/null
+++ b/test/regress/regress0/cores/issue3455.smt2
@@ -0,0 +1,16 @@
+; COMMAND-LINE: -q --incremental --no-check-proofs
+; EXPECT: sat
+; EXPECT: sat
+; EXPECT: unsat
+; EXPECT: unsat
+; EXPECT: unsat
+(declare-fun x0 () Real)
+(check-sat)
+(assert (<= (* x0 (- 1)) 0))
+(assert (or (>= 0 x0) (> (+ 1.0 x0) (- 12))))
+(check-sat)
+(push)
+(assert (<= x0 (- 13)))
+(check-sat)
+(check-sat)
+(check-sat)
\ No newline at end of file
diff --git a/test/regress/regress0/cores/issue3651.smt2 b/test/regress/regress0/cores/issue3651.smt2
new file mode 100644
index 000000000..104767439
--- /dev/null
+++ b/test/regress/regress0/cores/issue3651.smt2
@@ -0,0 +1,21 @@
+; COMMAND-LINE: --incremental -q
+; EXPECT: sat
+; EXPECT: sat
+; EXPECT: sat
+; EXPECT: sat
+; EXPECT: unsat
+(declare-fun a () Real)
+(declare-fun b () Real)
+(declare-fun c () Real)
+(assert (> (+ (/ (- 2) a) (* 8 a)) 0))
+(assert (<= b 0))
+(assert (= (+ (* 4 a) (* 2 b)) 1))
+(assert (>= (* b c) 0))
+(check-sat)
+(check-sat)
+(check-sat)
+(push)
+(check-sat)
+(pop)
+(assert (>= c 1))
+(check-sat)
diff --git a/test/regress/regress0/cores/issue4925.smt2 b/test/regress/regress0/cores/issue4925.smt2
new file mode 100644
index 000000000..951f7e008
--- /dev/null
+++ b/test/regress/regress0/cores/issue4925.smt2
@@ -0,0 +1,16 @@
+; COMMAND-LINE: --no-check-proofs
+; EXPECT: sat
+; EXPECT: unsat
+; EXPECT: unsat
+(set-logic QF_LRA)
+(set-option :incremental true)
+(declare-fun a () Real)
+(declare-fun b () Real)
+(declare-fun c () Real)
+(assert (< c 0))
+(assert (> (+ a b) 0))
+(assert (or (< a 1) (> c 1)))
+(check-sat)
+(assert (= b (- 1)))
+(check-sat true)
+(check-sat)
\ No newline at end of file
diff --git a/test/regress/regress0/cores/issue4971-3.smt2 b/test/regress/regress0/cores/issue4971-3.smt2
new file mode 100644
index 000000000..ebbe07519
--- /dev/null
+++ b/test/regress/regress0/cores/issue4971-3.smt2
@@ -0,0 +1,38 @@
+; COMMAND-LINE: --incremental -q --check-unsat-cores
+; EXPECT: sat
+; EXPECT: sat
+; EXPECT: sat
+; EXPECT: sat
+(declare-const v1 Bool)
+(declare-const v2 Bool)
+(declare-const v3 Bool)
+(declare-const v5 Bool)
+(declare-const v6 Bool)
+(declare-const v9 Bool)
+(declare-const v10 Bool)
+(declare-const v11 Bool)
+(declare-const v12 Bool)
+(declare-const v13 Bool)
+(declare-const i1 Int)
+(declare-const i4 Int)
+(declare-const r0 Real)
+(declare-const r9 Real)
+(declare-const r16 Real)
+(declare-const Str3 String)
+(declare-const Str5 String)
+(declare-const Str6 String)
+(declare-const Str9 String)
+(declare-const Str10 String)
+(declare-const Str11 String)
+(declare-const Str19 String)
+(assert (>= (str.len Str10) 45))
+(assert (! (=> v11 v12) :named IP_1))
+(assert (! (= (is_int 925.05885) (> i4 45) v13 v3 v6 v6) :named IP_2))
+(check-sat)
+(assert (! (=> v10 v9) :named IP_3))
+(assert (str.in_re Str6(re.++ (str.to_re Str10) (str.to_re "wlzjqa" ))))
+(assert (! (not v10) :named IP_4))
+(check-sat-assuming (IP_2 IP_4))
+(check-sat-assuming (IP_1 IP_3))
+(assert (! (xor v3 v1 v5 v3 v2 (distinct Str19 Str3 Str5 Str9 Str11) (distinct 359 i1) v2 (>= r16 9873987263.0 r9 r0)) :named IP_6))
+(check-sat)
\ No newline at end of file
diff --git a/test/regress/regress0/cores/issue5079.smt2 b/test/regress/regress0/cores/issue5079.smt2
new file mode 100644
index 000000000..cc828deb1
--- /dev/null
+++ b/test/regress/regress0/cores/issue5079.smt2
@@ -0,0 +1,16 @@
+; EXPECT: sat
+; EXPECT: sat
+; EXPECT: unsat
+(set-logic ALL)
+(set-option :incremental true)
+(declare-fun a () Real)
+(declare-fun b () Real)
+(assert (<= b 0.25))
+(assert (= (- b a) 3))
+(assert (or (> (* 2 b) 0) (= (/ 1 b) 3)))
+(check-sat)
+(push)
+(check-sat)
+(pop)
+(assert (>= (* 3 a) 1))
+(check-sat)
\ No newline at end of file
diff --git a/test/regress/regress0/cores/issue5238.smt2 b/test/regress/regress0/cores/issue5238.smt2
new file mode 100644
index 000000000..ae3bed2e2
--- /dev/null
+++ b/test/regress/regress0/cores/issue5238.smt2
@@ -0,0 +1,14 @@
+; COMMAND-LINE: --incremental --no-check-models
+; EXPECT: sat
+; EXPECT: unsat
+; EXPECT: unsat
+(set-logic ALL)
+(declare-fun a () Real)
+(declare-fun b () Real)
+(assert (distinct b 0))
+(assert (= b 2))
+(assert (= (/ 0 a) 1))
+(check-sat)
+(assert (= (+ a b) 0))
+(check-sat (> b 1))
+(check-sat)
\ No newline at end of file
diff --git a/test/regress/regress0/cores/issue5902.smt2 b/test/regress/regress0/cores/issue5902.smt2
new file mode 100644
index 000000000..809873003
--- /dev/null
+++ b/test/regress/regress0/cores/issue5902.smt2
@@ -0,0 +1,3 @@
+; COMMAND-LINE: -q
+; EXPECT: unsat
+(check-sat false)
diff --git a/test/regress/regress0/cores/issue5908.smt2 b/test/regress/regress0/cores/issue5908.smt2
new file mode 100644
index 000000000..3224079ba
--- /dev/null
+++ b/test/regress/regress0/cores/issue5908.smt2
@@ -0,0 +1,22 @@
+; COMMAND-LINE: -i -q
+; EXPECT: sat
+; EXPECT: sat
+; EXPECT: unsat
+(declare-fun a () Int)
+(declare-fun b () Int)
+(declare-fun c () Int)
+(declare-fun d () Int)
+(declare-fun e () Int)
+(declare-fun f () Int)
+(assert (<= 0 a))
+(assert (= 0 c))
+(assert (not (= a b)))
+(assert (= b c))
+(assert (not (= d f)))
+(check-sat)
+(push)
+(check-sat)
+(pop)
+(assert (> e a))
+(assert (= e 0))
+(check-sat)
\ No newline at end of file
diff --git a/test/regress/regress1/cores/issue5604.smt2 b/test/regress/regress1/cores/issue5604.smt2
new file mode 100644
index 000000000..e41335a4a
--- /dev/null
+++ b/test/regress/regress1/cores/issue5604.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --strings-exp -q
+; EXPECT: unsat
+(declare-fun a () String)
+(declare-fun b () String)
+(declare-fun c () String)
+(assert (xor (str.prefixof (str.replace "B" (str.substr a 0 (str.len b)) "") b) (str.prefixof "B" b)))
+(assert (= a (str.++ b c)))
+(check-sat)
-- 
2.30.2