From b8ddf766460bfcf475e08ff52c889246e78f76cc Mon Sep 17 00:00:00 2001 From: Kshitij Bansal Date: Sun, 22 Jun 2014 01:17:27 -0400 Subject: Renaming of SMT2 operator names, kinds for set theory * SET_SINGLETON kind renamed to just SINGLETON * "setenum" smt2 opertor renamed to "singleton"[1] * "in" smt2 operator renamed to "member"[2] [1] It was anyhow accepting exactly one argument, so was bit misleading to call set enumerator. [2] The corresponding kind was called MEMBER, so this will also make them consistent. Only inconsistency now is for subset: kind is called SUBSET but operator is called "subseteq". --- .../sets/jan24/deepmeas0.hs.fqout.cvc4.47.smt2 | 4 +- .../sets/jan24/deepmeas0.hs.fqout.small.smt2 | 6 +- .../regress0/sets/jan24/insert_invariant_37_2.smt2 | 218 ++++++++++----------- .../sets/jan24/remove_check_free_31_6.smt2 | 58 +++--- 4 files changed, 143 insertions(+), 143 deletions(-) (limited to 'test/regress/regress0/sets/jan24') diff --git a/test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.cvc4.47.smt2 b/test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.cvc4.47.smt2 index b90563199..bc919673d 100644 --- a/test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.cvc4.47.smt2 +++ b/test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.cvc4.47.smt2 @@ -3,8 +3,8 @@ (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 (in x s)) -(define-fun smt_set_add ((s mySet) (x Elt)) mySet (union s (setenum x))) +(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)) diff --git a/test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.small.smt2 b/test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.small.smt2 index 204af2f2d..652307645 100644 --- a/test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.small.smt2 +++ b/test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.small.smt2 @@ -7,12 +7,12 @@ (declare-fun S () (Set Int)) (declare-fun T () (Set Int)) -(assert (in x S)) +(assert (member x S)) -(assert (= S (union T (setenum y)))) +(assert (= S (union T (singleton y)))) (assert (not (= x y))) -(assert (not (in x T))) +(assert (not (member x T))) (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 index ad0a7e464..4a588aeb6 100644 --- a/test/regress/regress0/sets/jan24/insert_invariant_37_2.smt2 +++ b/test/regress/regress0/sets/jan24/insert_invariant_37_2.smt2 @@ -61,13 +61,13 @@ (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 (in l1 sk_?X$0)) - (not (in l2 sk_?X$0))))) + (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) - (in (read$0 data$0 l1) + (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)) @@ -78,7 +78,7 @@ (witness$0 (read$0 data$0 curr_2$0) (sorted_set_c$0 data$0 next$0 lst$0 null$0)) null$0) - (in (read$0 data$0 curr_2$0) + (member (read$0 data$0 curr_2$0) (sorted_set_c$0 data$0 next$0 lst$0 null$0))) (or (and @@ -86,12 +86,12 @@ (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)))) - (in + (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 - (in (read$0 data$0 curr_2$0) + (member (read$0 data$0 curr_2$0) (sorted_set_c$0 data$0 next$0 lst$0 null$0))))) :named sorted_set_2)) @@ -101,7 +101,7 @@ (witness$0 (read$0 data$0 prev_2$0) (sorted_set_c$0 data$0 next$0 lst$0 null$0)) null$0) - (in (read$0 data$0 prev_2$0) + (member (read$0 data$0 prev_2$0) (sorted_set_c$0 data$0 next$0 lst$0 null$0))) (or (and @@ -109,12 +109,12 @@ (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)))) - (in + (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 - (in (read$0 data$0 prev_2$0) + (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)) @@ -124,7 +124,7 @@ (witness$0 (read$0 data$0 sk_l1$0) (sorted_set_c$0 data$0 next$0 lst$0 null$0)) null$0) - (in (read$0 data$0 sk_l1$0) + (member (read$0 data$0 sk_l1$0) (sorted_set_c$0 data$0 next$0 lst$0 null$0))) (or (and @@ -132,12 +132,12 @@ (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)))) - (in + (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 - (in (read$0 data$0 sk_l1$0) + (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)) @@ -147,7 +147,7 @@ (witness$0 (read$0 data$0 sk_l1_1$0) (sorted_set_c$0 data$0 next$0 lst$0 null$0)) null$0) - (in (read$0 data$0 sk_l1_1$0) + (member (read$0 data$0 sk_l1_1$0) (sorted_set_c$0 data$0 next$0 lst$0 null$0))) (or (and @@ -155,12 +155,12 @@ (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)))) - (in + (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 - (in (read$0 data$0 sk_l1_1$0) + (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)) @@ -170,7 +170,7 @@ (witness$0 (read$0 data$0 sk_l2$0) (sorted_set_c$0 data$0 next$0 lst$0 null$0)) null$0) - (in (read$0 data$0 sk_l2$0) + (member (read$0 data$0 sk_l2$0) (sorted_set_c$0 data$0 next$0 lst$0 null$0))) (or (and @@ -178,12 +178,12 @@ (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)))) - (in + (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 - (in (read$0 data$0 sk_l2$0) + (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)) @@ -193,7 +193,7 @@ (witness$0 (read$0 data$0 sk_l2_1$0) (sorted_set_c$0 data$0 next$0 lst$0 null$0)) null$0) - (in (read$0 data$0 sk_l2_1$0) + (member (read$0 data$0 sk_l2_1$0) (sorted_set_c$0 data$0 next$0 lst$0 null$0))) (or (and @@ -201,12 +201,12 @@ (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)))) - (in + (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 - (in (read$0 data$0 sk_l2_1$0) + (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)) @@ -215,18 +215,18 @@ (= (witness$0 sk_?e$0 (sorted_set_c$0 data$0 next$0 lst$0 null$0)) null$0) - (in sk_?e$0 (sorted_set_c$0 data$0 next$0 lst$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)))) - (in + (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 (in sk_?e$0 (sorted_set_c$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 @@ -235,30 +235,30 @@ (witness$0 sk_?e_3$0 (sorted_set_c$0 data$0 next$0 lst$0 null$0)) null$0) - (in sk_?e_3$0 (sorted_set_c$0 data$0 next$0 lst$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)))) - (in + (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 (in sk_?e_3$0 (sorted_set_c$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) - (in (read$0 data$0 l1) + (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) - (in (read$0 data$0 l1) + (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)) @@ -269,7 +269,7 @@ (witness$0 (read$0 data$0 curr_2$0) (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)) null$0) - (in (read$0 data$0 curr_2$0) + (member (read$0 data$0 curr_2$0) (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))) (or (and @@ -277,12 +277,12 @@ (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)))) - (in + (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 - (in (read$0 data$0 curr_2$0) + (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)) @@ -292,7 +292,7 @@ (witness$0 (read$0 data$0 prev_2$0) (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)) null$0) - (in (read$0 data$0 prev_2$0) + (member (read$0 data$0 prev_2$0) (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))) (or (and @@ -300,12 +300,12 @@ (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)))) - (in + (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 - (in (read$0 data$0 prev_2$0) + (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)) @@ -315,7 +315,7 @@ (witness$0 (read$0 data$0 sk_l1$0) (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)) null$0) - (in (read$0 data$0 sk_l1$0) + (member (read$0 data$0 sk_l1$0) (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))) (or (and @@ -323,12 +323,12 @@ (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)))) - (in + (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 - (in (read$0 data$0 sk_l1$0) + (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)) @@ -338,7 +338,7 @@ (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) - (in (read$0 data$0 sk_l1_1$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 @@ -346,12 +346,12 @@ (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)))) - (in + (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 - (in (read$0 data$0 sk_l1_1$0) + (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)) @@ -361,7 +361,7 @@ (witness$0 (read$0 data$0 sk_l2$0) (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)) null$0) - (in (read$0 data$0 sk_l2$0) + (member (read$0 data$0 sk_l2$0) (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))) (or (and @@ -369,12 +369,12 @@ (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)))) - (in + (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 - (in (read$0 data$0 sk_l2$0) + (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)) @@ -384,7 +384,7 @@ (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) - (in (read$0 data$0 sk_l2_1$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 @@ -392,12 +392,12 @@ (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)))) - (in + (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 - (in (read$0 data$0 sk_l2_1$0) + (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)) @@ -407,18 +407,18 @@ (witness$0 sk_?e$0 (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)) null$0) - (in sk_?e$0 (sorted_set_c$0 data$0 next$0 curr_2$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)))) - (in + (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 (in sk_?e$0 (sorted_set_c$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 @@ -427,19 +427,19 @@ (witness$0 sk_?e_3$0 (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)) null$0) - (in sk_?e_3$0 (sorted_set_c$0 data$0 next$0 curr_2$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)))) - (in + (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 - (in sk_?e_3$0 + (member sk_?e_3$0 (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))))) :named sorted_set_2_15)) @@ -449,7 +449,7 @@ (witness$0 (read$0 data$0 curr_2$0) (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)) null$0) - (in (read$0 data$0 curr_2$0) + (member (read$0 data$0 curr_2$0) (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))) (or (and @@ -457,12 +457,12 @@ (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)))) - (in + (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 - (in (read$0 data$0 curr_2$0) + (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)) @@ -472,7 +472,7 @@ (witness$0 (read$0 data$0 prev_2$0) (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)) null$0) - (in (read$0 data$0 prev_2$0) + (member (read$0 data$0 prev_2$0) (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))) (or (and @@ -480,12 +480,12 @@ (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)))) - (in + (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 - (in (read$0 data$0 prev_2$0) + (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)) @@ -495,7 +495,7 @@ (witness$0 (read$0 data$0 sk_l1$0) (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)) null$0) - (in (read$0 data$0 sk_l1$0) + (member (read$0 data$0 sk_l1$0) (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))) (or (and @@ -503,12 +503,12 @@ (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)))) - (in + (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 - (in (read$0 data$0 sk_l1$0) + (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)) @@ -518,7 +518,7 @@ (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) - (in (read$0 data$0 sk_l1_1$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 @@ -526,12 +526,12 @@ (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)))) - (in + (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 - (in (read$0 data$0 sk_l1_1$0) + (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)) @@ -541,7 +541,7 @@ (witness$0 (read$0 data$0 sk_l2$0) (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)) null$0) - (in (read$0 data$0 sk_l2$0) + (member (read$0 data$0 sk_l2$0) (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))) (or (and @@ -549,12 +549,12 @@ (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)))) - (in + (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 - (in (read$0 data$0 sk_l2$0) + (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)) @@ -564,7 +564,7 @@ (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) - (in (read$0 data$0 sk_l2_1$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 @@ -572,12 +572,12 @@ (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)))) - (in + (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 - (in (read$0 data$0 sk_l2_1$0) + (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)) @@ -587,18 +587,18 @@ (witness$0 sk_?e$0 (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)) null$0) - (in sk_?e$0 (sorted_set_c$0 data$0 next$0 lst$0 curr_2$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)))) - (in + (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 (in sk_?e$0 (sorted_set_c$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 @@ -607,19 +607,19 @@ (witness$0 sk_?e_3$0 (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)) null$0) - (in sk_?e_3$0 (sorted_set_c$0 data$0 next$0 lst$0 curr_2$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)))) - (in + (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 - (in sk_?e_3$0 (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))))) + (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)) @@ -627,26 +627,26 @@ (assert (! (forall ((l1 Loc)) (or (and (Btwn$0 next$0 lst$0 l1 null$0) - (in l1 (sorted_set_domain$0 data$0 next$0 lst$0 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 - (in l1 + (member l1 (sorted_set_domain$0 data$0 next$0 lst$0 null$0)))))) :named sorted_set_footprint)) -(assert (! (or (in sk_?e_3$0 c2_2$0) - (and (in sk_?e_2$0 sk_FP_1$0) (not (in sk_?e_2$0 FP$0))) - (and (in sk_?e_3$0 (union c1_2$0 c2_2$0)) - (not (in sk_?e_3$0 content$0))) - (and (in sk_?e_3$0 c1_2$0) +(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 - (in sk_?e_3$0 + (member sk_?e_3$0 (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)))) - (and (in sk_?e_3$0 content$0) - (not (in sk_?e_3$0 (union c1_2$0 c2_2$0)))) - (and (in sk_?e_3$0 (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)) - (not (in sk_?e_3$0 c1_2$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)) @@ -685,8 +685,8 @@ (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) (in sk_l1$0 sk_?X_3$0) - (in sk_l2$0 sk_?X_3$0) (not (= sk_l1$0 sk_l2$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)) @@ -694,47 +694,47 @@ (assert (! (forall ((l1 Loc)) (or (and (Btwn$0 next$0 lst$0 l1 curr_2$0) - (in l1 + (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 - (in l1 + (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) - (in l1 + (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 - (in l1 + (member l1 (sorted_set_domain$0 data$0 next$0 curr_2$0 null$0)))))) :named sorted_set_footprint_2)) -(assert (! (not (in null$0 Alloc$0)) :named initial_footprint_of_insert_27_11_1)) +(assert (! (not (member null$0 Alloc$0)) :named initial_footprint_of_insert_27_11_1)) (assert (! (or (= prev_2$0 curr_2$0) - (in sk_?e_1$0 (intersection sk_?X_4$0 sk_?X_3$0)) - (and (in sk_?e_1$0 sk_FP$0) (not (in sk_?e_1$0 FP$0))) - (and (in sk_?e$0 (union c1_2$0 c2_2$0)) (not (in sk_?e$0 content$0))) - (and (in sk_?e$0 c1_2$0) - (not (in sk_?e$0 (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)))) - (and (in sk_?e$0 c2_2$0) - (not (in sk_?e$0 (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)))) - (and (in sk_?e$0 content$0) (not (in sk_?e$0 (union c1_2$0 c2_2$0)))) - (and (in sk_?e$0 (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)) - (not (in sk_?e$0 c1_2$0))) - (and (in sk_?e$0 (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)) - (not (in sk_?e$0 c2_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)) @@ -772,7 +772,7 @@ (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) - (in sk_l1_1$0 sk_?X_5$0) (in sk_l2_1$0 sk_?X_5$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)) 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 index c1c65cea5..c10b14f2b 100644 --- a/test/regress/regress0/sets/jan24/remove_check_free_31_6.smt2 +++ b/test/regress/regress0/sets/jan24/remove_check_free_31_6.smt2 @@ -76,22 +76,22 @@ :named btwn_step_10)) (assert (! (forall ((?f FldLoc)) - (or (in (ep$0 ?f sk_?X_30$0 null$0) sk_?X_30$0) + (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 (in (ep$0 ?f sk_?X_30$0 lst_1$0) sk_?X_30$0) + (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 (in (ep$0 ?f sk_?X_30$0 curr_3$0) sk_?X_30$0) + (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 (in (ep$0 ?f sk_?X_30$0 tmp_2$0) sk_?X_30$0) + (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)) @@ -117,42 +117,42 @@ (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 (in ?y sk_?X_30$0)))) + (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 (in ?y sk_?X_30$0)))) + (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 (in ?y sk_?X_30$0)))) + (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 (in ?y sk_?X_30$0)))) + (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 (in ?y sk_?X_30$0)) - (in (ep$0 ?f sk_?X_30$0 null$0) sk_?X_30$0))) + (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 (in ?y sk_?X_30$0)) - (in (ep$0 ?f sk_?X_30$0 lst_1$0) sk_?X_30$0))) + (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 (in ?y sk_?X_30$0)) - (in (ep$0 ?f sk_?X_30$0 curr_3$0) sk_?X_30$0))) + (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 (in ?y sk_?X_30$0)) - (in (ep$0 ?f sk_?X_30$0 tmp_2$0) sk_?X_30$0))) + (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) @@ -181,28 +181,28 @@ (assert (! (forall ((l1 Loc)) (or (and (Btwn$0 next$0 lst$0 l1 curr_2$0) - (in l1 (lseg_domain$0 next$0 lst$0 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 (in l1 (lseg_domain$0 next$0 lst$0 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) - (in l1 (lseg_domain$0 next$0 curr_3$0 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 (in l1 (lseg_domain$0 next$0 curr_3$0 null$0)))))) + (not (member l1 (lseg_domain$0 next$0 curr_3$0 null$0)))))) :named lseg_footprint_21)) -(assert (! (not (in tmp_2$0 FP_2$0)) :named check_free_31_6)) +(assert (! (not (member tmp_2$0 FP_2$0)) :named check_free_31_6)) -(assert (! (not (in null$0 Alloc$0)) :named framecondition_of_remove_loop_18_4_15)) +(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)) @@ -263,35 +263,35 @@ (assert (! (forall ((l1 Loc)) (or (and (Btwn$0 next$0 lst_1$0 l1 curr_3$0) - (in l1 (lseg_domain$0 next$0 lst_1$0 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 (in l1 (lseg_domain$0 next$0 lst_1$0 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) - (in l1 (lseg_domain$0 next$0 lst$0 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 (in l1 (lseg_domain$0 next$0 lst$0 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) - (in l1 (lseg_domain$0 next$0 curr_2$0 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 (in l1 (lseg_domain$0 next$0 curr_2$0 null$0)))))) + (not (member l1 (lseg_domain$0 next$0 curr_2$0 null$0)))))) :named lseg_footprint_24)) -(assert (! (not (in null$0 Alloc$0)) :named initial_footprint_of_remove_10_11_11)) +(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)) -- cgit v1.2.3