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 e23b7cec25d4b3a3a8006c1b78ab678934c398ac..5257915b035790e75f50277f2b0815be968ace02 100644 (file)
--- 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 5baa0b16f83f71e509640efe5b32b6df96327c9b..a0d759cc2f80f428e32b701731fa12f959cfb73c 100644 (file)
--- 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 95f35a5a6838eff832fe438f0a56cfeeccaff36b..dbdc65ba95c47e12bdcba6510a07d10acfd4da1a 100644 (file)
--- 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 9f25b08257b804b12b99f3570e67e3066ace4083..2c309899d0475c48f650bbfa095c6acf49ef06f1 100644 (file)
--- 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 77a4efff5855128a26defdd8b65e6446f2a6f4e3..0d8f2c06d05cb0b26f5f1ac91291d21d9a4ca058 100644 (file)
--- 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 bc5b6b9e002931ab6136ee3a485c13546e78f8d9..93307d227d4c119ba00ff695a945afb0583ac334 100644 (file)
--- 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 799261634f39757654b6c3b47e1088a3c40ecf90..06d3be5a0e175ca7d61570630bb76e914518d593 100644 (file)
--- 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 f768bd62d6e8e5d116dd02c19186136a28a1699a..c06f1bd5ea5fa0fe9946f7003afedd21c27fb281 100644 (file)
--- 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 7b02c1bfbd17b5111c47d3659664b45201c07e31..ce469cc0c9faac96ea0c399bb6f7acef3987c258 100644 (file)
--- 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 2f4cc6a2f72f245c2daca3a1c21ca6c3456daba1..97fbfe94f8925ec7be6e944f7269e5a5484cee94 100644 (file)
--- 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 eff81622dd5470c2c0b9e19232dff16711fd36c0..2267ee22a035b5dd53a5d7bba6620d7f1dffc2e9 100644 (file)
--- 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 265d456b6b99729253ca15902e77e1d675e94186..109940090e3e0c386b14cfd881e995275e7c359f 100644 (file)
--- 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 9ba2d84d30c0e06e373073ab3d7e3f7a08ea89c1..b4ddfec41e29623a258710575a07829fc9d8c469 100644 (file)
--- 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 47fc256611b9afc48858b8fe5254cf35491347b0..2b2322d46a9df1b68bd4db40104e2b923b83893c 100644 (file)
--- 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 02577b00a6d1376dcf6501c09213440f78520251..cb816a3061123d0909aa16c726d264b1699d4f96 100644 (file)
--- 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 ac678c552c792d10d1308de622263d8ce761799c..0b8c5ab6587c4a790f8a57448fa85f31d416345c 100644 (file)
--- 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 7a8661e4d4337a928de07bac6613db7b9a5cd619..87cb9b73d90c98e3c9d1454c1535e5e94f6d5570 100644 (file)
--- 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 d5a49c601d84f73c9fe48ce6be5166f0cc0bb4e5..e7a7be97ac872ae2cea300982050061eb2cd1de6 100644 (file)
--- 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 8ddeb36d2bb1774a4ffe728dc688568a3924d87c..650c0ead16ae1fc53da8099f7a29adf87359579a 100644 (file)
--- 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 799dda0e2a05b4e8bdb2b9ff0144d2fe9b03b411..536d62d3d3a1823294fb46e2e320654fb6b35526 100644 (file)
--- 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 b90563199ee731dfe12c9e9d962a36715c482e70..bc919673dd76cf68b63be0b413154679b775b3fb 100644 (file)
--- 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 204af2f2d284103c3b5128623e7a6bd839189bb1..6523076451338ac48ff87c22f8e9e34c710b14fe 100644 (file)
--- 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 ad0a7e46426d71a1cf638be2950ccace5af59d4a..4a588aeb6e8330c9ddfc8e72595192cbe33d7489 100644 (file)
--- 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 c1c65cea56853c8a0e5c61a25186fbfccc702a84..c10b14f2b14aff137df272840d47c119141c98e7 100644 (file)
--- 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 7fea3435ea011eb603f351cbb3911250112ba715..f055a8e1c7c7c48a096de1f99af1a8bd2f8b6756 100644 (file)
--- 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 6c32bb5780d34da5dafd360dbc0304c27fc0a818..81b8794e5ea63612c837ad0171cacc99986ba584 100644 (file)
--- 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 0aa6c88ae5c562fc0fccf22e74790bc066b621b4..8b84c9153a03da1db42d8fda90b1ca87dd4b202a 100644 (file)
--- 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 d0fda8b869685f866e7fbe365d6c2cb1bab5d59d..ac5fdf48da98a0d12ce526f44de9d4afd8239a71 100644 (file)
--- 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 f37a8ccfe1fc83a79062d22097fda648b2472baa..e17911327ab573ff61e4c88ef35afbef70bbd287 100644 (file)
--- 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 59cc1a00e920efdd9300f400947c3b0f7cd6ea94..bea016683e777daad795b0506ecf9adfc41e6fda 100644 (file)
--- 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 5fa5101f015fb35196b08e89c89b3553b5534ab7..df659f0fbb64ca35d7b7d0adf88c70e2c6eee138 100644 (file)
--- 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 d01b7468efad998c9693385eb7cf77a5f31a32bc..af67a69a72a11b3ea363a0dc4e426c5f435ee55b 100644 (file)
--- 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 e6f1873318b63f511e1063c312f7b0b3050d2b82..9175a87234d38904736c11a53e931e0e0aca31ba 100644 (file)
--- 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 b8a27b967c5070dbf677ce6ee532525a717a9d5b..81117134c163d2cedb8827cf89bd537343b2c608 100644 (file)
--- 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 1ea3ea6b5b836b47e6528dec056769eb6a78bdf9..1e848695d367c664f708ee78fb2ef022afab8775 100644 (file)
--- 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 dc42abfa23a04828cc5d6571c1de9cec2ebc03a1..61af2124d54154c44fd14c7c697f7c1bb22fa5a0 100644 (file)
--- 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 838a279198b671555cdcdd5ddf6c2f4540f967f6..896b13219c0cb2ff601628bd9a6fa3b7853b84e4 100644 (file)
--- 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 876311de85fa7749a0f88d0fb9307a0041485189..22e029b69ddf3654d8bb647448748977bf12dd19 100644 (file)
--- 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 57d5d72ca3339f1e8a4b4a2fbe05d02dad1c5564..e5defb2accf21915f748085f0ca52efc23cb1469 100644 (file)
--- 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 8ed9a2e57fa81817a66c1a7c2a513045c7b09e39..b5d85c7e8f24705d8b1bc354ba563eaca5198013 100644 (file)
--- 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 907e074fe85ebd5b6a47dac9cfd89a373361df94..18ad053d6234213ffccd29bc018fef7d01fc456d 100644 (file)
--- 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 a2ce4b3c28bcec2056343611f7ab9e11a9994586..8fd29a244f9e7b730f017f1d4f8202f1d580e592 100644 (file)
--- 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 0f5e41864d55ca48b926fd7b05deb3dc128377e4..d3d8a90448b1b8b4bbb0147c0c92586bd30ba214 100644 (file)
--- 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 accb09799532282a02158a794158c2aaecf0838c..0f43ee10dfcba739963a5b110215918ce23d4000 100644 (file)
--- 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 1bd0eb396237e8972ac85332640bdac26e8f6a8c..4838c6cf283c430f7750e060c7f591c23c6d21f3 100644 (file)
--- 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 d2a94fdf452bde38d8733b9eaa42f0ac145ddf75..caada960631b8506599dffe3f5af313c3e9bcee2 100644 (file)
--- 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 656a0bc88d0bd5095f3dda6647c707888a0f9c0a..56ba520dca839fc7a9c15e7a502714efb7ac30a7 100644 (file)
--- 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 b2b61f739d457ee5cd3331589bd224ed50557a46..b388bb534dbd2bedc30ba44da1d95f6aa8e86af4 100644 (file)
--- 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 7bbe442e185f8ba3e9253d57df7590cfc5bc003b..6a73c5b91497cd8953030bb309ba7039fc524591 100644 (file)
--- 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 b594ac74de1f5655bca8a1fbc28c51fbe8cb707b..8636cb22041cf7f20309d9f76ea1f6e96e43b03b 100644 (file)
--- 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 72c5445532c6b5bc5fc088011961cbb5aefc200b..e2b19b31a066db52e2dd2cd08f45584907507952 100644 (file)
--- 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 85fce759c3de1518ccd1e466cdb6a5c99f6937a2..c354923c944a5479c640ad0f608e6a4414fd0d7f 100644 (file)
--- 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 e5e96be5ac95b414b6fbe54a9e059111ddd8ee83..6e293397520f180042a2a41fcc9f7442ea7f3577 100644 (file)
--- 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)