From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Sun, 22 Jun 2014 05:17:27 +0000 (-0400)
Subject: Renaming of SMT2 operator names, kinds for set theory
X-Git-Tag: cvc5-1.0.0~6712^2~8
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b8ddf766460bfcf475e08ff52c889246e78f76cc;p=cvc5.git

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

diff --git a/examples/sets-translate/sets_translate.cpp b/examples/sets-translate/sets_translate.cpp
index e23b7cec2..5257915b0 100644
--- a/examples/sets-translate/sets_translate.cpp
+++ b/examples/sets-translate/sets_translate.cpp
@@ -127,7 +127,7 @@ class Mapper {
              << " ( (x " << elementType << ") )"
              << " " << name << ""
              << " (store emptyset" << elementTypeAsString << " x true) )" << endl;
-      setoperators[ make_pair(t, kind::SET_SINGLETON) ] =
+      setoperators[ make_pair(t, kind::SINGLETON) ] =
         em->mkVar( std::string("setenum") + elementTypeAsString,
                    em->mkFunctionType( elementType, t ) );
 
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 5baa0b16f..a0d759cc2 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -150,8 +150,8 @@ void Smt2::addTheory(Theory theory) {
     addOperator(kind::INTERSECTION, "intersection");
     addOperator(kind::SETMINUS, "setminus");
     addOperator(kind::SUBSET, "subseteq");
-    addOperator(kind::MEMBER, "in");
-    addOperator(kind::SET_SINGLETON, "setenum");
+    addOperator(kind::MEMBER, "member");
+    addOperator(kind::SINGLETON, "singleton");
     break;
 
   case THEORY_DATATYPES:
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 95f35a5a6..dbdc65ba9 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -409,7 +409,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
   case kind::SUBSET:
   case kind::MEMBER:
   case kind::SET_TYPE:
-  case kind::SET_SINGLETON: out << smtKindString(k) << " "; break;
+  case kind::SINGLETON: out << smtKindString(k) << " "; break;
 
    // datatypes
   case kind::APPLY_TYPE_ASCRIPTION: {
@@ -610,9 +610,9 @@ static string smtKindString(Kind k) throw() {
   case kind::INTERSECTION: return "intersection";
   case kind::SETMINUS: return "setminus";
   case kind::SUBSET: return "subseteq";
-  case kind::MEMBER: return "in";
+  case kind::MEMBER: return "member";
   case kind::SET_TYPE: return "Set";
-  case kind::SET_SINGLETON: return "setenum";
+  case kind::SINGLETON: return "singleton";
   default:
     ; /* fall through */
   }
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 9f25b0825..2c309899d 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -74,7 +74,7 @@ unsigned TermDb::getNumGroundTerms( Node f ) {
 Node TermDb::getOperator( Node n ) {
   //return n.getOperator();
   Kind k = n.getKind();
-  if( k==SELECT || k==STORE || k==UNION || k==INTERSECTION || k==SUBSET || k==SETMINUS || k==MEMBER || k==SET_SINGLETON ){
+  if( k==SELECT || k==STORE || k==UNION || k==INTERSECTION || k==SUBSET || k==SETMINUS || k==MEMBER || k==SINGLETON ){
     //since it is parametric, use a particular one as op
     TypeNode tn = n[0].getType();
     Node op = n.getOperator();
diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp
index 77a4efff5..0d8f2c06d 100644
--- a/src/theory/quantifiers/trigger.cpp
+++ b/src/theory/quantifiers/trigger.cpp
@@ -330,7 +330,7 @@ bool Trigger::isAtomicTrigger( Node n ){
 bool Trigger::isAtomicTriggerKind( Kind k ) {
   return k==APPLY_UF || k==SELECT || k==STORE ||
          k==APPLY_CONSTRUCTOR || k==APPLY_SELECTOR_TOTAL || k==APPLY_TESTER ||
-         k==UNION || k==INTERSECTION || k==SUBSET || k==SETMINUS || k==MEMBER || k==SET_SINGLETON;
+         k==UNION || k==INTERSECTION || k==SUBSET || k==SETMINUS || k==MEMBER || k==SINGLETON;
 }
 
 bool Trigger::isSimpleTrigger( Node n ){
diff --git a/src/theory/sets/expr_patterns.h b/src/theory/sets/expr_patterns.h
index bc5b6b9e0..93307d227 100644
--- a/src/theory/sets/expr_patterns.h
+++ b/src/theory/sets/expr_patterns.h
@@ -44,8 +44,8 @@ static Node MEMBER(TNode a, TNode b) {
   return NodeManager::currentNM()->mkNode(kind::MEMBER, a, b);
 }
 
-static Node SET_SINGLETON(TNode a) {
-  return NodeManager::currentNM()->mkNode(kind::SET_SINGLETON, a);
+static Node SINGLETON(TNode a) {
+  return NodeManager::currentNM()->mkNode(kind::SINGLETON, a);
 }
 
 static Node EQUAL(TNode a, TNode b) {
diff --git a/src/theory/sets/kinds b/src/theory/sets/kinds
index 799261634..06d3be5a0 100644
--- a/src/theory/sets/kinds
+++ b/src/theory/sets/kinds
@@ -22,7 +22,7 @@ constant EMPTYSET \
     "the empty set constant; payload is an instance of the CVC4::EmptySet class"
 
 # the type
-operator SET_TYPE 1 "set type"
+operator SET_TYPE 1 "set type, takes as parameter the type of the elements"
 cardinality SET_TYPE \
     "::CVC4::theory::sets::SetsProperties::computeCardinality(%TYPE%)" \
     "theory/sets/theory_sets_type_rules.h"
@@ -40,19 +40,19 @@ operator INTERSECTION  2  "set intersection"
 operator SETMINUS      2  "set subtraction"
 operator SUBSET        2  "subset predicate; first parameter a subset of second"
 operator MEMBER        2  "set membership predicate; first parameter a member of second"
-operator SET_SINGLETON 1  "the set of the single element given as a parameter"
+operator SINGLETON     1  "the set of the single element given as a parameter"
 
 typerule UNION          ::CVC4::theory::sets::SetsBinaryOperatorTypeRule
 typerule INTERSECTION   ::CVC4::theory::sets::SetsBinaryOperatorTypeRule
 typerule SETMINUS       ::CVC4::theory::sets::SetsBinaryOperatorTypeRule
 typerule SUBSET         ::CVC4::theory::sets::SubsetTypeRule
 typerule MEMBER         ::CVC4::theory::sets::MemberTypeRule
-typerule SET_SINGLETON  ::CVC4::theory::sets::SetSingletonTypeRule
+typerule SINGLETON      ::CVC4::theory::sets::SingletonTypeRule
 typerule EMPTYSET       ::CVC4::theory::sets::EmptySetTypeRule
 
 construle UNION         ::CVC4::theory::sets::SetsBinaryOperatorTypeRule
 construle INTERSECTION  ::CVC4::theory::sets::SetsBinaryOperatorTypeRule
 construle SETMINUS      ::CVC4::theory::sets::SetsBinaryOperatorTypeRule
-construle SET_SINGLETON ::CVC4::theory::sets::SetSingletonTypeRule
+construle SINGLETON     ::CVC4::theory::sets::SingletonTypeRule
 
 endtheory
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index f768bd62d..c06f1bd5e 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -225,7 +225,7 @@ void TheorySetsPrivate::assertMemebership(TNode fact, TNode reason, bool learnt)
     if(S.getKind() == kind::UNION ||
        S.getKind() == kind::INTERSECTION ||
        S.getKind() == kind::SETMINUS ||
-       S.getKind() == kind::SET_SINGLETON) {
+       S.getKind() == kind::SINGLETON) {
       doSettermPropagation(x, S);
       if(d_conflict) return;
     }// propagation: children
@@ -276,7 +276,7 @@ void TheorySetsPrivate::doSettermPropagation(TNode x, TNode S)
     left_literal  =       MEMBER(x, S[0])   ;
     right_literal = NOT(  MEMBER(x, S[1])  );
     break;
-  case kind::SET_SINGLETON: {
+  case kind::SINGLETON: {
     Node atom = MEMBER(x, S);
     if(holds(atom, true)) {
       learnLiteral(EQUAL(x, S[0]), true, atom);
@@ -535,9 +535,9 @@ Node TheorySetsPrivate::elementsToShape(Elements elements, TypeNode setType) con
     return nm->mkConst(EmptySet(nm->toType(setType)));
   } else {
     Elements::iterator it = elements.begin();
-    Node cur = SET_SINGLETON(*it);
+    Node cur = SINGLETON(*it);
     while( ++it != elements.end() ) {
-      cur = nm->mkNode(kind::UNION, cur, SET_SINGLETON(*it));
+      cur = nm->mkNode(kind::UNION, cur, SINGLETON(*it));
     }
     return cur;
   }
@@ -948,7 +948,7 @@ void TheorySetsPrivate::preRegisterTerm(TNode node)
     d_equalityEngine.addTriggerTerm(node, THEORY_SETS);
     // d_equalityEngine.addTerm(node);
   }
-  if(node.getKind() == kind::SET_SINGLETON) {
+  if(node.getKind() == kind::SINGLETON) {
     Node true_node = NodeManager::currentNM()->mkConst<bool>(true);
     learnLiteral(MEMBER(node[0], node), true, true_node);
     //intentional fallthrough
@@ -1125,7 +1125,7 @@ void TheorySetsPrivate::TermInfoManager::pushToSettermPropagationQueue
   if(S.getKind() == kind::UNION ||
      S.getKind() == kind::INTERSECTION ||
      S.getKind() == kind::SETMINUS ||
-     S.getKind() == kind::SET_SINGLETON) {
+     S.getKind() == kind::SINGLETON) {
     d_theory.d_settermPropagationQueue.push_back(std::make_pair(x, S));
   }// propagation: children
 
diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp
index 7b02c1bfb..ce469cc0c 100644
--- a/src/theory/sets/theory_sets_rewriter.cpp
+++ b/src/theory/sets/theory_sets_rewriter.cpp
@@ -32,11 +32,11 @@ bool checkConstantMembership(TNode elementTerm, TNode setTerm)
     return false;
   }
 
-  if(setTerm.getKind() == kind::SET_SINGLETON) {
+  if(setTerm.getKind() == kind::SINGLETON) {
     return elementTerm == setTerm[0];
   }
 
-  Assert(setTerm.getKind() == kind::UNION && setTerm[1].getKind() == kind::SET_SINGLETON,
+  Assert(setTerm.getKind() == kind::UNION && setTerm[1].getKind() == kind::SINGLETON,
          "kind was %d, term: %s", setTerm.getKind(), setTerm.toString().c_str());
 
   return elementTerm == setTerm[1][0] || checkConstantMembership(elementTerm, setTerm[0]);
@@ -44,7 +44,7 @@ bool checkConstantMembership(TNode elementTerm, TNode setTerm)
   // switch(setTerm.getKind()) {
   // case kind::EMPTYSET:
   //   return false;
-  // case kind::SET_SINGLETON:
+  // case kind::SINGLETON:
   //   return elementTerm == setTerm[0];
   // case kind::UNION:
   //   return checkConstantMembership(elementTerm, setTerm[0]) ||
@@ -195,7 +195,7 @@ const Elements& collectConstantElements(TNode setterm, SettermElementsMap& sette
       case kind::EMPTYSET:
         /* assign emptyset, which is default */
         break;
-      case kind::SET_SINGLETON:
+      case kind::SINGLETON:
         Assert(setterm[0].isConst());
         cur.insert(TheorySetsRewriter::preRewrite(setterm[0]).node);
         break;
@@ -220,10 +220,10 @@ Node elementsToNormalConstant(Elements elements,
   } else {
 
     Elements::iterator it = elements.begin();
-    Node cur = nm->mkNode(kind::SET_SINGLETON, *it);
+    Node cur = nm->mkNode(kind::SINGLETON, *it);
     while( ++it != elements.end() ) {
       cur = nm->mkNode(kind::UNION, cur,
-                       nm->mkNode(kind::SET_SINGLETON, *it));
+                       nm->mkNode(kind::SINGLETON, *it));
     }
     return cur;
   }
diff --git a/src/theory/sets/theory_sets_type_enumerator.h b/src/theory/sets/theory_sets_type_enumerator.h
index 2f4cc6a2f..97fbfe94f 100644
--- a/src/theory/sets/theory_sets_type_enumerator.h
+++ b/src/theory/sets/theory_sets_type_enumerator.h
@@ -76,7 +76,7 @@ public:
     Assert(d_index == 0 || d_index == 1);
 
     if(d_index == 1) {
-      n = d_nm->mkNode(kind::SET_SINGLETON, *(*(d_constituentVec[0])));
+      n = d_nm->mkNode(kind::SINGLETON, *(*(d_constituentVec[0])));
     }
 
     // for (unsigned i = 0; i < d_indexVec.size(); ++i) {
diff --git a/src/theory/sets/theory_sets_type_rules.h b/src/theory/sets/theory_sets_type_rules.h
index eff81622d..2267ee22a 100644
--- a/src/theory/sets/theory_sets_type_rules.h
+++ b/src/theory/sets/theory_sets_type_rules.h
@@ -107,18 +107,18 @@ struct MemberTypeRule {
   }
 };/* struct MemberTypeRule */
 
-struct SetSingletonTypeRule {
+struct SingletonTypeRule {
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
     throw (TypeCheckingExceptionPrivate, AssertionException) {
-    Assert(n.getKind() == kind::SET_SINGLETON);
+    Assert(n.getKind() == kind::SINGLETON);
     return nodeManager->mkSetType(n[0].getType(check));
   }
 
   inline static bool computeIsConst(NodeManager* nodeManager, TNode n) {
-    Assert(n.getKind() == kind::SET_SINGLETON);
+    Assert(n.getKind() == kind::SINGLETON);
     return n[0].isConst();
   }
-};/* struct SetSingletonTypeRule */
+};/* struct SingletonTypeRule */
 
 struct EmptySetTypeRule {
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
diff --git a/test/regress/regress0/bug567.smt2 b/test/regress/regress0/bug567.smt2
index 265d456b6..109940090 100644
--- a/test/regress/regress0/bug567.smt2
+++ b/test/regress/regress0/bug567.smt2
@@ -27,7 +27,7 @@
 (assert (forall ((l4 List0) (e1 Int)) (! (= (buggySortedIns e1 l4) (ite (is-Nil l4) (Cons e1 Nil) (ite (<= (head0 l4) e1) (Cons (head0 l4) (buggySortedIns e1 (tail0 l4))) (Cons e1 l4)))) :pattern ((buggySortedIns e1 l4)))))
 (assert (forall ((l3 List0) (e Int)) (! (= (sortedIns e l3) (ite (is-Nil l3) (Cons e Nil) (ite (<= (head0 l3) e) (Cons (head0 l3) (sortedIns e (tail0 l3))) (Cons e l3)))) :pattern ((sortedIns e l3)))))
 (assert (forall ((l5 List0)) (! (= (sort l5) (ite (is-Nil l5) Nil (sortedIns (head0 l5) (sort (tail0 l5))))) :pattern ((sort l5)))))
-(assert (forall ((l1 List0)) (! (= (contents l1) (ite (is-Nil l1) (as emptyset (Set Int)) (union (contents (tail0 l1)) (setenum (head0 l1))))) :pattern ((contents l1)))))
+(assert (forall ((l1 List0)) (! (= (contents l1) (ite (is-Nil l1) (as emptyset (Set Int)) (union (contents (tail0 l1)) (singleton (head0 l1))))) :pattern ((contents l1)))))
 
 
 
@@ -42,7 +42,7 @@
 (pop)
 
 (push)
-(assert (forall ((l4 List0) (e1 Int)) (not (let ((result2 (ite (is-Nil l4) (Cons e1 Nil) (ite (<= (head0 l4) e1) (Cons (head0 l4) (buggySortedIns e1 (tail0 l4))) (Cons e1 l4))))) (and (= (contents result2) (union (contents l4) (setenum e1))) (isSorted result2) (= (size result2) (+ (size l4) 1)))))))
+(assert (forall ((l4 List0) (e1 Int)) (not (let ((result2 (ite (is-Nil l4) (Cons e1 Nil) (ite (<= (head0 l4) e1) (Cons (head0 l4) (buggySortedIns e1 (tail0 l4))) (Cons e1 l4))))) (and (= (contents result2) (union (contents l4) (singleton e1))) (isSorted result2) (= (size result2) (+ (size l4) 1)))))))
 (check-sat)
 (pop)
 
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
index 9ba2d84d3..b4ddfec41 100644
--- a/test/regress/regress0/sets/copy_check_heap_access_33_4.smt2
+++ b/test/regress/regress0/sets/copy_check_heap_access_33_4.smt2
@@ -46,15 +46,15 @@
 (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 (in l1 sk_?X_4$0))
-                   (not (in l2 sk_?X_4$0)))))
+                   (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 (in tmp_2$0 Alloc$0)) :named new_31_11))
+(assert (! (not (member tmp_2$0 Alloc$0)) :named new_31_11))
 
-(assert (! (not (in null$0 Alloc$0)) :named initial_footprint_of_copy_23_11_2))
+(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))
 
@@ -67,7 +67,7 @@
 
 (assert (! (= cp_2$0 res_1$0) :named assign_32_4))
 
-(assert (! (= FP_1$0 (union FP$0 (setenum tmp_2$0))) :named assign_31_11))
+(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)))
@@ -76,13 +76,13 @@
 (assert (! (forall ((l1 Loc))
            (or
                (and (Btwn$0 next$0 lst$0 l1 null$0)
-                    (in l1 (slseg_domain$0 data$0 next$0 lst$0 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 (in l1 (slseg_domain$0 data$0 next$0 lst$0 null$0))))))
+                    (not (member l1 (slseg_domain$0 data$0 next$0 lst$0 null$0))))))
    :named slseg_footprint_2))
 
-(assert (! (not (in curr_2$0 FP_1$0)) :named check_heap_access_33_4))
+(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))
 
@@ -99,7 +99,7 @@
 
 (assert (! (= FP_Caller_1$0 (setminus FP_Caller$0 FP$0)) :named assign_26_2_1))
 
-(assert (! (= Alloc_1$0 (union Alloc$0 (setenum tmp_2$0))) :named assign_31_11_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))
 
diff --git a/test/regress/regress0/sets/emptyset.smt2 b/test/regress/regress0/sets/emptyset.smt2
index 47fc25661..2b2322d46 100644
--- a/test/regress/regress0/sets/emptyset.smt2
+++ b/test/regress/regress0/sets/emptyset.smt2
@@ -1,4 +1,4 @@
 (set-logic ALL_SUPPORTED)
 (set-info :status unsat)
-(assert (in 5 (as emptyset (Set Int) )))
+(assert (member 5 (as emptyset (Set Int) )))
 (check-sat)
diff --git a/test/regress/regress0/sets/eqtest.smt2 b/test/regress/regress0/sets/eqtest.smt2
index 02577b00a..cb816a306 100644
--- a/test/regress/regress0/sets/eqtest.smt2
+++ b/test/regress/regress0/sets/eqtest.smt2
@@ -10,8 +10,8 @@
 (declare-fun H () (Set Int) )
 (declare-fun I () (Set Int) )
 (declare-fun x () Int)
-(assert (in x (intersection (union A B) C)))
-(assert (not (in x G)))
+(assert (member x (intersection (union A B) C)))
+(assert (not (member x G)))
 (assert (= (union A B) D))
 (assert (= C (intersection E F)))
 (assert (and (= F H) (= G H) (= H I)))
diff --git a/test/regress/regress0/sets/error2.smt2 b/test/regress/regress0/sets/error2.smt2
index ac678c552..0b8c5ab65 100644
--- a/test/regress/regress0/sets/error2.smt2
+++ b/test/regress/regress0/sets/error2.smt2
@@ -1,4 +1,4 @@
 (set-logic QF_ALL_SUPPORTED)
 (set-info :status unsat)
-(assert (= (as emptyset (Set Int)) (setenum 5)))
+(assert (= (as emptyset (Set Int)) (singleton 5)))
 (check-sat)
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
index 7a8661e4d..87cb9b73d 100644
--- a/test/regress/regress0/sets/feb3/ListElts.hs.fqout.cvc4.317.smt2
+++ b/test/regress/regress0/sets/feb3/ListElts.hs.fqout.cvc4.317.smt2
@@ -4,8 +4,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))
 ;(define-fun smt_set_com ((s mySet)) mySet ((_ map not) s))
diff --git a/test/regress/regress0/sets/fuzz14418.smt2 b/test/regress/regress0/sets/fuzz14418.smt2
index d5a49c601..e7a7be97a 100644
--- a/test/regress/regress0/sets/fuzz14418.smt2
+++ b/test/regress/regress0/sets/fuzz14418.smt2
@@ -36,19 +36,19 @@
 (let ((e16 (f1 e14 v1 v4)))
 (let ((e17 (intersection e16 e15)))
 (let ((e18 (f1 v4 e15 v2)))
-(let ((e19 (ite (p1 e13) (setenum 1) (setenum 0))))
-(let ((e20 (in v0 e17)))
-(let ((e21 (in e7 e16)))
-(let ((e22 (in e10 e16)))
-(let ((e23 (in e8 e17)))
-(let ((e24 (in e9 e14)))
-(let ((e25 (in e8 e16)))
-(let ((e26 (in v0 e13)))
-(let ((e27 (in e12 v4)))
-(let ((e28 (in e8 e14)))
-(let ((e29 (in e8 v1)))
-(let ((e30 (in e10 e13)))
-(let ((e31 (in e7 e13)))
+(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)))
diff --git a/test/regress/regress0/sets/fuzz15201.smt2 b/test/regress/regress0/sets/fuzz15201.smt2
index 8ddeb36d2..650c0ead1 100644
--- a/test/regress/regress0/sets/fuzz15201.smt2
+++ b/test/regress/regress0/sets/fuzz15201.smt2
@@ -33,37 +33,37 @@
 (let ((e20 (intersection e17 e18)))
 (let ((e21 (intersection v1 e16)))
 (let ((e22 (setminus e20 e16)))
-(let ((e23 (ite (p1 v2 e18 e21) (setenum 1) (setenum 0))))
+(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) (setenum 1) (setenum 0))))
+(let ((e27 (ite (p1 e20 e19 e25) (singleton 1) (singleton 0))))
 (let ((e28 (f1 e20)))
-(let ((e29 (in e14 e17)))
-(let ((e30 (in e13 e23)))
-(let ((e31 (in e11 e25)))
-(let ((e32 (in e6 v1)))
-(let ((e33 (in e9 v1)))
-(let ((e34 (in v0 e28)))
-(let ((e35 (in e9 e16)))
-(let ((e36 (in e4 e17)))
-(let ((e37 (in e9 e18)))
-(let ((e38 (in e14 e25)))
-(let ((e39 (in e14 v2)))
-(let ((e40 (in v0 v1)))
-(let ((e41 (in e4 e16)))
-(let ((e42 (in e15 e21)))
-(let ((e43 (in e7 e22)))
-(let ((e44 (in e11 v2)))
-(let ((e45 (in e14 e22)))
-(let ((e46 (in e11 e16)))
-(let ((e47 (in e15 e22)))
-(let ((e48 (in e10 e23)))
-(let ((e49 (in e4 e21)))
-(let ((e50 (in e5 e28)))
-(let ((e51 (in e6 e28)))
-(let ((e52 (in v0 e22)))
-(let ((e53 (in e14 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)))
diff --git a/test/regress/regress0/sets/fuzz31811.smt2 b/test/regress/regress0/sets/fuzz31811.smt2
index 799dda0e2..536d62d3d 100644
--- a/test/regress/regress0/sets/fuzz31811.smt2
+++ b/test/regress/regress0/sets/fuzz31811.smt2
@@ -26,27 +26,27 @@
 (let ((e8 (* e6 (- e5))))
 (let ((e9 (ite (p0 e7 v0 e6) 1 0)))
 (let ((e10 (f0 v0 e8 e8)))
-(let ((e11 (ite (p1 v1) (setenum 1) (setenum 0))))
+(let ((e11 (ite (p1 v1) (singleton 1) (singleton 0))))
 (let ((e12 (union v3 v3)))
 (let ((e13 (intersection v3 v1)))
-(let ((e14 (ite (p1 v3) (setenum 1) (setenum 0))))
+(let ((e14 (ite (p1 v3) (singleton 1) (singleton 0))))
 (let ((e15 (intersection v2 e14)))
-(let ((e16 (ite (p1 e11) (setenum 1) (setenum 0))))
-(let ((e17 (ite (p1 v4) (setenum 1) (setenum 0))))
+(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) (setenum 1) (setenum 0))))
+(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) (setenum 1) (setenum 0))))
+(let ((e26 (ite (p1 e15) (singleton 1) (singleton 0))))
 (let ((e27 (setminus e17 e15)))
 (let ((e28 (f1 e23 e12)))
-(let ((e29 (in e10 e16)))
-(let ((e30 (in e10 v1)))
-(let ((e31 (in e7 e19)))
+(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)))
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))
 
diff --git a/test/regress/regress0/sets/jan27/ListConcat.hs.fqout.cvc4.177.smt2 b/test/regress/regress0/sets/jan27/ListConcat.hs.fqout.cvc4.177.smt2
index 7fea3435e..f055a8e1c 100644
--- a/test/regress/regress0/sets/jan27/ListConcat.hs.fqout.cvc4.177.smt2
+++ b/test/regress/regress0/sets/jan27/ListConcat.hs.fqout.cvc4.177.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))
 ;(define-fun smt_set_com ((s mySet)) mySet ((_ map not) s))
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
index 6c32bb578..81b8794e5 100644
--- a/test/regress/regress0/sets/jan27/ListElem.hs.fqout.cvc4.38.smt2
+++ b/test/regress/regress0/sets/jan27/ListElem.hs.fqout.cvc4.38.smt2
@@ -9,8 +9,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))
 ;(define-fun smt_set_com ((s mySet)) mySet ((_ map not) s))
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
index 0aa6c88ae..8b84c9153 100644
--- a/test/regress/regress0/sets/jan27/deepmeas0.hs.fqout.cvc4.41.smt2
+++ b/test/regress/regress0/sets/jan27/deepmeas0.hs.fqout.cvc4.41.smt2
@@ -4,8 +4,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))
 ;(define-fun smt_set_com ((s mySet)) mySet ((_ map not) s))
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
index d0fda8b86..ac5fdf48d 100644
--- a/test/regress/regress0/sets/jan28/TalkingAboutSets.hs.fqout.cvc4.3577.smt2
+++ b/test/regress/regress0/sets/jan28/TalkingAboutSets.hs.fqout.cvc4.3577.smt2
@@ -4,8 +4,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))
 ;(define-fun smt_set_com ((s mySet)) mySet ((_ map not) s))
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
index f37a8ccfe..e17911327 100644
--- a/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.cvc4.10.smt2
+++ b/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.cvc4.10.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))
 (define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (setminus s1 s2))
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
index 59cc1a00e..bea016683 100644
--- a/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.cvc4.1832.smt2
+++ b/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.cvc4.1832.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))
 ;(define-fun smt_set_com ((s mySet)) mySet ((_ map not) s))
diff --git a/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.minimized10.smt2 b/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.minimized10.smt2
index 5fa5101f0..df659f0fb 100644
--- a/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.minimized10.smt2
+++ b/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.minimized10.smt2
@@ -8,12 +8,12 @@
 ; What was going on?
 ;
 ; The solver was unable to reason that (emptyset) cannot equal
-; (setenum 0). There were no membership predicates anywhere, just
+; (singleton 0). There were no membership predicates anywhere, just
 ; equalities.
 ;
 ; Fix
 ;
-; Add the propagation rule: (true) => (in x (setenum x))
+; Add the propagation rule: (true) => (member x (singleton x))
 
 (declare-fun z3f70 (Int) (Set Int))
 (declare-fun z3v85 () Int)
@@ -21,7 +21,7 @@
 (declare-fun z3v87 () Int)
 (declare-fun z3v90 () Int)
 
-(assert (= (z3f70 z3v90) (union (z3f70 z3v85) (union (as emptyset (Set Int)) (setenum z3v86)))))
+(assert (= (z3f70 z3v90) (union (z3f70 z3v85) (union (as emptyset (Set Int)) (singleton z3v86)))))
 (assert (= (z3f70 z3v90) (z3f70 z3v87)))
 (assert (= (as emptyset (Set Int)) (z3f70 z3v87)))
 (check-sat)
diff --git a/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.minimized1832.smt2 b/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.minimized1832.smt2
index d01b7468e..af67a69a7 100644
--- a/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.minimized1832.smt2
+++ b/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.minimized1832.smt2
@@ -9,10 +9,10 @@
 (declare-fun T () (Set Int))
 (declare-fun x () Int)
 
-(assert (or (not (= S smt_set_emp)) (in x T)))
+(assert (or (not (= S smt_set_emp)) (member x T)))
 
 (assert (= smt_set_emp 
-           (ite (in x T) 
-                (union (union smt_set_emp (setenum x)) S) 
+           (ite (member x T) 
+                (union (union smt_set_emp (singleton x)) S) 
                 S)))
 (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
index e6f187331..9175a8723 100644
--- a/test/regress/regress0/sets/mar2014/UniqueZipper.hs.1030minimized.cvc4.smt2
+++ b/test/regress/regress0/sets/mar2014/UniqueZipper.hs.1030minimized.cvc4.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))
 (define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (setminus s1 s2))
diff --git a/test/regress/regress0/sets/mar2014/UniqueZipper.hs.1030minimized2.cvc4.smt2 b/test/regress/regress0/sets/mar2014/UniqueZipper.hs.1030minimized2.cvc4.smt2
index b8a27b967..81117134c 100644
--- a/test/regress/regress0/sets/mar2014/UniqueZipper.hs.1030minimized2.cvc4.smt2
+++ b/test/regress/regress0/sets/mar2014/UniqueZipper.hs.1030minimized2.cvc4.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))
 (define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (setminus s1 s2))
diff --git a/test/regress/regress0/sets/mar2014/lemmabug-ListElts317minimized.smt2 b/test/regress/regress0/sets/mar2014/lemmabug-ListElts317minimized.smt2
index 1ea3ea6b5..1e848695d 100644
--- a/test/regress/regress0/sets/mar2014/lemmabug-ListElts317minimized.smt2
+++ b/test/regress/regress0/sets/mar2014/lemmabug-ListElts317minimized.smt2
@@ -1,7 +1,7 @@
 ; EXPECT: sat
 
 ; Observed behavior:
-;   --check-model failed for set-term (union (z3f69 z3v151) (setenum z3v143))
+;   --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.
 ;
@@ -24,8 +24,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))
 ;(define-fun smt_set_com ((s mySet)) mySet ((_ map not) s))
@@ -69,16 +69,16 @@
                         (z3f69 z3v140))))
 
 (assert (= (z3f69 z3v152)
-           (smt_set_cup (setenum z3v143) (z3f69 z3v151))))
+           (smt_set_cup (singleton z3v143) (z3f69 z3v151))))
 
 (assert (= (z3f70 z3v152)
-           (smt_set_cup (setenum z3v143) (z3f70 z3v151))))
+           (smt_set_cup (singleton z3v143) (z3f70 z3v151))))
 
 (assert (and
         (= (z3f69 z3v142)
-           (smt_set_cup (setenum z3v143) (z3f69 z3v141)))
+           (smt_set_cup (singleton z3v143) (z3f69 z3v141)))
         (= (z3f70 z3v142)
-           (smt_set_cup (setenum z3v143) (z3f70 z3v141)))
+           (smt_set_cup (singleton z3v143) (z3f70 z3v141)))
          (= z3v142 (z3f92 z3v143 z3v141))
          (= z3v142 z3v144)
          (= (z3f62 z3v61) z3v61)
diff --git a/test/regress/regress0/sets/mar2014/sharing-preregister.smt2 b/test/regress/regress0/sets/mar2014/sharing-preregister.smt2
index dc42abfa2..61af2124d 100644
--- a/test/regress/regress0/sets/mar2014/sharing-preregister.smt2
+++ b/test/regress/regress0/sets/mar2014/sharing-preregister.smt2
@@ -5,8 +5,8 @@
 (declare-fun b () Int)
 (declare-fun x () (Set Int))
 (declare-fun y () (Set Int))
-(assert (= x (setenum a)))
-(assert (= y (setenum b)))
+(assert (= x (singleton a)))
+(assert (= y (singleton b)))
 (assert (not (= x y)))
 (assert (and (< 1 a) (< a 3) (< 1 b) (< b 3)))
 (check-sat)
diff --git a/test/regress/regress0/sets/mar2014/small.smt2 b/test/regress/regress0/sets/mar2014/small.smt2
index 838a27919..896b13219 100644
--- a/test/regress/regress0/sets/mar2014/small.smt2
+++ b/test/regress/regress0/sets/mar2014/small.smt2
@@ -10,9 +10,9 @@
 (declare-fun z () Int)
 (declare-fun a () (Set Int))
 (declare-fun b () (Set Int))
-(assert (in x (union a b)))
-(assert (not (in y a)))
-(assert (not (in z b)))
+(assert (member x (union a b)))
+(assert (not (member y a)))
+(assert (not (member z b)))
 (assert (= z y))
 (assert (= x y))
 (check-sat)
diff --git a/test/regress/regress0/sets/mar2014/smaller.smt2 b/test/regress/regress0/sets/mar2014/smaller.smt2
index 876311de8..22e029b69 100644
--- a/test/regress/regress0/sets/mar2014/smaller.smt2
+++ b/test/regress/regress0/sets/mar2014/smaller.smt2
@@ -9,7 +9,7 @@
 (declare-fun y () Int)
 (declare-fun a () (Set Int))
 (declare-fun b () (Set Int))
-(assert (in x (union a b)))
-(assert (not (in y a)))
+(assert (member x (union a b)))
+(assert (not (member y a)))
 (assert (= x y))
 (check-sat)
diff --git a/test/regress/regress0/sets/rec_copy_loop_check_heap_access_43_4.smt2 b/test/regress/regress0/sets/rec_copy_loop_check_heap_access_43_4.smt2
index 57d5d72ca..e5defb2ac 100644
--- a/test/regress/regress0/sets/rec_copy_loop_check_heap_access_43_4.smt2
+++ b/test/regress/regress0/sets/rec_copy_loop_check_heap_access_43_4.smt2
@@ -45,15 +45,15 @@
 (assert (! (forall ((l1 Loc))
            (or
                (and (Btwn$0 next$0 curr$0 l1 null$0)
-                    (in l1 (lseg_domain$0 next$0 curr$0 null$0))
+                    (member l1 (lseg_domain$0 next$0 curr$0 null$0))
                     (not (= l1 null$0)))
                (and (or (= l1 null$0) (not (Btwn$0 next$0 curr$0 l1 null$0)))
-                    (not (in l1 (lseg_domain$0 next$0 curr$0 null$0))))))
+                    (not (member l1 (lseg_domain$0 next$0 curr$0 null$0))))))
    :named lseg_footprint_14))
 
-(assert (! (not (in tmp_1$0 Alloc$0)) :named new_42_10))
+(assert (! (not (member tmp_1$0 Alloc$0)) :named new_42_10))
 
-(assert (! (not (in null$0 Alloc$0))
+(assert (! (not (member null$0 Alloc$0))
    :named initial_footprint_of_rec_copy_loop_34_11_4))
 
 (assert (! (not (= curr$0 null$0)) :named if_else_37_6))
@@ -73,7 +73,7 @@
 
 (assert (! (= FP_Caller_2$0 (setminus FP_Caller$0 FP$0)) :named assign_37_2_2))
 
-(assert (! (= Alloc_2$0 (union Alloc$0 (setenum tmp_1$0))) :named assign_42_10))
+(assert (! (= Alloc_2$0 (union Alloc$0 (singleton tmp_1$0))) :named assign_42_10))
 
 (assert (! (or (Btwn$0 next$0 cp$0 null$0 null$0)
        (not (lseg_struct$0 sk_?X_38$0 next$0 cp$0 null$0)))
@@ -82,13 +82,13 @@
 (assert (! (forall ((l1 Loc))
            (or
                (and (Btwn$0 next$0 cp$0 l1 null$0)
-                    (in l1 (lseg_domain$0 next$0 cp$0 null$0))
+                    (member l1 (lseg_domain$0 next$0 cp$0 null$0))
                     (not (= l1 null$0)))
                (and (or (= l1 null$0) (not (Btwn$0 next$0 cp$0 l1 null$0)))
-                    (not (in l1 (lseg_domain$0 next$0 cp$0 null$0))))))
+                    (not (member l1 (lseg_domain$0 next$0 cp$0 null$0))))))
    :named lseg_footprint_15))
 
-(assert (! (not (in cp_1$0 FP_3$0)) :named check_heap_access_43_4))
+(assert (! (not (member cp_1$0 FP_3$0)) :named check_heap_access_43_4))
 
 (assert (! (not (= tmp_1$0 null$0)) :named new_42_10_1))
 
@@ -109,7 +109,7 @@
 
 (assert (! (= cp_1$0 tmp_1$0) :named assign_42_4))
 
-(assert (! (= FP_3$0 (union FP$0 (setenum tmp_1$0))) :named assign_42_10_1))
+(assert (! (= FP_3$0 (union FP$0 (singleton tmp_1$0))) :named assign_42_10_1))
 
 (assert (! (or (Btwn$0 next$0 curr$0 null$0 null$0)
        (not (lseg_struct$0 sk_?X_37$0 next$0 curr$0 null$0)))
diff --git a/test/regress/regress0/sets/setel-eq.smt2 b/test/regress/regress0/sets/setel-eq.smt2
index 8ed9a2e57..b5d85c7e8 100644
--- a/test/regress/regress0/sets/setel-eq.smt2
+++ b/test/regress/regress0/sets/setel-eq.smt2
@@ -4,7 +4,7 @@
 (declare-fun T () (Set Int))
 (declare-fun x () Int)
 (declare-fun y () Int)
-(assert (in y S))
-(assert (not (in x (union S T))))
+(assert (member y S))
+(assert (not (member x (union S T))))
 (assert (= x y))
 (check-sat)
diff --git a/test/regress/regress0/sets/setofsets-disequal.smt2 b/test/regress/regress0/sets/setofsets-disequal.smt2
index 907e074fe..18ad053d6 100644
--- a/test/regress/regress0/sets/setofsets-disequal.smt2
+++ b/test/regress/regress0/sets/setofsets-disequal.smt2
@@ -11,52 +11,52 @@
 (assert (not (= S (as emptyset myset))))
 
 ; 1 element is S
-(assert (not (= S (setenum (as emptyset (Set (_ BitVec 1)))))))
-(assert (not (= S (setenum (setenum (_ bv0 1)) ))))
-(assert (not (= S (setenum (setenum (_ bv1 1)) ))))
-(assert (not (= S (setenum (union (setenum (_ bv0 1))
-                                  (setenum (_ bv1 1)))))))
+(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 (setenum (as emptyset (Set (_ BitVec 1))))
-                         (setenum (setenum (_ bv0 1)))) )))
-(assert (not (= S (union (setenum (as emptyset (Set (_ BitVec 1))))
-                         (setenum (setenum (_ bv1 1)))))))
-(assert (not (= S (union (setenum (as emptyset (Set (_ BitVec 1))))
-                         (setenum (union (setenum (_ bv0 1))
-                                         (setenum (_ bv1 1))))))))
-(assert (not (= S (union (setenum (union (setenum (_ bv0 1))
-                                         (setenum (_ bv1 1))))
-                         (setenum (setenum (_ bv0 1)))) )))
-(assert (not (= S (union (setenum (setenum (_ bv0 1)))
-                         (setenum (setenum (_ bv1 1))))   )))
-(assert (not (= S (union (setenum (union (setenum (_ bv0 1))
-                                         (setenum (_ bv1 1))))
-                         (setenum (setenum (_ bv1 1)))))))
+(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 (setenum (setenum (_ bv1 1)))
-                         (union (setenum (as emptyset (Set (_ BitVec 1))))
-                                (setenum (setenum (_ bv0 1)))))  )))
-(assert (not (= S (union (setenum (union (setenum (_ bv0 1))
-                                         (setenum (_ bv1 1))))
-                         (union (setenum (as emptyset (Set (_ BitVec 1))))
-                                (setenum (setenum (_ bv1 1)))))  )))
-(assert (not (= S (union (setenum (union (setenum (_ bv0 1))
-                                         (setenum (_ bv1 1))))
-                         (union (setenum (setenum (_ bv0 1)))
-                                (setenum (setenum (_ bv1 1)))))  )))
-(assert (not (= S (union (setenum (union (setenum (_ bv0 1))
-                                         (setenum (_ bv1 1))))
-                         (union (setenum (as emptyset (Set (_ BitVec 1))))
-                                (setenum (setenum (_ bv0 1)))))  )))
+(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 (setenum (union (setenum (_ bv0 1))
-                                         (setenum (_ bv1 1))))
-                         (union (setenum (setenum (_ bv1 1)))
-                                (union (setenum (as emptyset (Set (_ BitVec 1))))
-                                       (setenum (setenum (_ bv0 1))))))  )))
+(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)
 
diff --git a/test/regress/regress0/sets/sets-equal.smt2 b/test/regress/regress0/sets/sets-equal.smt2
index a2ce4b3c2..8fd29a244 100644
--- a/test/regress/regress0/sets/sets-equal.smt2
+++ b/test/regress/regress0/sets/sets-equal.smt2
@@ -6,9 +6,9 @@
 (assert (= x y))
 (declare-fun a () (Set Int))
 (declare-fun b () (Set Int))
-(assert (not (in x a)))
-(assert (in y (union a b)))
+(assert (not (member x a)))
+(assert (member y (union a b)))
 (assert (= x z))
-(assert (not (in z a)))
+(assert (not (member z a)))
 (assert (= a b))
 (check-sat)
diff --git a/test/regress/regress0/sets/sets-inter.smt2 b/test/regress/regress0/sets/sets-inter.smt2
index 0f5e41864..d3d8a9044 100644
--- a/test/regress/regress0/sets/sets-inter.smt2
+++ b/test/regress/regress0/sets/sets-inter.smt2
@@ -4,8 +4,8 @@
 (declare-fun a () (Set Int))
 (declare-fun b () (Set Int))
 (declare-fun x () Int)
-;(assert (not (in x a)))
-(assert (in x (intersection a b)))
-(assert (not (in x b)))
+;(assert (not (member x a)))
+(assert (member x (intersection a b)))
+(assert (not (member x b)))
 (check-sat)
 (exit)
diff --git a/test/regress/regress0/sets/sets-new.smt2 b/test/regress/regress0/sets/sets-new.smt2
index accb09799..0f43ee10d 100644
--- a/test/regress/regress0/sets/sets-new.smt2
+++ b/test/regress/regress0/sets/sets-new.smt2
@@ -6,11 +6,11 @@
 (declare-fun A () SetInt)
 (declare-fun B () SetInt)
 (declare-fun x () Int)
-(assert (in x (union A B)))
+(assert (member x (union A B)))
 
-(assert (not (in x (intersection A B))))
-(assert (not (in x (setminus A B))))
-;(assert (not (in x (setminus B A))))
-;(assert (in x B))
+(assert (not (member x (intersection A B))))
+(assert (not (member x (setminus A B))))
+;(assert (not (member x (setminus B A))))
+;(assert (member x B))
 
 (check-sat)
diff --git a/test/regress/regress0/sets/sets-sample.smt2 b/test/regress/regress0/sets/sets-sample.smt2
index 1bd0eb396..4838c6cf2 100644
--- a/test/regress/regress0/sets/sets-sample.smt2
+++ b/test/regress/regress0/sets/sets-sample.smt2
@@ -12,14 +12,14 @@
 (declare-fun b () (Set Int))
 (declare-fun c () (Set Int))
 (declare-fun e () Int)
-(assert (= a (setenum 5)))
+(assert (= a (singleton 5)))
 (assert (= c (union a b) ))
 (assert (not (= c (intersection a b) )))
 (assert (= c (setminus a b) ))
 (assert (subseteq a b))
-(assert (in e c))
-(assert (in e a))
-(assert (in e (intersection a b)))
+(assert (member e c))
+(assert (member e a))
+(assert (member e (intersection a b)))
 (check-sat)
 (pop 1)
 
@@ -41,8 +41,8 @@
 (declare-fun e2 () Int)
 (assert (= x y))
 (assert (= e1 e2))
-(assert (in e1 x))
-(assert (not (in e2 y)))
+(assert (member e1 x))
+(assert (not (member e2 y)))
 (check-sat)
 (pop 1)
 
@@ -55,8 +55,8 @@
 (declare-fun e2 () Int)
 (assert (= x y))
 (assert (= e1 e2))
-(assert (in e1 (union x z)))
-(assert (not (in e2 (union y z))))
+(assert (member e1 (union x z)))
+(assert (not (member e2 (union y z))))
 (check-sat)
 (pop 1)
  
diff --git a/test/regress/regress0/sets/sets-sharing.smt2 b/test/regress/regress0/sets/sets-sharing.smt2
index d2a94fdf4..caada9606 100644
--- a/test/regress/regress0/sets/sets-sharing.smt2
+++ b/test/regress/regress0/sets/sets-sharing.smt2
@@ -4,8 +4,8 @@
 (declare-fun S () (Set Int))
 (declare-fun x () Int)
 
-(assert (in (+ 5 x) S))
-(assert (not (in 9 S)))
+(assert (member (+ 5 x) S))
+(assert (not (member 9 S)))
 (assert (= x 4))
 
 (check-sat)
diff --git a/test/regress/regress0/sets/sets-union.smt2 b/test/regress/regress0/sets/sets-union.smt2
index 656a0bc88..56ba520dc 100644
--- a/test/regress/regress0/sets/sets-union.smt2
+++ b/test/regress/regress0/sets/sets-union.smt2
@@ -6,10 +6,10 @@
 (declare-fun a () (Set Int))
 (declare-fun b () (Set Int))
 (declare-fun x () Int)
-(assert (not (in x a)))
-(assert (in x (union a b)))
+(assert (not (member x a)))
+(assert (member x (union a b)))
 (check-sat)
 ;(get-model)
-(assert (not (in x b)))
+(assert (not (member x b)))
 (check-sat)
 (exit)
diff --git a/test/regress/regress0/sets/sharingbug.smt2 b/test/regress/regress0/sets/sharingbug.smt2
index b2b61f739..b388bb534 100644
--- a/test/regress/regress0/sets/sharingbug.smt2
+++ b/test/regress/regress0/sets/sharingbug.smt2
@@ -23,9 +23,9 @@
 (let ((e12 (* (- e4) e7)))
 (let ((e13 (- e10)))
 (let ((e14 (f0 e5 e7 e6)))
-(let ((e15 (in v0 v1)))
-(let ((e16 (in e12 v2)))
-(let ((e17 (in e14 v1)))
+(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)))
diff --git a/test/regress/regress0/sets/union-1a-flip.smt2 b/test/regress/regress0/sets/union-1a-flip.smt2
index 7bbe442e1..6a73c5b91 100644
--- a/test/regress/regress0/sets/union-1a-flip.smt2
+++ b/test/regress/regress0/sets/union-1a-flip.smt2
@@ -8,9 +8,9 @@
 (declare-fun A () (Set Int))
 (declare-fun B () (Set Int))
 (declare-fun x () Int)
-(assert (in x A))
+(assert (member x A))
 (push 1)
-(assert (not (in x (union A B))))
+(assert (not (member x (union A B))))
 (check-sat)
 (pop 1)
 (check-sat)
diff --git a/test/regress/regress0/sets/union-1a.smt2 b/test/regress/regress0/sets/union-1a.smt2
index b594ac74d..8636cb220 100644
--- a/test/regress/regress0/sets/union-1a.smt2
+++ b/test/regress/regress0/sets/union-1a.smt2
@@ -8,9 +8,9 @@
 (declare-fun A () (Set Int))
 (declare-fun B () (Set Int))
 (declare-fun x () Int)
-(assert (not (in x (union A B))))
+(assert (not (member x (union A B))))
 (push 1)
-(assert (in x A))
+(assert (member x A))
 (check-sat)
 (pop 1)
 (check-sat)
diff --git a/test/regress/regress0/sets/union-1b-flip.smt2 b/test/regress/regress0/sets/union-1b-flip.smt2
index 72c544553..e2b19b31a 100644
--- a/test/regress/regress0/sets/union-1b-flip.smt2
+++ b/test/regress/regress0/sets/union-1b-flip.smt2
@@ -8,9 +8,9 @@
 (declare-fun A () (Set Int))
 (declare-fun B () (Set Int))
 (declare-fun x () Int)
-(assert (in x B))
+(assert (member x B))
 (push 1)
-(assert (not (in x (union A B))))
+(assert (not (member x (union A B))))
 (check-sat)
 (pop 1)
 (check-sat)
diff --git a/test/regress/regress0/sets/union-1b.smt2 b/test/regress/regress0/sets/union-1b.smt2
index 85fce759c..c354923c9 100644
--- a/test/regress/regress0/sets/union-1b.smt2
+++ b/test/regress/regress0/sets/union-1b.smt2
@@ -8,9 +8,9 @@
 (declare-fun A () (Set Int))
 (declare-fun B () (Set Int))
 (declare-fun x () Int)
-(assert (not (in x (union A B))))
+(assert (not (member x (union A B))))
 (push 1)
-(assert (in x B))
+(assert (member x B))
 (check-sat)
 (pop 1)
 (check-sat)
diff --git a/test/regress/regress0/sets/union-2.smt2 b/test/regress/regress0/sets/union-2.smt2
index e5e96be5a..6e2933975 100644
--- a/test/regress/regress0/sets/union-2.smt2
+++ b/test/regress/regress0/sets/union-2.smt2
@@ -6,7 +6,7 @@
 (declare-fun B () (Set Int))
 (declare-fun x () Int)
 (declare-fun y () Int)
-(assert (in x (union A B)))
-(assert (not (in y A)))
-(assert (not (in y B)))
+(assert (member x (union A B)))
+(assert (not (member y A)))
+(assert (not (member y B)))
 (check-sat)