diff options
5 files changed, 34 insertions, 0 deletions
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) |