From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 25 Nov 2020 19:35:58 +0000 (-0600)
Subject: Add regressions for closed issues (#5526)
X-Git-Tag: cvc5-1.0.0~2551
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8e21ca2de274f82ded4429d21a34741fc1501b1b;p=cvc5.git

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 f66dc2d10..effe70c1c 100644
--- 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
index 000000000..794eefb37
--- /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
index 000000000..eae8d369d
--- /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
index 000000000..b8628a432
--- /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
index 000000000..3fc4fe8e5
--- /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)