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".

4 files changed, 143 insertions, 143 deletions

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))