From 82a71608588e2cbf7ef581940abccb2f9632eef4 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 15 Oct 2021 17:57:00 -0500 Subject: [PATCH] Add more regressions for fixed issues (#7382) Fixes #6535, Fixes #6475, Fixes #5660, Fixes #6607, Fixes #6638, Fixes #6642, Fixes #6775. --- test/regress/CMakeLists.txt | 7 +++++++ .../push-pop/issue6535-inc-solve.smt2 | 9 ++++++++ .../quantifiers/issue6475-rr-const.smt2 | 8 +++++++ .../regress1/nl/issue5660-mb-success.smt2 | 21 +++++++++++++++++++ .../quantifiers/issue6607-witness-te.smt2 | 5 +++++ .../quantifiers/issue6638-sygus-inst.smt2 | 8 +++++++ .../quantifiers/issue6642-em-types.smt2 | 6 ++++++ .../quantifiers/issue6775-vts-int.smt2 | 19 +++++++++++++++++ 8 files changed, 83 insertions(+) create mode 100644 test/regress/regress0/push-pop/issue6535-inc-solve.smt2 create mode 100644 test/regress/regress0/quantifiers/issue6475-rr-const.smt2 create mode 100644 test/regress/regress1/nl/issue5660-mb-success.smt2 create mode 100644 test/regress/regress1/quantifiers/issue6607-witness-te.smt2 create mode 100644 test/regress/regress1/quantifiers/issue6638-sygus-inst.smt2 create mode 100644 test/regress/regress1/quantifiers/issue6642-em-types.smt2 create mode 100644 test/regress/regress1/quantifiers/issue6775-vts-int.smt2 diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 587b2d9d6..da9c9f001 100644 --- 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 index 000000000..c4a9a770f --- /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 index 000000000..11cc56547 --- /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 index 000000000..6284b0580 --- /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 index 000000000..ff426c139 --- /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 index 000000000..b7cc50885 --- /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 index 000000000..19dc11227 --- /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 index 000000000..39b92a6ad --- /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 -- 2.30.2