Add regressions for closed issues (#5526)

We can close #5520, we can close #5378.

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index f66dc2d10fde9f074c58bd76f3828c1dbe240d79..effe70c1c6e5c5ef50efd1df35f51ff734de88d9 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1283,6 +1283,8 @@ set(regress_1_tests
   regress1/arith/div.08.smt2
   regress1/arith/div.09.smt2
   regress1/arith/issue3952-rew-eq.smt2
+  regress1/arith/issue4985-model-success.smt2
+  regress1/arith/issue4985b-model-success.smt2
   regress1/arith/issue789.smt2
   regress1/arith/miplib3.cvc
   regress1/arith/mod.02.smt2
@@ -1613,6 +1615,7 @@ set(regress_1_tests
   regress1/quantifiers/issue5019-cegqi-i.smt2
   regress1/quantifiers/issue5279-nqe.smt2
   regress1/quantifiers/issue5365-nqe.smt2
+  regress1/quantifiers/issue5378-witness.smt2
   regress1/quantifiers/issue5469-aext.smt2
   regress1/quantifiers/issue5470-aext.smt2
   regress1/quantifiers/issue5471-aext.smt2
@@ -1864,6 +1867,7 @@ set(regress_1_tests
   regress1/strings/issue5374-proxy-i.smt2
   regress1/strings/issue5483-pp-leq.smt2
   regress1/strings/issue5510-re-consume.smt2
+  regress1/strings/issue5520-re-consume.smt2
   regress1/strings/kaluza-fl.smt2
   regress1/strings/loop002.smt2
   regress1/strings/loop003.smt2

diff --git a/test/regress/regress1/arith/issue4985-model-success.smt2 b/test/regress/regress1/arith/issue4985-model-success.smt2
new file mode 100644 (file)
index 0000000..794eefb
--- /dev/null
+++ b/test/regress/regress1/arith/issue4985-model-success.smt2
@@ -0,0 +1,7 @@
+(set-logic QF_AUFNRA)
+(set-info :status sat)
+(declare-const arr0 (Array Real Real))
+(declare-const r5 Real)
+(declare-const r19 Real)
+(assert (! (<= 0.0 0.0 48107.0 (- 6.7954749 0.0 6.7954749 0.0 (select arr0 (/ 40.87941 r5))) r19) :named IP_174))
+(check-sat)

diff --git a/test/regress/regress1/arith/issue4985b-model-success.smt2 b/test/regress/regress1/arith/issue4985b-model-success.smt2
new file mode 100644 (file)
index 0000000..eae8d36
--- /dev/null
+++ b/test/regress/regress1/arith/issue4985b-model-success.smt2
@@ -0,0 +1,6 @@
+(set-logic QF_AUFNRA)
+(set-info :status sat)
+(declare-const a (Array Real Real))
+(declare-const r Real)
+(assert (= 1.0 (select a (/ 2 r))))
+(check-sat)

diff --git a/test/regress/regress1/quantifiers/issue5378-witness.smt2 b/test/regress/regress1/quantifiers/issue5378-witness.smt2
new file mode 100644 (file)
index 0000000..b8628a4
--- /dev/null
+++ b/test/regress/regress1/quantifiers/issue5378-witness.smt2
@@ -0,0 +1,5 @@
+; COMMAND-LINE: --sygus-inst --strings-exp
+; EXPECT: unsat
+(set-logic ALL)
+(assert (forall ((a Int) (b Int)) (or (> a (/ 0 b)) (exists ((c Int)) (< a c b)))))
+(check-sat)

diff --git a/test/regress/regress1/strings/issue5520-re-consume.smt2 b/test/regress/regress1/strings/issue5520-re-consume.smt2
new file mode 100644 (file)
index 0000000..3fc4fe8
--- /dev/null
+++ b/test/regress/regress1/strings/issue5520-re-consume.smt2
@@ -0,0 +1,12 @@
+; COMMAND-LINE: --strings-exp
+; EXPECT: sat
+(set-logic QF_S)
+(set-info :status sat)
+(declare-fun x () String)
+(assert
+ (not
+ (str.in_re (str.++ "a" x "ca")
+  (re.*
+  (re.++ (re.union (str.to_re "a") (str.to_re "b"))
+   (re.union (re.* (str.to_re "a")) (str.to_re "b") (str.to_re "c")))))))
+(check-sat)