add new theory (sets)

Specification (smt2) -- as per this commit, subject to change

- Parameterized sort Set, e.g. (Set Int)

- Empty set constant (typed), use with "as" to specify the type, e.g.
    (as emptyset (Set Int))

- Create a singleton set
    (setenum X (Set X)) : creates singleton set

- Functions/operators
    (union (Set X) (Set X) (Set X))
    (intersection (Set X) (Set X) (Set X))
    (setminus (Set X) (Set X) (Set X))

- Predicates
    (in X (Set X) Bool) : membership
    (subseteq (Set X) (Set X) Bool) : set containment

78 files changed, 5216 insertions, 98 deletions

diff --git a/.gitignore b/.gitignore
index 741f08ccd..b3cce03ed 100644
--- a/.gitignore
+++ b/.gitignore
@@ -30,3 +30,4 @@ config.reconfig
 /debug/
 /personal.conf
 /personal.mk
+/antlr-3.4
diff --git a/src/Makefile.am b/src/Makefile.am
index f20fabf6b..86067d3ef 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -20,7 +20,7 @@ AM_CPPFLAGS = \
 AM_CXXFLAGS = -Wall -Wno-unknown-pragmas -Wno-parentheses $(FLAG_VISIBILITY_HIDDEN)
 
 SUBDIRS = lib options expr util prop/minisat prop/bvminisat . parser compat bindings main
-THEORIES = builtin booleans uf arith bv arrays datatypes strings quantifiers rewriterules idl
+THEORIES = builtin booleans uf arith bv arrays datatypes sets strings quantifiers rewriterules idl
 
 lib_LTLIBRARIES = libcvc4.la
 
@@ -220,6 +220,13 @@ libcvc4_la_SOURCES = \
 	theory/datatypes/theory_datatypes.h \
 	theory/datatypes/datatypes_rewriter.h \
 	theory/datatypes/theory_datatypes.cpp \
+	theory/sets/theory_sets.h \
+	theory/sets/theory_sets.cpp \
+	theory/sets/theory_sets_private.h \
+	theory/sets/theory_sets_private.cpp \
+	theory/sets/theory_sets_rewriter.h \
+	theory/sets/theory_sets_rewriter.cpp \
+	theory/sets/theory_sets_type_rules.h \
 	theory/strings/theory_strings.h \
 	theory/strings/theory_strings.cpp \
 	theory/strings/theory_strings_rewriter.h \
@@ -453,6 +460,7 @@ EXTRA_DIST = \
 	theory/idl/kinds \
 	theory/builtin/kinds \
 	theory/datatypes/kinds \
+	theory/sets/kinds \
 	theory/strings/kinds \
 	theory/arrays/kinds \
 	theory/quantifiers/kinds \
diff --git a/src/context/cdhashset.h b/src/context/cdhashset.h
index e2ffac49b..881c3f629 100644
--- a/src/context/cdhashset.h
+++ b/src/context/cdhashset.h
@@ -57,6 +57,10 @@ public:
     return super::size();
   }
 
+  bool empty() const {
+    return super::empty();
+  }
+
   bool insert(const V& v) {
     return super::insert_safe(v, true);
   }
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 5fe7b34c1..41f69e587 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -540,6 +540,11 @@ ArrayType ExprManager::mkArrayType(Type indexType, Type constituentType) const {
   return ArrayType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkArrayType(*indexType.d_typeNode, *constituentType.d_typeNode))));
 }
 
+SetType ExprManager::mkSetType(Type elementType) const {
+  NodeManagerScope nms(d_nodeManager);
+  return SetType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkSetType(*elementType.d_typeNode))));
+}
+
 DatatypeType ExprManager::mkDatatypeType(const Datatype& datatype) {
   // Not worth a special implementation; this doesn't need to be fast
   // code anyway.
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index 3f0ec2f9c..f5e01d545 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -376,6 +376,9 @@ public:
   /** Make the type of arrays with the given parameterization. */
   ArrayType mkArrayType(Type indexType, Type constituentType) const;
 
+  /** Make the type of set with the given parameterization. */
+  SetType mkSetType(Type elementType) const;
+
   /** Make a type representing the given datatype. */
   DatatypeType mkDatatypeType(const Datatype& datatype);
 
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index caf8f5ad4..b4d20b514 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -751,6 +751,9 @@ public:
   /** Make the type of arrays with the given parameterization */
   inline TypeNode mkArrayType(TypeNode indexType, TypeNode constituentType);
 
+  /** Make the type of arrays with the given parameterization */
+  inline TypeNode mkSetType(TypeNode elementType);
+
   /** Make a type representing a constructor with the given parameterization */
   TypeNode mkConstructorType(const DatatypeConstructor& constructor, TypeNode range);
 
@@ -1058,6 +1061,16 @@ inline TypeNode NodeManager::mkArrayType(TypeNode indexType,
   return mkTypeNode(kind::ARRAY_TYPE, indexType, constituentType);
 }
 
+inline TypeNode NodeManager::mkSetType(TypeNode elementType) {
+  CheckArgument(!elementType.isNull(), elementType,
+                "unexpected NULL element type");
+  // TODO: Confirm meaning of isFunctionLike(). --K
+  CheckArgument(!elementType.isFunctionLike(), elementType,
+                "cannot store function-like types in sets");
+  Debug("sets") << "making sets type " << elementType << std::endl;
+  return mkTypeNode(kind::SET_TYPE, elementType);
+}
+
 inline TypeNode NodeManager::mkSelectorType(TypeNode domain, TypeNode range) {
   CheckArgument(!domain.isFunctionLike(), domain,
                 "cannot create higher-order function types");
diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index 672fc6aae..d0fe77aae 100644
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -292,6 +292,12 @@ bool Type::isArray() const {
   return d_typeNode->isArray();
 }
 
+/** Is this a Set type? */
+bool Type::isSet() const {
+  NodeManagerScope nms(d_nodeManager);
+  return d_typeNode->isSet();
+}
+
 /** Is this a sort kind */
 bool Type::isSort() const {
   NodeManagerScope nms(d_nodeManager);
@@ -480,6 +486,11 @@ ArrayType::ArrayType(const Type& t) throw(IllegalArgumentException) :
   CheckArgument(isNull() || isArray(), this);
 }
 
+SetType::SetType(const Type& t) throw(IllegalArgumentException) :
+  Type(t) {
+  CheckArgument(isNull() || isSet(), this);
+}
+
 SortType::SortType(const Type& t) throw(IllegalArgumentException) :
   Type(t) {
   CheckArgument(isNull() || isSort(), this);
@@ -517,6 +528,10 @@ Type ArrayType::getConstituentType() const {
   return makeType(d_typeNode->getArrayConstituentType());
 }
 
+Type SetType::getElementType() const {
+  return makeType(d_typeNode->getSetElementType());
+}
+
 DatatypeType ConstructorType::getRangeType() const {
   return DatatypeType(makeType(d_typeNode->getConstructorRangeType()));
 }
diff --git a/src/expr/type.h b/src/expr/type.h
index 3c772d461..b4761e1d6 100644
--- a/src/expr/type.h
+++ b/src/expr/type.h
@@ -49,6 +49,7 @@ class RealType;
 class StringType;
 class BitVectorType;
 class ArrayType;
+class SetType;
 class DatatypeType;
 class ConstructorType;
 class SelectorType;
@@ -301,6 +302,12 @@ public:
   bool isArray() const;
 
   /**
+   * Is this a Set type?
+   * @return true if the type is a Set type
+   */
+  bool isSet() const;
+
+ /**
    * Is this a datatype type?
    * @return true if the type is a datatype type
    */
@@ -489,6 +496,20 @@ public:
 };/* class ArrayType */
 
 /**
+ * Class encapsulating an set type.
+ */
+class CVC4_PUBLIC SetType : public Type {
+
+public:
+
+  /** Construct from the base type */
+  SetType(const Type& type = Type()) throw(IllegalArgumentException);
+
+  /** Get the index type */
+  Type getElementType() const;
+};/* class SetType */
+
+/**
  * Class encapsulating a user-defined sort.
  */
 class CVC4_PUBLIC SortType : public Type {
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index c823190bf..a49ae31bf 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -466,6 +466,9 @@ public:
   /** Is this an array type? */
   bool isArray() const;
 
+  /** Is this a Set type? */
+  bool isSet() const;
+
   /** Get the index type (for array types) */
   TypeNode getArrayIndexType() const;
 
@@ -475,6 +478,9 @@ public:
   /** Get the return type (for constructor types) */
   TypeNode getConstructorRangeType() const;
 
+  /** Get the element type (for set types) */
+  TypeNode getSetElementType() const;
+
   /**
    * Is this a function type?  Function-like things (e.g. datatype
    * selectors) that aren't actually functions are NOT considered
@@ -867,6 +873,15 @@ inline TypeNode TypeNode::getConstructorRangeType() const {
   return (*this)[getNumChildren()-1];
 }
 
+inline bool TypeNode::isSet() const {
+  return getKind() == kind::SET_TYPE;
+}
+
+inline TypeNode TypeNode::getSetElementType() const {
+  Assert(isSet());
+  return (*this)[0];
+}
+
 inline bool TypeNode::isFunction() const {
   return getKind() == kind::FUNCTION_TYPE;
 }
diff --git a/src/options/Makefile.am b/src/options/Makefile.am
index 5b0894680..8780922c9 100644
--- a/src/options/Makefile.am
+++ b/src/options/Makefile.am
@@ -40,7 +40,9 @@ OPTIONS_FILES_SRCS = \
 	../parser/options.cpp \
 	../parser/options.h \
 	../theory/idl/options.cpp \
-	../theory/idl/options.h
+	../theory/idl/options.h \
+	../theory/sets/options.cpp \
+	../theory/sets/options.h
 
 OPTIONS_FILES = \
 	$(patsubst %.cpp,%,$(filter %.cpp,$(OPTIONS_FILES_SRCS)))
@@ -101,7 +103,9 @@ nodist_liboptions_la_SOURCES = \
 	../parser/options.cpp \
 	../parser/options.h \
 	../theory/idl/options.cpp \
-	../theory/idl/options.h
+	../theory/idl/options.h \
+	../theory/sets/options.cpp \
+	../theory/sets/options.h
 
 BUILT_SOURCES = \
 	exprs-builts \
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index f97f4a8ae..6974c62af 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -833,6 +833,11 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
                              MK_CONST(AscriptionType(dtc.getSpecializedConstructorType(type))), f.getOperator() ));
         v.insert(v.end(), f.begin(), f.end());
         expr = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, v);
+      } else if(f.getKind() == CVC4::kind::EMPTYSET) {
+        Debug("parser") << "Empty set encountered: " << f << " "
+                          << f2 << " " << type <<  std::endl;
+        // TODO: what is f2 about, should we add some assertions?
+        expr = MK_CONST( ::CVC4::EmptySet(type) );
       } else {
         if(f.getType() != type) {
           PARSER_STATE->parseError("Type ascription not satisfied.");
@@ -1028,6 +1033,9 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
   | str[s,false]
     { expr = MK_CONST( ::CVC4::String(s) ); }
 
+  | EMPTYSET_TOK
+    { expr = MK_CONST( ::CVC4::EmptySet()); }
+
     // NOTE: Theory constants go here
   ;
 
@@ -1298,6 +1306,12 @@ builtinOp[CVC4::Kind& kind]
   | REPLUS_TOK     { $kind = CVC4::kind::REGEXP_PLUS; }
   | REOPT_TOK      { $kind = CVC4::kind::REGEXP_OPT; }
   | RERANGE_TOK    { $kind = CVC4::kind::REGEXP_RANGE; }
+  | SETUNION_TOK  { $kind = CVC4::kind::UNION; }
+  | SETINT_TOK    { $kind = CVC4::kind::INTERSECTION; }
+  | SETMINUS_TOK  { $kind = CVC4::kind::SETMINUS; }
+  | SETSUB_TOK    { $kind = CVC4::kind::SUBSET; }
+  | SETIN_TOK     { $kind = CVC4::kind::IN; }
+  | SETSINGLETON_TOK { $kind = CVC4::kind::SET_SINGLETON; }
 
   // NOTE: Theory operators go here
   ;
@@ -1407,6 +1421,11 @@ sortSymbol[CVC4::Type& t, CVC4::parser::DeclarationCheck check]
           PARSER_STATE->parseError("Illegal array type.");
         }
         t = EXPR_MANAGER->mkArrayType( args[0], args[1] );
+      } else if(name == "Set") {
+        if(args.size() != 1) {
+          PARSER_STATE->parseError("Illegal set type.");
+        }
+        t = EXPR_MANAGER->mkSetType( args[0] );
       } else if(check == CHECK_DECLARED ||
                 PARSER_STATE->isDeclared(name, SYM_SORT)) {
         t = PARSER_STATE->getSort(name, args);
@@ -1688,6 +1707,14 @@ REPLUS_TOK : 're.+';
 REOPT_TOK : 're.opt';
 RERANGE_TOK : 're.range';
 
+SETUNION_TOK: 'union';
+SETINT_TOK: 'intersection';
+SETMINUS_TOK: 'setminus';
+SETSUB_TOK: 'subseteq';
+SETIN_TOK: 'in';
+SETSINGLETON_TOK: 'setenum';
+EMPTYSET_TOK: 'emptyset';
+
 /**
  * A sequence of printable ASCII characters (except backslash) that starts
  * and ends with | and does not otherwise contain |.
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 5dc3043af..fcb352ea7 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -203,6 +203,10 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
       break;
     }
 
+    case kind::EMPTYSET:
+      out << "(as emptyset " << n.getConst<EmptySet>().getType() << ")";
+      break;
+
     default:
       // fall back on whatever operator<< does on underlying type; we
       // might luck out and be SMT-LIB v2 compliant
@@ -343,7 +347,16 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
     stillNeedToPrintParams = false;
     break;
 
-    // datatypes
+    // sets
+  case kind::UNION:
+  case kind::INTERSECTION:
+  case kind::SETMINUS:
+  case kind::SUBSET:
+  case kind::IN:
+  case kind::SET_TYPE:
+  case kind::SET_SINGLETON: out << smtKindString(k) << " "; break;
+
+   // datatypes
   case kind::APPLY_TYPE_ASCRIPTION: {
       out << "as ";
       toStream(out, n[0], toDepth < 0 ? toDepth : toDepth - 1, types);
@@ -528,6 +541,14 @@ static string smtKindString(Kind k) throw() {
   case kind::BITVECTOR_SIGN_EXTEND: return "sign_extend";
   case kind::BITVECTOR_ROTATE_LEFT: return "rotate_left";
   case kind::BITVECTOR_ROTATE_RIGHT: return "rotate_right";
+
+  case kind::UNION: return "union";
+  case kind::INTERSECTION: return "intersection";
+  case kind::SETMINUS: return "setminus";
+  case kind::SUBSET: return "subseteq";
+  case kind::IN: return "in";
+  case kind::SET_TYPE: return "Set";
+  case kind::SET_SINGLETON: return "setenum";
   default:
     ; /* fall through */
   }
diff --git a/src/theory/arrays/array_info.h b/src/theory/arrays/array_info.h
index 1f97c02ca..0a2a96603 100644
--- a/src/theory/arrays/array_info.h
+++ b/src/theory/arrays/array_info.h
@@ -75,8 +75,6 @@ public:
   }
 
   ~Info() {
-    //FIXME!
-    //indices->deleteSelf();
     indices->deleteSelf();
     stores->deleteSelf();
     in_stores->deleteSelf();
diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp
index 525b129cf..a30867ee1 100644
--- a/src/theory/logic_info.cpp
+++ b/src/theory/logic_info.cpp
@@ -122,6 +122,10 @@ std::string LogicInfo::getLogicString() const {
         }
         ++seen;
       }
+      if(d_theories[THEORY_SETS]) {
+        ss << "_SETS";
+        ++seen;
+      }
 
       if(seen != d_sharingTheories) {
         Unhandled("can't extract a logic string from LogicInfo; at least one "
@@ -256,6 +260,10 @@ void LogicInfo::setLogicString(std::string logicString) throw(IllegalArgumentExc
         arithNonLinear();
         p += 4;
       }
+      if(!strncmp(p, "_SETS", 5)) {
+        enableTheory(THEORY_SETS);
+        p += 5;
+      }
     }
   }
   if(*p != '\0') {
diff --git a/src/theory/sets/.gitignore b/src/theory/sets/.gitignore
new file mode 100644
index 000000000..4c83ffd6f
--- /dev/null
+++ b/src/theory/sets/.gitignore
@@ -0,0 +1 @@
+README.WHATS-NEXT
diff --git a/src/theory/sets/Makefile b/src/theory/sets/Makefile
new file mode 100644
index 000000000..68a2c5cb6
--- /dev/null
+++ b/src/theory/sets/Makefile
@@ -0,0 +1,4 @@
+topdir = ../../..
+srcdir = src/theory/sets
+
+include $(topdir)/Makefile.subdir
diff --git a/src/theory/sets/Makefile.am b/src/theory/sets/Makefile.am
new file mode 100644
index 000000000..00678628f
--- /dev/null
+++ b/src/theory/sets/Makefile.am
@@ -0,0 +1,20 @@
+AM_CPPFLAGS = \
+	-D__BUILDING_CVC4LIB \
+	-I@builddir@/../.. -I@srcdir@/../../include -I@srcdir@/../..
+AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
+
+noinst_LTLIBRARIES = libsets.la
+
+libsets_la_SOURCES = \
+	theory_sets.h \
+	theory_sets.cpp \
+	theory_sets_private.h \
+	theory_sets_private.cpp \
+	theory_sets_rewriter.h \
+	theory_sets_rewriter.cpp \
+	theory_sets_type_rules.h \
+	theory_set_type_enumerator.h
+
+EXTRA_DIST = \
+	kinds \
+	options_handlers.h
diff --git a/src/theory/sets/expr_patterns.h b/src/theory/sets/expr_patterns.h
new file mode 100644
index 000000000..089549457
--- /dev/null
+++ b/src/theory/sets/expr_patterns.h
@@ -0,0 +1,51 @@
+/*********************                                                        */
+/*! \file expr_patterns.h
+ ** \verbatim
+ ** Original author: Kshitij Bansal
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2013-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Expr patterns.
+ **
+ ** Expr patterns.
+ **/
+
+#include "cvc4_private.h"
+
+#pragma once
+
+namespace CVC4 {
+namespace expr {
+namespace pattern {
+
+static Node AND(TNode a, TNode b) {
+  return NodeManager::currentNM()->mkNode(kind::AND, a, b);
+}
+
+static Node OR(TNode a, TNode b) {
+  return NodeManager::currentNM()->mkNode(kind::OR, a, b);
+}
+
+static Node OR(TNode a, TNode b, TNode c) {
+  return NodeManager::currentNM()->mkNode(kind::OR, a, b, c);
+}
+
+static Node IN(TNode a, TNode b) {
+  return NodeManager::currentNM()->mkNode(kind::IN, a, b);
+}
+
+static Node EQUAL(TNode a, TNode b) {
+  return NodeManager::currentNM()->mkNode(kind::EQUAL, a, b);
+}
+
+static Node NOT(TNode a) {
+  return NodeManager::currentNM()->mkNode(kind::NOT, a);
+}
+
+}/* CVC4::expr::pattern namespace */
+}/* CVC4::expr namespace */
+}/* CVC4 namespace */
diff --git a/src/theory/sets/kinds b/src/theory/sets/kinds
new file mode 100644
index 000000000..bae0c5f1d
--- /dev/null
+++ b/src/theory/sets/kinds
@@ -0,0 +1,55 @@
+# kinds                                                               -*- sh -*-
+#
+# For documentation on this file format, please refer to
+# src/theory/builtin/kinds.
+#
+
+theory THEORY_SETS ::CVC4::theory::sets::TheorySets "theory/sets/theory_sets.h"
+typechecker "theory/sets/theory_sets_type_rules.h"
+rewriter ::CVC4::theory::sets::TheorySetsRewriter "theory/sets/theory_sets_rewriter.h"
+
+properties check propagate #presolve postsolve
+
+# Theory content goes here.
+
+# constants...
+constant EMPTYSET \
+    ::CVC4::EmptySet \
+    ::CVC4::EmptySetHashFunction \
+    "util/emptyset.h" \
+    "empty set"
+
+# types...
+operator SET_TYPE 1 "set type"   # the type
+cardinality SET_TYPE \
+    "::CVC4::theory::sets::SetsProperties::computeCardinality(%TYPE%)" \
+    "theory/sets/theory_sets_type_rules.h"
+well-founded SET_TYPE \
+    "::CVC4::theory::sets::SetsProperties::isWellFounded(%TYPE%)" \
+    "::CVC4::theory::sets::SetsProperties::mkGroundTerm(%TYPE%)" \
+    "theory/sets/theory_sets_type_rules.h"
+enumerator SET_TYPE \
+    "::CVC4::theory::sets::SetEnumerator" \
+    "theory/sets/theory_sets_type_enumerator.h"
+
+# operators...
+operator UNION 2 "set union"
+operator INTERSECTION 2 "set intersection"
+operator SETMINUS 2 "set subtraction"
+operator SUBSET 2 "subset"
+operator IN 2 "set membership"
+
+operator SET_SINGLETON 1 "singleton set"
+
+typerule UNION ::CVC4::theory::sets::SetUnionTypeRule
+typerule INTERSECTION ::CVC4::theory::sets::SetIntersectionTypeRule
+typerule SETMINUS ::CVC4::theory::sets::SetSetminusTypeRule
+typerule SUBSET ::CVC4::theory::sets::SetSubsetTypeRule
+typerule IN ::CVC4::theory::sets::SetInTypeRule
+typerule SET_SINGLETON ::CVC4::theory::sets::SetSingletonTypeRule
+typerule EMPTYSET ::CVC4::theory::sets::EmptySetTypeRule
+
+construle SET_SINGLETON ::CVC4::theory::sets::SetConstTypeRule
+construle UNION ::CVC4::theory::sets::SetConstTypeRule
+
+endtheory
diff --git a/src/theory/sets/options b/src/theory/sets/options
new file mode 100644
index 000000000..dc6c6e907
--- /dev/null
+++ b/src/theory/sets/options
@@ -0,0 +1,14 @@
+#
+# Option specification file for CVC4
+# See src/options/base_options for a description of this file format
+#
+
+module SETS "theory/sets/options.h" Sets
+
+option setsPropagate --sets-propagate bool :default true
+ determines whether to propagate learnt facts to Theory Engine / SAT solver
+
+option setsEagerLemmas --sets-eager-lemmas bool :default false
+ if true, will add lemmas even if not at FULL_EFFORT
+
+endmodule
diff --git a/src/theory/sets/options_handlers.h b/src/theory/sets/options_handlers.h
new file mode 100644
index 000000000..ff535945e
--- /dev/null
+++ b/src/theory/sets/options_handlers.h
@@ -0,0 +1,14 @@
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__SETS__OPTIONS_HANDLERS_H
+#define __CVC4__THEORY__SETS__OPTIONS_HANDLERS_H
+
+namespace CVC4 {
+namespace theory {
+namespace sets {
+
+}/* CVC4::theory::sets namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__SETS__OPTIONS_HANDLERS_H */
diff --git a/src/theory/sets/term_info.h b/src/theory/sets/term_info.h
new file mode 100644
index 000000000..ea435d9b7
--- /dev/null
+++ b/src/theory/sets/term_info.h
@@ -0,0 +1,57 @@
+/*********************                                                        */
+/*! \file term_info.h
+ ** \verbatim
+ ** Original author: Kshitij Bansal
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2013-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Term info.
+ **
+ ** Term info.
+ **/
+
+#include "cvc4_private.h"
+
+#pragma once
+
+namespace CVC4 {
+namespace theory {
+namespace sets {
+
+
+typedef context::CDList<TNode> CDTNodeList;
+typedef context::CDHashSet<Node, NodeHashFunction> CDNodeSet;
+typedef context::CDHashSet<Node, NodeHashFunction> CDNodeSet;
+
+class TheorySetsTermInfo {
+public:
+  CDTNodeList* elementsInThisSet;
+  CDTNodeList* elementsNotInThisSet;
+  CDTNodeList* parents;
+
+  TheorySetsTermInfo(context::Context* c)
+  {
+    elementsInThisSet = new(true)CDTNodeList(c);
+    elementsNotInThisSet = new(true)CDTNodeList(c);
+    parents = new(true)CDTNodeList(c);
+  }
+
+  void addToElementList(TNode n, bool polarity) {
+    if(polarity) elementsInThisSet -> push_back(n);
+    else elementsNotInThisSet -> push_back(n);
+  }
+
+  ~TheorySetsTermInfo() {
+    elementsInThisSet -> deleteSelf();
+    elementsNotInThisSet -> deleteSelf();
+    parents -> deleteSelf();
+  }
+};
+
+}/* CVC4::theory::sets namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp
new file mode 100644
index 000000000..91195e67e
--- /dev/null
+++ b/src/theory/sets/theory_sets.cpp
@@ -0,0 +1,55 @@
+/*********************                                                        */
+/*! \file theory_sets.cpp
+ ** \verbatim
+ ** Original author: Kshitij Bansal
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2013-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Sets theory.
+ **
+ ** Sets theory.
+ **/
+
+#include "theory/sets/theory_sets.h"
+#include "theory/sets/theory_sets_private.h"
+
+namespace CVC4 {
+namespace theory {
+namespace sets {
+
+TheorySets::TheorySets(context::Context* c,
+                       context::UserContext* u,
+                       OutputChannel& out,
+                       Valuation valuation,
+                       const LogicInfo& logicInfo) :
+  Theory(THEORY_SETS, c, u, out, valuation, logicInfo),
+  d_internal(new TheorySetsPrivate(*this, c, u)) {
+}
+
+TheorySets::~TheorySets() {
+  delete d_internal;
+}
+
+void TheorySets::check(Effort e) {
+  d_internal->check(e);
+}
+
+void TheorySets::propagate(Effort e) {
+  d_internal->propagate(e);
+}
+
+Node TheorySets::explain(TNode node) {
+  return d_internal->explain(node);
+}
+
+void TheorySets::preRegisterTerm(TNode node) {
+  return d_internal->preRegisterTerm(node);
+}
+
+}/* CVC4::theory::sets namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h
new file mode 100644
index 000000000..c95229f05
--- /dev/null
+++ b/src/theory/sets/theory_sets.h
@@ -0,0 +1,65 @@
+/*********************                                                        */
+/*! \file theory_sets.h
+ ** \verbatim
+ ** Original author: Kshitij Bansal
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2013-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Sets theory.
+ **
+ ** Sets theory.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__SETS__THEORY_SETS_H
+#define __CVC4__THEORY__SETS__THEORY_SETS_H
+
+#include "theory/theory.h"
+#include "theory/uf/equality_engine.h"
+
+namespace CVC4 {
+namespace theory {
+namespace sets {
+
+class TheorySetsPrivate;
+
+class TheorySets : public Theory {
+private:
+  friend class TheorySetsPrivate;
+  TheorySetsPrivate* d_internal;
+public:
+
+  /**
+   * Constructs a new instance of TheorySets w.r.t. the provided
+   * contexts.
+   */
+  TheorySets(context::Context* c,
+               context::UserContext* u,
+               OutputChannel& out,
+               Valuation valuation,
+               const LogicInfo& logicInfo);
+
+  ~TheorySets();
+
+  void check(Effort);
+
+  void propagate(Effort);
+
+  Node explain(TNode);
+
+  std::string identify() const { return "THEORY_SETS"; }
+
+  void preRegisterTerm(TNode node);
+
+};/* class TheorySets */
+
+}/* CVC4::theory::sets namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__SETS__THEORY_SETS_H */
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
new file mode 100644
index 000000000..8fd490554
--- /dev/null
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -0,0 +1,871 @@
+/*********************                                                        */
+/*! \file theory_sets_private.cpp
+ ** \verbatim
+ ** Original author: Kshitij Bansal
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2013-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Sets theory implementation.
+ **
+ ** Sets theory implementation.
+ **/
+
+#include "theory/sets/theory_sets.h"
+#include "theory/sets/theory_sets_private.h"
+
+#include "theory/sets/options.h"
+#include "theory/sets/expr_patterns.h" // ONLY included here
+
+#include "util/result.h"
+
+using namespace std;
+using namespace CVC4::expr::pattern;
+
+namespace CVC4 {
+namespace theory {
+namespace sets {
+
+const char* element_of_str = " \u2208 ";
+
+/**************************** TheorySetsPrivate *****************************/
+/**************************** TheorySetsPrivate *****************************/
+/**************************** TheorySetsPrivate *****************************/
+
+void TheorySetsPrivate::check(Theory::Effort level) {
+
+  CodeTimer checkCodeTimer(d_statistics.d_checkTime);
+
+  while(!d_external.done() && !d_conflict) {
+    // Get all the assertions
+    Assertion assertion = d_external.get();
+    TNode fact = assertion.assertion;
+
+    Debug("sets") << "\n\n[sets] TheorySetsPrivate::check(): processing "
+                  << fact << std::endl;
+
+    bool polarity = fact.getKind() != kind::NOT;
+    TNode atom = polarity ? fact : fact[0];
+
+    // Solve each
+    switch(atom.getKind()) {
+    case kind::EQUAL:
+      Debug("sets") << atom[0] << " should " << (polarity ? "":"NOT ")
+                    << "be equal to " << atom[1] << std::endl;
+      assertEquality(fact, fact, /* learnt = */ false);
+      break;
+
+    case kind::IN:
+      Debug("sets") << atom[0] << " should " << (polarity ? "":"NOT ")
+                    << "be in " << atom[1] << std::endl;
+      assertMemebership(fact, fact, /* learnt = */ false);
+      break;
+
+    default:
+      Unhandled(fact.getKind());
+    }
+    finishPropagation();
+
+    Debug("sets") << "[sets]  in conflict = " << d_conflict << std::endl;
+
+    if(d_conflict && !d_equalityEngine.consistent()) return;
+    Assert(!d_conflict);
+    Assert(d_equalityEngine.consistent());
+  }
+
+  Debug("sets") << "[sets]  is complete = " << isComplete() << std::endl;
+
+  if( (Theory::EFFORT_FULL || options::setsEagerLemmas() ) && !isComplete()) {
+    d_external.d_out->lemma(getLemma());
+  }
+
+  return;
+}/* TheorySetsPrivate::check() */
+
+
+void TheorySetsPrivate::assertEquality(TNode fact, TNode reason, bool learnt)
+{
+  Debug("sets-assert") << "\n[sets-assert] adding equality: " << fact
+                    << ", " << reason
+                    << ", " << learnt << std::endl;
+
+  bool polarity = fact.getKind() != kind::NOT;
+  TNode atom = polarity ? fact : fact[0];
+
+  // fact already holds
+  if( holds(atom, polarity) ) {
+    Debug("sets-assert") << "[sets-assert]   already present, skipping" << std::endl;
+    return;
+  }
+
+  // assert fact & check for conflict
+  if(learnt) {
+    registerReason(reason, /*save=*/ true);
+  }
+  d_equalityEngine.assertEquality(atom, polarity, reason);
+
+  if(!d_equalityEngine.consistent()) {
+    Debug("sets-assert") << "[sets-assert]   running into a conflict" << std::endl;
+    d_conflict = true;
+    return;
+  }
+
+  if(!polarity && atom[0].getType().isSet()) {
+    addToPending(atom);
+  }
+
+}/* TheorySetsPrivate::assertEquality() */
+
+
+void TheorySetsPrivate::assertMemebership(TNode fact, TNode reason, bool learnt)
+{
+  Debug("sets-assert") << "\n[sets-assert] adding membership: " << fact
+                       << ", " << reason
+                       << ", " << learnt << std::endl;
+
+  bool polarity = fact.getKind() == kind::NOT ? false : true;
+  TNode atom = polarity ? fact : fact[0];
+
+  // fact already holds
+  if( holds(atom, polarity) ) {
+    Debug("sets-assert") << "[sets-assert]   already present, skipping" << std::endl;
+    return;
+  }
+
+  // assert fact & check for conflict
+  if(learnt) {
+    registerReason(reason, true);
+  }
+  d_equalityEngine.assertPredicate(atom, polarity, reason);
+
+  if(!d_equalityEngine.consistent()) {
+    Debug("sets-assert") << "[sets-assert]   running into a conflict" << std::endl;
+    d_conflict = true;
+    return;
+  }
+
+  // update term info data structures
+  d_termInfoManager->notifyMembership(fact);
+
+  // propagation
+  TNode x = d_equalityEngine.getRepresentative(atom[0]);
+  eq::EqClassIterator j(d_equalityEngine.getRepresentative(atom[1]),
+                        &d_equalityEngine);
+  TNode S = (*j);
+  Node cur_atom = IN(x, S);
+
+  /**
+   * It is sufficient to do emptyset propagation outside the loop as
+   * constant term is guaranteed to be class representative.
+   */
+  if(polarity && S.getKind() == kind::EMPTYSET) {
+    Debug("sets-prop") << "[sets-prop]  something in empty set? conflict."
+                       << std::endl;
+    learnLiteral(cur_atom, false, cur_atom);
+    Assert(d_conflict);
+    return;
+  }
+
+  for(; !j.isFinished(); ++j) {
+    TNode S = (*j);
+    Node cur_atom = IN(x, S);
+
+    // propagation : children
+    Debug("sets-prop") << "[sets-prop] Propagating 'down' for "
+                       << x << element_of_str << S << std::endl;
+    if(S.getKind() == kind::UNION ||
+       S.getKind() == kind::INTERSECTION ||
+       S.getKind() == kind::SETMINUS ||
+       S.getKind() == kind::SET_SINGLETON) {
+      doSettermPropagation(x, S);
+      if(d_conflict) return;
+    }// propagation: children
+
+
+    // propagation : parents
+    Debug("sets-prop") << "[sets-prop] Propagating 'up' for "
+                       << x << element_of_str << S << std::endl;
+    const CDTNodeList* parentList = d_termInfoManager->getParents(S);
+    for(typeof(parentList->begin()) k = parentList->begin();
+        k != parentList->end(); ++k) {
+      doSettermPropagation(x, *k);
+      if(d_conflict) return;
+    }// propagation : parents
+
+
+  }//j loop
+
+}/* TheorySetsPrivate::assertMemebership() */
+
+
+void TheorySetsPrivate::doSettermPropagation(TNode x, TNode S)
+{
+  Debug("sets-prop") << "[sets-prop] doSettermPropagation("
+                     << x << ", " << S << std::endl;
+
+  Assert(S.getType().isSet() && S.getType().getSetElementType() == x.getType());
+
+  Node literal, left_literal, right_literal;
+
+  // axiom: literal <=> left_literal AND right_literal
+  switch(S.getKind()) {
+  case kind::INTERSECTION:
+    literal       =       IN(x, S)      ;
+    left_literal  =       IN(x, S[0])   ;
+    right_literal =       IN(x, S[1])   ;
+    break;
+  case kind::UNION:
+    literal       = NOT(  IN(x, S)     );
+    left_literal  = NOT(  IN(x, S[0])  );
+    right_literal = NOT(  IN(x, S[1])  );
+    break;
+  case kind::SETMINUS:
+    literal       =       IN(x, S)      ;
+    left_literal  =       IN(x, S[0])   ;
+    right_literal = NOT(  IN(x, S[1])  );
+    break;
+  case kind::SET_SINGLETON: {
+    Node atom = IN(x, S);
+    if(holds(atom, true)) {
+      learnLiteral(EQUAL(x, S[0]), true, atom);
+    } else if(holds(atom, false)) {
+      learnLiteral(EQUAL(x, S[0]), false, NOT(atom));
+    }
+    return;
+  }
+  default:
+    Unhandled();
+  }
+
+  Debug("sets-prop-details")
+    << "[sets-prop-details]   " << literal << " IFF " << left_literal
+    << " AND " << right_literal << std::endl;
+
+  Debug("sets-prop-details")
+    << "[sets-prop-details]   "
+    << (holds(literal) ? "yes" : (holds(literal.negate()) ? " no" : " _ "))
+    << " IFF "
+    << (holds(left_literal) ? "yes" : (holds(left_literal.negate()) ? "no " : " _ "))
+    << " AND "
+    << (holds(right_literal) ? "yes" : (holds(right_literal.negate()) ? "no " : " _ "))
+    << std::endl;
+
+  Assert( present( IN(x, S)    ) ||
+          present( IN(x, S[0]) ) ||
+          present( IN(x, S[1]) ) );
+
+  if( holds(literal) ) {
+    // 1a. literal => left_literal
+    Debug("sets-prop") << "[sets-prop]  ... via case 1a. ..." << std::endl;
+    learnLiteral(left_literal, literal);
+    if(d_conflict) return;
+
+    // 1b. literal => right_literal
+    Debug("sets-prop") << "[sets-prop]  ... via case 1b. ..." << std::endl;
+    learnLiteral(right_literal, literal);
+    if(d_conflict) return;
+
+    // subsumption requirement met, exit
+    return;
+  }
+  else if( holds(literal.negate() ) ) {
+    // 4. neg(literal), left_literal => neg(right_literal)
+    if( holds(left_literal) ) {
+      Debug("sets-prop") << "[sets-prop]  ... via case 4. ..." << std::endl;
+      learnLiteral(right_literal.negate(), AND( literal.negate(),
+                                                left_literal) );
+      if(d_conflict) return;
+    }
+
+    // 5. neg(literal), right_literal => neg(left_literal)
+    if( holds(right_literal) ) {
+      Debug("sets-prop") << "[sets-prop]  ... via case 5. ..." << std::endl;
+      learnLiteral(left_literal.negate(), AND( literal.negate(),
+                                               right_literal) );
+      if(d_conflict) return;
+    }
+  }
+  else {
+    // 2,3. neg(left_literal) v neg(right_literal) => neg(literal)
+    if(holds(left_literal.negate())) {
+      Debug("sets-prop") << "[sets-prop]  ... via case 2. ..." << std::endl;
+      learnLiteral(literal.negate(), left_literal.negate());
+      if(d_conflict) return;
+    }
+    else if(holds(right_literal.negate())) {
+      Debug("sets-prop") << "[sets-prop]  ... via case 3. ..." << std::endl;
+      learnLiteral(literal.negate(), right_literal.negate());
+      if(d_conflict) return;
+    }
+
+    // 6. the axiom itself:
+    else if(holds(left_literal) && holds(right_literal)) {
+      Debug("sets-prop") << "[sets-prop]  ... via case 6. ..." << std::endl;
+      learnLiteral(literal, AND(left_literal, right_literal) );
+      if(d_conflict) return;
+    }
+  }
+
+  // check fulfilling rule
+  Node n;
+  switch(S.getKind()) {
+  case kind::UNION:
+    if( holds(IN(x, S)) &&
+        !present( IN(x, S[0]) ) )
+      addToPending( IN(x, S[0]) );
+    break;
+  case kind::SETMINUS: // intentional fallthrough
+  case kind::INTERSECTION:
+    if( holds(IN(x, S[0])) &&
+        !present( IN(x, S[1]) ))
+      addToPending( IN(x, S[1]) );
+    break;
+  default:
+    Assert(false, "MembershipEngine::doSettermPropagation");
+  }
+}
+
+
+void TheorySetsPrivate::learnLiteral(TNode atom, bool polarity, Node reason) {
+  Debug("sets-learn") << "[sets-learn] learnLiteral(" << atom
+                      << ", " << polarity << ")" << std::endl;
+
+  if( holds(atom, polarity) ) {
+    Debug("sets-learn") << "[sets-learn] \u2514 already known, skipping" << std::endl;
+    return;
+  }
+
+  if( holds(atom, !polarity) ) {
+    Debug("sets-learn") << "[sets-learn] \u2514 conflict found" << std::endl;
+
+    registerReason(reason, /*save=*/ true);
+
+    if(atom.getKind() == kind::EQUAL) {
+      d_equalityEngine.assertEquality(atom, polarity, reason);
+    } else {
+      d_equalityEngine.assertPredicate(atom, polarity, reason);
+    }
+    Assert(d_conflict);       // should be marked due to equality engine
+    return;
+  }
+
+  Assert(atom.getKind() == kind::EQUAL || atom.getKind() == kind::IN);
+
+  Node learnt_literal = polarity ? Node(atom) : NOT(atom);
+  d_propagationQueue.push_back( make_pair(learnt_literal, reason) );
+}
+
+/********************** Helper functions ***************************/
+/********************** Helper functions ***************************/
+/********************** Helper functions ***************************/
+
+Node mkAnd(const std::vector<TNode>& conjunctions) {
+  Assert(conjunctions.size() > 0);
+
+  std::set<TNode> all;
+
+  for (unsigned i = 0; i < conjunctions.size(); ++i) {
+    TNode t = conjunctions[i];
+
+    if (t.getKind() == kind::AND) {
+      for(TNode::iterator child_it = t.begin();
+          child_it != t.end(); ++child_it) {
+        Assert((*child_it).getKind() != kind::AND);
+        all.insert(*child_it);
+      }
+    }
+    else {
+      all.insert(t);
+    }
+
+  }
+
+  Assert(all.size() > 0);
+
+  if (all.size() == 1) {
+    // All the same, or just one
+    return conjunctions[0];
+  }
+
+  NodeBuilder<> conjunction(kind::AND);
+  std::set<TNode>::const_iterator it = all.begin();
+  std::set<TNode>::const_iterator it_end = all.end();
+  while (it != it_end) {
+    conjunction << *it;
+    ++ it;
+  }
+
+  return conjunction;
+}/* mkAnd() */
+
+
+TheorySetsPrivate::Statistics::Statistics() :
+  d_checkTime("theory::sets::time") {
+  StatisticsRegistry::registerStat(&d_checkTime);
+}
+
+
+TheorySetsPrivate::Statistics::~Statistics() {
+  StatisticsRegistry::unregisterStat(&d_checkTime);
+}
+
+
+bool TheorySetsPrivate::present(TNode atom) {
+  return holds(atom) || holds(atom.notNode());
+}
+
+
+bool TheorySetsPrivate::holds(TNode atom, bool polarity) {
+  Node polarity_atom = NodeManager::currentNM()->mkConst<bool>(polarity);
+
+  Node atomModEq = NodeManager::currentNM()->mkNode
+    (atom.getKind(), d_equalityEngine.getRepresentative(atom[0]),
+     d_equalityEngine.getRepresentative(atom[1]) );
+
+  d_equalityEngine.addTerm(atomModEq);
+
+  return d_equalityEngine.areEqual(atomModEq, polarity_atom);
+}
+
+
+void TheorySetsPrivate::registerReason(TNode reason, bool save)
+{
+  if(save) d_nodeSaver.insert(reason);
+
+  if(reason.getKind() == kind::AND) {
+    Assert(reason.getNumChildren() == 2);
+    registerReason(reason[0], false);
+    registerReason(reason[1], false);
+  } else if(reason.getKind() == kind::NOT) {
+    registerReason(reason[0], false);
+  } else if(reason.getKind() == kind::IN) {
+    d_equalityEngine.addTerm(reason);
+    Assert(present(reason));
+  } else if(reason.getKind() == kind::EQUAL) {
+    d_equalityEngine.addTerm(reason);
+    Assert(present(reason));
+  } else if(reason.getKind() == kind::CONST_BOOLEAN) {
+    // That's OK, already in EqEngine
+  } else {
+    Unhandled();
+  }
+}
+
+void TheorySetsPrivate::finishPropagation()
+{
+  while(!d_conflict && !d_settermPropagationQueue.empty()) {
+    std::pair<TNode,TNode> np = d_settermPropagationQueue.front();
+    d_settermPropagationQueue.pop();
+    doSettermPropagation(np.first, np.second);
+  }
+  while(!d_conflict && !d_propagationQueue.empty()) {
+    std::pair<Node,Node> np = d_propagationQueue.front();
+    d_propagationQueue.pop();
+    TNode atom = np.first.getKind() == kind::NOT ? np.first[0] : np.first;
+    if(atom.getKind() == kind::IN) {
+      assertMemebership(np.first, np.second, /* learnt = */ true);
+    } else {
+      assertEquality(np.first, np.second, /* learnt = */ true);
+    }
+  }
+}
+
+void TheorySetsPrivate::addToPending(Node n) {
+  if(d_pendingEverInserted.find(n) == d_pendingEverInserted.end()) {
+    if(n.getKind() == kind::IN) {
+      d_pending.push(n);
+    } else {
+      Assert(n.getKind() == kind::EQUAL);
+      d_pendingDisequal.push(n);
+    }
+    d_pendingEverInserted.insert(n);
+  }
+}
+
+bool TheorySetsPrivate::isComplete() {
+  while(!d_pending.empty() && present(d_pending.front()))
+    d_pending.pop();
+  return d_pending.empty() && d_pendingDisequal.empty();
+}
+
+Node TheorySetsPrivate::getLemma() {
+  Assert(!d_pending.empty() || !d_pendingDisequal.empty());
+
+  Node lemma;
+
+  if(!d_pending.empty()) {
+    Node n = d_pending.front();
+    d_pending.pop();
+
+    Assert(!present(n));
+    Assert(n.getKind() == kind::IN);
+
+    lemma = OR(n, NOT(n));
+  } else {
+    Node n = d_pendingDisequal.front();
+    d_pendingDisequal.pop();
+
+    Assert(n.getKind() == kind::EQUAL && n[0].getType().isSet());
+    Node x = NodeManager::currentNM()->mkSkolem("sde_$$", n[0].getType().getSetElementType());
+    Node l1 = IN(x, n[0]), l2 = IN(x, n[1]);
+
+    // d_equalityEngine.addTerm(x);
+    // d_equalityEngine.addTerm(l1);
+    // d_equalityEngine.addTerm(l2);
+    // d_terms.insert(x);
+
+    lemma = OR(n, AND(l1, NOT(l2)), AND(NOT(l1), l2));
+  }
+
+  Debug("sets-lemma") << "[sets-lemma] " << lemma << std::endl;
+
+  return  lemma;
+}
+
+
+TheorySetsPrivate::TheorySetsPrivate(TheorySets& external,
+                                     context::Context* c,
+                                     context::UserContext* u):
+  d_external(external),
+  d_notify(*this),
+  d_equalityEngine(d_notify, c, "theory::sets::TheorySetsPrivate"),
+  d_conflict(c),
+  d_termInfoManager(NULL),
+  d_propagationQueue(c),
+  d_settermPropagationQueue(c),
+  d_nodeSaver(c),
+  d_pending(u),
+  d_pendingDisequal(u),
+  d_pendingEverInserted(u)
+{
+  d_termInfoManager = new TermInfoManager(*this, c, &d_equalityEngine);
+
+  d_equalityEngine.addFunctionKind(kind::UNION);
+  d_equalityEngine.addFunctionKind(kind::INTERSECTION);
+  d_equalityEngine.addFunctionKind(kind::SETMINUS);
+
+  d_equalityEngine.addFunctionKind(kind::IN);
+  d_equalityEngine.addFunctionKind(kind::SUBSET);
+}/* TheorySetsPrivate::TheorySetsPrivate() */
+
+TheorySetsPrivate::~TheorySetsPrivate()
+{
+  delete d_termInfoManager;
+}
+
+
+
+void TheorySetsPrivate::propagate(Theory::Effort e)
+{
+  return;
+}
+
+bool TheorySetsPrivate::propagate(TNode literal) {
+  Debug("sets-prop") << " propagate(" << literal  << ")" << std::endl;
+
+  // If already in conflict, no more propagation
+  if (d_conflict) {
+    Debug("sets-prop") << "TheoryUF::propagate(" << literal << "): already in conflict" << std::endl;
+    return false;
+  }
+
+  // Propagate out
+  bool ok = d_external.d_out->propagate(literal);
+  if (!ok) {
+    d_conflict = true;
+  }
+
+  return ok;
+}/* TheorySetsPropagate::propagate(TNode) */
+
+
+void TheorySetsPrivate::conflict(TNode a, TNode b)
+{
+  if (a.getKind() == kind::CONST_BOOLEAN) {
+    d_conflictNode = explain(a.iffNode(b));
+  } else {
+    d_conflictNode = explain(a.eqNode(b));
+  }
+  d_external.d_out->conflict(d_conflictNode);
+  Debug("sets") << "[sets] conflict: " << a << " iff " << b
+                << ", explaination " << d_conflictNode << std::endl;
+  d_conflict = true;
+}
+
+Node TheorySetsPrivate::explain(TNode literal)
+{
+  Debug("sets") << "TheorySetsPrivate::explain(" << literal << ")"
+                << std::endl;
+
+  bool polarity = literal.getKind() != kind::NOT;
+  TNode atom = polarity ? literal : literal[0];
+  std::vector<TNode> assumptions;
+
+  if(atom.getKind() == kind::EQUAL || atom.getKind() == kind::IFF) {
+     d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions);
+  } else if(atom.getKind() == kind::IN) {
+    if( !d_equalityEngine.hasTerm(atom)) {
+      d_equalityEngine.addTerm(atom);
+    }
+    d_equalityEngine.explainPredicate(atom, polarity, assumptions);
+  } else {
+    Debug("sets") << "unhandled: " << literal << "; (" << atom << ", "
+                  << polarity << "); kind" << atom.getKind() << std::endl;
+    Unhandled();
+  }
+
+  return mkAnd(assumptions);
+}
+
+void TheorySetsPrivate::preRegisterTerm(TNode node)
+{
+  Debug("sets") << "TheorySetsPrivate::preRegisterTerm(" << node << ")"
+                << std::endl;
+
+  switch(node.getKind()) {
+  case kind::EQUAL:
+    // TODO: what's the point of this
+    d_equalityEngine.addTriggerEquality(node);
+    break;
+  case kind::IN:
+    // TODO: what's the point of this
+    d_equalityEngine.addTriggerPredicate(node);
+    break;
+  default:
+    d_termInfoManager->addTerm(node);
+    d_equalityEngine.addTriggerTerm(node, THEORY_SETS);
+    // d_equalityEngine.addTerm(node);
+  }
+  if(node.getKind() == kind::SET_SINGLETON) {
+    Node true_node = NodeManager::currentNM()->mkConst<bool>(true);
+    learnLiteral(IN(node[0], node), true, true_node);
+    //intentional fallthrough
+  }
+}
+
+
+
+/**************************** eq::NotifyClass *****************************/
+/**************************** eq::NotifyClass *****************************/
+/**************************** eq::NotifyClass *****************************/
+
+
+bool TheorySetsPrivate::NotifyClass::eqNotifyTriggerEquality(TNode equality, bool value)
+{
+  Debug("sets-eq") << "[sets-eq] eqNotifyTriggerEquality: equality = " << equality << " value = " << value << std::endl;
+  if (value) {
+    return d_theory.propagate(equality);
+  } else {
+    // We use only literal triggers so taking not is safe
+    return d_theory.propagate(equality.notNode());
+  }
+}
+
+bool TheorySetsPrivate::NotifyClass::eqNotifyTriggerPredicate(TNode predicate, bool value)
+{
+  Debug("sets-eq") << "[sets-eq] eqNotifyTriggerPredicate: predicate = " << predicate << " value = " << value << std::endl;
+  if (value) {
+    return d_theory.propagate(predicate);
+  } else {
+    return d_theory.propagate(predicate.notNode());
+  }
+}
+
+bool TheorySetsPrivate::NotifyClass::eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value)
+{
+  Debug("sets-eq") << "[sets-eq] eqNotifyTriggerTermEquality: tag = " << tag << " t1 = " << t1 << "  t2 = " << t2 << "  value = " << value << std::endl;
+  if(value) {
+    d_theory.d_termInfoManager->mergeTerms(t1, t2);
+  }
+  return true;
+}
+
+void TheorySetsPrivate::NotifyClass::eqNotifyConstantTermMerge(TNode t1, TNode t2)
+{
+  Debug("sets-eq") << "[sets-eq] eqNotifyConstantTermMerge " << " t1 = " << t1 << " t2 = " << t2 << std::endl;
+  d_theory.conflict(t1, t2);
+}
+
+void TheorySetsPrivate::NotifyClass::eqNotifyNewClass(TNode t)
+{
+  Debug("sets-eq") << "[sets-eq] eqNotifyNewClass:" << " t = " << t << std::endl;
+}
+
+void TheorySetsPrivate::NotifyClass::eqNotifyPreMerge(TNode t1, TNode t2)
+{
+  Debug("sets-eq") << "[sets-eq] eqNotifyPreMerge:" << " t1 = " << t1 << " t2 = " << t2 << std::endl;
+}
+
+void TheorySetsPrivate::NotifyClass::eqNotifyPostMerge(TNode t1, TNode t2)
+{
+  Debug("sets-eq") << "[sets-eq] eqNotifyPostMerge:" << " t1 = " << t1 << " t2 = " << t2 << std::endl;
+}
+
+void TheorySetsPrivate::NotifyClass::eqNotifyDisequal(TNode t1, TNode t2, TNode reason)
+{
+  Debug("sets-eq") << "[sets-eq] eqNotifyDisequal:" << " t1 = " << t1 << " t2 = " << t2 << " reason = " << reason << std::endl;
+}
+
+
+/**************************** TermInfoManager *****************************/
+/**************************** TermInfoManager *****************************/
+/**************************** TermInfoManager *****************************/
+
+void TheorySetsPrivate::TermInfoManager::mergeLists
+(CDTNodeList* la, const CDTNodeList* lb) const {
+  // straight from theory/arrays/array_info.cpp
+  std::set<TNode> temp;
+  CDTNodeList::const_iterator it;
+  for(it = la->begin() ; it != la->end(); it++ ) {
+    temp.insert((*it));
+  }
+
+  for(it = lb->begin() ; it!= lb->end(); it++ ) {
+    if(temp.count(*it) == 0) {
+      la->push_back(*it);
+    }
+  }
+}
+
+TheorySetsPrivate::TermInfoManager::TermInfoManager
+(TheorySetsPrivate& theory, context::Context* satContext, eq::EqualityEngine* eq):
+  d_theory(theory),
+  d_context(satContext),
+  d_eqEngine(eq),
+  d_terms(satContext),
+  d_info()
+{ }
+
+TheorySetsPrivate::TermInfoManager::~TermInfoManager() {
+  for( typeof(d_info.begin()) it = d_info.begin();
+       it != d_info.end(); ++it) {
+    delete (*it).second;
+  }
+}
+
+void TheorySetsPrivate::TermInfoManager::notifyMembership(TNode fact) {
+  bool polarity = fact.getKind() != kind::NOT;
+  TNode atom = polarity ? fact : fact[0];
+
+  TNode x = d_eqEngine->getRepresentative(atom[0]);
+  TNode S = d_eqEngine->getRepresentative(atom[1]);
+
+  Debug("sets-terminfo") << "[sets-terminfo] Adding membership " << x
+                         << " in " << S << " " << polarity << std::endl;
+
+  d_info[S]->addToElementList(x, polarity);
+}
+
+const CDTNodeList* TheorySetsPrivate::TermInfoManager::getParents(TNode x) {
+  return d_info[x]->parents;
+}
+
+void TheorySetsPrivate::TermInfoManager::addTerm(TNode n) {
+  unsigned numChild = n.getNumChildren();
+
+  if(!d_terms.contains(n)) {
+    d_terms.insert(n);
+    d_info[n] = new TheorySetsTermInfo(d_context);
+  }
+
+  if(n.getKind() == kind::UNION ||
+     n.getKind() == kind::INTERSECTION ||
+     n.getKind() == kind::SETMINUS ||
+     n.getKind() == kind::SET_SINGLETON) {
+
+    for(unsigned i = 0; i < numChild; ++i) {
+      if(d_terms.contains(n[i])) {
+        Debug("sets-parent") << "Adding " << n << " to parent list of "
+                             << n[i] << std::endl;
+        d_info[n[i]]->parents->push_back(n);
+      }
+    }
+
+  }
+}
+
+void TheorySetsPrivate::TermInfoManager::pushToSettermPropagationQueue
+(CDTNodeList* l, TNode S, bool polarity)
+{
+  for(typeof(l->begin()) i = l->begin(); i != l->end(); ++i) {
+    Debug("sets-prop") << "[sets-terminfo]  setterm todo: "
+                       << IN(*i, d_eqEngine->getRepresentative(S))
+                       << std::endl;
+
+    d_eqEngine->addTerm(IN(d_eqEngine->getRepresentative(*i),
+                           d_eqEngine->getRepresentative(S)));
+
+    for(eq::EqClassIterator j(d_eqEngine->getRepresentative(S), d_eqEngine);
+        !j.isFinished(); ++j) {
+
+      TNode x = (*i);
+      TNode S = (*j);
+      Node cur_atom = IN(x, S);
+
+      // propagation : empty set
+      if(polarity && S.getKind() == kind::EMPTYSET) {
+        Debug("sets-prop") << "[sets-prop]  something in empty set? conflict."
+                           << std::endl;
+        d_theory.learnLiteral(cur_atom, false, cur_atom);
+        return;
+      }// propagation: empty set
+
+      // propagation : children
+      if(S.getKind() == kind::UNION ||
+         S.getKind() == kind::INTERSECTION ||
+         S.getKind() == kind::SETMINUS ||
+         S.getKind() == kind::SET_SINGLETON) {
+        d_theory.d_settermPropagationQueue.push_back(std::make_pair(x, S));
+      }// propagation: children
+
+      // propagation : parents
+      const CDTNodeList* parentList = getParents(S);
+      for(typeof(parentList->begin()) k = parentList->begin();
+          k != parentList->end(); ++k) {
+        d_theory.d_settermPropagationQueue.push_back(std::make_pair(x, *k));
+      }// propagation : parents
+
+
+    }//j loop
+
+  }
+
+}
+
+void TheorySetsPrivate::TermInfoManager::mergeTerms(TNode a, TNode b) {
+  // merge b into a
+
+  if(!a.getType().isSet()) return;
+
+  Debug("sets-terminfo") << "[sets-terminfo] Merging (into) a = " << a
+                         << ", b = " << b << std::endl;
+  Debug("sets-terminfo") << "[sets-terminfo] reps"
+                         << ", a: " << d_eqEngine->getRepresentative(a)
+                         << ", b: " << d_eqEngine->getRepresentative(b)
+                         << std::endl;
+
+  typeof(d_info.begin()) ita = d_info.find(a);
+  typeof(d_info.begin()) itb = d_info.find(b);
+
+  Assert(ita != d_info.end());
+  Assert(itb != d_info.end());
+
+  pushToSettermPropagationQueue( (*ita).second->elementsInThisSet, b, true );
+  pushToSettermPropagationQueue( (*ita).second->elementsNotInThisSet, b, false );
+  pushToSettermPropagationQueue( (*itb).second->elementsNotInThisSet, a, false );
+  pushToSettermPropagationQueue( (*itb).second->elementsInThisSet, a, true );
+
+  mergeLists((*ita).second->elementsInThisSet,
+             (*itb).second->elementsInThisSet);
+
+  mergeLists((*ita).second->elementsNotInThisSet,
+             (*itb).second->elementsNotInThisSet);
+}
+
+
+}/* CVC4::theory::sets namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h
new file mode 100644
index 000000000..f1a8c0a46
--- /dev/null
+++ b/src/theory/sets/theory_sets_private.h
@@ -0,0 +1,166 @@
+/*********************                                                        */
+/*! \file theory_sets_private.h
+ ** \verbatim
+ ** Original author: Kshitij Bansal
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2013-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Sets theory implementation.
+ **
+ ** Sets theory implementation.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__SETS__THEORY_SETS_PRIVATE_H
+#define __CVC4__THEORY__SETS__THEORY_SETS_PRIVATE_H
+
+#include "context/cdhashset.h"
+#include "context/cdqueue.h"
+
+#include "theory/theory.h"
+#include "theory/uf/equality_engine.h"
+#include "theory/sets/term_info.h"
+
+namespace CVC4 {
+namespace theory {
+namespace sets {
+
+/** Internal classes, forward declared here */
+class TheorySetsTermInfoManager;
+class TheorySets;
+
+class TheorySetsPrivate {
+public:
+
+  /**
+   * Constructs a new instance of TheorySetsPrivate w.r.t. the provided
+   * contexts.
+   */
+  TheorySetsPrivate(TheorySets& external,
+                    context::Context* c,
+                    context::UserContext* u);
+
+  ~TheorySetsPrivate();
+
+  void check(Theory::Effort);
+
+  void propagate(Theory::Effort);
+
+  Node explain(TNode);
+
+  std::string identify() const { return "THEORY_SETS_PRIVATE"; }
+
+  void preRegisterTerm(TNode node);
+
+private:
+  TheorySets& d_external;
+
+  class Statistics {
+  public:
+    TimerStat d_checkTime;
+
+    Statistics();
+    ~Statistics();
+  } d_statistics;
+
+  /** Functions to handle callbacks from equality engine */
+  class NotifyClass : public eq::EqualityEngineNotify {
+    TheorySetsPrivate& d_theory;
+
+  public:
+    NotifyClass(TheorySetsPrivate& theory): d_theory(theory) {}
+    bool eqNotifyTriggerEquality(TNode equality, bool value);
+    bool eqNotifyTriggerPredicate(TNode predicate, bool value);
+    bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value);
+    void eqNotifyConstantTermMerge(TNode t1, TNode t2);
+    void eqNotifyNewClass(TNode t);
+    void eqNotifyPreMerge(TNode t1, TNode t2);
+    void eqNotifyPostMerge(TNode t1, TNode t2);
+    void eqNotifyDisequal(TNode t1, TNode t2, TNode reason);
+  } d_notify;
+
+  /** Equality engine */
+  eq::EqualityEngine d_equalityEngine;
+
+  context::CDO<bool> d_conflict;
+  Node d_conflictNode;
+
+  /** Proagate out to output channel */
+  bool propagate(TNode);
+
+  /** generate and send out conflict node */
+  void conflict(TNode, TNode);
+
+  class TermInfoManager {
+    TheorySetsPrivate& d_theory;
+    context::Context* d_context;
+    eq::EqualityEngine* d_eqEngine;
+
+    CDNodeSet d_terms;
+    std::hash_map<TNode, TheorySetsTermInfo*, TNodeHashFunction> d_info;
+
+    void mergeLists(CDTNodeList* la, const CDTNodeList* lb) const;
+    void pushToSettermPropagationQueue(CDTNodeList* l, TNode S, bool polarity);
+  public:
+    TermInfoManager(TheorySetsPrivate&,
+                    context::Context* satContext,
+                    eq::EqualityEngine*);
+    ~TermInfoManager();
+    void notifyMembership(TNode fact);
+    const CDTNodeList* getParents(TNode x);
+    void addTerm(TNode n);
+    void mergeTerms(TNode a, TNode b);
+  };
+  TermInfoManager* d_termInfoManager;
+
+  /** Assertions and helper functions */
+  bool present(TNode atom);
+  bool holds(TNode lit) {
+    bool polarity = lit.getKind() == kind::NOT ? false : true;
+    TNode atom = polarity ? lit : lit[0];
+    return holds(atom, polarity);
+  }
+  bool holds(TNode atom, bool polarity);
+
+  void assertEquality(TNode fact, TNode reason, bool learnt);
+  void assertMemebership(TNode fact, TNode reason, bool learnt);
+
+  /** Propagation / learning and helper functions. */
+  context::CDQueue< std::pair<Node, Node> > d_propagationQueue;
+  context::CDQueue< std::pair<TNode, TNode> > d_settermPropagationQueue;
+
+  void doSettermPropagation(TNode x, TNode S);
+  void registerReason(TNode reason, bool save);
+  void learnLiteral(TNode atom, bool polarity, Node reason);
+  void learnLiteral(TNode lit, Node reason) {
+    if(lit.getKind() == kind::NOT) {
+      learnLiteral(lit[0], false, reason);
+    } else {
+      learnLiteral(lit, true, reason);
+    }
+  }
+  void finishPropagation();
+
+  // for any nodes we need to save, because others use TNode
+  context::CDHashSet <Node, NodeHashFunction> d_nodeSaver;
+
+  /** Lemmas and helper functions */
+  context::CDQueue <TNode> d_pending;
+  context::CDQueue <TNode> d_pendingDisequal;
+  context::CDHashSet <Node, NodeHashFunction> d_pendingEverInserted;
+
+  void addToPending(Node n);
+  bool isComplete();
+  Node getLemma();
+};/* class TheorySetsPrivate */
+
+}/* CVC4::theory::sets namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__SETS__THEORY_SETS_PRIVATE_H */
diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp
new file mode 100644
index 000000000..11a2e9297
--- /dev/null
+++ b/src/theory/sets/theory_sets_rewriter.cpp
@@ -0,0 +1,110 @@
+#include "theory/sets/theory_sets_rewriter.h"
+
+namespace CVC4 {
+namespace theory {
+namespace sets {
+
+bool checkConstantMembership(TNode elementTerm, TNode setTerm)
+{
+  switch(setTerm.getKind()) {
+  case kind::EMPTYSET:
+    return false;
+  case kind::SET_SINGLETON:
+    return elementTerm == setTerm[0];
+  case kind::UNION:
+    return checkConstantMembership(elementTerm, setTerm[0]) ||
+      checkConstantMembership(elementTerm, setTerm[1]);
+  case kind::INTERSECTION:
+    return checkConstantMembership(elementTerm, setTerm[0]) &&
+      checkConstantMembership(elementTerm, setTerm[1]);
+  case kind::SETMINUS:
+    return checkConstantMembership(elementTerm, setTerm[0]) &&
+      !checkConstantMembership(elementTerm, setTerm[1]);
+  default:
+    Unhandled();
+  }
+}
+
+// static
+RewriteResponse TheorySetsRewriter::postRewrite(TNode node) {
+  NodeManager* nm = NodeManager::currentNM();
+
+  switch(node.getKind()) {
+
+  case kind::IN: {
+    if(!node[0].isConst() || !node[1].isConst())
+      break;
+
+    // both are constants
+    bool isMember = checkConstantMembership(node[0], node[1]);
+    return RewriteResponse(REWRITE_DONE, nm->mkConst(isMember));
+  }
+
+  case kind::SUBSET: {
+    // rewrite (A subset-or-equal B) as (A union B = B)
+    TNode A = node[0];
+    TNode B = node[1];
+    return RewriteResponse(REWRITE_AGAIN,
+                           nm->mkNode(kind::EQUAL,
+                                      nm->mkNode(kind::UNION, A, B),
+                                      B) );
+  }//kind::SUBSET
+
+  case kind::EQUAL:
+  case kind::IFF: {
+    //rewrite: t = t with true (t term)
+    //rewrite: c = c' with c different from c' false (c, c' constants)
+    //otherwise: sort them
+    if(node[0] == node[1]) {
+      Trace("sets-postrewrite") << "Sets::postRewrite returning true" << std::endl;
+      return RewriteResponse(REWRITE_DONE, nm->mkConst(true));
+    }
+    else if (node[0].isConst() && node[1].isConst()) {
+      Trace("sets-postrewrite") << "Sets::postRewrite returning false" << std::endl;
+      return RewriteResponse(REWRITE_DONE, nm->mkConst(false));
+    }
+    else if (node[0] > node[1]) {
+      Node newNode = nm->mkNode(node.getKind(), node[1], node[0]);
+      Trace("sets-postrewrite") << "Sets::postRewrite returning " << newNode << std::endl;
+      return RewriteResponse(REWRITE_DONE, newNode);
+    }
+    break;
+  }
+
+  case kind::UNION:
+  case kind::INTERSECTION: {
+    if(node[0] == node[1]) {
+      Trace("sets-postrewrite") << "Sets::postRewrite returning " << node[0] << std::endl;
+      return RewriteResponse(REWRITE_DONE, node[0]);
+    } else if (node[0] > node[1]) {
+      Node newNode = nm->mkNode(node.getKind(), node[1], node[0]);
+      Trace("sets-postrewrite") << "Sets::postRewrite returning " << newNode << std::endl;
+      return RewriteResponse(REWRITE_DONE, newNode);
+    }
+    break;
+  }
+
+  default:
+    break;
+
+  }//switch(node.getKind())
+
+  // This default implementation
+  return RewriteResponse(REWRITE_DONE, node);
+}
+
+// static
+RewriteResponse TheorySetsRewriter::preRewrite(TNode node) {
+  NodeManager* nm = NodeManager::currentNM();
+
+  // do nothing
+  if(node.getKind() == kind::EQUAL && node[0] == node[1])
+    return RewriteResponse(REWRITE_DONE, nm->mkConst(true));
+  // Further optimization, if constants but differing ones
+
+  return RewriteResponse(REWRITE_DONE, node);
+}
+
+}/* CVC4::theory::sets namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
diff --git a/src/theory/sets/theory_sets_rewriter.h b/src/theory/sets/theory_sets_rewriter.h
new file mode 100644
index 000000000..f01d198cf
--- /dev/null
+++ b/src/theory/sets/theory_sets_rewriter.h
@@ -0,0 +1,77 @@
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__SETS__THEORY_SETS_REWRITER_H
+#define __CVC4__THEORY__SETS__THEORY_SETS_REWRITER_H
+
+#include "theory/rewriter.h"
+
+namespace CVC4 {
+namespace theory {
+namespace sets {
+
+class TheorySetsRewriter {
+public:
+
+  /**
+   * Rewrite a node into the normal form for the theory of sets.
+   * Called in post-order (really reverse-topological order) when
+   * traversing the expression DAG during rewriting.  This is the
+   * main function of the rewriter, and because of the ordering,
+   * it can assume its children are all rewritten already.
+   *
+   * This function can return one of three rewrite response codes
+   * along with the rewritten node:
+   *
+   *   REWRITE_DONE indicates that no more rewriting is needed.
+   *   REWRITE_AGAIN means that the top-level expression should be
+   *     rewritten again, but that its children are in final form.
+   *   REWRITE_AGAIN_FULL means that the entire returned expression
+   *     should be rewritten again (top-down with preRewrite(), then
+   *     bottom-up with postRewrite()).
+   *
+   * Even if this function returns REWRITE_DONE, if the returned
+   * expression belongs to a different theory, it will be fully
+   * rewritten by that theory's rewriter.
+   */
+  static RewriteResponse postRewrite(TNode node);
+
+  /**
+   * Rewrite a node into the normal form for the theory of sets
+   * in pre-order (really topological order)---meaning that the
+   * children may not be in the normal form.  This is an optimization
+   * for theories with cancelling terms (e.g., 0 * (big-nasty-expression)
+   * in arithmetic rewrites to 0 without the need to look at the big
+   * nasty expression).  Since it's only an optimization, the
+   * implementation here can do nothing.
+   */
+  static RewriteResponse preRewrite(TNode node);
+
+  /**
+   * Rewrite an equality, in case special handling is required.
+   */
+  static Node rewriteEquality(TNode equality) {
+    // often this will suffice
+    return postRewrite(equality).node;
+  }
+
+  /**
+   * Initialize the rewriter.
+   */
+  static inline void init() {
+    // nothing to do
+  }
+
+  /**
+   * Shut down the rewriter.
+   */
+  static inline void shutdown() {
+    // nothing to do
+  }
+
+};/* class TheorySetsRewriter */
+
+}/* CVC4::theory::sets namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__SETS__THEORY_SETS_REWRITER_H */
diff --git a/src/theory/sets/theory_sets_type_enumerator.h b/src/theory/sets/theory_sets_type_enumerator.h
new file mode 100644
index 000000000..2f4cc6a2f
--- /dev/null
+++ b/src/theory/sets/theory_sets_type_enumerator.h
@@ -0,0 +1,161 @@
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__SETS__TYPE_ENUMERATOR_H
+#define __CVC4__THEORY__SETS__TYPE_ENUMERATOR_H
+
+#include "theory/type_enumerator.h"
+#include "expr/type_node.h"
+#include "expr/kind.h"
+#include "theory/rewriter.h"
+
+namespace CVC4 {
+namespace theory {
+namespace sets {
+
+class SetEnumerator : public TypeEnumeratorBase<SetEnumerator> {
+  unsigned d_index;
+  TypeNode d_constituentType;
+  NodeManager* d_nm;
+  std::vector<bool> d_indexVec;
+  std::vector<TypeEnumerator*> d_constituentVec;
+  bool d_finished;
+  Node d_setConst;
+
+public:
+
+  SetEnumerator(TypeNode type) throw(AssertionException) :
+    TypeEnumeratorBase<SetEnumerator>(type),
+    d_index(0),
+    d_constituentType(type.getSetElementType()),
+    d_nm(NodeManager::currentNM()),
+    d_indexVec(),
+    d_constituentVec(),
+    d_finished(false),
+    d_setConst()
+  {
+    // d_indexVec.push_back(false);
+    // d_constituentVec.push_back(new TypeEnumerator(d_constituentType));
+    d_setConst = d_nm->mkConst(EmptySet(type.toType()));
+  }
+
+  // An set enumerator could be large, and generally you don't want to
+  // go around copying these things; but a copy ctor is presently required
+  // by the TypeEnumerator framework.
+  SetEnumerator(const SetEnumerator& ae) throw() :
+    TypeEnumeratorBase<SetEnumerator>(ae.d_nm->mkSetType(ae.d_constituentType)),
+    d_constituentType(ae.d_constituentType),
+    d_nm(ae.d_nm),
+    d_indexVec(ae.d_indexVec),
+    d_constituentVec(),// copied below
+    d_finished(ae.d_finished),
+    d_setConst(ae.d_setConst)
+  {
+    for(std::vector<TypeEnumerator*>::const_iterator i =
+          ae.d_constituentVec.begin(), i_end = ae.d_constituentVec.end();
+        i != i_end;
+        ++i) {
+      d_constituentVec.push_back(new TypeEnumerator(**i));
+    }
+  }
+
+  ~SetEnumerator() {
+    while (!d_constituentVec.empty()) {
+      delete d_constituentVec.back();
+      d_constituentVec.pop_back();
+    }
+  }
+
+  Node operator*() throw(NoMoreValuesException) {
+    if (d_finished) {
+      throw NoMoreValuesException(getType());
+    }
+    Node n = d_setConst;
+
+    // For now only support only sets of size 1
+    Assert(d_index == 0 || d_index == 1);
+
+    if(d_index == 1) {
+      n = d_nm->mkNode(kind::SET_SINGLETON, *(*(d_constituentVec[0])));
+    }
+
+    // for (unsigned i = 0; i < d_indexVec.size(); ++i) {
+    //   n = d_nm->mkNode(kind::STORE, n, d_indexVec[d_indexVec.size() - 1 - i], *(*(d_constituentVec[i])));
+    // }
+    Trace("set-type-enum") << "operator * prerewrite: " << n << std::endl;
+    n = Rewriter::rewrite(n);
+    Trace("set-type-enum") << "operator * returning: " << n << std::endl;
+    return n;
+  }
+
+  SetEnumerator& operator++() throw() {
+    Trace("set-type-enum") << "operator++ called, **this = " << **this << std::endl;
+
+    if (d_finished) {
+      Trace("set-type-enum") << "operator++ finished!" << std::endl;
+      return *this;
+    }
+
+    // increment by one, at the same time deleting all elements that
+    // cannot be incremented any further (note: we are keeping a set
+    // -- no repetitions -- thus some trickery to know what to pop and
+    // what not to.)
+    if(d_index > 0) {
+      Assert(d_index == d_constituentVec.size());
+
+      Node last_pre_increment;
+      last_pre_increment = *(*d_constituentVec.back());
+
+      ++(*d_constituentVec.back());
+
+      if (d_constituentVec.back()->isFinished()) {
+        delete d_constituentVec.back();
+        d_constituentVec.pop_back();
+
+        while(!d_constituentVec.empty()) {
+          Node cur_pre_increment = *(*d_constituentVec.back());
+          ++(*d_constituentVec.back());
+          Node cur_post_increment = *(*d_constituentVec.back());
+          if(last_pre_increment == cur_post_increment) {
+            delete d_constituentVec.back();
+            d_constituentVec.pop_back();
+            last_pre_increment = cur_pre_increment;
+          } else {
+            break;
+          }
+        }
+      }
+    }
+
+    if (d_constituentVec.empty()) {
+      ++d_index;
+      d_constituentVec.push_back(new TypeEnumerator(d_constituentType));
+    }
+
+    while (d_constituentVec.size() < d_index) {
+      TypeEnumerator *d_newEnumerator = new TypeEnumerator(*d_constituentVec.back());
+      ++(*d_newEnumerator);
+      if( (*d_newEnumerator).isFinished() ) {
+        Trace("set-type-enum") << "operator++ finished!" << std::endl;
+        d_finished = true;
+        return *this;
+      }
+      d_constituentVec.push_back(d_newEnumerator);
+    }
+
+    Trace("set-type-enum") << "operator++ returning, **this = " << **this << std::endl;
+    return *this;
+  }
+
+  bool isFinished() throw() {
+    Trace("set-type-enum") << "isFinished returning: " << d_finished << std::endl;
+    return d_finished;
+  }
+
+};/* class SetEnumerator */
+
+}/* CVC4::theory::sets namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__SETS__TYPE_ENUMERATOR_H */
diff --git a/src/theory/sets/theory_sets_type_rules.h b/src/theory/sets/theory_sets_type_rules.h
new file mode 100644
index 000000000..026c90ca4
--- /dev/null
+++ b/src/theory/sets/theory_sets_type_rules.h
@@ -0,0 +1,176 @@
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__SETS__THEORY_SETS_TYPE_RULES_H
+#define __CVC4__THEORY__SETS__THEORY_SETS_TYPE_RULES_H
+
+namespace CVC4 {
+namespace theory {
+namespace sets {
+
+class SetsTypeRule {
+public:
+
+  /**
+   * Compute the type for (and optionally typecheck) a term belonging
+   * to the theory of sets.
+   *
+   * @param check if true, the node's type should be checked as well
+   * as computed.
+   */
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
+                                     bool check)
+    throw (TypeCheckingExceptionPrivate) {
+
+    // TODO: implement me!
+    Unimplemented();
+
+  }
+
+};/* class SetsTypeRule */
+
+// TODO: Union, Intersection and Setminus should be combined to one check
+struct SetUnionTypeRule {
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+    throw (TypeCheckingExceptionPrivate, AssertionException) {
+    Assert(n.getKind() == kind::UNION);
+    TypeNode setType = n[0].getType(check);
+    if( check ) {
+      if(!setType.isSet()) {
+        throw TypeCheckingExceptionPrivate(n, "set union operating on non-set");
+      }
+      TypeNode secondSetType = n[1].getType(check);
+      if(secondSetType != setType) {
+        throw TypeCheckingExceptionPrivate(n, "set union operating on sets of different types");
+      }
+    }
+    return setType;
+  }
+};/* struct SetUnionTypeRule */
+
+struct SetIntersectionTypeRule {
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+    throw (TypeCheckingExceptionPrivate, AssertionException) {
+    Assert(n.getKind() == kind::INTERSECTION);
+    TypeNode setType = n[0].getType(check);
+    if( check ) {
+      if(!setType.isSet()) {
+        throw TypeCheckingExceptionPrivate(n, "set intersection operating on non-set");
+      }
+      TypeNode secondSetType = n[1].getType(check);
+      if(secondSetType != setType) {
+        throw TypeCheckingExceptionPrivate(n, "set intersection operating on sets of different types");
+      }
+    }
+    return setType;
+  }
+};/* struct SetIntersectionTypeRule */
+
+struct SetSetminusTypeRule {
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+    throw (TypeCheckingExceptionPrivate, AssertionException) {
+    Assert(n.getKind() == kind::SETMINUS);
+    TypeNode setType = n[0].getType(check);
+    if( check ) {
+      if(!setType.isSet()) {
+        throw TypeCheckingExceptionPrivate(n, "set setminus operating on non-set");
+      }
+      TypeNode secondSetType = n[1].getType(check);
+      if(secondSetType != setType) {
+        throw TypeCheckingExceptionPrivate(n, "set setminus operating on sets of different types");
+      }
+    }
+    return setType;
+  }
+};/* struct SetSetminusTypeRule */
+
+struct SetSubsetTypeRule {
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+    throw (TypeCheckingExceptionPrivate, AssertionException) {
+    Assert(n.getKind() == kind::SUBSET);
+    TypeNode setType = n[0].getType(check);
+    if( check ) {
+      if(!setType.isSet()) {
+        throw TypeCheckingExceptionPrivate(n, "set subset operating on non-set");
+      }
+      TypeNode secondSetType = n[1].getType(check);
+      if(secondSetType != setType) {
+        throw TypeCheckingExceptionPrivate(n, "set subset operating on sets of different types");
+      }
+    }
+    return nodeManager->booleanType();
+  }
+};/* struct SetSubsetTypeRule */
+
+struct SetInTypeRule {
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+    throw (TypeCheckingExceptionPrivate, AssertionException) {
+    Assert(n.getKind() == kind::IN);
+    TypeNode setType = n[1].getType(check);
+    if( check ) {
+      if(!setType.isSet()) {
+        throw TypeCheckingExceptionPrivate(n, "checking for membership in a non-set");
+      }
+      TypeNode elementType = n[0].getType(check);
+      if(elementType != setType.getSetElementType()) {
+        throw TypeCheckingExceptionPrivate(n, "set in operating on sets of different types");
+      }
+    }
+    return nodeManager->booleanType();
+  }
+};/* struct SetInTypeRule */
+
+struct SetSingletonTypeRule {
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+    throw (TypeCheckingExceptionPrivate, AssertionException) {
+    Assert(n.getKind() == kind::SET_SINGLETON);
+    return nodeManager->mkSetType(n[0].getType(check));
+  }
+};/* struct SetInTypeRule */
+
+struct SetConstTypeRule {
+  inline static bool computeIsConst(NodeManager* nodeManager, TNode n) {
+    switch(n.getKind()) {
+    case kind::SET_SINGLETON:
+      return n[0].isConst();
+    case kind::UNION:
+      return n[0].isConst() && n[1].isConst();
+    default:
+      Unhandled();
+    }
+  }
+};
+
+struct EmptySetTypeRule {
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+    throw (TypeCheckingExceptionPrivate, AssertionException) {
+
+    Assert(n.getKind() == kind::EMPTYSET);
+    EmptySet emptySet = n.getConst<EmptySet>();
+    Type setType = emptySet.getType();
+    return TypeNode::fromType(setType);
+  }
+};
+
+
+struct SetsProperties {
+  inline static Cardinality computeCardinality(TypeNode type) {
+    Assert(type.getKind() == kind::SET_TYPE);
+    Cardinality elementCard = type[0].getCardinality();
+    return elementCard;
+  }
+
+  inline static bool isWellFounded(TypeNode type) {
+    return type[0].isWellFounded();
+  }
+
+  inline static Node mkGroundTerm(TypeNode type) {
+    Assert(type.isSet());
+    return NodeManager::currentNM()->mkConst(EmptySet(type.toType()));
+  }
+};
+
+}/* CVC4::theory::sets namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__SETS__THEORY_SETS_TYPE_RULES_H */
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 2359d5d86..e8d53e539 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -620,6 +620,9 @@ public:
    * check() or propagate() method called.  A Theory may empty its
    * assertFact() queue using get().  A Theory can raise conflicts,
    * add lemmas, and propagate literals during presolve().
+   *
+   * NOTE: The presolve property must be added to the kinds file for
+   * the theory.
    */
   virtual void presolve() { }
 
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 47ba50aad..63024e5d5 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -671,6 +671,7 @@ bool TheoryEngine::presolve() {
 void TheoryEngine::postsolve() {
   // Reset the interrupt flag
   d_interrupted = false;
+  bool CVC4_UNUSED wasInConflict = d_inConflict;
 
   try {
     // Definition of the statement that is to be run by every theory
@@ -680,7 +681,7 @@ void TheoryEngine::postsolve() {
 #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
     if (theory::TheoryTraits<THEORY>::hasPostsolve) { \
       theoryOf(THEORY)->postsolve(); \
-      Assert(! d_inConflict, "conflict raised during postsolve()"); \
+      Assert(! d_inConflict || wasInConflict, "conflict raised during postsolve()"); \
     }
 
     // Postsolve for each theory using the statement above
@@ -961,7 +962,7 @@ void TheoryEngine::assertToTheory(TNode assertion, TNode originalAssertion, theo
       bool value;
       if (d_propEngine->hasValue(assertion, value)) {
         if (!value) {
-          Trace("theory::propagate") << "TheoryEngine::assertToTheory(" << assertion << ", " << toTheoryId << ", " << fromTheoryId << "): conflict" << endl;
+          Trace("theory::propagate") << "TheoryEngine::assertToTheory(" << assertion << ", " << toTheoryId << ", " << fromTheoryId << "): conflict (no sharing)" << endl;
           d_inConflict = true;
         } else {
           return;
@@ -1011,6 +1012,7 @@ void TheoryEngine::assertToTheory(TNode assertion, TNode originalAssertion, theo
       // Check for propositional conflicts
       bool value;
       if (d_propEngine->hasValue(assertion, value) && !value) {
+          Trace("theory::propagate") << "TheoryEngine::assertToTheory(" << assertion << ", " << toTheoryId << ", " << fromTheoryId << "): conflict (sharing)" << endl;
         d_inConflict = true;
       }
     }
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index f8e361081..8bb849496 100644
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -833,12 +833,14 @@ public:
   void addTriggerPredicate(TNode predicate);
 
   /**
-   * Returns true if the two are currently in the database and equal.
+   * Returns true if the two terms are equal. Requires both terms to
+   * be in the database.
    */
   bool areEqual(TNode t1, TNode t2) const;
 
   /**
-   * Check whether the two term are dis-equal.
+   * Check whether the two term are dis-equal. Requires both terms to
+   * be in the database.
    */
   bool areDisequal(TNode t1, TNode t2, bool ensureProof) const;
 
diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index 1d6ce1a73..0717df907 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -87,6 +87,8 @@ libutil_la_SOURCES = \
 	abstract_value.cpp \
 	array_store_all.h \
 	array_store_all.cpp \
+	emptyset.h \
+	emptyset.cpp \
 	model.h \
 	model.cpp \
 	sort_inference.h \
diff --git a/src/util/emptyset.cpp b/src/util/emptyset.cpp
new file mode 100644
index 000000000..fa1bb8f10
--- /dev/null
+++ b/src/util/emptyset.cpp
@@ -0,0 +1,12 @@
+#include "util/emptyset.h"
+#include <iostream>
+
+using namespace std;
+
+namespace CVC4 {
+
+std::ostream& operator<<(std::ostream& out, const EmptySet& asa) {
+  return out << "emptyset(" << asa.getType() << ')';
+}
+
+}/* CVC4 namespace */
diff --git a/src/util/emptyset.h b/src/util/emptyset.h
new file mode 100644
index 000000000..aae08e43b
--- /dev/null
+++ b/src/util/emptyset.h
@@ -0,0 +1,65 @@
+
+#include "cvc4_public.h"
+
+#pragma once
+
+namespace CVC4 {
+  // messy; Expr needs ArrayStoreAll (because it's the payload of a
+  // CONSTANT-kinded expression), and ArrayStoreAll needs Expr.
+  class CVC4_PUBLIC EmptySet;
+}/* CVC4 namespace */
+
+#include "expr/expr.h"
+#include "expr/type.h"
+#include <iostream>
+
+namespace CVC4 {
+
+class CVC4_PUBLIC EmptySet {
+
+  const SetType d_type;
+
+public:
+
+  EmptySet() { }		/* Null typed */
+  EmptySet(SetType t):d_type(t) { }
+
+
+  ~EmptySet() throw() {
+  }
+
+  SetType getType() const { return d_type; }
+
+  bool operator==(const EmptySet& asa) const throw() {
+    return d_type == asa.d_type;
+  }
+  bool operator!=(const EmptySet& asa) const throw() {
+    return !(*this == asa);
+  }
+
+  bool operator<(const EmptySet& asa) const throw() {
+    return d_type < asa.d_type;
+  }
+  bool operator<=(const EmptySet& asa) const throw() {
+    return d_type <= asa.d_type;
+  }
+  bool operator>(const EmptySet& asa) const throw() {
+    return !(*this <= asa);
+  }
+  bool operator>=(const EmptySet& asa) const throw() {
+    return !(*this < asa);
+  }
+
+
+};/* class EmptySet */
+
+std::ostream& operator<<(std::ostream& out, const EmptySet& asa) CVC4_PUBLIC;
+
+struct CVC4_PUBLIC EmptySetHashFunction {
+  inline size_t operator()(const EmptySet& asa) const {
+    return TypeHashFunction()(asa.getType());
+  }
+};/* struct EmptysetHashFunction */
+
+
+}
diff --git a/test/Makefile.am b/test/Makefile.am
index 8a7a5a0a7..1da15dc43 100644
--- a/test/Makefile.am
+++ b/test/Makefile.am
@@ -56,6 +56,7 @@ subdirs_to_check = \
 	regress/regress0/decision \
 	regress/regress0/fmf \
 	regress/regress0/strings \
+	regress/regress0/sets \
 	regress/regress1 \
 	regress/regress1/arith \
 	regress/regress2 \
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index d7663e298..067b5d381 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -1,5 +1,5 @@
-SUBDIRS = . arith precedence uf uflra uflia bv arrays aufbv auflia datatypes quantifiers rewriterules lemmas push-pop preprocess tptp unconstrained decision fmf strings
-DIST_SUBDIRS = . arith precedence uf uflra uflia bv arrays aufbv auflia datatypes quantifiers rewriterules lemmas push-pop preprocess tptp unconstrained decision fmf strings
+SUBDIRS = . arith precedence uf uflra uflia bv arrays aufbv auflia datatypes quantifiers rewriterules lemmas push-pop preprocess tptp unconstrained decision fmf strings sets
+DIST_SUBDIRS = $(SUBDIRS) #. arith precedence uf uflra uflia bv arrays aufbv auflia datatypes quantifiers rewriterules lemmas push-pop preprocess tptp unconstrained decision fmf strings sets
 
 # don't override a BINARY imported from a personal.mk
 @mk_if@eq ($(BINARY),)
diff --git a/test/regress/regress0/quantifiers/set8.smt2 b/test/regress/regress0/quantifiers/set8.smt2
index 684d94b7a..6e4a84672 100644
--- a/test/regress/regress0/quantifiers/set8.smt2
+++ b/test/regress/regress0/quantifiers/set8.smt2
@@ -1,26 +1,26 @@
 (set-logic AUFLIA)
-(set-info :source | Set theory. |)
+(set-info :source | mySet theory. |)
 (set-info :smt-lib-version 2.0)
 (set-info :category "crafted")
 (set-info :status unsat)
-(declare-sort Set 0)
+(declare-sort mySet 0)
 (declare-sort Elem 0)
-(declare-fun member (Elem Set) Bool)
-(declare-fun subset (Set Set) Bool)
-(assert (forall ((?x Elem) (?s1 Set) (?s2 Set)) (=> (and (member ?x ?s1) (subset ?s1 ?s2)) (member ?x ?s2))))
-(assert (forall ((?s1 Set) (?s2 Set)) (=> (not (subset ?s1 ?s2)) (exists ((?x Elem)) (and (member ?x ?s1) (not (member ?x ?s2)))))))
-(assert (forall ((?s1 Set) (?s2 Set)) (=> (forall ((?x Elem)) (=> (member ?x ?s1) (member ?x ?s2))) (subset ?s1 ?s2))))
-(declare-fun seteq (Set Set) Bool)
-(assert (forall ((?s1 Set) (?s2 Set)) (= (seteq ?s1 ?s2) (= ?s1 ?s2))))
-(assert (forall ((?s1 Set) (?s2 Set)) (= (seteq ?s1 ?s2) (and (subset ?s1 ?s2) (subset ?s2 ?s1)))))
-(declare-fun union (Set Set) Set)
-(assert (forall ((?x Elem) (?s1 Set) (?s2 Set)) (= (member ?x (union ?s1 ?s2)) (or (member ?x ?s1) (member ?x ?s2)))))
-(declare-fun intersection (Set Set) Set)
-(assert (forall ((?x Elem) (?s1 Set) (?s2 Set)) (= (member ?x (intersection ?s1 ?s2)) (and (member ?x ?s1) (member ?x ?s2)))))
-(declare-fun difference (Set Set) Set)
-(assert (forall ((?x Elem) (?s1 Set) (?s2 Set)) (= (member ?x (difference ?s1 ?s2)) (and (member ?x ?s1) (not (member ?x ?s2))))))
-(declare-fun a () Set)
-(declare-fun b () Set)
-(assert (not (seteq (intersection a b) (intersection b a))))
+(declare-fun member (Elem mySet) Bool)
+(declare-fun subset (mySet mySet) Bool)
+(assert (forall ((?x Elem) (?s1 mySet) (?s2 mySet)) (=> (and (member ?x ?s1) (subset ?s1 ?s2)) (member ?x ?s2))))
+(assert (forall ((?s1 mySet) (?s2 mySet)) (=> (not (subset ?s1 ?s2)) (exists ((?x Elem)) (and (member ?x ?s1) (not (member ?x ?s2)))))))
+(assert (forall ((?s1 mySet) (?s2 mySet)) (=> (forall ((?x Elem)) (=> (member ?x ?s1) (member ?x ?s2))) (subset ?s1 ?s2))))
+(declare-fun seteq (mySet mySet) Bool)
+(assert (forall ((?s1 mySet) (?s2 mySet)) (= (seteq ?s1 ?s2) (= ?s1 ?s2))))
+(assert (forall ((?s1 mySet) (?s2 mySet)) (= (seteq ?s1 ?s2) (and (subset ?s1 ?s2) (subset ?s2 ?s1)))))
+(declare-fun myunion (mySet mySet) mySet)
+(assert (forall ((?x Elem) (?s1 mySet) (?s2 mySet)) (= (member ?x (myunion ?s1 ?s2)) (or (member ?x ?s1) (member ?x ?s2)))))
+(declare-fun myintersection (mySet mySet) mySet)
+(assert (forall ((?x Elem) (?s1 mySet) (?s2 mySet)) (= (member ?x (myintersection ?s1 ?s2)) (and (member ?x ?s1) (member ?x ?s2)))))
+(declare-fun difference (mySet mySet) mySet)
+(assert (forall ((?x Elem) (?s1 mySet) (?s2 mySet)) (= (member ?x (difference ?s1 ?s2)) (and (member ?x ?s1) (not (member ?x ?s2))))))
+(declare-fun a () mySet)
+(declare-fun b () mySet)
+(assert (not (seteq (myintersection a b) (myintersection b a))))
 (check-sat)
 (exit)
diff --git a/test/regress/regress0/rewriterules/set_A_new_fast_tableau-base.smt2 b/test/regress/regress0/rewriterules/set_A_new_fast_tableau-base.smt2
index 9bd49f714..56228e082 100644
--- a/test/regress/regress0/rewriterules/set_A_new_fast_tableau-base.smt2
+++ b/test/regress/regress0/rewriterules/set_A_new_fast_tableau-base.smt2
@@ -2,124 +2,124 @@
 (set-logic AUFLIA)
 (set-info :status unsat)
 
-;; don't use a datatypes for currently focusing in uf
+;; don't use a datatypes for currently focusing my_in uf
 (declare-sort elt 0)
 (declare-sort set 0)
 
-(declare-fun in (elt set) Bool)
+(declare-fun my_in (elt set) Bool)
 
 ;;;;;;;;;;;;;;;;;;;;
 ;; inter
 
 (declare-fun inter (set set)  set)
 (assert-propagation ((?s elt) (?t1 set) (?t2 set)) () ()
-                  ((in ?s (inter ?t1 ?t2))) (and (in ?s ?t1) (in ?s ?t2)))
+                  ((my_in ?s (inter ?t1 ?t2))) (and (my_in ?s ?t1) (my_in ?s ?t2)))
 
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                   (((inter ?t1 ?t2))) () ((not (in ?s ?t1))) (not (in ?s (inter ?t1 ?t2))) )
+                   (((inter ?t1 ?t2))) () ((not (my_in ?s ?t1))) (not (my_in ?s (inter ?t1 ?t2))) )
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                   (((inter ?t1 ?t2))) () ((not (in ?s ?t2))) (not (in ?s (inter ?t1 ?t2))) )
+                   (((inter ?t1 ?t2))) () ((not (my_in ?s ?t2))) (not (my_in ?s (inter ?t1 ?t2))) )
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                   () () ((not (in ?s (inter ?t1 ?t2))) (in ?s ?t1)) (not (in ?s ?t2)) )
+                   () () ((not (my_in ?s (inter ?t1 ?t2))) (my_in ?s ?t1)) (not (my_in ?s ?t2)) )
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                   () () ((not (in ?s (inter ?t1 ?t2))) (in ?s ?t2)) (not (in ?s ?t1)))
+                   () () ((not (my_in ?s (inter ?t1 ?t2))) (my_in ?s ?t2)) (not (my_in ?s ?t1)))
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                   (((inter ?t1 ?t2))) () ((in ?s ?t1) (in ?s ?t2)) (in ?s (inter ?t1 ?t2)) )
+                   (((inter ?t1 ?t2))) () ((my_in ?s ?t1) (my_in ?s ?t2)) (my_in ?s (inter ?t1 ?t2)) )
 
 ;;;;;;;;;;;;;;;;;
 ;; union
 
-(declare-fun union (set set)  set)
+(declare-fun my_union (set set)  set)
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                   () () ((not (in ?s (union ?t1 ?t2)))) (and (not (in ?s ?t1)) (not (in ?s ?t2))))
+                   () () ((not (my_in ?s (my_union ?t1 ?t2)))) (and (not (my_in ?s ?t1)) (not (my_in ?s ?t2))))
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                   (((union ?t1 ?t2))) () ((in ?s ?t1)) (in ?s (union ?t1 ?t2)))
+                   (((my_union ?t1 ?t2))) () ((my_in ?s ?t1)) (my_in ?s (my_union ?t1 ?t2)))
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                   (((union ?t1 ?t2))) () ((in ?s ?t2)) (in ?s (union ?t1 ?t2)))
+                   (((my_union ?t1 ?t2))) () ((my_in ?s ?t2)) (my_in ?s (my_union ?t1 ?t2)))
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                   () () ((in ?s (union ?t1 ?t2)) (not (in ?s ?t1))) (in ?s ?t2))
+                   () () ((my_in ?s (my_union ?t1 ?t2)) (not (my_in ?s ?t1))) (my_in ?s ?t2))
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                   () () ((in ?s (union ?t1 ?t2)) (not (in ?s ?t2))) (in ?s ?t1))
+                   () () ((my_in ?s (my_union ?t1 ?t2)) (not (my_in ?s ?t2))) (my_in ?s ?t1))
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                   (((union ?t1 ?t2))) () ((not (in ?s ?t1)) (not (in ?s ?t2))) (not (in ?s (union ?t1 ?t2))))
+                   (((my_union ?t1 ?t2))) () ((not (my_in ?s ?t1)) (not (my_in ?s ?t2))) (not (my_in ?s (my_union ?t1 ?t2))))
 
 ;;;;;;;;;;;;;;;;;;;;
 ;; diff
 
 (declare-fun diff (set set)  set)
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                   () () ((in ?s (diff ?t1 ?t2))) (and (in ?s ?t1) (not (in ?s ?t2))))
+                   () () ((my_in ?s (diff ?t1 ?t2))) (and (my_in ?s ?t1) (not (my_in ?s ?t2))))
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                   (((diff ?t1 ?t2))) () ((not (in ?s ?t1))) (not (in ?s (diff ?t1 ?t2))) )
+                   (((diff ?t1 ?t2))) () ((not (my_in ?s ?t1))) (not (my_in ?s (diff ?t1 ?t2))) )
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                   (((diff ?t1 ?t2))) () ((in ?s ?t2)) (not (in ?s (diff ?t1 ?t2))))
+                   (((diff ?t1 ?t2))) () ((my_in ?s ?t2)) (not (my_in ?s (diff ?t1 ?t2))))
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                   () () ((not (in ?s (diff ?t1 ?t2))) (in ?s ?t1)) (in ?s ?t2))
+                   () () ((not (my_in ?s (diff ?t1 ?t2))) (my_in ?s ?t1)) (my_in ?s ?t2))
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                   () () ((not (in ?s (diff ?t1 ?t2))) (not (in ?s ?t2))) (not (in ?s ?t1)))
+                   () () ((not (my_in ?s (diff ?t1 ?t2))) (not (my_in ?s ?t2))) (not (my_in ?s ?t1)))
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                   (((diff ?t1 ?t2))) () ((in ?s ?t1) (not (in ?s ?t2))) (in ?s (diff ?t1 ?t2)) )
+                   (((diff ?t1 ?t2))) () ((my_in ?s ?t1) (not (my_in ?s ?t2))) (my_in ?s (diff ?t1 ?t2)) )
 
 ;;;;;;;;;;;;;;;;
 ;;sing
 
 (declare-fun sing (elt)  set)
 (assert-propagation ((?s elt))
-                   (((sing ?s))) () () (in ?s (sing ?s)) )
+                   (((sing ?s))) () () (my_in ?s (sing ?s)) )
 
 (assert-propagation ((?s elt) (?t1 elt))
-                   () () ((in ?s (sing ?t1))) (= ?s ?t1))
+                   () () ((my_in ?s (sing ?t1))) (= ?s ?t1))
 
 (assert-propagation ((?s elt) (?t1 elt))
-                   () () ((not (in ?s (sing ?t1)))) (not (= ?s ?t1)))
+                   () () ((not (my_in ?s (sing ?t1)))) (not (= ?s ?t1)))
 
 ;;;;;;;;;;;;;;;;;;;
 ;; fullfiling runned at Full effort
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                   () () ((in ?s (union ?t1 ?t2))) (or (in ?s ?t1) (not (in ?s ?t1))))
+                   () () ((my_in ?s (my_union ?t1 ?t2))) (or (my_in ?s ?t1) (not (my_in ?s ?t1))))
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                   (((inter ?t1 ?t2))) () ((in ?s ?t1)) (or (in ?s ?t2) (not (in ?s ?t2))))
+                   (((inter ?t1 ?t2))) () ((my_in ?s ?t1)) (or (my_in ?s ?t2) (not (my_in ?s ?t2))))
 
 (assert-propagation ((?t1 set) (?t2 set))
-                   () () ((not (= ?t1 ?t2))) (exists ((?e elt)) (or (and (in ?e ?t1) (not (in ?e ?t2))) (and (not (in ?e ?t1)) (in ?e ?t2)))))
+                   () () ((not (= ?t1 ?t2))) (exists ((?e elt)) (or (and (my_in ?e ?t1) (not (my_in ?e ?t2))) (and (not (my_in ?e ?t1)) (my_in ?e ?t2)))))
 
 ;;;;;;;;;;;;;;;;;;;
 ;; shortcut
 (declare-fun subset (set set) Bool)
 (assert-reduction ((?t1 set) (?t2 set))
-                 () () ((subset ?t1 ?t2)) (= (union ?t1 ?t2) ?t2))
+                 () () ((subset ?t1 ?t2)) (= (my_union ?t1 ?t2) ?t2))
 
 (declare-fun e () elt)
 (declare-fun t1 () set)
 (declare-fun t2 () set)
 (declare-fun t3 () set)
 
-;;(assert (not (=> (in e (inter (union t1 t2) (union t1 t1))) (in e (union t1 t1)))))
-;;(assert (not (=> (in e (union t1 t1)) (in e t1))))
+;;(assert (not (=> (my_in e (inter (my_union t1 t2) (my_union t1 t1))) (my_in e (my_union t1 t1)))))
+;;(assert (not (=> (my_in e (my_union t1 t1)) (my_in e t1))))
 
 ;; hyp
-;;(assert (=> (in e (union t1 t1)) (in e t1)))
+;;(assert (=> (my_in e (my_union t1 t1)) (my_in e t1)))
 
-;;(assert (not (=> (in e (inter (union t1 t2) (union t1 t1))) (in e t1))))
+;;(assert (not (=> (my_in e (inter (my_union t1 t2) (my_union t1 t1))) (my_in e t1))))
 
-;;(assert (or (and (not (in e (union t1 (union t2 t3)))) (in e (union (union t1 t2) t3))) (and (in e (union t1 (union t2 t3))) (not (in e (union (union t1 t2) t3))))) )
-(assert (not (= (union t1 (union t2 t3)) (union (union t1 t2) t3))) )
+;;(assert (or (and (not (my_in e (my_union t1 (my_union t2 t3)))) (my_in e (my_union (my_union t1 t2) t3))) (and (my_in e (my_union t1 (my_union t2 t3))) (not (my_in e (my_union (my_union t1 t2) t3))))) )
+(assert (not (= (my_union t1 (my_union t2 t3)) (my_union (my_union t1 t2) t3))) )
 
 (check-sat)
 
diff --git a/test/regress/regress0/rewriterules/set_A_new_fast_tableau-base_sat.smt2 b/test/regress/regress0/rewriterules/set_A_new_fast_tableau-base_sat.smt2
index 4d65ffac5..2a7e59d6e 100644
--- a/test/regress/regress0/rewriterules/set_A_new_fast_tableau-base_sat.smt2
+++ b/test/regress/regress0/rewriterules/set_A_new_fast_tableau-base_sat.smt2
@@ -2,11 +2,11 @@
 (set-logic AUFLIA)
 (set-info :status sat)
 
-;; don't use a datatypes for currently focusing in uf
+;; don't use a datatypes for currently focusing my_in uf
 (declare-sort elt 0)
 (declare-sort set 0)
 
-(declare-fun in (elt set) Bool)
+(declare-fun my_in (elt set) Bool)
 
 
 ;;;;;;;;;;;;;;;;;;;;
@@ -14,112 +14,112 @@
 
 (declare-fun inter (set set)  set)
 (assert-propagation ((?s elt) (?t1 set) (?t2 set)) () ()
-                  ((in ?s (inter ?t1 ?t2))) (and (in ?s ?t1) (in ?s ?t2)))
+                  ((my_in ?s (inter ?t1 ?t2))) (and (my_in ?s ?t1) (my_in ?s ?t2)))
 
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                  (((inter ?t1 ?t2))) () ((not (in ?s ?t1))) (not (in ?s (inter ?t1 ?t2))) )
+                  (((inter ?t1 ?t2))) () ((not (my_in ?s ?t1))) (not (my_in ?s (inter ?t1 ?t2))) )
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                  (((inter ?t1 ?t2))) () ((not (in ?s ?t2))) (not (in ?s (inter ?t1 ?t2))) )
+                  (((inter ?t1 ?t2))) () ((not (my_in ?s ?t2))) (not (my_in ?s (inter ?t1 ?t2))) )
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                  () () ((not (in ?s (inter ?t1 ?t2))) (in ?s ?t1)) (not (in ?s ?t2)) )
+                  () () ((not (my_in ?s (inter ?t1 ?t2))) (my_in ?s ?t1)) (not (my_in ?s ?t2)) )
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                  () () ((not (in ?s (inter ?t1 ?t2))) (in ?s ?t2)) (not (in ?s ?t1)))
+                  () () ((not (my_in ?s (inter ?t1 ?t2))) (my_in ?s ?t2)) (not (my_in ?s ?t1)))
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                  (((inter ?t1 ?t2))) () ((in ?s ?t1) (in ?s ?t2)) (in ?s (inter ?t1 ?t2)) )
+                  (((inter ?t1 ?t2))) () ((my_in ?s ?t1) (my_in ?s ?t2)) (my_in ?s (inter ?t1 ?t2)) )
 
 ;;;;;;;;;;;;;;;;;
 ;; union
 
-(declare-fun union (set set)  set)
+(declare-fun my_union (set set)  set)
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                  () () ((not (in ?s (union ?t1 ?t2)))) (and (not (in ?s ?t1)) (not (in ?s ?t2))))
+                  () () ((not (my_in ?s (my_union ?t1 ?t2)))) (and (not (my_in ?s ?t1)) (not (my_in ?s ?t2))))
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                  (((union ?t1 ?t2))) () ((in ?s ?t1)) (in ?s (union ?t1 ?t2)))
+                  (((my_union ?t1 ?t2))) () ((my_in ?s ?t1)) (my_in ?s (my_union ?t1 ?t2)))
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                  (((union ?t1 ?t2))) () ((in ?s ?t2)) (in ?s (union ?t1 ?t2)))
+                  (((my_union ?t1 ?t2))) () ((my_in ?s ?t2)) (my_in ?s (my_union ?t1 ?t2)))
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                  () () ((in ?s (union ?t1 ?t2)) (not (in ?s ?t1))) (in ?s ?t2))
+                  () () ((my_in ?s (my_union ?t1 ?t2)) (not (my_in ?s ?t1))) (my_in ?s ?t2))
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                  () () ((in ?s (union ?t1 ?t2)) (not (in ?s ?t2))) (in ?s ?t1))
+                  () () ((my_in ?s (my_union ?t1 ?t2)) (not (my_in ?s ?t2))) (my_in ?s ?t1))
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                  (((union ?t1 ?t2))) () ((not (in ?s ?t1)) (not (in ?s ?t2))) (not (in ?s (union ?t1 ?t2))))
+                  (((my_union ?t1 ?t2))) () ((not (my_in ?s ?t1)) (not (my_in ?s ?t2))) (not (my_in ?s (my_union ?t1 ?t2))))
 
 ;;;;;;;;;;;;;;;;;;;;
 ;; diff
 
 (declare-fun diff (set set)  set)
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                  () () ((in ?s (diff ?t1 ?t2))) (and (in ?s ?t1) (not (in ?s ?t2))))
+                  () () ((my_in ?s (diff ?t1 ?t2))) (and (my_in ?s ?t1) (not (my_in ?s ?t2))))
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                  (((diff ?t1 ?t2))) () ((not (in ?s ?t1))) (not (in ?s (diff ?t1 ?t2))) )
+                  (((diff ?t1 ?t2))) () ((not (my_in ?s ?t1))) (not (my_in ?s (diff ?t1 ?t2))) )
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                  (((diff ?t1 ?t2))) () ((in ?s ?t2)) (not (in ?s (diff ?t1 ?t2))))
+                  (((diff ?t1 ?t2))) () ((my_in ?s ?t2)) (not (my_in ?s (diff ?t1 ?t2))))
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                  () () ((not (in ?s (diff ?t1 ?t2))) (in ?s ?t1)) (in ?s ?t2))
+                  () () ((not (my_in ?s (diff ?t1 ?t2))) (my_in ?s ?t1)) (my_in ?s ?t2))
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                  () () ((not (in ?s (diff ?t1 ?t2))) (not (in ?s ?t2))) (not (in ?s ?t1)))
+                  () () ((not (my_in ?s (diff ?t1 ?t2))) (not (my_in ?s ?t2))) (not (my_in ?s ?t1)))
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                  (((diff ?t1 ?t2))) () ((in ?s ?t1) (not (in ?s ?t2))) (in ?s (diff ?t1 ?t2)) )
+                  (((diff ?t1 ?t2))) () ((my_in ?s ?t1) (not (my_in ?s ?t2))) (my_in ?s (diff ?t1 ?t2)) )
 
 ;;;;;;;;;;;;;;;;
 ;;sing
 
 (declare-fun sing (elt)  set)
 (assert-propagation ((?s elt))
-                  (((sing ?s))) () () (in ?s (sing ?s)) )
+                  (((sing ?s))) () () (my_in ?s (sing ?s)) )
 
 (assert-propagation ((?s elt) (?t1 elt))
-                  () () ((in ?s (sing ?t1))) (= ?s ?t1))
+                  () () ((my_in ?s (sing ?t1))) (= ?s ?t1))
 
 (assert-propagation ((?s elt) (?t1 elt))
-                  () () ((not (in ?s (sing ?t1)))) (not (= ?s ?t1)))
+                  () () ((not (my_in ?s (sing ?t1)))) (not (= ?s ?t1)))
 
 ;;;;;;;;;;;;;;;;;;;
 ;; fullfiling runned at Full effort
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                  () () ((in ?s (union ?t1 ?t2))) (or (in ?s ?t1) (not (in ?s ?t1))))
+                  () () ((my_in ?s (my_union ?t1 ?t2))) (or (my_in ?s ?t1) (not (my_in ?s ?t1))))
 
 (assert-propagation ((?s elt) (?t1 set) (?t2 set))
-                  (((inter ?t1 ?t2))) () ((in ?s ?t1)) (or (in ?s ?t2) (not (in ?s ?t2))))
+                  (((inter ?t1 ?t2))) () ((my_in ?s ?t1)) (or (my_in ?s ?t2) (not (my_in ?s ?t2))))
 
 (assert-propagation ((?t1 set) (?t2 set))
-                  () () ((not (= ?t1 ?t2))) (exists ((?e elt)) (or (and (in ?e ?t1) (not (in ?e ?t2))) (and (not (in ?e ?t1)) (in ?e ?t2)))))
+                  () () ((not (= ?t1 ?t2))) (exists ((?e elt)) (or (and (my_in ?e ?t1) (not (my_in ?e ?t2))) (and (not (my_in ?e ?t1)) (my_in ?e ?t2)))))
 
 ;;;;;;;;;;;;;;;;;;;
 ;; shortcut
 (declare-fun subset (set set) Bool)
 (assert-reduction ((?t1 set) (?t2 set))
-                () () ((subset ?t1 ?t2)) (= (union ?t1 ?t2) ?t2))
+                () () ((subset ?t1 ?t2)) (= (my_union ?t1 ?t2) ?t2))
 
 (declare-fun e () elt)
 (declare-fun t1 () set)
 (declare-fun t2 () set)
 (declare-fun t3 () set)
 
-;;(assert (not (=> (in e (inter (union t1 t2) (union t1 t1))) (in e (union t1 t1)))))
-;;(assert (not (=> (in e (union t1 t1)) (in e t1))))
+;;(assert (not (=> (my_in e (inter (my_union t1 t2) (my_union t1 t1))) (my_in e (my_union t1 t1)))))
+;;(assert (not (=> (my_in e (my_union t1 t1)) (my_in e t1))))
 
 ;; hyp
-;;(assert (=> (in e (union t1 t1)) (in e t1)))
+;;(assert (=> (my_in e (my_union t1 t1)) (my_in e t1)))
 
-;;(assert (not (=> (in e (inter (union t1 t2) (union t1 t1))) (in e t1))))
+;;(assert (not (=> (my_in e (inter (my_union t1 t2) (my_union t1 t1))) (my_in e t1))))
 
-(assert (or (and (not (in e (union t1 (union t2 t3)))) (in e (union (union t1 t2) t3))) (and (in e (union t1 (union t2 t3))) (not (in e (union (union t2 t2) t3))))) )
+(assert (or (and (not (my_in e (my_union t1 (my_union t2 t3)))) (my_in e (my_union (my_union t1 t2) t3))) (and (my_in e (my_union t1 (my_union t2 t3))) (not (my_in e (my_union (my_union t2 t2) t3))))) )
 
 
 (check-sat)
diff --git a/test/regress/regress0/sets/Makefile b/test/regress/regress0/sets/Makefile
new file mode 100644
index 000000000..67ae35206
--- /dev/null
+++ b/test/regress/regress0/sets/Makefile
@@ -0,0 +1,8 @@
+topdir = ../../../..
+srcdir = test/regress/regress0/sets
+
+include $(topdir)/Makefile.subdir
+
+# synonyms for "check"
+.PHONY: test
+test: check
diff --git a/test/regress/regress0/sets/Makefile.am b/test/regress/regress0/sets/Makefile.am
new file mode 100644
index 000000000..f040a6cd0
--- /dev/null
+++ b/test/regress/regress0/sets/Makefile.am
@@ -0,0 +1,75 @@
+# don't override a BINARY imported from a personal.mk
+@mk_if@eq ($(BINARY),)
+@mk_empty@BINARY = cvc4
+end@mk_if@
+
+LOG_COMPILER = @srcdir@/../../run_regression
+AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT)
+
+if AUTOMAKE_1_11
+# old-style (pre-automake 1.12) test harness
+TESTS_ENVIRONMENT = \
+	$(TESTS_ENVIRONMENT) $(LOG_COMPILER) \
+	$(AM_LOG_FLAGS) $(LOG_FLAGS)
+endif
+
+# These are run for all build profiles.
+# If a test shouldn't be run in e.g. competition mode,
+# put it below in "TESTS +="
+TESTS =	\
+	union-1b-flip.smt2 \
+	sets-sharing.smt2 \
+	union-1a-flip.smt2 \
+	copy_check_heap_access_33_4.smt2 \
+	rec_copy_loop_check_heap_access_43_4.smt2 \
+	sets-testlemma.smt2 \
+	jan24/insert_invariant_37_2.smt2 \
+	jan24/deepmeas0.hs.fqout.cvc4.47.smt2 \
+	jan24/deepmeas0.hs.fqout.small.smt2 \
+	jan24/remove_check_free_31_6.smt2 \
+	sets-inter.smt2 \
+	sets-equal.smt2 \
+	union-2.smt2 \
+	jan27/deepmeas0.hs.fqout.cvc4.41.smt2 \
+	jan27/ListConcat.hs.fqout.cvc4.177.smt2 \
+	jan27/ListConcat.hs.fqout.177minimized.smt2 \
+	jan27/ListElem.hs.fqout.cvc4.38.smt2 \
+	feb3/ListElts.hs.fqout.cvc4.317.smt2 \
+	setel-eq.smt2 \
+	sets-new.smt2 \
+	jan30/UniqueZipper.hs.fqout.minimized10.smt2 \
+	jan30/UniqueZipper.hs.fqout.cvc4.10.smt2 \
+	jan30/UniqueZipper.hs.fqout.minimized1832.smt2 \
+	jan30/UniqueZipper.hs.fqout.cvc4.1832.smt2 \
+	emptyset.smt2 \
+	sets-union.smt2 \
+	error2.smt2 \
+	union-1b.smt2 \
+	union-1a.smt2 \
+	error1.smt2 \
+	jan28/TalkingAboutSets.hs.fqout.cvc4.3577.smt2 \
+	jan28/TalkingAboutSets.hs.fqout.3577minimized.smt2 \
+	sets-sample.smt2 \
+	eqtest.smt2 \
+	emptyset.smt2 \
+	error2.smt2
+
+EXTRA_DIST = $(TESTS)
+
+#if CVC4_BUILD_PROFILE_COMPETITION
+#else
+#TESTS += \
+#	error.cvc
+#endif
+#
+# and make sure to distribute it
+#EXTRA_DIST += \
+#	error.cvc
+
+# synonyms for "check"
+.PHONY: regress regress0 test
+regress regress0 test: check
+
+# do nothing in this subdir
+.PHONY: regress1 regress2 regress3
+regress1 regress2 regress3:
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
new file mode 100644
index 000000000..a8eccf4ad
--- /dev/null
+++ b/test/regress/regress0/sets/copy_check_heap_access_33_4.smt2
@@ -0,0 +1,133 @@
+(set-option :print-success false)
+(set-logic AUFLIA_SETS)
+(set-info :status unsat)
+(declare-sort Loc 0)
+(define-sort SetLoc () (Set Loc))
+(define-sort SetInt () (Set Int))
+(declare-sort FldLoc 0)
+(declare-sort FldInt 0)
+(declare-fun null$0 () Loc)
+(declare-fun read$0 (FldInt Loc) Int)
+(declare-fun read$1 (FldLoc Loc) Loc)
+(declare-fun Btwn$0 (FldLoc Loc Loc Loc) Bool)
+(declare-fun Alloc$0 () SetLoc)
+(declare-fun Alloc_1$0 () SetLoc)
+(declare-fun Axiom_1$0 () Bool)
+(declare-fun FP$0 () SetLoc)
+(declare-fun FP_1$0 () SetLoc)
+(declare-fun FP_Caller$0 () SetLoc)
+(declare-fun FP_Caller_1$0 () SetLoc)
+(declare-fun cp_2$0 () Loc)
+(declare-fun curr_2$0 () Loc)
+(declare-fun data$0 () FldInt)
+(declare-fun lst$0 () Loc)
+(declare-fun next$0 () FldLoc)
+(declare-fun res_1$0 () Loc)
+(declare-fun sk_?X_4$0 () SetLoc)
+(declare-fun slseg_domain$0 (FldInt FldLoc Loc Loc) SetLoc)
+(declare-fun slseg_struct$0 (SetLoc FldInt FldLoc Loc Loc) Bool)
+(declare-fun tmp_2$0 () Loc)
+
+(assert (! (forall ((?y Loc))
+           (or (not (Btwn$0 next$0 null$0 ?y ?y)) (= null$0 ?y)
+               (Btwn$0 next$0 null$0 (read$1 next$0 null$0) ?y)))
+   :named btwn_reach_1))
+
+(assert (! (forall ((?y Loc))
+           (or (not (= (read$1 next$0 null$0) null$0))
+               (not (Btwn$0 next$0 null$0 ?y ?y)) (= null$0 ?y)))
+   :named btwn_cycl_1))
+
+(assert (! (Btwn$0 next$0 null$0 (read$1 next$0 null$0) (read$1 next$0 null$0))
+   :named btwn_step_1))
+
+(assert (! (forall ((l1 Loc) (l2 Loc))
+           (or (not Axiom_1$0)
+               (or (<= (read$0 data$0 l1) (read$0 data$0 l2))
+                   (not (Btwn$0 next$0 l1 l2 null$0)) (not (in l1 sk_?X_4$0))
+                   (not (in 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 (in null$0 Alloc$0)) :named initial_footprint_of_copy_23_11_2))
+
+(assert (! (not (= lst$0 null$0)) :named if_else_26_6))
+
+(assert (! (= FP_Caller$0 (union FP$0 FP_Caller$0))
+   :named precondition_of_copy_23_11_4))
+
+(assert (! (= sk_?X_4$0 FP$0) :named precondition_of_copy_23_11_5))
+
+(assert (! (= res_1$0 tmp_2$0) :named assign_31_4))
+
+(assert (! (= cp_2$0 res_1$0) :named assign_32_4))
+
+(assert (! (= FP_1$0 (union FP$0 (setenum tmp_2$0))) :named assign_31_11))
+
+(assert (! (or (and (Btwn$0 next$0 lst$0 null$0 null$0) Axiom_1$0)
+       (not (slseg_struct$0 sk_?X_4$0 data$0 next$0 lst$0 null$0)))
+   :named unnamed_3))
+
+(assert (! (forall ((l1 Loc))
+           (or
+               (and (Btwn$0 next$0 lst$0 l1 null$0)
+                    (in 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))))))
+   :named slseg_footprint_2))
+
+(assert (! (not (in curr_2$0 FP_1$0)) :named check_heap_access_33_4))
+
+(assert (! (not (= tmp_2$0 null$0)) :named new_31_11_1))
+
+(assert (! (slseg_struct$0 sk_?X_4$0 data$0 next$0 lst$0 null$0)
+   :named precondition_of_copy_23_11_6))
+
+(assert (! (= sk_?X_4$0 (slseg_domain$0 data$0 next$0 lst$0 null$0))
+   :named precondition_of_copy_23_11_7))
+
+(assert (! (= Alloc$0 (union FP_Caller$0 Alloc$0))
+   :named initial_footprint_of_copy_23_11_3))
+
+(assert (! (= curr_2$0 lst$0) :named assign_30_4))
+
+(assert (! (= FP_Caller_1$0 (setminus FP_Caller$0 FP$0)) :named assign_26_2_1))
+
+(assert (! (= Alloc_1$0 (union Alloc$0 (setenum tmp_2$0))) :named assign_31_11_1))
+
+(assert (! (forall ((?x Loc)) (Btwn$0 next$0 ?x ?x ?x)) :named btwn_refl_1))
+
+(assert (! (forall ((?x Loc) (?y Loc)) (or (not (Btwn$0 next$0 ?x ?y ?x)) (= ?x ?y)))
+   :named btwn_sndw_1))
+
+(assert (! (forall ((?x Loc) (?y Loc) (?z Loc))
+           (or (not (Btwn$0 next$0 ?x ?y ?y)) (not (Btwn$0 next$0 ?x ?z ?z))
+               (Btwn$0 next$0 ?x ?y ?z) (Btwn$0 next$0 ?x ?z ?y)))
+   :named btwn_ord1_1))
+
+(assert (! (forall ((?x Loc) (?y Loc) (?z Loc))
+           (or (not (Btwn$0 next$0 ?x ?y ?z))
+               (and (Btwn$0 next$0 ?x ?y ?y) (Btwn$0 next$0 ?y ?z ?z))))
+   :named btwn_ord2_1))
+
+(assert (! (forall ((?x Loc) (?y Loc) (?z Loc))
+           (or (not (Btwn$0 next$0 ?x ?y ?y)) (not (Btwn$0 next$0 ?y ?z ?z))
+               (Btwn$0 next$0 ?x ?z ?z)))
+   :named btwn_trn1_1))
+
+(assert (! (forall ((?u Loc) (?x Loc) (?y Loc) (?z Loc))
+           (or (not (Btwn$0 next$0 ?x ?y ?z)) (not (Btwn$0 next$0 ?y ?u ?z))
+               (and (Btwn$0 next$0 ?x ?y ?u) (Btwn$0 next$0 ?x ?u ?z))))
+   :named btwn_trn2_1))
+
+(assert (! (forall ((?u Loc) (?x Loc) (?y Loc) (?z Loc))
+           (or (not (Btwn$0 next$0 ?x ?y ?z)) (not (Btwn$0 next$0 ?x ?u ?y))
+               (and (Btwn$0 next$0 ?x ?u ?z) (Btwn$0 next$0 ?u ?y ?z))))
+   :named btwn_trn3_1))
+
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/sets/emptyset.smt2 b/test/regress/regress0/sets/emptyset.smt2
new file mode 100644
index 000000000..47fc25661
--- /dev/null
+++ b/test/regress/regress0/sets/emptyset.smt2
@@ -0,0 +1,4 @@
+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+(assert (in 5 (as emptyset (Set Int) )))
+(check-sat)
diff --git a/test/regress/regress0/sets/eqtest.smt2 b/test/regress/regress0/sets/eqtest.smt2
new file mode 100644
index 000000000..02577b00a
--- /dev/null
+++ b/test/regress/regress0/sets/eqtest.smt2
@@ -0,0 +1,18 @@
+(set-logic QF_ALL_SUPPORTED)
+(set-info :status unsat)
+(declare-fun A () (Set Int) )
+(declare-fun B () (Set Int) )
+(declare-fun C () (Set Int) )
+(declare-fun D () (Set Int) )
+(declare-fun E () (Set Int) )
+(declare-fun F () (Set Int) )
+(declare-fun G () (Set Int) )
+(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 (= (union A B) D))
+(assert (= C (intersection E F)))
+(assert (and (= F H) (= G H) (= H I)))
+(check-sat)
diff --git a/test/regress/regress0/sets/error1.smt2 b/test/regress/regress0/sets/error1.smt2
new file mode 100644
index 000000000..c4b3dd551
--- /dev/null
+++ b/test/regress/regress0/sets/error1.smt2
@@ -0,0 +1,14 @@
+; COMMAND-LINE: --no-check-models
+; EXPECT: sat
+(set-logic QF_UFLIA_SETS)
+(set-info :status sat)
+(declare-fun A () (Set Int))
+(declare-fun C () (Set Int))
+(declare-fun D () (Set Int))
+(declare-fun E () (Set Int))
+(set-info :status sat)
+
+(assert (= A (union D C)))
+(assert (not (= A (union E A))))
+
+(check-sat)
diff --git a/test/regress/regress0/sets/error2.smt2 b/test/regress/regress0/sets/error2.smt2
new file mode 100644
index 000000000..ac678c552
--- /dev/null
+++ b/test/regress/regress0/sets/error2.smt2
@@ -0,0 +1,4 @@
+(set-logic QF_ALL_SUPPORTED)
+(set-info :status unsat)
+(assert (= (as emptyset (Set Int)) (setenum 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
new file mode 100644
index 000000000..290ee95d5
--- /dev/null
+++ b/test/regress/regress0/sets/feb3/ListElts.hs.fqout.cvc4.317.smt2
@@ -0,0 +1,99 @@
+; COMMAND-LINE: --no-check-models
+; EXPECT: sat
+(set-logic QF_ALL_SUPPORTED)
+(set-info :status sat)
+(define-sort Elt () Int)
+(define-sort mySet () (Set Elt ))
+(define-fun smt_set_emp () mySet (as emptyset mySet))
+(define-fun smt_set_mem ((x Elt) (s mySet)) Bool (in x s))
+(define-fun smt_set_add ((s mySet) (x Elt)) mySet (union s (setenum x)))
+(define-fun smt_set_cup ((s1 mySet) (s2 mySet)) mySet (union s1 s2))
+(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (intersection s1 s2))
+;(define-fun smt_set_com ((s mySet)) mySet ((_ map not) s))
+(define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (setminus s1 s2))
+;(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (= smt_set_emp (smt_set_dif s1 s2)))
+(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subseteq s1 s2))
+(declare-fun z3v58 () Int)
+(declare-fun z3v59 () Int)
+(assert (distinct z3v58 z3v59))
+(declare-fun z3f60 (Int) Bool)
+(declare-fun z3v61 () Int)
+(declare-fun z3f62 (Int) Int)
+(declare-fun z3v63 () Int)
+(declare-fun z3v64 () Int)
+(declare-fun z3v67 () Int)
+(declare-fun z3f68 (Int) Int)
+(declare-fun z3f69 (Int) mySet)
+(declare-fun z3f70 (Int) mySet)
+(declare-fun z3f71 (Int) Bool)
+(declare-fun z3v73 () Int)
+(declare-fun z3v76 () Int)
+(declare-fun z3v79 () Int)
+(declare-fun z3v82 () Int)
+(declare-fun z3v84 () Int)
+(declare-fun z3v85 () Int)
+(declare-fun z3v86 () Int)
+(declare-fun z3v89 () Int)
+(declare-fun z3v90 () Int)
+(declare-fun z3v91 () Int)
+(declare-fun z3f92 (Int Int) Int)
+(declare-fun z3v93 () Int)
+(declare-fun z3v94 () Int)
+(declare-fun z3f96 () Int)
+(declare-fun z3v97 () Int)
+(declare-fun z3v98 () Int)
+(declare-fun z3v99 () Int)
+(declare-fun z3v100 () Int)
+(declare-fun z3v101 () Int)
+(declare-fun z3v102 () Int)
+(declare-fun z3v104 () Int)
+(declare-fun z3v107 () Int)
+(declare-fun z3v110 () Int)
+(declare-fun z3v113 () Int)
+(declare-fun z3v116 () Int)
+(declare-fun z3v117 () Int)
+(declare-fun z3v118 () Int)
+(declare-fun z3v119 () Int)
+(declare-fun z3v120 () Int)
+(declare-fun z3v121 () Int)
+(declare-fun z3v122 () Int)
+(declare-fun z3v123 () Int)
+(declare-fun z3v124 () Int)
+(declare-fun z3v125 () Int)
+(declare-fun z3v127 () Int)
+(declare-fun z3v130 () Int)
+(declare-fun z3v133 () Int)
+(declare-fun z3v134 () Int)
+(declare-fun z3v135 () Int)
+(declare-fun z3v136 () Int)
+(declare-fun z3v137 () Int)
+(declare-fun z3v140 () Int)
+(declare-fun z3v141 () Int)
+(declare-fun z3v142 () Int)
+(declare-fun z3v143 () Int)
+(declare-fun z3v144 () Int)
+(declare-fun z3v145 () Int)
+(declare-fun z3v147 () Int)
+(declare-fun z3v150 () Int)
+(declare-fun z3v151 () Int)
+(declare-fun z3v152 () Int)
+(assert (= (z3f69 z3v152) (smt_set_cup (smt_set_add smt_set_emp z3v143) (z3f69 z3v151))))
+(assert (= (z3f70 z3v152) (smt_set_cup (smt_set_add smt_set_emp z3v143) (z3f70 z3v151))))
+(assert (= (z3f68 z3v152) (+ 1 (z3f68 z3v151))))
+(assert (= (z3f71 z3v152) false))
+(assert (and (>= (z3f68 z3v140) 0) (>= (z3f68 z3v141) 0) (>= (z3f68 z3v151) 0) (>= (z3f68 z3v142) 0) (= (z3f69 z3v142) (smt_set_cup (smt_set_add smt_set_emp z3v143) (z3f69 z3v141))) (= (z3f70 z3v142) (smt_set_cup (smt_set_add smt_set_emp z3v143) (z3f70 z3v141))) (= (z3f68 z3v142) (+ 1 (z3f68 z3v141))) (= (z3f71 z3v142) false) (= z3v142 (z3f92 z3v143 z3v141)) (>= (z3f68 z3v142) 0) (= z3v142 z3v144) (>= (z3f68 z3v142) 0) (>= (z3f68 z3v144) 0) (z3f60 z3v58) (= (z3f62 z3v61) z3v61) (= (z3f62 z3v63) z3v63) (not (z3f60 z3v59)) (= (z3f62 z3v64) z3v64)))
+(assert (= (z3f69 z3v151) (smt_set_cup (z3f69 z3v140) (z3f69 z3v141))))
+(assert (= (z3f69 z3v151) (smt_set_cup (z3f69 z3v140) (z3f69 z3v140))))
+(assert (= (z3f69 z3v151) (smt_set_cup (z3f69 z3v141) (z3f69 z3v140))))
+(assert (smt_set_sub (z3f69 z3v151) (z3f69 z3v140)))
+(assert (= (z3f69 z3v151) (z3f69 z3v140)))
+(assert (<= z3v151 z3v140))
+(assert (>= z3v151 z3v140))
+(assert (<= (z3f68 z3v151) (z3f68 z3v140)))
+(assert (>= (z3f68 z3v151) (z3f68 z3v141)))
+(assert (>= (z3f68 z3v151) (z3f68 z3v140)))
+(assert (= (z3f68 z3v151) (z3f68 z3v140)))
+(assert (= z3v151 z3v140))
+(assert (>= (z3f68 z3v151) 0))
+(assert (not (= (z3f69 z3v152) (smt_set_cup (z3f69 z3v140) (z3f69 z3v140)))))
+(check-sat)
diff --git a/test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.cvc4.47.smt2 b/test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.cvc4.47.smt2
new file mode 100644
index 000000000..b90563199
--- /dev/null
+++ b/test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.cvc4.47.smt2
@@ -0,0 +1,75 @@
+(set-logic QF_ALL_SUPPORTED)
+(set-info :status unsat)
+(define-sort Elt () Int)
+(define-sort mySet () (Set Elt ))
+(define-fun smt_set_emp () mySet (as emptyset mySet))
+(define-fun smt_set_mem ((x Elt) (s mySet)) Bool (in x s))
+(define-fun smt_set_add ((s mySet) (x Elt)) mySet (union s (setenum x)))
+(define-fun smt_set_cup ((s1 mySet) (s2 mySet)) mySet (union s1 s2))
+(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (intersection s1 s2))
+
+(define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (setminus s1 s2))
+
+(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subseteq s1 s2))
+(declare-fun z3v58 () Int)
+(declare-fun z3v59 () Int)
+(assert (distinct z3v58 z3v59))
+
+(declare-fun z3f60 (Int) Bool)
+(declare-fun z3v61 () Int)
+(declare-fun z3f62 (Int) Int)
+(declare-fun z3v63 () Int)
+(declare-fun z3v64 () Int)
+(declare-fun z3v65 () Int)
+(declare-fun z3v66 () Int)
+(declare-fun z3f67 (Int) mySet)
+(declare-fun z3v69 () Int)
+(declare-fun z3f70 (Int) Int)
+(declare-fun z3v76 () Int)
+(declare-fun z3v77 () Int)
+(declare-fun z3v78 () Int)
+(declare-fun z3v79 () Int)
+(declare-fun z3v80 () Int)
+(declare-fun z3v81 () Int)
+(declare-fun z3v82 () Int)
+(declare-fun z3f83 (Int) Int)
+(declare-fun z3f84 (Int) Int)
+(declare-fun z3v85 () Int)
+(declare-fun z3f86 (Int) Int)
+(declare-fun z3f87 (Int Int) Int)
+(declare-fun z3v88 () Int)
+(declare-fun z3v89 () Int)
+(declare-fun z3f90 (Int) mySet)
+(declare-fun z3f91 (Int) Bool)
+(declare-fun z3f92 (Int Int) Int)
+(declare-fun z3v93 () Int)
+(declare-fun z3v94 () Int)
+(declare-fun z3v95 () Int)
+(declare-fun z3v96 () Int)
+(declare-fun z3v97 () Int)
+(declare-fun z3v99 () Int)
+
+(assert (= z3v99 z3v89))
+(assert (>= (z3f70 z3v99) 0))
+
+(assert (and (not (z3f60 z3v79))
+             (not (z3f60 z3v79))
+             (= z3v79 z3v80)
+             (= (z3f60 z3v79)
+                (= z3v76 z3v81))
+             (= (z3f60 z3v80)
+                (= z3v76 z3v81))
+             (= (z3f83 z3v82) z3v81)
+             (= (z3f91 z3v78) false)
+             (= z3v78 (z3f92 z3v88 z3v89))
+             (= z3v82 z3v88)
+             (= (z3f67 z3v78)
+                (smt_set_cup (smt_set_add smt_set_emp (z3f83 z3v88))
+                             (z3f67 z3v89)))
+             (= (z3f62 z3v64) z3v64)))
+
+(assert (smt_set_mem z3v76 (z3f67 z3v78)))
+(assert (<= z3v95 z3v93))
+(assert (>= z3v95 z3v93))
+(assert (not (smt_set_mem z3v76 (z3f67 z3v99))))
+(check-sat)
diff --git a/test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.small.smt2 b/test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.small.smt2
new file mode 100644
index 000000000..204af2f2d
--- /dev/null
+++ b/test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.small.smt2
@@ -0,0 +1,18 @@
+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+
+(declare-fun x () Int)
+(declare-fun y () Int)
+
+(declare-fun S () (Set Int))
+(declare-fun T () (Set Int))
+
+(assert (in x S))
+
+(assert (= S (union T (setenum y))))
+
+(assert (not (= x y)))
+
+(assert (not (in 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
new file mode 100644
index 000000000..ad0a7e464
--- /dev/null
+++ b/test/regress/regress0/sets/jan24/insert_invariant_37_2.smt2
@@ -0,0 +1,812 @@
+(set-option :print-success false)
+(set-logic AUFLIA_SETS)
+(set-info :status unsat)
+(declare-sort Loc 0)
+(define-sort SetLoc () (Set Loc))
+(define-sort SetInt () (Set Int))
+(declare-sort FldLoc 0)
+(declare-sort FldInt 0)
+(declare-fun null$0 () Loc)
+(declare-fun read$0 (FldInt Loc) Int)
+(declare-fun read$1 (FldLoc Loc) Loc)
+(declare-fun Btwn$0 (FldLoc Loc Loc Loc) Bool)
+(declare-fun Alloc$0 () SetLoc)
+(declare-fun Axiom$0 () Bool)
+(declare-fun FP$0 () SetLoc)
+(declare-fun FP_Caller$0 () SetLoc)
+(declare-fun FP_Caller_1$0 () SetLoc)
+(declare-fun c1_2$0 () SetInt)
+(declare-fun c2_2$0 () SetInt)
+(declare-fun content$0 () SetInt)
+(declare-fun curr_2$0 () Loc)
+(declare-fun data$0 () FldInt)
+(declare-fun lst$0 () Loc)
+(declare-fun next$0 () FldLoc)
+(declare-fun prev_2$0 () Loc)
+(declare-fun sk_?X$0 () SetLoc)
+(declare-fun sk_?X_1$0 () SetLoc)
+(declare-fun sk_?X_2$0 () SetLoc)
+(declare-fun sk_?X_3$0 () SetLoc)
+(declare-fun sk_?X_4$0 () SetLoc)
+(declare-fun sk_?X_5$0 () SetLoc)
+(declare-fun sk_?e$0 () Int)
+(declare-fun sk_?e_1$0 () Loc)
+(declare-fun sk_?e_2$0 () Loc)
+(declare-fun sk_?e_3$0 () Int)
+(declare-fun sk_FP$0 () SetLoc)
+(declare-fun sk_FP_1$0 () SetLoc)
+(declare-fun sk_l1$0 () Loc)
+(declare-fun sk_l1_1$0 () Loc)
+(declare-fun sk_l2$0 () Loc)
+(declare-fun sk_l2_1$0 () Loc)
+(declare-fun sorted_set_c$0 (FldInt FldLoc Loc Loc) SetInt)
+(declare-fun sorted_set_domain$0 (FldInt FldLoc Loc Loc) SetLoc)
+(declare-fun sorted_set_struct$0 (SetLoc FldInt FldLoc Loc Loc SetInt) Bool)
+(declare-fun val$0 () Int)
+(declare-fun witness$0 (Int SetInt) Loc)
+
+(assert (! (forall ((?y Loc))
+           (or (not (Btwn$0 next$0 null$0 ?y ?y)) (= null$0 ?y)
+               (Btwn$0 next$0 null$0 (read$1 next$0 null$0) ?y)))
+   :named btwn_reach))
+
+(assert (! (forall ((?y Loc))
+           (or (not (= (read$1 next$0 null$0) null$0))
+               (not (Btwn$0 next$0 null$0 ?y ?y)) (= null$0 ?y)))
+   :named btwn_cycl))
+
+(assert (! (Btwn$0 next$0 null$0 (read$1 next$0 null$0) (read$1 next$0 null$0))
+   :named btwn_step))
+
+(assert (! (forall ((l1 Loc) (l2 Loc))
+           (or (not Axiom$0)
+               (or (= l1 l2) (< (read$0 data$0 l1) (read$0 data$0 l2))
+                   (not (Btwn$0 next$0 l1 l2 null$0)) (not (in l1 sk_?X$0))
+                   (not (in l2 sk_?X$0)))))
+   :named strict_sortedness))
+
+(assert (! (forall ((l1 Loc))
+           (or (= l1 null$0)
+               (in (read$0 data$0 l1)
+                 (sorted_set_c$0 data$0 next$0 lst$0 null$0))
+               (not (Btwn$0 next$0 lst$0 l1 null$0))))
+   :named sorted_set_1))
+
+(assert (! (and
+        (or
+            (=
+              (witness$0 (read$0 data$0 curr_2$0)
+                (sorted_set_c$0 data$0 next$0 lst$0 null$0))
+              null$0)
+            (in (read$0 data$0 curr_2$0)
+              (sorted_set_c$0 data$0 next$0 lst$0 null$0)))
+        (or
+            (and
+                 (= (read$0 data$0 curr_2$0)
+                   (read$0 data$0
+                     (witness$0 (read$0 data$0 curr_2$0)
+                       (sorted_set_c$0 data$0 next$0 lst$0 null$0))))
+                 (in
+                   (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)
+                   (sorted_set_c$0 data$0 next$0 lst$0 null$0)))))
+   :named sorted_set_2))
+
+(assert (! (and
+        (or
+            (=
+              (witness$0 (read$0 data$0 prev_2$0)
+                (sorted_set_c$0 data$0 next$0 lst$0 null$0))
+              null$0)
+            (in (read$0 data$0 prev_2$0)
+              (sorted_set_c$0 data$0 next$0 lst$0 null$0)))
+        (or
+            (and
+                 (= (read$0 data$0 prev_2$0)
+                   (read$0 data$0
+                     (witness$0 (read$0 data$0 prev_2$0)
+                       (sorted_set_c$0 data$0 next$0 lst$0 null$0))))
+                 (in
+                   (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)
+                   (sorted_set_c$0 data$0 next$0 lst$0 null$0)))))
+   :named sorted_set_2_1))
+
+(assert (! (and
+        (or
+            (=
+              (witness$0 (read$0 data$0 sk_l1$0)
+                (sorted_set_c$0 data$0 next$0 lst$0 null$0))
+              null$0)
+            (in (read$0 data$0 sk_l1$0)
+              (sorted_set_c$0 data$0 next$0 lst$0 null$0)))
+        (or
+            (and
+                 (= (read$0 data$0 sk_l1$0)
+                   (read$0 data$0
+                     (witness$0 (read$0 data$0 sk_l1$0)
+                       (sorted_set_c$0 data$0 next$0 lst$0 null$0))))
+                 (in
+                   (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)
+                   (sorted_set_c$0 data$0 next$0 lst$0 null$0)))))
+   :named sorted_set_2_2))
+
+(assert (! (and
+        (or
+            (=
+              (witness$0 (read$0 data$0 sk_l1_1$0)
+                (sorted_set_c$0 data$0 next$0 lst$0 null$0))
+              null$0)
+            (in (read$0 data$0 sk_l1_1$0)
+              (sorted_set_c$0 data$0 next$0 lst$0 null$0)))
+        (or
+            (and
+                 (= (read$0 data$0 sk_l1_1$0)
+                   (read$0 data$0
+                     (witness$0 (read$0 data$0 sk_l1_1$0)
+                       (sorted_set_c$0 data$0 next$0 lst$0 null$0))))
+                 (in
+                   (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)
+                   (sorted_set_c$0 data$0 next$0 lst$0 null$0)))))
+   :named sorted_set_2_3))
+
+(assert (! (and
+        (or
+            (=
+              (witness$0 (read$0 data$0 sk_l2$0)
+                (sorted_set_c$0 data$0 next$0 lst$0 null$0))
+              null$0)
+            (in (read$0 data$0 sk_l2$0)
+              (sorted_set_c$0 data$0 next$0 lst$0 null$0)))
+        (or
+            (and
+                 (= (read$0 data$0 sk_l2$0)
+                   (read$0 data$0
+                     (witness$0 (read$0 data$0 sk_l2$0)
+                       (sorted_set_c$0 data$0 next$0 lst$0 null$0))))
+                 (in
+                   (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)
+                   (sorted_set_c$0 data$0 next$0 lst$0 null$0)))))
+   :named sorted_set_2_4))
+
+(assert (! (and
+        (or
+            (=
+              (witness$0 (read$0 data$0 sk_l2_1$0)
+                (sorted_set_c$0 data$0 next$0 lst$0 null$0))
+              null$0)
+            (in (read$0 data$0 sk_l2_1$0)
+              (sorted_set_c$0 data$0 next$0 lst$0 null$0)))
+        (or
+            (and
+                 (= (read$0 data$0 sk_l2_1$0)
+                   (read$0 data$0
+                     (witness$0 (read$0 data$0 sk_l2_1$0)
+                       (sorted_set_c$0 data$0 next$0 lst$0 null$0))))
+                 (in
+                   (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)
+                   (sorted_set_c$0 data$0 next$0 lst$0 null$0)))))
+   :named sorted_set_2_5))
+
+(assert (! (and
+        (or
+            (=
+              (witness$0 sk_?e$0 (sorted_set_c$0 data$0 next$0 lst$0 null$0))
+              null$0)
+            (in 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
+                   (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)))))
+   :named sorted_set_2_6))
+
+(assert (! (and
+        (or
+            (=
+              (witness$0 sk_?e_3$0
+                (sorted_set_c$0 data$0 next$0 lst$0 null$0))
+              null$0)
+            (in 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
+                   (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)))))
+   :named sorted_set_2_7))
+
+(assert (! (forall ((l1 Loc))
+           (or (= l1 null$0)
+               (in (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)
+                 (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))
+               (not (Btwn$0 next$0 lst$0 l1 curr_2$0))))
+   :named sorted_set_1_2))
+
+(assert (! (and
+        (or
+            (=
+              (witness$0 (read$0 data$0 curr_2$0)
+                (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))
+              null$0)
+            (in (read$0 data$0 curr_2$0)
+              (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)))
+        (or
+            (and
+                 (= (read$0 data$0 curr_2$0)
+                   (read$0 data$0
+                     (witness$0 (read$0 data$0 curr_2$0)
+                       (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))))
+                 (in
+                   (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)
+                   (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)))))
+   :named sorted_set_2_8))
+
+(assert (! (and
+        (or
+            (=
+              (witness$0 (read$0 data$0 prev_2$0)
+                (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))
+              null$0)
+            (in (read$0 data$0 prev_2$0)
+              (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)))
+        (or
+            (and
+                 (= (read$0 data$0 prev_2$0)
+                   (read$0 data$0
+                     (witness$0 (read$0 data$0 prev_2$0)
+                       (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))))
+                 (in
+                   (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)
+                   (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)))))
+   :named sorted_set_2_9))
+
+(assert (! (and
+        (or
+            (=
+              (witness$0 (read$0 data$0 sk_l1$0)
+                (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))
+              null$0)
+            (in (read$0 data$0 sk_l1$0)
+              (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)))
+        (or
+            (and
+                 (= (read$0 data$0 sk_l1$0)
+                   (read$0 data$0
+                     (witness$0 (read$0 data$0 sk_l1$0)
+                       (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))))
+                 (in
+                   (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)
+                   (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)))))
+   :named sorted_set_2_10))
+
+(assert (! (and
+        (or
+            (=
+              (witness$0 (read$0 data$0 sk_l1_1$0)
+                (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))
+              null$0)
+            (in (read$0 data$0 sk_l1_1$0)
+              (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)))
+        (or
+            (and
+                 (= (read$0 data$0 sk_l1_1$0)
+                   (read$0 data$0
+                     (witness$0 (read$0 data$0 sk_l1_1$0)
+                       (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))))
+                 (in
+                   (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)
+                   (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)))))
+   :named sorted_set_2_11))
+
+(assert (! (and
+        (or
+            (=
+              (witness$0 (read$0 data$0 sk_l2$0)
+                (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))
+              null$0)
+            (in (read$0 data$0 sk_l2$0)
+              (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)))
+        (or
+            (and
+                 (= (read$0 data$0 sk_l2$0)
+                   (read$0 data$0
+                     (witness$0 (read$0 data$0 sk_l2$0)
+                       (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))))
+                 (in
+                   (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)
+                   (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)))))
+   :named sorted_set_2_12))
+
+(assert (! (and
+        (or
+            (=
+              (witness$0 (read$0 data$0 sk_l2_1$0)
+                (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))
+              null$0)
+            (in (read$0 data$0 sk_l2_1$0)
+              (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)))
+        (or
+            (and
+                 (= (read$0 data$0 sk_l2_1$0)
+                   (read$0 data$0
+                     (witness$0 (read$0 data$0 sk_l2_1$0)
+                       (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))))
+                 (in
+                   (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)
+                   (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)))))
+   :named sorted_set_2_13))
+
+(assert (! (and
+        (or
+            (=
+              (witness$0 sk_?e$0
+                (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))
+              null$0)
+            (in 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
+                   (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)))))
+   :named sorted_set_2_14))
+
+(assert (! (and
+        (or
+            (=
+              (witness$0 sk_?e_3$0
+                (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))
+              null$0)
+            (in 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
+                   (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
+                   (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)))))
+   :named sorted_set_2_15))
+
+(assert (! (and
+        (or
+            (=
+              (witness$0 (read$0 data$0 curr_2$0)
+                (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))
+              null$0)
+            (in (read$0 data$0 curr_2$0)
+              (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)))
+        (or
+            (and
+                 (= (read$0 data$0 curr_2$0)
+                   (read$0 data$0
+                     (witness$0 (read$0 data$0 curr_2$0)
+                       (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))))
+                 (in
+                   (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)
+                   (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)))))
+   :named sorted_set_2_16))
+
+(assert (! (and
+        (or
+            (=
+              (witness$0 (read$0 data$0 prev_2$0)
+                (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))
+              null$0)
+            (in (read$0 data$0 prev_2$0)
+              (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)))
+        (or
+            (and
+                 (= (read$0 data$0 prev_2$0)
+                   (read$0 data$0
+                     (witness$0 (read$0 data$0 prev_2$0)
+                       (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))))
+                 (in
+                   (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)
+                   (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)))))
+   :named sorted_set_2_17))
+
+(assert (! (and
+        (or
+            (=
+              (witness$0 (read$0 data$0 sk_l1$0)
+                (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))
+              null$0)
+            (in (read$0 data$0 sk_l1$0)
+              (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)))
+        (or
+            (and
+                 (= (read$0 data$0 sk_l1$0)
+                   (read$0 data$0
+                     (witness$0 (read$0 data$0 sk_l1$0)
+                       (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))))
+                 (in
+                   (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)
+                   (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)))))
+   :named sorted_set_2_18))
+
+(assert (! (and
+        (or
+            (=
+              (witness$0 (read$0 data$0 sk_l1_1$0)
+                (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))
+              null$0)
+            (in (read$0 data$0 sk_l1_1$0)
+              (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)))
+        (or
+            (and
+                 (= (read$0 data$0 sk_l1_1$0)
+                   (read$0 data$0
+                     (witness$0 (read$0 data$0 sk_l1_1$0)
+                       (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))))
+                 (in
+                   (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)
+                   (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)))))
+   :named sorted_set_2_19))
+
+(assert (! (and
+        (or
+            (=
+              (witness$0 (read$0 data$0 sk_l2$0)
+                (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))
+              null$0)
+            (in (read$0 data$0 sk_l2$0)
+              (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)))
+        (or
+            (and
+                 (= (read$0 data$0 sk_l2$0)
+                   (read$0 data$0
+                     (witness$0 (read$0 data$0 sk_l2$0)
+                       (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))))
+                 (in
+                   (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)
+                   (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)))))
+   :named sorted_set_2_20))
+
+(assert (! (and
+        (or
+            (=
+              (witness$0 (read$0 data$0 sk_l2_1$0)
+                (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))
+              null$0)
+            (in (read$0 data$0 sk_l2_1$0)
+              (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)))
+        (or
+            (and
+                 (= (read$0 data$0 sk_l2_1$0)
+                   (read$0 data$0
+                     (witness$0 (read$0 data$0 sk_l2_1$0)
+                       (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))))
+                 (in
+                   (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)
+                   (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)))))
+   :named sorted_set_2_21))
+
+(assert (! (and
+        (or
+            (=
+              (witness$0 sk_?e$0
+                (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))
+              null$0)
+            (in 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
+                   (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)))))
+   :named sorted_set_2_22))
+
+(assert (! (and
+        (or
+            (=
+              (witness$0 sk_?e_3$0
+                (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))
+              null$0)
+            (in 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
+                   (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)))))
+   :named sorted_set_2_23))
+
+(assert (! (= (read$1 next$0 null$0) null$0) :named read_null))
+
+(assert (! (forall ((l1 Loc))
+           (or
+               (and (Btwn$0 next$0 lst$0 l1 null$0)
+                    (in 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
+                           (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)
+            (not
+                 (in 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 (not (= curr_2$0 null$0)) (not (= prev_2$0 null$0))
+            (not (< (read$0 data$0 prev_2$0) (read$0 data$0 curr_2$0))))
+       (not (= curr_2$0 lst$0)) (not (= prev_2$0 null$0))
+       (not
+            (sorted_set_struct$0 sk_?X_3$0 data$0 next$0 curr_2$0 null$0
+              c1_2$0)))
+   :named invariant_37_2))
+
+(assert (! (= sk_FP_1$0 sk_?X_2$0) :named invariant_37_2_1))
+
+(assert (! (= sk_?X_5$0 (sorted_set_domain$0 data$0 next$0 lst$0 curr_2$0))
+   :named invariant_37_2_2))
+
+(assert (! (= sk_?X_3$0 (sorted_set_domain$0 data$0 next$0 curr_2$0 null$0))
+   :named invariant_37_2_3))
+
+(assert (! (= sk_?X_1$0 (union sk_?X_3$0 sk_?X_4$0)) :named invariant_37_2_4))
+
+(assert (! (= FP_Caller$0 (union FP$0 FP_Caller$0))
+   :named precondition_of_insert_27_11))
+
+(assert (! (= sk_?X$0 FP$0) :named precondition_of_insert_27_11_1))
+
+(assert (! (= Alloc$0 (union FP_Caller$0 Alloc$0))
+   :named initial_footprint_of_insert_27_11))
+
+(assert (! (= curr_2$0 lst$0) :named assign_31_2))
+
+(assert (! (= c1_2$0 content$0) :named assign_34_2))
+
+(assert (! (or (and (Btwn$0 next$0 lst$0 null$0 null$0) Axiom$0)
+       (not
+            (sorted_set_struct$0 sk_?X$0 data$0 next$0 lst$0 null$0
+              content$0)))
+   :named unnamed))
+
+(assert (! (or (sorted_set_struct$0 sk_?X_3$0 data$0 next$0 curr_2$0 null$0 c1_2$0)
+       (not (Btwn$0 next$0 curr_2$0 null$0 null$0))
+       (! (and (Btwn$0 next$0 sk_l1$0 sk_l2$0 null$0) (in sk_l1$0 sk_?X_3$0)
+               (in sk_l2$0 sk_?X_3$0) (not (= sk_l1$0 sk_l2$0))
+               (not (< (read$0 data$0 sk_l1$0) (read$0 data$0 sk_l2$0))))
+          :named strict_sortedness_1))
+   :named unnamed_1))
+
+(assert (! (forall ((l1 Loc))
+           (or
+               (and (Btwn$0 next$0 lst$0 l1 curr_2$0)
+                    (in 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
+                           (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
+                      (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
+                           (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 (! (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)))
+       (and (not (= curr_2$0 null$0)) (not (= prev_2$0 null$0))
+            (not (< (read$0 data$0 prev_2$0) (read$0 data$0 curr_2$0))))
+       (not (= (read$1 next$0 prev_2$0) curr_2$0))
+       (not (> val$0 (read$0 data$0 prev_2$0)))
+       (not (Btwn$0 next$0 lst$0 prev_2$0 curr_2$0))
+       (not
+            (sorted_set_struct$0 sk_?X_3$0 data$0 next$0 curr_2$0 null$0
+              c1_2$0))
+       (not
+            (sorted_set_struct$0 sk_?X_5$0 data$0 next$0 lst$0 curr_2$0
+              c2_2$0)))
+   :named invariant_37_2_5))
+
+(assert (! (= sk_FP$0 sk_?X_1$0) :named invariant_37_2_6))
+
+(assert (! (= sk_?X_4$0 sk_?X_5$0) :named invariant_37_2_7))
+
+(assert (! (= sk_?X_2$0 sk_?X_3$0) :named invariant_37_2_8))
+
+(assert (! (sorted_set_struct$0 sk_?X$0 data$0 next$0 lst$0 null$0 content$0)
+   :named precondition_of_insert_27_11_2))
+
+(assert (! (= sk_?X$0 (sorted_set_domain$0 data$0 next$0 lst$0 null$0))
+   :named precondition_of_insert_27_11_3))
+
+(assert (! (= content$0 (sorted_set_c$0 data$0 next$0 lst$0 null$0))
+   :named precondition_of_insert_27_11_4))
+
+(assert (! (= prev_2$0 null$0) :named assign_32_2))
+
+(assert (! (= c2_2$0 (as emptyset SetInt)) :named assign_35_2))
+
+(assert (! (= FP_Caller_1$0 (setminus FP_Caller$0 FP$0)) :named assign_29_0))
+
+(assert (! (or (sorted_set_struct$0 sk_?X_5$0 data$0 next$0 lst$0 curr_2$0 c2_2$0)
+       (not (Btwn$0 next$0 lst$0 curr_2$0 curr_2$0))
+       (! (and (Btwn$0 next$0 sk_l1_1$0 sk_l2_1$0 curr_2$0)
+               (in sk_l1_1$0 sk_?X_5$0) (in sk_l2_1$0 sk_?X_5$0)
+               (not (= sk_l1_1$0 sk_l2_1$0))
+               (not (< (read$0 data$0 sk_l1_1$0) (read$0 data$0 sk_l2_1$0))))
+          :named strict_sortedness_2))
+   :named unnamed_2))
+
+(assert (! (forall ((?x Loc)) (Btwn$0 next$0 ?x ?x ?x)) :named btwn_refl))
+
+(assert (! (forall ((?x Loc) (?y Loc)) (or (not (Btwn$0 next$0 ?x ?y ?x)) (= ?x ?y)))
+   :named btwn_sndw))
+
+(assert (! (forall ((?x Loc) (?y Loc) (?z Loc))
+           (or (not (Btwn$0 next$0 ?x ?y ?y)) (not (Btwn$0 next$0 ?x ?z ?z))
+               (Btwn$0 next$0 ?x ?y ?z) (Btwn$0 next$0 ?x ?z ?y)))
+   :named btwn_ord1))
+
+(assert (! (forall ((?x Loc) (?y Loc) (?z Loc))
+           (or (not (Btwn$0 next$0 ?x ?y ?z))
+               (and (Btwn$0 next$0 ?x ?y ?y) (Btwn$0 next$0 ?y ?z ?z))))
+   :named btwn_ord2))
+
+(assert (! (forall ((?x Loc) (?y Loc) (?z Loc))
+           (or (not (Btwn$0 next$0 ?x ?y ?y)) (not (Btwn$0 next$0 ?y ?z ?z))
+               (Btwn$0 next$0 ?x ?z ?z)))
+   :named btwn_trn1))
+
+(assert (! (forall ((?u Loc) (?x Loc) (?y Loc) (?z Loc))
+           (or (not (Btwn$0 next$0 ?x ?y ?z)) (not (Btwn$0 next$0 ?y ?u ?z))
+               (and (Btwn$0 next$0 ?x ?y ?u) (Btwn$0 next$0 ?x ?u ?z))))
+   :named btwn_trn2))
+
+(assert (! (forall ((?u Loc) (?x Loc) (?y Loc) (?z Loc))
+           (or (not (Btwn$0 next$0 ?x ?y ?z)) (not (Btwn$0 next$0 ?x ?u ?y))
+               (and (Btwn$0 next$0 ?x ?u ?z) (Btwn$0 next$0 ?u ?y ?z))))
+   :named btwn_trn3))
+
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/sets/jan24/remove_check_free_31_6.smt2 b/test/regress/regress0/sets/jan24/remove_check_free_31_6.smt2
new file mode 100644
index 000000000..c1c65cea5
--- /dev/null
+++ b/test/regress/regress0/sets/jan24/remove_check_free_31_6.smt2
@@ -0,0 +1,470 @@
+(set-option :print-success false)
+(set-logic AUFLIA_SETS)
+(set-info :status unsat)
+(declare-sort Loc 0)
+(define-sort SetLoc () (Set Loc))
+(define-sort SetInt () (Set Int))
+(declare-sort FldLoc 0)
+(declare-sort FldInt 0)
+(declare-fun null$0 () Loc)
+(declare-fun read$0 (FldLoc Loc) Loc)
+(declare-fun write$0 (FldLoc Loc Loc) FldLoc)
+(declare-fun ep$0 (FldLoc SetLoc Loc) Loc)
+(declare-fun Btwn$0 (FldLoc Loc Loc Loc) Bool)
+(declare-fun Frame$0 (SetLoc SetLoc FldLoc FldLoc) Bool)
+(declare-fun Alloc$0 () SetLoc)
+(declare-fun FP$0 () SetLoc)
+(declare-fun FP_1$0 () SetLoc)
+(declare-fun FP_2$0 () SetLoc)
+(declare-fun FP_Caller$0 () SetLoc)
+(declare-fun FP_Caller_1$0 () SetLoc)
+(declare-fun curr_2$0 () Loc)
+(declare-fun curr_3$0 () Loc)
+(declare-fun lseg_domain$0 (FldLoc Loc Loc) SetLoc)
+(declare-fun lseg_struct$0 (SetLoc FldLoc Loc Loc) Bool)
+(declare-fun lst$0 () Loc)
+(declare-fun lst_1$0 () Loc)
+(declare-fun next$0 () FldLoc)
+(declare-fun next_1$0 () FldLoc)
+(declare-fun nondet_2$0 () Bool)
+(declare-fun sk_?X_27$0 () SetLoc)
+(declare-fun sk_?X_28$0 () SetLoc)
+(declare-fun sk_?X_29$0 () SetLoc)
+(declare-fun sk_?X_30$0 () SetLoc)
+(declare-fun sk_?X_31$0 () SetLoc)
+(declare-fun sk_?X_32$0 () SetLoc)
+(declare-fun sk_?X_33$0 () SetLoc)
+(declare-fun tmp_2$0 () Loc)
+
+(assert (! (forall ((?y Loc))
+           (or (not (Btwn$0 next$0 null$0 ?y ?y)) (= null$0 ?y)
+               (Btwn$0 next$0 null$0 (read$0 next$0 null$0) ?y)))
+   :named btwn_reach_8))
+
+(assert (! (forall ((?y Loc))
+           (or (not (Btwn$0 next$0 tmp_2$0 ?y ?y)) (= tmp_2$0 ?y)
+               (Btwn$0 next$0 tmp_2$0 (read$0 next$0 tmp_2$0) ?y)))
+   :named btwn_reach_9))
+
+(assert (! (forall ((?y Loc))
+           (or (not (Btwn$0 next$0 curr_3$0 ?y ?y)) (= curr_3$0 ?y)
+               (Btwn$0 next$0 curr_3$0 (read$0 next$0 curr_3$0) ?y)))
+   :named btwn_reach_10))
+
+(assert (! (forall ((?y Loc))
+           (or (not (= (read$0 next$0 null$0) null$0))
+               (not (Btwn$0 next$0 null$0 ?y ?y)) (= null$0 ?y)))
+   :named btwn_cycl_8))
+
+(assert (! (forall ((?y Loc))
+           (or (not (= (read$0 next$0 tmp_2$0) tmp_2$0))
+               (not (Btwn$0 next$0 tmp_2$0 ?y ?y)) (= tmp_2$0 ?y)))
+   :named btwn_cycl_9))
+
+(assert (! (forall ((?y Loc))
+           (or (not (= (read$0 next$0 curr_3$0) curr_3$0))
+               (not (Btwn$0 next$0 curr_3$0 ?y ?y)) (= curr_3$0 ?y)))
+   :named btwn_cycl_10))
+
+(assert (! (Btwn$0 next$0 null$0 (read$0 next$0 null$0) (read$0 next$0 null$0))
+   :named btwn_step_8))
+
+(assert (! (Btwn$0 next$0 tmp_2$0 (read$0 next$0 tmp_2$0) (read$0 next$0 tmp_2$0))
+   :named btwn_step_9))
+
+(assert (! (Btwn$0 next$0 curr_3$0 (read$0 next$0 curr_3$0) (read$0 next$0 curr_3$0))
+   :named btwn_step_10))
+
+(assert (! (forall ((?f FldLoc))
+           (or (in (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)
+               (= 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)
+               (= 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)
+               (= tmp_2$0 (ep$0 ?f sk_?X_30$0 tmp_2$0))))
+   :named entry-point3_13))
+
+(assert (! (forall ((?f FldLoc))
+           (Btwn$0 ?f null$0 (ep$0 ?f sk_?X_30$0 null$0)
+             (ep$0 ?f sk_?X_30$0 null$0)))
+   :named entry-point1_10))
+
+(assert (! (forall ((?f FldLoc))
+           (Btwn$0 ?f lst_1$0 (ep$0 ?f sk_?X_30$0 lst_1$0)
+             (ep$0 ?f sk_?X_30$0 lst_1$0)))
+   :named entry-point1_11))
+
+(assert (! (forall ((?f FldLoc))
+           (Btwn$0 ?f curr_3$0 (ep$0 ?f sk_?X_30$0 curr_3$0)
+             (ep$0 ?f sk_?X_30$0 curr_3$0)))
+   :named entry-point1_12))
+
+(assert (! (forall ((?f FldLoc))
+           (Btwn$0 ?f tmp_2$0 (ep$0 ?f sk_?X_30$0 tmp_2$0)
+             (ep$0 ?f sk_?X_30$0 tmp_2$0)))
+   :named entry-point1_13))
+
+(assert (! (forall ((?f FldLoc) (?y Loc))
+           (or (Btwn$0 ?f null$0 (ep$0 ?f sk_?X_30$0 null$0) ?y)
+               (not (Btwn$0 ?f null$0 ?y ?y)) (not (in ?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))))
+   :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))))
+   :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))))
+   :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)))
+   :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)))
+   :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)))
+   :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)))
+   :named entry-point2_13))
+
+(assert (! (= (read$0 (write$0 next$0 curr_3$0 (read$0 next$0 tmp_2$0)) curr_3$0)
+     (read$0 next$0 tmp_2$0))
+   :named read_write2))
+
+(assert (! (or (= null$0 curr_3$0)
+       (= (read$0 next$0 null$0)
+         (read$0 (write$0 next$0 curr_3$0 (read$0 next$0 tmp_2$0)) null$0)))
+   :named read_write1))
+
+(assert (! (or (= tmp_2$0 curr_3$0)
+       (= (read$0 next$0 tmp_2$0)
+         (read$0 (write$0 next$0 curr_3$0 (read$0 next$0 tmp_2$0)) tmp_2$0)))
+   :named read_write1_1))
+
+(assert (! (or (= curr_3$0 curr_3$0)
+       (= (read$0 next$0 curr_3$0)
+         (read$0 (write$0 next$0 curr_3$0 (read$0 next$0 tmp_2$0)) curr_3$0)))
+   :named read_write1_2))
+
+(assert (! (= (read$0 next$0 null$0) null$0) :named read_null_5))
+
+(assert (! (= (read$0 next_1$0 null$0) null$0) :named read_null_6))
+
+(assert (! (forall ((l1 Loc))
+           (or
+               (and (Btwn$0 next$0 lst$0 l1 curr_2$0)
+                    (in 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))))))
+   :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))
+                    (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))))))
+   :named lseg_footprint_21))
+
+(assert (! (not (in 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 (= lst$0 null$0)) :named if_else_13_6_4))
+
+(assert (! (= FP_Caller$0 (union FP$0 FP_Caller$0))
+   :named precondition_of_remove_10_11_20))
+
+(assert (! (= sk_?X_33$0 FP$0) :named precondition_of_remove_10_11_21))
+
+(assert (! (lseg_struct$0 sk_?X_32$0 next$0 lst$0 curr_2$0) :named invariant_18_4_62))
+
+(assert (! (= FP$0 (union FP_1$0 FP$0)) :named invariant_18_4_63))
+
+(assert (! (= sk_?X_31$0 (lseg_domain$0 next$0 curr_2$0 null$0))
+   :named invariant_18_4_64))
+
+(assert (! (= sk_?X_30$0 (union sk_?X_31$0 sk_?X_32$0)) :named invariant_18_4_65))
+
+(assert (! (= (as emptyset SetLoc) (as emptyset SetLoc)) :named invariant_18_4_66))
+
+(assert (! (lseg_struct$0 sk_?X_28$0 next$0 curr_3$0 null$0)
+   :named invariant_18_4_67))
+
+(assert (! (= sk_?X_29$0 (union sk_?X_28$0 sk_?X_27$0)) :named invariant_18_4_68))
+
+(assert (! (= sk_?X_28$0 (lseg_domain$0 next$0 curr_3$0 null$0))
+   :named invariant_18_4_69))
+
+(assert (! (= (as emptyset SetLoc) (intersection sk_?X_27$0 sk_?X_28$0))
+   :named invariant_18_4_70))
+
+(assert (! (= Alloc$0 (union FP_Caller$0 Alloc$0))
+   :named initial_footprint_of_remove_10_11_10))
+
+(assert (! (Frame$0 FP_1$0 Alloc$0 next$0 next$0)
+   :named framecondition_of_remove_loop_18_4_16))
+
+(assert (! (= next_1$0 (write$0 next$0 curr_3$0 (read$0 next$0 tmp_2$0)))
+   :named assign_30_6))
+
+(assert (! (= curr_2$0 lst$0) :named assign_17_4_4))
+
+(assert (! (= FP_2$0
+     (union (setminus FP$0 FP_1$0)
+       (union (intersection Alloc$0 FP_1$0) (setminus Alloc$0 Alloc$0))))
+   :named framecondition_of_remove_loop_18_4_17))
+
+(assert (! (or (Btwn$0 next$0 lst$0 curr_2$0 curr_2$0)
+       (not (lseg_struct$0 sk_?X_32$0 next$0 lst$0 curr_2$0)))
+   :named unnamed_23))
+
+(assert (! (or (Btwn$0 next$0 curr_3$0 null$0 null$0)
+       (not (lseg_struct$0 sk_?X_28$0 next$0 curr_3$0 null$0)))
+   :named unnamed_24))
+
+(assert (! (or (= (read$0 next$0 curr_3$0) null$0) (not nondet_2$0))
+   :named unnamed_25))
+
+(assert (! (forall ((l1 Loc))
+           (or
+               (and (Btwn$0 next$0 lst_1$0 l1 curr_3$0)
+                    (in 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))))))
+   :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))
+                    (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))))))
+   :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))
+                    (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))))))
+   :named lseg_footprint_24))
+
+(assert (! (not (in null$0 Alloc$0)) :named initial_footprint_of_remove_10_11_11))
+
+(assert (! (not (= tmp_2$0 null$0)) :named if_else_28_8_2))
+
+(assert (! (lseg_struct$0 sk_?X_33$0 next$0 lst$0 null$0)
+   :named precondition_of_remove_10_11_22))
+
+(assert (! (= sk_?X_33$0 (lseg_domain$0 next$0 lst$0 null$0))
+   :named precondition_of_remove_10_11_23))
+
+(assert (! (not (= curr_2$0 null$0)) :named invariant_18_4_71))
+
+(assert (! (lseg_struct$0 sk_?X_31$0 next$0 curr_2$0 null$0)
+   :named invariant_18_4_72))
+
+(assert (! (= sk_?X_32$0 (lseg_domain$0 next$0 lst$0 curr_2$0))
+   :named invariant_18_4_73))
+
+(assert (! (= sk_?X_30$0 FP_1$0) :named invariant_18_4_74))
+
+(assert (! (= (as emptyset SetLoc) (intersection sk_?X_32$0 sk_?X_31$0))
+   :named invariant_18_4_75))
+
+(assert (! (not (= curr_3$0 null$0)) :named invariant_18_4_76))
+
+(assert (! (lseg_struct$0 sk_?X_27$0 next$0 lst_1$0 curr_3$0)
+   :named invariant_18_4_77))
+
+(assert (! (= sk_?X_29$0
+     (union (intersection Alloc$0 FP_1$0) (setminus Alloc$0 Alloc$0)))
+   :named invariant_18_4_78))
+
+(assert (! (= sk_?X_27$0 (lseg_domain$0 next$0 lst_1$0 curr_3$0))
+   :named invariant_18_4_79))
+
+(assert (! (= (as emptyset SetLoc) (as emptyset SetLoc)) :named invariant_18_4_80))
+
+(assert (! (= Alloc$0 (union FP_2$0 Alloc$0))
+   :named framecondition_of_remove_loop_18_4_18))
+
+(assert (! (= tmp_2$0 (read$0 next$0 curr_3$0)) :named assign_27_4_2))
+
+(assert (! (= lst_1$0 lst$0) :named framecondition_of_remove_loop_18_4_19))
+
+(assert (! (= FP_Caller_1$0 (setminus FP_Caller$0 FP$0)) :named assign_13_2_5))
+
+(assert (! (or (Btwn$0 next$0 lst_1$0 curr_3$0 curr_3$0)
+       (not (lseg_struct$0 sk_?X_27$0 next$0 lst_1$0 curr_3$0)))
+   :named unnamed_26))
+
+(assert (! (or (Btwn$0 next$0 lst$0 null$0 null$0)
+       (not (lseg_struct$0 sk_?X_33$0 next$0 lst$0 null$0)))
+   :named unnamed_27))
+
+(assert (! (or (Btwn$0 next$0 curr_2$0 null$0 null$0)
+       (not (lseg_struct$0 sk_?X_31$0 next$0 curr_2$0 null$0)))
+   :named unnamed_28))
+
+(assert (! (forall ((?u Loc) (?v Loc) (?z Loc))
+           (and
+                (or
+                    (Btwn$0 (write$0 next$0 curr_3$0 (read$0 next$0 tmp_2$0))
+                      ?z ?u ?v)
+                    (not
+                         (or
+                             (and (Btwn$0 next$0 ?z ?u ?v)
+                                  (or (Btwn$0 next$0 ?z ?v curr_3$0)
+                                      (and (Btwn$0 next$0 ?z ?v ?v)
+                                           (not
+                                                (Btwn$0 next$0 ?z curr_3$0
+                                                  curr_3$0)))))
+                             (and (not (= curr_3$0 ?v))
+                                  (or (Btwn$0 next$0 ?z curr_3$0 ?v)
+                                      (and
+                                           (Btwn$0 next$0 ?z curr_3$0
+                                             curr_3$0)
+                                           (not (Btwn$0 next$0 ?z ?v ?v))))
+                                  (Btwn$0 next$0 ?z ?u curr_3$0)
+                                  (or
+                                      (Btwn$0 next$0 (read$0 next$0 tmp_2$0)
+                                        ?v curr_3$0)
+                                      (and
+                                           (Btwn$0 next$0
+                                             (read$0 next$0 tmp_2$0) ?v ?v)
+                                           (not
+                                                (Btwn$0 next$0
+                                                  (read$0 next$0 tmp_2$0)
+                                                  curr_3$0 curr_3$0)))))
+                             (and (not (= curr_3$0 ?v))
+                                  (or (Btwn$0 next$0 ?z curr_3$0 ?v)
+                                      (and
+                                           (Btwn$0 next$0 ?z curr_3$0
+                                             curr_3$0)
+                                           (not (Btwn$0 next$0 ?z ?v ?v))))
+                                  (Btwn$0 next$0 (read$0 next$0 tmp_2$0) ?u
+                                    ?v)
+                                  (or
+                                      (Btwn$0 next$0 (read$0 next$0 tmp_2$0)
+                                        ?v curr_3$0)
+                                      (and
+                                           (Btwn$0 next$0
+                                             (read$0 next$0 tmp_2$0) ?v ?v)
+                                           (not
+                                                (Btwn$0 next$0
+                                                  (read$0 next$0 tmp_2$0)
+                                                  curr_3$0 curr_3$0))))))))
+                (or
+                    (and (Btwn$0 next$0 ?z ?u ?v)
+                         (or (Btwn$0 next$0 ?z ?v curr_3$0)
+                             (and (Btwn$0 next$0 ?z ?v ?v)
+                                  (not (Btwn$0 next$0 ?z curr_3$0 curr_3$0)))))
+                    (and (not (= curr_3$0 ?v))
+                         (or (Btwn$0 next$0 ?z curr_3$0 ?v)
+                             (and (Btwn$0 next$0 ?z curr_3$0 curr_3$0)
+                                  (not (Btwn$0 next$0 ?z ?v ?v))))
+                         (Btwn$0 next$0 ?z ?u curr_3$0)
+                         (or
+                             (Btwn$0 next$0 (read$0 next$0 tmp_2$0) ?v
+                               curr_3$0)
+                             (and
+                                  (Btwn$0 next$0 (read$0 next$0 tmp_2$0) ?v
+                                    ?v)
+                                  (not
+                                       (Btwn$0 next$0 (read$0 next$0 tmp_2$0)
+                                         curr_3$0 curr_3$0)))))
+                    (and (not (= curr_3$0 ?v))
+                         (or (Btwn$0 next$0 ?z curr_3$0 ?v)
+                             (and (Btwn$0 next$0 ?z curr_3$0 curr_3$0)
+                                  (not (Btwn$0 next$0 ?z ?v ?v))))
+                         (Btwn$0 next$0 (read$0 next$0 tmp_2$0) ?u ?v)
+                         (or
+                             (Btwn$0 next$0 (read$0 next$0 tmp_2$0) ?v
+                               curr_3$0)
+                             (and
+                                  (Btwn$0 next$0 (read$0 next$0 tmp_2$0) ?v
+                                    ?v)
+                                  (not
+                                       (Btwn$0 next$0 (read$0 next$0 tmp_2$0)
+                                         curr_3$0 curr_3$0)))))
+                    (not
+                         (Btwn$0
+                           (write$0 next$0 curr_3$0 (read$0 next$0 tmp_2$0))
+                           ?z ?u ?v)))))
+   :named btwn_write))
+
+(assert (! (forall ((?x Loc)) (Btwn$0 next$0 ?x ?x ?x)) :named btwn_refl_5))
+
+(assert (! (forall ((?x Loc) (?y Loc)) (or (not (Btwn$0 next$0 ?x ?y ?x)) (= ?x ?y)))
+   :named btwn_sndw_5))
+
+(assert (! (forall ((?x Loc) (?y Loc) (?z Loc))
+           (or (not (Btwn$0 next$0 ?x ?y ?y)) (not (Btwn$0 next$0 ?x ?z ?z))
+               (Btwn$0 next$0 ?x ?y ?z) (Btwn$0 next$0 ?x ?z ?y)))
+   :named btwn_ord1_5))
+
+(assert (! (forall ((?x Loc) (?y Loc) (?z Loc))
+           (or (not (Btwn$0 next$0 ?x ?y ?z))
+               (and (Btwn$0 next$0 ?x ?y ?y) (Btwn$0 next$0 ?y ?z ?z))))
+   :named btwn_ord2_5))
+
+(assert (! (forall ((?x Loc) (?y Loc) (?z Loc))
+           (or (not (Btwn$0 next$0 ?x ?y ?y)) (not (Btwn$0 next$0 ?y ?z ?z))
+               (Btwn$0 next$0 ?x ?z ?z)))
+   :named btwn_trn1_5))
+
+(assert (! (forall ((?u Loc) (?x Loc) (?y Loc) (?z Loc))
+           (or (not (Btwn$0 next$0 ?x ?y ?z)) (not (Btwn$0 next$0 ?y ?u ?z))
+               (and (Btwn$0 next$0 ?x ?y ?u) (Btwn$0 next$0 ?x ?u ?z))))
+   :named btwn_trn2_5))
+
+(assert (! (forall ((?u Loc) (?x Loc) (?y Loc) (?z Loc))
+           (or (not (Btwn$0 next$0 ?x ?y ?z)) (not (Btwn$0 next$0 ?x ?u ?y))
+               (and (Btwn$0 next$0 ?x ?u ?z) (Btwn$0 next$0 ?u ?y ?z))))
+   :named btwn_trn3_5))
+
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/sets/jan27/ListConcat.hs.fqout.177minimized.smt2 b/test/regress/regress0/sets/jan27/ListConcat.hs.fqout.177minimized.smt2
new file mode 100644
index 000000000..c4ee3b710
--- /dev/null
+++ b/test/regress/regress0/sets/jan27/ListConcat.hs.fqout.177minimized.smt2
@@ -0,0 +1,18 @@
+(set-logic QF_ALL_SUPPORTED)
+(set-info :status unsat)
+(define-sort Elt () Int)
+(define-sort mySet () (Set Elt ))
+(define-fun smt_set_emp () mySet (as emptyset mySet))
+
+(declare-fun S () (Set Int))
+(declare-fun T () (Set Int))
+
+(assert (not (= S T)))
+(assert (= T (union smt_set_emp S)))
+(check-sat)
+
+; What was the bug?
+;
+; When two sets were disequal, the corresponding lemma
+; was not being generated (stating there in an element
+; in one, but not in the other).
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
new file mode 100644
index 000000000..7fea3435e
--- /dev/null
+++ b/test/regress/regress0/sets/jan27/ListConcat.hs.fqout.cvc4.177.smt2
@@ -0,0 +1,49 @@
+(set-logic QF_ALL_SUPPORTED)
+(set-info :status unsat)
+(define-sort Elt () Int)
+(define-sort mySet () (Set Elt ))
+(define-fun smt_set_emp () mySet (as emptyset mySet))
+(define-fun smt_set_mem ((x Elt) (s mySet)) Bool (in x s))
+(define-fun smt_set_add ((s mySet) (x Elt)) mySet (union s (setenum x)))
+(define-fun smt_set_cup ((s1 mySet) (s2 mySet)) mySet (union s1 s2))
+(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (intersection s1 s2))
+;(define-fun smt_set_com ((s mySet)) mySet ((_ map not) s))
+(define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (setminus s1 s2))
+;(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (= smt_set_emp (smt_set_dif s1 s2)))
+(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subseteq s1 s2))
+(declare-fun z3v54 () Int)
+(declare-fun z3f55 (Int) Int)
+(declare-fun z3v56 () Int)
+(declare-fun z3v57 () Int)
+(declare-fun z3v58 () Int)
+(declare-fun z3v59 () Int)
+(declare-fun z3f60 (Int) mySet)
+(declare-fun z3f61 (Int) Bool)
+(declare-fun z3f62 (Int Int) Int)
+(declare-fun z3v63 () Int)
+(declare-fun z3v64 () Int)
+(declare-fun z3f65 (Int) mySet)
+(declare-fun z3v66 () Int)
+(declare-fun z3v67 () Int)
+(declare-fun z3v68 () Int)
+(declare-fun z3v69 () Int)
+(declare-fun z3f70 (Int) Int)
+(declare-fun z3v71 () Int)
+(declare-fun z3v72 () Int)
+(declare-fun z3v74 () Int)
+(declare-fun z3v76 () Int)
+(declare-fun z3v77 () Int)
+(declare-fun z3v78 () Int)
+(declare-fun z3v82 () Int)
+(declare-fun z3v85 () Int)
+(declare-fun z3v86 () Int)
+(declare-fun z3v87 () Int)
+(declare-fun z3f90 () Int)
+(declare-fun z3v91 () Int)
+(declare-fun z3v92 () Int)
+(declare-fun z3v93 () Int)
+(declare-fun z3v94 () Int)
+(assert (= (z3f60 z3v94) (z3f65 z3v56)))
+(assert (and (>= (z3f55 z3v56) 0) (>= (z3f55 z3v58) 0) (= (z3f60 z3v58) smt_set_emp) (= (z3f55 z3v58) 0) (= (z3f61 z3v58) true) (= z3v58 z3f90) (>= (z3f55 z3v58) 0) (= z3v58 z3v63) (>= (z3f55 z3v58) 0) (>= (z3f55 z3v64) 0) (= (z3f65 z3v64) (smt_set_cup (z3f60 z3v63) (z3f65 z3v56))) (= (z3f60 z3v64) (smt_set_cup (smt_set_add smt_set_emp z3v63) (z3f60 z3v56))) (= (z3f55 z3v64) (+ 1 (z3f55 z3v56))) (= (z3f61 z3v64) false) (= z3v64 (z3f62 z3v63 z3v56)) (>= (z3f55 z3v64) 0) (= z3v64 z3v66) (>= (z3f55 z3v64) 0) (>= (z3f55 z3v63) 0) (>= (z3f55 z3v66) 0) (= (z3f70 z3v69) z3v69) (= (z3f70 z3v71) z3v71) (= (z3f70 z3v72) z3v72)))
+(assert (not (= (z3f60 z3v94) (z3f65 z3v66))))
+(check-sat)
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
new file mode 100644
index 000000000..6c32bb578
--- /dev/null
+++ b/test/regress/regress0/sets/jan27/ListElem.hs.fqout.cvc4.38.smt2
@@ -0,0 +1,59 @@
+(set-logic QF_ALL_SUPPORTED)
+(set-info :status unsat)
+
+; What was the bug?
+; 
+; When asserting equality to equality engine, correct reason
+; was not being sent (the fact itself was being sent as reason)
+
+(define-sort Elt () Int)
+(define-sort mySet () (Set Elt ))
+(define-fun smt_set_emp () mySet (as emptyset mySet))
+(define-fun smt_set_mem ((x Elt) (s mySet)) Bool (in x s))
+(define-fun smt_set_add ((s mySet) (x Elt)) mySet (union s (setenum x)))
+(define-fun smt_set_cup ((s1 mySet) (s2 mySet)) mySet (union s1 s2))
+(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (intersection s1 s2))
+;(define-fun smt_set_com ((s mySet)) mySet ((_ map not) s))
+(define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (setminus s1 s2))
+;(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (= smt_set_emp (smt_set_dif s1 s2)))
+(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subseteq s1 s2))
+(declare-fun z3v56 () Int)
+(declare-fun z3v57 () Int)
+(assert (distinct z3v56 z3v57))
+(declare-fun z3v58 () Int)
+(declare-fun z3f59 (Int) Int)
+(declare-fun z3v60 () Int)
+(declare-fun z3f61 (Int) Bool)
+(declare-fun z3v62 () Int)
+(declare-fun z3v63 () Int)
+(declare-fun z3v64 () Int)
+(declare-fun z3v65 () Int)
+(declare-fun z3f66 (Int) mySet)
+(declare-fun z3f67 (Int) Bool)
+(declare-fun z3f68 (Int Int) Int)
+(declare-fun z3v69 () Int)
+(declare-fun z3v70 () Int)
+(declare-fun z3f71 (Int) Int)
+(declare-fun z3v72 () Int)
+(declare-fun z3v73 () Int)
+(declare-fun z3v74 () Int)
+(declare-fun z3v75 () Int)
+(declare-fun z3v76 () Int)
+(declare-fun z3v77 () Int)
+(declare-fun z3v78 () Int)
+(declare-fun z3v80 () Int)
+(declare-fun z3v81 () Int)
+(declare-fun z3f82 () Int)
+(declare-fun z3v83 () Int)
+(declare-fun z3v84 () Int)
+(declare-fun z3v85 () Int)
+(declare-fun z3v86 () Int)
+(declare-fun z3v87 () Int)
+(declare-fun z3v88 () Int)
+(declare-fun z3v89 () Int)
+(declare-fun z3v90 () Int)
+(assert (= z3v90 z3v56))
+(assert (z3f61 z3v90))
+(assert (and (>= (z3f59 z3v58) 0) (z3f61 z3v60) (z3f61 z3v60) (= z3v60 z3v62) (= (z3f61 z3v60) (= z3v64 z3v63)) (= (z3f61 z3v62) (= z3v64 z3v63)) (>= (z3f59 z3v65) 0) (= (z3f66 z3v65) (smt_set_cup (smt_set_add smt_set_emp z3v64) (z3f66 z3v58))) (= (z3f59 z3v65) (+ 1 (z3f59 z3v58))) (= (z3f67 z3v65) false) (= z3v65 (z3f68 z3v64 z3v58)) (>= (z3f59 z3v65) 0) (= z3v65 z3v69) (>= (z3f59 z3v65) 0) (>= (z3f59 z3v69) 0) (z3f61 z3v56) (= (z3f71 z3v70) z3v70) (= (z3f71 z3v72) z3v72) (not (z3f61 z3v57)) (= (z3f71 z3v73) z3v73)))
+(assert (not (= (z3f61 z3v90) (smt_set_mem z3v63 (z3f66 z3v69)))))
+(check-sat)
diff --git a/test/regress/regress0/sets/jan27/deepmeas0.hs.fqout.cvc4.41.smt2 b/test/regress/regress0/sets/jan27/deepmeas0.hs.fqout.cvc4.41.smt2
new file mode 100644
index 000000000..bcc4c33da
--- /dev/null
+++ b/test/regress/regress0/sets/jan27/deepmeas0.hs.fqout.cvc4.41.smt2
@@ -0,0 +1,59 @@
+; COMMAND-LINE: --no-check-models
+; EXPECT: sat
+(set-logic QF_ALL_SUPPORTED)
+(set-info :status sat)
+(define-sort Elt () Int)
+(define-sort mySet () (Set Elt ))
+(define-fun smt_set_emp () mySet (as emptyset mySet))
+(define-fun smt_set_mem ((x Elt) (s mySet)) Bool (in x s))
+(define-fun smt_set_add ((s mySet) (x Elt)) mySet (union s (setenum x)))
+(define-fun smt_set_cup ((s1 mySet) (s2 mySet)) mySet (union s1 s2))
+(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (intersection s1 s2))
+;(define-fun smt_set_com ((s mySet)) mySet ((_ map not) s))
+(define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (setminus s1 s2))
+;(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (= smt_set_emp (smt_set_dif s1 s2)))
+(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subseteq s1 s2))
+(declare-fun z3v58 () Int)
+(declare-fun z3v59 () Int)
+(assert (distinct z3v58 z3v59))
+(declare-fun z3f60 (Int) Bool)
+(declare-fun z3v61 () Int)
+(declare-fun z3f62 (Int) Int)
+(declare-fun z3v63 () Int)
+(declare-fun z3v64 () Int)
+(declare-fun z3v65 () Int)
+(declare-fun z3v66 () Int)
+(declare-fun z3f67 (Int) mySet)
+(declare-fun z3v69 () Int)
+(declare-fun z3f70 (Int) Int)
+(declare-fun z3v76 () Int)
+(declare-fun z3v77 () Int)
+(declare-fun z3v78 () Int)
+(declare-fun z3v79 () Int)
+(declare-fun z3v80 () Int)
+(declare-fun z3v81 () Int)
+(declare-fun z3v82 () Int)
+(declare-fun z3f83 (Int) Int)
+(declare-fun z3f84 (Int) Int)
+(declare-fun z3v85 () Int)
+(declare-fun z3f86 (Int) Int)
+(declare-fun z3f87 (Int Int) Int)
+(declare-fun z3v88 () Int)
+(declare-fun z3v89 () Int)
+(declare-fun z3f90 (Int) mySet)
+(declare-fun z3f91 (Int) Bool)
+(declare-fun z3f92 (Int Int) Int)
+(declare-fun z3v93 () Int)
+(declare-fun z3v94 () Int)
+(declare-fun z3v95 () Int)
+(declare-fun z3v96 () Int)
+(declare-fun z3v97 () Int)
+(assert (and (not (z3f60 z3v79)) (not (z3f60 z3v79)) (= z3v79 z3v80) (= (z3f60 z3v79) (= z3v76 z3v81)) (= (z3f60 z3v80) (= z3v76 z3v81)) (= (z3f83 z3v82) z3v81) (= (z3f84 z3v82) z3v81) (= (z3f86 z3v82) z3v85) (= z3v82 (z3f87 z3v81 z3v85)) (= z3v82 z3v88) (>= (z3f70 z3v78) 0) (= (z3f67 z3v78) (smt_set_cup (smt_set_add smt_set_emp (z3f83 z3v88)) (z3f67 z3v89))) (= (z3f90 z3v78) (smt_set_cup (smt_set_add smt_set_emp z3v88) (z3f90 z3v89))) (= (z3f70 z3v78) (+ 1 (z3f70 z3v89))) (= (z3f91 z3v78) false) (= z3v78 (z3f92 z3v88 z3v89)) (>= (z3f70 z3v78) 0) (= z3v78 z3v77) (>= (z3f70 z3v78) 0) (>= (z3f70 z3v89) 0) (>= (z3f70 z3v77) 0) (>= (z3f70 z3v97) 0) (= z3v97 z3v89) (>= (z3f70 z3v97) 0) (z3f60 z3v58) (= (z3f62 z3v61) z3v61) (= (z3f62 z3v63) z3v63) (not (z3f60 z3v59)) (= (z3f62 z3v64) z3v64)))
+(assert (smt_set_mem z3v76 (z3f67 z3v78)))
+(assert (<= z3v95 z3v93))
+(assert (>= z3v95 z3v93))
+(assert (= z3v95 z3v93))
+(assert (smt_set_mem z3v76 (z3f67 z3v77)))
+(declare-fun z3v98 () Int)
+(assert (not (<  z3v98 z3v85)))
+(check-sat)
diff --git a/test/regress/regress0/sets/jan28/TalkingAboutSets.hs.fqout.3577minimized.smt2 b/test/regress/regress0/sets/jan28/TalkingAboutSets.hs.fqout.3577minimized.smt2
new file mode 100644
index 000000000..5a44c0344
--- /dev/null
+++ b/test/regress/regress0/sets/jan28/TalkingAboutSets.hs.fqout.3577minimized.smt2
@@ -0,0 +1,34 @@
+; COMMAND-LINE: --no-check-models
+; EXPECT: sat
+(set-logic QF_ALL_SUPPORTED)
+(set-info :status sat)
+
+; Observed behavior
+;
+; Benchmark taking too long. Lemmas being generated indefinitely with
+; skolems due to the "two sets not being equal" axiom.
+;
+; What was the bug?
+;
+;
+
+(define-sort Elt () Int)
+(define-sort mySet () (Set Elt))
+
+(declare-fun f (Int) mySet)
+(declare-fun x () Int)
+(declare-fun y () Int)
+
+(declare-fun S () mySet)
+(declare-fun T () mySet)
+
+(assert (= (f x) 
+           (union S T)))
+
+(assert (= (f x) 
+           (union T (f y))))
+
+(assert (not (= (f y) 
+                (union T (f y)))))
+
+(check-sat)
diff --git a/test/regress/regress0/sets/jan28/TalkingAboutSets.hs.fqout.cvc4.3577.smt2 b/test/regress/regress0/sets/jan28/TalkingAboutSets.hs.fqout.cvc4.3577.smt2
new file mode 100644
index 000000000..67d64bd05
--- /dev/null
+++ b/test/regress/regress0/sets/jan28/TalkingAboutSets.hs.fqout.cvc4.3577.smt2
@@ -0,0 +1,287 @@
+; COMMAND-LINE: --no-check-models
+; EXPECT: sat
+(set-logic QF_ALL_SUPPORTED)
+(set-info :status sat)
+(define-sort Elt () Int)
+(define-sort mySet () (Set Elt ))
+(define-fun smt_set_emp () mySet (as emptyset mySet))
+(define-fun smt_set_mem ((x Elt) (s mySet)) Bool (in x s))
+(define-fun smt_set_add ((s mySet) (x Elt)) mySet (union s (setenum x)))
+(define-fun smt_set_cup ((s1 mySet) (s2 mySet)) mySet (union s1 s2))
+(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (intersection s1 s2))
+;(define-fun smt_set_com ((s mySet)) mySet ((_ map not) s))
+(define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (setminus s1 s2))
+;(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (= smt_set_emp (smt_set_dif s1 s2)))
+(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subseteq s1 s2))
+(declare-fun z3v60 () Int)
+(declare-fun z3v61 () Int)
+(assert (distinct z3v60 z3v61))
+(declare-fun z3f62 (Int) Bool)
+(declare-fun z3v63 () Int)
+(declare-fun z3f64 (Int) Int)
+(declare-fun z3v65 () Int)
+(declare-fun z3v66 () Int)
+(declare-fun z3v69 () mySet)
+(declare-fun z3v70 () mySet)
+(declare-fun z3v72 () mySet)
+(declare-fun z3v73 () mySet)
+(declare-fun z3v75 () Int)
+(declare-fun z3f76 (Int) Int)
+(declare-fun z3v79 () Int)
+(declare-fun z3v80 () Int)
+(declare-fun z3v84 () Int)
+(declare-fun z3v87 () mySet)
+(declare-fun z3v88 () mySet)
+(declare-fun z3v90 () mySet)
+(declare-fun z3v91 () mySet)
+(declare-fun z3v93 () mySet)
+(declare-fun z3v94 () mySet)
+(declare-fun z3v96 () Int)
+(declare-fun z3f97 (Int) mySet)
+(declare-fun z3f98 (Int) Bool)
+(declare-fun z3v99 () Int)
+(declare-fun z3v102 () Int)
+(declare-fun z3v105 () mySet)
+(declare-fun z3v107 () mySet)
+(declare-fun z3v108 () mySet)
+(declare-fun z3v109 () Int)
+(declare-fun z3v110 () Int)
+(declare-fun z3v111 () Int)
+(declare-fun z3v112 () Int)
+(declare-fun z3v113 () mySet)
+(declare-fun z3v114 () mySet)
+(declare-fun z3v117 () mySet)
+(declare-fun z3v118 () mySet)
+(declare-fun z3v121 () mySet)
+(declare-fun z3v123 () mySet)
+(declare-fun z3v124 () mySet)
+(declare-fun z3v126 () mySet)
+(declare-fun z3v128 () Int)
+(declare-fun z3v132 () Int)
+(declare-fun z3v135 () mySet)
+(declare-fun z3v136 () mySet)
+(declare-fun z3v138 () mySet)
+(declare-fun z3v140 () Int)
+(declare-fun z3v143 () mySet)
+(declare-fun z3v144 () mySet)
+(declare-fun z3v145 () mySet)
+(declare-fun z3v146 () Int)
+(declare-fun z3v147 () Int)
+(declare-fun z3v148 () mySet)
+(declare-fun z3v149 () mySet)
+(declare-fun z3v155 () mySet)
+(declare-fun z3v156 () mySet)
+(declare-fun z3v157 () mySet)
+(declare-fun z3v160 () Int)
+(declare-fun z3v161 () Int)
+(declare-fun z3v162 () Int)
+(declare-fun z3v163 () Int)
+(declare-fun z3v164 () mySet)
+(declare-fun z3v165 () mySet)
+(declare-fun z3v169 () Int)
+(declare-fun z3v172 () mySet)
+(declare-fun z3v173 () mySet)
+(declare-fun z3v175 () Int)
+(declare-fun z3v176 () Int)
+(declare-fun z3v177 () Int)
+(declare-fun z3v178 () Int)
+(declare-fun z3f179 (Int Int) Int)
+(declare-fun z3v180 () Int)
+(declare-fun z3v181 () Int)
+(declare-fun z3f183 () Int)
+(declare-fun z3v184 () Int)
+(declare-fun z3v185 () Int)
+(declare-fun z3v186 () Int)
+(declare-fun z3v187 () Int)
+(declare-fun z3v188 () Int)
+(declare-fun z3v189 () Int)
+(declare-fun z3v192 () Int)
+(declare-fun z3v193 () Int)
+(declare-fun z3v197 () Int)
+(declare-fun z3v198 () mySet)
+(declare-fun z3v200 () Int)
+(declare-fun z3v201 () Int)
+(declare-fun z3v202 () Int)
+(declare-fun z3v203 () Int)
+(declare-fun z3v204 () Int)
+(declare-fun z3v206 () Int)
+(declare-fun z3v207 () Int)
+(declare-fun z3v208 () Int)
+(declare-fun z3v209 () Int)
+(declare-fun z3v210 () Int)
+(declare-fun z3v211 () Int)
+(declare-fun z3f212 (Int) Int)
+(declare-fun z3f213 (Int) Int)
+(declare-fun z3v214 () Int)
+(declare-fun z3v215 () Int)
+(declare-fun z3v217 () Int)
+(declare-fun z3v218 () Int)
+(declare-fun z3v219 () Int)
+(declare-fun z3v220 () Int)
+(declare-fun z3f221 (Int Int) Int)
+(declare-fun z3v222 () Int)
+(declare-fun z3v223 () Int)
+(declare-fun z3v224 () Int)
+(declare-fun z3v225 () Int)
+(declare-fun z3v226 () Int)
+(declare-fun z3v227 () Int)
+(declare-fun z3v228 () Int)
+(declare-fun z3v229 () Int)
+(declare-fun z3v230 () Int)
+(declare-fun z3v231 () Int)
+(declare-fun z3v232 () Int)
+(declare-fun z3v233 () Int)
+(declare-fun z3v234 () Int)
+(declare-fun z3v235 () Int)
+(declare-fun z3v236 () Int)
+(declare-fun z3v237 () Int)
+(declare-fun z3v238 () Int)
+(declare-fun z3v239 () Int)
+(declare-fun z3v240 () Int)
+(declare-fun z3v241 () Int)
+(declare-fun z3v242 () Int)
+(declare-fun z3v243 () Int)
+(declare-fun z3v244 () Int)
+(declare-fun z3v245 () Int)
+(declare-fun z3v246 () Int)
+(declare-fun z3v247 () Int)
+(declare-fun z3v248 () Int)
+(declare-fun z3v249 () Int)
+(declare-fun z3v250 () Int)
+(declare-fun z3v251 () Int)
+(declare-fun z3v252 () Int)
+(declare-fun z3v253 () Int)
+(declare-fun z3v254 () Int)
+(declare-fun z3v255 () Int)
+(declare-fun z3v256 () Int)
+(declare-fun z3v257 () Int)
+(declare-fun z3v258 () Int)
+(declare-fun z3v259 () Int)
+(declare-fun z3v260 () Int)
+(declare-fun z3v261 () Int)
+(declare-fun z3v262 () Int)
+(declare-fun z3v263 () Int)
+(declare-fun z3v264 () Int)
+(declare-fun z3v265 () Int)
+(declare-fun z3v266 () Int)
+(declare-fun z3v267 () Int)
+(declare-fun z3v268 () Int)
+(declare-fun z3v269 () Int)
+(declare-fun z3v271 () Int)
+(declare-fun z3v273 () Int)
+(declare-fun z3v275 () Int)
+(declare-fun z3v277 () Int)
+(declare-fun z3v279 () Int)
+(declare-fun z3v281 () Int)
+(declare-fun z3v283 () Int)
+(declare-fun z3v286 () Int)
+(declare-fun z3v289 () Int)
+(declare-fun z3v290 () Int)
+(declare-fun z3v291 () Int)
+(declare-fun z3v292 () mySet)
+(declare-fun z3v295 () mySet)
+(declare-fun z3v297 () Int)
+(declare-fun z3v301 () Int)
+(declare-fun z3v302 () Int)
+(declare-fun z3v303 () Int)
+(declare-fun z3v304 () Int)
+(declare-fun z3v305 () Int)
+(declare-fun z3v306 () Int)
+(declare-fun z3v307 () Int)
+(declare-fun z3v308 () Int)
+(declare-fun z3v309 () Int)
+(declare-fun z3v310 () Int)
+(declare-fun z3v312 () Int)
+(declare-fun z3v314 () Int)
+(declare-fun z3v315 () Int)
+(declare-fun z3v316 () Int)
+(declare-fun z3v317 () Int)
+(declare-fun z3v318 () Int)
+(declare-fun z3v319 () Int)
+(declare-fun z3v320 () Int)
+(declare-fun z3v321 () Int)
+(declare-fun z3v322 () Int)
+(declare-fun z3v324 () Int)
+(declare-fun z3v327 () Int)
+(declare-fun z3v328 () Int)
+(declare-fun z3v329 () Int)
+(declare-fun z3v330 () Int)
+(declare-fun z3v331 () Int)
+(declare-fun z3v332 () Int)
+(declare-fun z3v333 () Int)
+(declare-fun z3v334 () Int)
+(declare-fun z3v335 () Int)
+(declare-fun z3v336 () Int)
+(declare-fun z3v337 () Int)
+(declare-fun z3v338 () Int)
+(declare-fun z3v339 () Int)
+(declare-fun z3v340 () Int)
+(declare-fun z3v341 () Int)
+(declare-fun z3v342 () Int)
+(declare-fun z3v343 () Int)
+(declare-fun z3v345 () Int)
+(declare-fun z3v349 () Int)
+(declare-fun z3v350 () Int)
+(declare-fun z3v351 () Int)
+(declare-fun z3v352 () Int)
+(declare-fun z3v353 () Int)
+(declare-fun z3v354 () Int)
+(declare-fun z3v355 () Int)
+(declare-fun z3v359 () Int)
+(declare-fun z3v361 () Int)
+(declare-fun z3v362 () Int)
+(declare-fun z3v363 () Int)
+(declare-fun z3v364 () Int)
+(declare-fun z3v366 () Int)
+(declare-fun z3v367 () Int)
+(declare-fun z3v368 () Int)
+(declare-fun z3v369 () Int)
+(declare-fun z3v370 () Int)
+(declare-fun z3v375 () Int)
+(assert (= (z3f97 z3v328) (smt_set_cup (z3f97 z3v331) (z3f97 z3v375))))
+(assert (= (z3f97 z3v328) (smt_set_cup (z3f97 z3v330) (z3f97 z3v375))))
+(assert (= (z3f97 z3v328) (smt_set_cup (z3f97 z3v328) (z3f97 z3v375))))
+(assert (= (z3f97 z3v328) (smt_set_cup (z3f97 z3v327) (z3f97 z3v375))))
+(assert (= (z3f97 z3v331) (smt_set_cup (z3f97 z3v331) (z3f97 z3v375))))
+(assert (= (z3f97 z3v331) (smt_set_cup (z3f97 z3v330) (z3f97 z3v375))))
+(assert (= (z3f97 z3v331) (smt_set_cup (z3f97 z3v328) (z3f97 z3v375))))
+(assert (= (z3f97 z3v331) (smt_set_cup (z3f97 z3v327) (z3f97 z3v375))))
+(assert (= (z3f97 z3v375) (z3f97 z3v331)))
+(assert (= (z3f97 z3v375) (z3f97 z3v328)))
+(assert (= (z3f97 z3v375) (smt_set_cup (z3f97 z3v327) (z3f97 z3v331))))
+(assert (= (z3f97 z3v375) (smt_set_cup (z3f97 z3v327) (z3f97 z3v328))))
+(assert (= (z3f97 z3v375) (smt_set_cup (z3f97 z3v328) (z3f97 z3v331))))
+(assert (= (z3f97 z3v375) (smt_set_cup (z3f97 z3v328) (z3f97 z3v330))))
+(assert (= (z3f97 z3v375) (smt_set_cup (z3f97 z3v328) (z3f97 z3v328))))
+(assert (= (z3f97 z3v375) (smt_set_cup (z3f97 z3v328) (z3f97 z3v327))))
+(assert (= (z3f97 z3v375) (smt_set_cup (z3f97 z3v330) (z3f97 z3v331))))
+(assert (= (z3f97 z3v375) (smt_set_cup (z3f97 z3v330) (z3f97 z3v328))))
+(assert (= (z3f97 z3v375) (smt_set_cup (z3f97 z3v331) (z3f97 z3v331))))
+(assert (= (z3f97 z3v375) (smt_set_cup (z3f97 z3v331) (z3f97 z3v330))))
+(assert (= (z3f97 z3v375) (smt_set_cup (z3f97 z3v331) (z3f97 z3v328))))
+(assert (= (z3f97 z3v375) (smt_set_cup (z3f97 z3v331) (z3f97 z3v327))))
+(assert (smt_set_sub (z3f97 z3v375) (z3f97 z3v331)))
+(assert (smt_set_sub (z3f97 z3v375) (z3f97 z3v328)))
+(assert (<= z3v375 z3v331))
+(assert (<= z3v375 z3v328))
+(assert (= z3v375 z3v328))
+(assert (>= z3v375 z3v331))
+(assert (>= z3v375 z3v328))
+(assert (not (= z3v375 z3v330)))
+(assert (not (= z3v375 z3v327)))
+(assert (<= (z3f76 z3v375) (z3f76 z3v331)))
+(assert (<= (z3f76 z3v375) (z3f76 z3v328)))
+(assert (>  (z3f76 z3v375) (z3f76 z3v330)))
+(assert (>  (z3f76 z3v375) (z3f76 z3v327)))
+(assert (>= (z3f76 z3v375) (z3f76 z3v331)))
+(assert (>= (z3f76 z3v375) (z3f76 z3v330)))
+(assert (>= (z3f76 z3v375) (z3f76 z3v328)))
+(assert (>= (z3f76 z3v375) (z3f76 z3v327)))
+(assert (= (z3f76 z3v375) (z3f76 z3v331)))
+(assert (= (z3f76 z3v375) (z3f76 z3v328)))
+(assert (>  (z3f76 z3v375) 0))
+(assert (= z3v375 z3v331))
+(assert (>= (z3f76 z3v375) 0))
+(assert (and (>= (z3f76 z3v327) 0) (>= (z3f76 z3v328) 0) (= (z3f97 z3v328) (smt_set_cup (smt_set_add smt_set_emp z3v329) (z3f97 z3v330))) (= (z3f76 z3v328) (+ 1 (z3f76 z3v330))) (= (z3f98 z3v328) false) (= z3v328 (z3f179 z3v329 z3v330)) (>= (z3f76 z3v328) 0) (= z3v328 z3v331) (>= (z3f76 z3v328) 0) (>= (z3f76 z3v330) 0) (>= (z3f76 z3v331) 0) (z3f62 z3v60) (= (z3f64 z3v63) z3v63) (= (z3f64 z3v65) z3v65) (not (z3f62 z3v61)) (= (z3f64 z3v66) z3v66)))
+(assert (not (= (z3f97 z3v327) (smt_set_cup (z3f97 z3v327) (z3f97 z3v375)))))
+(check-sat)
diff --git a/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.cvc4.10.smt2 b/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.cvc4.10.smt2
new file mode 100644
index 000000000..f37a8ccfe
--- /dev/null
+++ b/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.cvc4.10.smt2
@@ -0,0 +1,106 @@
+(set-logic QF_ALL_SUPPORTED)
+(set-info :status unsat)
+(define-sort Elt () Int)
+(define-sort mySet () (Set Elt ))
+(define-fun smt_set_emp () mySet (as emptyset mySet))
+(define-fun smt_set_mem ((x Elt) (s mySet)) Bool (in x s))
+(define-fun smt_set_add ((s mySet) (x Elt)) mySet (union s (setenum x)))
+(define-fun smt_set_cup ((s1 mySet) (s2 mySet)) mySet (union s1 s2))
+(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (intersection s1 s2))
+(define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (setminus s1 s2))
+(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subseteq s1 s2))
+(declare-fun z3v66 () Int)
+(declare-fun z3v67 () Int)
+(assert (distinct z3v66 z3v67))
+(declare-fun z3v68 () Int)
+(declare-fun z3f69 (Int) Int)
+(declare-fun z3f70 (Int) mySet)
+(declare-fun z3v71 () Int)
+(declare-fun z3f72 (Int) mySet)
+(declare-fun z3v73 () Int)
+(declare-fun z3v74 () Int)
+(declare-fun z3v75 () Int)
+(declare-fun z3f76 (Int) Bool)
+(declare-fun z3f77 (Int Int) Int)
+(declare-fun z3v78 () Int)
+(declare-fun z3f79 (Int) Bool)
+(declare-fun z3v80 () Int)
+(declare-fun z3f81 (Int) Int)
+(declare-fun z3v82 () Int)
+(declare-fun z3v83 () Int)
+(declare-fun z3v85 () Int)
+(declare-fun z3v86 () Int)
+(declare-fun z3v87 () Int)
+(declare-fun z3f88 () Int)
+(declare-fun z3v89 () Int)
+(declare-fun z3v90 () Int)
+(declare-fun z3v91 () Int)
+(declare-fun z3v92 () Int)
+(declare-fun z3v93 () Int)
+(declare-fun z3f94 (Int) Int)
+(declare-fun z3f95 (Int) Int)
+(declare-fun z3f96 (Int Int Int) Int)
+(declare-fun z3v97 () Int)
+(declare-fun z3v98 () Int)
+(declare-fun z3v99 () Int)
+(assert (= z3v99 z3v98))
+(assert (and (>= (z3f69 z3v85) 0)
+             (not (smt_set_mem z3v86 (z3f70 z3v85)))
+             (= (z3f72 z3v85) smt_set_emp)
+             (>= (z3f69 z3v87) 0)
+             (= (z3f72 z3v87) smt_set_emp)
+             (= (z3f70 z3v87) smt_set_emp)
+             (= (z3f69 z3v87) 0)
+             (= (z3f76 z3v87) true)
+             (= z3v87 z3f88)
+             (>= (z3f69 z3v87) 0)
+             (= z3v87 z3v89)
+             (>= (z3f69 z3v87) 0)
+             (= (z3f70 z3v87)
+                (z3f70 z3v90))
+             (= (z3f72 z3v87) smt_set_emp)
+             (>= (z3f69 z3v89) 0)
+             (= (z3f70 z3v89)
+                (z3f70 z3v90))
+             (= (z3f72 z3v89) smt_set_emp)
+             (>= (z3f69 z3v90) 0)
+             (= (z3f72 z3v90)
+                (ite (smt_set_mem z3v86 (z3f70 z3v85))
+                     (smt_set_cup (smt_set_add smt_set_emp z3v86)
+                                  (z3f72 z3v85))
+                     (z3f72 z3v85)))
+             (= (z3f70 z3v90)
+                (smt_set_cup (smt_set_add smt_set_emp z3v86)
+                             (z3f70 z3v85)))
+             (= (z3f69 z3v90)
+                (+ 1 (z3f69 z3v85)))
+             (= (z3f76 z3v90) false)
+             (>= (z3f69 z3v91) 0)
+             (= (z3f72 z3v91) smt_set_emp)
+             (= (z3f70 z3v91) smt_set_emp)
+             (= (z3f69 z3v91) 0)
+             (= (z3f76 z3v91) true)
+             (= z3v91 z3f88)
+             (>= (z3f69 z3v91) 0)
+             (= z3v91 z3v92)
+             (>= (z3f69 z3v91) 0)
+             (not (smt_set_mem z3v86 (z3f70 z3v91)))
+             (= (z3f72 z3v91) smt_set_emp)
+             (= (z3f94 z3v93) z3v92)
+             (= (z3f95 z3v93) z3v85)
+             (= z3v93 (z3f96 z3v86 z3v92 z3v85))
+             (= z3v93 z3v97)
+             (= (smt_set_cap (z3f70 (z3f94 z3v93))
+                             (z3f70 (z3f95 z3v93))) smt_set_emp)
+             (>= (z3f69 z3v92) 0)
+             (not (smt_set_mem z3v86 (z3f70 z3v92)))
+             (= (z3f72 z3v92) smt_set_emp)
+             (= (smt_set_cap (z3f70 (z3f94 z3v97))
+                             (z3f70 (z3f95 z3v97))) smt_set_emp)
+             (z3f79 z3v66)
+             (= (z3f81 z3v80) z3v80)
+             (= (z3f81 z3v82) z3v82)
+             (not (z3f79 z3v67))
+             (= (z3f81 z3v83) z3v83)))
+(assert (not (>  z3v99 z3v98)))
+(check-sat)
diff --git a/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.cvc4.1832.smt2 b/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.cvc4.1832.smt2
new file mode 100644
index 000000000..59cc1a00e
--- /dev/null
+++ b/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.cvc4.1832.smt2
@@ -0,0 +1,227 @@
+(set-logic QF_ALL_SUPPORTED)
+(set-info :status unsat)
+(define-sort Elt () Int)
+(define-sort mySet () (Set Elt ))
+(define-fun smt_set_emp () mySet (as emptyset mySet))
+(define-fun smt_set_mem ((x Elt) (s mySet)) Bool (in x s))
+(define-fun smt_set_add ((s mySet) (x Elt)) mySet (union s (setenum x)))
+(define-fun smt_set_cup ((s1 mySet) (s2 mySet)) mySet (union s1 s2))
+(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (intersection s1 s2))
+;(define-fun smt_set_com ((s mySet)) mySet ((_ map not) s))
+(define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (setminus s1 s2))
+;(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (= smt_set_emp (smt_set_dif s1 s2)))
+(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subseteq s1 s2))
+(declare-fun z3v66 () Int)
+(declare-fun z3v67 () Int)
+(assert (distinct z3v66 z3v67))
+(declare-fun z3v68 () Int)
+(declare-fun z3f69 (Int) Int)
+(declare-fun z3f70 (Int) mySet)
+(declare-fun z3v71 () Int)
+(declare-fun z3f72 (Int) mySet)
+(declare-fun z3v73 () Int)
+(declare-fun z3v74 () Int)
+(declare-fun z3v75 () Int)
+(declare-fun z3f76 (Int) Bool)
+(declare-fun z3f77 (Int Int) Int)
+(declare-fun z3v78 () Int)
+(declare-fun z3f79 (Int) Bool)
+(declare-fun z3v80 () Int)
+(declare-fun z3f81 (Int) Int)
+(declare-fun z3v82 () Int)
+(declare-fun z3v83 () Int)
+(declare-fun z3v85 () Int)
+(declare-fun z3v86 () Int)
+(declare-fun z3v87 () Int)
+(declare-fun z3f88 () Int)
+(declare-fun z3v89 () Int)
+(declare-fun z3v90 () Int)
+(declare-fun z3v91 () Int)
+(declare-fun z3v92 () Int)
+(declare-fun z3v93 () Int)
+(declare-fun z3f94 (Int) Int)
+(declare-fun z3f95 (Int) Int)
+(declare-fun z3f96 (Int Int Int) Int)
+(declare-fun z3v97 () Int)
+(declare-fun z3v98 () Int)
+(declare-fun z3v99 () Int)
+(declare-fun z3v100 () Int)
+(declare-fun z3v101 () Int)
+(declare-fun z3v102 () Int)
+(declare-fun z3v103 () Int)
+(declare-fun z3v104 () Int)
+(declare-fun z3v105 () Int)
+(declare-fun z3v106 () Int)
+(declare-fun z3v107 () Int)
+(declare-fun z3v108 () Int)
+(declare-fun z3v109 () Int)
+(declare-fun z3v110 () Int)
+(declare-fun z3v113 () Int)
+(declare-fun z3v114 () Int)
+(declare-fun z3v115 () Int)
+(declare-fun z3v116 () Int)
+(declare-fun z3v117 () Int)
+(declare-fun z3v118 () Int)
+(declare-fun z3v120 () Int)
+(declare-fun z3v121 () Int)
+(declare-fun z3v122 () Int)
+(declare-fun z3v124 () Int)
+(declare-fun z3v125 () Int)
+(declare-fun z3v126 () Int)
+(declare-fun z3v127 () Int)
+(declare-fun z3v128 () Int)
+(declare-fun z3v129 () Int)
+(declare-fun z3v131 () Int)
+(declare-fun z3v132 () Int)
+(declare-fun z3v133 () Int)
+(declare-fun z3v134 () Int)
+(declare-fun z3v135 () Int)
+(declare-fun z3v136 () Int)
+(declare-fun z3v137 () Int)
+(declare-fun z3v138 () Int)
+(declare-fun z3v139 () Int)
+(declare-fun z3v140 () Int)
+(declare-fun z3v141 () Int)
+(declare-fun z3v142 () Int)
+(declare-fun z3v144 () Int)
+(declare-fun z3v145 () Int)
+(declare-fun z3v146 () Int)
+(declare-fun z3v149 () Int)
+(declare-fun z3v151 () Int)
+(declare-fun z3v154 () Int)
+(declare-fun z3v155 () Int)
+(declare-fun z3v156 () Int)
+(declare-fun z3v157 () Int)
+(declare-fun z3v158 () Int)
+(declare-fun z3v159 () Int)
+(declare-fun z3v161 () Int)
+(declare-fun z3v163 () Int)
+(declare-fun z3v164 () Int)
+(declare-fun z3v165 () Int)
+(declare-fun z3v167 () Int)
+(declare-fun z3v170 () Int)
+(declare-fun z3v174 () Int)
+(declare-fun z3v175 () Int)
+(declare-fun z3v176 () Int)
+(declare-fun z3v179 () Int)
+(declare-fun z3v181 () Int)
+(declare-fun z3v182 () Int)
+(declare-fun z3v183 () Int)
+(declare-fun z3v184 () Int)
+(declare-fun z3v187 () Int)
+(declare-fun z3v188 () Int)
+(declare-fun z3v189 () Int)
+(declare-fun z3v190 () Int)
+(declare-fun z3f191 (Int) Int)
+(declare-fun z3f192 (Int) Int)
+(declare-fun z3v195 () Int)
+(declare-fun z3v196 () Int)
+(declare-fun z3v199 () Int)
+(declare-fun z3v200 () Int)
+(declare-fun z3v201 () Int)
+(declare-fun z3v202 () Int)
+(declare-fun z3v203 () Int)
+(declare-fun z3v206 () Int)
+(declare-fun z3v207 () Int)
+(declare-fun z3v208 () Int)
+(declare-fun z3v210 () Int)
+(declare-fun z3v211 () Int)
+(declare-fun z3v212 () Int)
+(declare-fun z3f213 (Int) Bool)
+(declare-fun z3f214 (Int) Int)
+(declare-fun z3v215 () Int)
+(declare-fun z3v216 () Int)
+(declare-fun z3v218 () Int)
+(declare-fun z3v220 () Int)
+(declare-fun z3v221 () Int)
+(declare-fun z3v222 () Int)
+(declare-fun z3v223 () Int)
+(declare-fun z3v224 () Int)
+(declare-fun z3v225 () Int)
+(declare-fun z3v226 () Int)
+(declare-fun z3v227 () Int)
+(declare-fun z3v228 () Int)
+(declare-fun z3v229 () Int)
+(declare-fun z3v230 () Int)
+(declare-fun z3v231 () Int)
+(declare-fun z3v233 () Int)
+(declare-fun z3v236 () Int)
+(declare-fun z3v242 () Int)
+(declare-fun z3v243 () Int)
+(declare-fun z3v244 () Int)
+(declare-fun z3v245 () Int)
+(declare-fun z3v247 () Int)
+(declare-fun z3v248 () Int)
+(declare-fun z3v249 () Int)
+(declare-fun z3v250 () Int)
+(declare-fun z3v251 () Int)
+(declare-fun z3v252 () Int)
+(declare-fun z3v253 () Int)
+(declare-fun z3v255 () Int)
+(declare-fun z3v256 () Int)
+(declare-fun z3v258 () Int)
+(declare-fun z3v259 () Int)
+(declare-fun z3v261 () Int)
+(declare-fun z3v262 () Int)
+(declare-fun z3v263 () Int)
+(declare-fun z3v264 () Int)
+(declare-fun z3v266 () Int)
+(declare-fun z3v268 () Int)
+(declare-fun z3v270 () Int)
+(declare-fun z3v271 () Int)
+(declare-fun z3v272 () Int)
+(declare-fun z3v274 () Int)
+(declare-fun z3v275 () Int)
+(declare-fun z3v276 () Int)
+(declare-fun z3v278 () Int)
+(declare-fun z3v279 () Int)
+(declare-fun z3v281 () Int)
+(declare-fun z3v282 () Int)
+(declare-fun z3v283 () Int)
+(declare-fun z3v284 () Int)
+(declare-fun z3v285 () Int)
+(declare-fun z3v287 () Int)
+(declare-fun z3v289 () Int)
+(declare-fun z3v290 () Int)
+(declare-fun z3v291 () Int)
+(declare-fun z3v292 () Int)
+(declare-fun z3v293 () Int)
+(declare-fun z3v296 () Int)
+(declare-fun z3v298 () Int)
+(declare-fun z3v299 () Int)
+(declare-fun z3f300 (Int Int) Int)
+(declare-fun z3v301 () Int)
+(declare-fun z3v302 () Int)
+(declare-fun z3v303 () Int)
+(declare-fun z3v304 () Int)
+(declare-fun z3v308 () Int)
+(declare-fun z3v309 () Int)
+(declare-fun z3v310 () Int)
+(declare-fun z3v314 () Int)
+(declare-fun z3v315 () Int)
+(declare-fun z3v316 () Int)
+(declare-fun z3v317 () Int)
+(declare-fun z3v318 () Int)
+(declare-fun z3v319 () Int)
+(declare-fun z3v320 () Int)
+(declare-fun z3v324 () Int)
+(declare-fun z3v325 () Int)
+(declare-fun z3v326 () Int)
+(declare-fun z3v327 () Int)
+(declare-fun z3v328 () Int)
+(declare-fun z3v330 () Int)
+(declare-fun z3v332 () Int)
+(declare-fun z3v333 () Int)
+(declare-fun z3v334 () Int)
+(declare-fun z3v335 () Int)
+(declare-fun z3v336 () Int)
+(declare-fun z3v337 () Int)
+(declare-fun z3v339 () Int)
+(declare-fun z3v340 () Int)
+(declare-fun z3v341 () Int)
+(declare-fun z3v342 () Int)
+(assert (= z3v342 z3v113))
+(assert (>= (z3f69 z3v342) 0))
+(assert (and (>= (z3f69 z3v113) 0) (>= (z3f69 z3v114) 0) (= (z3f72 z3v114) smt_set_emp) (= (z3f70 z3v114) smt_set_emp) (= (z3f69 z3v114) 0) (= (z3f76 z3v114) true) (>= (z3f69 z3v115) 0) (= (z3f72 z3v115) (ite (smt_set_mem z3v116 (z3f70 z3v113)) (smt_set_cup (smt_set_add smt_set_emp z3v116) (z3f72 z3v113)) (z3f72 z3v113))) (= (z3f70 z3v115) (smt_set_cup (smt_set_add smt_set_emp z3v116) (z3f70 z3v113))) (= (z3f69 z3v115) (+ 1 (z3f69 z3v113))) (= (z3f76 z3v115) false) (= z3v115 (z3f77 z3v116 z3v113)) (>= (z3f69 z3v115) 0) (= z3v115 z3v117) (>= (z3f69 z3v115) 0) (= (z3f72 z3v115) smt_set_emp) (>= (z3f69 z3v117) 0) (= (z3f72 z3v117) smt_set_emp) (z3f79 z3v66) (= (z3f81 z3v80) z3v80) (= (z3f81 z3v82) z3v82) (not (z3f79 z3v67)) (= (z3f81 z3v83) z3v83)))
+(assert (not (and (= (z3f72 z3v342) smt_set_emp) (not (smt_set_mem z3v116 (z3f70 z3v342))))))
+(check-sat)
diff --git a/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.minimized10.smt2 b/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.minimized10.smt2
new file mode 100644
index 000000000..5fa5101f0
--- /dev/null
+++ b/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.minimized10.smt2
@@ -0,0 +1,27 @@
+(set-logic QF_ALL_SUPPORTED)
+(set-info :status unsat)
+
+; Observed
+;
+; sat as output instead of unsat
+;
+; What was going on?
+;
+; The solver was unable to reason that (emptyset) cannot equal
+; (setenum 0). There were no membership predicates anywhere, just
+; equalities.
+;
+; Fix
+;
+; Add the propagation rule: (true) => (in x (setenum x))
+
+(declare-fun z3f70 (Int) (Set Int))
+(declare-fun z3v85 () Int)
+(declare-fun z3v86 () Int)
+(declare-fun z3v87 () Int)
+(declare-fun z3v90 () Int)
+
+(assert (= (z3f70 z3v90) (union (z3f70 z3v85) (union (as emptyset (Set Int)) (setenum 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
new file mode 100644
index 000000000..d01b7468e
--- /dev/null
+++ b/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.minimized1832.smt2
@@ -0,0 +1,18 @@
+(set-logic QF_ALL_SUPPORTED)
+(set-info :status unsat)
+(define-sort Elt () Int)
+(define-sort mySet ()
+  (Set Elt ))
+(define-fun smt_set_emp () mySet (as emptyset mySet))
+
+(declare-fun S () (Set Int))
+(declare-fun T () (Set Int))
+(declare-fun x () Int)
+
+(assert (or (not (= S smt_set_emp)) (in x T)))
+
+(assert (= smt_set_emp 
+           (ite (in x T) 
+                (union (union smt_set_emp (setenum x)) S) 
+                S)))
+(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
new file mode 100644
index 000000000..57d5d72ca
--- /dev/null
+++ b/test/regress/regress0/sets/rec_copy_loop_check_heap_access_43_4.smt2
@@ -0,0 +1,149 @@
+(set-option :print-success false)
+(set-logic AUFLIA_SETS)
+(set-info :status unsat)
+(declare-sort Loc 0)
+(define-sort SetLoc () (Set Loc))
+(define-sort SetInt () (Set Int))
+(declare-sort FldLoc 0)
+(declare-sort FldInt 0)
+(declare-fun null$0 () Loc)
+(declare-fun read$0 (FldLoc Loc) Loc)
+(declare-fun Btwn$0 (FldLoc Loc Loc Loc) Bool)
+(declare-fun Alloc$0 () SetLoc)
+(declare-fun Alloc_2$0 () SetLoc)
+(declare-fun FP$0 () SetLoc)
+(declare-fun FP_3$0 () SetLoc)
+(declare-fun FP_Caller$0 () SetLoc)
+(declare-fun FP_Caller_2$0 () SetLoc)
+(declare-fun cp$0 () Loc)
+(declare-fun cp_1$0 () Loc)
+(declare-fun curr$0 () Loc)
+(declare-fun lseg_domain$0 (FldLoc Loc Loc) SetLoc)
+(declare-fun lseg_struct$0 (SetLoc FldLoc Loc Loc) Bool)
+(declare-fun next$0 () FldLoc)
+(declare-fun old_cp_2$0 () Loc)
+(declare-fun sk_?X_36$0 () SetLoc)
+(declare-fun sk_?X_37$0 () SetLoc)
+(declare-fun sk_?X_38$0 () SetLoc)
+(declare-fun tmp_1$0 () Loc)
+
+(assert (! (forall ((?y Loc))
+           (or (not (Btwn$0 next$0 null$0 ?y ?y)) (= null$0 ?y)
+               (Btwn$0 next$0 null$0 (read$0 next$0 null$0) ?y)))
+   :named btwn_reach_6))
+
+(assert (! (forall ((?y Loc))
+           (or (not (= (read$0 next$0 null$0) null$0))
+               (not (Btwn$0 next$0 null$0 ?y ?y)) (= null$0 ?y)))
+   :named btwn_cycl_6))
+
+(assert (! (Btwn$0 next$0 null$0 (read$0 next$0 null$0) (read$0 next$0 null$0))
+   :named btwn_step_6))
+
+(assert (! (= (read$0 next$0 null$0) null$0) :named read_null_6))
+
+(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))
+                    (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))))))
+   :named lseg_footprint_14))
+
+(assert (! (not (in tmp_1$0 Alloc$0)) :named new_42_10))
+
+(assert (! (not (in 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))
+
+(assert (! (lseg_struct$0 sk_?X_37$0 next$0 curr$0 null$0)
+   :named precondition_of_rec_copy_loop_34_11_16))
+
+(assert (! (= sk_?X_38$0 (lseg_domain$0 next$0 cp$0 null$0))
+   :named precondition_of_rec_copy_loop_34_11_17))
+
+(assert (! (= sk_?X_36$0 FP$0) :named precondition_of_rec_copy_loop_34_11_18))
+
+(assert (! (= (as emptyset SetLoc) (intersection sk_?X_38$0 sk_?X_37$0))
+   :named precondition_of_rec_copy_loop_34_11_19))
+
+(assert (! (= old_cp_2$0 cp$0) :named assign_41_4))
+
+(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 (! (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)))
+   :named unnamed_22))
+
+(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))
+                    (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))))))
+   :named lseg_footprint_15))
+
+(assert (! (not (in cp_1$0 FP_3$0)) :named check_heap_access_43_4))
+
+(assert (! (not (= tmp_1$0 null$0)) :named new_42_10_1))
+
+(assert (! (lseg_struct$0 sk_?X_38$0 next$0 cp$0 null$0)
+   :named precondition_of_rec_copy_loop_34_11_20))
+
+(assert (! (= FP_Caller$0 (union FP$0 FP_Caller$0))
+   :named precondition_of_rec_copy_loop_34_11_21))
+
+(assert (! (= sk_?X_37$0 (lseg_domain$0 next$0 curr$0 null$0))
+   :named precondition_of_rec_copy_loop_34_11_22))
+
+(assert (! (= sk_?X_36$0 (union sk_?X_37$0 sk_?X_38$0))
+   :named precondition_of_rec_copy_loop_34_11_23))
+
+(assert (! (= Alloc$0 (union FP_Caller$0 Alloc$0))
+   :named initial_footprint_of_rec_copy_loop_34_11_5))
+
+(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 (! (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)))
+   :named unnamed_23))
+
+(assert (! (forall ((?x Loc)) (Btwn$0 next$0 ?x ?x ?x)) :named btwn_refl_6))
+
+(assert (! (forall ((?x Loc) (?y Loc)) (or (not (Btwn$0 next$0 ?x ?y ?x)) (= ?x ?y)))
+   :named btwn_sndw_6))
+
+(assert (! (forall ((?x Loc) (?y Loc) (?z Loc))
+           (or (not (Btwn$0 next$0 ?x ?y ?y)) (not (Btwn$0 next$0 ?x ?z ?z))
+               (Btwn$0 next$0 ?x ?y ?z) (Btwn$0 next$0 ?x ?z ?y)))
+   :named btwn_ord1_6))
+
+(assert (! (forall ((?x Loc) (?y Loc) (?z Loc))
+           (or (not (Btwn$0 next$0 ?x ?y ?z))
+               (and (Btwn$0 next$0 ?x ?y ?y) (Btwn$0 next$0 ?y ?z ?z))))
+   :named btwn_ord2_6))
+
+(assert (! (forall ((?x Loc) (?y Loc) (?z Loc))
+           (or (not (Btwn$0 next$0 ?x ?y ?y)) (not (Btwn$0 next$0 ?y ?z ?z))
+               (Btwn$0 next$0 ?x ?z ?z)))
+   :named btwn_trn1_6))
+
+(assert (! (forall ((?u Loc) (?x Loc) (?y Loc) (?z Loc))
+           (or (not (Btwn$0 next$0 ?x ?y ?z)) (not (Btwn$0 next$0 ?y ?u ?z))
+               (and (Btwn$0 next$0 ?x ?y ?u) (Btwn$0 next$0 ?x ?u ?z))))
+   :named btwn_trn2_6))
+
+(assert (! (forall ((?u Loc) (?x Loc) (?y Loc) (?z Loc))
+           (or (not (Btwn$0 next$0 ?x ?y ?z)) (not (Btwn$0 next$0 ?x ?u ?y))
+               (and (Btwn$0 next$0 ?x ?u ?z) (Btwn$0 next$0 ?u ?y ?z))))
+   :named btwn_trn3_6))
+
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/sets/setel-eq.smt2 b/test/regress/regress0/sets/setel-eq.smt2
new file mode 100644
index 000000000..8ed9a2e57
--- /dev/null
+++ b/test/regress/regress0/sets/setel-eq.smt2
@@ -0,0 +1,10 @@
+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+(declare-fun S () (Set Int))
+(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 (= x y))
+(check-sat)
diff --git a/test/regress/regress0/sets/sets-equal.smt2 b/test/regress/regress0/sets/sets-equal.smt2
new file mode 100644
index 000000000..a2ce4b3c2
--- /dev/null
+++ b/test/regress/regress0/sets/sets-equal.smt2
@@ -0,0 +1,14 @@
+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+(declare-fun x () Int)
+(declare-fun y () Int)
+(declare-fun z () Int)
+(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 (= x z))
+(assert (not (in 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
new file mode 100644
index 000000000..0f5e41864
--- /dev/null
+++ b/test/regress/regress0/sets/sets-inter.smt2
@@ -0,0 +1,11 @@
+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+(define-sort SetInt () (Set Int))
+(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)))
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/sets/sets-new.smt2 b/test/regress/regress0/sets/sets-new.smt2
new file mode 100644
index 000000000..c85ae4837
--- /dev/null
+++ b/test/regress/regress0/sets/sets-new.smt2
@@ -0,0 +1,17 @@
+; COMMAND-LINE: --no-check-models
+; EXPECT: sat
+(set-logic ALL_SUPPORTED)
+(set-info :status sat)
+(define-sort SetInt () (Set Int))
+
+(declare-fun A () SetInt)
+(declare-fun B () SetInt)
+(declare-fun x () Int)
+(assert (in 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))
+
+(check-sat)
diff --git a/test/regress/regress0/sets/sets-sample.smt2 b/test/regress/regress0/sets/sets-sample.smt2
new file mode 100644
index 000000000..1bd0eb396
--- /dev/null
+++ b/test/regress/regress0/sets/sets-sample.smt2
@@ -0,0 +1,64 @@
+; COMMAND-LINE: --incremental
+; EXPECT: unsat
+; EXPECT: unsat
+; EXPECT: unsat
+; EXPECT: unsat
+(set-logic ALL_SUPPORTED)
+(define-sort SetInt () (Set Int))
+
+; Something simple to test parsing
+(push 1)
+(declare-fun a () (Set Int))
+(declare-fun b () (Set Int))
+(declare-fun c () (Set Int))
+(declare-fun e () Int)
+(assert (= a (setenum 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)))
+(check-sat)
+(pop 1)
+
+; UF can tell that this is UNSAT (union)
+(push 1)
+(declare-fun x () (Set Int))
+(declare-fun y () (Set Int))
+(declare-fun z () (Set Int))
+(assert (= x y))
+(assert (not (= (union x z) (union y z))))
+(check-sat)
+(pop 1)
+
+; UF can tell that this is UNSAT (containment)
+(push 1)
+(declare-fun x () (Set Int))
+(declare-fun y () (Set Int))
+(declare-fun e1 () Int)
+(declare-fun e2 () Int)
+(assert (= x y))
+(assert (= e1 e2))
+(assert (in e1 x))
+(assert (not (in e2 y)))
+(check-sat)
+(pop 1)
+
+; UF can tell that this is UNSAT (merge union + containment examples)
+(push 1)
+(declare-fun x () (Set Int))
+(declare-fun y () (Set Int))
+(declare-fun z () (Set Int))
+(declare-fun e1 () Int)
+(declare-fun e2 () Int)
+(assert (= x y))
+(assert (= e1 e2))
+(assert (in e1 (union x z)))
+(assert (not (in e2 (union y z))))
+(check-sat)
+(pop 1)
+ 
+(exit) 
+(exit)
diff --git a/test/regress/regress0/sets/sets-sharing.smt2 b/test/regress/regress0/sets/sets-sharing.smt2
new file mode 100644
index 000000000..d2a94fdf4
--- /dev/null
+++ b/test/regress/regress0/sets/sets-sharing.smt2
@@ -0,0 +1,11 @@
+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+
+(declare-fun S () (Set Int))
+(declare-fun x () Int)
+
+(assert (in (+ 5 x) S))
+(assert (not (in 9 S)))
+(assert (= x 4))
+
+(check-sat)
diff --git a/test/regress/regress0/sets/sets-testlemma.smt2 b/test/regress/regress0/sets/sets-testlemma.smt2
new file mode 100644
index 000000000..74ce72747
--- /dev/null
+++ b/test/regress/regress0/sets/sets-testlemma.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --no-check-models
+; EXPECT: sat
+(set-logic QF_UFLIA_SETS)
+(set-info :status sat)
+(declare-fun x () (Set (_ BitVec 2)))
+(declare-fun y () (Set (_ BitVec 2)))
+(assert (not (= x y)))
+(check-sat)
diff --git a/test/regress/regress0/sets/sets-union.smt2 b/test/regress/regress0/sets/sets-union.smt2
new file mode 100644
index 000000000..6f6d3e019
--- /dev/null
+++ b/test/regress/regress0/sets/sets-union.smt2
@@ -0,0 +1,15 @@
+; COMMAND-LINE: --incremental --no-check-model
+; EXPECT: sat
+; EXPECT: unsat
+(set-logic ALL_SUPPORTED)
+(define-sort SetInt () (Set Int))
+(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)))
+(check-sat)
+;(get-model)
+(assert (not (in x b)))
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/sets/union-1a-flip.smt2 b/test/regress/regress0/sets/union-1a-flip.smt2
new file mode 100644
index 000000000..59c2a2024
--- /dev/null
+++ b/test/regress/regress0/sets/union-1a-flip.smt2
@@ -0,0 +1,16 @@
+; COMMAND-LINE: --incremental --no-check-models
+; EXPECT: unsat
+; EXPECT: sat
+
+; x not in A U B => x not in A
+(set-logic ALL_SUPPORTED)
+(define-sort SetInt () (Set Int))
+(declare-fun A () (Set Int))
+(declare-fun B () (Set Int))
+(declare-fun x () Int)
+(assert (in x A))
+(push 1)
+(assert (not (in 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
new file mode 100644
index 000000000..b594ac74d
--- /dev/null
+++ b/test/regress/regress0/sets/union-1a.smt2
@@ -0,0 +1,16 @@
+; COMMAND-LINE: --incremental
+; EXPECT: unsat
+; EXPECT: sat
+
+; x not in A U B => x not in A
+(set-logic ALL_SUPPORTED)
+(define-sort SetInt () (Set Int))
+(declare-fun A () (Set Int))
+(declare-fun B () (Set Int))
+(declare-fun x () Int)
+(assert (not (in x (union A B))))
+(push 1)
+(assert (in 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
new file mode 100644
index 000000000..86fed459b
--- /dev/null
+++ b/test/regress/regress0/sets/union-1b-flip.smt2
@@ -0,0 +1,16 @@
+; COMMAND-LINE: --incremental --no-check-models
+; EXPECT: unsat
+; EXPECT: sat
+
+; x not in A U B => x not in A
+(set-logic ALL_SUPPORTED)
+(define-sort SetInt () (Set Int))
+(declare-fun A () (Set Int))
+(declare-fun B () (Set Int))
+(declare-fun x () Int)
+(assert (in x B))
+(push 1)
+(assert (not (in 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
new file mode 100644
index 000000000..85fce759c
--- /dev/null
+++ b/test/regress/regress0/sets/union-1b.smt2
@@ -0,0 +1,16 @@
+; COMMAND-LINE: --incremental
+; EXPECT: unsat
+; EXPECT: sat
+
+; x not in A U B => x not in A
+(set-logic ALL_SUPPORTED)
+(define-sort SetInt () (Set Int))
+(declare-fun A () (Set Int))
+(declare-fun B () (Set Int))
+(declare-fun x () Int)
+(assert (not (in x (union A B))))
+(push 1)
+(assert (in 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
new file mode 100644
index 000000000..32d949a53
--- /dev/null
+++ b/test/regress/regress0/sets/union-2.smt2
@@ -0,0 +1,13 @@
+; COMMAND-LINE: --no-check-models
+; EXPECT: sat
+(set-logic ALL_SUPPORTED)
+(set-info :status sat)
+(define-sort SetInt () (Set Int))
+(declare-fun A () (Set Int))
+(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)))
+(check-sat)
diff --git a/test/unit/theory/logic_info_white.h b/test/unit/theory/logic_info_white.h
index 5f6a93ae7..f569d6389 100644
--- a/test/unit/theory/logic_info_white.h
+++ b/test/unit/theory/logic_info_white.h
@@ -512,6 +512,7 @@ public:
     info = info.getUnlockedCopy();
     TS_ASSERT( !info.isLocked() );
     info.disableTheory(THEORY_STRINGS);
+    info.disableTheory(THEORY_SETS);
     info.arithOnlyLinear();
     info.disableIntegers();
     info.lock();