diff options
Diffstat (limited to 'test/regress/regress0')
85 files changed, 1253 insertions, 46 deletions
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index 7d7690d22..45842065f 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -1,4 +1,4 @@ -SUBDIRS = . arith precedence uf uflra uflia bv arrays aufbv auflia datatypes quantifiers rewriterules lemmas push-pop preprocess tptp unconstrained decision fmf strings sets parser sygus +SUBDIRS = . arith precedence uf uflra uflia bv arrays aufbv auflia datatypes quantifiers rewriterules lemmas push-pop preprocess tptp unconstrained decision fmf strings sets parser sygus sep DIST_SUBDIRS = $(SUBDIRS) # don't override a BINARY imported from a personal.mk diff --git a/test/regress/regress0/aufbv/Makefile.am b/test/regress/regress0/aufbv/Makefile.am index 38b58cedd..38705c22a 100644 --- a/test/regress/regress0/aufbv/Makefile.am +++ b/test/regress/regress0/aufbv/Makefile.am @@ -22,7 +22,6 @@ TESTS = \ bug00.smt \ bug338.smt2 \ bug347.smt \ - bug348.smt \ bug451.smt \ bug509.smt \ bug580.smt2 \ diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am index 575aa4159..b7daadfd1 100644 --- a/test/regress/regress0/fmf/Makefile.am +++ b/test/regress/regress0/fmf/Makefile.am @@ -55,7 +55,9 @@ TESTS = \ datatypes-ufinite-nested.smt2 \ ForElimination-scala-9.smt2 \ agree466.smt2 \ - LeftistHeap.scala-8-ncm.smt2 + LeftistHeap.scala-8-ncm.smt2 \ + sc-crash-052316.smt2 \ + bound-int-alt.smt2 EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/fmf/bound-int-alt.smt2 b/test/regress/regress0/fmf/bound-int-alt.smt2 new file mode 100644 index 000000000..146487925 --- /dev/null +++ b/test/regress/regress0/fmf/bound-int-alt.smt2 @@ -0,0 +1,18 @@ +; COMMAND-LINE: --fmf-bound-int +; EXPECT: sat +(set-logic UFLIA) +(set-info :status sat) +(declare-sort U 0) +(declare-sort V 0) +(declare-fun P (U Int V Int U Int) Bool) + +(assert (forall ((x U) (y Int) (z V) (w Int) (v U) (d Int)) (=> (and (<= 0 d 1) (<= 2 y 6) (<= 40 w (+ 37 y))) (P x y z w v d)))) + +(declare-fun a () U) +(declare-fun b () V) + +(assert (not (P a 2 b 40 a 0))) +(assert (not (P a 6 b 39 a 0))) +(assert (not (P a 6 b 44 a 0))) + +(check-sat) diff --git a/test/regress/regress0/fmf/sc-crash-052316.smt2 b/test/regress/regress0/fmf/sc-crash-052316.smt2 new file mode 100644 index 000000000..2fc86cbed --- /dev/null +++ b/test/regress/regress0/fmf/sc-crash-052316.smt2 @@ -0,0 +1,35 @@ +; COMMAND-LINE: --finite-model-find +; EXPECT: unsat + (set-logic ALL_SUPPORTED) + (set-info :status unsat) + (declare-sort g_ 0) + (declare-fun __nun_card_witness_0_ () g_) + (declare-sort f_ 0) + (declare-fun __nun_card_witness_1_ () f_) + (declare-sort e_ 0) + (declare-fun __nun_card_witness_2_ () e_) +(declare-datatypes () + ((prod1_ (Pair1_ (_select_Pair1__0 e_) (_select_Pair1__1 f_))))) + (declare-sort d_ 0) + (declare-fun __nun_card_witness_3_ () d_) + (declare-sort c_ 0) + (declare-fun __nun_card_witness_4_ () c_) + (declare-sort b_ 0) + (declare-fun __nun_card_witness_5_ () b_) + (declare-sort a_ 0) + (declare-fun __nun_card_witness_6_ () a_) +(declare-datatypes () + ((prod_ (Pair_ (_select_Pair__0 a_) (_select_Pair__1 b_))))) + (declare-fun f1_ (prod_ c_ d_ prod1_) g_) + (declare-fun g1_ (prod_) c_) + (declare-fun h_ (prod_ d_) prod1_) + (declare-fun nun_sk_0_ () prod_) +(declare-fun nun_sk_1_ (c_) d_) + (assert + (not + (exists ((v/72 c_)) + (exists ((x/73 prod1_)) + (= (f1_ nun_sk_0_ v/72 (nun_sk_1_ v/72) x/73) + (f1_ nun_sk_0_ (g1_ nun_sk_0_) (nun_sk_1_ v/72) + (h_ nun_sk_0_ (nun_sk_1_ v/72)))))))) +(check-sat) diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am index 6b5e0d1ed..4c657adf1 100644 --- a/test/regress/regress0/quantifiers/Makefile.am +++ b/test/regress/regress0/quantifiers/Makefile.am @@ -79,7 +79,11 @@ TESTS = \ florian-case-ax.smt2 \ double-pattern.smt2 \ qcf-rel-dom-opt.smt2 \ - parametric-lists.smt2 + parametric-lists.smt2 \ + partial-trigger.smt2 \ + inst-max-level-segf.smt2 \ + small-bug1-fixpoint-3.smt2 \ + z3.620661-no-fv-trigger.smt2 # regression can be solved with --finite-model-find --fmf-inst-engine diff --git a/test/regress/regress0/quantifiers/inst-max-level-segf.smt2 b/test/regress/regress0/quantifiers/inst-max-level-segf.smt2 new file mode 100644 index 000000000..d85f3d094 --- /dev/null +++ b/test/regress/regress0/quantifiers/inst-max-level-segf.smt2 @@ -0,0 +1,326 @@ +; COMMAND-LINE: --inst-max-level=0 --simplification=none +; EXPECT: unsat +(set-logic UF) +(set-info :status unsat) +(declare-sort Node 0) +(declare-sort GrassPat 0) +(declare-sort GrassArray 1) +(declare-sort ArrayCell 1) +(declare-sort Loc 1) +(declare-sort Set 1) +(declare-sort Map 2) +(declare-sort GrassByte 0) +(declare-fun grass_null$0 () (Loc Node)) +(declare-fun grass_read$0 ((Map (Loc Node) (Loc Node)) (Loc Node)) + (Loc Node)) +(declare-fun grass_emptyset$0 () (Set (Loc Node))) +(declare-fun grass_singleton$0 ((Loc Node)) (Set (Loc Node))) +(declare-fun grass_union$0 ((Set (Loc Node)) (Set (Loc Node))) + (Set (Loc Node))) +(declare-fun grass_intersection$0 ((Set (Loc Node)) (Set (Loc Node))) + (Set (Loc Node))) +(declare-fun grass_setminus$0 ((Set (Loc Node)) (Set (Loc Node))) + (Set (Loc Node))) +(declare-fun grass_Btwn$0 ((Map (Loc Node) (Loc Node)) (Loc Node) (Loc Node) + (Loc Node)) Bool) +(declare-fun grass_member$0 ((Loc Node) (Set (Loc Node))) Bool) +(declare-fun grass_known$0 ((Map (Loc Node) (Loc Node))) GrassPat) +(declare-fun grass_known$1 (Bool) GrassPat) +(declare-fun Alloc_Node$0 () (Set (Loc Node))) +(declare-fun FP_Caller_Node$0 () (Set (Loc Node))) +(declare-fun FP_Caller_Node_1$0 () (Set (Loc Node))) +(declare-fun FP_Caller_final_Node_2$0 () (Set (Loc Node))) +(declare-fun FP_Node$0 () (Set (Loc Node))) +(declare-fun Label$0 () Bool) +(declare-fun Label_1$0 () Bool) +(declare-fun Label_2$0 () Bool) +(declare-fun Label_3$0 () Bool) +(declare-fun elt$0 () (Loc Node)) +(declare-fun lseg$0 ((Map (Loc Node) (Loc Node)) (Loc Node) (Loc Node) + (Set (Loc Node))) Bool) +(declare-fun lst$0 () (Loc Node)) +(declare-fun next$0 () (Map (Loc Node) (Loc Node))) +(declare-fun res_2$0 () (Loc Node)) +(declare-fun set_compr$0 ((Map (Loc Node) (Loc Node)) (Loc Node) (Loc Node)) + (Set (Loc Node))) +(declare-fun sk_?X$0 () (Set (Loc Node))) +(declare-fun sk_?X_1$0 () (Set (Loc Node))) +(declare-fun sk_?X_2$0 () (Set (Loc Node))) +(declare-fun sk_?X_3$0 () (Set (Loc Node))) +(declare-fun sk_?X_4$0 () (Set (Loc Node))) +(declare-fun sk_?e$0 () (Loc Node)) + +(assert (not (grass_member$0 grass_null$0 Alloc_Node$0))) +(assert + (and + (or + (or + (and (and (grass_member$0 sk_?e$0 sk_?X_4$0) Label_1$0) + (and + (not + (grass_member$0 sk_?e$0 + (set_compr$0 next$0 res_2$0 grass_null$0))) + Label_1$0)) + (and + (and + (grass_member$0 sk_?e$0 + (set_compr$0 next$0 res_2$0 grass_null$0)) + Label_1$0) + (and (not (grass_member$0 sk_?e$0 sk_?X_4$0)) Label_1$0))) + (and + (not (grass_Btwn$0 next$0 res_2$0 grass_null$0 grass_null$0)) + Label$0)) + Label_2$0)) +(assert (forall ((x (Loc Node))) (not (grass_member$0 x grass_emptyset$0)))) +(assert + (forall ((y (Loc Node)) (x (Loc Node))) + (or (and (= x y) (grass_member$0 x (grass_singleton$0 y))) + (and (not (= x y)) + (not (grass_member$0 x (grass_singleton$0 y))))))) +(assert + (forall ((x (Loc Node))) + (or + (and (grass_member$0 x FP_Caller_Node$0) + (grass_member$0 x + (grass_setminus$0 FP_Caller_Node$0 FP_Node$0)) + (not (grass_member$0 x FP_Node$0))) + (and + (or (grass_member$0 x FP_Node$0) + (not (grass_member$0 x FP_Caller_Node$0))) + (not + (grass_member$0 x + (grass_setminus$0 FP_Caller_Node$0 FP_Node$0))))))) +(assert + (forall ((x (Loc Node))) + (or + (and (grass_member$0 x Alloc_Node$0) + (grass_member$0 x + (grass_setminus$0 Alloc_Node$0 Alloc_Node$0)) + (not (grass_member$0 x Alloc_Node$0))) + (and + (or (grass_member$0 x Alloc_Node$0) + (not (grass_member$0 x Alloc_Node$0))) + (not + (grass_member$0 x + (grass_setminus$0 Alloc_Node$0 Alloc_Node$0))))))) +(assert + (forall ((x (Loc Node))) + (or + (and (grass_member$0 x Alloc_Node$0) + (grass_member$0 x FP_Node$0) + (grass_member$0 x + (grass_intersection$0 Alloc_Node$0 FP_Node$0))) + (and + (or (not (grass_member$0 x Alloc_Node$0)) + (not (grass_member$0 x FP_Node$0))) + (not + (grass_member$0 x + (grass_intersection$0 Alloc_Node$0 FP_Node$0))))))) +(assert + (forall ((x (Loc Node))) + (or + (and (grass_member$0 x sk_?X$0) + (grass_member$0 x sk_?X_1$0) + (grass_member$0 x + (grass_intersection$0 sk_?X$0 sk_?X_1$0))) + (and + (or (not (grass_member$0 x sk_?X$0)) + (not (grass_member$0 x sk_?X_1$0))) + (not + (grass_member$0 x + (grass_intersection$0 sk_?X$0 sk_?X_1$0))))))) +(assert + (forall ((x (Loc Node))) + (or + (and + (grass_member$0 x + (grass_union$0 + (grass_intersection$0 Alloc_Node$0 FP_Node$0) + (grass_setminus$0 Alloc_Node$0 Alloc_Node$0))) + (or + (grass_member$0 x + (grass_intersection$0 Alloc_Node$0 FP_Node$0)) + (grass_member$0 x + (grass_setminus$0 Alloc_Node$0 Alloc_Node$0)))) + (and + (not + (grass_member$0 x + (grass_intersection$0 Alloc_Node$0 FP_Node$0))) + (not + (grass_member$0 x + (grass_setminus$0 Alloc_Node$0 Alloc_Node$0))) + (not + (grass_member$0 x + (grass_union$0 + (grass_intersection$0 Alloc_Node$0 FP_Node$0) + (grass_setminus$0 Alloc_Node$0 Alloc_Node$0)))))))) +(assert + (forall ((x (Loc Node))) + (or + (and (grass_member$0 x (grass_union$0 sk_?X$0 sk_?X_1$0)) + (or (grass_member$0 x sk_?X$0) + (grass_member$0 x sk_?X_1$0))) + (and (not (grass_member$0 x sk_?X$0)) + (not (grass_member$0 x sk_?X_1$0)) + (not + (grass_member$0 x (grass_union$0 sk_?X$0 sk_?X_1$0))))))) +(assert + (forall ((x (Loc Node))) + (or + (and + (grass_member$0 x + (grass_union$0 FP_Caller_Node_1$0 FP_Node$0)) + (or (grass_member$0 x FP_Caller_Node_1$0) + (grass_member$0 x FP_Node$0))) + (and (not (grass_member$0 x FP_Caller_Node_1$0)) + (not (grass_member$0 x FP_Node$0)) + (not + (grass_member$0 x + (grass_union$0 FP_Caller_Node_1$0 FP_Node$0))))))) +(assert + (forall ((x (Loc Node))) + (or + (and + (grass_member$0 x + (grass_union$0 FP_Node$0 FP_Caller_Node$0)) + (or (grass_member$0 x FP_Node$0) + (grass_member$0 x FP_Caller_Node$0))) + (and (not (grass_member$0 x FP_Node$0)) + (not (grass_member$0 x FP_Caller_Node$0)) + (not + (grass_member$0 x + (grass_union$0 FP_Node$0 FP_Caller_Node$0))))))) +(assert + (forall ((x (Loc Node))) + (or + (and + (grass_member$0 x + (grass_union$0 FP_Caller_Node$0 Alloc_Node$0)) + (or (grass_member$0 x FP_Caller_Node$0) + (grass_member$0 x Alloc_Node$0))) + (and (not (grass_member$0 x FP_Caller_Node$0)) + (not (grass_member$0 x Alloc_Node$0)) + (not + (grass_member$0 x + (grass_union$0 FP_Caller_Node$0 Alloc_Node$0))))))) +(assert + (or (grass_Btwn$0 next$0 lst$0 lst$0 lst$0) + (not (lseg$0 next$0 lst$0 lst$0 sk_?X$0)))) +(assert + (forall + ((next (Map (Loc Node) (Loc Node))) (x (Loc Node)) + (y (Loc Node)) (z (Loc Node))) + (or + (and (grass_Btwn$0 next x z y) + (grass_member$0 z (set_compr$0 next x y)) (not (= z y))) + (and (or (= z y) (not (grass_Btwn$0 next x z y))) + (not (grass_member$0 z (set_compr$0 next x y))))))) +(assert + (forall + ((?u (Loc Node)) (?x (Loc Node)) (?y (Loc Node)) + (?z (Loc Node))) + (or (not (grass_Btwn$0 next$0 ?x ?y ?z)) + (not (grass_Btwn$0 next$0 ?x ?u ?y)) + (and (grass_Btwn$0 next$0 ?x ?u ?z) + (grass_Btwn$0 next$0 ?u ?y ?z))))) +(assert + (forall + ((?u (Loc Node)) (?x (Loc Node)) (?y (Loc Node)) + (?z (Loc Node))) + (or (not (grass_Btwn$0 next$0 ?x ?y ?z)) + (not (grass_Btwn$0 next$0 ?y ?u ?z)) + (and (grass_Btwn$0 next$0 ?x ?y ?u) + (grass_Btwn$0 next$0 ?x ?u ?z))))) +(assert + (forall ((?x (Loc Node)) (?y (Loc Node)) (?z (Loc Node))) + (or (not (grass_Btwn$0 next$0 ?x ?y ?y)) + (not (grass_Btwn$0 next$0 ?y ?z ?z)) + (grass_Btwn$0 next$0 ?x ?z ?z)))) +(assert + (forall ((?x (Loc Node)) (?y (Loc Node)) (?z (Loc Node))) + (or (not (grass_Btwn$0 next$0 ?x ?y ?z)) + (and (grass_Btwn$0 next$0 ?x ?y ?y) + (grass_Btwn$0 next$0 ?y ?z ?z))))) +(assert + (forall ((?x (Loc Node)) (?y (Loc Node)) (?z (Loc Node))) + (or (not (grass_Btwn$0 next$0 ?x ?y ?y)) + (not (grass_Btwn$0 next$0 ?x ?z ?z)) + (grass_Btwn$0 next$0 ?x ?y ?z) + (grass_Btwn$0 next$0 ?x ?z ?y)))) +(assert + (forall ((?x (Loc Node)) (?y (Loc Node))) + (or (not (grass_Btwn$0 next$0 ?x ?y ?x)) (= ?x ?y)))) +(assert + (forall ((?y (Loc Node))) + (or (not (grass_Btwn$0 next$0 res_2$0 ?y ?y)) (= res_2$0 ?y) + (grass_Btwn$0 next$0 res_2$0 (grass_read$0 next$0 res_2$0) + ?y)))) +(assert + (forall ((?y (Loc Node))) + (or (not (grass_Btwn$0 next$0 lst$0 ?y ?y)) (= lst$0 ?y) + (grass_Btwn$0 next$0 lst$0 (grass_read$0 next$0 lst$0) ?y)))) +(assert + (forall ((?y (Loc Node))) + (or (not (= (grass_read$0 next$0 res_2$0) res_2$0)) + (not (grass_Btwn$0 next$0 res_2$0 ?y ?y)) (= res_2$0 ?y)))) +(assert + (forall ((?y (Loc Node))) + (or (not (= (grass_read$0 next$0 lst$0) lst$0)) + (not (grass_Btwn$0 next$0 lst$0 ?y ?y)) (= lst$0 ?y)))) +(assert + (grass_Btwn$0 next$0 res_2$0 (grass_read$0 next$0 res_2$0) + (grass_read$0 next$0 res_2$0))) +(assert + (grass_Btwn$0 next$0 lst$0 (grass_read$0 next$0 lst$0) + (grass_read$0 next$0 lst$0))) +(assert (forall ((?x (Loc Node))) (grass_Btwn$0 next$0 ?x ?x ?x))) +(assert + (or (= sk_?X$0 (set_compr$0 next$0 lst$0 lst$0)) + (not (lseg$0 next$0 lst$0 lst$0 sk_?X$0)))) +(assert (= (grass_read$0 next$0 grass_null$0) grass_null$0)) +(assert (= FP_Caller_Node_1$0 (grass_setminus$0 FP_Caller_Node$0 FP_Node$0))) +(assert (and (= lst$0 grass_null$0) Label_3$0)) +(assert (= Alloc_Node$0 (grass_union$0 FP_Caller_Node$0 Alloc_Node$0))) +(assert + (= sk_?X_4$0 + (grass_union$0 (grass_intersection$0 Alloc_Node$0 FP_Node$0) + (grass_setminus$0 Alloc_Node$0 Alloc_Node$0)))) +(assert (= sk_?X_3$0 (grass_union$0 sk_?X$0 sk_?X_2$0))) +(assert (= sk_?X_2$0 sk_?X_1$0)) +(assert (= sk_?X_1$0 (grass_singleton$0 elt$0))) +(assert (= (grass_read$0 next$0 elt$0) grass_null$0)) +(assert (= FP_Node$0 sk_?X_3$0)) +(assert (= FP_Caller_Node$0 (grass_union$0 FP_Node$0 FP_Caller_Node$0))) +(assert (= grass_emptyset$0 (grass_intersection$0 sk_?X$0 sk_?X_2$0))) +(assert (= grass_emptyset$0 grass_emptyset$0)) +(assert (lseg$0 next$0 lst$0 grass_null$0 sk_?X$0)) +(assert + (= FP_Caller_final_Node_2$0 + (grass_union$0 FP_Caller_Node_1$0 FP_Node$0))) +(assert (= res_2$0 elt$0)) +(assert (= (grass_union$0 FP_Caller_Node$0 Alloc_Node$0) Alloc_Node$0)) +(assert (= (grass_read$0 next$0 grass_null$0) grass_null$0)) +(assert (= (grass_read$0 next$0 grass_null$0) lst$0)) +(assert (= (grass_read$0 next$0 grass_null$0) (grass_read$0 next$0 elt$0))) +(assert + (= (grass_known$1 (lseg$0 next$0 lst$0 grass_null$0 sk_?X$0)) + (grass_known$1 (lseg$0 next$0 lst$0 lst$0 sk_?X$0)))) +(assert (= (grass_intersection$0 sk_?X$0 sk_?X_2$0) grass_emptyset$0)) +(assert + (= + (grass_union$0 (grass_intersection$0 Alloc_Node$0 FP_Node$0) + (grass_setminus$0 Alloc_Node$0 Alloc_Node$0)) + sk_?X_4$0)) +(assert (= res_2$0 elt$0)) +(assert (= (grass_union$0 FP_Node$0 FP_Caller_Node$0) FP_Caller_Node$0)) +(assert (= sk_?X_1$0 (grass_singleton$0 elt$0))) +(assert (= sk_?X_1$0 sk_?X_2$0)) +(assert + (= FP_Caller_final_Node_2$0 + (grass_union$0 FP_Caller_Node_1$0 FP_Node$0))) +(assert (= FP_Node$0 sk_?X_3$0)) +(assert (= FP_Node$0 (grass_union$0 sk_?X$0 sk_?X_2$0))) +(assert (= FP_Caller_Node_1$0 (grass_setminus$0 FP_Caller_Node$0 FP_Node$0))) +(assert (= sk_?X$0 (set_compr$0 next$0 lst$0 lst$0))) +(assert (= sk_?X$0 (set_compr$0 next$0 lst$0 grass_null$0))) +(check-sat) diff --git a/test/regress/regress0/quantifiers/partial-trigger.smt2 b/test/regress/regress0/quantifiers/partial-trigger.smt2 new file mode 100644 index 000000000..beea57bdb --- /dev/null +++ b/test/regress/regress0/quantifiers/partial-trigger.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --partial-triggers +; EXPECT: unsat +(set-logic ALL_SUPPORTED) +(set-info :status unsat) +(declare-fun P (Int) Bool) +(assert (forall ((x Int) (y Int)) (=> (> y 6) (or (> x y) (P x))))) + +(assert (not (P 5))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/small-bug1-fixpoint-3.smt2 b/test/regress/regress0/quantifiers/small-bug1-fixpoint-3.smt2 new file mode 100644 index 000000000..da48f5e68 --- /dev/null +++ b/test/regress/regress0/quantifiers/small-bug1-fixpoint-3.smt2 @@ -0,0 +1,15 @@ +; COMMAND-LINE: --cbqi-all --no-check-models +; EXPECT: sat +(set-logic UFBV) +(set-info :status sat) +(declare-fun Verilog__main.impl_PC_valid_64_1_39_!3 (Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool) Bool) +(declare-fun Verilog__main.impl_flush_64_1_39_!1 (Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool) Bool) +(declare-fun Verilog__main.reset_64_0_39_!4 (Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool) Bool) +(declare-fun Verilog__main.impl_PC_valid_64_2_39_!6 (Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool) Bool) +(declare-fun Verilog__main.impl_flush_64_0_39_!0 (Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool) Bool) +(declare-fun Verilog__main.reset_64_1_39_!7 (Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool) Bool) +(declare-fun Verilog__main.impl_PC_valid_64_0_39_!5 (Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool) Bool) +(declare-fun Verilog__main.impl_flush_64_2_39_!2 (Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool) Bool) +(assert (forall ((Verilog__main.impl_flush_64_0 Bool) (Verilog__main.impl_flush_64_1 Bool) (Verilog__main.impl_flush_64_2 Bool) (Verilog__main.impl_flush_64_3 Bool) (Verilog__main.impl_PC_valid_64_1 Bool) (Verilog__main.reset_64_0 Bool) (Verilog__main.impl_PC_valid_64_0 Bool) (Verilog__main.impl_PC_valid_64_2 Bool) (Verilog__main.reset_64_1 Bool) (Verilog__main.impl_PC_valid_64_3 Bool) (Verilog__main.reset_64_2 Bool)) (=> (and (= Verilog__main.impl_flush_64_0 false) (= Verilog__main.impl_flush_64_1 false) (= Verilog__main.impl_flush_64_2 false) (= Verilog__main.impl_flush_64_3 false) (= Verilog__main.impl_PC_valid_64_1 (ite Verilog__main.reset_64_0 true (ite Verilog__main.impl_flush_64_0 false Verilog__main.impl_PC_valid_64_0))) (= Verilog__main.impl_PC_valid_64_2 (ite Verilog__main.reset_64_1 true (ite Verilog__main.impl_flush_64_1 false Verilog__main.impl_PC_valid_64_1))) (= Verilog__main.impl_PC_valid_64_3 (ite Verilog__main.reset_64_2 true (ite Verilog__main.impl_flush_64_2 false Verilog__main.impl_PC_valid_64_2)))) (and (= (Verilog__main.impl_flush_64_0_39_!0 Verilog__main.reset_64_2 Verilog__main.impl_PC_valid_64_3 Verilog__main.reset_64_1 Verilog__main.impl_PC_valid_64_2 Verilog__main.impl_PC_valid_64_0 Verilog__main.reset_64_0 Verilog__main.impl_PC_valid_64_1 Verilog__main.impl_flush_64_3 Verilog__main.impl_flush_64_2 Verilog__main.impl_flush_64_1 Verilog__main.impl_flush_64_0) false) (= (Verilog__main.impl_flush_64_1_39_!1 Verilog__main.reset_64_2 Verilog__main.impl_PC_valid_64_3 Verilog__main.reset_64_1 Verilog__main.impl_PC_valid_64_2 Verilog__main.impl_PC_valid_64_0 Verilog__main.reset_64_0 Verilog__main.impl_PC_valid_64_1 Verilog__main.impl_flush_64_3 Verilog__main.impl_flush_64_2 Verilog__main.impl_flush_64_1 Verilog__main.impl_flush_64_0) false) (= (Verilog__main.impl_flush_64_2_39_!2 Verilog__main.reset_64_2 Verilog__main.impl_PC_valid_64_3 Verilog__main.reset_64_1 Verilog__main.impl_PC_valid_64_2 Verilog__main.impl_PC_valid_64_0 Verilog__main.reset_64_0 Verilog__main.impl_PC_valid_64_1 Verilog__main.impl_flush_64_3 Verilog__main.impl_flush_64_2 Verilog__main.impl_flush_64_1 Verilog__main.impl_flush_64_0) false) (= (Verilog__main.impl_PC_valid_64_1_39_!3 Verilog__main.reset_64_2 Verilog__main.impl_PC_valid_64_3 Verilog__main.reset_64_1 Verilog__main.impl_PC_valid_64_2 Verilog__main.impl_PC_valid_64_0 Verilog__main.reset_64_0 Verilog__main.impl_PC_valid_64_1 Verilog__main.impl_flush_64_3 Verilog__main.impl_flush_64_2 Verilog__main.impl_flush_64_1 Verilog__main.impl_flush_64_0) (ite (Verilog__main.reset_64_0_39_!4 Verilog__main.reset_64_2 Verilog__main.impl_PC_valid_64_3 Verilog__main.reset_64_1 Verilog__main.impl_PC_valid_64_2 Verilog__main.impl_PC_valid_64_0 Verilog__main.reset_64_0 Verilog__main.impl_PC_valid_64_1 Verilog__main.impl_flush_64_3 Verilog__main.impl_flush_64_2 Verilog__main.impl_flush_64_1 Verilog__main.impl_flush_64_0) true (ite (Verilog__main.impl_flush_64_0_39_!0 Verilog__main.reset_64_2 Verilog__main.impl_PC_valid_64_3 Verilog__main.reset_64_1 Verilog__main.impl_PC_valid_64_2 Verilog__main.impl_PC_valid_64_0 Verilog__main.reset_64_0 Verilog__main.impl_PC_valid_64_1 Verilog__main.impl_flush_64_3 Verilog__main.impl_flush_64_2 Verilog__main.impl_flush_64_1 Verilog__main.impl_flush_64_0) false (Verilog__main.impl_PC_valid_64_0_39_!5 Verilog__main.reset_64_2 Verilog__main.impl_PC_valid_64_3 Verilog__main.reset_64_1 Verilog__main.impl_PC_valid_64_2 Verilog__main.impl_PC_valid_64_0 Verilog__main.reset_64_0 Verilog__main.impl_PC_valid_64_1 Verilog__main.impl_flush_64_3 Verilog__main.impl_flush_64_2 Verilog__main.impl_flush_64_1 Verilog__main.impl_flush_64_0)))) (= (Verilog__main.impl_PC_valid_64_2_39_!6 Verilog__main.reset_64_2 Verilog__main.impl_PC_valid_64_3 Verilog__main.reset_64_1 Verilog__main.impl_PC_valid_64_2 Verilog__main.impl_PC_valid_64_0 Verilog__main.reset_64_0 Verilog__main.impl_PC_valid_64_1 Verilog__main.impl_flush_64_3 Verilog__main.impl_flush_64_2 Verilog__main.impl_flush_64_1 Verilog__main.impl_flush_64_0) (ite (Verilog__main.reset_64_1_39_!7 Verilog__main.reset_64_2 Verilog__main.impl_PC_valid_64_3 Verilog__main.reset_64_1 Verilog__main.impl_PC_valid_64_2 Verilog__main.impl_PC_valid_64_0 Verilog__main.reset_64_0 Verilog__main.impl_PC_valid_64_1 Verilog__main.impl_flush_64_3 Verilog__main.impl_flush_64_2 Verilog__main.impl_flush_64_1 Verilog__main.impl_flush_64_0) true (ite (Verilog__main.impl_flush_64_1_39_!1 Verilog__main.reset_64_2 Verilog__main.impl_PC_valid_64_3 Verilog__main.reset_64_1 Verilog__main.impl_PC_valid_64_2 Verilog__main.impl_PC_valid_64_0 Verilog__main.reset_64_0 Verilog__main.impl_PC_valid_64_1 Verilog__main.impl_flush_64_3 Verilog__main.impl_flush_64_2 Verilog__main.impl_flush_64_1 Verilog__main.impl_flush_64_0) false (Verilog__main.impl_PC_valid_64_1_39_!3 Verilog__main.reset_64_2 Verilog__main.impl_PC_valid_64_3 Verilog__main.reset_64_1 Verilog__main.impl_PC_valid_64_2 Verilog__main.impl_PC_valid_64_0 Verilog__main.reset_64_0 Verilog__main.impl_PC_valid_64_1 Verilog__main.impl_flush_64_3 Verilog__main.impl_flush_64_2 Verilog__main.impl_flush_64_1 Verilog__main.impl_flush_64_0)))) (or (and (= Verilog__main.impl_flush_64_3 (Verilog__main.impl_flush_64_0_39_!0 Verilog__main.reset_64_2 Verilog__main.impl_PC_valid_64_3 Verilog__main.reset_64_1 Verilog__main.impl_PC_valid_64_2 Verilog__main.impl_PC_valid_64_0 Verilog__main.reset_64_0 Verilog__main.impl_PC_valid_64_1 Verilog__main.impl_flush_64_3 Verilog__main.impl_flush_64_2 Verilog__main.impl_flush_64_1 Verilog__main.impl_flush_64_0)) (= Verilog__main.impl_PC_valid_64_3 (Verilog__main.impl_PC_valid_64_0_39_!5 Verilog__main.reset_64_2 Verilog__main.impl_PC_valid_64_3 Verilog__main.reset_64_1 Verilog__main.impl_PC_valid_64_2 Verilog__main.impl_PC_valid_64_0 Verilog__main.reset_64_0 Verilog__main.impl_PC_valid_64_1 Verilog__main.impl_flush_64_3 Verilog__main.impl_flush_64_2 Verilog__main.impl_flush_64_1 Verilog__main.impl_flush_64_0))) (and (= Verilog__main.impl_flush_64_3 (Verilog__main.impl_flush_64_1_39_!1 Verilog__main.reset_64_2 Verilog__main.impl_PC_valid_64_3 Verilog__main.reset_64_1 Verilog__main.impl_PC_valid_64_2 Verilog__main.impl_PC_valid_64_0 Verilog__main.reset_64_0 Verilog__main.impl_PC_valid_64_1 Verilog__main.impl_flush_64_3 Verilog__main.impl_flush_64_2 Verilog__main.impl_flush_64_1 Verilog__main.impl_flush_64_0)) (= Verilog__main.impl_PC_valid_64_3 (Verilog__main.impl_PC_valid_64_1_39_!3 Verilog__main.reset_64_2 Verilog__main.impl_PC_valid_64_3 Verilog__main.reset_64_1 Verilog__main.impl_PC_valid_64_2 Verilog__main.impl_PC_valid_64_0 Verilog__main.reset_64_0 Verilog__main.impl_PC_valid_64_1 Verilog__main.impl_flush_64_3 Verilog__main.impl_flush_64_2 Verilog__main.impl_flush_64_1 Verilog__main.impl_flush_64_0))) (and (= Verilog__main.impl_flush_64_3 (Verilog__main.impl_flush_64_2_39_!2 Verilog__main.reset_64_2 Verilog__main.impl_PC_valid_64_3 Verilog__main.reset_64_1 Verilog__main.impl_PC_valid_64_2 Verilog__main.impl_PC_valid_64_0 Verilog__main.reset_64_0 Verilog__main.impl_PC_valid_64_1 Verilog__main.impl_flush_64_3 Verilog__main.impl_flush_64_2 Verilog__main.impl_flush_64_1 Verilog__main.impl_flush_64_0)) (= Verilog__main.impl_PC_valid_64_3 (Verilog__main.impl_PC_valid_64_2_39_!6 Verilog__main.reset_64_2 Verilog__main.impl_PC_valid_64_3 Verilog__main.reset_64_1 Verilog__main.impl_PC_valid_64_2 Verilog__main.impl_PC_valid_64_0 Verilog__main.reset_64_0 Verilog__main.impl_PC_valid_64_1 Verilog__main.impl_flush_64_3 Verilog__main.impl_flush_64_2 Verilog__main.impl_flush_64_1 Verilog__main.impl_flush_64_0)))))) )) +(check-sat) +(exit) diff --git a/test/regress/regress0/quantifiers/z3.620661-no-fv-trigger.smt2 b/test/regress/regress0/quantifiers/z3.620661-no-fv-trigger.smt2 new file mode 100644 index 000000000..aad2a4691 --- /dev/null +++ b/test/regress/regress0/quantifiers/z3.620661-no-fv-trigger.smt2 @@ -0,0 +1,87 @@ +(set-logic AUFNIRA) +(set-info :status unsat) +(declare-sort S1 0) +(declare-sort S2 0) +(declare-sort S3 0) +(declare-sort S4 0) +(declare-sort S5 0) +(declare-sort S6 0) +(declare-sort S7 0) +(declare-sort S8 0) +(declare-sort S9 0) +(declare-sort S10 0) +(declare-sort S11 0) +(declare-sort S12 0) +(declare-sort S13 0) +(declare-fun f1 () S1) +(declare-fun f2 () S1) +(declare-fun f3 (S2 Real) Real) +(declare-fun f4 (S3 Real) S2) +(declare-fun f5 () S3) +(declare-fun f6 (S4 Int) Int) +(declare-fun f7 (S5 Int) S4) +(declare-fun f8 () S5) +(declare-fun f9 () S2) +(declare-fun f10 () Real) +(declare-fun f11 () Real) +(declare-fun f12 () S2) +(declare-fun f13 (S7 S6) Real) +(declare-fun f14 () S7) +(declare-fun f15 () S2) +(declare-fun f16 () S2) +(declare-fun f17 (S8 Int) S6) +(declare-fun f18 () S8) +(declare-fun f19 (S9 S6) Int) +(declare-fun f20 () S9) +(declare-fun f21 (S10 Real) S7) +(declare-fun f22 () S10) +(declare-fun f23 () S2) +(declare-fun f24 (S11 S6) S6) +(declare-fun f25 (S12 S6) S11) +(declare-fun f26 () S12) +(declare-fun f27 () S12) +(declare-fun f28 (S13 Int) S9) +(declare-fun f29 () S13) +(declare-fun f30 () S2) +(declare-fun f31 () S4) +(assert (not (= f1 f2))) +(assert (forall ((?v0 Real) (?v1 Real)) (= (f3 (f4 f5 ?v0) ?v1) (* ?v0 ?v1)))) +(assert (forall ((?v0 Int) (?v1 Int)) (= (f6 (f7 f8 ?v0) ?v1) (* ?v0 ?v1)))) +(assert (not (= (f3 f9 (- f10 f11)) (- (f3 f9 f10))))) +(assert (= (f3 f9 f11) 0.0)) +(assert (forall ((?v0 Real)) (= (f3 f9 (+ f11 ?v0)) (- (f3 f9 ?v0))))) +(assert (= (f3 f9 (/ f11 2.0)) 1.0)) +(assert (= (f3 f9 (/ f11 6.0)) (/ 1.0 2.0))) +(assert (= (f3 f9 (* 2.0 f11)) 0.0)) +(assert (= (f3 f9 (* (/ 3.0 2.0) f11)) (- 1.0))) +(assert (let ((?v_0 2.0)) (<= (/ f11 ?v_0) ?v_0))) +(assert (let ((?v_0 2.0)) (< (/ f11 ?v_0) ?v_0))) +(assert (< (- (* 2.0 f11)) f11)) +(assert (< (- (/ f11 2.0)) 0.0)) +(assert (<= 2.0 f11)) +(assert (<= 0.0 (/ f11 2.0))) +(assert (< 0.0 (/ f11 2.0))) +(assert (< f11 4.0)) +(assert (<= 0.0 f11)) +(assert (< 0.0 f11)) +(assert (let ((?v_0 2.0)) (not (= (/ f11 ?v_0) ?v_0)))) +(assert (not (= (/ f11 2.0) 0.0))) +(assert (not (< f11 0.0))) +(assert (not (= f11 0.0))) +(assert (forall ((?v0 S6) (?v1 S6)) (= (= (f13 f14 ?v0) (f13 f14 ?v1)) (= ?v0 ?v1)))) +(assert (forall ((?v0 S6) (?v1 S6)) (= (< (f13 f14 ?v0) (f13 f14 ?v1)) (< (f19 f20 ?v0) (f19 f20 ?v1))))) +(assert (forall ((?v0 S6) (?v1 S6)) (= (<= (f13 f14 ?v0) (f13 f14 ?v1)) (<= (f19 f20 ?v0) (f19 f20 ?v1))))) +(assert (forall ((?v0 S6) (?v1 S6)) (let ((?v_0 (f19 f20 ?v1)) (?v_1 (f19 f20 ?v0))) (=> (<= ?v_1 ?v_0) (= (f13 f14 (f17 f18 (- ?v_0 ?v_1))) (- (f13 f14 ?v1) (f13 f14 ?v0))))))) +(assert (forall ((?v0 Real) (?v1 Real)) (exists ((?v2 Real) (?v3 Real)) (and (= ?v0 (* ?v2 (f3 f15 ?v3))) (= ?v1 (* ?v2 (f3 f9 ?v3))))))) +(assert (< 1.0 (f3 f16 2.0))) +(assert (< 0.0 (f3 f16 2.0))) +(assert (<= 0.0 (f3 f16 2.0))) +(assert (forall ((?v0 Real) (?v1 Real)) (<= 0.0 (f3 f16 (+ (* ?v0 ?v0) (* ?v1 ?v1)))))) +(assert (forall ((?v0 Real) (?v1 Real)) (=> (<= ?v0 ?v1) (<= (f3 f16 ?v0) (f3 f16 ?v1))))) +(assert (forall ((?v0 Real) (?v1 Real)) (=> (< ?v0 ?v1) (< (f3 f16 ?v0) (f3 f16 ?v1))))) +(assert (forall ((?v0 Real)) (let ((?v_0 0.0)) (=> (<= ?v_0 ?v0) (=> (= (f3 f16 ?v0) ?v_0) (= ?v0 ?v_0)))))) +(assert (forall ((?v0 Real)) (=> (< 0.0 ?v0) (< (/ ?v0 (f3 f16 2.0)) ?v0)))) +(assert (forall ((?v0 Real)) (let ((?v_0 0.0)) (=> (<= ?v_0 ?v0) (<= ?v_0 (f3 f16 ?v0)))))) +(assert (forall ((?v0 Real)) (let ((?v_0 1.0)) (=> (<= ?v_0 ?v0) (<= ?v_0 (f3 f16 ?v0)))))) +(check-sat) +(exit) diff --git a/test/regress/regress0/sep/Makefile.am b/test/regress/regress0/sep/Makefile.am new file mode 100644 index 000000000..9d2abaa18 --- /dev/null +++ b/test/regress/regress0/sep/Makefile.am @@ -0,0 +1,76 @@ +# don't override a BINARY imported from a personal.mk +@mk_if@eq ($(BINARY),) +@mk_empty@BINARY = cvc4 +end@mk_if@ + +LOG_COMPILER = @srcdir@/../../run_regression +AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) + +if AUTOMAKE_1_11 +# old-style (pre-automake 1.12) test harness +TESTS_ENVIRONMENT = \ + $(LOG_COMPILER) \ + $(AM_LOG_FLAGS) $(LOG_FLAGS) +endif + +MAKEFLAGS = -k + +# These are run for all build profiles. +# If a test shouldn't be run in e.g. competition mode, +# put it below in "TESTS +=" +TESTS = \ + pto-01.smt2 \ + pto-02.smt2 \ + pto-04.smt2 \ + sep-01.smt2 \ + sep-02.smt2 \ + sep-03.smt2 \ + sep-find2.smt2 \ + sep-neg-nstrict.smt2 \ + sep-plus1.smt2 \ + sep-nterm-val-model.smt2 \ + crash1220.smt2 \ + nspatial-simp.smt2 \ + sep-neg-1refine.smt2 \ + sep-neg-simple.smt2 \ + sep-simp-unc.smt2 \ + sep-simp-unsat-emp.smt2 \ + simple-neg-sat.smt2 \ + wand-simp-sat.smt2 \ + wand-simp-sat2.smt2 \ + wand-simp-unsat.smt2 \ + sep-nterm-again.smt2 \ + split-find-unsat.smt2 \ + split-find-unsat-w-emp.smt2 \ + nemp.smt2 \ + wand-crash.smt2 \ + wand-nterm-simp.smt2 \ + wand-nterm-simp2.smt2 \ + loop-1220.smt2 \ + chain-int.smt2 \ + sep-neg-swap.smt2 \ + sep-neg-nstrict2.smt2 \ + dispose-list-4-init.smt2 \ + wand-0526-sat.smt2 \ + quant_wand.smt2 \ + fmf-nemp-2.smt2 + + +FAILING_TESTS = +# loop-1220.smt2 (slow) + +EXTRA_DIST = $(TESTS) + +# slow after changes on Nov 20 : artemis-0512-nonterm.smt2 +# slow after decision engine respects requirePhase: type003.smt2 loop007.smt2 + +# and make sure to distribute it +EXTRA_DIST += + +# synonyms for "check" +.PHONY: regress regress0 test +regress regress0 test: check + +# do nothing in this subdir +.PHONY: regress1 regress2 regress3 +regress1 regress2 regress3: diff --git a/test/regress/regress0/sep/chain-int.smt2 b/test/regress/regress0/sep/chain-int.smt2 new file mode 100644 index 000000000..d3245e33f --- /dev/null +++ b/test/regress/regress0/sep/chain-int.smt2 @@ -0,0 +1,11 @@ +(set-logic ALL_SUPPORTED) +(set-info :status unsat) + +(declare-const x Int) +(declare-const y Int) +(declare-const z Int) + +(assert (sep (pto x y) (pto y z))) +(assert (and (> x 3) (< x 5))) +(assert (and (> y 3) (< y 5))) +(check-sat) diff --git a/test/regress/regress0/sep/crash1220.smt2 b/test/regress/regress0/sep/crash1220.smt2 new file mode 100755 index 000000000..a0fc5a187 --- /dev/null +++ b/test/regress/regress0/sep/crash1220.smt2 @@ -0,0 +1,15 @@ +; COMMAND-LINE: --no-check-models +; EXPECT: sat +(set-logic ALL_SUPPORTED) +(set-info :status sat) + +(declare-const x Int) +(declare-const a Int) + +(declare-const y Int) +(declare-const b Int) + +(assert (or (pto x a) (sep (pto x a) (pto y b)))) +(assert (or (not (pto x a)) (sep (not (pto x a)) (not (pto y b))))) + +(check-sat) diff --git a/test/regress/regress0/sep/dispose-list-4-init.smt2 b/test/regress/regress0/sep/dispose-list-4-init.smt2 new file mode 100644 index 000000000..766354cd9 --- /dev/null +++ b/test/regress/regress0/sep/dispose-list-4-init.smt2 @@ -0,0 +1,36 @@ +; COMMAND-LINE: --no-check-models +; EXPECT: sat +(set-logic ALL_SUPPORTED) + +(declare-sort Loc 0) + +(declare-const w Loc) +(declare-const u1 Loc) +(declare-const u2 Loc) +(declare-const u3 Loc) +(declare-const nil Loc) + +(declare-const w1 Loc) +(declare-const w2 Loc) +(declare-const w3 Loc) +(declare-const w4 Loc) + +; allocated (not nil) +(assert (not (= w nil))) +(assert (not (= u1 nil))) +(assert (not (= u2 nil))) +(assert (not (= u3 nil))) +(assert (not (= w1 nil))) +(assert (not (= w2 nil))) +(assert (not (= w4 nil))) + +; from model +;(assert (= w1 u3)) +;(assert (= w2 u2)) +;(assert (= w3 u1)) +;(assert (= w4 u1)) + +(assert (sep (pto w u1) (pto u1 u2) (pto u2 u3) (pto u3 nil))) +(assert (and (sep (sep (pto w4 w1) (pto w1 w2) (pto w2 nil)) (pto w w3)) (sep (pto w w4) true))) + +(check-sat) diff --git a/test/regress/regress0/sep/fmf-nemp-2.smt2 b/test/regress/regress0/sep/fmf-nemp-2.smt2 new file mode 100644 index 000000000..71fe96d71 --- /dev/null +++ b/test/regress/regress0/sep/fmf-nemp-2.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --finite-model-find --no-check-models +; EXPECT: sat +(set-logic ALL_SUPPORTED) +(declare-sort U 0) +(declare-fun u1 () U) +(declare-fun u2 () U) +(assert (not (= u1 u2))) +(assert (forall ((x U)) (=> (not (= x (as sep.nil U))) (sep (not (emp u1)) (pto x 0))))) +; satisfiable with heap of size 2, model of U of size 3 +(check-sat) diff --git a/test/regress/regress0/sep/loop-1220.smt2 b/test/regress/regress0/sep/loop-1220.smt2 new file mode 100644 index 000000000..2981606d8 --- /dev/null +++ b/test/regress/regress0/sep/loop-1220.smt2 @@ -0,0 +1,19 @@ +; COMMAND-LINE: --no-check-models +; EXPECT: sat +(set-logic ALL_SUPPORTED) +(set-info :status sat) + +(declare-const x Int) +(declare-const a Int) + +(declare-const y Int) +(declare-const b Int) +(declare-const y0 Int) +(declare-const b0 Int) +(declare-const y00 Int) +(declare-const b00 Int) + +(assert (or false (sep (pto x a) (or false (sep (pto y b) (or false (sep (pto y0 b0) (pto y00 b00) ))))))) +(assert (not (or false (sep (pto x a) (not (or false (sep (pto y b) (not (or false (sep (pto y0 b0) (not (pto y00 b00)) )))))))))) + +(check-sat) diff --git a/test/regress/regress0/sep/nemp.smt2 b/test/regress/regress0/sep/nemp.smt2 new file mode 100644 index 000000000..e1e21dd10 --- /dev/null +++ b/test/regress/regress0/sep/nemp.smt2 @@ -0,0 +1,5 @@ +; COMMAND-LINE: --no-check-models +; EXPECT: sat +(set-logic ALL_SUPPORTED) +(assert (not (emp 0))) +(check-sat) diff --git a/test/regress/regress0/sep/nspatial-simp.smt2 b/test/regress/regress0/sep/nspatial-simp.smt2 new file mode 100755 index 000000000..0c93719c9 --- /dev/null +++ b/test/regress/regress0/sep/nspatial-simp.smt2 @@ -0,0 +1,11 @@ +; COMMAND-LINE: --no-check-models +; EXPECT: sat +(set-logic ALL_SUPPORTED) +(set-info :status sat) +(declare-fun x () Int) + +(assert (sep (= x 0) (not (= x 5)))) + +(declare-fun y () Int) +(assert (pto y 0)) +(check-sat) diff --git a/test/regress/regress0/sep/pto-01.smt2 b/test/regress/regress0/sep/pto-01.smt2 new file mode 100644 index 000000000..b0dece248 --- /dev/null +++ b/test/regress/regress0/sep/pto-01.smt2 @@ -0,0 +1,13 @@ +(set-logic ALL_SUPPORTED) +(set-info :status unsat) + +(declare-const x Int) + +(declare-const a Int) +(declare-const b Int) + +(assert (and (pto x a) (pto x b))) + +(assert (not (= a b))) + +(check-sat) diff --git a/test/regress/regress0/sep/pto-02.smt2 b/test/regress/regress0/sep/pto-02.smt2 new file mode 100644 index 000000000..f0b6d2dee --- /dev/null +++ b/test/regress/regress0/sep/pto-02.smt2 @@ -0,0 +1,25 @@ +(set-logic ALL_SUPPORTED) +(set-info :status unsat) + + +(declare-const x Int) + +(declare-const a1 Int) +(declare-const a2 Int) +(declare-const a3 Int) +(declare-const a4 Int) +(declare-const a5 Int) +(declare-const a6 Int) +(declare-const a7 Int) +(declare-const a8 Int) +(declare-const a9 Int) + +(assert (and (pto x a1) (pto x a2) (pto x a3) + (pto x a4) (pto x a5) (pto x a6) + (pto x a7) (pto x a8) (pto x a9) + ) +) + +(assert (not (= a1 a2 a3 a4 a5 a6 a7 a8 a9))) + +(check-sat) diff --git a/test/regress/regress0/sep/pto-04.smt2 b/test/regress/regress0/sep/pto-04.smt2 new file mode 100644 index 000000000..1734c93bb --- /dev/null +++ b/test/regress/regress0/sep/pto-04.smt2 @@ -0,0 +1,36 @@ +(set-logic ALL_SUPPORTED) +(set-info :status unsat) + +(declare-const x1 Int) +(declare-const x2 Int) +(declare-const x3 Int) +(declare-const x4 Int) +(declare-const x5 Int) +(declare-const x6 Int) +(declare-const x7 Int) +(declare-const x8 Int) +(declare-const x9 Int) + +(declare-const a1 Int) +(declare-const a2 Int) +(declare-const a3 Int) +(declare-const a4 Int) +(declare-const a5 Int) +(declare-const a6 Int) +(declare-const a7 Int) +(declare-const a8 Int) +(declare-const a9 Int) + +(assert (and (pto x1 a1) (pto x2 a2) (pto x3 a3) + (pto x4 a4) (pto x5 a5) (pto x6 a6) + (pto x7 a7) (pto x8 a8) (pto x9 a9) + ) +) + +(assert (not (and (= x1 x2 x3 x4 x5 x6 x7 x8 x9) + (= a1 a2 a3 a4 a5 a6 a7 a8 a9) + ) + ) +) + +(check-sat) diff --git a/test/regress/regress0/sep/quant_wand.smt2 b/test/regress/regress0/sep/quant_wand.smt2 new file mode 100644 index 000000000..d71b937fc --- /dev/null +++ b/test/regress/regress0/sep/quant_wand.smt2 @@ -0,0 +1,15 @@ +; COMMAND-LINE: --cbqi-all +; EXPECT: unsat +(set-logic ALL_SUPPORTED) +(set-info :status unsat) + +(declare-const u Int) + +(assert (emp 0)) + +(assert +(forall ((y Int)) +(not (wand (pto u 5) (and (= y 42) (pto u 5)))) +)) + +(check-sat) diff --git a/test/regress/regress0/sep/sep-01.smt2 b/test/regress/regress0/sep/sep-01.smt2 new file mode 100644 index 000000000..c3330f036 --- /dev/null +++ b/test/regress/regress0/sep/sep-01.smt2 @@ -0,0 +1,14 @@ +(set-logic ALL_SUPPORTED) +(set-info :status unsat) + +(declare-const x Int) +(declare-const y Int) + +(declare-const a Int) +(declare-const b Int) + +(assert (sep (pto x a) (pto y b))) + +(assert (= x y)) + +(check-sat) diff --git a/test/regress/regress0/sep/sep-02.smt2 b/test/regress/regress0/sep/sep-02.smt2 new file mode 100644 index 000000000..403bcf077 --- /dev/null +++ b/test/regress/regress0/sep/sep-02.smt2 @@ -0,0 +1,16 @@ +(set-logic ALL_SUPPORTED) +(set-info :status unsat) + +(declare-const x Int) +(declare-const y Int) +(declare-const z Int) + +(declare-const a Int) +(declare-const b Int) +(declare-const c Int) + +(assert (sep (pto x a) (pto y b) (pto z c))) + +(assert (or (= x y) (= y z) (= x z))) + +(check-sat) diff --git a/test/regress/regress0/sep/sep-03.smt2 b/test/regress/regress0/sep/sep-03.smt2 new file mode 100644 index 000000000..427c44b50 --- /dev/null +++ b/test/regress/regress0/sep/sep-03.smt2 @@ -0,0 +1,17 @@ +(set-logic ALL_SUPPORTED) +(set-info :status unsat) + +(declare-const x Int) +(declare-const y Int) + +(declare-const a Int) +(declare-const b Int) + +(assert (and (sep (pto x a) (or (pto x a) (pto y b))) + (sep (pto y b) (or (pto x a) (pto y b))) + ) +) + +(assert (not (sep (pto x a) (pto y b)))) + +(check-sat) diff --git a/test/regress/regress0/sep/sep-find2.smt2 b/test/regress/regress0/sep/sep-find2.smt2 new file mode 100644 index 000000000..26a27eb22 --- /dev/null +++ b/test/regress/regress0/sep/sep-find2.smt2 @@ -0,0 +1,22 @@ +(set-logic ALL_SUPPORTED) +(set-info :status unsat) + +(declare-const x1 Int) +(declare-const x2 Int) +(declare-const x3 Int) +(declare-const x4 Int) +(declare-const x5 Int) +(declare-const x6 Int) +(declare-const x7 Int) + +(declare-const a1 Int) +(declare-const a2 Int) + +(assert (and +(sep (pto x1 a1) (pto x2 a2) (pto x4 a2) (pto x5 a2) (pto x6 a2) (pto x7 a2)) +(sep (pto x1 a1) (pto x3 a2)) +)) + +(assert (distinct x3 x2 x4 x5 x6 x7)) + +(check-sat) diff --git a/test/regress/regress0/sep/sep-neg-1refine.smt2 b/test/regress/regress0/sep/sep-neg-1refine.smt2 new file mode 100644 index 000000000..8ddbdd05f --- /dev/null +++ b/test/regress/regress0/sep/sep-neg-1refine.smt2 @@ -0,0 +1,17 @@ +; COMMAND-LINE: --no-check-models +; EXPECT: sat +(set-logic ALL_SUPPORTED) +(set-info :status sat) + +(declare-const x Int) +(declare-const y Int) +(declare-const z Int) + +(declare-const a Int) +(declare-const b Int) + +(assert (not (sep (pto x a) (pto y b)))) +(assert (sep (pto x a) (pto z b))) + +; sat with model where y != z +(check-sat) diff --git a/test/regress/regress0/sep/sep-neg-nstrict.smt2 b/test/regress/regress0/sep/sep-neg-nstrict.smt2 new file mode 100644 index 000000000..1a69336a8 --- /dev/null +++ b/test/regress/regress0/sep/sep-neg-nstrict.smt2 @@ -0,0 +1,15 @@ +(set-logic ALL_SUPPORTED) +(set-info :status unsat) + +(declare-const x Int) +(declare-const y Int) +(declare-const z Int) + +(declare-const a Int) +(declare-const b Int) + +(assert (not (sep true (pto x a)))) +(assert (sep (pto x a) (pto z b))) + + +(check-sat) diff --git a/test/regress/regress0/sep/sep-neg-nstrict2.smt2 b/test/regress/regress0/sep/sep-neg-nstrict2.smt2 new file mode 100644 index 000000000..e71e6a51a --- /dev/null +++ b/test/regress/regress0/sep/sep-neg-nstrict2.smt2 @@ -0,0 +1,18 @@ +; COMMAND-LINE: --no-check-models +; EXPECT: sat +(set-logic ALL_SUPPORTED) +(set-info :status sat) + +(declare-const x Int) +(declare-const y Int) +(declare-const z Int) + +(declare-const a Int) +(declare-const b Int) + +(assert (not (= a b))) +(assert (not (sep true (pto x b)))) +(assert (sep (pto x a) (pto z b))) + + +(check-sat) diff --git a/test/regress/regress0/sep/sep-neg-simple.smt2 b/test/regress/regress0/sep/sep-neg-simple.smt2 new file mode 100644 index 000000000..191e7527f --- /dev/null +++ b/test/regress/regress0/sep/sep-neg-simple.smt2 @@ -0,0 +1,16 @@ +; COMMAND-LINE: --no-check-models +; EXPECT: sat +(set-logic ALL_SUPPORTED) +(set-info :status sat) + +(declare-const x Int) +(declare-const y Int) +(declare-const z Int) + +(declare-const a Int) +(declare-const b Int) + +(assert (not (pto x a))) +(assert (sep (pto x a) (pto z b))) + +(check-sat) diff --git a/test/regress/regress0/sep/sep-neg-swap.smt2 b/test/regress/regress0/sep/sep-neg-swap.smt2 new file mode 100644 index 000000000..f89a9c0ac --- /dev/null +++ b/test/regress/regress0/sep/sep-neg-swap.smt2 @@ -0,0 +1,17 @@ +; COMMAND-LINE: --no-check-models +; EXPECT: sat +(set-logic ALL_SUPPORTED) +(set-info :status sat) + +(declare-const x Int) +(declare-const y Int) +(declare-const z Int) + +(declare-const a Int) +(declare-const b Int) + +(assert (not (sep (pto y a) (pto x b)))) +(assert (sep (pto x a) (pto y b))) + + +(check-sat) diff --git a/test/regress/regress0/sep/sep-nterm-again.smt2 b/test/regress/regress0/sep/sep-nterm-again.smt2 new file mode 100644 index 000000000..9b4afe36a --- /dev/null +++ b/test/regress/regress0/sep/sep-nterm-again.smt2 @@ -0,0 +1,20 @@ +; COMMAND-LINE: --no-check-models +; EXPECT: sat +(set-logic ALL_SUPPORTED) +(set-info :status sat) + +(declare-const x Int) +(declare-const y Int) +(declare-const z Int) + +(declare-const a Int) +(declare-const b Int) +(declare-const c Int) + +(assert (and + (not (sep (not (sep (not (pto x a)) (not (pto y b)))) (pto x a) )) + (sep (pto x a) (pto y b)) + ) +) + +(check-sat) diff --git a/test/regress/regress0/sep/sep-nterm-val-model.smt2 b/test/regress/regress0/sep/sep-nterm-val-model.smt2 new file mode 100644 index 000000000..0178134cb --- /dev/null +++ b/test/regress/regress0/sep/sep-nterm-val-model.smt2 @@ -0,0 +1,17 @@ +(set-logic ALL_SUPPORTED) +(set-info :status unsat) + +(declare-const x Int) +(declare-const y Int) +(declare-const z Int) + +(declare-const a Int) +(declare-const b Int) + +(assert (and + (not (sep (not (pto x a)) (not (pto y b)) )) + (sep (pto x (+ a 1)) (pto y (+ b 1))) + ) +) + +(check-sat) diff --git a/test/regress/regress0/sep/sep-plus1.smt2 b/test/regress/regress0/sep/sep-plus1.smt2 new file mode 100644 index 000000000..772acd981 --- /dev/null +++ b/test/regress/regress0/sep/sep-plus1.smt2 @@ -0,0 +1,18 @@ +(set-logic ALL_SUPPORTED) +(set-info :status unsat) + +(declare-const x Int) +(declare-const y Int) +(declare-const z Int) + +(declare-const a Int) +(declare-const b Int) +(declare-const c Int) + +(assert (and + (sep (pto x a) true) + (sep (pto y (+ a 1)) true) +)) +(assert (= x y)) + +(check-sat) diff --git a/test/regress/regress0/sep/sep-simp-unc.smt2 b/test/regress/regress0/sep/sep-simp-unc.smt2 new file mode 100755 index 000000000..6cdf51294 --- /dev/null +++ b/test/regress/regress0/sep/sep-simp-unc.smt2 @@ -0,0 +1,12 @@ +; COMMAND-LINE: --no-check-models +; EXPECT: sat +(set-logic ALL_SUPPORTED) +(set-info :status sat) +(declare-sort U 0) +(declare-fun x () U) +(declare-fun y () U) +(declare-fun a () U) +(declare-fun b () U) + +(assert (not (sep (not (pto x a)) (pto y b)))) +(check-sat) diff --git a/test/regress/regress0/sep/sep-simp-unsat-emp.smt2 b/test/regress/regress0/sep/sep-simp-unsat-emp.smt2 new file mode 100644 index 000000000..fb58b9d10 --- /dev/null +++ b/test/regress/regress0/sep/sep-simp-unsat-emp.smt2 @@ -0,0 +1,12 @@ +(set-logic ALL_SUPPORTED) +(set-info :status unsat) + +(declare-sort U 0) +(declare-fun x () U) +(declare-fun y () U) +(declare-fun a () U) +(declare-fun b () U) + +(assert (emp x)) +(assert (sep (pto x a) (pto y b))) +(check-sat) diff --git a/test/regress/regress0/sep/simple-neg-sat.smt2 b/test/regress/regress0/sep/simple-neg-sat.smt2 new file mode 100644 index 000000000..0c0b6a9a3 --- /dev/null +++ b/test/regress/regress0/sep/simple-neg-sat.smt2 @@ -0,0 +1,20 @@ +; COMMAND-LINE: --no-check-models +; EXPECT: sat +(set-logic ALL_SUPPORTED) +(set-info :status sat) + +(declare-const x Int) +(declare-const y Int) +(declare-const z Int) + +(declare-const a Int) +(declare-const b Int) +(declare-const c Int) + +(assert (and + (not (sep (not (pto x a)) (pto y b) )) + (sep (pto x a) (pto y b)) + ) +) + +(check-sat) diff --git a/test/regress/regress0/sep/split-find-unsat-w-emp.smt2 b/test/regress/regress0/sep/split-find-unsat-w-emp.smt2 new file mode 100644 index 000000000..ed3187a96 --- /dev/null +++ b/test/regress/regress0/sep/split-find-unsat-w-emp.smt2 @@ -0,0 +1,18 @@ +(set-logic ALL_SUPPORTED) +(set-info :status unsat) + +(declare-const x Int) +(declare-const y Int) +(declare-const z Int) + +(declare-const a Int) +(declare-const b Int) +(declare-const c Int) + +(assert (and + (not (sep (not (pto x a)) (not (pto y b)) (not (sep (pto x a) (pto y b))) (not (emp x)) )) + (sep (pto x a) (pto y b)) + ) +) + +(check-sat) diff --git a/test/regress/regress0/sep/split-find-unsat.smt2 b/test/regress/regress0/sep/split-find-unsat.smt2 new file mode 100644 index 000000000..54530cbf4 --- /dev/null +++ b/test/regress/regress0/sep/split-find-unsat.smt2 @@ -0,0 +1,20 @@ +; COMMAND-LINE: --no-check-models +; EXPECT: sat +(set-logic ALL_SUPPORTED) +(set-info :status sat) + +(declare-const x Int) +(declare-const y Int) +(declare-const z Int) + +(declare-const a Int) +(declare-const b Int) +(declare-const c Int) + +(assert (and + (not (sep (not (pto x a)) (not (pto y b)) (not (sep (pto x a) (pto y b))) )) + (sep (pto x a) (pto y b)) + ) +) + +(check-sat) diff --git a/test/regress/regress0/sep/wand-0526-sat.smt2 b/test/regress/regress0/sep/wand-0526-sat.smt2 new file mode 100644 index 000000000..0c0ee72ad --- /dev/null +++ b/test/regress/regress0/sep/wand-0526-sat.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --no-check-models +; EXPECT: sat +(set-logic ALL_SUPPORTED) +(declare-fun x () Int) +(declare-fun y () Int) +(declare-fun u () Int) +(declare-fun v () Int) +(assert (wand (pto x u) (pto y v))) +(assert (emp 0)) +(check-sat) diff --git a/test/regress/regress0/sep/wand-crash.smt2 b/test/regress/regress0/sep/wand-crash.smt2 new file mode 100644 index 000000000..9b4871323 --- /dev/null +++ b/test/regress/regress0/sep/wand-crash.smt2 @@ -0,0 +1,5 @@ +; COMMAND-LINE: --no-check-models +; EXPECT: sat +(set-logic ALL_SUPPORTED) +(assert (wand (emp 0) (emp 0))) +(check-sat) diff --git a/test/regress/regress0/sep/wand-nterm-simp.smt2 b/test/regress/regress0/sep/wand-nterm-simp.smt2 new file mode 100644 index 000000000..e8ee4252c --- /dev/null +++ b/test/regress/regress0/sep/wand-nterm-simp.smt2 @@ -0,0 +1,7 @@ +; COMMAND-LINE: --no-check-models +; EXPECT: sat +(set-logic ALL_SUPPORTED) +(declare-fun x () Int) +(assert (wand (emp x) (pto x 3))) +(check-sat) + diff --git a/test/regress/regress0/sep/wand-nterm-simp2.smt2 b/test/regress/regress0/sep/wand-nterm-simp2.smt2 new file mode 100644 index 000000000..69305e95c --- /dev/null +++ b/test/regress/regress0/sep/wand-nterm-simp2.smt2 @@ -0,0 +1,6 @@ +; COMMAND-LINE: --no-check-models +; EXPECT: unsat +(set-logic ALL_SUPPORTED) +(declare-fun x () Int) +(assert (wand (pto x 1) (emp x))) +(check-sat) diff --git a/test/regress/regress0/sep/wand-simp-sat.smt2 b/test/regress/regress0/sep/wand-simp-sat.smt2 new file mode 100755 index 000000000..df4bfa6d8 --- /dev/null +++ b/test/regress/regress0/sep/wand-simp-sat.smt2 @@ -0,0 +1,6 @@ +; COMMAND-LINE: --no-check-models +; EXPECT: sat +(set-logic ALL_SUPPORTED) +(declare-fun x () Int) +(assert (wand (pto x 1) (pto x 1))) +(check-sat) diff --git a/test/regress/regress0/sep/wand-simp-sat2.smt2 b/test/regress/regress0/sep/wand-simp-sat2.smt2 new file mode 100755 index 000000000..ebc115fdd --- /dev/null +++ b/test/regress/regress0/sep/wand-simp-sat2.smt2 @@ -0,0 +1,6 @@ +; COMMAND-LINE: --no-check-models +; EXPECT: unsat +(set-logic ALL_SUPPORTED) +(declare-fun x () Int) +(assert (wand (pto x 1) (pto x 3))) +(check-sat) diff --git a/test/regress/regress0/sep/wand-simp-unsat.smt2 b/test/regress/regress0/sep/wand-simp-unsat.smt2 new file mode 100755 index 000000000..95bc85537 --- /dev/null +++ b/test/regress/regress0/sep/wand-simp-unsat.smt2 @@ -0,0 +1,7 @@ +; COMMAND-LINE: --no-check-models +; EXPECT: unsat +(set-logic ALL_SUPPORTED) +(declare-fun x () Int) +(assert (wand (pto x 1) (pto x 3))) +(assert (emp x)) +(check-sat) diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am index 771b9f031..477d336e6 100644 --- a/test/regress/regress0/strings/Makefile.am +++ b/test/regress/regress0/strings/Makefile.am @@ -76,7 +76,9 @@ TESTS = \ type002.smt2 \ crash-1019.smt2 \ norn-31.smt2 \ - strings-native-simple.cvc + strings-native-simple.cvc \ + cmu-2db2-extf-reg.smt2 \ + norn-nel-bug-052116.smt2 FAILING_TESTS = diff --git a/test/regress/regress0/strings/cmu-2db2-extf-reg.smt2 b/test/regress/regress0/strings/cmu-2db2-extf-reg.smt2 new file mode 100644 index 000000000..b513494b8 --- /dev/null +++ b/test/regress/regress0/strings/cmu-2db2-extf-reg.smt2 @@ -0,0 +1,9 @@ +(set-logic ALL_SUPPORTED) +(set-info :status sat) +(set-option :strings-exp true) + +(declare-fun s () String) + +(assert (and (not (not (= (ite (= (str.indexof s "bar" 1) (- 1)) 1 0) 0))) (not (not (= (ite (= (str.indexof s "bar" 1) 3) 1 0) 0))))) + +(check-sat) diff --git a/test/regress/regress0/strings/norn-nel-bug-052116.smt2 b/test/regress/regress0/strings/norn-nel-bug-052116.smt2 new file mode 100644 index 000000000..f0c2534a1 --- /dev/null +++ b/test/regress/regress0/strings/norn-nel-bug-052116.smt2 @@ -0,0 +1,23 @@ +(set-logic QF_S) +(set-info :status sat) +(set-option :strings-exp true) + +(declare-fun var_0 () String) +(declare-fun var_1 () String) +(declare-fun var_2 () String) +(declare-fun var_3 () String) +(declare-fun var_4 () String) +(declare-fun var_5 () String) +(declare-fun var_6 () String) +(declare-fun var_7 () String) +(declare-fun var_8 () String) +(declare-fun var_9 () String) +(declare-fun var_10 () String) +(declare-fun var_11 () String) +(declare-fun var_12 () String) + +(assert (str.in.re var_4 (re.* (re.range "a" "u")))) +(assert (str.in.re var_4 (re.++ (re.* (re.union (str.to.re "a") (re.++ (str.to.re "b") (str.to.re "a")))) (str.to.re "b")))) +(assert (str.in.re (str.++ "a" var_4 "b" ) (re.* (re.range "a" "u")))) +(assert (not (str.in.re (str.++ "a" var_4 "b" ) (re.++ (re.* (str.to.re "a")) (re.++ (str.to.re "b") (re.* (str.to.re "b"))))))) +(check-sat) diff --git a/test/regress/regress0/sygus/Makefile.am b/test/regress/regress0/sygus/Makefile.am index 2ca807662..b503a65b8 100644 --- a/test/regress/regress0/sygus/Makefile.am +++ b/test/regress/regress0/sygus/Makefile.am @@ -48,7 +48,10 @@ TESTS = commutative.sy \ clock-inc-tuple.sy \ dt-test-ns.sy \ no-mention.sy \ - max2-univ.sy + max2-univ.sy \ + strings-small.sy \ + strings-unconstrained.sy \ + hd-sdiv.sy # sygus tests currently taking too long for make regress EXTRA_DIST = $(TESTS) \ diff --git a/test/regress/regress0/sygus/array_search_2.sy b/test/regress/regress0/sygus/array_search_2.sy index 56a30b210..e6683ced9 100644 --- a/test/regress/regress0/sygus/array_search_2.sy +++ b/test/regress/regress0/sygus/array_search_2.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si --no-dump-synth +; COMMAND-LINE: --cegqi-si=all --no-dump-synth (set-logic LIA) (synth-fun findIdx ( (y1 Int) (y2 Int) (k1 Int)) Int ((Start Int ( 0 1 2 y1 y2 k1 (ite BoolExpr Start Start))) (BoolExpr Bool ((< Start Start) (<= Start Start) (> Start Start) (>= Start Start))))) (declare-var x1 Int) diff --git a/test/regress/regress0/sygus/array_sum_2_5.sy b/test/regress/regress0/sygus/array_sum_2_5.sy index f6c0320e2..387ce9487 100644 --- a/test/regress/regress0/sygus/array_sum_2_5.sy +++ b/test/regress/regress0/sygus/array_sum_2_5.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si --no-dump-synth +; COMMAND-LINE: --cegqi-si=all --no-dump-synth (set-logic LIA) (synth-fun findSum ( (y1 Int) (y2 Int) )Int ((Start Int ( 0 1 2 y1 y2 (+ Start Start) (ite BoolExpr Start Start))) (BoolExpr Bool ((< Start Start) (<= Start Start) (> Start Start) (>= Start Start))))) (declare-var x1 Int) diff --git a/test/regress/regress0/sygus/clock-inc-tuple.sy b/test/regress/regress0/sygus/clock-inc-tuple.sy index 09bdb8b4d..3519319bd 100644 --- a/test/regress/regress0/sygus/clock-inc-tuple.sy +++ b/test/regress/regress0/sygus/clock-inc-tuple.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si --no-dump-synth +; COMMAND-LINE: --cegqi-si=all --no-dump-synth (set-logic ALL_SUPPORTED) (declare-var m Int) diff --git a/test/regress/regress0/sygus/commutative.sy b/test/regress/regress0/sygus/commutative.sy index 46dbd2981..f675bddad 100644 --- a/test/regress/regress0/sygus/commutative.sy +++ b/test/regress/regress0/sygus/commutative.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi --no-dump-synth +; COMMAND-LINE: --no-dump-synth (set-logic LIA) @@ -19,4 +19,4 @@ (check-synth) -; (+ x y) is a valid solution
\ No newline at end of file +; (+ x y) is a valid solution diff --git a/test/regress/regress0/sygus/const-var-test.sy b/test/regress/regress0/sygus/const-var-test.sy index 428cb2adc..b79b7eeec 100644 --- a/test/regress/regress0/sygus/const-var-test.sy +++ b/test/regress/regress0/sygus/const-var-test.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si --no-dump-synth +; COMMAND-LINE: --cegqi-si=all --no-dump-synth (set-logic LIA) diff --git a/test/regress/regress0/sygus/constant.sy b/test/regress/regress0/sygus/constant.sy index 0059f6947..5c48f5e39 100644 --- a/test/regress/regress0/sygus/constant.sy +++ b/test/regress/regress0/sygus/constant.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi --no-dump-synth +; COMMAND-LINE: --no-dump-synth (set-logic LIA) @@ -20,4 +20,4 @@ (check-synth) -; 0, 1, (- x x) are valid solutions
\ No newline at end of file +; 0, 1, (- x x) are valid solutions diff --git a/test/regress/regress0/sygus/dt-no-syntax.sy b/test/regress/regress0/sygus/dt-no-syntax.sy index e0f8112ce..42382ac91 100644 --- a/test/regress/regress0/sygus/dt-no-syntax.sy +++ b/test/regress/regress0/sygus/dt-no-syntax.sy @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cegqi --no-dump-synth +; COMMAND-LINE: --no-dump-synth ; EXPECT: unsat (set-logic LIA) diff --git a/test/regress/regress0/sygus/dt-test-ns.sy b/test/regress/regress0/sygus/dt-test-ns.sy index ed17f4ff2..052065061 100644 --- a/test/regress/regress0/sygus/dt-test-ns.sy +++ b/test/regress/regress0/sygus/dt-test-ns.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si --no-dump-synth +; COMMAND-LINE: --cegqi-si=all --no-dump-synth (set-logic LIA) (declare-datatypes () ((List (cons (head Int) (tail List)) (nil)))) diff --git a/test/regress/regress0/sygus/dup-op.sy b/test/regress/regress0/sygus/dup-op.sy index e5448d626..bed9972fd 100644 --- a/test/regress/regress0/sygus/dup-op.sy +++ b/test/regress/regress0/sygus/dup-op.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi --no-cegqi-si --no-dump-synth +; COMMAND-LINE: --cegqi-si=none --no-dump-synth (set-logic LIA) (synth-fun f ((x Int)) Int ((Start Int ((+ Con Con) (+ Start Start) x)) diff --git a/test/regress/regress0/sygus/enum-test.sy b/test/regress/regress0/sygus/enum-test.sy index cd129385e..7b59f5f1a 100644 --- a/test/regress/regress0/sygus/enum-test.sy +++ b/test/regress/regress0/sygus/enum-test.sy @@ -1,8 +1,8 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si --no-dump-synth +; COMMAND-LINE: --cegqi-si=all --no-dump-synth (set-logic LIA) (define-sort D (Enum (a b))) (define-fun f ((x D)) Int (ite (= x D::a) 3 7)) (synth-fun g () D ((Start D (D::a D::b)))) (constraint (= (f g) 7)) -(check-synth)
\ No newline at end of file +(check-synth) diff --git a/test/regress/regress0/sygus/hd-sdiv.sy b/test/regress/regress0/sygus/hd-sdiv.sy new file mode 100644 index 000000000..019b48a1c --- /dev/null +++ b/test/regress/regress0/sygus/hd-sdiv.sy @@ -0,0 +1,16 @@ +; EXPECT: unsat +; COMMAND-LINE: --cegqi-si=none --no-dump-synth +(set-logic BV) + +(define-fun hd01 ((x (BitVec 32))) (BitVec 32) (bvand x #x00000001)) + +(synth-fun f ((x (BitVec 32))) (BitVec 32) + ((Start (BitVec 32) ((bvsdiv Start Start) + (bvand Start Start) + x + #x00000001)))) + +(declare-var y (BitVec 32)) +(constraint (= (hd01 y) (f y))) +(check-synth) + diff --git a/test/regress/regress0/sygus/icfp_28_10.sy b/test/regress/regress0/sygus/icfp_28_10.sy index b07be0e98..74e054159 100644 --- a/test/regress/regress0/sygus/icfp_28_10.sy +++ b/test/regress/regress0/sygus/icfp_28_10.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi --no-dump-synth +; COMMAND-LINE: --no-dump-synth (set-logic BV) diff --git a/test/regress/regress0/sygus/inv-example.sy b/test/regress/regress0/sygus/inv-example.sy index aafbbd987..b56425964 100644 --- a/test/regress/regress0/sygus/inv-example.sy +++ b/test/regress/regress0/sygus/inv-example.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si --no-dump-synth +; COMMAND-LINE: --no-dump-synth (set-logic LIA) (synth-inv inv-f ((x Int) (y Int) (b Bool))) (declare-primed-var x Int) @@ -9,4 +9,4 @@ (define-fun trans-f ((x Int) (y Int) (b Bool) (x! Int) (y! Int) (b! Bool)) Bool (and (and (= b! b) (= y! x)) (ite b (= x! (+ x 10)) (= x! (+ x 12))))) (define-fun post-f ((x Int) (y Int) (b Bool)) Bool (<= y x)) (inv-constraint inv-f pre-f trans-f post-f) -(check-synth)
\ No newline at end of file +(check-synth) diff --git a/test/regress/regress0/sygus/let-ringer.sy b/test/regress/regress0/sygus/let-ringer.sy index 4bae90b00..d5d40ace4 100644 --- a/test/regress/regress0/sygus/let-ringer.sy +++ b/test/regress/regress0/sygus/let-ringer.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si --no-dump-synth +; COMMAND-LINE: --cegqi-si=all --no-dump-synth (set-logic LIA) (define-fun g ((x Int)) Int (ite (= x 1) 15 19)) (synth-fun f ((x Int)) Int diff --git a/test/regress/regress0/sygus/let-simp.sy b/test/regress/regress0/sygus/let-simp.sy index 71cd27e8f..d07f6a717 100644 --- a/test/regress/regress0/sygus/let-simp.sy +++ b/test/regress/regress0/sygus/let-simp.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si --no-dump-synth +; COMMAND-LINE: --cegqi-si=all --no-dump-synth (set-logic LIA) (synth-fun f ((x Int) (y Int)) Int ((Start Int (x diff --git a/test/regress/regress0/sygus/list-head-x.sy b/test/regress/regress0/sygus/list-head-x.sy index a5977d1e7..21362dc2c 100644 --- a/test/regress/regress0/sygus/list-head-x.sy +++ b/test/regress/regress0/sygus/list-head-x.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si --no-dump-synth +; COMMAND-LINE: --cegqi-si=all --no-dump-synth (set-logic ALL_SUPPORTED) (declare-datatypes () ((List (cons (head Int) (tail List)) (nil)))) diff --git a/test/regress/regress0/sygus/max.sy b/test/regress/regress0/sygus/max.sy index dec4594d7..e6e3de5fc 100644 --- a/test/regress/regress0/sygus/max.sy +++ b/test/regress/regress0/sygus/max.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si --no-dump-synth +; COMMAND-LINE: --cegqi-si=all --no-dump-synth (set-logic LIA) (synth-fun max ((x Int) (y Int)) Int diff --git a/test/regress/regress0/sygus/max2-univ.sy b/test/regress/regress0/sygus/max2-univ.sy index 3f8aac3b2..927148d81 100644 --- a/test/regress/regress0/sygus/max2-univ.sy +++ b/test/regress/regress0/sygus/max2-univ.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi --no-dump-synth +; COMMAND-LINE: --no-dump-synth ; Synthesize the maximum of 2 integers, but property has 4 variables (requires 2 passes) (set-logic LIA) (synth-fun max2 ((x Int) (y Int)) Int) diff --git a/test/regress/regress0/sygus/multi-fun-polynomial2.sy b/test/regress/regress0/sygus/multi-fun-polynomial2.sy index 6d185ba3f..c238de5dd 100644 --- a/test/regress/regress0/sygus/multi-fun-polynomial2.sy +++ b/test/regress/regress0/sygus/multi-fun-polynomial2.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi --no-dump-synth +; COMMAND-LINE: --no-dump-synth (set-logic LIA) @@ -32,4 +32,4 @@ (check-synth) -; (x, y), (x-y, 0) ... are valid solutions
\ No newline at end of file +; (x, y), (x-y, 0) ... are valid solutions diff --git a/test/regress/regress0/sygus/nflat-fwd-3.sy b/test/regress/regress0/sygus/nflat-fwd-3.sy index 9065a1025..d3624a731 100644 --- a/test/regress/regress0/sygus/nflat-fwd-3.sy +++ b/test/regress/regress0/sygus/nflat-fwd-3.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si --no-dump-synth +; COMMAND-LINE: --no-dump-synth (set-logic LIA) (synth-fun f ((x Int)) Int ((Start Int ((+ (+ Con Con) Con) x)) diff --git a/test/regress/regress0/sygus/nflat-fwd.sy b/test/regress/regress0/sygus/nflat-fwd.sy index d211d475b..3f15d5915 100644 --- a/test/regress/regress0/sygus/nflat-fwd.sy +++ b/test/regress/regress0/sygus/nflat-fwd.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi --no-dump-synth +; COMMAND-LINE: --no-dump-synth (set-logic LIA) (synth-fun f ((x Int)) Int ((Start Int ((+ Con Con) (+ (+ Start Start) Con) x)) diff --git a/test/regress/regress0/sygus/no-flat-simp.sy b/test/regress/regress0/sygus/no-flat-simp.sy index cb284b180..af1284f13 100644 --- a/test/regress/regress0/sygus/no-flat-simp.sy +++ b/test/regress/regress0/sygus/no-flat-simp.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si --no-dump-synth +; COMMAND-LINE: --no-dump-synth (set-logic LIA) diff --git a/test/regress/regress0/sygus/no-mention.sy b/test/regress/regress0/sygus/no-mention.sy index 05dfbced3..60efc1b74 100644 --- a/test/regress/regress0/sygus/no-mention.sy +++ b/test/regress/regress0/sygus/no-mention.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi --no-dump-synth +; COMMAND-LINE: --no-dump-synth (set-logic LIA) (synth-fun p ((x Int) (y Int)) Int) diff --git a/test/regress/regress0/sygus/no-syntax-test-bool.sy b/test/regress/regress0/sygus/no-syntax-test-bool.sy index 4b3fa22e6..ee27b30eb 100644 --- a/test/regress/regress0/sygus/no-syntax-test-bool.sy +++ b/test/regress/regress0/sygus/no-syntax-test-bool.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si --no-dump-synth +; COMMAND-LINE: --no-dump-synth (set-logic LIA) diff --git a/test/regress/regress0/sygus/no-syntax-test-no-si.sy b/test/regress/regress0/sygus/no-syntax-test-no-si.sy index 86b60638b..bd8da1900 100644 --- a/test/regress/regress0/sygus/no-syntax-test-no-si.sy +++ b/test/regress/regress0/sygus/no-syntax-test-no-si.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi --no-dump-synth +; COMMAND-LINE: --no-dump-synth (set-logic LIA) diff --git a/test/regress/regress0/sygus/no-syntax-test.sy b/test/regress/regress0/sygus/no-syntax-test.sy index b95f31aa7..2b3d5f3e9 100644 --- a/test/regress/regress0/sygus/no-syntax-test.sy +++ b/test/regress/regress0/sygus/no-syntax-test.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si --no-dump-synth +; COMMAND-LINE: --no-dump-synth (set-logic LIA) diff --git a/test/regress/regress0/sygus/parity-AIG-d0.sy b/test/regress/regress0/sygus/parity-AIG-d0.sy index 03d180634..3cc577bd8 100644 --- a/test/regress/regress0/sygus/parity-AIG-d0.sy +++ b/test/regress/regress0/sygus/parity-AIG-d0.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si --no-dump-synth +; COMMAND-LINE: --cegqi-si=all --no-dump-synth (set-logic BV) (define-fun parity ((a Bool) (b Bool) (c Bool) (d Bool)) Bool @@ -27,4 +27,4 @@ ;(not ; (and ; (and (not (and (not a) b)) (not (and d (not c)))) -; (and (not (and (not b) a)) (not (and (not d) c))))))
\ No newline at end of file +; (and (not (and (not b) a)) (not (and (not d) c)))))) diff --git a/test/regress/regress0/sygus/strings-small.sy b/test/regress/regress0/sygus/strings-small.sy new file mode 100644 index 000000000..40346bcdf --- /dev/null +++ b/test/regress/regress0/sygus/strings-small.sy @@ -0,0 +1,35 @@ +; EXPECT: unsat +; COMMAND-LINE: --no-dump-synth +(set-logic SLIA) +(synth-fun f ((firstname String) (lastname String)) String +((Start String (ntString)) + +(ntString String ( +firstname +lastname +" " +(str.++ ntString ntString))) + +(ntInt Int ( +0 +1 +2 +(+ ntInt ntInt) +(- ntInt ntInt) +(str.len ntString) +(str.to.int ntString) +(str.indexof ntString ntString ntInt))) + +(ntBool Bool ( +true +false +(str.prefixof ntString ntString) +(str.suffixof ntString ntString) +(str.contains ntString ntString))) + +)) + +(constraint (= (f "Nancy" "FreeHafer") "Nancy FreeHafer")) + +(check-synth) + diff --git a/test/regress/regress0/sygus/strings-unconstrained.sy b/test/regress/regress0/sygus/strings-unconstrained.sy new file mode 100644 index 000000000..38e69e337 --- /dev/null +++ b/test/regress/regress0/sygus/strings-unconstrained.sy @@ -0,0 +1,15 @@ +; EXPECT: unsat +; COMMAND-LINE: --no-dump-synth +(set-logic SLIA) +(synth-fun f ((firstname String) (lastname String)) String +((Start String (ntString)) + +(ntString String ( +firstname +lastname +" " +(str.++ ntString ntString))) +)) + +(check-synth) + diff --git a/test/regress/regress0/sygus/sygus-dt.sy b/test/regress/regress0/sygus/sygus-dt.sy index e842477e8..be6749139 100644 --- a/test/regress/regress0/sygus/sygus-dt.sy +++ b/test/regress/regress0/sygus/sygus-dt.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi --no-dump-synth +; COMMAND-LINE: --no-dump-synth (set-logic LIA) @@ -13,4 +13,4 @@ (declare-var x Int) (constraint (= (f x) (cons x nil))) -(check-synth)
\ No newline at end of file +(check-synth) diff --git a/test/regress/regress0/sygus/tl-type.sy b/test/regress/regress0/sygus/tl-type.sy index 1545f86cd..a6980425a 100644 --- a/test/regress/regress0/sygus/tl-type.sy +++ b/test/regress/regress0/sygus/tl-type.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi --no-cegqi-si --no-dump-synth +; COMMAND-LINE: --cegqi-si=none --no-dump-synth (set-logic LIA) (synth-fun f ((x Int)) Int ((Start Int (Term (+ Start Start))) diff --git a/test/regress/regress0/sygus/twolets1.sy b/test/regress/regress0/sygus/twolets1.sy index 7f84ce06c..b016872b4 100644 --- a/test/regress/regress0/sygus/twolets1.sy +++ b/test/regress/regress0/sygus/twolets1.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si --no-dump-synth +; COMMAND-LINE: --cegqi-si=all --no-dump-synth (set-logic LIA) ;; f1 is x plus 2 ;; f2 is 2x plus 5 diff --git a/test/regress/regress0/sygus/twolets2-orig.sy b/test/regress/regress0/sygus/twolets2-orig.sy index 91bab5ece..70d1ffa02 100644 --- a/test/regress/regress0/sygus/twolets2-orig.sy +++ b/test/regress/regress0/sygus/twolets2-orig.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si --no-dump-synth +; COMMAND-LINE: --cegqi-si=all --no-dump-synth (set-logic LIA) (synth-fun f1 ((x Int)) Int ( diff --git a/test/regress/regress0/sygus/uminus_one.sy b/test/regress/regress0/sygus/uminus_one.sy index 9886f6a7b..e98be942b 100644 --- a/test/regress/regress0/sygus/uminus_one.sy +++ b/test/regress/regress0/sygus/uminus_one.sy @@ -1,7 +1,7 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi --no-dump-synth +; COMMAND-LINE: --no-dump-synth (set-logic LIA) (synth-fun f ((x Int)) Int ((Start Int ((- 1))))) (declare-var x Int) (constraint (= (f x) (- 1))) -(check-synth)
\ No newline at end of file +(check-synth) diff --git a/test/regress/regress0/sygus/unbdd_inv_gen_winf1.sy b/test/regress/regress0/sygus/unbdd_inv_gen_winf1.sy index 7c9d6c601..300b6b65c 100644 --- a/test/regress/regress0/sygus/unbdd_inv_gen_winf1.sy +++ b/test/regress/regress0/sygus/unbdd_inv_gen_winf1.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi --no-dump-synth +; COMMAND-LINE: --no-dump-synth (set-logic LIA) (synth-fun inv ((x Int)) Bool |