diff options
Diffstat (limited to 'test/regress')
33 files changed, 178 insertions, 73 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 2529a8622..da7c40bc2 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -237,7 +237,6 @@ set(regress_0_tests regress0/bv/bug440.smtv1.smt2 regress0/bv/bug733.smt2 regress0/bv/bug734.smt2 - regress0/bv/bv-abstr-bug.smt2 regress0/bv/bv-abstr-bug2.smt2 regress0/bv/bv-int-collapse1.smt2 regress0/bv/bv-int-collapse2.smt2 @@ -614,6 +613,7 @@ set(regress_0_tests regress0/fp/issue5734.smt2 regress0/fp/issue6164.smt2 regress0/fp/issue7002.smt2 + regress0/fp/proj-issue329-prereg-context.smt2 regress0/fp/rti_3_5_bug.smt2 regress0/fp/simple.smt2 regress0/fp/word-blast.smt2 @@ -661,6 +661,7 @@ set(regress_0_tests regress0/ho/match-middle.smt2 regress0/ho/modulo-func-equality.smt2 regress0/ho/qgu-fuzz-ho-1-dd.smt2 + regress0/ho/qgu-fuzz-ho-2-dd-no-ext.smt2 regress0/ho/shadowing-defs.smt2 regress0/ho/simple-matching-partial.smt2 regress0/ho/simple-matching.smt2 @@ -846,6 +847,7 @@ set(regress_0_tests regress0/preprocess/proj-issue305-circuit-prop-ite-c.smt2 regress0/preprocess/proj-issue305-circuit-prop-ite-d.smt2 regress0/preprocess/proj-issue309-circuit-prop-ite.smt2 + regress0/preprocess/proj-issue332-circuit-prop-xor.smt2 regress0/print_define_fun_internal.smt2 regress0/print_lambda.cvc.smt2 regress0/print_model.cvc.smt2 @@ -864,6 +866,8 @@ set(regress_0_tests regress0/proofs/open-pf-if-unordered-iff.smt2 regress0/proofs/open-pf-rederivation.smt2 regress0/proofs/project-issue317-inc-sat-conflictlit.smt2 + regress0/proofs/project-issue330-eqproof.smt2 + regress0/proofs/proj-issue326-nl-bounds-check.smt2 regress0/proofs/qgu-fuzz-1-bool-sat.smt2 regress0/proofs/qgu-fuzz-2-bool-chainres-checking.smt2 regress0/proofs/qgu-fuzz-3-chainres-checking.smt2 @@ -1033,7 +1037,6 @@ set(regress_0_tests regress0/rels/rel_tc_2_1.cvc.smt2 regress0/rels/rel_tc_3_1.cvc.smt2 regress0/rels/rel_tc_3.cvc.smt2 - regress0/rels/rel_tc_7.cvc.smt2 regress0/rels/rel_tc_8.cvc.smt2 regress0/rels/rel_tp_3_1.cvc.smt2 regress0/rels/rel_tp_join_0.cvc.smt2 @@ -1586,6 +1589,9 @@ set(regress_1_tests regress1/bags/emptybag1.smt2 regress1/bags/fuzzy1.smt2 regress1/bags/fuzzy2.smt2 + regress1/bags/fuzzy3.smt2 + regress1/bags/fuzzy4.smt2 + regress1/bags/fuzzy5.smt2 regress1/bags/intersection_min1.smt2 regress1/bags/intersection_min2.smt2 regress1/bags/issue5759.smt2 @@ -1618,7 +1624,6 @@ set(regress_1_tests regress1/bv/issue3776.smt2 regress1/bv/issue3958.smt2 regress1/bv/min-pp-rewrite-error.smt2 - regress1/bv/test-bv-abstraction.smt2 regress1/bv/unsound1.smt2 regress1/bvdiv2.smt2 regress1/cee-bug0909-dd-scope.smt2 @@ -1953,6 +1958,7 @@ set(regress_1_tests regress1/quantifiers/issue4433-nqe.smt2 regress1/quantifiers/issue4620-erq-witness-unsound.smt2 regress1/quantifiers/issue4685-wrewrite.smt2 + regress1/quantifiers/issue4813-qe-quant.smt2 regress1/quantifiers/issue4849-nqe.smt2 regress1/quantifiers/issue5019-cegqi-i.smt2 regress1/quantifiers/issue5279-nqe.smt2 @@ -1979,6 +1985,7 @@ set(regress_1_tests regress1/quantifiers/issue6775-vts-int.smt2 regress1/quantifiers/issue6845-nl-lemma-tc.smt2 regress1/quantifiers/issue7385-sygus-inst-i.smt2 + regress1/quantifiers/issue7537-cegqi-comp-types.smt2 regress1/quantifiers/issue993.smt2 regress1/quantifiers/javafe.ast.StmtVec.009.smt2 regress1/quantifiers/lia-witness-div-pp.smt2 @@ -2068,6 +2075,8 @@ set(regress_1_tests regress1/rels/joinImg_2_1.cvc.smt2 regress1/rels/prod-mod-eq.cvc.smt2 regress1/rels/prod-mod-eq2.cvc.smt2 + regress1/rels/qgu-fuzz-relations-2.smt2 + regress1/rels/qgu-fuzz-relations-3-upwards.smt2 regress1/rels/rel_complex_3.cvc.smt2 regress1/rels/rel_complex_4.cvc.smt2 regress1/rels/rel_complex_5.cvc.smt2 @@ -2312,6 +2321,7 @@ set(regress_1_tests regress1/strings/policy_variable.smt2 regress1/strings/pre_ctn_no_skolem_share.smt2 regress1/strings/proj254-re-elim-agg.smt2 + regress1/strings/proj-issue331.smt2 regress1/strings/query4674.smt2 regress1/strings/query8485.smt2 regress1/strings/re-all-char-hard.smt2 @@ -2768,6 +2778,8 @@ set(regression_disabled_tests regress0/auflia/fuzz01.smtv1.smt2 ### regress0/bv/test00.smtv1.smt2 + # timeout after fixing upwards closure for relations + regress0/rels/rel_tc_7.cvc.smt2 # timeout after changes to equality rewriting policy in strings regress0/strings/quad-028-2-2-unsat.smt2 # FIXME #1649 diff --git a/test/regress/regress0/bug522.smt2 b/test/regress/regress0/bug522.smt2 index 3a9ea0eaa..ad6e526a8 100644 --- a/test/regress/regress0/bug522.smt2 +++ b/test/regress/regress0/bug522.smt2 @@ -1,6 +1,6 @@ ; EXPECT: sat ; EXPECT: sat -(set-option :incremental "true") +(set-option :incremental true) (set-logic QF_UF) (push 1) diff --git a/test/regress/regress0/bv/bv-abstr-bug.smt2 b/test/regress/regress0/bv/bv-abstr-bug.smt2 deleted file mode 100644 index cc38075a9..000000000 --- a/test/regress/regress0/bv/bv-abstr-bug.smt2 +++ /dev/null @@ -1,16 +0,0 @@ -; COMMAND-LINE: --bv-abstraction --bitblast=eager -; -; BV-abstraction should not be applied -(set-logic QF_BV) -(set-info :status sat) -(declare-const a Bool) -(declare-const b Bool) -(declare-const c Bool) -(declare-const d Bool) -(assert - (or - (and a b) - (and c d) - ) -) -(check-sat) diff --git a/test/regress/regress0/bv/test-bv_intro_pow2.smt2 b/test/regress/regress0/bv/test-bv_intro_pow2.smt2 index e89dd4c50..65471a6b9 100644 --- a/test/regress/regress0/bv/test-bv_intro_pow2.smt2 +++ b/test/regress/regress0/bv/test-bv_intro_pow2.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --bv-intro-pow2 --no-check-unsat-cores --bv-solver=layered +; COMMAND-LINE: --bv-intro-pow2 --no-check-unsat-cores (set-info :smt-lib-version 2.6) (set-logic QF_BV) (set-info :status unsat) diff --git a/test/regress/regress0/fmf/cruanes-no-minimal-unk.smt2 b/test/regress/regress0/fmf/cruanes-no-minimal-unk.smt2 index f38a3ce41..6ce1c41cd 100644 --- a/test/regress/regress0/fmf/cruanes-no-minimal-unk.smt2 +++ b/test/regress/regress0/fmf/cruanes-no-minimal-unk.smt2 @@ -4,7 +4,7 @@ ; generated by Nunchaku (declare-sort i_ 0) (declare-fun __nun_card_witness_0_ () i_) -(assert (fmf.card __nun_card_witness_0_ 2)) +(assert (_ fmf.card i_ 2)) (declare-fun i2_ () i_) (declare-fun i1_ () i_) (declare-fun i3_ () i_) diff --git a/test/regress/regress0/fmf/fc-simple.smt2 b/test/regress/regress0/fmf/fc-simple.smt2 index d1fd2301c..26c9b423f 100644 --- a/test/regress/regress0/fmf/fc-simple.smt2 +++ b/test/regress/regress0/fmf/fc-simple.smt2 @@ -6,7 +6,7 @@ (declare-fun a () U) (declare-fun c () U) -(assert (fmf.card c 2)) -(assert (not (fmf.card a 4))) +(assert (_ fmf.card U 2)) +(assert (not (_ fmf.card U 4))) (check-sat) diff --git a/test/regress/regress0/fmf/fc-unsat-pent.smt2 b/test/regress/regress0/fmf/fc-unsat-pent.smt2 index 2d4000e6e..b07c53077 100644 --- a/test/regress/regress0/fmf/fc-unsat-pent.smt2 +++ b/test/regress/regress0/fmf/fc-unsat-pent.smt2 @@ -15,6 +15,6 @@ (assert (not (= d e))) (assert (not (= e a))) -(assert (fmf.card c 2)) +(assert (_ fmf.card U 2)) -(check-sat)
\ No newline at end of file +(check-sat) diff --git a/test/regress/regress0/fmf/fc-unsat-tot-2.smt2 b/test/regress/regress0/fmf/fc-unsat-tot-2.smt2 index 0d438f718..404b3abea 100644 --- a/test/regress/regress0/fmf/fc-unsat-tot-2.smt2 +++ b/test/regress/regress0/fmf/fc-unsat-tot-2.smt2 @@ -7,8 +7,8 @@ (declare-fun b () U) (declare-fun c () U) -(assert (not (fmf.card a 2))) +(assert (not (_ fmf.card U 2))) (assert (forall ((x U)) (or (= x a) (= x b)))) -(check-sat)
\ No newline at end of file +(check-sat) diff --git a/test/regress/regress0/fmf/issue4850-force-card.smt2 b/test/regress/regress0/fmf/issue4850-force-card.smt2 index 5aa7fc894..465584a83 100644 --- a/test/regress/regress0/fmf/issue4850-force-card.smt2 +++ b/test/regress/regress0/fmf/issue4850-force-card.smt2 @@ -2,5 +2,5 @@ (set-info :status sat) (declare-sort a 0) (declare-fun b () a) -(assert (not (fmf.card b 1))) +(assert (not (_ fmf.card a 1))) (check-sat) diff --git a/test/regress/regress0/fmf/issue4872-qf_ufc.smt2 b/test/regress/regress0/fmf/issue4872-qf_ufc.smt2 index c46bc1e28..c265dddcd 100644 --- a/test/regress/regress0/fmf/issue4872-qf_ufc.smt2 +++ b/test/regress/regress0/fmf/issue4872-qf_ufc.smt2 @@ -2,6 +2,6 @@ (set-info :status sat) (declare-sort S0 0) (declare-const S0-0 S0) -(assert (fmf.card S0-0 1)) -(assert (fmf.card S0-0 4)) +(assert (_ fmf.card S0 1)) +(assert (_ fmf.card S0 4)) (check-sat) diff --git a/test/regress/regress0/fmf/issue5239-uf-ss-tot.smt2 b/test/regress/regress0/fmf/issue5239-uf-ss-tot.smt2 index a92f2f441..d032114ac 100644 --- a/test/regress/regress0/fmf/issue5239-uf-ss-tot.smt2 +++ b/test/regress/regress0/fmf/issue5239-uf-ss-tot.smt2 @@ -2,5 +2,5 @@ (set-info :status sat) (declare-sort a 0) (declare-fun b () a) -(assert (fmf.card b 2)) +(assert (_ fmf.card a 2)) (check-sat) diff --git a/test/regress/regress0/fp/proj-issue329-prereg-context.smt2 b/test/regress/regress0/fp/proj-issue329-prereg-context.smt2 new file mode 100644 index 000000000..f32a4ed33 --- /dev/null +++ b/test/regress/regress0/fp/proj-issue329-prereg-context.smt2 @@ -0,0 +1,7 @@ +; COMMAND-LINE: --fp-exp +; EXPECT: sat +(set-logic ALL) +(declare-const x Float128) +(declare-const _x String) +(declare-fun x5 (Bool Float128) Bool) +(check-sat-assuming ((x5 (exists ((x (Array String Bool))) (and (select x _x) (or (select x _x) (x5 (exists ((x Bool)) true) (_ -oo 15 113))))) x))) diff --git a/test/regress/regress0/ho/qgu-fuzz-ho-2-dd-no-ext.smt2 b/test/regress/regress0/ho/qgu-fuzz-ho-2-dd-no-ext.smt2 new file mode 100644 index 000000000..7dc3188f2 --- /dev/null +++ b/test/regress/regress0/ho/qgu-fuzz-ho-2-dd-no-ext.smt2 @@ -0,0 +1,10 @@ +(set-logic HO_ALL) +(set-info :status sat) +(declare-const x6 Bool) +(declare-const x Int) +(declare-const b (-> Int Int Int)) +(declare-const c (-> Int Int)) +(assert (> (b 1 0) 0)) +(assert (= (c 0) (b 0 1))) +(assert(= c (ite x6 (b 1) (b (+ 1 x))))) +(check-sat) diff --git a/test/regress/regress0/issue5550-num-children.smt2 b/test/regress/regress0/issue5550-num-children.smt2 index 75810699b..62d078b32 100644 --- a/test/regress/regress0/issue5550-num-children.smt2 +++ b/test/regress/regress0/issue5550-num-children.smt2 @@ -2,5 +2,5 @@ (set-logic UFC) (declare-sort a 0) (declare-fun b () a) -(assert (not (fmf.card b 1))) -(check-sat)
\ No newline at end of file +(assert (not (_ fmf.card a 1))) +(check-sat) diff --git a/test/regress/regress0/options/ast-and-sexpr.smt2 b/test/regress/regress0/options/ast-and-sexpr.smt2 index 2a464571c..41012f888 100644 --- a/test/regress/regress0/options/ast-and-sexpr.smt2 +++ b/test/regress/regress0/options/ast-and-sexpr.smt2 @@ -13,5 +13,6 @@ (get-option :command-verbosity) ; There is no SMT option to get the verbosity of a specific command -(set-info :source (0 1 True False x "")) +(set-info :source (true false (- 15) 15 15.0 #b00001111 #x0f x |x +"| "" """")) (get-info :status) diff --git a/test/regress/regress0/preprocess/issue5729-rewritten-assertions.smt2 b/test/regress/regress0/preprocess/issue5729-rewritten-assertions.smt2 index 56d8bc107..a4c3c29f6 100644 --- a/test/regress/regress0/preprocess/issue5729-rewritten-assertions.smt2 +++ b/test/regress/regress0/preprocess/issue5729-rewritten-assertions.smt2 @@ -1,6 +1,5 @@ -; COMMAND-LINE: --no-bv-eq-solver ; EXPECT: sat (set-logic QF_ALL) (declare-fun x () (_ BitVec 1)) (assert (= (_ bv0 1) ((_ int2bv 1) (bv2nat x)))) -(check-sat)
\ No newline at end of file +(check-sat) diff --git a/test/regress/regress0/preprocess/proj-issue332-circuit-prop-xor.smt2 b/test/regress/regress0/preprocess/proj-issue332-circuit-prop-xor.smt2 new file mode 100644 index 000000000..841e7392b --- /dev/null +++ b/test/regress/regress0/preprocess/proj-issue332-circuit-prop-xor.smt2 @@ -0,0 +1,9 @@ +; EXPECT: sat +(set-logic ALL) +(set-option :check-proofs true) +(declare-const x Real) +(declare-const x4 Real) +(declare-const x8 Bool) +(assert (<= x4 x)) +(assert (not (xor (> x4 x) x8))) +(check-sat) diff --git a/test/regress/regress0/proofs/proj-issue326-nl-bounds-check.smt2 b/test/regress/regress0/proofs/proj-issue326-nl-bounds-check.smt2 new file mode 100644 index 000000000..bc10e9cac --- /dev/null +++ b/test/regress/regress0/proofs/proj-issue326-nl-bounds-check.smt2 @@ -0,0 +1,13 @@ +; EXPECT: unknown +(set-logic ALL) +(set-option :check-proofs true) +(set-option :proof-check eager) +(declare-const x Real) +(assert + (and + (< 1.0 x) + (<= x (/ 0.0 0.0 x)) + (<= (/ 0.0 0.0 x) x) + ) +) +(check-sat) diff --git a/test/regress/regress0/proofs/project-issue330-eqproof.smt2 b/test/regress/regress0/proofs/project-issue330-eqproof.smt2 new file mode 100644 index 000000000..1da778205 --- /dev/null +++ b/test/regress/regress0/proofs/project-issue330-eqproof.smt2 @@ -0,0 +1,7 @@ +; EXPECT: sat +(set-logic QF_SLIA) +(declare-const x String) +(declare-const x1 Int) +(set-option :check-proofs true) +(declare-const _x String) +(check-sat-assuming ((>= 0 (ite (= x (str.++ (str.from_code 0) (str.replace_all x (str.from_code 0) (str.++ (str.from_code 0) (str.from_code 0))) _x) (ite false x (str.++ _x _x _x)) x) x1 0))))
\ No newline at end of file diff --git a/test/regress/regress0/push-pop/inc-define.smt2 b/test/regress/regress0/push-pop/inc-define.smt2 index 27261eff6..57f4d711c 100644 --- a/test/regress/regress0/push-pop/inc-define.smt2 +++ b/test/regress/regress0/push-pop/inc-define.smt2 @@ -4,6 +4,6 @@ (set-logic QF_LIA) (declare-fun x () Int) (check-sat) -(define t (not (= x 0))) +(define-const t Bool (not (= x 0))) (assert t) (check-sat) diff --git a/test/regress/regress0/smtlib/issue4552.smt2 b/test/regress/regress0/smtlib/issue4552.smt2 index af8e0b948..8fcfabd5e 100644 --- a/test/regress/regress0/smtlib/issue4552.smt2 +++ b/test/regress/regress0/smtlib/issue4552.smt2 @@ -6,8 +6,8 @@ (set-option :global-declarations true) (push) -(define a true) -(define (f (b Bool)) b) +(define-const a Bool true) +(define-fun f ((b Bool)) Bool b) (define-const a2 Bool true) (define-fun a3 () Bool true) diff --git a/test/regress/regress1/bags/fuzzy3.smt2 b/test/regress/regress1/bags/fuzzy3.smt2 new file mode 100644 index 000000000..dd6dd02dc --- /dev/null +++ b/test/regress/regress1/bags/fuzzy3.smt2 @@ -0,0 +1,13 @@ +(set-logic ALL) +(set-info :status sat) +(set-option :produce-models true) +(declare-fun A () (Bag (Tuple Int Int))) +(declare-fun B () (Bag (Tuple Int Int))) +(declare-fun c () Int) +(declare-fun d () (Tuple Int Int)) +(assert + (not + (= + (= A (difference_remove (bag d c) A)) + (= A (bag (tuple c c) c))))) +(check-sat) diff --git a/test/regress/regress1/bags/fuzzy4.smt2 b/test/regress/regress1/bags/fuzzy4.smt2 new file mode 100644 index 000000000..b733a4862 --- /dev/null +++ b/test/regress/regress1/bags/fuzzy4.smt2 @@ -0,0 +1,15 @@ +(set-logic ALL) +(set-option :produce-models true) +(set-info :status sat) +(declare-fun A () (Bag (Tuple Int Int))) +(declare-fun c () Int) +(declare-fun d () (Tuple Int Int)) +(assert + (not + (= + (= A (bag d (+ c (bag.count d (union_disjoint A A))))) + (= A (difference_remove (bag d c) A))))) +(assert (= A (bag (tuple 0 0) 5))) +(assert (= c (- 5))) +(assert (= d (tuple 0 0))) +(check-sat) diff --git a/test/regress/regress1/bags/fuzzy5.smt2 b/test/regress/regress1/bags/fuzzy5.smt2 new file mode 100644 index 000000000..2dea236a5 --- /dev/null +++ b/test/regress/regress1/bags/fuzzy5.smt2 @@ -0,0 +1,21 @@ +(set-logic ALL) +(set-option :produce-models true) +(set-info :status sat) +(declare-fun A () (Bag (Tuple Int Int))) +(declare-fun c () Int) +(declare-fun d () (Tuple Int Int)) + +(assert + (let ((c_plus_1 (+ c 1))) + (and + (not + (= (= A (bag (tuple 0 c) (+ c c))) + (= A (difference_remove (bag d c) A)))) + (not + (= (= A (bag (tuple 0 1) c_plus_1)) + (= A (bag (tuple c 1) c_plus_1))))))) + +;(assert (= A (bag (tuple 0 1) 2))) +;(assert (= c 1)) +;(assert (= d (tuple 0 1))) +(check-sat)
\ No newline at end of file diff --git a/test/regress/regress1/bv/test-bv-abstraction.smt2 b/test/regress/regress1/bv/test-bv-abstraction.smt2 deleted file mode 100644 index 7a926d4be..000000000 --- a/test/regress/regress1/bv/test-bv-abstraction.smt2 +++ /dev/null @@ -1,24 +0,0 @@ -; COMMAND-LINE: --bv-abstraction -(set-logic QF_BV) -(set-info :status sat) -(declare-fun x0 () (_ BitVec 8)) -(declare-fun x1 () (_ BitVec 8)) -(declare-fun y0 () (_ BitVec 8)) -(declare-fun y1 () (_ BitVec 8)) -(declare-fun y2 () (_ BitVec 8)) -(assert - (or - (= x0 (bvadd (bvmul (_ bv2 8) y0) y1)) - (= x0 (bvadd (bvmul (_ bv2 8) y1) y2)) - (= x0 (bvadd (bvmul (_ bv2 8) y2) y0)) - ) -) -(assert - (or - (= x1 (bvadd (bvadd (bvmul (_ bv3 8) y0) (bvmul (_ bv2 8) x0)) (_ bv5 8))) - (= x1 (bvadd (bvadd (bvmul (_ bv3 8) y1) (bvmul (_ bv2 8) x0)) (_ bv5 8))) - (= x1 (bvadd (bvadd (bvmul (_ bv3 8) x0) (bvmul (_ bv2 8) y2)) (_ bv5 8))) - ) -) -(check-sat) -(exit) diff --git a/test/regress/regress1/fmf/fc-pigeonhole19.smt2 b/test/regress/regress1/fmf/fc-pigeonhole19.smt2 index f145013d8..2945a8a24 100644 --- a/test/regress/regress1/fmf/fc-pigeonhole19.smt2 +++ b/test/regress/regress1/fmf/fc-pigeonhole19.smt2 @@ -8,13 +8,13 @@ (declare-fun h () H) ; pigeonhole using native cardinality constraints -(assert (fmf.card p 19)) -(assert (not (fmf.card p 18))) -(assert (fmf.card h 18)) -(assert (not (fmf.card h 17))) +(assert (_ fmf.card P 19)) +(assert (not (_ fmf.card P 18))) +(assert (_ fmf.card H 18)) +(assert (not (_ fmf.card H 17))) ; each pigeon has different holes (declare-fun f (P) H) (assert (forall ((p1 P) (p2 P)) (=> (not (= p1 p2)) (not (= (f p1) (f p2)))))) -(check-sat)
\ No newline at end of file +(check-sat) diff --git a/test/regress/regress1/quantifiers/bi-artm-s.smt2 b/test/regress/regress1/quantifiers/bi-artm-s.smt2 index af8ee945d..9c6b821b5 100644 --- a/test/regress/regress1/quantifiers/bi-artm-s.smt2 +++ b/test/regress/regress1/quantifiers/bi-artm-s.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --fmf-bound-lazy ; EXPECT: unsat -(set-option :incremental "false") +(set-option :incremental false) (set-info :status unsat) (set-logic ALL) (declare-fun Y () String) diff --git a/test/regress/regress1/quantifiers/issue4813-qe-quant.smt2 b/test/regress/regress1/quantifiers/issue4813-qe-quant.smt2 new file mode 100644 index 000000000..d20f14a7c --- /dev/null +++ b/test/regress/regress1/quantifiers/issue4813-qe-quant.smt2 @@ -0,0 +1,6 @@ +; EXPECT: v24 +(set-logic LIA) +(declare-const v8 Bool) +(assert (not (exists ((q16 Bool)) (xor true q16 v8 q16)))) +(declare-const v24 Bool) +(get-qe (exists ((q17 Bool) (q18 Int) (q19 Int) (q20 Int) (q21 Int) (q22 Bool)) v24)) diff --git a/test/regress/regress1/quantifiers/issue7537-cegqi-comp-types.smt2 b/test/regress/regress1/quantifiers/issue7537-cegqi-comp-types.smt2 new file mode 100644 index 000000000..bc9691ece --- /dev/null +++ b/test/regress/regress1/quantifiers/issue7537-cegqi-comp-types.smt2 @@ -0,0 +1,6 @@ +(set-logic ALL) +(set-info :status sat) +(declare-fun r1 () Real) +(declare-fun r5 () Real) +(assert (forall ((q102 Int)) (or (= q102 (/ r1 r5)) (= (= 0.0 q102) (< 1.0 (/ r1 r5)))))) +(check-sat) diff --git a/test/regress/regress1/rels/qgu-fuzz-relations-2.smt2 b/test/regress/regress1/rels/qgu-fuzz-relations-2.smt2 new file mode 100644 index 000000000..185c06502 --- /dev/null +++ b/test/regress/regress1/rels/qgu-fuzz-relations-2.smt2 @@ -0,0 +1,8 @@ +(set-logic ALL) +(set-info :status sat) +(declare-fun a () (Set (Tuple Int Int))) +(declare-fun b () (Set (Tuple Int Int))) +(declare-fun c () Int) +(declare-fun d () (Tuple Int Int)) +(assert (and (= a (singleton (tuple (+ c 1) 1))) (= (tclosure b) (join a a)))) +(check-sat) diff --git a/test/regress/regress1/rels/qgu-fuzz-relations-3-upwards.smt2 b/test/regress/regress1/rels/qgu-fuzz-relations-3-upwards.smt2 new file mode 100644 index 000000000..1cb91e94c --- /dev/null +++ b/test/regress/regress1/rels/qgu-fuzz-relations-3-upwards.smt2 @@ -0,0 +1,11 @@ +(set-logic ALL) +(set-info :status sat) +(declare-fun b () (Set (Tuple Int Int))) +(assert +(= (join b (tclosure (join b b))) (as emptyset (Set (Tuple Int Int)))) +) +(assert +(distinct b (as emptyset (Set (Tuple Int Int)))) +) +(assert (= (join b b) (as emptyset (Set (Tuple Int Int))))) +(check-sat) diff --git a/test/regress/regress1/strings/proj-issue331.smt2 b/test/regress/regress1/strings/proj-issue331.smt2 new file mode 100644 index 000000000..e993419f1 --- /dev/null +++ b/test/regress/regress1/strings/proj-issue331.smt2 @@ -0,0 +1,7 @@ +; COMMAND-LINE: --strings-exp +; EXPECT: unsat +(set-logic ALL) +(set-option :check-proofs true) +(set-info :status unsat) +(declare-const x Int) +(check-sat-assuming ((str.< (str.++ (str.from_int x) (str.replace_re (str.from_int x) re.none (str.from_int 0)) (str.replace_re (str.from_int x) re.none (str.from_int 0))) (str.from_int x)))) diff --git a/test/regress/regress2/quantifiers/cee-event-wrong-sat.smt2 b/test/regress/regress2/quantifiers/cee-event-wrong-sat.smt2 index c0b3aac7c..4a132a39b 100644 --- a/test/regress/regress2/quantifiers/cee-event-wrong-sat.smt2 +++ b/test/regress/regress2/quantifiers/cee-event-wrong-sat.smt2 @@ -1,5 +1,5 @@ -; COMMAND-LINE: --full-saturate-quant --ee-mode=distributed -; COMMAND-LINE: --full-saturate-quant --ee-mode=central +; COMMAND-LINE: -q --full-saturate-quant --ee-mode=distributed +; COMMAND-LINE: -q --full-saturate-quant --ee-mode=central ; EXPECT: unsat (set-logic ALL) (set-info :status unsat) @@ -23,7 +23,7 @@ (declare-fun $Event_EventHandleGenerator_type_value () T@$TypeValue) (assert (= 0 (|l#R| $EmptyValueArray))) (assert (forall ((v1 T@$Value) (v2 T@$Value)) (= ($IsEqual_stratified v1 v2) (or (= v1 v2) (forall ((i Int)) (or (> 0 i) (>= i (|l#R| (|v#V| v1))) ($IsEqual_stratified (sel (|v#R| (|v#V| v1)) i) (sel (|v#R| (|v#V| v2)) i)))))))) -(assert (forall ((m@@0 T@M) (a@@0 T@$Value)) (! (or (not (is-D a@@0)) (and (is-I (sel (|v#R| (|v#V| (s (|contents#M| m@@0) (G $Event_EventHandleGenerator_type_value (|a#D| a@@0))))) $Event_EventHandleGenerator_counter)) (forall ((x@@10 Int)) (or (> x@@10 0) (= E (sel (|v#R| (|v#V| (s (|contents#M| m@@0) (G $LibraAccount_T_type_value (|a#D| a@@0))))) x@@10)))))) :qid :skolemid))) +(assert (forall ((m@@0 T@M) (a@@0 T@$Value)) (! (or (not (is-D a@@0)) (and (is-I (sel (|v#R| (|v#V| (s (|contents#M| m@@0) (G $Event_EventHandleGenerator_type_value (|a#D| a@@0))))) $Event_EventHandleGenerator_counter)) (forall ((x@@10 Int)) (or (> x@@10 0) (= E (sel (|v#R| (|v#V| (s (|contents#M| m@@0) (G $LibraAccount_T_type_value (|a#D| a@@0))))) x@@10)))))) :qid || :skolemid ||))) (declare-fun |Select_[$Location]$bool| (b T@$Location) Bool) (declare-fun $m@@0 () T@M) (declare-fun $abort_flag@2 () Bool) |