diff options
Diffstat (limited to 'test/regress/regress0/sets')
26 files changed, 1 insertions, 3800 deletions
diff --git a/test/regress/regress0/sets/Makefile.am b/test/regress/regress0/sets/Makefile.am index de2170768..afcae32fe 100644 --- a/test/regress/regress0/sets/Makefile.am +++ b/test/regress/regress0/sets/Makefile.am @@ -19,36 +19,22 @@ MAKEFLAGS = -k # If a test shouldn't be run in e.g. competition mode, # put it below in "TESTS +=" TESTS = \ - jan24/insert_invariant_37_2.smt2 \ jan24/deepmeas0.hs.fqout.cvc4.47.smt2 \ jan24/deepmeas0.hs.fqout.small.smt2 \ - jan24/remove_check_free_31_6.smt2 \ - jan27/deepmeas0.hs.fqout.cvc4.41.smt2 \ jan27/ListConcat.hs.fqout.cvc4.177.smt2 \ jan27/ListConcat.hs.fqout.177minimized.smt2 \ - jan27/ListElem.hs.fqout.cvc4.38.smt2 \ jan28/TalkingAboutSets.hs.fqout.3577minimized.smt2 \ jan30/UniqueZipper.hs.fqout.minimized10.smt2 \ - jan30/UniqueZipper.hs.fqout.cvc4.10.smt2 \ jan30/UniqueZipper.hs.fqout.minimized1832.smt2 \ - jan30/UniqueZipper.hs.fqout.cvc4.1832.smt2 \ - feb3/ListElts.hs.fqout.cvc4.317.smt2 \ - mar2014/lemmabug-ListElts317minimized.smt2 \ mar2014/sharing-preregister.smt2 \ mar2014/small.smt2 \ mar2014/smaller.smt2 \ - mar2014/UniqueZipper.hs.1030minimized2.cvc4.smt2 \ - mar2014/UniqueZipper.hs.1030minimized.cvc4.smt2 \ - copy_check_heap_access_33_4.smt2 \ cvc-sample.cvc \ emptyset.smt2 \ error1.smt2 \ error2.smt2 \ eqtest.smt2 \ insert.smt2 \ - fuzz14418.smt2 \ - fuzz15201.smt2 \ - fuzz31811.smt2 \ rec_copy_loop_check_heap_access_43_4.smt2 \ sets-equal.smt2 \ sets-inter.smt2 \ @@ -56,7 +42,6 @@ TESTS = \ sets-sharing.smt2 \ sets-testlemma.smt2 \ sets-union.smt2 \ - sharingbug.smt2 \ union-1a-flip.smt2 \ union-1a.smt2 \ union-1b-flip.smt2 \ @@ -67,11 +52,6 @@ TESTS = \ card-3sets.cvc \ card.smt2 \ card-2.smt2 \ - card-3.smt2 \ - card-4.smt2 \ - card-5.smt2 \ - card-6.smt2 \ - card-7.smt2 \ abt-min.smt2 \ abt-te-exh.smt2 \ abt-te-exh2.smt2 \ @@ -85,24 +65,10 @@ TESTS = \ sets-poly-int-real.smt2 \ sets-poly-nonint.smt2 \ int-real-univ.smt2 \ - int-real-univ-unsat.smt2 \ - sets-tuple-poly.cvc \ - arjun-set-univ.cvc \ - univ-set-uf-elim.smt2 + int-real-univ-unsat.smt2 EXTRA_DIST = $(TESTS) -#if CVC4_BUILD_PROFILE_COMPETITION -#else -#TESTS += \ -# error.cvc -#endif - -# disabled tests, yet distribute -EXTRA_DIST += \ - jan28/TalkingAboutSets.hs.fqout.cvc4.3577.smt2 \ - setofsets-disequal.smt2 - # synonyms for "check" .PHONY: regress regress0 test regress regress0 test: check diff --git a/test/regress/regress0/sets/arjun-set-univ.cvc b/test/regress/regress0/sets/arjun-set-univ.cvc deleted file mode 100644 index 3c35a62a5..000000000 --- a/test/regress/regress0/sets/arjun-set-univ.cvc +++ /dev/null @@ -1,8 +0,0 @@ -% EXPECT: Extended set operators are not supported in default mode, try --sets-ext. -% EXIT: 1 -OPTION "produce-models" true; -x,y,z : SET OF BOOLEAN; -ASSERT x = {TRUE}; -ASSERT y = {FALSE}; -CHECKSAT z = ~ y; -COUNTERMODEL; diff --git a/test/regress/regress0/sets/card-3.smt2 b/test/regress/regress0/sets/card-3.smt2 deleted file mode 100644 index 0e96b0231..000000000 --- a/test/regress/regress0/sets/card-3.smt2 +++ /dev/null @@ -1,12 +0,0 @@ -(set-logic QF_UFLIAFS) -(set-info :status unsat) -(declare-sort E 0) -(declare-fun s () (Set E)) -(declare-fun t () (Set E)) -(declare-fun u () (Set E)) -(assert (>= (card (union s t)) 8)) -(assert (>= (card (union s u)) 8)) -(assert (<= (card (union t u)) 5)) -(assert (<= (card s) 5)) -(assert (= (as emptyset (Set E)) (intersection t u))) -(check-sat) diff --git a/test/regress/regress0/sets/card-4.smt2 b/test/regress/regress0/sets/card-4.smt2 deleted file mode 100644 index 456e24ca7..000000000 --- a/test/regress/regress0/sets/card-4.smt2 +++ /dev/null @@ -1,24 +0,0 @@ -(set-logic QF_UFLIAFS) -(set-info :status sat) -(declare-sort E 0) -(declare-fun s () (Set E)) -(declare-fun t () (Set E)) -(declare-fun u () (Set E)) -(assert (>= (card (union s t)) 8)) -(assert (>= (card (union s u)) 8)) -;(assert (<= (card (union t u)) 5)) -(assert (<= (card s) 5)) -(assert (= (as emptyset (Set E)) (intersection t u))) -(declare-fun x1 () E) -(declare-fun x2 () E) -(declare-fun x3 () E) -(declare-fun x4 () E) -(declare-fun x5 () E) -(declare-fun x6 () E) -(assert (member x1 s)) -(assert (member x2 s)) -(assert (member x3 s)) -(assert (member x4 s)) -(assert (member x5 s)) -(assert (member x6 s)) -(check-sat) diff --git a/test/regress/regress0/sets/card-5.smt2 b/test/regress/regress0/sets/card-5.smt2 deleted file mode 100644 index 4135a0c16..000000000 --- a/test/regress/regress0/sets/card-5.smt2 +++ /dev/null @@ -1,25 +0,0 @@ -(set-logic QF_UFLIAFS) -(set-info :status unsat) -(declare-sort E 0) -(declare-fun s () (Set E)) -(declare-fun t () (Set E)) -(declare-fun u () (Set E)) -(assert (>= (card (union s t)) 8)) -(assert (>= (card (union s u)) 8)) -;(assert (<= (card (union t u)) 5)) -(assert (<= (card s) 5)) -(assert (= (as emptyset (Set E)) (intersection t u))) -(declare-fun x1 () E) -(declare-fun x2 () E) -(declare-fun x3 () E) -(declare-fun x4 () E) -(declare-fun x5 () E) -(declare-fun x6 () E) -(assert (member x1 s)) -(assert (member x2 s)) -(assert (member x3 s)) -(assert (member x4 s)) -(assert (member x5 s)) -(assert (member x6 s)) -(assert (distinct x1 x2 x3 x4 x5 x6)) -(check-sat) diff --git a/test/regress/regress0/sets/card-6.smt2 b/test/regress/regress0/sets/card-6.smt2 deleted file mode 100644 index 87d87c03b..000000000 --- a/test/regress/regress0/sets/card-6.smt2 +++ /dev/null @@ -1,17 +0,0 @@ -(set-logic QF_UFLIAFS) -(set-info :status unsat) -(declare-sort E 0) -(declare-fun A () (Set E)) -(declare-fun B () (Set E)) -(declare-fun C () (Set E)) -(assert - (and - (= (as emptyset (Set E)) - (intersection A B)) - (subset C (union A B)) - (>= (card C) 5) - (<= (card A) 2) - (<= (card B) 2) - ) -) -(check-sat) diff --git a/test/regress/regress0/sets/card-7.smt2 b/test/regress/regress0/sets/card-7.smt2 deleted file mode 100644 index df1867c63..000000000 --- a/test/regress/regress0/sets/card-7.smt2 +++ /dev/null @@ -1,47 +0,0 @@ -(set-logic QF_UFLIAFS) -(set-info :status sat) -(declare-sort E 0) -(declare-fun A1 () (Set E)) -(declare-fun A2 () (Set E)) -(declare-fun A3 () (Set E)) -(declare-fun A4 () (Set E)) -(declare-fun A5 () (Set E)) -(declare-fun A6 () (Set E)) -(declare-fun A7 () (Set E)) -(declare-fun A8 () (Set E)) -(declare-fun A9 () (Set E)) -(declare-fun A10 () (Set E)) -(declare-fun A11 () (Set E)) -(declare-fun A12 () (Set E)) -(declare-fun A13 () (Set E)) -(declare-fun A14 () (Set E)) -(declare-fun A15 () (Set E)) -(declare-fun A16 () (Set E)) -(declare-fun A17 () (Set E)) -(declare-fun A18 () (Set E)) -(declare-fun A19 () (Set E)) -(declare-fun A20 () (Set E)) -(assert (and - (= (card A1) 1) - (= (card A2) 1) - (= (card A3) 1) - (= (card A4) 1) - (= (card A5) 1) - (= (card A6) 1) - (= (card A7) 1) - (= (card A8) 1) - (= (card A9) 1) - (= (card A10) 1) - (= (card A11) 1) - (= (card A12) 1) - (= (card A13) 1) - (= (card A14) 1) - (= (card A15) 1) - (= (card A16) 1) - (= (card A17) 1) - (= (card A18) 1) - (= (card A19) 1) - (= (card A20) 1) -)) -(assert (= 20 (+ (card A1) (card A2) (card A3) (card A4) (card A5) (card A6) (card A7) (card A8) (card A9) (card A10) (card A11) (card A12) (card A13) (card A14) (card A15) (card A16) (card A17) (card A18) (card A19) (card A20)))) -(check-sat) diff --git a/test/regress/regress0/sets/copy_check_heap_access_33_4.smt2 b/test/regress/regress0/sets/copy_check_heap_access_33_4.smt2 deleted file mode 100644 index 9af45c2dd..000000000 --- a/test/regress/regress0/sets/copy_check_heap_access_33_4.smt2 +++ /dev/null @@ -1,135 +0,0 @@ -; COMMAND-LINE: --full-saturate-quant -; EXPECT: unsat -(set-option :print-success false) -(set-logic AUFLIAFS) -(set-info :status unsat) -(declare-sort Loc 0) -(define-sort SetLoc () (Set Loc)) -(define-sort SetInt () (Set Int)) -(declare-sort FldLoc 0) -(declare-sort FldInt 0) -(declare-fun null$0 () Loc) -(declare-fun read$0 (FldInt Loc) Int) -(declare-fun read$1 (FldLoc Loc) Loc) -(declare-fun Btwn$0 (FldLoc Loc Loc Loc) Bool) -(declare-fun Alloc$0 () SetLoc) -(declare-fun Alloc_1$0 () SetLoc) -(declare-fun Axiom_1$0 () Bool) -(declare-fun FP$0 () SetLoc) -(declare-fun FP_1$0 () SetLoc) -(declare-fun FP_Caller$0 () SetLoc) -(declare-fun FP_Caller_1$0 () SetLoc) -(declare-fun cp_2$0 () Loc) -(declare-fun curr_2$0 () Loc) -(declare-fun data$0 () FldInt) -(declare-fun lst$0 () Loc) -(declare-fun next$0 () FldLoc) -(declare-fun res_1$0 () Loc) -(declare-fun sk_?X_4$0 () SetLoc) -(declare-fun slseg_domain$0 (FldInt FldLoc Loc Loc) SetLoc) -(declare-fun slseg_struct$0 (SetLoc FldInt FldLoc Loc Loc) Bool) -(declare-fun tmp_2$0 () Loc) - -(assert (! (forall ((?y Loc)) - (or (not (Btwn$0 next$0 null$0 ?y ?y)) (= null$0 ?y) - (Btwn$0 next$0 null$0 (read$1 next$0 null$0) ?y))) - :named btwn_reach_1)) - -(assert (! (forall ((?y Loc)) - (or (not (= (read$1 next$0 null$0) null$0)) - (not (Btwn$0 next$0 null$0 ?y ?y)) (= null$0 ?y))) - :named btwn_cycl_1)) - -(assert (! (Btwn$0 next$0 null$0 (read$1 next$0 null$0) (read$1 next$0 null$0)) - :named btwn_step_1)) - -(assert (! (forall ((l1 Loc) (l2 Loc)) - (or (not Axiom_1$0) - (or (<= (read$0 data$0 l1) (read$0 data$0 l2)) - (not (Btwn$0 next$0 l1 l2 null$0)) (not (member l1 sk_?X_4$0)) - (not (member l2 sk_?X_4$0))))) - :named sortedness_3)) - -(assert (! (= (read$1 next$0 null$0) null$0) :named read_null_1)) - -(assert (! (not (member tmp_2$0 Alloc$0)) :named new_31_11)) - -(assert (! (not (member null$0 Alloc$0)) :named initial_footprint_of_copy_23_11_2)) - -(assert (! (not (= lst$0 null$0)) :named if_else_26_6)) - -(assert (! (= FP_Caller$0 (union FP$0 FP_Caller$0)) - :named precondition_of_copy_23_11_4)) - -(assert (! (= sk_?X_4$0 FP$0) :named precondition_of_copy_23_11_5)) - -(assert (! (= res_1$0 tmp_2$0) :named assign_31_4)) - -(assert (! (= cp_2$0 res_1$0) :named assign_32_4)) - -(assert (! (= FP_1$0 (union FP$0 (singleton tmp_2$0))) :named assign_31_11)) - -(assert (! (or (and (Btwn$0 next$0 lst$0 null$0 null$0) Axiom_1$0) - (not (slseg_struct$0 sk_?X_4$0 data$0 next$0 lst$0 null$0))) - :named unnamed_3)) - -(assert (! (forall ((l1 Loc)) - (or - (and (Btwn$0 next$0 lst$0 l1 null$0) - (member l1 (slseg_domain$0 data$0 next$0 lst$0 null$0)) - (not (= l1 null$0))) - (and (or (= l1 null$0) (not (Btwn$0 next$0 lst$0 l1 null$0))) - (not (member l1 (slseg_domain$0 data$0 next$0 lst$0 null$0)))))) - :named slseg_footprint_2)) - -(assert (! (not (member curr_2$0 FP_1$0)) :named check_heap_access_33_4)) - -(assert (! (not (= tmp_2$0 null$0)) :named new_31_11_1)) - -(assert (! (slseg_struct$0 sk_?X_4$0 data$0 next$0 lst$0 null$0) - :named precondition_of_copy_23_11_6)) - -(assert (! (= sk_?X_4$0 (slseg_domain$0 data$0 next$0 lst$0 null$0)) - :named precondition_of_copy_23_11_7)) - -(assert (! (= Alloc$0 (union FP_Caller$0 Alloc$0)) - :named initial_footprint_of_copy_23_11_3)) - -(assert (! (= curr_2$0 lst$0) :named assign_30_4)) - -(assert (! (= FP_Caller_1$0 (setminus FP_Caller$0 FP$0)) :named assign_26_2_1)) - -(assert (! (= Alloc_1$0 (union Alloc$0 (singleton tmp_2$0))) :named assign_31_11_1)) - -(assert (! (forall ((?x Loc)) (Btwn$0 next$0 ?x ?x ?x)) :named btwn_refl_1)) - -(assert (! (forall ((?x Loc) (?y Loc)) (or (not (Btwn$0 next$0 ?x ?y ?x)) (= ?x ?y))) - :named btwn_sndw_1)) - -(assert (! (forall ((?x Loc) (?y Loc) (?z Loc)) - (or (not (Btwn$0 next$0 ?x ?y ?y)) (not (Btwn$0 next$0 ?x ?z ?z)) - (Btwn$0 next$0 ?x ?y ?z) (Btwn$0 next$0 ?x ?z ?y))) - :named btwn_ord1_1)) - -(assert (! (forall ((?x Loc) (?y Loc) (?z Loc)) - (or (not (Btwn$0 next$0 ?x ?y ?z)) - (and (Btwn$0 next$0 ?x ?y ?y) (Btwn$0 next$0 ?y ?z ?z)))) - :named btwn_ord2_1)) - -(assert (! (forall ((?x Loc) (?y Loc) (?z Loc)) - (or (not (Btwn$0 next$0 ?x ?y ?y)) (not (Btwn$0 next$0 ?y ?z ?z)) - (Btwn$0 next$0 ?x ?z ?z))) - :named btwn_trn1_1)) - -(assert (! (forall ((?u Loc) (?x Loc) (?y Loc) (?z Loc)) - (or (not (Btwn$0 next$0 ?x ?y ?z)) (not (Btwn$0 next$0 ?y ?u ?z)) - (and (Btwn$0 next$0 ?x ?y ?u) (Btwn$0 next$0 ?x ?u ?z)))) - :named btwn_trn2_1)) - -(assert (! (forall ((?u Loc) (?x Loc) (?y Loc) (?z Loc)) - (or (not (Btwn$0 next$0 ?x ?y ?z)) (not (Btwn$0 next$0 ?x ?u ?y)) - (and (Btwn$0 next$0 ?x ?u ?z) (Btwn$0 next$0 ?u ?y ?z)))) - :named btwn_trn3_1)) - -(check-sat) -(exit) diff --git a/test/regress/regress0/sets/feb3/ListElts.hs.fqout.cvc4.317.smt2 b/test/regress/regress0/sets/feb3/ListElts.hs.fqout.cvc4.317.smt2 deleted file mode 100644 index 7b5294aec..000000000 --- a/test/regress/regress0/sets/feb3/ListElts.hs.fqout.cvc4.317.smt2 +++ /dev/null @@ -1,98 +0,0 @@ -; EXPECT: sat -(set-logic QF_ALL_SUPPORTED) -(set-info :status sat) -(define-sort Elt () Int) -(define-sort mySet () (Set Elt )) -(define-fun smt_set_emp () mySet (as emptyset mySet)) -(define-fun smt_set_mem ((x Elt) (s mySet)) Bool (member x s)) -(define-fun smt_set_add ((s mySet) (x Elt)) mySet (union s (singleton x))) -(define-fun smt_set_cup ((s1 mySet) (s2 mySet)) mySet (union s1 s2)) -(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (intersection s1 s2)) -;(define-fun smt_set_com ((s mySet)) mySet ((_ map not) s)) -(define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (setminus s1 s2)) -;(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (= smt_set_emp (smt_set_dif s1 s2))) -(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subset s1 s2)) -(declare-fun z3v58 () Int) -(declare-fun z3v59 () Int) -(assert (distinct z3v58 z3v59)) -(declare-fun z3f60 (Int) Bool) -(declare-fun z3v61 () Int) -(declare-fun z3f62 (Int) Int) -(declare-fun z3v63 () Int) -(declare-fun z3v64 () Int) -(declare-fun z3v67 () Int) -(declare-fun z3f68 (Int) Int) -(declare-fun z3f69 (Int) mySet) -(declare-fun z3f70 (Int) mySet) -(declare-fun z3f71 (Int) Bool) -(declare-fun z3v73 () Int) -(declare-fun z3v76 () Int) -(declare-fun z3v79 () Int) -(declare-fun z3v82 () Int) -(declare-fun z3v84 () Int) -(declare-fun z3v85 () Int) -(declare-fun z3v86 () Int) -(declare-fun z3v89 () Int) -(declare-fun z3v90 () Int) -(declare-fun z3v91 () Int) -(declare-fun z3f92 (Int Int) Int) -(declare-fun z3v93 () Int) -(declare-fun z3v94 () Int) -(declare-fun z3f96 () Int) -(declare-fun z3v97 () Int) -(declare-fun z3v98 () Int) -(declare-fun z3v99 () Int) -(declare-fun z3v100 () Int) -(declare-fun z3v101 () Int) -(declare-fun z3v102 () Int) -(declare-fun z3v104 () Int) -(declare-fun z3v107 () Int) -(declare-fun z3v110 () Int) -(declare-fun z3v113 () Int) -(declare-fun z3v116 () Int) -(declare-fun z3v117 () Int) -(declare-fun z3v118 () Int) -(declare-fun z3v119 () Int) -(declare-fun z3v120 () Int) -(declare-fun z3v121 () Int) -(declare-fun z3v122 () Int) -(declare-fun z3v123 () Int) -(declare-fun z3v124 () Int) -(declare-fun z3v125 () Int) -(declare-fun z3v127 () Int) -(declare-fun z3v130 () Int) -(declare-fun z3v133 () Int) -(declare-fun z3v134 () Int) -(declare-fun z3v135 () Int) -(declare-fun z3v136 () Int) -(declare-fun z3v137 () Int) -(declare-fun z3v140 () Int) -(declare-fun z3v141 () Int) -(declare-fun z3v142 () Int) -(declare-fun z3v143 () Int) -(declare-fun z3v144 () Int) -(declare-fun z3v145 () Int) -(declare-fun z3v147 () Int) -(declare-fun z3v150 () Int) -(declare-fun z3v151 () Int) -(declare-fun z3v152 () Int) -(assert (= (z3f69 z3v152) (smt_set_cup (smt_set_add smt_set_emp z3v143) (z3f69 z3v151)))) -(assert (= (z3f70 z3v152) (smt_set_cup (smt_set_add smt_set_emp z3v143) (z3f70 z3v151)))) -(assert (= (z3f68 z3v152) (+ 1 (z3f68 z3v151)))) -(assert (= (z3f71 z3v152) false)) -(assert (and (>= (z3f68 z3v140) 0) (>= (z3f68 z3v141) 0) (>= (z3f68 z3v151) 0) (>= (z3f68 z3v142) 0) (= (z3f69 z3v142) (smt_set_cup (smt_set_add smt_set_emp z3v143) (z3f69 z3v141))) (= (z3f70 z3v142) (smt_set_cup (smt_set_add smt_set_emp z3v143) (z3f70 z3v141))) (= (z3f68 z3v142) (+ 1 (z3f68 z3v141))) (= (z3f71 z3v142) false) (= z3v142 (z3f92 z3v143 z3v141)) (>= (z3f68 z3v142) 0) (= z3v142 z3v144) (>= (z3f68 z3v142) 0) (>= (z3f68 z3v144) 0) (z3f60 z3v58) (= (z3f62 z3v61) z3v61) (= (z3f62 z3v63) z3v63) (not (z3f60 z3v59)) (= (z3f62 z3v64) z3v64))) -(assert (= (z3f69 z3v151) (smt_set_cup (z3f69 z3v140) (z3f69 z3v141)))) -(assert (= (z3f69 z3v151) (smt_set_cup (z3f69 z3v140) (z3f69 z3v140)))) -(assert (= (z3f69 z3v151) (smt_set_cup (z3f69 z3v141) (z3f69 z3v140)))) -(assert (smt_set_sub (z3f69 z3v151) (z3f69 z3v140))) -(assert (= (z3f69 z3v151) (z3f69 z3v140))) -(assert (<= z3v151 z3v140)) -(assert (>= z3v151 z3v140)) -(assert (<= (z3f68 z3v151) (z3f68 z3v140))) -(assert (>= (z3f68 z3v151) (z3f68 z3v141))) -(assert (>= (z3f68 z3v151) (z3f68 z3v140))) -(assert (= (z3f68 z3v151) (z3f68 z3v140))) -(assert (= z3v151 z3v140)) -(assert (>= (z3f68 z3v151) 0)) -(assert (not (= (z3f69 z3v152) (smt_set_cup (z3f69 z3v140) (z3f69 z3v140))))) -(check-sat) diff --git a/test/regress/regress0/sets/fuzz14418.smt2 b/test/regress/regress0/sets/fuzz14418.smt2 deleted file mode 100644 index 24679749c..000000000 --- a/test/regress/regress0/sets/fuzz14418.smt2 +++ /dev/null @@ -1,171 +0,0 @@ -; symptom: assertion failure in EqEngine : hasTerm(t) -; -; issue: had some nodes in d_pending, even though sat context had been popped, -; and those were no longer relevant. -; -; fix: make pending queues sat context depending. d_pendingEverInserted which -; is still user-context dependent takes care of not generating a lemma twice. -; -; sat -(set-info :source |fuzzsmt|) -(set-info :smt-lib-version 2.0) -(set-info :category "random") -(set-info :status sat) -(set-logic QF_UFLIAFS) -(define-sort Element () Int) -(declare-fun f0 ( Int) Int) -(declare-fun f1 ( (Set Element) (Set Element) (Set Element)) (Set Element)) -(declare-fun p0 ( Int Int) Bool) -(declare-fun p1 ( (Set Element)) Bool) -(declare-fun v0 () Int) -(declare-fun v1 () (Set Element)) -(declare-fun v2 () (Set Element)) -(declare-fun v3 () (Set Element)) -(declare-fun v4 () (Set Element)) -(assert (let ((e5 7)) -(let ((e6 (* e5 v0))) -(let ((e7 (* v0 e5))) -(let ((e8 (f0 e6))) -(let ((e9 (* v0 (- e5)))) -(let ((e10 (f0 v0))) -(let ((e11 (* (- e5) e10))) -(let ((e12 (ite (p0 e7 e6) 1 0))) -(let ((e13 (union v3 v4))) -(let ((e14 (setminus v2 v2))) -(let ((e15 (f1 v1 v4 v1))) -(let ((e16 (f1 e14 v1 v4))) -(let ((e17 (intersection e16 e15))) -(let ((e18 (f1 v4 e15 v2))) -(let ((e19 (ite (p1 e13) (singleton 1) (singleton 0)))) -(let ((e20 (member v0 e17))) -(let ((e21 (member e7 e16))) -(let ((e22 (member e10 e16))) -(let ((e23 (member e8 e17))) -(let ((e24 (member e9 e14))) -(let ((e25 (member e8 e16))) -(let ((e26 (member v0 e13))) -(let ((e27 (member e12 v4))) -(let ((e28 (member e8 e14))) -(let ((e29 (member e8 v1))) -(let ((e30 (member e10 e13))) -(let ((e31 (member e7 e13))) -(let ((e32 (f1 e13 e13 e13))) -(let ((e33 (f1 e18 v4 e17))) -(let ((e34 (f1 v2 v2 e15))) -(let ((e35 (f1 e33 e18 e15))) -(let ((e36 (f1 e19 e14 e17))) -(let ((e37 (f1 e34 e18 e34))) -(let ((e38 (f1 v3 e34 e18))) -(let ((e39 (f1 e16 v4 e13))) -(let ((e40 (f1 v1 e34 e15))) -(let ((e41 (< e10 e11))) -(let ((e42 (= e6 e12))) -(let ((e43 (> e6 e11))) -(let ((e44 (< e12 e8))) -(let ((e45 (< e7 e10))) -(let ((e46 (= e11 e12))) -(let ((e47 (= e11 e7))) -(let ((e48 (<= e11 e10))) -(let ((e49 (p0 e9 e9))) -(let ((e50 (>= v0 e10))) -(let ((e51 (ite e22 e14 e33))) -(let ((e52 (ite e45 e16 e37))) -(let ((e53 (ite e42 e39 e17))) -(let ((e54 (ite e21 e39 e33))) -(let ((e55 (ite e29 e13 e13))) -(let ((e56 (ite e48 e15 e34))) -(let ((e57 (ite e50 e38 e53))) -(let ((e58 (ite e47 e32 v1))) -(let ((e59 (ite e20 e36 e33))) -(let ((e60 (ite e28 e35 v2))) -(let ((e61 (ite e48 e40 e38))) -(let ((e62 (ite e30 e38 e53))) -(let ((e63 (ite e22 v4 e19))) -(let ((e64 (ite e46 e60 e53))) -(let ((e65 (ite e25 e61 e16))) -(let ((e66 (ite e23 v3 e38))) -(let ((e67 (ite e49 v4 e18))) -(let ((e68 (ite e21 e54 v3))) -(let ((e69 (ite e25 e15 v4))) -(let ((e70 (ite e20 e55 e19))) -(let ((e71 (ite e27 e38 e36))) -(let ((e72 (ite e28 e14 e33))) -(let ((e73 (ite e42 e66 e60))) -(let ((e74 (ite e26 e54 e69))) -(let ((e75 (ite e28 e68 e71))) -(let ((e76 (ite e24 e33 e52))) -(let ((e77 (ite e44 e40 e74))) -(let ((e78 (ite e48 e32 e51))) -(let ((e79 (ite e22 e34 e62))) -(let ((e80 (ite e22 e78 e73))) -(let ((e81 (ite e22 e13 e55))) -(let ((e82 (ite e43 e37 e70))) -(let ((e83 (ite e48 e59 e80))) -(let ((e84 (ite e29 e15 e77))) -(let ((e85 (ite e41 e19 e35))) -(let ((e86 (ite e22 e63 e69))) -(let ((e87 (ite e26 e19 e70))) -(let ((e88 (ite e46 e37 e53))) -(let ((e89 (ite e25 e70 e76))) -(let ((e90 (ite e31 v4 e73))) -(let ((e91 (ite e46 e12 e8))) -(let ((e92 (ite e43 e11 e6))) -(let ((e93 (ite e50 e10 e7))) -(let ((e94 (ite e21 e8 e7))) -(let ((e95 (ite e27 v0 e6))) -(let ((e96 (ite e24 e9 e92))) -(let ((e97 (ite e22 e6 e92))) -(let ((e98 (ite e49 e96 e12))) -(let ((e99 (ite e27 e98 e6))) -(let ((e100 (ite e31 e11 e8))) -(let ((e101 (ite e26 e12 v0))) -(let ((e102 (ite e22 e92 e96))) -(let ((e103 (ite e28 e92 e6))) -(let ((e104 (ite e27 e12 v0))) -(let ((e105 (ite e23 e101 e9))) -(let ((e106 (ite e47 e11 e104))) -(let ((e107 (ite e45 e105 e100))) -(let ((e108 (ite e48 e12 e9))) -(let ((e109 (ite e42 e96 e91))) -(let ((e110 (ite e29 e11 e101))) -(let ((e111 (ite e50 e107 e110))) -(let ((e112 (ite e29 e104 e92))) -(let ((e113 (ite e20 e108 e12))) -(let ((e114 (ite e44 e96 e104))) -(let ((e115 (ite e41 e105 e110))) -(let ((e116 (ite e41 e6 e103))) -(let ((e117 (ite e28 e92 e114))) -(let ((e118 (ite e30 e111 e113))) -(let ((e119 (ite e30 e109 e8))) -(let ((e120 (ite e25 e12 e118))) -(let ((e121 (xor e46 e42))) -(let ((e122 (xor e28 e29))) -(let ((e123 (= e122 e49))) -(let ((e124 (and e43 e45))) -(let ((e125 (or e121 e23))) -(let ((e126 (and e125 e24))) -(let ((e127 (= e41 e126))) -(let ((e128 (xor e124 e44))) -(let ((e129 (not e26))) -(let ((e130 (= e22 e123))) -(let ((e131 (not e20))) -(let ((e132 (and e127 e27))) -(let ((e133 (=> e50 e131))) -(let ((e134 (=> e132 e30))) -(let ((e135 (xor e128 e48))) -(let ((e136 (ite e129 e47 e129))) -(let ((e137 (and e133 e130))) -(let ((e138 (or e136 e134))) -(let ((e139 (and e31 e31))) -(let ((e140 (not e137))) -(let ((e141 (= e140 e139))) -(let ((e142 (= e25 e21))) -(let ((e143 (not e142))) -(let ((e144 (and e143 e135))) -(let ((e145 (and e144 e138))) -(let ((e146 (and e145 e145))) -(let ((e147 (= e141 e146))) -e147 -)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) - -(check-sat) diff --git a/test/regress/regress0/sets/fuzz15201.smt2 b/test/regress/regress0/sets/fuzz15201.smt2 deleted file mode 100644 index e12b74d18..000000000 --- a/test/regress/regress0/sets/fuzz15201.smt2 +++ /dev/null @@ -1,269 +0,0 @@ -; symptom: unsat instead of sat -; issue/fix: buggy rewriter for setminus -(set-info :source |fuzzsmt|) -(set-info :smt-lib-version 2.0) -(set-info :category "random") -(set-info :status sat) -(set-logic QF_UFLIAFS) -(define-sort Element () Int) -(declare-fun f0 ( Int) Int) -(declare-fun f1 ( (Set Element)) (Set Element)) -(declare-fun p0 ( Int) Bool) -(declare-fun p1 ( (Set Element) (Set Element) (Set Element)) Bool) -(declare-fun v0 () Int) -(declare-fun v1 () (Set Element)) -(declare-fun v2 () (Set Element)) -(assert (let ((e3 0)) -(let ((e4 (+ v0 v0))) -(let ((e5 (+ v0 e4))) -(let ((e6 (* (- e3) e4))) -(let ((e7 (- e4 e6))) -(let ((e8 (+ e7 e5))) -(let ((e9 (- v0))) -(let ((e10 (* e6 e3))) -(let ((e11 (- e8 e5))) -(let ((e12 (- e5))) -(let ((e13 (* e7 (- e3)))) -(let ((e14 (f0 e7))) -(let ((e15 (ite (p0 e9) 1 0))) -(let ((e16 (setminus v2 v1))) -(let ((e17 (setminus v1 v2))) -(let ((e18 (union e17 e17))) -(let ((e19 (intersection e17 v1))) -(let ((e20 (intersection e17 e18))) -(let ((e21 (intersection v1 e16))) -(let ((e22 (setminus e20 e16))) -(let ((e23 (ite (p1 v2 e18 e21) (singleton 1) (singleton 0)))) -(let ((e24 (setminus e17 e23))) -(let ((e25 (union v2 e22))) -(let ((e26 (union e24 e18))) -(let ((e27 (ite (p1 e20 e19 e25) (singleton 1) (singleton 0)))) -(let ((e28 (f1 e20))) -(let ((e29 (member e14 e17))) -(let ((e30 (member e13 e23))) -(let ((e31 (member e11 e25))) -(let ((e32 (member e6 v1))) -(let ((e33 (member e9 v1))) -(let ((e34 (member v0 e28))) -(let ((e35 (member e9 e16))) -(let ((e36 (member e4 e17))) -(let ((e37 (member e9 e18))) -(let ((e38 (member e14 e25))) -(let ((e39 (member e14 v2))) -(let ((e40 (member v0 v1))) -(let ((e41 (member e4 e16))) -(let ((e42 (member e15 e21))) -(let ((e43 (member e7 e22))) -(let ((e44 (member e11 v2))) -(let ((e45 (member e14 e22))) -(let ((e46 (member e11 e16))) -(let ((e47 (member e15 e22))) -(let ((e48 (member e10 e23))) -(let ((e49 (member e4 e21))) -(let ((e50 (member e5 e28))) -(let ((e51 (member e6 e28))) -(let ((e52 (member v0 e22))) -(let ((e53 (member e14 e20))) -(let ((e54 (f1 e21))) -(let ((e55 (f1 e28))) -(let ((e56 (f1 e27))) -(let ((e57 (f1 e17))) -(let ((e58 (f1 e22))) -(let ((e59 (f1 e26))) -(let ((e60 (f1 e19))) -(let ((e61 (f1 v1))) -(let ((e62 (f1 e24))) -(let ((e63 (f1 e20))) -(let ((e64 (f1 e23))) -(let ((e65 (f1 v2))) -(let ((e66 (f1 e25))) -(let ((e67 (f1 e62))) -(let ((e68 (f1 e18))) -(let ((e69 (f1 e18))) -(let ((e70 (f1 e23))) -(let ((e71 (f1 e55))) -(let ((e72 (f1 e26))) -(let ((e73 (f1 e16))) -(let ((e74 (= e13 e13))) -(let ((e75 (p0 e11))) -(let ((e76 (distinct e15 e4))) -(let ((e77 (> e14 e10))) -(let ((e78 (= e4 e15))) -(let ((e79 (distinct v0 e9))) -(let ((e80 (= e15 e14))) -(let ((e81 (>= e10 e11))) -(let ((e82 (distinct e9 e8))) -(let ((e83 (p0 v0))) -(let ((e84 (>= e12 e14))) -(let ((e85 (distinct e7 e13))) -(let ((e86 (<= e6 e11))) -(let ((e87 (= e13 e10))) -(let ((e88 (>= e7 e8))) -(let ((e89 (<= v0 e10))) -(let ((e90 (>= e5 e15))) -(let ((e91 (ite e33 e66 e26))) -(let ((e92 (ite e88 e54 v1))) -(let ((e93 (ite e76 e70 e16))) -(let ((e94 (ite e85 e19 e24))) -(let ((e95 (ite e88 e68 e20))) -(let ((e96 (ite e86 e25 e65))) -(let ((e97 (ite e83 v2 e23))) -(let ((e98 (ite e50 e63 e63))) -(let ((e99 (ite e48 e56 e93))) -(let ((e100 (ite e38 e60 v2))) -(let ((e101 (ite e30 e61 e61))) -(let ((e102 (ite e85 e69 e57))) -(let ((e103 (ite e83 e18 e102))) -(let ((e104 (ite e43 e62 e97))) -(let ((e105 (ite e76 e27 e21))) -(let ((e106 (ite e89 e92 e55))) -(let ((e107 (ite e46 e72 e65))) -(let ((e108 (ite e79 e71 e97))) -(let ((e109 (ite e44 e64 e21))) -(let ((e110 (ite e33 e70 e25))) -(let ((e111 (ite e43 e63 e105))) -(let ((e112 (ite e39 e56 e108))) -(let ((e113 (ite e49 e17 e107))) -(let ((e114 (ite e74 e63 e113))) -(let ((e115 (ite e84 e28 v1))) -(let ((e116 (ite e82 e68 e67))) -(let ((e117 (ite e75 e73 e21))) -(let ((e118 (ite e36 e59 e16))) -(let ((e119 (ite e48 e118 e61))) -(let ((e120 (ite e90 e56 e100))) -(let ((e121 (ite e80 e24 e25))) -(let ((e122 (ite e31 e22 v2))) -(let ((e123 (ite e45 e107 e16))) -(let ((e124 (ite e40 e70 e73))) -(let ((e125 (ite e52 e58 e118))) -(let ((e126 (ite e88 e72 e72))) -(let ((e127 (ite e35 e58 e27))) -(let ((e128 (ite e42 e59 e21))) -(let ((e129 (ite e44 e127 e103))) -(let ((e130 (ite e51 e118 e69))) -(let ((e131 (ite e37 e16 e24))) -(let ((e132 (ite e83 e105 e28))) -(let ((e133 (ite e48 e107 e60))) -(let ((e134 (ite e34 e101 e22))) -(let ((e135 (ite e86 e97 e57))) -(let ((e136 (ite e47 e94 e100))) -(let ((e137 (ite e78 e104 e95))) -(let ((e138 (ite e75 e26 e96))) -(let ((e139 (ite e35 e97 e121))) -(let ((e140 (ite e44 e112 e118))) -(let ((e141 (ite e77 e107 e56))) -(let ((e142 (ite e53 e64 e129))) -(let ((e143 (ite e48 e128 e23))) -(let ((e144 (ite e50 e73 e17))) -(let ((e145 (ite e33 e98 e114))) -(let ((e146 (ite e32 e137 e105))) -(let ((e147 (ite e41 e98 e96))) -(let ((e148 (ite e29 e93 e121))) -(let ((e149 (ite e87 e104 e21))) -(let ((e150 (ite e46 e131 e110))) -(let ((e151 (ite e81 e25 e65))) -(let ((e152 (ite e34 e10 e10))) -(let ((e153 (ite e36 e7 e13))) -(let ((e154 (ite e43 e12 e10))) -(let ((e155 (ite e50 e14 e7))) -(let ((e156 (ite e34 e9 e6))) -(let ((e157 (ite e33 e7 v0))) -(let ((e158 (ite e50 e157 e10))) -(let ((e159 (ite e51 e8 e11))) -(let ((e160 (ite e32 v0 e157))) -(let ((e161 (ite e85 e15 e158))) -(let ((e162 (ite e43 e5 e11))) -(let ((e163 (ite e76 e4 v0))) -(let ((e164 (ite e53 e10 e159))) -(let ((e165 (ite e80 e161 e163))) -(let ((e166 (ite e78 e13 e11))) -(let ((e167 (ite e49 e4 e8))) -(let ((e168 (ite e45 e11 e155))) -(let ((e169 (ite e81 e155 e166))) -(let ((e170 (ite e87 e169 e161))) -(let ((e171 (ite e53 e165 e13))) -(let ((e172 (ite e83 e12 e160))) -(let ((e173 (ite e80 e168 e159))) -(let ((e174 (ite e46 e171 e168))) -(let ((e175 (ite e74 e5 e155))) -(let ((e176 (ite e89 e159 e4))) -(let ((e177 (ite e29 e159 e172))) -(let ((e178 (ite e79 e165 e162))) -(let ((e179 (ite e88 e166 e168))) -(let ((e180 (ite e77 e175 e167))) -(let ((e181 (ite e47 e157 e165))) -(let ((e182 (ite e84 e172 e7))) -(let ((e183 (ite e30 e174 e157))) -(let ((e184 (ite e90 e4 e14))) -(let ((e185 (ite e38 e178 e14))) -(let ((e186 (ite e44 e166 e154))) -(let ((e187 (ite e42 e162 e186))) -(let ((e188 (ite e86 e187 e10))) -(let ((e189 (ite e29 e171 e182))) -(let ((e190 (ite e77 e185 e165))) -(let ((e191 (ite e75 e171 e9))) -(let ((e192 (ite e39 e161 e181))) -(let ((e193 (ite e82 e166 e10))) -(let ((e194 (ite e31 e183 e179))) -(let ((e195 (ite e44 e191 e169))) -(let ((e196 (ite e35 e171 e156))) -(let ((e197 (ite e86 e179 e164))) -(let ((e198 (ite e41 e5 e5))) -(let ((e199 (ite e85 e160 e161))) -(let ((e200 (ite e52 e173 e157))) -(let ((e201 (ite e47 e161 e4))) -(let ((e202 (ite e52 e6 e186))) -(let ((e203 (ite e45 e162 e198))) -(let ((e204 (ite e48 e194 e11))) -(let ((e205 (ite e37 e197 e157))) -(let ((e206 (ite e35 e153 e176))) -(let ((e207 (ite e40 e185 e188))) -(let ((e208 (= e53 e41))) -(let ((e209 (not e79))) -(let ((e210 (= e30 e87))) -(let ((e211 (or e34 e48))) -(let ((e212 (=> e82 e29))) -(let ((e213 (xor e77 e211))) -(let ((e214 (and e31 e78))) -(let ((e215 (ite e36 e76 e37))) -(let ((e216 (= e84 e45))) -(let ((e217 (or e43 e46))) -(let ((e218 (and e88 e40))) -(let ((e219 (not e89))) -(let ((e220 (not e35))) -(let ((e221 (or e218 e213))) -(let ((e222 (xor e216 e75))) -(let ((e223 (ite e85 e90 e219))) -(let ((e224 (= e32 e217))) -(let ((e225 (not e39))) -(let ((e226 (xor e212 e49))) -(let ((e227 (and e222 e81))) -(let ((e228 (or e33 e210))) -(let ((e229 (xor e225 e226))) -(let ((e230 (xor e74 e47))) -(let ((e231 (= e220 e38))) -(let ((e232 (xor e231 e229))) -(let ((e233 (and e50 e221))) -(let ((e234 (and e42 e224))) -(let ((e235 (xor e223 e214))) -(let ((e236 (= e234 e228))) -(let ((e237 (and e227 e235))) -(let ((e238 (not e51))) -(let ((e239 (= e80 e232))) -(let ((e240 (or e230 e86))) -(let ((e241 (not e238))) -(let ((e242 (xor e44 e237))) -(let ((e243 (= e236 e242))) -(let ((e244 (= e209 e240))) -(let ((e245 (and e239 e83))) -(let ((e246 (or e208 e245))) -(let ((e247 (=> e215 e246))) -(let ((e248 (ite e233 e247 e244))) -(let ((e249 (and e248 e241))) -(let ((e250 (=> e243 e249))) -(let ((e251 (and e52 e250))) -e251 -)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) - -(check-sat) -;(get-model) diff --git a/test/regress/regress0/sets/fuzz31811.smt2 b/test/regress/regress0/sets/fuzz31811.smt2 deleted file mode 100644 index 5e7c032ea..000000000 --- a/test/regress/regress0/sets/fuzz31811.smt2 +++ /dev/null @@ -1,187 +0,0 @@ -; symptom: assertion failure : conflict <=> equality engine inconsistent -; -; issue: the assertion is too strong. what is true is that there is an internal -; conflict <=> equality engine inconsistent. but in case of propagating (dis)equalities -; between shared terms, the some other theory might become inconsistent, and we should -; stop. -; -(set-info :source |fuzzsmt|) -(set-info :smt-lib-version 2.0) -(set-info :category "random") -(set-info :status sat) -(set-logic QF_UFLIAFS) -(define-sort Element () Int) -(declare-fun f0 ( Int Int Int) Int) -(declare-fun f1 ( (Set Element) (Set Element)) (Set Element)) -(declare-fun p0 ( Int Int Int) Bool) -(declare-fun p1 ( (Set Element)) Bool) -(declare-fun v0 () Int) -(declare-fun v1 () (Set Element)) -(declare-fun v2 () (Set Element)) -(declare-fun v3 () (Set Element)) -(declare-fun v4 () (Set Element)) -(assert (let ((e5 2)) -(let ((e6 (+ v0 v0))) -(let ((e7 (* e6 e5))) -(let ((e8 (* e6 (- e5)))) -(let ((e9 (ite (p0 e7 v0 e6) 1 0))) -(let ((e10 (f0 v0 e8 e8))) -(let ((e11 (ite (p1 v1) (singleton 1) (singleton 0)))) -(let ((e12 (union v3 v3))) -(let ((e13 (intersection v3 v1))) -(let ((e14 (ite (p1 v3) (singleton 1) (singleton 0)))) -(let ((e15 (intersection v2 e14))) -(let ((e16 (ite (p1 e11) (singleton 1) (singleton 0)))) -(let ((e17 (ite (p1 v4) (singleton 1) (singleton 0)))) -(let ((e18 (union e15 v2))) -(let ((e19 (ite (p1 e16) (singleton 1) (singleton 0)))) -(let ((e20 (intersection e18 v3))) -(let ((e21 (setminus v4 e12))) -(let ((e22 (union v3 v2))) -(let ((e23 (setminus e12 v4))) -(let ((e24 (setminus v3 e16))) -(let ((e25 (intersection e19 e20))) -(let ((e26 (ite (p1 e15) (singleton 1) (singleton 0)))) -(let ((e27 (setminus e17 e15))) -(let ((e28 (f1 e23 e12))) -(let ((e29 (member e10 e16))) -(let ((e30 (member e10 v1))) -(let ((e31 (member e7 e19))) -(let ((e32 (f1 e12 e12))) -(let ((e33 (f1 e16 e25))) -(let ((e34 (f1 v1 e27))) -(let ((e35 (f1 e19 e19))) -(let ((e36 (f1 e24 e32))) -(let ((e37 (f1 e28 e35))) -(let ((e38 (f1 e27 e20))) -(let ((e39 (f1 e23 e23))) -(let ((e40 (f1 e39 e27))) -(let ((e41 (f1 e17 e32))) -(let ((e42 (f1 e34 e33))) -(let ((e43 (f1 e34 e17))) -(let ((e44 (f1 e34 e25))) -(let ((e45 (f1 e26 e26))) -(let ((e46 (f1 e17 e21))) -(let ((e47 (f1 e40 e26))) -(let ((e48 (f1 e16 v2))) -(let ((e49 (f1 e46 e33))) -(let ((e50 (f1 e15 e15))) -(let ((e51 (f1 e18 e18))) -(let ((e52 (f1 e15 e18))) -(let ((e53 (f1 e11 e49))) -(let ((e54 (f1 e14 e42))) -(let ((e55 (f1 e48 e18))) -(let ((e56 (f1 e49 e52))) -(let ((e57 (f1 v4 e12))) -(let ((e58 (f1 e22 e45))) -(let ((e59 (f1 e13 e13))) -(let ((e60 (f1 v3 e36))) -(let ((e61 (distinct e8 e7))) -(let ((e62 (> v0 e8))) -(let ((e63 (< e10 e10))) -(let ((e64 (distinct v0 e10))) -(let ((e65 (<= e7 e8))) -(let ((e66 (distinct e9 v0))) -(let ((e67 (<= e6 e8))) -(let ((e68 (p0 e8 e7 e6))) -(let ((e69 (ite e63 e35 e13))) -(let ((e70 (ite e66 e25 e32))) -(let ((e71 (ite e62 e33 e19))) -(let ((e72 (ite e64 e46 v1))) -(let ((e73 (ite e65 e59 e51))) -(let ((e74 (ite e30 e14 e26))) -(let ((e75 (ite e68 e36 e39))) -(let ((e76 (ite e66 e35 e34))) -(let ((e77 (ite e64 e44 e54))) -(let ((e78 (ite e61 e70 e46))) -(let ((e79 (ite e31 e60 e26))) -(let ((e80 (ite e64 e55 e19))) -(let ((e81 (ite e63 e58 e33))) -(let ((e82 (ite e29 e32 e75))) -(let ((e83 (ite e67 e27 e73))) -(let ((e84 (ite e63 e51 e60))) -(let ((e85 (ite e64 e16 e73))) -(let ((e86 (ite e68 e47 e46))) -(let ((e87 (ite e67 v2 e11))) -(let ((e88 (ite e63 e59 e75))) -(let ((e89 (ite e30 e12 e83))) -(let ((e90 (ite e62 e45 e87))) -(let ((e91 (ite e29 e36 e89))) -(let ((e92 (ite e68 e24 e16))) -(let ((e93 (ite e61 e49 e76))) -(let ((e94 (ite e61 e12 e54))) -(let ((e95 (ite e67 e33 e16))) -(let ((e96 (ite e66 e26 e15))) -(let ((e97 (ite e65 e52 e13))) -(let ((e98 (ite e68 e38 e17))) -(let ((e99 (ite e65 e48 e46))) -(let ((e100 (ite e31 v3 e95))) -(let ((e101 (ite e31 e95 e18))) -(let ((e102 (ite e66 e37 e78))) -(let ((e103 (ite e31 e33 e17))) -(let ((e104 (ite e62 e55 e91))) -(let ((e105 (ite e65 e20 e90))) -(let ((e106 (ite e63 e22 e79))) -(let ((e107 (ite e64 e94 e97))) -(let ((e108 (ite e61 e53 e80))) -(let ((e109 (ite e63 e23 e52))) -(let ((e110 (ite e31 e100 e101))) -(let ((e111 (ite e68 e28 e98))) -(let ((e112 (ite e62 e50 e74))) -(let ((e113 (ite e30 e49 e96))) -(let ((e114 (ite e67 e14 e40))) -(let ((e115 (ite e61 e92 e91))) -(let ((e116 (ite e65 e18 e89))) -(let ((e117 (ite e63 e34 e51))) -(let ((e118 (ite e64 e56 e47))) -(let ((e119 (ite e68 e102 e18))) -(let ((e120 (ite e61 e43 e53))) -(let ((e121 (ite e31 e41 e98))) -(let ((e122 (ite e67 e114 e103))) -(let ((e123 (ite e65 v4 e92))) -(let ((e124 (ite e68 e33 e88))) -(let ((e125 (ite e68 e37 e101))) -(let ((e126 (ite e31 e36 e26))) -(let ((e127 (ite e65 e21 e95))) -(let ((e128 (ite e62 e42 v4))) -(let ((e129 (ite e66 e100 e19))) -(let ((e130 (ite e66 e78 e12))) -(let ((e131 (ite e62 e34 e103))) -(let ((e132 (ite e64 e59 e14))) -(let ((e133 (ite e31 e53 e89))) -(let ((e134 (ite e66 e57 e60))) -(let ((e135 (ite e31 e7 e10))) -(let ((e136 (ite e67 e10 e9))) -(let ((e137 (ite e65 e136 v0))) -(let ((e138 (ite e68 e6 e7))) -(let ((e139 (ite e66 e9 e9))) -(let ((e140 (ite e62 e8 e135))) -(let ((e141 (ite e30 e137 e6))) -(let ((e142 (ite e30 e140 e138))) -(let ((e143 (ite e29 e140 e6))) -(let ((e144 (ite e67 e141 v0))) -(let ((e145 (ite e62 e6 e137))) -(let ((e146 (ite e29 e137 e139))) -(let ((e147 (ite e30 e140 e144))) -(let ((e148 (ite e66 e142 e141))) -(let ((e149 (ite e63 e8 e144))) -(let ((e150 (ite e31 e135 e140))) -(let ((e151 (ite e64 e147 e141))) -(let ((e152 (ite e61 e147 e148))) -(let ((e153 (or e30 e63))) -(let ((e154 (or e67 e62))) -(let ((e155 (ite e154 e29 e154))) -(let ((e156 (and e66 e155))) -(let ((e157 (=> e31 e64))) -(let ((e158 (or e65 e153))) -(let ((e159 (not e158))) -(let ((e160 (xor e157 e68))) -(let ((e161 (xor e159 e61))) -(let ((e162 (= e156 e160))) -(let ((e163 (or e161 e161))) -(let ((e164 (not e162))) -(let ((e165 (=> e164 e163))) -e165 -)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) - -(check-sat) diff --git a/test/regress/regress0/sets/jan24/insert_invariant_37_2.smt2 b/test/regress/regress0/sets/jan24/insert_invariant_37_2.smt2 deleted file mode 100644 index 2ef07f920..000000000 --- a/test/regress/regress0/sets/jan24/insert_invariant_37_2.smt2 +++ /dev/null @@ -1,812 +0,0 @@ -(set-option :print-success false) -(set-logic AUFLIAFS) -(set-info :status unsat) -(declare-sort Loc 0) -(define-sort SetLoc () (Set Loc)) -(define-sort SetInt () (Set Int)) -(declare-sort FldLoc 0) -(declare-sort FldInt 0) -(declare-fun null$0 () Loc) -(declare-fun read$0 (FldInt Loc) Int) -(declare-fun read$1 (FldLoc Loc) Loc) -(declare-fun Btwn$0 (FldLoc Loc Loc Loc) Bool) -(declare-fun Alloc$0 () SetLoc) -(declare-fun Axiom$0 () Bool) -(declare-fun FP$0 () SetLoc) -(declare-fun FP_Caller$0 () SetLoc) -(declare-fun FP_Caller_1$0 () SetLoc) -(declare-fun c1_2$0 () SetInt) -(declare-fun c2_2$0 () SetInt) -(declare-fun content$0 () SetInt) -(declare-fun curr_2$0 () Loc) -(declare-fun data$0 () FldInt) -(declare-fun lst$0 () Loc) -(declare-fun next$0 () FldLoc) -(declare-fun prev_2$0 () Loc) -(declare-fun sk_?X$0 () SetLoc) -(declare-fun sk_?X_1$0 () SetLoc) -(declare-fun sk_?X_2$0 () SetLoc) -(declare-fun sk_?X_3$0 () SetLoc) -(declare-fun sk_?X_4$0 () SetLoc) -(declare-fun sk_?X_5$0 () SetLoc) -(declare-fun sk_?e$0 () Int) -(declare-fun sk_?e_1$0 () Loc) -(declare-fun sk_?e_2$0 () Loc) -(declare-fun sk_?e_3$0 () Int) -(declare-fun sk_FP$0 () SetLoc) -(declare-fun sk_FP_1$0 () SetLoc) -(declare-fun sk_l1$0 () Loc) -(declare-fun sk_l1_1$0 () Loc) -(declare-fun sk_l2$0 () Loc) -(declare-fun sk_l2_1$0 () Loc) -(declare-fun sorted_set_c$0 (FldInt FldLoc Loc Loc) SetInt) -(declare-fun sorted_set_domain$0 (FldInt FldLoc Loc Loc) SetLoc) -(declare-fun sorted_set_struct$0 (SetLoc FldInt FldLoc Loc Loc SetInt) Bool) -(declare-fun val$0 () Int) -(declare-fun witness$0 (Int SetInt) Loc) - -(assert (! (forall ((?y Loc)) - (or (not (Btwn$0 next$0 null$0 ?y ?y)) (= null$0 ?y) - (Btwn$0 next$0 null$0 (read$1 next$0 null$0) ?y))) - :named btwn_reach)) - -(assert (! (forall ((?y Loc)) - (or (not (= (read$1 next$0 null$0) null$0)) - (not (Btwn$0 next$0 null$0 ?y ?y)) (= null$0 ?y))) - :named btwn_cycl)) - -(assert (! (Btwn$0 next$0 null$0 (read$1 next$0 null$0) (read$1 next$0 null$0)) - :named btwn_step)) - -(assert (! (forall ((l1 Loc) (l2 Loc)) - (or (not Axiom$0) - (or (= l1 l2) (< (read$0 data$0 l1) (read$0 data$0 l2)) - (not (Btwn$0 next$0 l1 l2 null$0)) (not (member l1 sk_?X$0)) - (not (member l2 sk_?X$0))))) - :named strict_sortedness)) - -(assert (! (forall ((l1 Loc)) - (or (= l1 null$0) - (member (read$0 data$0 l1) - (sorted_set_c$0 data$0 next$0 lst$0 null$0)) - (not (Btwn$0 next$0 lst$0 l1 null$0)))) - :named sorted_set_1)) - -(assert (! (and - (or - (= - (witness$0 (read$0 data$0 curr_2$0) - (sorted_set_c$0 data$0 next$0 lst$0 null$0)) - null$0) - (member (read$0 data$0 curr_2$0) - (sorted_set_c$0 data$0 next$0 lst$0 null$0))) - (or - (and - (= (read$0 data$0 curr_2$0) - (read$0 data$0 - (witness$0 (read$0 data$0 curr_2$0) - (sorted_set_c$0 data$0 next$0 lst$0 null$0)))) - (member - (witness$0 (read$0 data$0 curr_2$0) - (sorted_set_c$0 data$0 next$0 lst$0 null$0)) - (sorted_set_domain$0 data$0 next$0 lst$0 null$0))) - (not - (member (read$0 data$0 curr_2$0) - (sorted_set_c$0 data$0 next$0 lst$0 null$0))))) - :named sorted_set_2)) - -(assert (! (and - (or - (= - (witness$0 (read$0 data$0 prev_2$0) - (sorted_set_c$0 data$0 next$0 lst$0 null$0)) - null$0) - (member (read$0 data$0 prev_2$0) - (sorted_set_c$0 data$0 next$0 lst$0 null$0))) - (or - (and - (= (read$0 data$0 prev_2$0) - (read$0 data$0 - (witness$0 (read$0 data$0 prev_2$0) - (sorted_set_c$0 data$0 next$0 lst$0 null$0)))) - (member - (witness$0 (read$0 data$0 prev_2$0) - (sorted_set_c$0 data$0 next$0 lst$0 null$0)) - (sorted_set_domain$0 data$0 next$0 lst$0 null$0))) - (not - (member (read$0 data$0 prev_2$0) - (sorted_set_c$0 data$0 next$0 lst$0 null$0))))) - :named sorted_set_2_1)) - -(assert (! (and - (or - (= - (witness$0 (read$0 data$0 sk_l1$0) - (sorted_set_c$0 data$0 next$0 lst$0 null$0)) - null$0) - (member (read$0 data$0 sk_l1$0) - (sorted_set_c$0 data$0 next$0 lst$0 null$0))) - (or - (and - (= (read$0 data$0 sk_l1$0) - (read$0 data$0 - (witness$0 (read$0 data$0 sk_l1$0) - (sorted_set_c$0 data$0 next$0 lst$0 null$0)))) - (member - (witness$0 (read$0 data$0 sk_l1$0) - (sorted_set_c$0 data$0 next$0 lst$0 null$0)) - (sorted_set_domain$0 data$0 next$0 lst$0 null$0))) - (not - (member (read$0 data$0 sk_l1$0) - (sorted_set_c$0 data$0 next$0 lst$0 null$0))))) - :named sorted_set_2_2)) - -(assert (! (and - (or - (= - (witness$0 (read$0 data$0 sk_l1_1$0) - (sorted_set_c$0 data$0 next$0 lst$0 null$0)) - null$0) - (member (read$0 data$0 sk_l1_1$0) - (sorted_set_c$0 data$0 next$0 lst$0 null$0))) - (or - (and - (= (read$0 data$0 sk_l1_1$0) - (read$0 data$0 - (witness$0 (read$0 data$0 sk_l1_1$0) - (sorted_set_c$0 data$0 next$0 lst$0 null$0)))) - (member - (witness$0 (read$0 data$0 sk_l1_1$0) - (sorted_set_c$0 data$0 next$0 lst$0 null$0)) - (sorted_set_domain$0 data$0 next$0 lst$0 null$0))) - (not - (member (read$0 data$0 sk_l1_1$0) - (sorted_set_c$0 data$0 next$0 lst$0 null$0))))) - :named sorted_set_2_3)) - -(assert (! (and - (or - (= - (witness$0 (read$0 data$0 sk_l2$0) - (sorted_set_c$0 data$0 next$0 lst$0 null$0)) - null$0) - (member (read$0 data$0 sk_l2$0) - (sorted_set_c$0 data$0 next$0 lst$0 null$0))) - (or - (and - (= (read$0 data$0 sk_l2$0) - (read$0 data$0 - (witness$0 (read$0 data$0 sk_l2$0) - (sorted_set_c$0 data$0 next$0 lst$0 null$0)))) - (member - (witness$0 (read$0 data$0 sk_l2$0) - (sorted_set_c$0 data$0 next$0 lst$0 null$0)) - (sorted_set_domain$0 data$0 next$0 lst$0 null$0))) - (not - (member (read$0 data$0 sk_l2$0) - (sorted_set_c$0 data$0 next$0 lst$0 null$0))))) - :named sorted_set_2_4)) - -(assert (! (and - (or - (= - (witness$0 (read$0 data$0 sk_l2_1$0) - (sorted_set_c$0 data$0 next$0 lst$0 null$0)) - null$0) - (member (read$0 data$0 sk_l2_1$0) - (sorted_set_c$0 data$0 next$0 lst$0 null$0))) - (or - (and - (= (read$0 data$0 sk_l2_1$0) - (read$0 data$0 - (witness$0 (read$0 data$0 sk_l2_1$0) - (sorted_set_c$0 data$0 next$0 lst$0 null$0)))) - (member - (witness$0 (read$0 data$0 sk_l2_1$0) - (sorted_set_c$0 data$0 next$0 lst$0 null$0)) - (sorted_set_domain$0 data$0 next$0 lst$0 null$0))) - (not - (member (read$0 data$0 sk_l2_1$0) - (sorted_set_c$0 data$0 next$0 lst$0 null$0))))) - :named sorted_set_2_5)) - -(assert (! (and - (or - (= - (witness$0 sk_?e$0 (sorted_set_c$0 data$0 next$0 lst$0 null$0)) - null$0) - (member sk_?e$0 (sorted_set_c$0 data$0 next$0 lst$0 null$0))) - (or - (and - (= sk_?e$0 - (read$0 data$0 - (witness$0 sk_?e$0 - (sorted_set_c$0 data$0 next$0 lst$0 null$0)))) - (member - (witness$0 sk_?e$0 - (sorted_set_c$0 data$0 next$0 lst$0 null$0)) - (sorted_set_domain$0 data$0 next$0 lst$0 null$0))) - (not (member sk_?e$0 (sorted_set_c$0 data$0 next$0 lst$0 null$0))))) - :named sorted_set_2_6)) - -(assert (! (and - (or - (= - (witness$0 sk_?e_3$0 - (sorted_set_c$0 data$0 next$0 lst$0 null$0)) - null$0) - (member sk_?e_3$0 (sorted_set_c$0 data$0 next$0 lst$0 null$0))) - (or - (and - (= sk_?e_3$0 - (read$0 data$0 - (witness$0 sk_?e_3$0 - (sorted_set_c$0 data$0 next$0 lst$0 null$0)))) - (member - (witness$0 sk_?e_3$0 - (sorted_set_c$0 data$0 next$0 lst$0 null$0)) - (sorted_set_domain$0 data$0 next$0 lst$0 null$0))) - (not (member sk_?e_3$0 (sorted_set_c$0 data$0 next$0 lst$0 null$0))))) - :named sorted_set_2_7)) - -(assert (! (forall ((l1 Loc)) - (or (= l1 null$0) - (member (read$0 data$0 l1) - (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)) - (not (Btwn$0 next$0 curr_2$0 l1 null$0)))) - :named sorted_set_1_1)) - -(assert (! (forall ((l1 Loc)) - (or (= l1 curr_2$0) - (member (read$0 data$0 l1) - (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)) - (not (Btwn$0 next$0 lst$0 l1 curr_2$0)))) - :named sorted_set_1_2)) - -(assert (! (and - (or - (= - (witness$0 (read$0 data$0 curr_2$0) - (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)) - null$0) - (member (read$0 data$0 curr_2$0) - (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))) - (or - (and - (= (read$0 data$0 curr_2$0) - (read$0 data$0 - (witness$0 (read$0 data$0 curr_2$0) - (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)))) - (member - (witness$0 (read$0 data$0 curr_2$0) - (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)) - (sorted_set_domain$0 data$0 next$0 curr_2$0 null$0))) - (not - (member (read$0 data$0 curr_2$0) - (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))))) - :named sorted_set_2_8)) - -(assert (! (and - (or - (= - (witness$0 (read$0 data$0 prev_2$0) - (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)) - null$0) - (member (read$0 data$0 prev_2$0) - (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))) - (or - (and - (= (read$0 data$0 prev_2$0) - (read$0 data$0 - (witness$0 (read$0 data$0 prev_2$0) - (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)))) - (member - (witness$0 (read$0 data$0 prev_2$0) - (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)) - (sorted_set_domain$0 data$0 next$0 curr_2$0 null$0))) - (not - (member (read$0 data$0 prev_2$0) - (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))))) - :named sorted_set_2_9)) - -(assert (! (and - (or - (= - (witness$0 (read$0 data$0 sk_l1$0) - (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)) - null$0) - (member (read$0 data$0 sk_l1$0) - (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))) - (or - (and - (= (read$0 data$0 sk_l1$0) - (read$0 data$0 - (witness$0 (read$0 data$0 sk_l1$0) - (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)))) - (member - (witness$0 (read$0 data$0 sk_l1$0) - (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)) - (sorted_set_domain$0 data$0 next$0 curr_2$0 null$0))) - (not - (member (read$0 data$0 sk_l1$0) - (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))))) - :named sorted_set_2_10)) - -(assert (! (and - (or - (= - (witness$0 (read$0 data$0 sk_l1_1$0) - (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)) - null$0) - (member (read$0 data$0 sk_l1_1$0) - (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))) - (or - (and - (= (read$0 data$0 sk_l1_1$0) - (read$0 data$0 - (witness$0 (read$0 data$0 sk_l1_1$0) - (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)))) - (member - (witness$0 (read$0 data$0 sk_l1_1$0) - (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)) - (sorted_set_domain$0 data$0 next$0 curr_2$0 null$0))) - (not - (member (read$0 data$0 sk_l1_1$0) - (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))))) - :named sorted_set_2_11)) - -(assert (! (and - (or - (= - (witness$0 (read$0 data$0 sk_l2$0) - (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)) - null$0) - (member (read$0 data$0 sk_l2$0) - (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))) - (or - (and - (= (read$0 data$0 sk_l2$0) - (read$0 data$0 - (witness$0 (read$0 data$0 sk_l2$0) - (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)))) - (member - (witness$0 (read$0 data$0 sk_l2$0) - (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)) - (sorted_set_domain$0 data$0 next$0 curr_2$0 null$0))) - (not - (member (read$0 data$0 sk_l2$0) - (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))))) - :named sorted_set_2_12)) - -(assert (! (and - (or - (= - (witness$0 (read$0 data$0 sk_l2_1$0) - (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)) - null$0) - (member (read$0 data$0 sk_l2_1$0) - (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))) - (or - (and - (= (read$0 data$0 sk_l2_1$0) - (read$0 data$0 - (witness$0 (read$0 data$0 sk_l2_1$0) - (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)))) - (member - (witness$0 (read$0 data$0 sk_l2_1$0) - (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)) - (sorted_set_domain$0 data$0 next$0 curr_2$0 null$0))) - (not - (member (read$0 data$0 sk_l2_1$0) - (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))))) - :named sorted_set_2_13)) - -(assert (! (and - (or - (= - (witness$0 sk_?e$0 - (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)) - null$0) - (member sk_?e$0 (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))) - (or - (and - (= sk_?e$0 - (read$0 data$0 - (witness$0 sk_?e$0 - (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)))) - (member - (witness$0 sk_?e$0 - (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)) - (sorted_set_domain$0 data$0 next$0 curr_2$0 null$0))) - (not (member sk_?e$0 (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))))) - :named sorted_set_2_14)) - -(assert (! (and - (or - (= - (witness$0 sk_?e_3$0 - (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)) - null$0) - (member sk_?e_3$0 (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))) - (or - (and - (= sk_?e_3$0 - (read$0 data$0 - (witness$0 sk_?e_3$0 - (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)))) - (member - (witness$0 sk_?e_3$0 - (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)) - (sorted_set_domain$0 data$0 next$0 curr_2$0 null$0))) - (not - (member sk_?e_3$0 - (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))))) - :named sorted_set_2_15)) - -(assert (! (and - (or - (= - (witness$0 (read$0 data$0 curr_2$0) - (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)) - null$0) - (member (read$0 data$0 curr_2$0) - (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))) - (or - (and - (= (read$0 data$0 curr_2$0) - (read$0 data$0 - (witness$0 (read$0 data$0 curr_2$0) - (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)))) - (member - (witness$0 (read$0 data$0 curr_2$0) - (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)) - (sorted_set_domain$0 data$0 next$0 lst$0 curr_2$0))) - (not - (member (read$0 data$0 curr_2$0) - (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))))) - :named sorted_set_2_16)) - -(assert (! (and - (or - (= - (witness$0 (read$0 data$0 prev_2$0) - (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)) - null$0) - (member (read$0 data$0 prev_2$0) - (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))) - (or - (and - (= (read$0 data$0 prev_2$0) - (read$0 data$0 - (witness$0 (read$0 data$0 prev_2$0) - (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)))) - (member - (witness$0 (read$0 data$0 prev_2$0) - (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)) - (sorted_set_domain$0 data$0 next$0 lst$0 curr_2$0))) - (not - (member (read$0 data$0 prev_2$0) - (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))))) - :named sorted_set_2_17)) - -(assert (! (and - (or - (= - (witness$0 (read$0 data$0 sk_l1$0) - (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)) - null$0) - (member (read$0 data$0 sk_l1$0) - (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))) - (or - (and - (= (read$0 data$0 sk_l1$0) - (read$0 data$0 - (witness$0 (read$0 data$0 sk_l1$0) - (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)))) - (member - (witness$0 (read$0 data$0 sk_l1$0) - (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)) - (sorted_set_domain$0 data$0 next$0 lst$0 curr_2$0))) - (not - (member (read$0 data$0 sk_l1$0) - (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))))) - :named sorted_set_2_18)) - -(assert (! (and - (or - (= - (witness$0 (read$0 data$0 sk_l1_1$0) - (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)) - null$0) - (member (read$0 data$0 sk_l1_1$0) - (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))) - (or - (and - (= (read$0 data$0 sk_l1_1$0) - (read$0 data$0 - (witness$0 (read$0 data$0 sk_l1_1$0) - (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)))) - (member - (witness$0 (read$0 data$0 sk_l1_1$0) - (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)) - (sorted_set_domain$0 data$0 next$0 lst$0 curr_2$0))) - (not - (member (read$0 data$0 sk_l1_1$0) - (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))))) - :named sorted_set_2_19)) - -(assert (! (and - (or - (= - (witness$0 (read$0 data$0 sk_l2$0) - (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)) - null$0) - (member (read$0 data$0 sk_l2$0) - (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))) - (or - (and - (= (read$0 data$0 sk_l2$0) - (read$0 data$0 - (witness$0 (read$0 data$0 sk_l2$0) - (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)))) - (member - (witness$0 (read$0 data$0 sk_l2$0) - (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)) - (sorted_set_domain$0 data$0 next$0 lst$0 curr_2$0))) - (not - (member (read$0 data$0 sk_l2$0) - (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))))) - :named sorted_set_2_20)) - -(assert (! (and - (or - (= - (witness$0 (read$0 data$0 sk_l2_1$0) - (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)) - null$0) - (member (read$0 data$0 sk_l2_1$0) - (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))) - (or - (and - (= (read$0 data$0 sk_l2_1$0) - (read$0 data$0 - (witness$0 (read$0 data$0 sk_l2_1$0) - (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)))) - (member - (witness$0 (read$0 data$0 sk_l2_1$0) - (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)) - (sorted_set_domain$0 data$0 next$0 lst$0 curr_2$0))) - (not - (member (read$0 data$0 sk_l2_1$0) - (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))))) - :named sorted_set_2_21)) - -(assert (! (and - (or - (= - (witness$0 sk_?e$0 - (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)) - null$0) - (member sk_?e$0 (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))) - (or - (and - (= sk_?e$0 - (read$0 data$0 - (witness$0 sk_?e$0 - (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)))) - (member - (witness$0 sk_?e$0 - (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)) - (sorted_set_domain$0 data$0 next$0 lst$0 curr_2$0))) - (not (member sk_?e$0 (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))))) - :named sorted_set_2_22)) - -(assert (! (and - (or - (= - (witness$0 sk_?e_3$0 - (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)) - null$0) - (member sk_?e_3$0 (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))) - (or - (and - (= sk_?e_3$0 - (read$0 data$0 - (witness$0 sk_?e_3$0 - (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)))) - (member - (witness$0 sk_?e_3$0 - (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)) - (sorted_set_domain$0 data$0 next$0 lst$0 curr_2$0))) - (not - (member sk_?e_3$0 (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))))) - :named sorted_set_2_23)) - -(assert (! (= (read$1 next$0 null$0) null$0) :named read_null)) - -(assert (! (forall ((l1 Loc)) - (or - (and (Btwn$0 next$0 lst$0 l1 null$0) - (member l1 (sorted_set_domain$0 data$0 next$0 lst$0 null$0)) - (not (= l1 null$0))) - (and (or (= l1 null$0) (not (Btwn$0 next$0 lst$0 l1 null$0))) - (not - (member l1 - (sorted_set_domain$0 data$0 next$0 lst$0 null$0)))))) - :named sorted_set_footprint)) - -(assert (! (or (member sk_?e_3$0 c2_2$0) - (and (member sk_?e_2$0 sk_FP_1$0) (not (member sk_?e_2$0 FP$0))) - (and (member sk_?e_3$0 (union c1_2$0 c2_2$0)) - (not (member sk_?e_3$0 content$0))) - (and (member sk_?e_3$0 c1_2$0) - (not - (member sk_?e_3$0 - (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)))) - (and (member sk_?e_3$0 content$0) - (not (member sk_?e_3$0 (union c1_2$0 c2_2$0)))) - (and (member sk_?e_3$0 (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)) - (not (member sk_?e_3$0 c1_2$0))) - (and (not (= curr_2$0 null$0)) (not (= prev_2$0 null$0)) - (not (< (read$0 data$0 prev_2$0) (read$0 data$0 curr_2$0)))) - (not (= curr_2$0 lst$0)) (not (= prev_2$0 null$0)) - (not - (sorted_set_struct$0 sk_?X_3$0 data$0 next$0 curr_2$0 null$0 - c1_2$0))) - :named invariant_37_2)) - -(assert (! (= sk_FP_1$0 sk_?X_2$0) :named invariant_37_2_1)) - -(assert (! (= sk_?X_5$0 (sorted_set_domain$0 data$0 next$0 lst$0 curr_2$0)) - :named invariant_37_2_2)) - -(assert (! (= sk_?X_3$0 (sorted_set_domain$0 data$0 next$0 curr_2$0 null$0)) - :named invariant_37_2_3)) - -(assert (! (= sk_?X_1$0 (union sk_?X_3$0 sk_?X_4$0)) :named invariant_37_2_4)) - -(assert (! (= FP_Caller$0 (union FP$0 FP_Caller$0)) - :named precondition_of_insert_27_11)) - -(assert (! (= sk_?X$0 FP$0) :named precondition_of_insert_27_11_1)) - -(assert (! (= Alloc$0 (union FP_Caller$0 Alloc$0)) - :named initial_footprint_of_insert_27_11)) - -(assert (! (= curr_2$0 lst$0) :named assign_31_2)) - -(assert (! (= c1_2$0 content$0) :named assign_34_2)) - -(assert (! (or (and (Btwn$0 next$0 lst$0 null$0 null$0) Axiom$0) - (not - (sorted_set_struct$0 sk_?X$0 data$0 next$0 lst$0 null$0 - content$0))) - :named unnamed)) - -(assert (! (or (sorted_set_struct$0 sk_?X_3$0 data$0 next$0 curr_2$0 null$0 c1_2$0) - (not (Btwn$0 next$0 curr_2$0 null$0 null$0)) - (! (and (Btwn$0 next$0 sk_l1$0 sk_l2$0 null$0) (member sk_l1$0 sk_?X_3$0) - (member sk_l2$0 sk_?X_3$0) (not (= sk_l1$0 sk_l2$0)) - (not (< (read$0 data$0 sk_l1$0) (read$0 data$0 sk_l2$0)))) - :named strict_sortedness_1)) - :named unnamed_1)) - -(assert (! (forall ((l1 Loc)) - (or - (and (Btwn$0 next$0 lst$0 l1 curr_2$0) - (member l1 - (sorted_set_domain$0 data$0 next$0 lst$0 curr_2$0)) - (not (= l1 curr_2$0))) - (and - (or (= l1 curr_2$0) - (not (Btwn$0 next$0 lst$0 l1 curr_2$0))) - (not - (member l1 - (sorted_set_domain$0 data$0 next$0 lst$0 curr_2$0)))))) - :named sorted_set_footprint_1)) - -(assert (! (forall ((l1 Loc)) - (or - (and (Btwn$0 next$0 curr_2$0 l1 null$0) - (member l1 - (sorted_set_domain$0 data$0 next$0 curr_2$0 null$0)) - (not (= l1 null$0))) - (and - (or (= l1 null$0) - (not (Btwn$0 next$0 curr_2$0 l1 null$0))) - (not - (member l1 - (sorted_set_domain$0 data$0 next$0 curr_2$0 - null$0)))))) - :named sorted_set_footprint_2)) - -(assert (! (not (member null$0 Alloc$0)) :named initial_footprint_of_insert_27_11_1)) - -(assert (! (or (= prev_2$0 curr_2$0) - (member sk_?e_1$0 (intersection sk_?X_4$0 sk_?X_3$0)) - (and (member sk_?e_1$0 sk_FP$0) (not (member sk_?e_1$0 FP$0))) - (and (member sk_?e$0 (union c1_2$0 c2_2$0)) (not (member sk_?e$0 content$0))) - (and (member sk_?e$0 c1_2$0) - (not (member sk_?e$0 (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)))) - (and (member sk_?e$0 c2_2$0) - (not (member sk_?e$0 (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)))) - (and (member sk_?e$0 content$0) (not (member sk_?e$0 (union c1_2$0 c2_2$0)))) - (and (member sk_?e$0 (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)) - (not (member sk_?e$0 c1_2$0))) - (and (member sk_?e$0 (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)) - (not (member sk_?e$0 c2_2$0))) - (and (not (= curr_2$0 null$0)) (not (= prev_2$0 null$0)) - (not (< (read$0 data$0 prev_2$0) (read$0 data$0 curr_2$0)))) - (not (= (read$1 next$0 prev_2$0) curr_2$0)) - (not (> val$0 (read$0 data$0 prev_2$0))) - (not (Btwn$0 next$0 lst$0 prev_2$0 curr_2$0)) - (not - (sorted_set_struct$0 sk_?X_3$0 data$0 next$0 curr_2$0 null$0 - c1_2$0)) - (not - (sorted_set_struct$0 sk_?X_5$0 data$0 next$0 lst$0 curr_2$0 - c2_2$0))) - :named invariant_37_2_5)) - -(assert (! (= sk_FP$0 sk_?X_1$0) :named invariant_37_2_6)) - -(assert (! (= sk_?X_4$0 sk_?X_5$0) :named invariant_37_2_7)) - -(assert (! (= sk_?X_2$0 sk_?X_3$0) :named invariant_37_2_8)) - -(assert (! (sorted_set_struct$0 sk_?X$0 data$0 next$0 lst$0 null$0 content$0) - :named precondition_of_insert_27_11_2)) - -(assert (! (= sk_?X$0 (sorted_set_domain$0 data$0 next$0 lst$0 null$0)) - :named precondition_of_insert_27_11_3)) - -(assert (! (= content$0 (sorted_set_c$0 data$0 next$0 lst$0 null$0)) - :named precondition_of_insert_27_11_4)) - -(assert (! (= prev_2$0 null$0) :named assign_32_2)) - -(assert (! (= c2_2$0 (as emptyset SetInt)) :named assign_35_2)) - -(assert (! (= FP_Caller_1$0 (setminus FP_Caller$0 FP$0)) :named assign_29_0)) - -(assert (! (or (sorted_set_struct$0 sk_?X_5$0 data$0 next$0 lst$0 curr_2$0 c2_2$0) - (not (Btwn$0 next$0 lst$0 curr_2$0 curr_2$0)) - (! (and (Btwn$0 next$0 sk_l1_1$0 sk_l2_1$0 curr_2$0) - (member sk_l1_1$0 sk_?X_5$0) (member sk_l2_1$0 sk_?X_5$0) - (not (= sk_l1_1$0 sk_l2_1$0)) - (not (< (read$0 data$0 sk_l1_1$0) (read$0 data$0 sk_l2_1$0)))) - :named strict_sortedness_2)) - :named unnamed_2)) - -(assert (! (forall ((?x Loc)) (Btwn$0 next$0 ?x ?x ?x)) :named btwn_refl)) - -(assert (! (forall ((?x Loc) (?y Loc)) (or (not (Btwn$0 next$0 ?x ?y ?x)) (= ?x ?y))) - :named btwn_sndw)) - -(assert (! (forall ((?x Loc) (?y Loc) (?z Loc)) - (or (not (Btwn$0 next$0 ?x ?y ?y)) (not (Btwn$0 next$0 ?x ?z ?z)) - (Btwn$0 next$0 ?x ?y ?z) (Btwn$0 next$0 ?x ?z ?y))) - :named btwn_ord1)) - -(assert (! (forall ((?x Loc) (?y Loc) (?z Loc)) - (or (not (Btwn$0 next$0 ?x ?y ?z)) - (and (Btwn$0 next$0 ?x ?y ?y) (Btwn$0 next$0 ?y ?z ?z)))) - :named btwn_ord2)) - -(assert (! (forall ((?x Loc) (?y Loc) (?z Loc)) - (or (not (Btwn$0 next$0 ?x ?y ?y)) (not (Btwn$0 next$0 ?y ?z ?z)) - (Btwn$0 next$0 ?x ?z ?z))) - :named btwn_trn1)) - -(assert (! (forall ((?u Loc) (?x Loc) (?y Loc) (?z Loc)) - (or (not (Btwn$0 next$0 ?x ?y ?z)) (not (Btwn$0 next$0 ?y ?u ?z)) - (and (Btwn$0 next$0 ?x ?y ?u) (Btwn$0 next$0 ?x ?u ?z)))) - :named btwn_trn2)) - -(assert (! (forall ((?u Loc) (?x Loc) (?y Loc) (?z Loc)) - (or (not (Btwn$0 next$0 ?x ?y ?z)) (not (Btwn$0 next$0 ?x ?u ?y)) - (and (Btwn$0 next$0 ?x ?u ?z) (Btwn$0 next$0 ?u ?y ?z)))) - :named btwn_trn3)) - -(check-sat) -(exit) diff --git a/test/regress/regress0/sets/jan24/remove_check_free_31_6.smt2 b/test/regress/regress0/sets/jan24/remove_check_free_31_6.smt2 deleted file mode 100644 index 2bf2d4c62..000000000 --- a/test/regress/regress0/sets/jan24/remove_check_free_31_6.smt2 +++ /dev/null @@ -1,470 +0,0 @@ -(set-option :print-success false) -(set-logic AUFLIAFS) -(set-info :status unsat) -(declare-sort Loc 0) -(define-sort SetLoc () (Set Loc)) -(define-sort SetInt () (Set Int)) -(declare-sort FldLoc 0) -(declare-sort FldInt 0) -(declare-fun null$0 () Loc) -(declare-fun read$0 (FldLoc Loc) Loc) -(declare-fun write$0 (FldLoc Loc Loc) FldLoc) -(declare-fun ep$0 (FldLoc SetLoc Loc) Loc) -(declare-fun Btwn$0 (FldLoc Loc Loc Loc) Bool) -(declare-fun Frame$0 (SetLoc SetLoc FldLoc FldLoc) Bool) -(declare-fun Alloc$0 () SetLoc) -(declare-fun FP$0 () SetLoc) -(declare-fun FP_1$0 () SetLoc) -(declare-fun FP_2$0 () SetLoc) -(declare-fun FP_Caller$0 () SetLoc) -(declare-fun FP_Caller_1$0 () SetLoc) -(declare-fun curr_2$0 () Loc) -(declare-fun curr_3$0 () Loc) -(declare-fun lseg_domain$0 (FldLoc Loc Loc) SetLoc) -(declare-fun lseg_struct$0 (SetLoc FldLoc Loc Loc) Bool) -(declare-fun lst$0 () Loc) -(declare-fun lst_1$0 () Loc) -(declare-fun next$0 () FldLoc) -(declare-fun next_1$0 () FldLoc) -(declare-fun nondet_2$0 () Bool) -(declare-fun sk_?X_27$0 () SetLoc) -(declare-fun sk_?X_28$0 () SetLoc) -(declare-fun sk_?X_29$0 () SetLoc) -(declare-fun sk_?X_30$0 () SetLoc) -(declare-fun sk_?X_31$0 () SetLoc) -(declare-fun sk_?X_32$0 () SetLoc) -(declare-fun sk_?X_33$0 () SetLoc) -(declare-fun tmp_2$0 () Loc) - -(assert (! (forall ((?y Loc)) - (or (not (Btwn$0 next$0 null$0 ?y ?y)) (= null$0 ?y) - (Btwn$0 next$0 null$0 (read$0 next$0 null$0) ?y))) - :named btwn_reach_8)) - -(assert (! (forall ((?y Loc)) - (or (not (Btwn$0 next$0 tmp_2$0 ?y ?y)) (= tmp_2$0 ?y) - (Btwn$0 next$0 tmp_2$0 (read$0 next$0 tmp_2$0) ?y))) - :named btwn_reach_9)) - -(assert (! (forall ((?y Loc)) - (or (not (Btwn$0 next$0 curr_3$0 ?y ?y)) (= curr_3$0 ?y) - (Btwn$0 next$0 curr_3$0 (read$0 next$0 curr_3$0) ?y))) - :named btwn_reach_10)) - -(assert (! (forall ((?y Loc)) - (or (not (= (read$0 next$0 null$0) null$0)) - (not (Btwn$0 next$0 null$0 ?y ?y)) (= null$0 ?y))) - :named btwn_cycl_8)) - -(assert (! (forall ((?y Loc)) - (or (not (= (read$0 next$0 tmp_2$0) tmp_2$0)) - (not (Btwn$0 next$0 tmp_2$0 ?y ?y)) (= tmp_2$0 ?y))) - :named btwn_cycl_9)) - -(assert (! (forall ((?y Loc)) - (or (not (= (read$0 next$0 curr_3$0) curr_3$0)) - (not (Btwn$0 next$0 curr_3$0 ?y ?y)) (= curr_3$0 ?y))) - :named btwn_cycl_10)) - -(assert (! (Btwn$0 next$0 null$0 (read$0 next$0 null$0) (read$0 next$0 null$0)) - :named btwn_step_8)) - -(assert (! (Btwn$0 next$0 tmp_2$0 (read$0 next$0 tmp_2$0) (read$0 next$0 tmp_2$0)) - :named btwn_step_9)) - -(assert (! (Btwn$0 next$0 curr_3$0 (read$0 next$0 curr_3$0) (read$0 next$0 curr_3$0)) - :named btwn_step_10)) - -(assert (! (forall ((?f FldLoc)) - (or (member (ep$0 ?f sk_?X_30$0 null$0) sk_?X_30$0) - (= null$0 (ep$0 ?f sk_?X_30$0 null$0)))) - :named entry-point3_10)) - -(assert (! (forall ((?f FldLoc)) - (or (member (ep$0 ?f sk_?X_30$0 lst_1$0) sk_?X_30$0) - (= lst_1$0 (ep$0 ?f sk_?X_30$0 lst_1$0)))) - :named entry-point3_11)) - -(assert (! (forall ((?f FldLoc)) - (or (member (ep$0 ?f sk_?X_30$0 curr_3$0) sk_?X_30$0) - (= curr_3$0 (ep$0 ?f sk_?X_30$0 curr_3$0)))) - :named entry-point3_12)) - -(assert (! (forall ((?f FldLoc)) - (or (member (ep$0 ?f sk_?X_30$0 tmp_2$0) sk_?X_30$0) - (= tmp_2$0 (ep$0 ?f sk_?X_30$0 tmp_2$0)))) - :named entry-point3_13)) - -(assert (! (forall ((?f FldLoc)) - (Btwn$0 ?f null$0 (ep$0 ?f sk_?X_30$0 null$0) - (ep$0 ?f sk_?X_30$0 null$0))) - :named entry-point1_10)) - -(assert (! (forall ((?f FldLoc)) - (Btwn$0 ?f lst_1$0 (ep$0 ?f sk_?X_30$0 lst_1$0) - (ep$0 ?f sk_?X_30$0 lst_1$0))) - :named entry-point1_11)) - -(assert (! (forall ((?f FldLoc)) - (Btwn$0 ?f curr_3$0 (ep$0 ?f sk_?X_30$0 curr_3$0) - (ep$0 ?f sk_?X_30$0 curr_3$0))) - :named entry-point1_12)) - -(assert (! (forall ((?f FldLoc)) - (Btwn$0 ?f tmp_2$0 (ep$0 ?f sk_?X_30$0 tmp_2$0) - (ep$0 ?f sk_?X_30$0 tmp_2$0))) - :named entry-point1_13)) - -(assert (! (forall ((?f FldLoc) (?y Loc)) - (or (Btwn$0 ?f null$0 (ep$0 ?f sk_?X_30$0 null$0) ?y) - (not (Btwn$0 ?f null$0 ?y ?y)) (not (member ?y sk_?X_30$0)))) - :named entry-point4_10)) - -(assert (! (forall ((?f FldLoc) (?y Loc)) - (or (Btwn$0 ?f lst_1$0 (ep$0 ?f sk_?X_30$0 lst_1$0) ?y) - (not (Btwn$0 ?f lst_1$0 ?y ?y)) (not (member ?y sk_?X_30$0)))) - :named entry-point4_11)) - -(assert (! (forall ((?f FldLoc) (?y Loc)) - (or (Btwn$0 ?f curr_3$0 (ep$0 ?f sk_?X_30$0 curr_3$0) ?y) - (not (Btwn$0 ?f curr_3$0 ?y ?y)) (not (member ?y sk_?X_30$0)))) - :named entry-point4_12)) - -(assert (! (forall ((?f FldLoc) (?y Loc)) - (or (Btwn$0 ?f tmp_2$0 (ep$0 ?f sk_?X_30$0 tmp_2$0) ?y) - (not (Btwn$0 ?f tmp_2$0 ?y ?y)) (not (member ?y sk_?X_30$0)))) - :named entry-point4_13)) - -(assert (! (forall ((?f FldLoc) (?y Loc)) - (or (not (Btwn$0 ?f null$0 ?y ?y)) (not (member ?y sk_?X_30$0)) - (member (ep$0 ?f sk_?X_30$0 null$0) sk_?X_30$0))) - :named entry-point2_10)) - -(assert (! (forall ((?f FldLoc) (?y Loc)) - (or (not (Btwn$0 ?f lst_1$0 ?y ?y)) (not (member ?y sk_?X_30$0)) - (member (ep$0 ?f sk_?X_30$0 lst_1$0) sk_?X_30$0))) - :named entry-point2_11)) - -(assert (! (forall ((?f FldLoc) (?y Loc)) - (or (not (Btwn$0 ?f curr_3$0 ?y ?y)) (not (member ?y sk_?X_30$0)) - (member (ep$0 ?f sk_?X_30$0 curr_3$0) sk_?X_30$0))) - :named entry-point2_12)) - -(assert (! (forall ((?f FldLoc) (?y Loc)) - (or (not (Btwn$0 ?f tmp_2$0 ?y ?y)) (not (member ?y sk_?X_30$0)) - (member (ep$0 ?f sk_?X_30$0 tmp_2$0) sk_?X_30$0))) - :named entry-point2_13)) - -(assert (! (= (read$0 (write$0 next$0 curr_3$0 (read$0 next$0 tmp_2$0)) curr_3$0) - (read$0 next$0 tmp_2$0)) - :named read_write2)) - -(assert (! (or (= null$0 curr_3$0) - (= (read$0 next$0 null$0) - (read$0 (write$0 next$0 curr_3$0 (read$0 next$0 tmp_2$0)) null$0))) - :named read_write1)) - -(assert (! (or (= tmp_2$0 curr_3$0) - (= (read$0 next$0 tmp_2$0) - (read$0 (write$0 next$0 curr_3$0 (read$0 next$0 tmp_2$0)) tmp_2$0))) - :named read_write1_1)) - -(assert (! (or (= curr_3$0 curr_3$0) - (= (read$0 next$0 curr_3$0) - (read$0 (write$0 next$0 curr_3$0 (read$0 next$0 tmp_2$0)) curr_3$0))) - :named read_write1_2)) - -(assert (! (= (read$0 next$0 null$0) null$0) :named read_null_5)) - -(assert (! (= (read$0 next_1$0 null$0) null$0) :named read_null_6)) - -(assert (! (forall ((l1 Loc)) - (or - (and (Btwn$0 next$0 lst$0 l1 curr_2$0) - (member l1 (lseg_domain$0 next$0 lst$0 curr_2$0)) - (not (= l1 curr_2$0))) - (and - (or (= l1 curr_2$0) - (not (Btwn$0 next$0 lst$0 l1 curr_2$0))) - (not (member l1 (lseg_domain$0 next$0 lst$0 curr_2$0)))))) - :named lseg_footprint_20)) - -(assert (! (forall ((l1 Loc)) - (or - (and (Btwn$0 next$0 curr_3$0 l1 null$0) - (member l1 (lseg_domain$0 next$0 curr_3$0 null$0)) - (not (= l1 null$0))) - (and - (or (= l1 null$0) - (not (Btwn$0 next$0 curr_3$0 l1 null$0))) - (not (member l1 (lseg_domain$0 next$0 curr_3$0 null$0)))))) - :named lseg_footprint_21)) - -(assert (! (not (member tmp_2$0 FP_2$0)) :named check_free_31_6)) - -(assert (! (not (member null$0 Alloc$0)) :named framecondition_of_remove_loop_18_4_15)) - -(assert (! (not (= lst$0 null$0)) :named if_else_13_6_4)) - -(assert (! (= FP_Caller$0 (union FP$0 FP_Caller$0)) - :named precondition_of_remove_10_11_20)) - -(assert (! (= sk_?X_33$0 FP$0) :named precondition_of_remove_10_11_21)) - -(assert (! (lseg_struct$0 sk_?X_32$0 next$0 lst$0 curr_2$0) :named invariant_18_4_62)) - -(assert (! (= FP$0 (union FP_1$0 FP$0)) :named invariant_18_4_63)) - -(assert (! (= sk_?X_31$0 (lseg_domain$0 next$0 curr_2$0 null$0)) - :named invariant_18_4_64)) - -(assert (! (= sk_?X_30$0 (union sk_?X_31$0 sk_?X_32$0)) :named invariant_18_4_65)) - -(assert (! (= (as emptyset SetLoc) (as emptyset SetLoc)) :named invariant_18_4_66)) - -(assert (! (lseg_struct$0 sk_?X_28$0 next$0 curr_3$0 null$0) - :named invariant_18_4_67)) - -(assert (! (= sk_?X_29$0 (union sk_?X_28$0 sk_?X_27$0)) :named invariant_18_4_68)) - -(assert (! (= sk_?X_28$0 (lseg_domain$0 next$0 curr_3$0 null$0)) - :named invariant_18_4_69)) - -(assert (! (= (as emptyset SetLoc) (intersection sk_?X_27$0 sk_?X_28$0)) - :named invariant_18_4_70)) - -(assert (! (= Alloc$0 (union FP_Caller$0 Alloc$0)) - :named initial_footprint_of_remove_10_11_10)) - -(assert (! (Frame$0 FP_1$0 Alloc$0 next$0 next$0) - :named framecondition_of_remove_loop_18_4_16)) - -(assert (! (= next_1$0 (write$0 next$0 curr_3$0 (read$0 next$0 tmp_2$0))) - :named assign_30_6)) - -(assert (! (= curr_2$0 lst$0) :named assign_17_4_4)) - -(assert (! (= FP_2$0 - (union (setminus FP$0 FP_1$0) - (union (intersection Alloc$0 FP_1$0) (setminus Alloc$0 Alloc$0)))) - :named framecondition_of_remove_loop_18_4_17)) - -(assert (! (or (Btwn$0 next$0 lst$0 curr_2$0 curr_2$0) - (not (lseg_struct$0 sk_?X_32$0 next$0 lst$0 curr_2$0))) - :named unnamed_23)) - -(assert (! (or (Btwn$0 next$0 curr_3$0 null$0 null$0) - (not (lseg_struct$0 sk_?X_28$0 next$0 curr_3$0 null$0))) - :named unnamed_24)) - -(assert (! (or (= (read$0 next$0 curr_3$0) null$0) (not nondet_2$0)) - :named unnamed_25)) - -(assert (! (forall ((l1 Loc)) - (or - (and (Btwn$0 next$0 lst_1$0 l1 curr_3$0) - (member l1 (lseg_domain$0 next$0 lst_1$0 curr_3$0)) - (not (= l1 curr_3$0))) - (and - (or (= l1 curr_3$0) - (not (Btwn$0 next$0 lst_1$0 l1 curr_3$0))) - (not (member l1 (lseg_domain$0 next$0 lst_1$0 curr_3$0)))))) - :named lseg_footprint_22)) - -(assert (! (forall ((l1 Loc)) - (or - (and (Btwn$0 next$0 lst$0 l1 null$0) - (member l1 (lseg_domain$0 next$0 lst$0 null$0)) - (not (= l1 null$0))) - (and (or (= l1 null$0) (not (Btwn$0 next$0 lst$0 l1 null$0))) - (not (member l1 (lseg_domain$0 next$0 lst$0 null$0)))))) - :named lseg_footprint_23)) - -(assert (! (forall ((l1 Loc)) - (or - (and (Btwn$0 next$0 curr_2$0 l1 null$0) - (member l1 (lseg_domain$0 next$0 curr_2$0 null$0)) - (not (= l1 null$0))) - (and - (or (= l1 null$0) - (not (Btwn$0 next$0 curr_2$0 l1 null$0))) - (not (member l1 (lseg_domain$0 next$0 curr_2$0 null$0)))))) - :named lseg_footprint_24)) - -(assert (! (not (member null$0 Alloc$0)) :named initial_footprint_of_remove_10_11_11)) - -(assert (! (not (= tmp_2$0 null$0)) :named if_else_28_8_2)) - -(assert (! (lseg_struct$0 sk_?X_33$0 next$0 lst$0 null$0) - :named precondition_of_remove_10_11_22)) - -(assert (! (= sk_?X_33$0 (lseg_domain$0 next$0 lst$0 null$0)) - :named precondition_of_remove_10_11_23)) - -(assert (! (not (= curr_2$0 null$0)) :named invariant_18_4_71)) - -(assert (! (lseg_struct$0 sk_?X_31$0 next$0 curr_2$0 null$0) - :named invariant_18_4_72)) - -(assert (! (= sk_?X_32$0 (lseg_domain$0 next$0 lst$0 curr_2$0)) - :named invariant_18_4_73)) - -(assert (! (= sk_?X_30$0 FP_1$0) :named invariant_18_4_74)) - -(assert (! (= (as emptyset SetLoc) (intersection sk_?X_32$0 sk_?X_31$0)) - :named invariant_18_4_75)) - -(assert (! (not (= curr_3$0 null$0)) :named invariant_18_4_76)) - -(assert (! (lseg_struct$0 sk_?X_27$0 next$0 lst_1$0 curr_3$0) - :named invariant_18_4_77)) - -(assert (! (= sk_?X_29$0 - (union (intersection Alloc$0 FP_1$0) (setminus Alloc$0 Alloc$0))) - :named invariant_18_4_78)) - -(assert (! (= sk_?X_27$0 (lseg_domain$0 next$0 lst_1$0 curr_3$0)) - :named invariant_18_4_79)) - -(assert (! (= (as emptyset SetLoc) (as emptyset SetLoc)) :named invariant_18_4_80)) - -(assert (! (= Alloc$0 (union FP_2$0 Alloc$0)) - :named framecondition_of_remove_loop_18_4_18)) - -(assert (! (= tmp_2$0 (read$0 next$0 curr_3$0)) :named assign_27_4_2)) - -(assert (! (= lst_1$0 lst$0) :named framecondition_of_remove_loop_18_4_19)) - -(assert (! (= FP_Caller_1$0 (setminus FP_Caller$0 FP$0)) :named assign_13_2_5)) - -(assert (! (or (Btwn$0 next$0 lst_1$0 curr_3$0 curr_3$0) - (not (lseg_struct$0 sk_?X_27$0 next$0 lst_1$0 curr_3$0))) - :named unnamed_26)) - -(assert (! (or (Btwn$0 next$0 lst$0 null$0 null$0) - (not (lseg_struct$0 sk_?X_33$0 next$0 lst$0 null$0))) - :named unnamed_27)) - -(assert (! (or (Btwn$0 next$0 curr_2$0 null$0 null$0) - (not (lseg_struct$0 sk_?X_31$0 next$0 curr_2$0 null$0))) - :named unnamed_28)) - -(assert (! (forall ((?u Loc) (?v Loc) (?z Loc)) - (and - (or - (Btwn$0 (write$0 next$0 curr_3$0 (read$0 next$0 tmp_2$0)) - ?z ?u ?v) - (not - (or - (and (Btwn$0 next$0 ?z ?u ?v) - (or (Btwn$0 next$0 ?z ?v curr_3$0) - (and (Btwn$0 next$0 ?z ?v ?v) - (not - (Btwn$0 next$0 ?z curr_3$0 - curr_3$0))))) - (and (not (= curr_3$0 ?v)) - (or (Btwn$0 next$0 ?z curr_3$0 ?v) - (and - (Btwn$0 next$0 ?z curr_3$0 - curr_3$0) - (not (Btwn$0 next$0 ?z ?v ?v)))) - (Btwn$0 next$0 ?z ?u curr_3$0) - (or - (Btwn$0 next$0 (read$0 next$0 tmp_2$0) - ?v curr_3$0) - (and - (Btwn$0 next$0 - (read$0 next$0 tmp_2$0) ?v ?v) - (not - (Btwn$0 next$0 - (read$0 next$0 tmp_2$0) - curr_3$0 curr_3$0))))) - (and (not (= curr_3$0 ?v)) - (or (Btwn$0 next$0 ?z curr_3$0 ?v) - (and - (Btwn$0 next$0 ?z curr_3$0 - curr_3$0) - (not (Btwn$0 next$0 ?z ?v ?v)))) - (Btwn$0 next$0 (read$0 next$0 tmp_2$0) ?u - ?v) - (or - (Btwn$0 next$0 (read$0 next$0 tmp_2$0) - ?v curr_3$0) - (and - (Btwn$0 next$0 - (read$0 next$0 tmp_2$0) ?v ?v) - (not - (Btwn$0 next$0 - (read$0 next$0 tmp_2$0) - curr_3$0 curr_3$0)))))))) - (or - (and (Btwn$0 next$0 ?z ?u ?v) - (or (Btwn$0 next$0 ?z ?v curr_3$0) - (and (Btwn$0 next$0 ?z ?v ?v) - (not (Btwn$0 next$0 ?z curr_3$0 curr_3$0))))) - (and (not (= curr_3$0 ?v)) - (or (Btwn$0 next$0 ?z curr_3$0 ?v) - (and (Btwn$0 next$0 ?z curr_3$0 curr_3$0) - (not (Btwn$0 next$0 ?z ?v ?v)))) - (Btwn$0 next$0 ?z ?u curr_3$0) - (or - (Btwn$0 next$0 (read$0 next$0 tmp_2$0) ?v - curr_3$0) - (and - (Btwn$0 next$0 (read$0 next$0 tmp_2$0) ?v - ?v) - (not - (Btwn$0 next$0 (read$0 next$0 tmp_2$0) - curr_3$0 curr_3$0))))) - (and (not (= curr_3$0 ?v)) - (or (Btwn$0 next$0 ?z curr_3$0 ?v) - (and (Btwn$0 next$0 ?z curr_3$0 curr_3$0) - (not (Btwn$0 next$0 ?z ?v ?v)))) - (Btwn$0 next$0 (read$0 next$0 tmp_2$0) ?u ?v) - (or - (Btwn$0 next$0 (read$0 next$0 tmp_2$0) ?v - curr_3$0) - (and - (Btwn$0 next$0 (read$0 next$0 tmp_2$0) ?v - ?v) - (not - (Btwn$0 next$0 (read$0 next$0 tmp_2$0) - curr_3$0 curr_3$0))))) - (not - (Btwn$0 - (write$0 next$0 curr_3$0 (read$0 next$0 tmp_2$0)) - ?z ?u ?v))))) - :named btwn_write)) - -(assert (! (forall ((?x Loc)) (Btwn$0 next$0 ?x ?x ?x)) :named btwn_refl_5)) - -(assert (! (forall ((?x Loc) (?y Loc)) (or (not (Btwn$0 next$0 ?x ?y ?x)) (= ?x ?y))) - :named btwn_sndw_5)) - -(assert (! (forall ((?x Loc) (?y Loc) (?z Loc)) - (or (not (Btwn$0 next$0 ?x ?y ?y)) (not (Btwn$0 next$0 ?x ?z ?z)) - (Btwn$0 next$0 ?x ?y ?z) (Btwn$0 next$0 ?x ?z ?y))) - :named btwn_ord1_5)) - -(assert (! (forall ((?x Loc) (?y Loc) (?z Loc)) - (or (not (Btwn$0 next$0 ?x ?y ?z)) - (and (Btwn$0 next$0 ?x ?y ?y) (Btwn$0 next$0 ?y ?z ?z)))) - :named btwn_ord2_5)) - -(assert (! (forall ((?x Loc) (?y Loc) (?z Loc)) - (or (not (Btwn$0 next$0 ?x ?y ?y)) (not (Btwn$0 next$0 ?y ?z ?z)) - (Btwn$0 next$0 ?x ?z ?z))) - :named btwn_trn1_5)) - -(assert (! (forall ((?u Loc) (?x Loc) (?y Loc) (?z Loc)) - (or (not (Btwn$0 next$0 ?x ?y ?z)) (not (Btwn$0 next$0 ?y ?u ?z)) - (and (Btwn$0 next$0 ?x ?y ?u) (Btwn$0 next$0 ?x ?u ?z)))) - :named btwn_trn2_5)) - -(assert (! (forall ((?u Loc) (?x Loc) (?y Loc) (?z Loc)) - (or (not (Btwn$0 next$0 ?x ?y ?z)) (not (Btwn$0 next$0 ?x ?u ?y)) - (and (Btwn$0 next$0 ?x ?u ?z) (Btwn$0 next$0 ?u ?y ?z)))) - :named btwn_trn3_5)) - -(check-sat) -(exit) diff --git a/test/regress/regress0/sets/jan27/ListElem.hs.fqout.cvc4.38.smt2 b/test/regress/regress0/sets/jan27/ListElem.hs.fqout.cvc4.38.smt2 deleted file mode 100644 index 3c0ef1dda..000000000 --- a/test/regress/regress0/sets/jan27/ListElem.hs.fqout.cvc4.38.smt2 +++ /dev/null @@ -1,59 +0,0 @@ -(set-logic QF_ALL_SUPPORTED) -(set-info :status unsat) - -; What was the bug? -; -; When asserting equality to equality engine, correct reason -; was not being sent (the fact itself was being sent as reason) - -(define-sort Elt () Int) -(define-sort mySet () (Set Elt )) -(define-fun smt_set_emp () mySet (as emptyset mySet)) -(define-fun smt_set_mem ((x Elt) (s mySet)) Bool (member x s)) -(define-fun smt_set_add ((s mySet) (x Elt)) mySet (union s (singleton x))) -(define-fun smt_set_cup ((s1 mySet) (s2 mySet)) mySet (union s1 s2)) -(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (intersection s1 s2)) -;(define-fun smt_set_com ((s mySet)) mySet ((_ map not) s)) -(define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (setminus s1 s2)) -;(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (= smt_set_emp (smt_set_dif s1 s2))) -(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subset s1 s2)) -(declare-fun z3v56 () Int) -(declare-fun z3v57 () Int) -(assert (distinct z3v56 z3v57)) -(declare-fun z3v58 () Int) -(declare-fun z3f59 (Int) Int) -(declare-fun z3v60 () Int) -(declare-fun z3f61 (Int) Bool) -(declare-fun z3v62 () Int) -(declare-fun z3v63 () Int) -(declare-fun z3v64 () Int) -(declare-fun z3v65 () Int) -(declare-fun z3f66 (Int) mySet) -(declare-fun z3f67 (Int) Bool) -(declare-fun z3f68 (Int Int) Int) -(declare-fun z3v69 () Int) -(declare-fun z3v70 () Int) -(declare-fun z3f71 (Int) Int) -(declare-fun z3v72 () Int) -(declare-fun z3v73 () Int) -(declare-fun z3v74 () Int) -(declare-fun z3v75 () Int) -(declare-fun z3v76 () Int) -(declare-fun z3v77 () Int) -(declare-fun z3v78 () Int) -(declare-fun z3v80 () Int) -(declare-fun z3v81 () Int) -(declare-fun z3f82 () Int) -(declare-fun z3v83 () Int) -(declare-fun z3v84 () Int) -(declare-fun z3v85 () Int) -(declare-fun z3v86 () Int) -(declare-fun z3v87 () Int) -(declare-fun z3v88 () Int) -(declare-fun z3v89 () Int) -(declare-fun z3v90 () Int) -(assert (= z3v90 z3v56)) -(assert (z3f61 z3v90)) -(assert (and (>= (z3f59 z3v58) 0) (z3f61 z3v60) (z3f61 z3v60) (= z3v60 z3v62) (= (z3f61 z3v60) (= z3v64 z3v63)) (= (z3f61 z3v62) (= z3v64 z3v63)) (>= (z3f59 z3v65) 0) (= (z3f66 z3v65) (smt_set_cup (smt_set_add smt_set_emp z3v64) (z3f66 z3v58))) (= (z3f59 z3v65) (+ 1 (z3f59 z3v58))) (= (z3f67 z3v65) false) (= z3v65 (z3f68 z3v64 z3v58)) (>= (z3f59 z3v65) 0) (= z3v65 z3v69) (>= (z3f59 z3v65) 0) (>= (z3f59 z3v69) 0) (z3f61 z3v56) (= (z3f71 z3v70) z3v70) (= (z3f71 z3v72) z3v72) (not (z3f61 z3v57)) (= (z3f71 z3v73) z3v73))) -(assert (not (= (z3f61 z3v90) (smt_set_mem z3v63 (z3f66 z3v69))))) -(check-sat) diff --git a/test/regress/regress0/sets/jan27/deepmeas0.hs.fqout.cvc4.41.smt2 b/test/regress/regress0/sets/jan27/deepmeas0.hs.fqout.cvc4.41.smt2 deleted file mode 100644 index 83dfe41e5..000000000 --- a/test/regress/regress0/sets/jan27/deepmeas0.hs.fqout.cvc4.41.smt2 +++ /dev/null @@ -1,58 +0,0 @@ -; EXPECT: sat -(set-logic QF_ALL_SUPPORTED) -(set-info :status sat) -(define-sort Elt () Int) -(define-sort mySet () (Set Elt )) -(define-fun smt_set_emp () mySet (as emptyset mySet)) -(define-fun smt_set_mem ((x Elt) (s mySet)) Bool (member x s)) -(define-fun smt_set_add ((s mySet) (x Elt)) mySet (union s (singleton x))) -(define-fun smt_set_cup ((s1 mySet) (s2 mySet)) mySet (union s1 s2)) -(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (intersection s1 s2)) -;(define-fun smt_set_com ((s mySet)) mySet ((_ map not) s)) -(define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (setminus s1 s2)) -;(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (= smt_set_emp (smt_set_dif s1 s2))) -(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subset s1 s2)) -(declare-fun z3v58 () Int) -(declare-fun z3v59 () Int) -(assert (distinct z3v58 z3v59)) -(declare-fun z3f60 (Int) Bool) -(declare-fun z3v61 () Int) -(declare-fun z3f62 (Int) Int) -(declare-fun z3v63 () Int) -(declare-fun z3v64 () Int) -(declare-fun z3v65 () Int) -(declare-fun z3v66 () Int) -(declare-fun z3f67 (Int) mySet) -(declare-fun z3v69 () Int) -(declare-fun z3f70 (Int) Int) -(declare-fun z3v76 () Int) -(declare-fun z3v77 () Int) -(declare-fun z3v78 () Int) -(declare-fun z3v79 () Int) -(declare-fun z3v80 () Int) -(declare-fun z3v81 () Int) -(declare-fun z3v82 () Int) -(declare-fun z3f83 (Int) Int) -(declare-fun z3f84 (Int) Int) -(declare-fun z3v85 () Int) -(declare-fun z3f86 (Int) Int) -(declare-fun z3f87 (Int Int) Int) -(declare-fun z3v88 () Int) -(declare-fun z3v89 () Int) -(declare-fun z3f90 (Int) mySet) -(declare-fun z3f91 (Int) Bool) -(declare-fun z3f92 (Int Int) Int) -(declare-fun z3v93 () Int) -(declare-fun z3v94 () Int) -(declare-fun z3v95 () Int) -(declare-fun z3v96 () Int) -(declare-fun z3v97 () Int) -(assert (and (not (z3f60 z3v79)) (not (z3f60 z3v79)) (= z3v79 z3v80) (= (z3f60 z3v79) (= z3v76 z3v81)) (= (z3f60 z3v80) (= z3v76 z3v81)) (= (z3f83 z3v82) z3v81) (= (z3f84 z3v82) z3v81) (= (z3f86 z3v82) z3v85) (= z3v82 (z3f87 z3v81 z3v85)) (= z3v82 z3v88) (>= (z3f70 z3v78) 0) (= (z3f67 z3v78) (smt_set_cup (smt_set_add smt_set_emp (z3f83 z3v88)) (z3f67 z3v89))) (= (z3f90 z3v78) (smt_set_cup (smt_set_add smt_set_emp z3v88) (z3f90 z3v89))) (= (z3f70 z3v78) (+ 1 (z3f70 z3v89))) (= (z3f91 z3v78) false) (= z3v78 (z3f92 z3v88 z3v89)) (>= (z3f70 z3v78) 0) (= z3v78 z3v77) (>= (z3f70 z3v78) 0) (>= (z3f70 z3v89) 0) (>= (z3f70 z3v77) 0) (>= (z3f70 z3v97) 0) (= z3v97 z3v89) (>= (z3f70 z3v97) 0) (z3f60 z3v58) (= (z3f62 z3v61) z3v61) (= (z3f62 z3v63) z3v63) (not (z3f60 z3v59)) (= (z3f62 z3v64) z3v64))) -(assert (smt_set_mem z3v76 (z3f67 z3v78))) -(assert (<= z3v95 z3v93)) -(assert (>= z3v95 z3v93)) -(assert (= z3v95 z3v93)) -(assert (smt_set_mem z3v76 (z3f67 z3v77))) -(declare-fun z3v98 () Int) -(assert (not (< z3v98 z3v85))) -(check-sat) diff --git a/test/regress/regress0/sets/jan28/TalkingAboutSets.hs.fqout.cvc4.3577.smt2 b/test/regress/regress0/sets/jan28/TalkingAboutSets.hs.fqout.cvc4.3577.smt2 deleted file mode 100644 index 282325f14..000000000 --- a/test/regress/regress0/sets/jan28/TalkingAboutSets.hs.fqout.cvc4.3577.smt2 +++ /dev/null @@ -1,286 +0,0 @@ -; EXPECT: sat -(set-logic QF_ALL_SUPPORTED) -(set-info :status sat) -(define-sort Elt () Int) -(define-sort mySet () (Set Elt )) -(define-fun smt_set_emp () mySet (as emptyset mySet)) -(define-fun smt_set_mem ((x Elt) (s mySet)) Bool (member x s)) -(define-fun smt_set_add ((s mySet) (x Elt)) mySet (union s (singleton x))) -(define-fun smt_set_cup ((s1 mySet) (s2 mySet)) mySet (union s1 s2)) -(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (intersection s1 s2)) -;(define-fun smt_set_com ((s mySet)) mySet ((_ map not) s)) -(define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (setminus s1 s2)) -;(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (= smt_set_emp (smt_set_dif s1 s2))) -(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subset s1 s2)) -(declare-fun z3v60 () Int) -(declare-fun z3v61 () Int) -(assert (distinct z3v60 z3v61)) -(declare-fun z3f62 (Int) Bool) -(declare-fun z3v63 () Int) -(declare-fun z3f64 (Int) Int) -(declare-fun z3v65 () Int) -(declare-fun z3v66 () Int) -(declare-fun z3v69 () mySet) -(declare-fun z3v70 () mySet) -(declare-fun z3v72 () mySet) -(declare-fun z3v73 () mySet) -(declare-fun z3v75 () Int) -(declare-fun z3f76 (Int) Int) -(declare-fun z3v79 () Int) -(declare-fun z3v80 () Int) -(declare-fun z3v84 () Int) -(declare-fun z3v87 () mySet) -(declare-fun z3v88 () mySet) -(declare-fun z3v90 () mySet) -(declare-fun z3v91 () mySet) -(declare-fun z3v93 () mySet) -(declare-fun z3v94 () mySet) -(declare-fun z3v96 () Int) -(declare-fun z3f97 (Int) mySet) -(declare-fun z3f98 (Int) Bool) -(declare-fun z3v99 () Int) -(declare-fun z3v102 () Int) -(declare-fun z3v105 () mySet) -(declare-fun z3v107 () mySet) -(declare-fun z3v108 () mySet) -(declare-fun z3v109 () Int) -(declare-fun z3v110 () Int) -(declare-fun z3v111 () Int) -(declare-fun z3v112 () Int) -(declare-fun z3v113 () mySet) -(declare-fun z3v114 () mySet) -(declare-fun z3v117 () mySet) -(declare-fun z3v118 () mySet) -(declare-fun z3v121 () mySet) -(declare-fun z3v123 () mySet) -(declare-fun z3v124 () mySet) -(declare-fun z3v126 () mySet) -(declare-fun z3v128 () Int) -(declare-fun z3v132 () Int) -(declare-fun z3v135 () mySet) -(declare-fun z3v136 () mySet) -(declare-fun z3v138 () mySet) -(declare-fun z3v140 () Int) -(declare-fun z3v143 () mySet) -(declare-fun z3v144 () mySet) -(declare-fun z3v145 () mySet) -(declare-fun z3v146 () Int) -(declare-fun z3v147 () Int) -(declare-fun z3v148 () mySet) -(declare-fun z3v149 () mySet) -(declare-fun z3v155 () mySet) -(declare-fun z3v156 () mySet) -(declare-fun z3v157 () mySet) -(declare-fun z3v160 () Int) -(declare-fun z3v161 () Int) -(declare-fun z3v162 () Int) -(declare-fun z3v163 () Int) -(declare-fun z3v164 () mySet) -(declare-fun z3v165 () mySet) -(declare-fun z3v169 () Int) -(declare-fun z3v172 () mySet) -(declare-fun z3v173 () mySet) -(declare-fun z3v175 () Int) -(declare-fun z3v176 () Int) -(declare-fun z3v177 () Int) -(declare-fun z3v178 () Int) -(declare-fun z3f179 (Int Int) Int) -(declare-fun z3v180 () Int) -(declare-fun z3v181 () Int) -(declare-fun z3f183 () Int) -(declare-fun z3v184 () Int) -(declare-fun z3v185 () Int) -(declare-fun z3v186 () Int) -(declare-fun z3v187 () Int) -(declare-fun z3v188 () Int) -(declare-fun z3v189 () Int) -(declare-fun z3v192 () Int) -(declare-fun z3v193 () Int) -(declare-fun z3v197 () Int) -(declare-fun z3v198 () mySet) -(declare-fun z3v200 () Int) -(declare-fun z3v201 () Int) -(declare-fun z3v202 () Int) -(declare-fun z3v203 () Int) -(declare-fun z3v204 () Int) -(declare-fun z3v206 () Int) -(declare-fun z3v207 () Int) -(declare-fun z3v208 () Int) -(declare-fun z3v209 () Int) -(declare-fun z3v210 () Int) -(declare-fun z3v211 () Int) -(declare-fun z3f212 (Int) Int) -(declare-fun z3f213 (Int) Int) -(declare-fun z3v214 () Int) -(declare-fun z3v215 () Int) -(declare-fun z3v217 () Int) -(declare-fun z3v218 () Int) -(declare-fun z3v219 () Int) -(declare-fun z3v220 () Int) -(declare-fun z3f221 (Int Int) Int) -(declare-fun z3v222 () Int) -(declare-fun z3v223 () Int) -(declare-fun z3v224 () Int) -(declare-fun z3v225 () Int) -(declare-fun z3v226 () Int) -(declare-fun z3v227 () Int) -(declare-fun z3v228 () Int) -(declare-fun z3v229 () Int) -(declare-fun z3v230 () Int) -(declare-fun z3v231 () Int) -(declare-fun z3v232 () Int) -(declare-fun z3v233 () Int) -(declare-fun z3v234 () Int) -(declare-fun z3v235 () Int) -(declare-fun z3v236 () Int) -(declare-fun z3v237 () Int) -(declare-fun z3v238 () Int) -(declare-fun z3v239 () Int) -(declare-fun z3v240 () Int) -(declare-fun z3v241 () Int) -(declare-fun z3v242 () Int) -(declare-fun z3v243 () Int) -(declare-fun z3v244 () Int) -(declare-fun z3v245 () Int) -(declare-fun z3v246 () Int) -(declare-fun z3v247 () Int) -(declare-fun z3v248 () Int) -(declare-fun z3v249 () Int) -(declare-fun z3v250 () Int) -(declare-fun z3v251 () Int) -(declare-fun z3v252 () Int) -(declare-fun z3v253 () Int) -(declare-fun z3v254 () Int) -(declare-fun z3v255 () Int) -(declare-fun z3v256 () Int) -(declare-fun z3v257 () Int) -(declare-fun z3v258 () Int) -(declare-fun z3v259 () Int) -(declare-fun z3v260 () Int) -(declare-fun z3v261 () Int) -(declare-fun z3v262 () Int) -(declare-fun z3v263 () Int) -(declare-fun z3v264 () Int) -(declare-fun z3v265 () Int) -(declare-fun z3v266 () Int) -(declare-fun z3v267 () Int) -(declare-fun z3v268 () Int) -(declare-fun z3v269 () Int) -(declare-fun z3v271 () Int) -(declare-fun z3v273 () Int) -(declare-fun z3v275 () Int) -(declare-fun z3v277 () Int) -(declare-fun z3v279 () Int) -(declare-fun z3v281 () Int) -(declare-fun z3v283 () Int) -(declare-fun z3v286 () Int) -(declare-fun z3v289 () Int) -(declare-fun z3v290 () Int) -(declare-fun z3v291 () Int) -(declare-fun z3v292 () mySet) -(declare-fun z3v295 () mySet) -(declare-fun z3v297 () Int) -(declare-fun z3v301 () Int) -(declare-fun z3v302 () Int) -(declare-fun z3v303 () Int) -(declare-fun z3v304 () Int) -(declare-fun z3v305 () Int) -(declare-fun z3v306 () Int) -(declare-fun z3v307 () Int) -(declare-fun z3v308 () Int) -(declare-fun z3v309 () Int) -(declare-fun z3v310 () Int) -(declare-fun z3v312 () Int) -(declare-fun z3v314 () Int) -(declare-fun z3v315 () Int) -(declare-fun z3v316 () Int) -(declare-fun z3v317 () Int) -(declare-fun z3v318 () Int) -(declare-fun z3v319 () Int) -(declare-fun z3v320 () Int) -(declare-fun z3v321 () Int) -(declare-fun z3v322 () Int) -(declare-fun z3v324 () Int) -(declare-fun z3v327 () Int) -(declare-fun z3v328 () Int) -(declare-fun z3v329 () Int) -(declare-fun z3v330 () Int) -(declare-fun z3v331 () Int) -(declare-fun z3v332 () Int) -(declare-fun z3v333 () Int) -(declare-fun z3v334 () Int) -(declare-fun z3v335 () Int) -(declare-fun z3v336 () Int) -(declare-fun z3v337 () Int) -(declare-fun z3v338 () Int) -(declare-fun z3v339 () Int) -(declare-fun z3v340 () Int) -(declare-fun z3v341 () Int) -(declare-fun z3v342 () Int) -(declare-fun z3v343 () Int) -(declare-fun z3v345 () Int) -(declare-fun z3v349 () Int) -(declare-fun z3v350 () Int) -(declare-fun z3v351 () Int) -(declare-fun z3v352 () Int) -(declare-fun z3v353 () Int) -(declare-fun z3v354 () Int) -(declare-fun z3v355 () Int) -(declare-fun z3v359 () Int) -(declare-fun z3v361 () Int) -(declare-fun z3v362 () Int) -(declare-fun z3v363 () Int) -(declare-fun z3v364 () Int) -(declare-fun z3v366 () Int) -(declare-fun z3v367 () Int) -(declare-fun z3v368 () Int) -(declare-fun z3v369 () Int) -(declare-fun z3v370 () Int) -(declare-fun z3v375 () Int) -(assert (= (z3f97 z3v328) (smt_set_cup (z3f97 z3v331) (z3f97 z3v375)))) -(assert (= (z3f97 z3v328) (smt_set_cup (z3f97 z3v330) (z3f97 z3v375)))) -(assert (= (z3f97 z3v328) (smt_set_cup (z3f97 z3v328) (z3f97 z3v375)))) -(assert (= (z3f97 z3v328) (smt_set_cup (z3f97 z3v327) (z3f97 z3v375)))) -(assert (= (z3f97 z3v331) (smt_set_cup (z3f97 z3v331) (z3f97 z3v375)))) -(assert (= (z3f97 z3v331) (smt_set_cup (z3f97 z3v330) (z3f97 z3v375)))) -(assert (= (z3f97 z3v331) (smt_set_cup (z3f97 z3v328) (z3f97 z3v375)))) -(assert (= (z3f97 z3v331) (smt_set_cup (z3f97 z3v327) (z3f97 z3v375)))) -(assert (= (z3f97 z3v375) (z3f97 z3v331))) -(assert (= (z3f97 z3v375) (z3f97 z3v328))) -(assert (= (z3f97 z3v375) (smt_set_cup (z3f97 z3v327) (z3f97 z3v331)))) -(assert (= (z3f97 z3v375) (smt_set_cup (z3f97 z3v327) (z3f97 z3v328)))) -(assert (= (z3f97 z3v375) (smt_set_cup (z3f97 z3v328) (z3f97 z3v331)))) -(assert (= (z3f97 z3v375) (smt_set_cup (z3f97 z3v328) (z3f97 z3v330)))) -(assert (= (z3f97 z3v375) (smt_set_cup (z3f97 z3v328) (z3f97 z3v328)))) -(assert (= (z3f97 z3v375) (smt_set_cup (z3f97 z3v328) (z3f97 z3v327)))) -(assert (= (z3f97 z3v375) (smt_set_cup (z3f97 z3v330) (z3f97 z3v331)))) -(assert (= (z3f97 z3v375) (smt_set_cup (z3f97 z3v330) (z3f97 z3v328)))) -(assert (= (z3f97 z3v375) (smt_set_cup (z3f97 z3v331) (z3f97 z3v331)))) -(assert (= (z3f97 z3v375) (smt_set_cup (z3f97 z3v331) (z3f97 z3v330)))) -(assert (= (z3f97 z3v375) (smt_set_cup (z3f97 z3v331) (z3f97 z3v328)))) -(assert (= (z3f97 z3v375) (smt_set_cup (z3f97 z3v331) (z3f97 z3v327)))) -(assert (smt_set_sub (z3f97 z3v375) (z3f97 z3v331))) -(assert (smt_set_sub (z3f97 z3v375) (z3f97 z3v328))) -(assert (<= z3v375 z3v331)) -(assert (<= z3v375 z3v328)) -(assert (= z3v375 z3v328)) -(assert (>= z3v375 z3v331)) -(assert (>= z3v375 z3v328)) -(assert (not (= z3v375 z3v330))) -(assert (not (= z3v375 z3v327))) -(assert (<= (z3f76 z3v375) (z3f76 z3v331))) -(assert (<= (z3f76 z3v375) (z3f76 z3v328))) -(assert (> (z3f76 z3v375) (z3f76 z3v330))) -(assert (> (z3f76 z3v375) (z3f76 z3v327))) -(assert (>= (z3f76 z3v375) (z3f76 z3v331))) -(assert (>= (z3f76 z3v375) (z3f76 z3v330))) -(assert (>= (z3f76 z3v375) (z3f76 z3v328))) -(assert (>= (z3f76 z3v375) (z3f76 z3v327))) -(assert (= (z3f76 z3v375) (z3f76 z3v331))) -(assert (= (z3f76 z3v375) (z3f76 z3v328))) -(assert (> (z3f76 z3v375) 0)) -(assert (= z3v375 z3v331)) -(assert (>= (z3f76 z3v375) 0)) -(assert (and (>= (z3f76 z3v327) 0) (>= (z3f76 z3v328) 0) (= (z3f97 z3v328) (smt_set_cup (smt_set_add smt_set_emp z3v329) (z3f97 z3v330))) (= (z3f76 z3v328) (+ 1 (z3f76 z3v330))) (= (z3f98 z3v328) false) (= z3v328 (z3f179 z3v329 z3v330)) (>= (z3f76 z3v328) 0) (= z3v328 z3v331) (>= (z3f76 z3v328) 0) (>= (z3f76 z3v330) 0) (>= (z3f76 z3v331) 0) (z3f62 z3v60) (= (z3f64 z3v63) z3v63) (= (z3f64 z3v65) z3v65) (not (z3f62 z3v61)) (= (z3f64 z3v66) z3v66))) -(assert (not (= (z3f97 z3v327) (smt_set_cup (z3f97 z3v327) (z3f97 z3v375))))) -(check-sat) diff --git a/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.cvc4.10.smt2 b/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.cvc4.10.smt2 deleted file mode 100644 index 10ed4be7c..000000000 --- a/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.cvc4.10.smt2 +++ /dev/null @@ -1,106 +0,0 @@ -(set-logic QF_ALL_SUPPORTED) -(set-info :status unsat) -(define-sort Elt () Int) -(define-sort mySet () (Set Elt )) -(define-fun smt_set_emp () mySet (as emptyset mySet)) -(define-fun smt_set_mem ((x Elt) (s mySet)) Bool (member x s)) -(define-fun smt_set_add ((s mySet) (x Elt)) mySet (union s (singleton x))) -(define-fun smt_set_cup ((s1 mySet) (s2 mySet)) mySet (union s1 s2)) -(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (intersection s1 s2)) -(define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (setminus s1 s2)) -(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subset s1 s2)) -(declare-fun z3v66 () Int) -(declare-fun z3v67 () Int) -(assert (distinct z3v66 z3v67)) -(declare-fun z3v68 () Int) -(declare-fun z3f69 (Int) Int) -(declare-fun z3f70 (Int) mySet) -(declare-fun z3v71 () Int) -(declare-fun z3f72 (Int) mySet) -(declare-fun z3v73 () Int) -(declare-fun z3v74 () Int) -(declare-fun z3v75 () Int) -(declare-fun z3f76 (Int) Bool) -(declare-fun z3f77 (Int Int) Int) -(declare-fun z3v78 () Int) -(declare-fun z3f79 (Int) Bool) -(declare-fun z3v80 () Int) -(declare-fun z3f81 (Int) Int) -(declare-fun z3v82 () Int) -(declare-fun z3v83 () Int) -(declare-fun z3v85 () Int) -(declare-fun z3v86 () Int) -(declare-fun z3v87 () Int) -(declare-fun z3f88 () Int) -(declare-fun z3v89 () Int) -(declare-fun z3v90 () Int) -(declare-fun z3v91 () Int) -(declare-fun z3v92 () Int) -(declare-fun z3v93 () Int) -(declare-fun z3f94 (Int) Int) -(declare-fun z3f95 (Int) Int) -(declare-fun z3f96 (Int Int Int) Int) -(declare-fun z3v97 () Int) -(declare-fun z3v98 () Int) -(declare-fun z3v99 () Int) -(assert (= z3v99 z3v98)) -(assert (and (>= (z3f69 z3v85) 0) - (not (smt_set_mem z3v86 (z3f70 z3v85))) - (= (z3f72 z3v85) smt_set_emp) - (>= (z3f69 z3v87) 0) - (= (z3f72 z3v87) smt_set_emp) - (= (z3f70 z3v87) smt_set_emp) - (= (z3f69 z3v87) 0) - (= (z3f76 z3v87) true) - (= z3v87 z3f88) - (>= (z3f69 z3v87) 0) - (= z3v87 z3v89) - (>= (z3f69 z3v87) 0) - (= (z3f70 z3v87) - (z3f70 z3v90)) - (= (z3f72 z3v87) smt_set_emp) - (>= (z3f69 z3v89) 0) - (= (z3f70 z3v89) - (z3f70 z3v90)) - (= (z3f72 z3v89) smt_set_emp) - (>= (z3f69 z3v90) 0) - (= (z3f72 z3v90) - (ite (smt_set_mem z3v86 (z3f70 z3v85)) - (smt_set_cup (smt_set_add smt_set_emp z3v86) - (z3f72 z3v85)) - (z3f72 z3v85))) - (= (z3f70 z3v90) - (smt_set_cup (smt_set_add smt_set_emp z3v86) - (z3f70 z3v85))) - (= (z3f69 z3v90) - (+ 1 (z3f69 z3v85))) - (= (z3f76 z3v90) false) - (>= (z3f69 z3v91) 0) - (= (z3f72 z3v91) smt_set_emp) - (= (z3f70 z3v91) smt_set_emp) - (= (z3f69 z3v91) 0) - (= (z3f76 z3v91) true) - (= z3v91 z3f88) - (>= (z3f69 z3v91) 0) - (= z3v91 z3v92) - (>= (z3f69 z3v91) 0) - (not (smt_set_mem z3v86 (z3f70 z3v91))) - (= (z3f72 z3v91) smt_set_emp) - (= (z3f94 z3v93) z3v92) - (= (z3f95 z3v93) z3v85) - (= z3v93 (z3f96 z3v86 z3v92 z3v85)) - (= z3v93 z3v97) - (= (smt_set_cap (z3f70 (z3f94 z3v93)) - (z3f70 (z3f95 z3v93))) smt_set_emp) - (>= (z3f69 z3v92) 0) - (not (smt_set_mem z3v86 (z3f70 z3v92))) - (= (z3f72 z3v92) smt_set_emp) - (= (smt_set_cap (z3f70 (z3f94 z3v97)) - (z3f70 (z3f95 z3v97))) smt_set_emp) - (z3f79 z3v66) - (= (z3f81 z3v80) z3v80) - (= (z3f81 z3v82) z3v82) - (not (z3f79 z3v67)) - (= (z3f81 z3v83) z3v83))) -(assert (not (> z3v99 z3v98))) -(check-sat) diff --git a/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.cvc4.1832.smt2 b/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.cvc4.1832.smt2 deleted file mode 100644 index 6165b98de..000000000 --- a/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.cvc4.1832.smt2 +++ /dev/null @@ -1,227 +0,0 @@ -(set-logic QF_ALL_SUPPORTED) -(set-info :status unsat) -(define-sort Elt () Int) -(define-sort mySet () (Set Elt )) -(define-fun smt_set_emp () mySet (as emptyset mySet)) -(define-fun smt_set_mem ((x Elt) (s mySet)) Bool (member x s)) -(define-fun smt_set_add ((s mySet) (x Elt)) mySet (union s (singleton x))) -(define-fun smt_set_cup ((s1 mySet) (s2 mySet)) mySet (union s1 s2)) -(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (intersection s1 s2)) -;(define-fun smt_set_com ((s mySet)) mySet ((_ map not) s)) -(define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (setminus s1 s2)) -;(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (= smt_set_emp (smt_set_dif s1 s2))) -(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subset s1 s2)) -(declare-fun z3v66 () Int) -(declare-fun z3v67 () Int) -(assert (distinct z3v66 z3v67)) -(declare-fun z3v68 () Int) -(declare-fun z3f69 (Int) Int) -(declare-fun z3f70 (Int) mySet) -(declare-fun z3v71 () Int) -(declare-fun z3f72 (Int) mySet) -(declare-fun z3v73 () Int) -(declare-fun z3v74 () Int) -(declare-fun z3v75 () Int) -(declare-fun z3f76 (Int) Bool) -(declare-fun z3f77 (Int Int) Int) -(declare-fun z3v78 () Int) -(declare-fun z3f79 (Int) Bool) -(declare-fun z3v80 () Int) -(declare-fun z3f81 (Int) Int) -(declare-fun z3v82 () Int) -(declare-fun z3v83 () Int) -(declare-fun z3v85 () Int) -(declare-fun z3v86 () Int) -(declare-fun z3v87 () Int) -(declare-fun z3f88 () Int) -(declare-fun z3v89 () Int) -(declare-fun z3v90 () Int) -(declare-fun z3v91 () Int) -(declare-fun z3v92 () Int) -(declare-fun z3v93 () Int) -(declare-fun z3f94 (Int) Int) -(declare-fun z3f95 (Int) Int) -(declare-fun z3f96 (Int Int Int) Int) -(declare-fun z3v97 () Int) -(declare-fun z3v98 () Int) -(declare-fun z3v99 () Int) -(declare-fun z3v100 () Int) -(declare-fun z3v101 () Int) -(declare-fun z3v102 () Int) -(declare-fun z3v103 () Int) -(declare-fun z3v104 () Int) -(declare-fun z3v105 () Int) -(declare-fun z3v106 () Int) -(declare-fun z3v107 () Int) -(declare-fun z3v108 () Int) -(declare-fun z3v109 () Int) -(declare-fun z3v110 () Int) -(declare-fun z3v113 () Int) -(declare-fun z3v114 () Int) -(declare-fun z3v115 () Int) -(declare-fun z3v116 () Int) -(declare-fun z3v117 () Int) -(declare-fun z3v118 () Int) -(declare-fun z3v120 () Int) -(declare-fun z3v121 () Int) -(declare-fun z3v122 () Int) -(declare-fun z3v124 () Int) -(declare-fun z3v125 () Int) -(declare-fun z3v126 () Int) -(declare-fun z3v127 () Int) -(declare-fun z3v128 () Int) -(declare-fun z3v129 () Int) -(declare-fun z3v131 () Int) -(declare-fun z3v132 () Int) -(declare-fun z3v133 () Int) -(declare-fun z3v134 () Int) -(declare-fun z3v135 () Int) -(declare-fun z3v136 () Int) -(declare-fun z3v137 () Int) -(declare-fun z3v138 () Int) -(declare-fun z3v139 () Int) -(declare-fun z3v140 () Int) -(declare-fun z3v141 () Int) -(declare-fun z3v142 () Int) -(declare-fun z3v144 () Int) -(declare-fun z3v145 () Int) -(declare-fun z3v146 () Int) -(declare-fun z3v149 () Int) -(declare-fun z3v151 () Int) -(declare-fun z3v154 () Int) -(declare-fun z3v155 () Int) -(declare-fun z3v156 () Int) -(declare-fun z3v157 () Int) -(declare-fun z3v158 () Int) -(declare-fun z3v159 () Int) -(declare-fun z3v161 () Int) -(declare-fun z3v163 () Int) -(declare-fun z3v164 () Int) -(declare-fun z3v165 () Int) -(declare-fun z3v167 () Int) -(declare-fun z3v170 () Int) -(declare-fun z3v174 () Int) -(declare-fun z3v175 () Int) -(declare-fun z3v176 () Int) -(declare-fun z3v179 () Int) -(declare-fun z3v181 () Int) -(declare-fun z3v182 () Int) -(declare-fun z3v183 () Int) -(declare-fun z3v184 () Int) -(declare-fun z3v187 () Int) -(declare-fun z3v188 () Int) -(declare-fun z3v189 () Int) -(declare-fun z3v190 () Int) -(declare-fun z3f191 (Int) Int) -(declare-fun z3f192 (Int) Int) -(declare-fun z3v195 () Int) -(declare-fun z3v196 () Int) -(declare-fun z3v199 () Int) -(declare-fun z3v200 () Int) -(declare-fun z3v201 () Int) -(declare-fun z3v202 () Int) -(declare-fun z3v203 () Int) -(declare-fun z3v206 () Int) -(declare-fun z3v207 () Int) -(declare-fun z3v208 () Int) -(declare-fun z3v210 () Int) -(declare-fun z3v211 () Int) -(declare-fun z3v212 () Int) -(declare-fun z3f213 (Int) Bool) -(declare-fun z3f214 (Int) Int) -(declare-fun z3v215 () Int) -(declare-fun z3v216 () Int) -(declare-fun z3v218 () Int) -(declare-fun z3v220 () Int) -(declare-fun z3v221 () Int) -(declare-fun z3v222 () Int) -(declare-fun z3v223 () Int) -(declare-fun z3v224 () Int) -(declare-fun z3v225 () Int) -(declare-fun z3v226 () Int) -(declare-fun z3v227 () Int) -(declare-fun z3v228 () Int) -(declare-fun z3v229 () Int) -(declare-fun z3v230 () Int) -(declare-fun z3v231 () Int) -(declare-fun z3v233 () Int) -(declare-fun z3v236 () Int) -(declare-fun z3v242 () Int) -(declare-fun z3v243 () Int) -(declare-fun z3v244 () Int) -(declare-fun z3v245 () Int) -(declare-fun z3v247 () Int) -(declare-fun z3v248 () Int) -(declare-fun z3v249 () Int) -(declare-fun z3v250 () Int) -(declare-fun z3v251 () Int) -(declare-fun z3v252 () Int) -(declare-fun z3v253 () Int) -(declare-fun z3v255 () Int) -(declare-fun z3v256 () Int) -(declare-fun z3v258 () Int) -(declare-fun z3v259 () Int) -(declare-fun z3v261 () Int) -(declare-fun z3v262 () Int) -(declare-fun z3v263 () Int) -(declare-fun z3v264 () Int) -(declare-fun z3v266 () Int) -(declare-fun z3v268 () Int) -(declare-fun z3v270 () Int) -(declare-fun z3v271 () Int) -(declare-fun z3v272 () Int) -(declare-fun z3v274 () Int) -(declare-fun z3v275 () Int) -(declare-fun z3v276 () Int) -(declare-fun z3v278 () Int) -(declare-fun z3v279 () Int) -(declare-fun z3v281 () Int) -(declare-fun z3v282 () Int) -(declare-fun z3v283 () Int) -(declare-fun z3v284 () Int) -(declare-fun z3v285 () Int) -(declare-fun z3v287 () Int) -(declare-fun z3v289 () Int) -(declare-fun z3v290 () Int) -(declare-fun z3v291 () Int) -(declare-fun z3v292 () Int) -(declare-fun z3v293 () Int) -(declare-fun z3v296 () Int) -(declare-fun z3v298 () Int) -(declare-fun z3v299 () Int) -(declare-fun z3f300 (Int Int) Int) -(declare-fun z3v301 () Int) -(declare-fun z3v302 () Int) -(declare-fun z3v303 () Int) -(declare-fun z3v304 () Int) -(declare-fun z3v308 () Int) -(declare-fun z3v309 () Int) -(declare-fun z3v310 () Int) -(declare-fun z3v314 () Int) -(declare-fun z3v315 () Int) -(declare-fun z3v316 () Int) -(declare-fun z3v317 () Int) -(declare-fun z3v318 () Int) -(declare-fun z3v319 () Int) -(declare-fun z3v320 () Int) -(declare-fun z3v324 () Int) -(declare-fun z3v325 () Int) -(declare-fun z3v326 () Int) -(declare-fun z3v327 () Int) -(declare-fun z3v328 () Int) -(declare-fun z3v330 () Int) -(declare-fun z3v332 () Int) -(declare-fun z3v333 () Int) -(declare-fun z3v334 () Int) -(declare-fun z3v335 () Int) -(declare-fun z3v336 () Int) -(declare-fun z3v337 () Int) -(declare-fun z3v339 () Int) -(declare-fun z3v340 () Int) -(declare-fun z3v341 () Int) -(declare-fun z3v342 () Int) -(assert (= z3v342 z3v113)) -(assert (>= (z3f69 z3v342) 0)) -(assert (and (>= (z3f69 z3v113) 0) (>= (z3f69 z3v114) 0) (= (z3f72 z3v114) smt_set_emp) (= (z3f70 z3v114) smt_set_emp) (= (z3f69 z3v114) 0) (= (z3f76 z3v114) true) (>= (z3f69 z3v115) 0) (= (z3f72 z3v115) (ite (smt_set_mem z3v116 (z3f70 z3v113)) (smt_set_cup (smt_set_add smt_set_emp z3v116) (z3f72 z3v113)) (z3f72 z3v113))) (= (z3f70 z3v115) (smt_set_cup (smt_set_add smt_set_emp z3v116) (z3f70 z3v113))) (= (z3f69 z3v115) (+ 1 (z3f69 z3v113))) (= (z3f76 z3v115) false) (= z3v115 (z3f77 z3v116 z3v113)) (>= (z3f69 z3v115) 0) (= z3v115 z3v117) (>= (z3f69 z3v115) 0) (= (z3f72 z3v115) smt_set_emp) (>= (z3f69 z3v117) 0) (= (z3f72 z3v117) smt_set_emp) (z3f79 z3v66) (= (z3f81 z3v80) z3v80) (= (z3f81 z3v82) z3v82) (not (z3f79 z3v67)) (= (z3f81 z3v83) z3v83))) -(assert (not (and (= (z3f72 z3v342) smt_set_emp) (not (smt_set_mem z3v116 (z3f70 z3v342)))))) -(check-sat) diff --git a/test/regress/regress0/sets/mar2014/UniqueZipper.hs.1030minimized.cvc4.smt2 b/test/regress/regress0/sets/mar2014/UniqueZipper.hs.1030minimized.cvc4.smt2 deleted file mode 100644 index 38477c46a..000000000 --- a/test/regress/regress0/sets/mar2014/UniqueZipper.hs.1030minimized.cvc4.smt2 +++ /dev/null @@ -1,209 +0,0 @@ -; EXPECT: sat -(set-logic QF_ALL_SUPPORTED) -(define-sort Elt () Int) -(define-sort mySet () (Set Elt )) -(define-fun smt_set_emp () mySet (as emptyset mySet)) -(define-fun smt_set_mem ((x Elt) (s mySet)) Bool (member x s)) -(define-fun smt_set_add ((s mySet) (x Elt)) mySet (union s (singleton x))) -(define-fun smt_set_cup ((s1 mySet) (s2 mySet)) mySet (union s1 s2)) -(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (intersection s1 s2)) -(define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (setminus s1 s2)) -(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subset s1 s2)) - -(declare-fun z3v66 () Int) -(declare-fun z3v67 () Int) -(assert (distinct z3v66 z3v67)) - -(declare-fun z3f70 (Int) mySet) -(declare-fun z3f72 (Int) mySet) -(declare-fun z3f76 (Int) Bool) -(declare-fun z3f77 (Int Int) Int) -(declare-fun z3v78 () Int) -(declare-fun z3f79 (Int) Bool) -(declare-fun z3v80 () Int) -(declare-fun z3f81 (Int) Int) -(declare-fun z3v82 () Int) -(declare-fun z3v83 () Int) -(declare-fun z3v85 () Int) -(declare-fun z3v86 () Int) -(declare-fun z3v87 () Int) -(declare-fun z3f88 () Int) -(declare-fun z3v89 () Int) -(declare-fun z3v90 () Int) -(declare-fun z3v91 () Int) -(declare-fun z3v92 () Int) -(declare-fun z3v93 () Int) -(declare-fun z3f94 (Int) Int) -(declare-fun z3f95 (Int) Int) -(declare-fun z3f96 (Int Int Int) Int) -(declare-fun z3v97 () Int) -(declare-fun z3v98 () Int) -(declare-fun z3v99 () Int) -(declare-fun z3v100 () Int) -(declare-fun z3v101 () Int) -(declare-fun z3v102 () Int) -(declare-fun z3v103 () Int) -(declare-fun z3v104 () Int) -(declare-fun z3v105 () Int) -(declare-fun z3v106 () Int) -(declare-fun z3v107 () Int) -(declare-fun z3v108 () Int) -(declare-fun z3v109 () Int) -(declare-fun z3v110 () Int) -(declare-fun z3v113 () Int) -(declare-fun z3v114 () Int) -(declare-fun z3v115 () Int) -(declare-fun z3v116 () Int) -(declare-fun z3v117 () Int) -(declare-fun z3v118 () Int) -(declare-fun z3v120 () Int) -(declare-fun z3v121 () Int) -(declare-fun z3v122 () Int) -(declare-fun z3v124 () Int) -(declare-fun z3v125 () Int) -(declare-fun z3v126 () Int) -(declare-fun z3v127 () Int) -(declare-fun z3v128 () Int) -(declare-fun z3v129 () Int) -(declare-fun z3v131 () Int) -(declare-fun z3v132 () Int) -(declare-fun z3v133 () Int) -(declare-fun z3v134 () Int) -(declare-fun z3v135 () Int) -(declare-fun z3v136 () Int) -(declare-fun z3v137 () Int) -(declare-fun z3v138 () Int) -(declare-fun z3v139 () Int) -(declare-fun z3v140 () Int) -(declare-fun z3v141 () Int) -(declare-fun z3v142 () Int) -(declare-fun z3v144 () Int) -(declare-fun z3v145 () Int) -(declare-fun z3v146 () Int) -(declare-fun z3v149 () Int) -(declare-fun z3v151 () Int) -(declare-fun z3v154 () Int) -(declare-fun z3v155 () Int) -(declare-fun z3v156 () Int) -(declare-fun z3v157 () Int) -(declare-fun z3v158 () Int) -(declare-fun z3v159 () Int) -(declare-fun z3v161 () Int) -(declare-fun z3v163 () Int) -(declare-fun z3v164 () Int) -(declare-fun z3v165 () Int) -(declare-fun z3v167 () Int) -(declare-fun z3v170 () Int) -(declare-fun z3v174 () Int) -(declare-fun z3v175 () Int) -(declare-fun z3v176 () Int) -(declare-fun z3v179 () Int) -(declare-fun z3v181 () Int) -(declare-fun z3v182 () Int) -(declare-fun z3v183 () Int) -(declare-fun z3v184 () Int) -(declare-fun z3v187 () Int) -(declare-fun z3v188 () Int) -(declare-fun z3v189 () Int) -(declare-fun z3v190 () Int) -(declare-fun z3f191 (Int) Int) -(declare-fun z3f192 (Int) Int) -(declare-fun z3v195 () Int) -(declare-fun z3v196 () Int) -(declare-fun z3v199 () Int) -(declare-fun z3v200 () Int) -(declare-fun z3v201 () Int) -(declare-fun z3v202 () Int) -(declare-fun z3v203 () Int) -(declare-fun z3v206 () Int) -(declare-fun z3v207 () Int) -(declare-fun z3v208 () Int) -(declare-fun z3v210 () Int) -(declare-fun z3v211 () Int) -(declare-fun z3v212 () Int) -(declare-fun z3f213 (Int) Bool) -(declare-fun z3f214 (Int) Int) -(declare-fun z3v215 () Int) -(declare-fun z3v216 () Int) -(declare-fun z3v218 () Int) -(declare-fun z3v220 () Int) -(declare-fun z3v221 () Int) -(declare-fun z3v222 () Int) -(declare-fun z3v223 () Int) -(declare-fun z3v224 () Int) -(declare-fun z3v225 () Int) -(declare-fun z3v226 () Int) -(declare-fun z3v227 () Int) -(declare-fun z3v228 () Int) -(declare-fun z3v229 () Int) -(declare-fun z3v230 () Int) -(declare-fun z3v231 () Int) -(declare-fun z3v233 () Int) -(declare-fun z3v236 () Int) -(declare-fun z3v242 () Int) -(declare-fun z3v243 () Int) -(declare-fun z3v244 () Int) -(declare-fun z3v245 () Int) -(declare-fun z3v247 () Int) -(declare-fun z3v248 () Int) -(declare-fun z3v249 () Int) -(declare-fun z3v250 () Int) -(declare-fun z3v251 () Int) -(declare-fun z3v252 () Int) -(declare-fun z3v253 () Int) -(declare-fun z3v255 () Int) -(declare-fun z3v256 () Int) -(declare-fun z3v258 () Int) -(declare-fun z3v259 () Int) -(declare-fun z3v261 () Int) -(declare-fun z3v262 () Int) -(declare-fun z3v263 () Int) -(declare-fun z3v264 () Int) -(declare-fun z3v266 () Int) -(declare-fun z3v268 () Int) -(declare-fun z3v270 () Int) -(declare-fun z3v271 () Int) -(declare-fun z3v272 () Int) - -(assert (and (not (smt_set_mem z3v132 (z3f70 z3v131))) - (= (z3f72 z3v131) smt_set_emp) - (= (z3f72 z3v133) smt_set_emp) - (= (z3f72 z3v242) - (ite (smt_set_mem z3v271 (z3f70 z3v270)) - (smt_set_cup (smt_set_add smt_set_emp z3v271) - (z3f72 z3v270)) - (z3f72 z3v270))) - (= (z3f70 z3v242) - (smt_set_cup (smt_set_add smt_set_emp z3v271) - (z3f70 z3v270))) - (= z3v242 (z3f77 z3v271 z3v270)) - (= z3v242 z3v243) - (smt_set_sub (z3f70 z3v242) - (z3f70 z3v244)) - (= (z3f72 z3v242) smt_set_emp) - (smt_set_sub (z3f70 z3v243) - (z3f70 z3v244)) - (= (z3f72 z3v243) smt_set_emp) - (= (z3f72 z3v244) - (ite (smt_set_mem z3v132 (z3f70 z3v131)) - (smt_set_cup (smt_set_add smt_set_emp z3v132) - (z3f72 z3v131)) - (z3f72 z3v131))) - (= (z3f70 z3v244) - (smt_set_cup (smt_set_add smt_set_emp z3v132) - (z3f70 z3v131))) - (= (z3f94 z3v134) z3v133) - (= (z3f95 z3v134) z3v131) - (= z3v134 z3v135) - (= (smt_set_cap (z3f70 (z3f94 z3v134)) - (z3f70 (z3f95 z3v134))) smt_set_emp) - (= (smt_set_cap (z3f70 (z3f94 z3v135)) - (z3f70 (z3f95 z3v135))) smt_set_emp) - (= z3v272 z3v133) - (= (z3f72 z3v272) smt_set_emp) - (= (z3f81 z3v80) z3v80) - (= (z3f81 z3v82) z3v82) - (= (z3f81 z3v83) z3v83) - )) - -(check-sat) diff --git a/test/regress/regress0/sets/mar2014/UniqueZipper.hs.1030minimized2.cvc4.smt2 b/test/regress/regress0/sets/mar2014/UniqueZipper.hs.1030minimized2.cvc4.smt2 deleted file mode 100644 index e282e446e..000000000 --- a/test/regress/regress0/sets/mar2014/UniqueZipper.hs.1030minimized2.cvc4.smt2 +++ /dev/null @@ -1,202 +0,0 @@ -; EXPECT: sat -(set-logic QF_ALL_SUPPORTED) -(define-sort Elt () Int) -(define-sort mySet () (Set Elt )) -(define-fun smt_set_emp () mySet (as emptyset mySet)) -(define-fun smt_set_mem ((x Elt) (s mySet)) Bool (member x s)) -(define-fun smt_set_add ((s mySet) (x Elt)) mySet (union s (singleton x))) -(define-fun smt_set_cup ((s1 mySet) (s2 mySet)) mySet (union s1 s2)) -(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (intersection s1 s2)) -(define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (setminus s1 s2)) -(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subset s1 s2)) - -(declare-fun z3f70 (Int) mySet) -(declare-fun z3f72 (Int) mySet) -(declare-fun z3f76 (Int) Bool) -(declare-fun z3f77 (Int Int) Int) -(declare-fun z3v78 () Int) -(declare-fun z3f79 (Int) Bool) -(declare-fun z3v80 () Int) -(declare-fun z3f81 (Int) Int) -(declare-fun z3v82 () Int) -(declare-fun z3v83 () Int) -(declare-fun z3v85 () Int) -(declare-fun z3v86 () Int) -(declare-fun z3v87 () Int) -(declare-fun z3f88 () Int) -(declare-fun z3v89 () Int) -(declare-fun z3v90 () Int) -(declare-fun z3v91 () Int) -(declare-fun z3v92 () Int) -(declare-fun z3v93 () Int) -(declare-fun z3f94 (Int) Int) -(declare-fun z3f95 (Int) Int) -(declare-fun z3f96 (Int Int Int) Int) -(declare-fun z3v97 () Int) -(declare-fun z3v98 () Int) -(declare-fun z3v99 () Int) -(declare-fun z3v100 () Int) -(declare-fun z3v101 () Int) -(declare-fun z3v102 () Int) -(declare-fun z3v103 () Int) -(declare-fun z3v104 () Int) -(declare-fun z3v105 () Int) -(declare-fun z3v106 () Int) -(declare-fun z3v107 () Int) -(declare-fun z3v108 () Int) -(declare-fun z3v109 () Int) -(declare-fun z3v110 () Int) -(declare-fun z3v113 () Int) -(declare-fun z3v114 () Int) -(declare-fun z3v115 () Int) -(declare-fun z3v116 () Int) -(declare-fun z3v117 () Int) -(declare-fun z3v118 () Int) -(declare-fun z3v120 () Int) -(declare-fun z3v121 () Int) -(declare-fun z3v122 () Int) -(declare-fun z3v124 () Int) -(declare-fun z3v125 () Int) -(declare-fun z3v126 () Int) -(declare-fun z3v127 () Int) -(declare-fun z3v128 () Int) -(declare-fun z3v129 () Int) -(declare-fun z3v131 () Int) -(declare-fun z3v132 () Int) -(declare-fun z3v133 () Int) -(declare-fun z3v134 () Int) -(declare-fun z3v135 () Int) -(declare-fun z3v136 () Int) -(declare-fun z3v137 () Int) -(declare-fun z3v138 () Int) -(declare-fun z3v139 () Int) -(declare-fun z3v140 () Int) -(declare-fun z3v141 () Int) -(declare-fun z3v142 () Int) -(declare-fun z3v144 () Int) -(declare-fun z3v145 () Int) -(declare-fun z3v146 () Int) -(declare-fun z3v149 () Int) -(declare-fun z3v151 () Int) -(declare-fun z3v154 () Int) -(declare-fun z3v155 () Int) -(declare-fun z3v156 () Int) -(declare-fun z3v157 () Int) -(declare-fun z3v158 () Int) -(declare-fun z3v159 () Int) -(declare-fun z3v161 () Int) -(declare-fun z3v163 () Int) -(declare-fun z3v164 () Int) -(declare-fun z3v165 () Int) -(declare-fun z3v167 () Int) -(declare-fun z3v170 () Int) -(declare-fun z3v174 () Int) -(declare-fun z3v175 () Int) -(declare-fun z3v176 () Int) -(declare-fun z3v179 () Int) -(declare-fun z3v181 () Int) -(declare-fun z3v182 () Int) -(declare-fun z3v183 () Int) -(declare-fun z3v184 () Int) -(declare-fun z3v187 () Int) -(declare-fun z3v188 () Int) -(declare-fun z3v189 () Int) -(declare-fun z3v190 () Int) -(declare-fun z3f191 (Int) Int) -(declare-fun z3f192 (Int) Int) -(declare-fun z3v195 () Int) -(declare-fun z3v196 () Int) -(declare-fun z3v199 () Int) -(declare-fun z3v200 () Int) -(declare-fun z3v201 () Int) -(declare-fun z3v202 () Int) -(declare-fun z3v203 () Int) -(declare-fun z3v206 () Int) -(declare-fun z3v207 () Int) -(declare-fun z3v208 () Int) -(declare-fun z3v210 () Int) -(declare-fun z3v211 () Int) -(declare-fun z3v212 () Int) -(declare-fun z3f213 (Int) Bool) -(declare-fun z3f214 (Int) Int) -(declare-fun z3v215 () Int) -(declare-fun z3v216 () Int) -(declare-fun z3v218 () Int) -(declare-fun z3v220 () Int) -(declare-fun z3v221 () Int) -(declare-fun z3v222 () Int) -(declare-fun z3v223 () Int) -(declare-fun z3v224 () Int) -(declare-fun z3v225 () Int) -(declare-fun z3v226 () Int) -(declare-fun z3v227 () Int) -(declare-fun z3v228 () Int) -(declare-fun z3v229 () Int) -(declare-fun z3v230 () Int) -(declare-fun z3v231 () Int) -(declare-fun z3v233 () Int) -(declare-fun z3v236 () Int) -(declare-fun z3v242 () Int) -(declare-fun z3v243 () Int) -(declare-fun z3v244 () Int) -(declare-fun z3v245 () Int) -(declare-fun z3v247 () Int) -(declare-fun z3v248 () Int) -(declare-fun z3v249 () Int) -(declare-fun z3v250 () Int) -(declare-fun z3v251 () Int) -(declare-fun z3v252 () Int) -(declare-fun z3v253 () Int) -(declare-fun z3v255 () Int) -(declare-fun z3v256 () Int) -(declare-fun z3v258 () Int) -(declare-fun z3v259 () Int) -(declare-fun z3v261 () Int) -(declare-fun z3v262 () Int) -(declare-fun z3v263 () Int) -(declare-fun z3v264 () Int) -(declare-fun z3v266 () Int) -(declare-fun z3v268 () Int) -(declare-fun z3v270 () Int) -(declare-fun z3v271 () Int) -(declare-fun z3v272 () Int) - - -(declare-fun z3v66 () Int) -(declare-fun z3v67 () Int) -(assert (distinct z3v66 z3v67)) -(assert (not (smt_set_mem z3v132 (z3f70 z3v131)))) -(assert (= (z3f72 z3v131) smt_set_emp)) -(assert (= (z3f72 z3v242) - (ite (smt_set_mem z3v271 (z3f70 z3v270)) - (smt_set_cup (smt_set_add smt_set_emp z3v271) - (z3f72 z3v270)) - (z3f72 z3v270)))) -(assert (= (z3f70 z3v242) - (smt_set_cup (smt_set_add smt_set_emp z3v271) - (z3f70 z3v270)))) -(assert (= z3v242 (z3f77 z3v271 z3v270))) -(assert (= z3v242 z3v243)) -(assert (subset (z3f70 z3v242) - (z3f70 z3v244))) -(assert (= (z3f72 z3v243) smt_set_emp)) -(assert (= (z3f72 z3v244) - (ite (smt_set_mem z3v132 (z3f70 z3v131)) - (smt_set_cup (smt_set_add smt_set_emp z3v132) - (z3f72 z3v131)) - (z3f72 z3v131)))) -(assert (= (z3f70 z3v244) - (smt_set_cup (smt_set_add smt_set_emp z3v132) - (z3f70 z3v131)))) -(assert (= (z3f94 z3v134) z3v133)) -(assert (= (z3f95 z3v134) z3v131)) -(assert (= z3v134 z3v135)) -(assert (= (smt_set_cap (z3f70 (z3f94 z3v135)) - (z3f70 (z3f95 z3v135))) smt_set_emp)) -(assert (= z3v272 z3v133)) -(assert (= (z3f72 z3v272) smt_set_emp)) -(assert (= (z3f81 z3v80) z3v80)) -(assert (= (z3f81 z3v82) z3v82)) -(assert (= (z3f81 z3v83) z3v83)) - -(check-sat) diff --git a/test/regress/regress0/sets/mar2014/lemmabug-ListElts317minimized.smt2 b/test/regress/regress0/sets/mar2014/lemmabug-ListElts317minimized.smt2 deleted file mode 100644 index 0fc8ca067..000000000 --- a/test/regress/regress0/sets/mar2014/lemmabug-ListElts317minimized.smt2 +++ /dev/null @@ -1,89 +0,0 @@ -; EXPECT: sat - -; Observed behavior: -; --check-model failed for set-term (union (z3f69 z3v151) (singleton z3v143)) -; with different set of elements in the model for representative and the node -; itself. -; -; Issue: -; The trouble with data structure being mainted to ensure that things -; for which lemmas have been generated are not generated again. This -; data structure (d_pendingEverInserted) needs to be user context -; dependent. The bug was in the sequence of steps from requesting that -; a lemma be generated to when it actually was. Sequence was: -; addToPending (and also adds to pending ever inserted) -> -; isComplete (might remove things from pending if requirment met in other ways) -> -; getLemma (actually generated the lemma, if requirement not already met) -; -; Resolution: -; adding terms to d_pendingEverInserted was moved from addToPending() -; to getLemma(). - -(set-logic QF_ALL_SUPPORTED) -(set-info :status sat) -(define-sort Elt () Int) -(define-sort mySet () (Set Elt )) -(define-fun smt_set_emp () mySet (as emptyset mySet)) -(define-fun smt_set_mem ((x Elt) (s mySet)) Bool (member x s)) -(define-fun smt_set_add ((s mySet) (x Elt)) mySet (union s (singleton x))) -(define-fun smt_set_cup ((s1 mySet) (s2 mySet)) mySet (union s1 s2)) -(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (intersection s1 s2)) -;(define-fun smt_set_com ((s mySet)) mySet ((_ map not) s)) -(define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (setminus s1 s2)) -;(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (= smt_set_emp (smt_set_dif s1 s2))) -(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subset s1 s2)) - -(declare-fun z3v58 () Int) -(declare-fun z3v59 () Int) -(assert (distinct z3v58 z3v59)) - -(declare-fun z3f60 (Int) Bool) -(declare-fun z3v61 () Int) -(declare-fun z3f62 (Int) Int) -(declare-fun z3v63 () Int) -(declare-fun z3v64 () Int) -(declare-fun z3v67 () Int) -(declare-fun z3f68 (Int) Int) -(declare-fun z3f69 (Int) mySet) -(declare-fun z3f70 (Int) mySet) -(declare-fun z3f71 (Int) Bool) -(declare-fun z3v90 () Int) -(declare-fun z3v91 () Int) -(declare-fun z3f92 (Int Int) Int) -(declare-fun z3v140 () Int) -(declare-fun z3v141 () Int) -(declare-fun z3v142 () Int) -(declare-fun z3v143 () Int) -(declare-fun z3v144 () Int) -(declare-fun z3v145 () Int) -(declare-fun z3v147 () Int) -(declare-fun z3v150 () Int) -(declare-fun z3v151 () Int) -(declare-fun z3v152 () Int) - -(assert (not (= (z3f69 z3v152) - (z3f69 z3v140)))) - -(assert (= (z3f69 z3v151) - (smt_set_cup (z3f69 z3v141) - (z3f69 z3v140)))) - -(assert (= (z3f69 z3v152) - (smt_set_cup (singleton z3v143) (z3f69 z3v151)))) - -(assert (= (z3f70 z3v152) - (smt_set_cup (singleton z3v143) (z3f70 z3v151)))) - -(assert (and - (= (z3f69 z3v142) - (smt_set_cup (singleton z3v143) (z3f69 z3v141))) - (= (z3f70 z3v142) - (smt_set_cup (singleton z3v143) (z3f70 z3v141))) - (= z3v142 (z3f92 z3v143 z3v141)) - (= z3v142 z3v144) - (= (z3f62 z3v61) z3v61) - (= (z3f62 z3v63) z3v63) - ) - ) - -(check-sat) diff --git a/test/regress/regress0/sets/setofsets-disequal.smt2 b/test/regress/regress0/sets/setofsets-disequal.smt2 deleted file mode 100644 index 1702aab27..000000000 --- a/test/regress/regress0/sets/setofsets-disequal.smt2 +++ /dev/null @@ -1,64 +0,0 @@ -; On a production build (as of 2014-05-16), takes several minutes -; to finish (2967466 decisions). - -(set-logic QF_BVFS) -(set-info :status unsat) - -(define-sort myset () (Set (Set (_ BitVec 1)))) -(declare-fun S () myset) - -; 0 elements -(assert (not (= S (as emptyset myset)))) - -; 1 element is S -(assert (not (= S (singleton (as emptyset (Set (_ BitVec 1))))))) -(assert (not (= S (singleton (singleton (_ bv0 1)) )))) -(assert (not (= S (singleton (singleton (_ bv1 1)) )))) -(assert (not (= S (singleton (union (singleton (_ bv0 1)) - (singleton (_ bv1 1))))))) - -; 2 elements in S -(assert (not (= S (union (singleton (as emptyset (Set (_ BitVec 1)))) - (singleton (singleton (_ bv0 1)))) ))) -(assert (not (= S (union (singleton (as emptyset (Set (_ BitVec 1)))) - (singleton (singleton (_ bv1 1))))))) -(assert (not (= S (union (singleton (as emptyset (Set (_ BitVec 1)))) - (singleton (union (singleton (_ bv0 1)) - (singleton (_ bv1 1)))))))) -(assert (not (= S (union (singleton (union (singleton (_ bv0 1)) - (singleton (_ bv1 1)))) - (singleton (singleton (_ bv0 1)))) ))) -(assert (not (= S (union (singleton (singleton (_ bv0 1))) - (singleton (singleton (_ bv1 1)))) ))) -(assert (not (= S (union (singleton (union (singleton (_ bv0 1)) - (singleton (_ bv1 1)))) - (singleton (singleton (_ bv1 1))))))) - -; 3 elements in S -(assert (not (= S (union (singleton (singleton (_ bv1 1))) - (union (singleton (as emptyset (Set (_ BitVec 1)))) - (singleton (singleton (_ bv0 1))))) ))) -(assert (not (= S (union (singleton (union (singleton (_ bv0 1)) - (singleton (_ bv1 1)))) - (union (singleton (as emptyset (Set (_ BitVec 1)))) - (singleton (singleton (_ bv1 1))))) ))) -(assert (not (= S (union (singleton (union (singleton (_ bv0 1)) - (singleton (_ bv1 1)))) - (union (singleton (singleton (_ bv0 1))) - (singleton (singleton (_ bv1 1))))) ))) -(assert (not (= S (union (singleton (union (singleton (_ bv0 1)) - (singleton (_ bv1 1)))) - (union (singleton (as emptyset (Set (_ BitVec 1)))) - (singleton (singleton (_ bv0 1))))) ))) - -; 4 elements in S -(assert (not (= S (union (singleton (union (singleton (_ bv0 1)) - (singleton (_ bv1 1)))) - (union (singleton (singleton (_ bv1 1))) - (union (singleton (as emptyset (Set (_ BitVec 1)))) - (singleton (singleton (_ bv0 1)))))) ))) - -(check-sat) - -; if you delete any of the above assertions, you should get sat -; (get-model) diff --git a/test/regress/regress0/sets/sets-tuple-poly.cvc b/test/regress/regress0/sets/sets-tuple-poly.cvc deleted file mode 100644 index 4cac9a24e..000000000 --- a/test/regress/regress0/sets/sets-tuple-poly.cvc +++ /dev/null @@ -1,17 +0,0 @@ -% EXPECT: sat -OPTION "sets-ext"; -OPTION "logic" "ALL_SUPPORTED"; - -a : SET OF [REAL, INT]; -b : SET OF [INT, REAL]; - -x : [ REAL, REAL ]; - -ASSERT NOT x = (0.0,0.0); - -ASSERT (x.0, FLOOR(x.1)) IS_IN a; -ASSERT (FLOOR(x.0), x.1) IS_IN b; - -ASSERT NOT x.0 = x.1; - -CHECKSAT; diff --git a/test/regress/regress0/sets/sharingbug.smt2 b/test/regress/regress0/sets/sharingbug.smt2 deleted file mode 100644 index b87579816..000000000 --- a/test/regress/regress0/sets/sharingbug.smt2 +++ /dev/null @@ -1,157 +0,0 @@ -(set-info :source |fuzzsmt|) -(set-info :smt-lib-version 2.0) -(set-info :category "random") -(set-info :status sat) -(set-logic QF_UFLIAFS) -(define-sort Element () Int) -(declare-fun f0 ( Int Int Int) Int) -(declare-fun f1 ( (Set Element)) (Set Element)) -(declare-fun p0 ( Int Int Int) Bool) -(declare-fun p1 ( (Set Element)) Bool) -(declare-fun v0 () Int) -(declare-fun v1 () (Set Element)) -(declare-fun v2 () (Set Element)) -(declare-fun v3 () (Set Element)) -(assert (let ((e4 1)) -(let ((e5 (- v0))) -(let ((e6 (* v0 (- e4)))) -(let ((e7 (ite (p0 v0 e5 v0) 1 0))) -(let ((e8 (- e6 e7))) -(let ((e9 (+ e5 v0))) -(let ((e10 (ite (p0 e7 e7 e5) 1 0))) -(let ((e11 (+ e8 e10))) -(let ((e12 (* (- e4) e7))) -(let ((e13 (- e10))) -(let ((e14 (f0 e5 e7 e6))) -(let ((e15 (member v0 v1))) -(let ((e16 (member e12 v2))) -(let ((e17 (member e14 v1))) -(let ((e18 (f1 v3))) -(let ((e19 (f1 v2))) -(let ((e20 (f1 v1))) -(let ((e21 (>= v0 e9))) -(let ((e22 (> e6 e6))) -(let ((e23 (> e5 e12))) -(let ((e24 (distinct e8 e11))) -(let ((e25 (= e10 e10))) -(let ((e26 (> e13 e13))) -(let ((e27 (distinct e14 e10))) -(let ((e28 (> e11 e5))) -(let ((e29 (>= e14 e6))) -(let ((e30 (< e14 e14))) -(let ((e31 (< e7 e12))) -(let ((e32 (<= e11 e12))) -(let ((e33 (< e14 e11))) -(let ((e34 (<= e7 e9))) -(let ((e35 (distinct e12 e5))) -(let ((e36 (= e14 e6))) -(let ((e37 (< v0 e8))) -(let ((e38 (< e13 e14))) -(let ((e39 (>= e6 e13))) -(let ((e40 (< e12 e13))) -(let ((e41 (< v0 e14))) -(let ((e42 (< v0 e11))) -(let ((e43 (p0 e13 e7 e8))) -(let ((e44 (ite e17 e19 e19))) -(let ((e45 (ite e34 v1 v1))) -(let ((e46 (ite e28 v1 e44))) -(let ((e47 (ite e24 e44 e20))) -(let ((e48 (ite e39 e18 v3))) -(let ((e49 (ite e35 v2 v3))) -(let ((e50 (ite e38 e18 e20))) -(let ((e51 (ite e22 v2 e44))) -(let ((e52 (ite e17 e20 e18))) -(let ((e53 (ite e35 e52 e19))) -(let ((e54 (ite e38 e49 e20))) -(let ((e55 (ite e15 e20 e45))) -(let ((e56 (ite e37 v1 v3))) -(let ((e57 (ite e41 e50 v1))) -(let ((e58 (ite e28 v1 e54))) -(let ((e59 (ite e27 e19 e53))) -(let ((e60 (ite e16 e46 e44))) -(let ((e61 (ite e29 e57 e52))) -(let ((e62 (ite e21 e50 e53))) -(let ((e63 (ite e32 e45 e19))) -(let ((e64 (ite e42 v3 e57))) -(let ((e65 (ite e33 e50 v3))) -(let ((e66 (ite e43 e49 e20))) -(let ((e67 (ite e22 v1 e63))) -(let ((e68 (ite e40 e45 e19))) -(let ((e69 (ite e30 e62 e58))) -(let ((e70 (ite e24 e52 e58))) -(let ((e71 (ite e31 e64 e67))) -(let ((e72 (ite e30 e18 e20))) -(let ((e73 (ite e25 e58 e44))) -(let ((e74 (ite e36 e63 v3))) -(let ((e75 (ite e43 e62 e73))) -(let ((e76 (ite e26 e61 e55))) -(let ((e77 (ite e23 e61 e71))) -(let ((e78 (ite e40 e13 v0))) -(let ((e79 (ite e23 e8 e13))) -(let ((e80 (ite e24 e78 e6))) -(let ((e81 (ite e39 e9 e80))) -(let ((e82 (ite e31 e7 v0))) -(let ((e83 (ite e43 e14 e6))) -(let ((e84 (ite e38 e80 e81))) -(let ((e85 (ite e32 e14 e10))) -(let ((e86 (ite e29 e84 e78))) -(let ((e87 (ite e27 e12 e8))) -(let ((e88 (ite e31 e11 e6))) -(let ((e89 (ite e33 e88 e85))) -(let ((e90 (ite e36 e12 v0))) -(let ((e91 (ite e23 e5 e7))) -(let ((e92 (ite e34 e89 e80))) -(let ((e93 (ite e15 e79 v0))) -(let ((e94 (ite e21 e6 e7))) -(let ((e95 (ite e26 v0 e91))) -(let ((e96 (ite e28 e94 e87))) -(let ((e97 (ite e32 e90 e78))) -(let ((e98 (ite e42 e78 e83))) -(let ((e99 (ite e40 e13 e82))) -(let ((e100 (ite e25 e88 e90))) -(let ((e101 (ite e26 e11 e81))) -(let ((e102 (ite e17 e101 e81))) -(let ((e103 (ite e30 v0 e80))) -(let ((e104 (ite e28 e80 e79))) -(let ((e105 (ite e27 e95 e101))) -(let ((e106 (ite e22 e92 e94))) -(let ((e107 (ite e16 e82 e94))) -(let ((e108 (ite e41 e10 e78))) -(let ((e109 (ite e37 e107 e84))) -(let ((e110 (ite e35 e89 e92))) -(let ((e111 (and e30 e37))) -(let ((e112 (=> e21 e41))) -(let ((e113 (ite e25 e33 e26))) -(let ((e114 (and e34 e38))) -(let ((e115 (=> e22 e43))) -(let ((e116 (and e24 e35))) -(let ((e117 (not e112))) -(let ((e118 (=> e27 e116))) -(let ((e119 (= e36 e15))) -(let ((e120 (= e42 e42))) -(let ((e121 (xor e29 e115))) -(let ((e122 (xor e39 e16))) -(let ((e123 (or e118 e32))) -(let ((e124 (not e28))) -(let ((e125 (=> e23 e40))) -(let ((e126 (ite e17 e123 e111))) -(let ((e127 (not e117))) -(let ((e128 (not e31))) -(let ((e129 (xor e121 e126))) -(let ((e130 (or e125 e119))) -(let ((e131 (=> e127 e114))) -(let ((e132 (or e113 e128))) -(let ((e133 (= e122 e124))) -(let ((e134 (not e130))) -(let ((e135 (or e133 e132))) -(let ((e136 (= e129 e135))) -(let ((e137 (=> e120 e120))) -(let ((e138 (or e134 e137))) -(let ((e139 (or e138 e138))) -(let ((e140 (and e139 e131))) -(let ((e141 (or e136 e136))) -(let ((e142 (= e140 e141))) -e142 -)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) - -(check-sat) diff --git a/test/regress/regress0/sets/univ-set-uf-elim.smt2 b/test/regress/regress0/sets/univ-set-uf-elim.smt2 deleted file mode 100644 index a22f2a44f..000000000 --- a/test/regress/regress0/sets/univ-set-uf-elim.smt2 +++ /dev/null @@ -1,16 +0,0 @@ -; EXPECT: (error "Extended set operators are not supported in default mode, try --sets-ext.") -; EXIT: 1 -(set-logic ALL) -(declare-fun a () Int) -(declare-fun f ((Set Bool)) Int) -(declare-fun s () (Set Bool)) - -(assert (member true s)) -(assert (member false s)) -(assert (= a (f (as univset (Set Bool))))) - -(assert (= (f (as emptyset (Set Bool))) 1)) -(assert (= (f (singleton true)) 2)) -(assert (= (f (singleton false)) 3)) -(assert (= (f (union (singleton true) (singleton false))) 4)) -(check-sat) |