Add more regressions for fixed issues (#7382)

Fixes #6535, Fixes #6475, Fixes #5660, Fixes #6607, Fixes #6638, Fixes #6642, Fixes #6775.

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 587b2d9d6f6e86905424dbddbeb3bcac60511dec..da9c9f00141aa5544a15cf3a05b909e2b6f91cae 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -877,6 +877,7 @@ set(regress_0_tests
   regress0/push-pop/incremental-subst-bug.cvc.smt2
   regress0/push-pop/issue1986.smt2
   regress0/push-pop/issue2137.min.smt2
+  regress0/push-pop/issue6535-inc-solve.smt2
   regress0/push-pop/quant-fun-proc-unfd.smt2
   regress0/push-pop/real-as-int-incremental.smt2
   regress0/push-pop/simple_unsat_cores.smt2
@@ -919,6 +920,7 @@ set(regress_0_tests
   regress0/quantifiers/issue4576.smt2
   regress0/quantifiers/issue5645-dt-cm-spurious.smt2
   regress0/quantifiers/issue5693-prenex.smt2
+  regress0/quantifiers/issue6475-rr-const.smt2 
   regress0/quantifiers/issue6603-dt-bool-cegqi.smt2
   regress0/quantifiers/issue6838-qpdt.smt2
   regress0/quantifiers/issue6996-trivial-elim.smt2
@@ -1713,6 +1715,7 @@ set(regress_1_tests
   regress1/nl/issue3966-conf-coeff.smt2 
   regress1/nl/issue4791-llr.smt2
   regress1/nl/issue5372-2-no-m-presolve.smt2
+  regress1/nl/issue5660-mb-success.smt2
   regress1/nl/issue5662-nl-tc.smt2
   regress1/nl/issue5662-nl-tc-min.smt2
   regress1/nl/metitarski-1025.smt2
@@ -1904,7 +1907,11 @@ set(regress_1_tests
   regress1/quantifiers/issue5658-qe.smt2
   regress1/quantifiers/issue5766-wrong-sel-trigger.smt2
   regress1/quantifiers/issue5899-qe.smt2
+  regress1/quantifiers/issue6607-witness-te.smt2 
+  regress1/quantifiers/issue6638-sygus-inst.smt2
+  regress1/quantifiers/issue6642-em-types.smt2
   regress1/quantifiers/issue6699-nc-shadow.smt2
+  regress1/quantifiers/issue6775-vts-int.smt2
   regress1/quantifiers/issue6845-nl-lemma-tc.smt2
   regress1/quantifiers/issue993.smt2
   regress1/quantifiers/javafe.ast.StmtVec.009.smt2

diff --git a/test/regress/regress0/push-pop/issue6535-inc-solve.smt2 b/test/regress/regress0/push-pop/issue6535-inc-solve.smt2
new file mode 100644 (file)
index 0000000..c4a9a77
--- /dev/null
+++ b/test/regress/regress0/push-pop/issue6535-inc-solve.smt2
@@ -0,0 +1,9 @@
+; COMMAND-LINE: -i
+; EXPECT: sat
+(set-logic ALL)
+(declare-fun f0_2 (Real Real) Real)
+(declare-fun x8 () Real)
+(assert (= 0.0 (f0_2 x8 1.0)))
+(push)
+(assert (= x8 1.0))
+(check-sat)

diff --git a/test/regress/regress0/quantifiers/issue6475-rr-const.smt2 b/test/regress/regress0/quantifiers/issue6475-rr-const.smt2
new file mode 100644 (file)
index 0000000..11cc565
--- /dev/null
+++ b/test/regress/regress0/quantifiers/issue6475-rr-const.smt2
@@ -0,0 +1,8 @@
+(set-logic ALL)
+(set-info :status sat)
+(set-option :macros-quant true)
+(declare-sort I_fb 0)
+(declare-fun fb_arg_0_1 (I_fb) Int)
+(declare-fun name!0 (I_fb) Int)
+(assert (forall ((?j I_fb)) (! (= (name!0 ?j) (fb_arg_0_1 ?j)) :qid k!9)))
+(check-sat)

diff --git a/test/regress/regress1/nl/issue5660-mb-success.smt2 b/test/regress/regress1/nl/issue5660-mb-success.smt2
new file mode 100644 (file)
index 0000000..6284b05
--- /dev/null
+++ b/test/regress/regress1/nl/issue5660-mb-success.smt2
@@ -0,0 +1,21 @@
+(set-logic QF_AUFNRA)
+(set-info :status sat)
+(declare-fun r2 () Real)
+(declare-fun r9 () Real)
+(declare-fun r13 () Real)
+(declare-fun ufrb5 (Real Real Real Real Real) Bool)
+(declare-fun v3 () Bool)
+(declare-fun v4 () Bool)
+(declare-fun arr0 () (Array Bool Real))
+(declare-fun arr1 () (Array Bool (Array Bool Real)))
+(declare-fun v5 () Bool)
+(declare-fun v7 () Bool)
+(declare-fun v8 () Bool)
+(declare-fun v71 () Bool)
+(declare-fun v81 () Bool)
+(declare-fun v161 () Bool)
+(assert (or v161 (and v3 (not v7))))
+(assert (or v8 (distinct v7 (and v7 v81) (ufrb5 0.0 1.0 0.0 1.0 (/ r13 r9)))))
+(assert (or v161 (distinct v71 v8 (= v4 v81))))
+(assert (or v81 (= arr0 (store (select (store arr1 (xor v81 (and (= r2 1.0) (= r13 1))) arr0) v7) v81 (select (store arr0 v5 1.0) false)))))
+(check-sat)

diff --git a/test/regress/regress1/quantifiers/issue6607-witness-te.smt2 b/test/regress/regress1/quantifiers/issue6607-witness-te.smt2
new file mode 100644 (file)
index 0000000..ff426c1
--- /dev/null
+++ b/test/regress/regress1/quantifiers/issue6607-witness-te.smt2
@@ -0,0 +1,5 @@
+; COMMAND-LINE: --no-check-models
+(set-logic ALL)
+(set-info :status sat)
+(assert (exists ((skoY Real)) (forall ((skoX Real)) (or (= 0.0 (* skoY skoY)) (and (< skoY 0.0) (or (= skoY skoX) (= 2 (* skoY skoY))))))))
+(check-sat)

diff --git a/test/regress/regress1/quantifiers/issue6638-sygus-inst.smt2 b/test/regress/regress1/quantifiers/issue6638-sygus-inst.smt2
new file mode 100644 (file)
index 0000000..b7cc508
--- /dev/null
+++ b/test/regress/regress1/quantifiers/issue6638-sygus-inst.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --sygus-inst --no-check-models
+; EXPECT: sat
+(set-logic ALL)
+(declare-fun b (Int) Int)
+(assert (distinct 0 (ite (exists ((t Int)) (and (forall ((tt Int) (t Int)) (! (or (distinct 0 tt) (> 0 (+ tt t)) (> (+ tt t) 0) (= (b 0) (b t))) :qid k!7)))) 1 (b 0))))
+(check-sat)
+
+; check-models disabled due to intermediate terms from sygus-inst

diff --git a/test/regress/regress1/quantifiers/issue6642-em-types.smt2 b/test/regress/regress1/quantifiers/issue6642-em-types.smt2
new file mode 100644 (file)
index 0000000..19dc112
--- /dev/null
+++ b/test/regress/regress1/quantifiers/issue6642-em-types.smt2
@@ -0,0 +1,6 @@
+; COMMAND-LINE: --full-saturate-quant
+; EXPECT: unsat
+(set-logic ALL)
+(declare-fun b () String)
+(assert (forall ((c (Seq Int))) (exists ((a String)) (and (= 1 (seq.len c)) (not (= b a))))))
+(check-sat)

diff --git a/test/regress/regress1/quantifiers/issue6775-vts-int.smt2 b/test/regress/regress1/quantifiers/issue6775-vts-int.smt2
new file mode 100644 (file)
index 0000000..39b92a6
--- /dev/null
+++ b/test/regress/regress1/quantifiers/issue6775-vts-int.smt2
@@ -0,0 +1,19 @@
+; COMMAND-LINE: -i --no-check-models
+; EXPECT: sat
+; EXPECT: sat
+(set-logic NIA)
+(declare-const x43799 Bool)
+(declare-const x32 Bool)
+(declare-fun v11 () Bool)
+(declare-fun i2 () Int)
+(declare-fun i3 () Int)
+(declare-fun i () Int)
+(assert (or (< 0 i2) (not x32) (not v11)))
+(assert (or x32 (exists ((q Int)) (not (= x32 (> q (abs i3)))))))
+(assert (< i2 i))
+(check-sat)
+(assert (or (not v11) x43799))
+(assert (= (+ 3 i (* 13 4 5 (abs i3))) (* 157 4 (- 1) (+ 1 1 i2 i))))
+(check-sat)
+
+; check-models disabled due to intermediate terms from sygus-inst