diff options
Diffstat (limited to 'test/regress')
33 files changed, 385 insertions, 11 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 8969f8b7a..3ea588e01 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -499,6 +499,7 @@ set(regress_0_tests regress0/datatypes/is_test.smt2 regress0/datatypes/issue1433.smt2 regress0/datatypes/issue2838.cvc.smt2 + regress0/datatypes/issue4393-cdt-model.smt2 regress0/datatypes/issue5280-no-nrec.smt2 regress0/datatypes/jsat-2.6.smt2 regress0/datatypes/list-bool.smt2 @@ -558,6 +559,7 @@ set(regress_0_tests regress0/distinct.smtv1.smt2 regress0/dump-unsat-core-full.smt2 regress0/echo.smt2 + regress0/eqrange0.smt2 regress0/eqrange1.smt2 regress0/eqrange2.smt2 regress0/eqrange3.smt2 @@ -766,10 +768,12 @@ set(regress_0_tests regress0/nl/very-simple-unsat.smt2 regress0/opt-abd-no-use.smt2 regress0/options/ast-and-sexpr.smt2 + regress0/options/interactive-mode.smt2 regress0/options/invalid_dump.smt2 regress0/options/set-after-init.smt2 regress0/options/set-and-get-options.smt2 regress0/options/statistics.smt2 + regress0/options/stream-printing.smt2 regress0/parallel-let.smt2 regress0/parser/as.smt2 regress0/parser/bv_arity_smt2.6.smt2 @@ -780,6 +784,7 @@ set(regress_0_tests regress0/parser/force_logic_set_logic.smt2 regress0/parser/force_logic_success.smt2 regress0/parser/issue5163.smt2 + regress0/parser/issue6908-get-value-uc.smt2 regress0/parser/issue7274.smt2 regress0/parser/linear_arithmetic_err1.smt2 regress0/parser/linear_arithmetic_err2.smt2 @@ -876,6 +881,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 @@ -918,10 +924,12 @@ 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 regress0/quantifiers/issue6999-deq-elim.smt2 + regress0/quantifiers/issue7353-var-elim-par-dt.smt2 regress0/quantifiers/lra-triv-gn.smt2 regress0/quantifiers/macro-back-subs-sat.smt2 regress0/quantifiers/macros-int-real.smt2 @@ -965,6 +973,7 @@ set(regress_0_tests regress0/quantifiers/simp-len.smt2 regress0/quantifiers/simp-typ-test.smt2 regress0/quantifiers/ufnia-fv-delta.smt2 + regress0/quantifiers/veqt-delta.smt2 regress0/rec-fun-const-parse-bug.smt2 regress0/rels/addr_book_0.cvc.smt2 regress0/rels/atom_univ2.cvc.smt2 @@ -1500,6 +1509,8 @@ set(regress_1_tests regress1/arith/issue3952-rew-eq.smt2 regress1/arith/issue4985-model-success.smt2 regress1/arith/issue4985b-model-success.smt2 + regress1/arith/issue6774-sanity-int-model.smt2 + regress1/arith/issue7252-arith-sanity.smt2 regress1/arith/issue789.smt2 regress1/arith/miplib3.cvc.smt2 regress1/arith/mod.02.smt2 @@ -1571,6 +1582,7 @@ set(regress_1_tests regress1/constarr3.cvc.smt2 regress1/constarr3.smt2 regress1/cores/issue5604.smt2 + regress1/cores/issue6988-arith-sanity.smt2 regress1/datatypes/acyclicity-sr-ground096.smt2 regress1/datatypes/cee-prs-small-dd2.smt2 regress1/datatypes/dt-color-2.6.smt2 @@ -1639,8 +1651,11 @@ set(regress_1_tests regress1/fmf/issue4225-univ-fun.smt2 regress1/fmf/issue5738-dt-interp-finite.smt2 regress1/fmf/issue6690-re-enum.smt2 + regress1/fmf/issue6744-2-unc-bool-var.smt2 + regress1/fmf/issue6744-3-unc-bool-var.smt2 regress1/fmf/issue916-fmf-or.smt2 regress1/fmf/jasmin-cdt-crash.smt2 + regress1/fmf/ko-bound-set.cvc.smt2 regress1/fmf/loopy_coda.smt2 regress1/fmf/lst-no-self-rev-exp.smt2 regress1/fmf/memory_model-R_cpp-dd.cvc.smt2 @@ -1662,6 +1677,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 @@ -1680,6 +1696,7 @@ set(regress_1_tests regress1/model-blocker-simple.smt2 regress1/model-blocker-values.smt2 regress1/nl/approx-sqrt.smt2 + regress1/nl/approx-sqrt-unsat.smt2 regress1/nl/arctan2-expdef.smt2 regress1/nl/arrowsmith-050317.smt2 regress1/nl/bad-050217.smt2 @@ -1708,8 +1725,10 @@ set(regress_1_tests regress1/nl/issue3656.smt2 regress1/nl/issue3803-nl-check-model.smt2 regress1/nl/issue3955-ee-double-notify.smt2 + 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 @@ -1753,6 +1772,7 @@ set(regress_1_tests regress1/proofs/issue6625-unsat-core-proofs.smt2 regress1/proofs/macro-res-exp-crowding-lit-inside-unit.smt2 regress1/proofs/macro-res-exp-singleton-after-elimCrowd.smt2 + regress1/proofs/qgu-fuzz-1-strings-pp.smt2 regress1/proofs/quant-alpha-eq.smt2 regress1/proofs/sat-trivial-cycle.smt2 regress1/proofs/unsat-cores-proofs.smt2 @@ -1843,6 +1863,7 @@ set(regress_1_tests regress1/quantifiers/cee-npnt-dd.smt2 regress1/quantifiers/cee-os-delta.smt2 regress1/quantifiers/cdt-0208-to.smt2 + regress1/quantifiers/choice-move-delta-relt.smt2 regress1/quantifiers/const.cvc.smt2 regress1/quantifiers/constfunc.cvc.smt2 regress1/quantifiers/ddatv-delta2.smt2 @@ -1888,6 +1909,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 @@ -1899,9 +1921,16 @@ 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 + 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 regress1/quantifiers/lia-witness-div-pp.smt2 @@ -1947,10 +1976,12 @@ set(regress_1_tests regress1/quantifiers/quaternion_ds1_symm_0428.fof.smt2 regress1/quantifiers/qs-has-term.smt2 regress1/quantifiers/recfact.cvc.smt2 + regress1/quantifiers/rel-trigger-unusable.smt2 regress1/quantifiers/repair-const-nterm.smt2 regress1/quantifiers/rew-to-0211-dd.smt2 regress1/quantifiers/ricart-agrawala6.smt2 regress1/quantifiers/set-choice-koikonomou.cvc.smt2 + regress1/quantifiers/set3.smt2 regress1/quantifiers/set8.smt2 regress1/quantifiers/seu169+1.smt2 regress1/quantifiers/seq-solved-enum.smt2 @@ -1961,6 +1992,7 @@ set(regress_1_tests regress1/quantifiers/smtlib46f14a.smt2 regress1/quantifiers/smtlibe99bbe.smt2 regress1/quantifiers/smtlibf957ea.smt2 + regress1/quantifiers/stream-x2014-09-18-unsat.smt2 regress1/quantifiers/sygus-infer-nested.smt2 regress1/quantifiers/sygus-inst-nia-psyco-060.smt2 regress1/quantifiers/sygus-inst-ufnia-sat-t3_rw1505.smt2 @@ -2179,6 +2211,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 @@ -2195,11 +2228,13 @@ set(regress_1_tests regress1/strings/issue6604-2.smt2 regress1/strings/issue6635-rre.smt2 regress1/strings/issue6653-2-update-c-len.smt2 + regress1/strings/issue6653-3-seq.smt2 regress1/strings/issue6653-4-rre.smt2 regress1/strings/issue6653-rre.smt2 regress1/strings/issue6653-rre-small.smt2 regress1/strings/issue6777-seq-nth-eval-cm.smt2 regress1/strings/issue6913.smt2 + regress1/strings/issue6973-dup-lemma-conc.smt2 regress1/strings/kaluza-fl.smt2 regress1/strings/loop002.smt2 regress1/strings/loop003.smt2 @@ -2251,6 +2286,7 @@ set(regress_1_tests regress1/strings/rev-ex5.smt2 regress1/strings/rew-020618.smt2 regress1/strings/rew-check1.smt2 + regress1/strings/seq-cardinality.smt2 regress1/strings/seq-quant-infinite-branch.smt2 regress1/strings/simple-re-consume.smt2 regress1/strings/stoi-400million.smt2 @@ -2290,6 +2326,7 @@ set(regress_1_tests regress1/sygus/abv.sy regress1/sygus/array-grammar-store.sy regress1/sygus/array_search_5-Q-easy.sy + regress1/sygus/array-uc.sy regress1/sygus/bvudiv-by-2.sy regress1/sygus/cegar1.sy regress1/sygus/cegis-unif-inv-eq-fair.sy @@ -2524,6 +2561,7 @@ set(regress_2_tests regress2/push-pop/DRAGON_4_e2_2799_e3_1915.lus.ic3.1.min.smt2 regress2/quantifiers/AdditiveMethods_AdditiveMethods..ctor.smt2 regress2/quantifiers/cee-event-wrong-sat.smt2 + regress2/quantifiers/exp-trivially-dd3.smt2 regress2/quantifiers/gn-wrong-091018.smt2 regress2/quantifiers/issue3481-unsat1.smt2 regress2/quantifiers/javafe.ast.StandardPrettyPrint.319.smt2 @@ -2702,16 +2740,12 @@ set(regression_disabled_tests ### regress1/bug472.smt2 regress1/datatypes/non-simple-rec-set.smt2 - # TODO: fix models (projects #276) - regress1/fmf/ko-bound-set.cvc.smt2 # results in an assertion failure (see issue #1650). regress1/ho/hoa0102.smt2 # after disallowing solving for terms with quantifiers regress1/ho/nested_lambdas-AGT034^2.smt2 regress1/ho/nested_lambdas-sat-SYO056^1-delta.smt2 regress1/ho/SYO056^1.p - # slow on some builds after changes to tangent planes - regress1/nl/approx-sqrt-unsat.smt2 # times out after update to circuit propagator regress1/nl/dumortier_llibre_artes_ex_5_13.transcendental.k2.smt2 # times out after update to tangent planes @@ -2728,12 +2762,6 @@ set(regression_disabled_tests regress1/quantifiers/macro-subtype-param.smt2 # times out with competition build, ok with other builds: regress1/quantifiers/model_6_1_bv.smt2 - # timeout after changes to nonlinear on PR #5351 - regress1/quantifiers/rel-trigger-unusable.smt2 - # does not terminate/takes a long time when doing a coverage build with LFSC. - regress1/quantifiers/set3.smt2 - # changes to expand definitions, related to trigger selection for selectors - regress1/quantifiers/stream-x2014-09-18-unsat.smt2 # ajreynol: different error messages on production and debug: regress1/quantifiers/subtype-param-unk.smt2 regress1/quantifiers/subtype-param.smt2 @@ -2770,7 +2798,6 @@ set(regression_disabled_tests # previously sygus inference did not apply, now (correctly) times out regress1/sygus/issue3498.smt2 regress2/arith/miplib-opt1217--27.smt2 - regress2/quantifiers/exp-trivially-dd3.smt2 regress2/nl/dumortier-050317.smt2 # timeout on some builds after changes to justification heuristic regress2/nl/nt-lemmas-bad.smt2 diff --git a/test/regress/regress0/datatypes/issue4393-cdt-model.smt2 b/test/regress/regress0/datatypes/issue4393-cdt-model.smt2 new file mode 100644 index 000000000..950cb61a9 --- /dev/null +++ b/test/regress/regress0/datatypes/issue4393-cdt-model.smt2 @@ -0,0 +1,8 @@ +(set-logic QF_DTLIA) +(set-info :status sat) +(declare-codatatypes ((a 0)) (((b (c Int) (d a))))) +(declare-fun e () a) +(declare-fun f () a) +(assert (distinct f (b 0 f))) +(assert (= e f)) +(check-sat) diff --git a/test/regress/regress0/eqrange0.smt2 b/test/regress/regress0/eqrange0.smt2 new file mode 100644 index 000000000..01713d18f --- /dev/null +++ b/test/regress/regress0/eqrange0.smt2 @@ -0,0 +1,6 @@ +; EXPECT: (error "Term of kind EQ_RANGE not supported in default mode, try --arrays-exp") +; EXIT: 1 +(set-logic QF_AUFLIA) +(declare-const a (Array Int Int)) +(assert (eqrange a a 0 0)) +(check-sat) diff --git a/test/regress/regress0/options/interactive-mode.smt2 b/test/regress/regress0/options/interactive-mode.smt2 new file mode 100644 index 000000000..549fdfd24 --- /dev/null +++ b/test/regress/regress0/options/interactive-mode.smt2 @@ -0,0 +1,10 @@ +; EXPECT: true +; EXPECT: true +; EXPECT: false +; EXPECT: false +(set-option :interactive-mode true) +(get-option :interactive-mode) +(get-option :produce-assertions) +(set-option :produce-assertions false) +(get-option :interactive-mode) +(get-option :produce-assertions)
\ No newline at end of file diff --git a/test/regress/regress0/options/stream-printing.smt2 b/test/regress/regress0/options/stream-printing.smt2 new file mode 100644 index 000000000..21ea85aa1 --- /dev/null +++ b/test/regress/regress0/options/stream-printing.smt2 @@ -0,0 +1,18 @@ +; EXPECT: stdout +; EXPECT: stderr +; EXPECT: stdin +; EXPECT-ERROR: stderr +; EXPECT-ERROR: stdout +; EXPECT-ERROR: stdin + +(get-option :regular-output-channel) +(get-option :diagnostic-output-channel) +(get-option :in) + +(set-option :regular-output-channel stderr) +(set-option :diagnostic-output-channel stdout) +(set-option :in stdin) + +(get-option :regular-output-channel) +(get-option :diagnostic-output-channel) +(get-option :in) diff --git a/test/regress/regress0/parser/issue6908-get-value-uc.smt2 b/test/regress/regress0/parser/issue6908-get-value-uc.smt2 new file mode 100644 index 000000000..b6825fe27 --- /dev/null +++ b/test/regress/regress0/parser/issue6908-get-value-uc.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --produce-models +; EXPECT: sat +; EXPECT: (((f (as @uc_Foo_0 Foo)) 3)) +(set-logic ALL) +(set-option :produce-models true) +(declare-sort Foo 0) +(declare-fun f (Foo) Int) +(assert (exists ((x Foo)) (= (f x) 3))) +(check-sat) +(get-value ((f @uc_Foo_0))) 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/regress0/quantifiers/issue7353-var-elim-par-dt.smt2 b/test/regress/regress0/quantifiers/issue7353-var-elim-par-dt.smt2 new file mode 100644 index 000000000..8c9d9eb66 --- /dev/null +++ b/test/regress/regress0/quantifiers/issue7353-var-elim-par-dt.smt2 @@ -0,0 +1,9 @@ +(set-logic ALL) +(set-info :status sat) +(declare-datatype Option (par (T) ((none) (some (extractSome T))))) +(assert + (forall ((x (Option Int))) + (=> (and ((_ is some) x) + (= (extractSome x) 0)) + (= x (some 0))))) +(check-sat) diff --git a/test/regress/regress0/quantifiers/veqt-delta.smt2 b/test/regress/regress0/quantifiers/veqt-delta.smt2 new file mode 100644 index 000000000..dfac015c6 --- /dev/null +++ b/test/regress/regress0/quantifiers/veqt-delta.smt2 @@ -0,0 +1,8 @@ +; COMMAND-LINE: --relational-triggers +; EXPECT: unsat +(set-logic ALL) +(declare-sort S 0) +(declare-fun f () S) +(assert (forall ((? S)) (= ? f))) +(assert (exists ((? S) (v S)) (distinct ? v))) +(check-sat) diff --git a/test/regress/regress1/arith/issue6774-sanity-int-model.smt2 b/test/regress/regress1/arith/issue6774-sanity-int-model.smt2 new file mode 100644 index 000000000..732b709f9 --- /dev/null +++ b/test/regress/regress1/arith/issue6774-sanity-int-model.smt2 @@ -0,0 +1,21 @@ +; COMMAND-LINE: -i -q +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +(set-logic ALIRA) +(declare-const x Real) +(declare-fun i () Int) +(declare-fun i1 () Int) +(push) +(assert (< 1 (- i))) +(check-sat) +(pop) +(push) +(assert (or (>= i1 (* 5 (- i))))) +(check-sat) +(pop) +(assert (or (> i1 1) (= x (to_real i)))) +(check-sat) +(assert (not (is_int x))) +(check-sat) diff --git a/test/regress/regress1/arith/issue7252-arith-sanity.smt2 b/test/regress/regress1/arith/issue7252-arith-sanity.smt2 new file mode 100644 index 000000000..dd7a1fa2e --- /dev/null +++ b/test/regress/regress1/arith/issue7252-arith-sanity.smt2 @@ -0,0 +1,14 @@ +; COMMAND-LINE: -q +; EXPECT: sat +(set-logic ALL) +(set-info :status sat) +(declare-fun a () Int) +(declare-fun b () Int) +(declare-fun c () Int) +(declare-fun d () Int) +(declare-fun e () Int) +(declare-fun f () Int) +(declare-fun g () Int) +(assert (> 0 (* a (mod 0 b)))) +(assert (or (and (> (* b d) (* 2 (+ g c))) (= g (- c)) (> (+ e c) 0)) (> f 0))) +(check-sat) diff --git a/test/regress/regress1/cores/issue6988-arith-sanity.smt2 b/test/regress/regress1/cores/issue6988-arith-sanity.smt2 new file mode 100644 index 000000000..622d64375 --- /dev/null +++ b/test/regress/regress1/cores/issue6988-arith-sanity.smt2 @@ -0,0 +1,18 @@ +; COMMAND-LINE: -i -q +; EXPECT: sat +; EXPECT: sat +(set-logic ANIA) +(declare-const x Bool) +(set-option :produce-unsat-cores true) +(declare-fun i () Int) +(declare-fun i5 () Int) +(declare-fun i8 () Int) +(assert (or x (< i5 0))) +(push) +(assert (and (= i8 1) (= i5 (+ 1 i)) (= i8 (+ 1 i)))) +(push) +(check-sat) +(pop) +(pop) +(assert (= i8 (* i8 3 (+ i8 1)))) +(check-sat) diff --git a/test/regress/regress1/fmf/issue6744-2-unc-bool-var.smt2 b/test/regress/regress1/fmf/issue6744-2-unc-bool-var.smt2 new file mode 100644 index 000000000..024d5b6a3 --- /dev/null +++ b/test/regress/regress1/fmf/issue6744-2-unc-bool-var.smt2 @@ -0,0 +1,7 @@ +(set-logic ALL) +(set-option :finite-model-find true) +(set-info :status sat) +(declare-fun v () Bool) +(declare-fun v2 () Bool) +(assert (exists ((q (Array Bool (Array Bool (Array Int Bool))))) (forall ((q3 (Array Bool (Array Bool (Array Int Bool))))) (xor v2 v2 v v2 (or v2 (not (= q3 q))))))) +(check-sat) diff --git a/test/regress/regress1/fmf/issue6744-3-unc-bool-var.smt2 b/test/regress/regress1/fmf/issue6744-3-unc-bool-var.smt2 new file mode 100644 index 000000000..eb0c35f68 --- /dev/null +++ b/test/regress/regress1/fmf/issue6744-3-unc-bool-var.smt2 @@ -0,0 +1,5 @@ +(set-logic UFC) +(set-info :status sat) +(declare-fun v () Bool) +(assert (and (forall ((q Bool)) (not (xor v (exists ((q Bool)) true) (and (not v) (not q))))))) +(check-sat) 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/nl/issue3966-conf-coeff.smt2 b/test/regress/regress1/nl/issue3966-conf-coeff.smt2 new file mode 100644 index 000000000..7bfbf4140 --- /dev/null +++ b/test/regress/regress1/nl/issue3966-conf-coeff.smt2 @@ -0,0 +1,22 @@ +(set-logic QF_UFNIA) +(set-info :status sat) +(set-option :nl-ext-ent-conf true) +(declare-const v0 Bool) +(declare-const v1 Bool) +(declare-const v2 Bool) +(declare-const v3 Bool) +(declare-const i0 Int) +(declare-const i1 Int) +(declare-const i2 Int) +(declare-const i4 Int) +(declare-const i5 Int) +(declare-const i9 Int) +(declare-const i10 Int) +(declare-const i12 Int) +(declare-const i13 Int) +(assert v0) +(declare-sort S0 0) +(declare-const v4 Bool) +(assert (xor v2 v1 (> i12 i2) (and v3 v3) (> i12 i2) v4 v2 v1 v0 v3)) +(assert (xor (<= 52 (div 15 (- i1 84 i0 99 i5))) v4 (=> v4 (>= i5 88)) (> i12 i2) (and v3 v3) (<= 52 (div 15 (- i1 84 i0 99 i5))) v1 (> i12 i2) (distinct i0 615) v0)) +(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/proofs/qgu-fuzz-1-strings-pp.smt2 b/test/regress/regress1/proofs/qgu-fuzz-1-strings-pp.smt2 new file mode 100644 index 000000000..c0c1f16f7 --- /dev/null +++ b/test/regress/regress1/proofs/qgu-fuzz-1-strings-pp.smt2 @@ -0,0 +1,5 @@ +(set-logic ALL) +(set-info :status unsat) +(declare-fun x () String) +(assert (let ((_let_1 (str.to_re "B"))) (and (str.in_re x (re.++ re.allchar (str.to_re (str.++ "B" "A")))) (str.in_re x (re.* (re.union re.allchar (str.to_re "A")))) (str.in_re x (re.* (re.union re.allchar _let_1))) (str.in_re x (re.* (re.++ re.allchar _let_1)))))) +(check-sat) diff --git a/test/regress/regress1/quantifiers/choice-move-delta-relt.smt2 b/test/regress/regress1/quantifiers/choice-move-delta-relt.smt2 new file mode 100644 index 000000000..a8fd0d498 --- /dev/null +++ b/test/regress/regress1/quantifiers/choice-move-delta-relt.smt2 @@ -0,0 +1,6 @@ +; COMMAND-LINE: --relational-triggers --user-pat=use +; EXPECT: unsat +(set-logic ALL) +(declare-fun F (Int) Bool) +(assert (forall ((v Int)) (! (= (F 0) (< v 0)) :qid |outputbpl.194:24| :pattern ((F 0))))) +(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/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 diff --git a/test/regress/regress1/quantifiers/issue6845-nl-lemma-tc.smt2 b/test/regress/regress1/quantifiers/issue6845-nl-lemma-tc.smt2 new file mode 100644 index 000000000..087137653 --- /dev/null +++ b/test/regress/regress1/quantifiers/issue6845-nl-lemma-tc.smt2 @@ -0,0 +1,15 @@ +; COMMAND-LINE: -i +; EXPECT: sat +; EXPECT: sat +(set-logic NIRA) +(declare-const x Bool) +(declare-fun i () Int) +(declare-fun i1 () Int) +(assert (< 1.0 (to_real i))) +(assert (distinct 0 (/ 7 (to_real i)))) +(push) +(assert (or (exists ((q Int)) (= 0 (* i i1))))) +(check-sat) +(pop) +(assert (or (= i1 1) x)) +(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) diff --git a/test/regress/regress1/strings/issue6653-3-seq.smt2 b/test/regress/regress1/strings/issue6653-3-seq.smt2 new file mode 100644 index 000000000..a48fc7664 --- /dev/null +++ b/test/regress/regress1/strings/issue6653-3-seq.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: -q +; EXPECT: sat +(set-logic QF_SLIA) +(set-info :status sat) +(set-option :strings-lazy-pp false) +(declare-fun z () Int) +(declare-fun a () (Seq Int)) +(assert (not (= (seq.nth a 1) (seq.nth a z)))) +(assert (= z (- 1))) +(check-sat) diff --git a/test/regress/regress1/strings/issue6973-dup-lemma-conc.smt2 b/test/regress/regress1/strings/issue6973-dup-lemma-conc.smt2 new file mode 100644 index 000000000..4c6fe5c62 --- /dev/null +++ b/test/regress/regress1/strings/issue6973-dup-lemma-conc.smt2 @@ -0,0 +1,15 @@ +(set-logic QF_SLIA) +(set-info :status unsat) +(declare-fun a () String) +(assert + (str.in_re "" + (re.++ (re.diff (re.comp re.all) (re.++ (str.to_re a) (re.comp re.all))) + (str.to_re + (ite + (str.in_re "" + (re.++ (str.to_re (ite (str.in_re "" (re.++ (str.to_re a) (re.comp re.all))) a "")) + (re.inter (str.to_re a) + (re.++ (str.to_re a) + (re.comp (re.union (re.++ (str.to_re a) (re.comp re.all)) re.all)))))) + a ""))))) +(check-sat) diff --git a/test/regress/regress1/strings/seq-cardinality.smt2 b/test/regress/regress1/strings/seq-cardinality.smt2 new file mode 100644 index 000000000..93a4985d4 --- /dev/null +++ b/test/regress/regress1/strings/seq-cardinality.smt2 @@ -0,0 +1,11 @@ +(set-logic ALL) +(set-info :status unsat) +(declare-fun x () (Seq (_ BitVec 1))) +(declare-fun y () (Seq (_ BitVec 1))) +(declare-fun z () (Seq (_ BitVec 1))) + +(assert (= (seq.len x) 1)) +(assert (= (seq.len y) 1)) +(assert (= (seq.len z) 1)) +(assert (distinct x y z)) +(check-sat) diff --git a/test/regress/regress1/sygus/array-uc.sy b/test/regress/regress1/sygus/array-uc.sy new file mode 100644 index 000000000..b3d950436 --- /dev/null +++ b/test/regress/regress1/sygus/array-uc.sy @@ -0,0 +1,14 @@ +; COMMAND-LINE: --sygus-out=status +; EXPECT: unsat +(set-logic ALL) +(declare-sort U 0) +(synth-fun f ((x (Array U Int)) (y U)) Bool) + +(declare-var x (Array U Int)) +(declare-var y U) + +(constraint (= (f (store x y 0) y) true)) +(constraint (= (f (store x y 1) y) false)) + +; f can be (= (select x y) 0) +(check-synth) |