Add regressions for fixed issues (#7421)

Fixes #5288, fixes (the 3rd benchmark on) #5741, fixes #6184, fixes #5735, which do not trigger on master.

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 0f7b19e47f22f6f2d84cf5228defe6a188674acf..cdd023a17f20765b933fb29eab31bea87aa87d5b 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1674,6 +1674,7 @@ set(regress_1_tests
   regress1/ho/issue4065-no-rep.smt2
   regress1/ho/issue4092-sinf.smt2
   regress1/ho/issue4134-sinf.smt2
+  regress1/ho/issue5741-3.smt2
   regress1/ho/NUM638^1.smt2
   regress1/ho/NUM925^1.p
   regress1/ho/soundness_fmf_SYO362^5-delta.p
@@ -1904,6 +1905,7 @@ set(regress_1_tests
   regress1/quantifiers/issue4849-nqe.smt2
   regress1/quantifiers/issue5019-cegqi-i.smt2
   regress1/quantifiers/issue5279-nqe.smt2
+  regress1/quantifiers/issue5288-vts-real-int.smt2
   regress1/quantifiers/issue5365-nqe.smt2
   regress1/quantifiers/issue5378-witness.smt2
   regress1/quantifiers/issue5469-aext.smt2
@@ -1915,6 +1917,8 @@ set(regress_1_tests
   regress1/quantifiers/issue5506-qe.smt2
   regress1/quantifiers/issue5507-qe.smt2
   regress1/quantifiers/issue5658-qe.smt2
+  regress1/quantifiers/issue5735-subtypes.smt2
+  regress1/quantifiers/issue5735-2-subtypes.smt2
   regress1/quantifiers/issue5766-wrong-sel-trigger.smt2
   regress1/quantifiers/issue5899-qe.smt2
   regress1/quantifiers/issue6607-witness-te.smt2 
@@ -2200,6 +2204,7 @@ set(regress_1_tests
   regress1/strings/issue6101-2.smt2
   regress1/strings/issue6132-non-unique-skolem.smt2
   regress1/strings/issue6142-repl-inv-rew.smt2
+  regress1/strings/issue6184-unsat-core.smt2 
   regress1/strings/issue6191-replace-all.smt2
   regress1/strings/issue6203-1-substr-ctn-strip.smt2
   regress1/strings/issue6203-2-re-ccache.smt2

diff --git a/test/regress/regress1/ho/issue5741-3.smt2 b/test/regress/regress1/ho/issue5741-3.smt2
new file mode 100644 (file)
index 0000000..abc4b76
--- /dev/null
+++ b/test/regress/regress1/ho/issue5741-3.smt2
@@ -0,0 +1,5 @@
+(set-logic HO_ALL)
+(set-info :status sat)
+(declare-fun p ((_ BitVec 17) (_ BitVec 16)) Bool)
+(assert (p (_ bv0 17) ((_ sign_extend 15) (ite (p (_ bv0 17) (_ bv0 16)) (_ bv1 1) (_ bv0 1)))))
+(check-sat)

diff --git a/test/regress/regress1/quantifiers/issue5288-vts-real-int.smt2 b/test/regress/regress1/quantifiers/issue5288-vts-real-int.smt2
new file mode 100644 (file)
index 0000000..b36b8cc
--- /dev/null
+++ b/test/regress/regress1/quantifiers/issue5288-vts-real-int.smt2
@@ -0,0 +1,9 @@
+; COMMAND-LINE: --strings-exp
+; EXPECT: unsat
+(set-logic ALL)
+(set-info :status unsat)
+(assert
+ (forall ((a Int) (b Int))
+ (or (< a (/ 3 b (- 2)))
+  (forall ((c Int)) (or (<= c b) (>= c a))))))
+(check-sat)

diff --git a/test/regress/regress1/quantifiers/issue5735-2-subtypes.smt2 b/test/regress/regress1/quantifiers/issue5735-2-subtypes.smt2
new file mode 100644 (file)
index 0000000..76a58bd
--- /dev/null
+++ b/test/regress/regress1/quantifiers/issue5735-2-subtypes.smt2
@@ -0,0 +1,4 @@
+(set-logic ALL)
+(set-info :status unsat)
+(assert (forall ((a Real)) (exists ((b Int)) (= (exists ((c Int)) (<= a c (+ a 1))) (and (>= b (/ a (+ a 1))) (< 1 (+ a 1)))))))
+(check-sat)

diff --git a/test/regress/regress1/quantifiers/issue5735-subtypes.smt2 b/test/regress/regress1/quantifiers/issue5735-subtypes.smt2
new file mode 100644 (file)
index 0000000..3008190
--- /dev/null
+++ b/test/regress/regress1/quantifiers/issue5735-subtypes.smt2
@@ -0,0 +1,6 @@
+(set-logic ALL)
+(set-info :status unsat)
+(declare-fun a () Bool)
+(assert (forall ((b Int) (c Bool) (d Int))
+(or (= d (/ 1 (ite c 9 0))) (<= (ite a 1 b) (/ 1 (ite c 9 0))))))
+(check-sat)

diff --git a/test/regress/regress1/strings/issue6184-unsat-core.smt2 b/test/regress/regress1/strings/issue6184-unsat-core.smt2
new file mode 100644 (file)
index 0000000..6673dc3
--- /dev/null
+++ b/test/regress/regress1/strings/issue6184-unsat-core.smt2
@@ -0,0 +1,15 @@
+; COMMAND-LINE: --strings-exp
+; EXPECT: unsat
+(set-logic ALL)
+(set-info :status unsat)
+(set-option :check-unsat-cores true)
+(declare-fun i8 () Int)
+(declare-fun st6 () (Set String))
+(declare-fun st8 () (Set String))
+(declare-fun str6 () String)
+(declare-fun str7 () String)
+(assert (= 0 (card st8)))
+(assert (str.in_re str6 (re.opt re.none)))
+(assert (str.in_re (str.substr str7 0 i8) re.allchar))
+(assert (xor true (subset st8 st6) (not (= str7 str6)) true))
+(check-sat)