From dc23d706d8fa567d40b334dd89289595f5b0961a Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 20 Oct 2021 17:28:52 -0500 Subject: [PATCH] Add regressions for fixed issues (#7421) Fixes #5288, fixes (the 3rd benchmark on) #5741, fixes #6184, fixes #5735, which do not trigger on master. --- test/regress/CMakeLists.txt | 5 +++++ test/regress/regress1/ho/issue5741-3.smt2 | 5 +++++ .../quantifiers/issue5288-vts-real-int.smt2 | 9 +++++++++ .../quantifiers/issue5735-2-subtypes.smt2 | 4 ++++ .../regress1/quantifiers/issue5735-subtypes.smt2 | 6 ++++++ .../regress1/strings/issue6184-unsat-core.smt2 | 15 +++++++++++++++ 6 files changed, 44 insertions(+) create mode 100644 test/regress/regress1/ho/issue5741-3.smt2 create mode 100644 test/regress/regress1/quantifiers/issue5288-vts-real-int.smt2 create mode 100644 test/regress/regress1/quantifiers/issue5735-2-subtypes.smt2 create mode 100644 test/regress/regress1/quantifiers/issue5735-subtypes.smt2 create mode 100644 test/regress/regress1/strings/issue6184-unsat-core.smt2 diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 0f7b19e47..cdd023a17 100644 --- 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 index 000000000..abc4b76a6 --- /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 index 000000000..b36b8cc94 --- /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 index 000000000..76a58bdb7 --- /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 index 000000000..300819007 --- /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 index 000000000..6673dc3b9 --- /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) -- 2.30.2