Merge remote-tracking branch 'origin/master'

42 files changed, 1297 insertions, 1015 deletions

diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp
index ed8478ee8..52174dce0 100644
--- a/src/compat/cvc3_compat.cpp
+++ b/src/compat/cvc3_compat.cpp
@@ -1782,14 +1782,16 @@ Expr ValidityChecker::geExpr(const Expr& left, const Expr& right) {
 
 Expr ValidityChecker::recordExpr(const std::string& field, const Expr& expr) {
   CVC4::Type t = recordType(field, expr.getType());
-  return d_em->mkExpr(CVC4::kind::RECORD, d_em->mkConst(CVC4::RecordType(t).getRecord()), expr);
+  const CVC4::Datatype& dt = ((CVC4::DatatypeType)t).getDatatype();
+  return d_em->mkExpr(CVC4::kind::APPLY_CONSTRUCTOR, dt[0].getConstructor(), expr);
 }
 
 Expr ValidityChecker::recordExpr(const std::string& field0, const Expr& expr0,
                                  const std::string& field1, const Expr& expr1) {
   CVC4::Type t = recordType(field0, expr0.getType(),
                             field1, expr1.getType());
-  return d_em->mkExpr(CVC4::kind::RECORD, d_em->mkConst(CVC4::RecordType(t).getRecord()), expr0, expr1);
+  const CVC4::Datatype& dt = ((CVC4::DatatypeType)t).getDatatype();
+  return d_em->mkExpr(CVC4::kind::APPLY_CONSTRUCTOR, dt[0].getConstructor(), expr0, expr1);
 }
 
 Expr ValidityChecker::recordExpr(const std::string& field0, const Expr& expr0,
@@ -1798,7 +1800,8 @@ Expr ValidityChecker::recordExpr(const std::string& field0, const Expr& expr0,
   CVC4::Type t = recordType(field0, expr0.getType(),
                             field1, expr1.getType(),
                             field2, expr2.getType());
-  return d_em->mkExpr(CVC4::kind::RECORD, d_em->mkConst(CVC4::RecordType(t).getRecord()), expr0, expr1, expr2);
+  const CVC4::Datatype& dt = ((CVC4::DatatypeType)t).getDatatype();
+  return d_em->mkExpr(CVC4::kind::APPLY_CONSTRUCTOR, dt[0].getConstructor(), expr0, expr1, expr2);
 }
 
 Expr ValidityChecker::recordExpr(const std::vector<std::string>& fields,
@@ -1808,11 +1811,16 @@ Expr ValidityChecker::recordExpr(const std::vector<std::string>& fields,
     types.push_back(exprs[i].getType());
   }
   CVC4::Type t = recordType(fields, types);
-  return d_em->mkExpr(d_em->mkConst(CVC4::RecordType(t).getRecord()), *reinterpret_cast<const vector<CVC4::Expr>*>(&exprs));
+  const CVC4::Datatype& dt = ((CVC4::DatatypeType)t).getDatatype();
+  return d_em->mkExpr(CVC4::kind::APPLY_CONSTRUCTOR, dt[0].getConstructor(), *reinterpret_cast<const vector<CVC4::Expr>*>(&exprs));
 }
 
 Expr ValidityChecker::recSelectExpr(const Expr& record, const std::string& field) {
-  return d_em->mkExpr(d_em->mkConst(CVC4::RecordSelect(field)), record);
+  Type t = record.getType();
+  const CVC4::Datatype& dt = ((CVC4::DatatypeType)t).getDatatype();
+  const CVC4::Record& rec = ((CVC4::DatatypeType)t).getRecord();
+  unsigned index = rec.getIndex(field);
+  return d_em->mkExpr(CVC4::kind::APPLY_SELECTOR_TOTAL, dt[0][index].getSelector(), record);
 }
 
 Expr ValidityChecker::recUpdateExpr(const Expr& record, const std::string& field,
@@ -2200,15 +2208,23 @@ Rational ValidityChecker::computeBVConst(const Expr& e) {
 }
 
 Expr ValidityChecker::tupleExpr(const std::vector<Expr>& exprs) {
-  const vector<CVC4::Expr>& v =
-    *reinterpret_cast<const vector<CVC4::Expr>*>(&exprs);
-  return d_em->mkExpr(CVC4::kind::TUPLE, v);
+  std::vector< Type > types;
+  std::vector<CVC4::Expr> v;
+  for( unsigned i=0; i<exprs.size(); i++ ){
+    types.push_back( exprs[i].getType() );  
+    v.push_back( exprs[i] );
+  }
+  Type t = tupleType( types );
+  const CVC4::Datatype& dt = ((CVC4::DatatypeType)t).getDatatype();
+  v.insert( v.begin(), dt[0].getConstructor() );
+  return d_em->mkExpr(CVC4::kind::APPLY_CONSTRUCTOR, v);
 }
 
 Expr ValidityChecker::tupleSelectExpr(const Expr& tuple, int index) {
-  CompatCheckArgument(index >= 0 && index < tuple.getNumChildren(),
+  CompatCheckArgument(index >= 0 && index < ((CVC4::DatatypeType)tuple.getType()).getTupleLength(),
                       "invalid index in tuple select");
-  return d_em->mkExpr(d_em->mkConst(CVC4::TupleSelect(index)), tuple);
+  const CVC4::Datatype& dt = ((CVC4::DatatypeType)tuple.getType()).getDatatype();
+  return d_em->mkExpr(CVC4::kind::APPLY_SELECTOR_TOTAL, dt[0][index].getSelector(), tuple);
 }
 
 Expr ValidityChecker::tupleUpdateExpr(const Expr& tuple, int index,
diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp
index b9870afb4..32c0bb6dd 100644
--- a/src/expr/datatype.cpp
+++ b/src/expr/datatype.cpp
@@ -151,6 +151,13 @@ void Datatype::setSygus( Type st, Expr bvl, bool allow_const, bool allow_all ){
   d_sygus_allow_all = allow_all;
 }
 
+void Datatype::setTuple() {
+  d_isTuple = true;
+}
+
+void Datatype::setRecord() {
+  d_isRecord = true;
+}
 
 Cardinality Datatype::getCardinality() const throw(IllegalArgumentException) {
   PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
@@ -663,7 +670,6 @@ void DatatypeConstructor::setSygus( Expr op, Expr let_body, std::vector< Expr >&
   d_sygus_num_let_input_args = num_let_input_args;
 }
 
-
 void DatatypeConstructor::addArg(std::string selectorName, Type selectorType) {
   // We don't want to introduce a new data member, because eventually
   // we're going to be a constant stuffed inside a node.  So we stow
diff --git a/src/expr/datatype.h b/src/expr/datatype.h
index 5f80c54f7..625fbb5d4 100644
--- a/src/expr/datatype.h
+++ b/src/expr/datatype.h
@@ -237,9 +237,6 @@ public:
    */
   DatatypeConstructor(std::string name, std::string tester);
 
-  /** set sygus */
-  void setSygus( Expr op, Expr let_body, std::vector< Expr >& let_args, unsigned num_let_input_argus );
-
   /**
    * Add an argument (i.e., a data field) of the given name and type
    * to this Datatype constructor.  Selector names need not be unique;
@@ -382,6 +379,8 @@ public:
   bool involvesExternalType() const;
   bool involvesUninterpretedType() const;
 
+  /** set sygus */
+  void setSygus( Expr op, Expr let_body, std::vector< Expr >& let_args, unsigned num_let_input_argus );
 };/* class DatatypeConstructor */
 
 /**
@@ -473,6 +472,8 @@ private:
   std::string d_name;
   std::vector<Type> d_params;
   bool d_isCo;
+  bool d_isTuple;
+  bool d_isRecord;
   std::vector<DatatypeConstructor> d_constructors;
   bool d_resolved;
   Type d_self;
@@ -565,6 +566,12 @@ public:
    */
   void setSygus( Type st, Expr bvl, bool allow_const, bool allow_all );
 
+  /** set tuple */
+  void setTuple();
+
+  /** set tuple */
+  void setRecord();
+
   /** Get the name of this Datatype. */
   inline std::string getName() const throw();
 
@@ -589,6 +596,12 @@ public:
   /** is this a sygus datatype? */
   inline bool isSygus() const;
 
+  /** is this a tuple datatype? */
+  inline bool isTuple() const;
+
+  /** is this a record datatype? */
+  inline bool isRecord() const;
+
   /**
    * Return the cardinality of this datatype (the sum of the
    * cardinalities of its constructors).  The Datatype must be
@@ -757,6 +770,8 @@ inline Datatype::Datatype(std::string name, bool isCo) :
   d_name(name),
   d_params(),
   d_isCo(isCo),
+  d_isTuple(false),
+  d_isRecord(false),
   d_constructors(),
   d_resolved(false),
   d_self(),
@@ -771,6 +786,8 @@ inline Datatype::Datatype(std::string name, const std::vector<Type>& params, boo
   d_name(name),
   d_params(params),
   d_isCo(isCo),
+  d_isTuple(false),
+  d_isRecord(false),
   d_constructors(),
   d_resolved(false),
   d_self(),
@@ -819,6 +836,14 @@ inline bool Datatype::isSygus() const {
   return !d_sygus_type.isNull();
 }
 
+inline bool Datatype::isTuple() const {
+  return d_isTuple;
+}
+
+inline bool Datatype::isRecord() const {
+  return d_isRecord;
+}
+
 inline bool Datatype::operator!=(const Datatype& other) const throw() {
   return !(*this == other);
 }
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 0b9557cc8..ce7a92b48 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -20,6 +20,7 @@
 
 #include "expr/node_manager.h"
 #include "expr/variable_type_map.h"
+#include "expr/node_manager_attributes.h"
 #include "options/options.h"
 #include "util/statistics_registry.h"
 
@@ -596,18 +597,18 @@ FunctionType ExprManager::mkPredicateType(const std::vector<Type>& sorts) {
   return FunctionType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkPredicateType(sortNodes))));
 }
 
-TupleType ExprManager::mkTupleType(const std::vector<Type>& types) {
+DatatypeType ExprManager::mkTupleType(const std::vector<Type>& types) {
   NodeManagerScope nms(d_nodeManager);
   std::vector<TypeNode> typeNodes;
   for (unsigned i = 0, i_end = types.size(); i < i_end; ++ i) {
      typeNodes.push_back(*types[i].d_typeNode);
   }
-  return TupleType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkTupleType(typeNodes))));
+  return DatatypeType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkTupleType(typeNodes))));
 }
 
-RecordType ExprManager::mkRecordType(const Record& rec) {
+DatatypeType ExprManager::mkRecordType(const Record& rec) {
   NodeManagerScope nms(d_nodeManager);
-  return RecordType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkRecordType(rec))));
+  return DatatypeType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkRecordType(rec))));
 }
 
 SExprType ExprManager::mkSExprType(const std::vector<Type>& types) {
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index e65cfc358..37ef128f4 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -341,12 +341,12 @@ public:
    * <code>types[0..types.size()-1]</code>.  <code>types</code> must
    * have at least one element.
    */
-  TupleType mkTupleType(const std::vector<Type>& types);
+  DatatypeType mkTupleType(const std::vector<Type>& types);
 
   /**
    * Make a record type with types from the rec parameter.
    */
-  RecordType mkRecordType(const Record& rec);
+  DatatypeType mkRecordType(const Record& rec);
 
   /**
    * Make a symbolic expressiontype with types from
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index e52776fce..e6e44928d 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -461,79 +461,66 @@ TypeNode NodeManager::mkSubrangeType(const SubrangeBounds& bounds)
   return TypeNode(mkTypeConst(bounds));
 }
 
-TypeNode NodeManager::getDatatypeForTupleRecord(TypeNode t) {
-  Assert(t.isTuple() || t.isRecord());
-
-  //AJR: not sure why .getBaseType() was used in two cases below,
-  //     disabling this, which is necessary to fix bug 605/667,
-  //     which involves records of INT which were mapped to records of REAL below.
-  TypeNode tOrig = t;
-  if(t.isTuple()) {
-    vector<TypeNode> v;
-    bool changed = false;
-    for(size_t i = 0; i < t.getNumChildren(); ++i) {
-      TypeNode tn = t[i];
-      TypeNode base;
-      if(tn.isTuple() || tn.isRecord()) {
-        base = getDatatypeForTupleRecord(tn);
-      } else {
-        base = tn;//.getBaseType();
-      }
-      changed = changed || (tn != base);
-      v.push_back(base);
-    }
-    if(changed) {
-      t = mkTupleType(v);
-    }
-  } else {
-    const Record& r = t.getRecord();
-    std::vector< std::pair<std::string, Type> > v;
-    bool changed = false;
-    const Record::FieldVector& fields = r.getFields();
-    for(Record::FieldVector::const_iterator i = fields.begin(); i != fields.end(); ++i) {
-      Type tn = (*i).second;
-      Type base;
-      if(tn.isTuple() || tn.isRecord()) {
-        base = getDatatypeForTupleRecord(TypeNode::fromType(tn)).toType();
-      } else {
-        base = tn;//.getBaseType();
-      }
-      changed = changed || (tn != base);
-      v.push_back(std::make_pair((*i).first, base));
-    }
-    if(changed) {
-      t = mkRecordType(Record(v));
+TypeNode NodeManager::mkTupleType(const std::vector<TypeNode>& types) {
+  std::vector< TypeNode > ts;
+  Debug("tuprec-debug") << "Make tuple type : ";
+  for (unsigned i = 0; i < types.size(); ++ i) {
+    CheckArgument(!types[i].isFunctionLike(), types, "cannot put function-like types in tuples");
+    ts.push_back( types[i] );
+    Debug("tuprec-debug") << types[i] << " ";
+  }
+  Debug("tuprec-debug") << std::endl;
+  //index based on function type
+  TypeNode tindex;
+  if( types.empty() ){
+    //do nothing (will index on null type)
+  }else if( types.size()==1 ){
+    tindex = types[0];
+  }else{
+    TypeNode tt = ts.back();
+    ts.pop_back();
+    tindex = mkFunctionType( ts, tt );
+    ts.push_back( tt );
+  }
+  TypeNode& dtt = d_tupleAndRecordTypes[tindex];
+  if(dtt.isNull()) {
+    Datatype dt("__cvc4_tuple");
+    dt.setTuple();
+    DatatypeConstructor c("__cvc4_tuple_ctor");
+    for (unsigned i = 0; i < ts.size(); ++ i) {
+      std::stringstream ss;
+      ss << "__cvc4_tuple_stor_" << i;
+      c.addArg(ss.str().c_str(), ts[i].toType());
     }
+    dt.addConstructor(c);
+    dtt = TypeNode::fromType(toExprManager()->mkDatatypeType(dt));
+    dtt.setAttribute(DatatypeTupleAttr(), tindex);
+    Debug("tuprec-debug") << "Return type : " << dtt << std::endl;
+  }else{
+    Debug("tuprec-debug") << "Return cached type : " << dtt << std::endl;
   }
+  Assert(!dtt.isNull());
+  return dtt;
+}
 
-  // if the type doesn't have an associated datatype, then make one for it
-  TypeNode& dtt = d_tupleAndRecordTypes[t];
+TypeNode NodeManager::mkRecordType(const Record& rec) {
+  //index based on type constant
+  TypeNode tindex = mkTypeConst(rec);
+  TypeNode& dtt = d_tupleAndRecordTypes[tindex];
   if(dtt.isNull()) {
-    if(t.isTuple()) {
-      Datatype dt("__cvc4_tuple");
-      DatatypeConstructor c("__cvc4_tuple_ctor");
-      for(TypeNode::const_iterator i = t.begin(); i != t.end(); ++i) {
-        c.addArg("__cvc4_tuple_stor", (*i).toType());
-      }
-      dt.addConstructor(c);
-      dtt = TypeNode::fromType(toExprManager()->mkDatatypeType(dt));
-      Debug("tuprec") << "REWROTE " << t << " to " << dtt << std::endl;
-      dtt.setAttribute(DatatypeTupleAttr(), tOrig);
-    } else {
-      const Record& rec = t.getRecord();
-      const Record::FieldVector& fields = rec.getFields();
-      Datatype dt("__cvc4_record");
-      DatatypeConstructor c("__cvc4_record_ctor");
-      for(Record::FieldVector::const_iterator i = fields.begin(); i != fields.end(); ++i) {
-        c.addArg((*i).first, (*i).second);
-      }
-      dt.addConstructor(c);
-      dtt = TypeNode::fromType(toExprManager()->mkDatatypeType(dt));
-      Debug("tuprec") << "REWROTE " << t << " to " << dtt << std::endl;
-      dtt.setAttribute(DatatypeRecordAttr(), tOrig);
+    const Record::FieldVector& fields = rec.getFields();
+    Datatype dt("__cvc4_record");
+    dt.setRecord();
+    DatatypeConstructor c("__cvc4_record_ctor");
+    for(Record::FieldVector::const_iterator i = fields.begin(); i != fields.end(); ++i) {
+      c.addArg((*i).first, (*i).second);
     }
-  } else {
-    Debug("tuprec") << "REUSING cached " << t << ": " << dtt << std::endl;
+    dt.addConstructor(c);
+    dtt = TypeNode::fromType(toExprManager()->mkDatatypeType(dt));
+    dtt.setAttribute(DatatypeRecordAttr(), tindex);
+    Debug("tuprec-debug") << "Return type : " << dtt << std::endl;
+  }else{
+    Debug("tuprec-debug") << "Return cached type : " << dtt << std::endl;
   }
   Assert(!dtt.isNull());
   return dtt;
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 1ae9f1e8e..45c9afbde 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -756,7 +756,7 @@ public:
    * @param types a vector of types
    * @returns the tuple type (types[0], ..., types[n])
    */
-  inline TypeNode mkTupleType(const std::vector<TypeNode>& types);
+  TypeNode mkTupleType(const std::vector<TypeNode>& types);
 
   /**
    * Make a record type with the description from rec.
@@ -764,7 +764,7 @@ public:
    * @param rec a description of the record
    * @returns the record type
    */
-  inline TypeNode mkRecordType(const Record& rec);
+  TypeNode mkRecordType(const Record& rec);
 
   /**
    * Make a symbolic expression type with types from
@@ -839,12 +839,6 @@ public:
     throw(TypeCheckingExceptionPrivate);
 
   /**
-   * Given a tuple or record type, get the internal datatype used for
-   * it.  Makes the DatatypeType if necessary.
-   */
-  TypeNode getDatatypeForTupleRecord(TypeNode tupleRecordType);
-
-  /**
    * Get the type for the given node and optionally do type checking.
    *
    * Initial type computation will be near-constant time if
@@ -1063,20 +1057,6 @@ NodeManager::mkPredicateType(const std::vector<TypeNode>& sorts) {
   return mkTypeNode(kind::FUNCTION_TYPE, sortNodes);
 }
 
-inline TypeNode NodeManager::mkTupleType(const std::vector<TypeNode>& types) {
-  std::vector<TypeNode> typeNodes;
-  for (unsigned i = 0; i < types.size(); ++ i) {
-    CheckArgument(!types[i].isFunctionLike(), types,
-                  "cannot put function-like types in tuples");
-    typeNodes.push_back(types[i]);
-  }
-  return mkTypeNode(kind::TUPLE_TYPE, typeNodes);
-}
-
-inline TypeNode NodeManager::mkRecordType(const Record& rec) {
-  return mkTypeConst(rec);
-}
-
 inline TypeNode NodeManager::mkSExprType(const std::vector<TypeNode>& types) {
   std::vector<TypeNode> typeNodes;
   for (unsigned i = 0; i < types.size(); ++ i) {
diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index 99d04d658..6b5bdf07c 100644
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -358,27 +358,6 @@ Type FunctionType::getRangeType() const {
   return makeType(d_typeNode->getRangeType());
 }
 
-size_t TupleType::getLength() const {
-  return d_typeNode->getTupleLength();
-}
-
-vector<Type> TupleType::getTypes() const {
-  NodeManagerScope nms(d_nodeManager);
-  vector<Type> types;
-  vector<TypeNode> typeNodes = d_typeNode->getTupleTypes();
-  vector<TypeNode>::iterator it = typeNodes.begin();
-  vector<TypeNode>::iterator it_end = typeNodes.end();
-  for(; it != it_end; ++ it) {
-    types.push_back(makeType(*it));
-  }
-  return types;
-}
-
-const Record& RecordType::getRecord() const {
-  NodeManagerScope nms(d_nodeManager);
-  return d_typeNode->getRecord();
-}
-
 vector<Type> SExprType::getTypes() const {
   NodeManagerScope nms(d_nodeManager);
   vector<Type> types;
@@ -488,16 +467,6 @@ FunctionType::FunctionType(const Type& t) throw(IllegalArgumentException)
   PrettyCheckArgument(isNull() || isFunction(), this);
 }
 
-TupleType::TupleType(const Type& t) throw(IllegalArgumentException)
-    : Type(t) {
-  PrettyCheckArgument(isNull() || isTuple(), this);
-}
-
-RecordType::RecordType(const Type& t) throw(IllegalArgumentException)
-    : Type(t) {
-  PrettyCheckArgument(isNull() || isRecord(), this);
-}
-
 SExprType::SExprType(const Type& t) throw(IllegalArgumentException)
     : Type(t) {
   PrettyCheckArgument(isNull() || isSExpr(), this);
@@ -640,6 +609,29 @@ DatatypeType DatatypeType::instantiate(const std::vector<Type>& params) const {
   return DatatypeType(makeType(d_nodeManager->mkTypeNode(kind::PARAMETRIC_DATATYPE, paramsNodes)));
 }
 
+/** Get the length of a tuple type */
+size_t DatatypeType::getTupleLength() const {
+  NodeManagerScope nms(d_nodeManager);
+  return d_typeNode->getTupleLength();
+}
+
+/** Get the constituent types of a tuple type */
+std::vector<Type> DatatypeType::getTupleTypes() const {
+  NodeManagerScope nms(d_nodeManager);
+  std::vector< TypeNode > vec = d_typeNode->getTupleTypes();
+  std::vector< Type > vect;
+  for( unsigned i=0; i<vec.size(); i++ ){
+    vect.push_back( vec[i].toType() );
+  }
+  return vect;
+}
+
+/** Get the description of the record type */
+const Record& DatatypeType::getRecord() const {
+  NodeManagerScope nms(d_nodeManager);
+  return d_typeNode->getRecord();
+}
+
 DatatypeType SelectorType::getDomain() const {
   return DatatypeType(makeType((*d_typeNode)[0]));
 }
diff --git a/src/expr/type.h b/src/expr/type.h
index 0f2118c44..67d259fec 100644
--- a/src/expr/type.h
+++ b/src/expr/type.h
@@ -56,8 +56,6 @@ class ConstructorType;
 class SelectorType;
 class TesterType;
 class FunctionType;
-class TupleType;
-class RecordType;
 class SExprType;
 class SortType;
 class SortConstructorType;
@@ -459,39 +457,7 @@ public:
 };/* class FunctionType */
 
 /**
- * Class encapsulating a tuple type.
- */
-class CVC4_PUBLIC TupleType : public Type {
-
-public:
-
-  /** Construct from the base type */
-  TupleType(const Type& type = Type()) throw(IllegalArgumentException);
-
-  /** Get the length of the tuple.  The same as getTypes().size(). */
-  size_t getLength() const;
-
-  /** Get the constituent types */
-  std::vector<Type> getTypes() const;
-
-};/* class TupleType */
-
-/**
- * Class encapsulating a record type.
- */
-class CVC4_PUBLIC RecordType : public Type {
-
-public:
-
-  /** Construct from the base type */
-  RecordType(const Type& type = Type()) throw(IllegalArgumentException);
-
-  /** Get the constituent types */
-  const Record& getRecord() const;
-};/* class RecordType */
-
-/**
- * Class encapsulating a tuple type.
+ * Class encapsulating a sexpr type.
  */
 class CVC4_PUBLIC SExprType : public Type {
 
@@ -704,6 +670,15 @@ public:
   /** Instantiate a datatype using this datatype constructor */
   DatatypeType instantiate(const std::vector<Type>& params) const;
 
+  /** Get the length of a tuple type */
+  size_t getTupleLength() const;
+
+  /** Get the constituent types of a tuple type */
+  std::vector<Type> getTupleTypes() const;
+
+  /** Get the description of the record type */
+  const Record& getRecord() const;
+
 };/* class DatatypeType */
 
 /**
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index ea185f98b..755b16e46 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -94,9 +94,6 @@ bool TypeNode::isSubtypeOf(TypeNode t) const {
     }
   }
   if(isTuple() || isRecord()) {
-    if(t == NodeManager::currentNM()->getDatatypeForTupleRecord(*this)) {
-      return true;
-    }
     if(isTuple() != t.isTuple() || isRecord() != t.isRecord()) {
       return false;
     }
@@ -111,8 +108,8 @@ bool TypeNode::isSubtypeOf(TypeNode t) const {
         }
       }
     } else {
-      const Record& r1 = getConst<Record>();
-      const Record& r2 = t.getConst<Record>();
+      const Record& r1 = getRecord();
+      const Record& r2 = t.getRecord();
       if(r1.getNumFields() != r2.getNumFields()) {
         return false;
       }
@@ -166,12 +163,8 @@ bool TypeNode::isComparableTo(TypeNode t) const {
   if(isSubtypeOf(NodeManager::currentNM()->realType())) {
     return t.isSubtypeOf(NodeManager::currentNM()->realType());
   }
-  if(t.isDatatype() && (isTuple() || isRecord())) {
+  if(isTuple() || isRecord()) {
     if(t.isTuple() || t.isRecord()) {
-      if(NodeManager::currentNM()->getDatatypeForTupleRecord(t) ==
-         NodeManager::currentNM()->getDatatypeForTupleRecord(*this)) {
-        return true;
-      }
       if(isTuple() != t.isTuple() || isRecord() != t.isRecord()) {
         return false;
       }
@@ -186,8 +179,8 @@ bool TypeNode::isComparableTo(TypeNode t) const {
           }
         }
       } else {
-        const Record& r1 = getConst<Record>();
-        const Record& r2 = t.getConst<Record>();
+        const Record& r1 = getRecord();
+        const Record& r2 = t.getRecord();
         if(r1.getNumFields() != r2.getNumFields()) {
           return false;
         }
@@ -202,12 +195,7 @@ bool TypeNode::isComparableTo(TypeNode t) const {
         }
       }
       return true;
-    } else {
-      return t == NodeManager::currentNM()->getDatatypeForTupleRecord(*this);
     }
-  } else if(isDatatype() && (t.isTuple() || t.isRecord())) {
-    Assert(!isTuple() && !isRecord());// should have been handled above
-    return *this == NodeManager::currentNM()->getDatatypeForTupleRecord(t);
   } else if(isParametricDatatype() && t.isParametricDatatype()) {
     Assert(getKind() == kind::PARAMETRIC_DATATYPE);
     Assert(t.getKind() == kind::PARAMETRIC_DATATYPE);
@@ -244,8 +232,6 @@ TypeNode TypeNode::getBaseType() const {
   TypeNode realt = NodeManager::currentNM()->realType();
   if (isSubtypeOf(realt)) {
     return realt;
-  } else if (isTuple() || isRecord()) {
-    return NodeManager::currentNM()->getDatatypeForTupleRecord(*this);
   } else if (isPredicateSubtype()) {
     return getSubtypeParentType().getBaseType();
   } else if (isParametricDatatype()) {
@@ -282,23 +268,40 @@ std::vector<TypeNode> TypeNode::getParamTypes() const {
   return params;
 }
 
+
+/** Is this a tuple type? */
+bool TypeNode::isTuple() const {
+  return ( getKind() == kind::DATATYPE_TYPE && hasAttribute(expr::DatatypeTupleAttr()) ) ||
+    ( isPredicateSubtype() && getSubtypeParentType().isTuple() );
+}
+
+/** Is this a record type? */
+bool TypeNode::isRecord() const {
+  return ( getKind() == kind::DATATYPE_TYPE && hasAttribute(expr::DatatypeRecordAttr()) )  ||
+    ( isPredicateSubtype() && getSubtypeParentType().isRecord() );
+}
+
 size_t TypeNode::getTupleLength() const {
   Assert(isTuple());
-  return getNumChildren();
+  const Datatype& dt = getConst<Datatype>();
+  Assert(dt.getNumConstructors()==1);
+  return dt[0].getNumArgs();
 }
 
 vector<TypeNode> TypeNode::getTupleTypes() const {
   Assert(isTuple());
+  const Datatype& dt = getConst<Datatype>();
+  Assert(dt.getNumConstructors()==1);
   vector<TypeNode> types;
-  for(unsigned i = 0, i_end = getNumChildren(); i < i_end; ++i) {
-    types.push_back((*this)[i]);
+  for(unsigned i = 0; i < dt[0].getNumArgs(); ++i) {
+    types.push_back(TypeNode::fromType(((SelectorType)dt[0][i].getSelector().getType()).getRangeType()));
   }
   return types;
 }
 
 const Record& TypeNode::getRecord() const {
   Assert(isRecord());
-  return getConst<Record>();
+  return getAttribute(expr::DatatypeRecordAttr()).getConst<Record>();
 }
 
 vector<TypeNode> TypeNode::getSExprTypes() const {
@@ -446,6 +449,7 @@ TypeNode TypeNode::leastCommonTypeNode(TypeNode t0, TypeNode t1){
       Assert(t1.isInteger());
       return TypeNode();
     }
+/*
   case kind::TUPLE_TYPE: {
     // if the other == this one, we returned already, above
     if(t0.getBaseType() == t1) {
@@ -495,6 +499,7 @@ TypeNode TypeNode::leastCommonTypeNode(TypeNode t0, TypeNode t1){
     // if we make it here, we constructed the least common type
     return NodeManager::currentNM()->mkRecordType(Record(fields));
   }
+*/
   case kind::DATATYPE_TYPE:
     // t1 might be a subtype tuple or record
     if(t1.getBaseType() == t0) {
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index 59f602f09..4c48cc3ca 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -929,18 +929,6 @@ inline TypeNode TypeNode::getRangeType() const {
   return (*this)[getNumChildren() - 1];
 }
 
-/** Is this a tuple type? */
-inline bool TypeNode::isTuple() const {
-  return getKind() == kind::TUPLE_TYPE ||
-    ( isPredicateSubtype() && getSubtypeParentType().isTuple() );
-}
-
-/** Is this a record type? */
-inline bool TypeNode::isRecord() const {
-  return getKind() == kind::RECORD_TYPE ||
-    ( isPredicateSubtype() && getSubtypeParentType().isRecord() );
-}
-
 /** Is this a symbolic expression type? */
 inline bool TypeNode::isSExpr() const {
   return getKind() == kind::SEXPR_TYPE ||
@@ -973,7 +961,6 @@ inline bool TypeNode::isBitVector() const {
 /** Is this a datatype type */
 inline bool TypeNode::isDatatype() const {
   return getKind() == kind::DATATYPE_TYPE ||
-    getKind() == kind::TUPLE_TYPE || getKind() == kind::RECORD_TYPE ||
     ( isPredicateSubtype() && getSubtypeParentType().isDatatype() );
 }
 
@@ -1027,11 +1014,7 @@ inline bool TypeNode::isBitVector(unsigned size) const {
 /** Get the datatype specification from a datatype type */
 inline const Datatype& TypeNode::getDatatype() const {
   Assert(isDatatype());
-  if(getKind() == kind::DATATYPE_TYPE) {
-    return getConst<Datatype>();
-  } else {
-    return NodeManager::currentNM()->getDatatypeForTupleRecord(*this).getConst<Datatype>();
-  }
+  return getConst<Datatype>();
 }
 
 /** Get the exponent size of this floating-point type */
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index f3a2bbe02..3991da886 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -1116,7 +1116,7 @@ type[CVC4::Type& t,
   : restrictedTypePossiblyFunctionLHS[t,check,lhs]
     { if(lhs) {
         assert(t.isTuple());
-        args = TupleType(t).getTypes();
+        args = ((DatatypeType)t).getTupleTypes();
       } else {
         args.push_back(t);
       }
@@ -1554,13 +1554,17 @@ tupleStore[CVC4::Expr& f]
       if(! t.isTuple()) {
         PARSER_STATE->parseError("tuple-update applied to non-tuple");
       }
-      size_t length = TupleType(t).getLength();
+      size_t length = ((DatatypeType)t).getTupleLength();
       if(k >= length) {
         std::stringstream ss;
         ss << "tuple is of length " << length << "; cannot update index " << k;
         PARSER_STATE->parseError(ss.str());
       }
-      f2 = MK_EXPR(MK_CONST(TupleSelect(k)), f);
+      std::vector<Expr> args;
+      const Datatype & dt = ((DatatypeType)t).getDatatype();
+      args.push_back( dt[0][k].getSelector() );
+      args.push_back( f );
+      f2 = MK_EXPR(CVC4::kind::APPLY_SELECTOR_TOTAL,args);
     }
     ( ( arrayStore[f2]
       | DOT ( tupleStore[f2]
@@ -1587,11 +1591,15 @@ recordStore[CVC4::Expr& f]
            << "its type: " << t;
         PARSER_STATE->parseError(ss.str());
       }
-      const Record& rec = RecordType(t).getRecord();
+      const Record& rec = ((DatatypeType)t).getRecord();
       if(! rec.contains(id)) {
         PARSER_STATE->parseError(std::string("no such field `") + id + "' in record");
       }
-      f2 = MK_EXPR(MK_CONST(RecordSelect(id)), f);
+      std::vector<Expr> args;
+      const Datatype & dt = ((DatatypeType)t).getDatatype();
+      args.push_back( dt[0][id].getSelector() );
+      args.push_back( f );
+      f2 = MK_EXPR(CVC4::kind::APPLY_SELECTOR_TOTAL,args);
     }
     ( ( arrayStore[f2]
       | DOT ( tupleStore[f2]
@@ -1718,24 +1726,32 @@ postfixTerm[CVC4::Expr& f]
           if(! t.isRecord()) {
             PARSER_STATE->parseError("record-select applied to non-record");
           }
-          const Record& rec = RecordType(t).getRecord();
+          const Record& rec = ((DatatypeType)t).getRecord();
           if(!rec.contains(id)){
             PARSER_STATE->parseError(std::string("no such field `") + id + "' in record");
           }
-          f = MK_EXPR(MK_CONST(RecordSelect(id)), f);
+          const Datatype & dt = ((DatatypeType)t).getDatatype();
+          std::vector<Expr> sargs;
+          sargs.push_back( dt[0][id].getSelector() );
+          sargs.push_back( f );
+          f = MK_EXPR(CVC4::kind::APPLY_SELECTOR_TOTAL,sargs);
         }
       | k=numeral
         { Type t = f.getType();
           if(! t.isTuple()) {
             PARSER_STATE->parseError("tuple-select applied to non-tuple");
           }
-          size_t length = TupleType(t).getLength();
+          size_t length = ((DatatypeType)t).getTupleLength();
           if(k >= length) {
             std::stringstream ss;
             ss << "tuple is of length " << length << "; cannot access index " << k;
             PARSER_STATE->parseError(ss.str());
           }
-          f = MK_EXPR(MK_CONST(TupleSelect(k)), f);
+          const Datatype & dt = ((DatatypeType)t).getDatatype();
+          std::vector<Expr> sargs;
+          sargs.push_back( dt[0][k].getSelector() );
+          sargs.push_back( f );
+          f = MK_EXPR(CVC4::kind::APPLY_SELECTOR_TOTAL,sargs);
         }
       )
     )*
@@ -1956,20 +1972,25 @@ simpleTerm[CVC4::Expr& f]
         for(std::vector<Expr>::const_iterator i = args.begin(); i != args.end(); ++i) {
           types.push_back((*i).getType());
         }
-        TupleType t = EXPR_MANAGER->mkTupleType(types);
-        f = MK_EXPR(kind::TUPLE, args);
+        DatatypeType t = EXPR_MANAGER->mkTupleType(types);
+        const Datatype& dt = t.getDatatype();
+        args.insert( args.begin(), dt[0].getConstructor() );
+        f = MK_EXPR(kind::APPLY_CONSTRUCTOR, args);
       }
     }
 
     /* empty tuple literal */
   | LPAREN RPAREN
-    { f = MK_EXPR(kind::TUPLE, std::vector<Expr>()); }
+    { std::vector<Type> types;
+      DatatypeType t = EXPR_MANAGER->mkTupleType(types);
+      const Datatype& dt = t.getDatatype();
+      f = MK_EXPR(kind::APPLY_CONSTRUCTOR, dt[0].getConstructor()); }
     /* empty record literal */
   | PARENHASH HASHPAREN
-    { RecordType t = EXPR_MANAGER->mkRecordType(std::vector< std::pair<std::string, Type> >());
-      f = MK_EXPR(kind::RECORD, MK_CONST(t.getRecord()), std::vector<Expr>());
+    { DatatypeType t = EXPR_MANAGER->mkRecordType(std::vector< std::pair<std::string, Type> >());
+      const Datatype& dt = t.getDatatype();
+      f = MK_EXPR(kind::APPLY_CONSTRUCTOR, dt[0].getConstructor());
     }
-
     /* empty set literal */
   | LBRACE RBRACE
     { f = MK_CONST(EmptySet(Type())); }
@@ -2035,8 +2056,10 @@ simpleTerm[CVC4::Expr& f]
       for(unsigned i = 0; i < names.size(); ++i) {
         typeIds.push_back(std::make_pair(names[i], args[i].getType()));
       }
-      RecordType t = EXPR_MANAGER->mkRecordType(typeIds);
-      f = MK_EXPR(kind::RECORD, MK_CONST(t.getRecord()), args);
+      DatatypeType t = EXPR_MANAGER->mkRecordType(typeIds);
+      const Datatype& dt = t.getDatatype();
+      args.insert( args.begin(), dt[0].getConstructor() );
+      f = MK_EXPR(kind::APPLY_CONSTRUCTOR, args);
     }
 
     /* variable / zero-ary constructor application */
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index db4949c1f..58835d4e6 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -162,8 +162,32 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
       }
       break;
 
-    case kind::DATATYPE_TYPE:
-      out << n.getConst<Datatype>().getName();
+    case kind::DATATYPE_TYPE: {
+      const Datatype& dt = n.getConst<Datatype>();
+      if( dt.isTuple() ){
+        out << '[';
+        for (unsigned i = 0; i < dt[0].getNumArgs(); ++ i) {
+          if (i > 0) {
+            out << ", ";
+          }
+          Type t = ((SelectorType)dt[0][i].getSelector().getType()).getRangeType();
+          out << t;
+        }
+        out << ']';
+      }else if( dt.isRecord() ){
+        out << "[# ";
+        for (unsigned i = 0; i < dt[0].getNumArgs(); ++ i) {
+          if (i > 0) {
+            out << ", ";
+          }
+          Type t = ((SelectorType)dt[0][i].getSelector().getType()).getRangeType();
+          out << dt[0][i].getSelector() << ":" << t;
+        }
+        out << " #]";
+      }else{
+        out << dt.getName();
+      }
+    }
       break;
 
     case kind::EMPTYSET:
@@ -214,7 +238,6 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
       out << " ENDIF";
       return;
       break;
-    case kind::TUPLE_TYPE:
     case kind::SEXPR_TYPE:
       out << '[';
       for (unsigned i = 0; i < n.getNumChildren(); ++ i) {
@@ -329,9 +352,48 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
       }
       return;
       break;
-    case kind::APPLY_CONSTRUCTOR:
+    case kind::APPLY_CONSTRUCTOR: {
+        TypeNode t = n.getType();
+        if( t.isTuple() ){
+          //no-op
+        }else if( t.isRecord() ){
+          const Record& rec = t.getRecord();
+          out << "(# ";
+          TNode::iterator i = n.begin();
+          bool first = true;
+          const Record::FieldVector& fields = rec.getFields();
+          for(Record::FieldVector::const_iterator j = fields.begin(); j != fields.end(); ++i, ++j) {
+            if(!first) {
+              out << ", ";
+            }
+            out << (*j).first << " := ";
+            toStream(out, *i, depth, types, false);
+            first = false;
+          }
+          out << " #)";
+          return;
+        }else{
+          toStream(op, n.getOperator(), depth, types, false);
+        }
+      }
+      break;
     case kind::APPLY_SELECTOR:
-    case kind::APPLY_SELECTOR_TOTAL:
+    case kind::APPLY_SELECTOR_TOTAL: {
+        TypeNode t = n.getType();
+        if( t.isTuple() ){
+          toStream(out, n[0], depth, types, true);
+          out << '.' << Datatype::indexOf( n.getOperator().toExpr() );
+        }else if( t.isRecord() ){
+          toStream(out, n[0], depth, types, true);
+          const Record& rec = t.getRecord();
+          unsigned index = Datatype::indexOf( n.getOperator().toExpr() );
+          std::pair<std::string, Type> fld = rec[index];
+          out << '.' << fld.first;
+        }else{
+          toStream(op, n.getOperator(), depth, types, false);
+        }
+      }
+      break;
     case kind::APPLY_TESTER:
       toStream(op, n.getOperator(), depth, types, false);
       break;
@@ -359,16 +421,6 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
       out << " -> BOOLEAN";
       return;
       break;
-    case kind::TUPLE_SELECT:
-      toStream(out, n[0], depth, types, true);
-      out << '.' << n.getOperator().getConst<TupleSelect>().getIndex();
-      return;
-      break;
-    case kind::RECORD_SELECT:
-      toStream(out, n[0], depth, types, true);
-      out << '.' << n.getOperator().getConst<RecordSelect>().getField();
-      return;
-      break;
     case kind::TUPLE_UPDATE:
       toStream(out, n[0], depth, types, true);
       out << " WITH ." << n.getOperator().getConst<TupleUpdate>().getIndex() << " := ";
@@ -381,28 +433,6 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
       toStream(out, n[1], depth, types, true);
       return;
       break;
-    case kind::TUPLE:
-      // no-op
-      break;
-    case kind::RECORD: {
-      // (# _a := 2, _b := 2 #)
-      const Record& rec = n.getOperator().getConst<Record>();
-      out << "(# ";
-      TNode::iterator i = n.begin();
-      bool first = true;
-      const Record::FieldVector& fields = rec.getFields();
-      for(Record::FieldVector::const_iterator j = fields.begin(); j != fields.end(); ++i, ++j) {
-        if(!first) {
-          out << ", ";
-        }
-        out << (*j).first << " := ";
-        toStream(out, *i, depth, types, false);
-        first = false;
-      }
-      out << " #)";
-      return;
-      break;
-    }
 
     // ARRAYS
     case kind::ARRAY_TYPE:
@@ -1122,8 +1152,9 @@ static void toStream(std::ostream& out, const DefineFunctionCommand* c, bool cvc
 
 static void toStream(std::ostream& out, const DeclareTypeCommand* c, bool cvc3Mode) throw() {
   if(c->getArity() > 0) {
+    //TODO?
     out << "ERROR: Don't know how to print parameterized type declaration "
-           "in CVC language:" << endl << c->toString() << endl;
+           "in CVC language." << endl;
   } else {
     out << c->getSymbol() << " : TYPE;";
   }
@@ -1245,7 +1276,13 @@ static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c, boo
           }
           firstSelector = false;
           const DatatypeConstructorArg& selector = *k;
-          out << selector.getName() << ": " << SelectorType(selector.getType()).getRangeType();
+          Type t = SelectorType(selector.getType()).getRangeType();
+          if( t.isDatatype() ){
+            const Datatype & sdt = ((DatatypeType)t).getDatatype();
+            out << selector.getName() << ": " << sdt.getName();
+          }else{
+            out << selector.getName() << ": " << t;
+          }
         }
         out << ')';
       }
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 7afbf4e40..d37f4ae99 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -333,7 +333,6 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
   case kind::EQUAL:
   case kind::DISTINCT: out << smtKindString(k) << " "; break;
   case kind::CHAIN: break;
-  case kind::TUPLE: break;
   case kind::FUNCTION_TYPE:
     for(size_t i = 0; i < n.getNumChildren() - 1; ++i) {
       if(i > 0) {
@@ -698,7 +697,6 @@ static string smtKindString(Kind k) throw() {
   case kind::EQUAL: return "=";
   case kind::DISTINCT: return "distinct";
   case kind::CHAIN: break;
-  case kind::TUPLE: break;
   case kind::SEXPR: break;
 
     // bool theory
diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp
index 4372c0c18..07d78a6fd 100644
--- a/src/smt/boolean_terms.cpp
+++ b/src/smt/boolean_terms.cpp
@@ -139,14 +139,15 @@ Node BooleanTermConverter::rewriteAs(TNode in, TypeNode as, std::map< TypeNode,
     processing[in_t] = true;
     if(in.getType().isRecord()) {
       Assert(as.isRecord());
-      const Record& inRec = in.getType().getConst<Record>();
-      const Record& asRec = as.getConst<Record>();
+      const Record& inRec = in.getType().getRecord();
+      const Record& asRec = as.getRecord();
       Assert(inRec.getNumFields() == asRec.getNumFields());
-      NodeBuilder<> nb(kind::RECORD);
+      const Datatype & dt = ((DatatypeType)in.getType().toType()).getDatatype();
+      NodeBuilder<> nb(kind::APPLY_CONSTRUCTOR);
       nb << NodeManager::currentNM()->mkConst(asRec);
       for(size_t i = 0; i < asRec.getNumFields(); ++i) {
         Assert(inRec[i].first == asRec[i].first);
-        Node arg = NodeManager::currentNM()->mkNode(NodeManager::currentNM()->mkConst(RecordSelect(inRec[i].first)), in);
+        Node arg = NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, dt[0][i].getSelector(), in);
         if(inRec[i].second != asRec[i].second) {
           arg = rewriteAs(arg, TypeNode::fromType(asRec[i].second), processing);
         }
@@ -156,21 +157,6 @@ Node BooleanTermConverter::rewriteAs(TNode in, TypeNode as, std::map< TypeNode,
       processing.erase( in_t );
       return out;
     }
-    if(in.getType().isTuple()) {
-      Assert(as.isTuple());
-      Assert(in.getType().getNumChildren() == as.getNumChildren());
-      NodeBuilder<> nb(kind::TUPLE);
-      for(size_t i = 0; i < as.getNumChildren(); ++i) {
-        Node arg = NodeManager::currentNM()->mkNode(NodeManager::currentNM()->mkConst(TupleSelect(i)), in);
-        if(in.getType()[i] != as[i]) {
-          arg = rewriteAs(arg, as[i], processing);
-        }
-        nb << arg;
-      }
-      Node out = nb;
-      processing.erase( in_t );
-      return out;
-    }
     if(in.getType().isDatatype()) {
       if(as.isBoolean() && in.getType().hasAttribute(BooleanTermAttr())) {
         processing.erase( in_t );
@@ -387,25 +373,6 @@ TypeNode BooleanTermConverter::convertType(TypeNode type, bool datatypesContext)
     } else Debug("boolean-terms") << "OUT is DIFFERENT FROM TYPE" << endl;
     return out;
   }
-  if(type.isRecord()) {
-    const Record& rec = type.getConst<Record>();
-    const Record::FieldVector& fields = rec.getFields();
-    vector< pair<string, Type> > flds;
-    for(Record::FieldVector::const_iterator i = fields.begin(); i != fields.end(); ++i) {
-      TypeNode converted = convertType(TypeNode::fromType((*i).second), true);
-      if(TypeNode::fromType((*i).second) != converted) {
-        flds.push_back(make_pair((*i).first, converted.toType()));
-      } else {
-        flds.push_back(*i);
-      }
-    }
-    TypeNode newRec = NodeManager::currentNM()->mkRecordType(Record(flds));
-    Debug("tuprec") << "converted " << type << " to " << newRec << endl;
-    if(newRec != type) {
-      outNode = newRec;// cache it
-    }
-    return newRec;
-  }
   if(!type.isSort() && type.getNumChildren() > 0) {
     Debug("boolean-terms") << "here at A for " << type << ":" << type.getId() << endl;
     // This should handle tuples and arrays ok.
@@ -460,7 +427,9 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa
   stack< triple<TNode, theory::TheoryId, bool> > worklist;
   worklist.push(triple<TNode, theory::TheoryId, bool>(top, parentTheory, false));
   stack< NodeBuilder<> > result;
-  result.push(NodeBuilder<>(kind::TUPLE));
+  //AJR: not sure what the significance of "TUPLE" is here, seems to be a placeholder.  Since TUPLE is no longer a kind, replacing this with "AND".
+  //result.push(NodeBuilder<>(kind::TUPLE));
+  result.push(NodeBuilder<>(kind::AND));
 
   NodeManager* nm = NodeManager::currentNM();
 
@@ -670,26 +639,6 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa
           result.top() << top;
           worklist.pop();
           goto next_worklist;
-        } else if(t.isTuple() || t.isRecord()) {
-          TypeNode newType = convertType(t, true);
-          if(t != newType) {
-            Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()) + "'",
-                                  newType, "a tuple/record variable introduced by Boolean-term conversion",
-                                  NodeManager::SKOLEM_EXACT_NAME);
-            top.setAttribute(BooleanTermAttr(), n);
-            n.setAttribute(BooleanTermAttr(), top);
-            Debug("boolean-terms") << "adding subs: " << top << " :=> " << n << endl;
-            d_smt.d_theoryEngine->getModel()->addSubstitution(top, n);
-            Debug("boolean-terms") << "constructed: " << n << " of type " << newType << endl;
-            d_varCache[top] = n;
-            result.top() << n;
-            worklist.pop();
-            goto next_worklist;
-          }
-          d_varCache[top] = Node::null();
-          result.top() << top;
-          worklist.pop();
-          goto next_worklist;
         } else if(t.isDatatype() || t.isParametricDatatype()) {
           Debug("boolean-terms") << "found a var of datatype type" << endl;
           TypeNode newT = convertType(t, parentTheory == theory::THEORY_DATATYPES);
@@ -857,17 +806,13 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa
         Debug("bt") << "looking at: " << top << endl;
         // rewrite the operator, as necessary
         if(mk == kind::metakind::PARAMETERIZED) {
-          if(k == kind::RECORD) {
-            result.top() << convertType(top.getType(), parentTheory == theory::THEORY_DATATYPES);
-          } else if(k == kind::APPLY_TYPE_ASCRIPTION) {
+          if(k == kind::APPLY_TYPE_ASCRIPTION) {
             Node asc = nm->mkConst(AscriptionType(convertType(TypeNode::fromType(top.getOperator().getConst<AscriptionType>().getType()), parentTheory == theory::THEORY_DATATYPES).toType()));
             result.top() << asc;
             Debug("boolean-terms") << "setting " << top.getOperator() << ":" << top.getOperator().getId() << " to point to " << asc << ":" << asc.getId() << endl;
             asc.setAttribute(BooleanTermAttr(), top.getOperator());
           } else if(kindToTheoryId(k) != THEORY_BV &&
-                    k != kind::TUPLE_SELECT &&
                     k != kind::TUPLE_UPDATE &&
-                    k != kind::RECORD_SELECT &&
                     k != kind::RECORD_UPDATE &&
                     k != kind::DIVISIBLE &&
         // Theory parametric functions go here
@@ -899,7 +844,7 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa
     } else {
       Node n = result.top();
       result.pop();
-      Debug("boolean-terms") << "constructed: " << n << endl;
+      Debug("boolean-terms") << "constructed: " << n << " of type " << n.getType() << endl;
       if(parentTheory == theory::THEORY_BOOL) {
         if(n.getType().isBitVector() &&
            n.getType().getBitVectorSize() == 1) {
diff --git a/src/smt/model_postprocessor.cpp b/src/smt/model_postprocessor.cpp
index f9e449be3..aa645954b 100644
--- a/src/smt/model_postprocessor.cpp
+++ b/src/smt/model_postprocessor.cpp
@@ -71,21 +71,6 @@ Node ModelPostprocessor::rewriteAs(TNode n, TypeNode asType) {
       return NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, (tf ? asDatatype[0] : asDatatype[1]).getConstructor());
     }
   }
-  if(n.getType().isRecord() && asType.isRecord()) {
-    Debug("boolean-terms") << "+++ got a record - rewriteAs " << n << " : " << asType << endl;
-    const Record& rec CVC4_UNUSED = n.getType().getConst<Record>();
-    const Record& asRec = asType.getConst<Record>();
-    Assert(rec.getNumFields() == asRec.getNumFields());
-    Assert(n.getNumChildren() == asRec.getNumFields());
-    NodeBuilder<> b(n.getKind());
-    b << asType;
-    for(size_t i = 0; i < n.getNumChildren(); ++i) {
-      b << rewriteAs(n[i], TypeNode::fromType(asRec[i].second));
-    }
-    Node out = b;
-    Debug("boolean-terms") << "+++ returning record " << out << endl;
-    return out;
-  }
   Debug("boolean-terms") << "+++ rewriteAs " << n << " : " << asType << endl;
   if(n.getType().isArray()) {
     Assert(asType.isArray());
@@ -156,71 +141,8 @@ Node ModelPostprocessor::rewriteAs(TNode n, TypeNode asType) {
 void ModelPostprocessor::visit(TNode current, TNode parent) {
   Debug("tuprec") << "visiting " << current << endl;
   Assert(!alreadyVisited(current, TNode::null()));
-  if(current.getType().hasAttribute(expr::DatatypeTupleAttr())) {
-    Assert(current.getKind() == kind::APPLY_CONSTRUCTOR);
-    TypeNode expectType = current.getType().getAttribute(expr::DatatypeTupleAttr());
-    NodeBuilder<> b(kind::TUPLE);
-    TypeNode::iterator t = expectType.begin();
-    for(TNode::iterator i = current.begin(); i != current.end(); ++i, ++t) {
-      Assert(alreadyVisited(*i, TNode::null()));
-      Assert(t != expectType.end());
-      TNode n = d_nodes[*i];
-      n = n.isNull() ? *i : n;
-      if(!n.getType().isSubtypeOf(*t)) {
-        Assert(n.getType().isBitVector(1u) ||
-               (n.getType().isDatatype() && n.getType().hasAttribute(BooleanTermAttr())));
-        Assert(n.isConst());
-        Assert((*t).isBoolean());
-        if(n.getType().isBitVector(1u)) {
-          b << NodeManager::currentNM()->mkConst(bool(n.getConst<BitVector>().getValue() == 1));
-        } else {
-          // we assume (by construction) false is first; see boolean_terms.cpp
-          b << NodeManager::currentNM()->mkConst(bool(Datatype::indexOf(n.getOperator().toExpr()) == 1));
-        }
-      } else {
-        b << n;
-      }
-    }
-    Assert(t == expectType.end());
-    d_nodes[current] = b;
-    Debug("tuprec") << "returning " << d_nodes[current] << ", operator = " << d_nodes[current].getOperator() << endl;
-    // The assert below is too strong---we might be returning a model value but
-    // expect a type that still uses datatypes for tuples/records.  If it's
-    // really not the right type we should catch it in SmtEngine anyway.
-    // Assert(d_nodes[current].getType() == expectType);
-  } else if(current.getType().hasAttribute(expr::DatatypeRecordAttr())) {
-    Assert(current.getKind() == kind::APPLY_CONSTRUCTOR);
-    TypeNode expectType = current.getType().getAttribute(expr::DatatypeRecordAttr());
-    const Record& expectRec = expectType.getConst<Record>();
-    NodeBuilder<> b(kind::RECORD);
-    b << current.getType().getAttribute(expr::DatatypeRecordAttr());
-    const Record::FieldVector& fields = expectRec.getFields();
-    Record::FieldVector::const_iterator t = fields.begin();
-    for(TNode::iterator i = current.begin(); i != current.end(); ++i, ++t) {
-      Assert(alreadyVisited(*i, TNode::null()));
-      Assert(t != fields.end());
-      TNode n = d_nodes[*i];
-      n = n.isNull() ? *i : n;
-      if(!n.getType().isSubtypeOf(TypeNode::fromType((*t).second))) {
-        Assert(n.getType().isBitVector(1u) ||
-               (n.getType().isDatatype() && n.getType().hasAttribute(BooleanTermAttr())));
-        Assert(n.isConst());
-        Assert((*t).second.isBoolean());
-        if(n.getType().isBitVector(1u)) {
-          b << NodeManager::currentNM()->mkConst(bool(n.getConst<BitVector>().getValue() == 1));
-        } else {
-          // we assume (by construction) false is first; see boolean_terms.cpp
-          b << NodeManager::currentNM()->mkConst(bool(Datatype::indexOf(n.getOperator().toExpr()) == 1));
-        }
-      } else {
-        b << n;
-      }
-    }
-    Assert(t == fields.end());
-    d_nodes[current] = b;
-    Debug("tuprec") << "returning " << d_nodes[current] << ", operator = " << d_nodes[current].getOperator() << endl;
-    Assert(d_nodes[current].getType() == expectType);
-  } else if(current.getKind() == kind::APPLY_CONSTRUCTOR &&
+  bool rewriteChildren = false;
+  if(current.getKind() == kind::APPLY_CONSTRUCTOR &&
             ( current.getOperator().hasAttribute(BooleanTermAttr()) ||
               ( current.getOperator().getKind() == kind::APPLY_TYPE_ASCRIPTION &&
                 current.getOperator()[0].hasAttribute(BooleanTermAttr()) ) )) {
@@ -257,9 +179,13 @@ void ModelPostprocessor::visit(TNode current, TNode parent) {
     Debug("boolean-terms") << "model-post: " << current << endl
                            << "- returning " << n << endl;
     d_nodes[current] = n;
+    return;
   //all kinds with children that can occur in nodes in a model go here
   } else if(current.getKind() == kind::LAMBDA || current.getKind() == kind::SINGLETON || current.getKind() == kind::UNION || 
             current.getKind()==kind::STORE || current.getKind()==kind::STORE_ALL || current.getKind()==kind::APPLY_CONSTRUCTOR ) {
+    rewriteChildren = true;
+  }
+  if( rewriteChildren ){
     // rewrite based on children
     bool self = true;
     for(size_t i = 0; i < current.getNumChildren(); ++i) {
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 850b37fe0..007c5e049 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -2587,6 +2587,9 @@ bool SmtEnginePrivate::nonClausalSimplify() {
   TimerStat::CodeTimer nonclausalTimer(d_smt.d_stats->d_nonclausalSimplificationTime);
 
   Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify()" << endl;
+  for (unsigned i = 0; i < d_assertions.size(); ++ i) {
+    Trace("simplify") << "Assertion #" << i << " : " << d_assertions[i] << std::endl;
+  }
 
   if(d_propagatorNeedsFinish) {
     d_propagator.finish();
@@ -2622,6 +2625,8 @@ bool SmtEnginePrivate::nonClausalSimplify() {
     return false;
   }
 
+
+  Trace("simplify") << "Iterate through " << d_nonClausalLearnedLiterals.size() << " learned literals." << std::endl;
   // No conflict, go through the literals and solve them
   SubstitutionMap constantPropagations(d_smt.d_context);
   SubstitutionMap newSubstitutions(d_smt.d_context);
@@ -2632,10 +2637,12 @@ bool SmtEnginePrivate::nonClausalSimplify() {
     Node learnedLiteral = d_nonClausalLearnedLiterals[i];
     Assert(Rewriter::rewrite(learnedLiteral) == learnedLiteral);
     Assert(d_topLevelSubstitutions.apply(learnedLiteral) == learnedLiteral);
+    Trace("simplify") << "Process learnedLiteral : " << learnedLiteral << std::endl;
     Node learnedLiteralNew = newSubstitutions.apply(learnedLiteral);
     if (learnedLiteral != learnedLiteralNew) {
       learnedLiteral = Rewriter::rewrite(learnedLiteralNew);
     }
+    Trace("simplify") << "Process learnedLiteral, after newSubs : " << learnedLiteral << std::endl;
     for (;;) {
       learnedLiteralNew = constantPropagations.apply(learnedLiteral);
       if (learnedLiteralNew == learnedLiteral) {
@@ -2644,6 +2651,7 @@ bool SmtEnginePrivate::nonClausalSimplify() {
       ++d_smt.d_stats->d_numConstantProps;
       learnedLiteral = Rewriter::rewrite(learnedLiteralNew);
     }
+    Trace("simplify") << "Process learnedLiteral, after constProp : " << learnedLiteral << std::endl;
     // It might just simplify to a constant
     if (learnedLiteral.isConst()) {
       if (learnedLiteral.getConst<bool>()) {
@@ -2763,6 +2771,7 @@ bool SmtEnginePrivate::nonClausalSimplify() {
 #endif /* CVC4_ASSERTIONS */
   }
   // Resize the learnt
+  Trace("simplify") << "Resize non-clausal learned literals to " << j << std::endl;
   d_nonClausalLearnedLiterals.resize(j);
 
   hash_set<TNode, TNodeHashFunction> s;
@@ -3895,14 +3904,11 @@ void SmtEnginePrivate::processAssertions() {
       //apply pre-skolemization to existential quantifiers
       for (unsigned i = 0; i < d_assertions.size(); ++ i) {
         Node prev = d_assertions[i];
-        Trace("quantifiers-rewrite-debug") << "Pre-skolemize " << prev << "..." << std::endl;
-        vector< TypeNode > fvTypes;
-        vector< TNode > fvs;
-        d_assertions.replace(i, quantifiers::QuantifiersRewriter::preSkolemizeQuantifiers( prev, true, fvTypes, fvs ));
-        if( prev!=d_assertions[i] ){
-          d_assertions.replace(i, Rewriter::rewrite( d_assertions[i] ));
-          Trace("quantifiers-rewrite") << "*** Pre-skolemize " << prev << endl;
-          Trace("quantifiers-rewrite") << "   ...got " << d_assertions[i] << endl;
+        Node next = quantifiers::QuantifiersRewriter::preprocess( prev );
+        if( next!=prev ){
+          d_assertions.replace(i, Rewriter::rewrite( next ));
+          Trace("quantifiers-preprocess") << "*** Pre-skolemize " << prev << endl;
+          Trace("quantifiers-preprocess") << "   ...got " << d_assertions[i] << endl;
         }
       }
     }
diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h
index 1e7e714cf..0c00ed8df 100644
--- a/src/theory/datatypes/datatypes_rewriter.h
+++ b/src/theory/datatypes/datatypes_rewriter.h
@@ -100,43 +100,6 @@ public:
         }
       }
     }
-    if(in.getKind() == kind::TUPLE_SELECT && in[0].getKind() == kind::APPLY_CONSTRUCTOR) {
-      return RewriteResponse(REWRITE_DONE, in[0][in.getOperator().getConst<TupleSelect>().getIndex()]);
-    }
-    if(in.getKind() == kind::RECORD_SELECT && in[0].getKind() == kind::APPLY_CONSTRUCTOR) {
-      const Record& rec = in[0].getType().getAttribute(expr::DatatypeRecordAttr()).getConst<Record>();
-      return RewriteResponse(REWRITE_DONE, in[0][rec.getIndex(in.getOperator().getConst<RecordSelect>().getField())]);
-    }
-    if(in.getKind() == kind::APPLY_SELECTOR_TOTAL &&
-       (in[0].getKind() == kind::TUPLE || in[0].getKind() == kind::RECORD)) {
-      // These strange (half-tuple-converted) terms can be created by
-      // the system if you have something like "foo.1" for a tuple
-      // term foo.  The select is rewritten to "select_1(foo)".  If
-      // foo gets a value in the model from the TypeEnumerator, you
-      // then have a select of a tuple, and we should flatten that
-      // here.  Ditto for records, below.
-      Expr selectorExpr = in.getOperator().toExpr();
-      const Datatype& dt CVC4_UNUSED = Datatype::datatypeOf(selectorExpr);
-      TypeNode dtt CVC4_UNUSED = TypeNode::fromType(dt.getDatatypeType());
-      size_t selectorIndex = Datatype::indexOf(selectorExpr);
-      Debug("tuprec") << "looking at " << in << ", got selector index " << selectorIndex << std::endl;
-#ifdef CVC4_ASSERTIONS
-      // sanity checks: tuple- and record-converted datatypes should have one constructor
-      Assert(NodeManager::currentNM()->getDatatypeForTupleRecord(in[0].getType()) == dtt);
-      if(in[0].getKind() == kind::TUPLE) {
-        Assert(dtt.hasAttribute(expr::DatatypeTupleAttr()));
-        Assert(dtt.getAttribute(expr::DatatypeTupleAttr()) == in[0].getType());
-      } else {
-        Assert(dtt.hasAttribute(expr::DatatypeRecordAttr()));
-        Assert(dtt.getAttribute(expr::DatatypeRecordAttr()) == in[0].getType());
-      }
-      Assert(dt.getNumConstructors() == 1);
-      Assert(dt[0].getNumArgs() > selectorIndex);
-      Assert(dt[0][selectorIndex].getSelector() == selectorExpr);
-#endif /* CVC4_ASSERTIONS */
-      Debug("tuprec") << "==> returning " << in[0][selectorIndex] << std::endl;
-      return RewriteResponse(REWRITE_DONE, in[0][selectorIndex]);
-    }
     if(in.getKind() == kind::APPLY_SELECTOR_TOTAL && in[0].getKind() == kind::APPLY_CONSTRUCTOR) {
       // Have to be careful not to rewrite well-typed expressions
       // where the selector doesn't match the constructor,
@@ -236,45 +199,6 @@ public:
         return RewriteResponse(REWRITE_AGAIN_FULL, res );
       }
     }
-    if(in.getKind() == kind::TUPLE_SELECT &&
-       in[0].getKind() == kind::TUPLE) {
-      return RewriteResponse(REWRITE_DONE, in[0][in.getOperator().getConst<TupleSelect>().getIndex()]);
-    }
-    if(in.getKind() == kind::TUPLE_UPDATE &&
-       in[0].getKind() == kind::TUPLE) {
-      size_t ix = in.getOperator().getConst<TupleUpdate>().getIndex();
-      NodeBuilder<> b(kind::TUPLE);
-      for(TNode::const_iterator i = in[0].begin(); i != in[0].end(); ++i, --ix) {
-        if(ix == 0) {
-          b << in[1];
-        } else {
-          b << *i;
-        }
-      }
-      Node n = b;
-      Assert(n.getType().isSubtypeOf(in.getType()));
-      return RewriteResponse(REWRITE_DONE, n);
-    }
-    if(in.getKind() == kind::RECORD_SELECT &&
-       in[0].getKind() == kind::RECORD) {
-      return RewriteResponse(REWRITE_DONE, in[0][in[0].getOperator().getConst<Record>().getIndex(in.getOperator().getConst<RecordSelect>().getField())]);
-    }
-    if(in.getKind() == kind::RECORD_UPDATE &&
-       in[0].getKind() == kind::RECORD) {
-      size_t ix = in[0].getOperator().getConst<Record>().getIndex(in.getOperator().getConst<RecordUpdate>().getField());
-      NodeBuilder<> b(kind::RECORD);
-      b << in[0].getOperator();
-      for(TNode::const_iterator i = in[0].begin(); i != in[0].end(); ++i, --ix) {
-        if(ix == 0) {
-          b << in[1];
-        } else {
-          b << *i;
-        }
-      }
-      Node n = b;
-      Assert(n.getType().isSubtypeOf(in.getType()));
-      return RewriteResponse(REWRITE_DONE, n);
-    }
 
     if(in.getKind() == kind::EQUAL && in[0] == in[1]) {
       return RewriteResponse(REWRITE_DONE,
@@ -306,10 +230,7 @@ public:
 
   static bool checkClash( Node n1, Node n2, std::vector< Node >& rew ) {
     Trace("datatypes-rewrite-debug") << "Check clash : " << n1 << " " << n2 << std::endl;
-    if( (n1.getKind() == kind::APPLY_CONSTRUCTOR && n2.getKind() == kind::APPLY_CONSTRUCTOR) ||
-        (n1.getKind() == kind::TUPLE && n2.getKind() == kind::TUPLE) ||
-        (n1.getKind() == kind::RECORD && n2.getKind() == kind::RECORD) ) {
-      //n1.getKind()==kind::APPLY_CONSTRUCTOR
+    if( n1.getKind() == kind::APPLY_CONSTRUCTOR && n2.getKind() == kind::APPLY_CONSTRUCTOR ) {
       if( n1.getOperator() != n2.getOperator() ) {
         Trace("datatypes-rewrite-debug") << "Clash operators : " << n1 << " " << n2 << " " << n1.getOperator() << " " << n2.getOperator() << std::endl;
         return true;
@@ -459,12 +380,10 @@ public:
   /** is this term a datatype */
   static bool isTermDatatype( TNode n ){
     TypeNode tn = n.getType();
-    return tn.isDatatype() || tn.isParametricDatatype() ||
-           tn.isTuple() || tn.isRecord();
+    return tn.isDatatype() || tn.isParametricDatatype();
   }
   static bool isTypeDatatype( TypeNode tn ){
-    return tn.isDatatype() || tn.isParametricDatatype() ||
-           tn.isTuple() || tn.isRecord();
+    return tn.isDatatype() || tn.isParametricDatatype();
   }
 private:
   static Node collectRef( Node n, std::vector< Node >& sk, std::map< Node, Node >& rf, std::vector< Node >& rf_pending,
diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds
index 749d6b58a..c31a462bd 100644
--- a/src/theory/datatypes/kinds
+++ b/src/theory/datatypes/kinds
@@ -91,30 +91,6 @@ typerule MU ::CVC4::theory::datatypes::DatatypeMuTypeRule
 # mu applications are constant expressions
 construle MU ::CVC4::theory::datatypes::DatatypeMuTypeRule
 
-operator TUPLE_TYPE 0: "tuple type"
-cardinality TUPLE_TYPE \
-    "::CVC4::theory::datatypes::TupleProperties::computeCardinality(%TYPE%)" \
-    "theory/datatypes/theory_datatypes_type_rules.h"
-well-founded TUPLE_TYPE \
-    "::CVC4::theory::datatypes::TupleProperties::isWellFounded(%TYPE%)" \
-    "::CVC4::theory::datatypes::TupleProperties::mkGroundTerm(%TYPE%)" \
-    "theory/datatypes/theory_datatypes_type_rules.h"
-enumerator TUPLE_TYPE \
-    "::CVC4::theory::datatypes::TupleEnumerator" \
-    "theory/datatypes/type_enumerator.h"
-
-operator TUPLE 0: "a tuple (N-ary)"
-typerule TUPLE ::CVC4::theory::datatypes::TupleTypeRule
-construle TUPLE ::CVC4::theory::datatypes::TupleProperties
-
-constant TUPLE_SELECT_OP \
-        ::CVC4::TupleSelect \
-        ::CVC4::TupleSelectHashFunction \
-        "util/tuple.h" \
-        "operator for a tuple select; payload is an instance of the CVC4::TupleSelect class"
-parameterized TUPLE_SELECT TUPLE_SELECT_OP 1 "tuple select; first parameter is a TUPLE_SELECT_OP, second is the tuple"
-typerule TUPLE_SELECT ::CVC4::theory::datatypes::TupleSelectTypeRule
-
 constant TUPLE_UPDATE_OP \
         ::CVC4::TupleUpdate \
         ::CVC4::TupleUpdateHashFunction \
@@ -129,33 +105,21 @@ constant RECORD_TYPE \
     "expr/record.h" \
     "record type"
 cardinality RECORD_TYPE \
-    "::CVC4::theory::datatypes::TupleProperties::computeCardinality(%TYPE%)" \
+    "::CVC4::theory::datatypes::RecordProperties::computeCardinality(%TYPE%)" \
     "theory/datatypes/theory_datatypes_type_rules.h"
 well-founded RECORD_TYPE \
-    "::CVC4::theory::datatypes::TupleProperties::isWellFounded(%TYPE%)" \
+    "::CVC4::theory::datatypes::RecordProperties::isWellFounded(%TYPE%)" \
     "::CVC4::theory::datatypes::RecordProperties::mkGroundTerm(%TYPE%)" \
     "theory/datatypes/theory_datatypes_type_rules.h"
 enumerator RECORD_TYPE \
     "::CVC4::theory::datatypes::RecordEnumerator" \
     "theory/datatypes/type_enumerator.h"
 
-parameterized RECORD RECORD_TYPE 0: "a record; first parameter is a RECORD_TYPE; remaining parameters (if any) are the individual values for fields, in order"
-typerule RECORD ::CVC4::theory::datatypes::RecordTypeRule
-construle RECORD ::CVC4::theory::datatypes::RecordProperties
-
-constant RECORD_SELECT_OP \
-        ::CVC4::RecordSelect \
-        ::CVC4::RecordSelectHashFunction \
-        "expr/record.h" \
-        "operator for a record select; payload is an instance CVC4::RecordSelect class"
-parameterized RECORD_SELECT RECORD_SELECT_OP 1 "record select; first parameter is a RECORD_SELECT_OP, second is a record term to select from"
-typerule RECORD_SELECT ::CVC4::theory::datatypes::RecordSelectTypeRule
-
 constant RECORD_UPDATE_OP \
         ::CVC4::RecordUpdate \
         ::CVC4::RecordUpdateHashFunction \
         "expr/record.h" \
-        "operator for a record update; payload is an instance CVC4::RecordSelect class"
+        "operator for a record update; payload is an instance CVC4::RecordUpdate class"
 parameterized RECORD_UPDATE RECORD_UPDATE_OP 2 "record update; first parameter is a RECORD_UPDATE_OP (which references a field), second is a record term to update, third is the element to store in the record in the given field"
 typerule RECORD_UPDATE ::CVC4::theory::datatypes::RecordUpdateTypeRule
 
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index c8d7338a7..ad2b1a297 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -147,12 +147,8 @@ void TheoryDatatypes::check(Effort e) {
 
     // extra debug check to make sure that the rewriter did its job correctly
     Assert( atom.getKind() != kind::EQUAL ||
-            ( atom[0].getKind() != kind::TUPLE && atom[1].getKind() != kind::TUPLE &&
-              atom[0].getKind() != kind::RECORD && atom[1].getKind() != kind::RECORD &&
-              atom[0].getKind() != kind::TUPLE_UPDATE && atom[1].getKind() != kind::TUPLE_UPDATE &&
-              atom[0].getKind() != kind::RECORD_UPDATE && atom[1].getKind() != kind::RECORD_UPDATE &&
-              atom[0].getKind() != kind::TUPLE_SELECT && atom[1].getKind() != kind::TUPLE_SELECT &&
-              atom[0].getKind() != kind::RECORD_SELECT && atom[1].getKind() != kind::RECORD_SELECT ),
+            ( atom[0].getKind() != kind::TUPLE_UPDATE && atom[1].getKind() != kind::TUPLE_UPDATE &&
+              atom[0].getKind() != kind::RECORD_UPDATE && atom[1].getKind() != kind::RECORD_UPDATE),
             "tuple/record escaped into datatypes decision procedure; should have been rewritten away" );
 
     //assert the fact
@@ -550,86 +546,21 @@ void TheoryDatatypes::presolve() {
 Node TheoryDatatypes::ppRewrite(TNode in) {
   Debug("tuprec") << "TheoryDatatypes::ppRewrite(" << in << ")" << endl;
 
-  if(in.getKind() == kind::TUPLE_SELECT) {
-    TypeNode t = in[0].getType();
-    if(t.hasAttribute(expr::DatatypeTupleAttr())) {
-      t = t.getAttribute(expr::DatatypeTupleAttr());
-    }
-    TypeNode dtt = NodeManager::currentNM()->getDatatypeForTupleRecord(t);
-    const Datatype& dt = DatatypeType(dtt.toType()).getDatatype();
-    return NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, Node::fromExpr(dt[0][in.getOperator().getConst<TupleSelect>().getIndex()].getSelector()), in[0]);
-  } else if(in.getKind() == kind::RECORD_SELECT) {
-    TypeNode t = in[0].getType();
-    if(t.hasAttribute(expr::DatatypeRecordAttr())) {
-      t = t.getAttribute(expr::DatatypeRecordAttr());
-    }
-    TypeNode dtt = NodeManager::currentNM()->getDatatypeForTupleRecord(t);
-    const Datatype& dt = DatatypeType(dtt.toType()).getDatatype();
-    return NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, Node::fromExpr(dt[0][in.getOperator().getConst<RecordSelect>().getField()].getSelector()), in[0]);
-  }
-
   TypeNode t = in.getType();
 
-  // we only care about tuples and records here
-  if(in.getKind() != kind::TUPLE && in.getKind() != kind::TUPLE_UPDATE &&
-     in.getKind() != kind::RECORD && in.getKind() != kind::RECORD_UPDATE) {
-    if((t.isTuple() || t.isRecord()) && in.hasAttribute(smt::BooleanTermAttr())) {
-      Debug("tuprec") << "should map " << in << " of type " << t << " back to " << in.getAttribute(smt::BooleanTermAttr()).getType() << endl;
-      Debug("tuprec") << "so " << NodeManager::currentNM()->getDatatypeForTupleRecord(t).getDatatype() << " goes to " << NodeManager::currentNM()->getDatatypeForTupleRecord(in.getAttribute(smt::BooleanTermAttr()).getType()).getDatatype() << endl;
-      if(t.isTuple()) {
-        Debug("tuprec") << "current datatype-tuple-attr is " << NodeManager::currentNM()->getDatatypeForTupleRecord(t).getAttribute(expr::DatatypeTupleAttr()) << endl;
-        Debug("tuprec") << "setting to " << NodeManager::currentNM()->getDatatypeForTupleRecord(in.getAttribute(smt::BooleanTermAttr()).getType()).getAttribute(expr::DatatypeTupleAttr()) << endl;
-        NodeManager::currentNM()->getDatatypeForTupleRecord(t).setAttribute(expr::DatatypeTupleAttr(), NodeManager::currentNM()->getDatatypeForTupleRecord(in.getAttribute(smt::BooleanTermAttr()).getType()).getAttribute(expr::DatatypeTupleAttr()));
-      } else {
-        Debug("tuprec") << "current datatype-record-attr is " << NodeManager::currentNM()->getDatatypeForTupleRecord(t).getAttribute(expr::DatatypeRecordAttr()) << endl;
-        Debug("tuprec") << "setting to " << NodeManager::currentNM()->getDatatypeForTupleRecord(in.getAttribute(smt::BooleanTermAttr()).getType()).getAttribute(expr::DatatypeRecordAttr()) << endl;
-        NodeManager::currentNM()->getDatatypeForTupleRecord(t).setAttribute(expr::DatatypeRecordAttr(), NodeManager::currentNM()->getDatatypeForTupleRecord(in.getAttribute(smt::BooleanTermAttr()).getType()).getAttribute(expr::DatatypeRecordAttr()));
-      }
-    }
-
-    if( in.getKind()==EQUAL ){
-      Node nn;
-      std::vector< Node > rew;
-      if( DatatypesRewriter::checkClash(in[0], in[1], rew) ){
-        nn = NodeManager::currentNM()->mkConst(false);
-      }else{
-        nn = rew.size()==0 ? d_true :
-                  ( rew.size()==1 ? rew[0] : NodeManager::currentNM()->mkNode( kind::AND, rew ) );
-      }
-      return nn;
-    }
-
-    // nothing to do
-    return in;
-  }
-
-  if(t.hasAttribute(expr::DatatypeTupleAttr())) {
-    t = t.getAttribute(expr::DatatypeTupleAttr());
-  } else if(t.hasAttribute(expr::DatatypeRecordAttr())) {
-    t = t.getAttribute(expr::DatatypeRecordAttr());
-  }
-
-  // if the type doesn't have an associated datatype, then make one for it
-  TypeNode dtt = (t.isTuple() || t.isRecord()) ? NodeManager::currentNM()->getDatatypeForTupleRecord(t) : t;
-
-  const Datatype& dt = DatatypeType(dtt.toType()).getDatatype();
-
-  // now rewrite the expression
-  Node n;
-  if(in.getKind() == kind::TUPLE || in.getKind() == kind::RECORD) {
-    NodeBuilder<> b(kind::APPLY_CONSTRUCTOR);
-    b << Node::fromExpr(dt[0].getConstructor());
-    b.append(in.begin(), in.end());
-    n = b;
-  } else if(in.getKind() == kind::TUPLE_UPDATE || in.getKind() == kind::RECORD_UPDATE) {
+  if(in.getKind() == kind::TUPLE_UPDATE || in.getKind() == kind::RECORD_UPDATE) {
+    Assert( t.isDatatype() );
+    const Datatype& dt = DatatypeType(t.toType()).getDatatype();
     NodeBuilder<> b(kind::APPLY_CONSTRUCTOR);
     b << Node::fromExpr(dt[0].getConstructor());
     size_t size, updateIndex;
     if(in.getKind() == kind::TUPLE_UPDATE) {
-      size = t.getNumChildren();
+      Assert( t.isTuple() );
+      size = t.getTupleLength();
       updateIndex = in.getOperator().getConst<TupleUpdate>().getIndex();
     } else { // kind::RECORD_UPDATE
-      const Record& record = t.getConst<Record>();
+      Assert( t.isRecord() );
+      const Record& record = t.getRecord();
       size = record.getNumFields();
       updateIndex = record.getIndex(in.getOperator().getConst<RecordUpdate>().getField());
     }
@@ -647,15 +578,39 @@ Node TheoryDatatypes::ppRewrite(TNode in) {
       }
     }
     Debug("tuprec") << "builder says " << b << std::endl;
-    n = b;
+    Node n = b;
+    return n;
   }
 
-  Assert(!n.isNull());
+  if((t.isTuple() || t.isRecord()) && in.hasAttribute(smt::BooleanTermAttr())) {
+    Debug("tuprec") << "should map " << in << " of type " << t << " back to " << in.getAttribute(smt::BooleanTermAttr()).getType() << endl;
+    Debug("tuprec") << "so " << t.getDatatype() << " goes to " << in.getAttribute(smt::BooleanTermAttr()).getType().getDatatype() << endl;
+    if(t.isTuple()) {
+      Debug("tuprec") << "current datatype-tuple-attr is " << t.getAttribute(expr::DatatypeTupleAttr()) << endl;
+      Debug("tuprec") << "setting to " << in.getAttribute(smt::BooleanTermAttr()).getType().getAttribute(expr::DatatypeTupleAttr()) << endl;
+      t.setAttribute(expr::DatatypeTupleAttr(), in.getAttribute(smt::BooleanTermAttr()).getType().getAttribute(expr::DatatypeTupleAttr()));
+    } else {
+      Debug("tuprec") << "current datatype-record-attr is " << t.getAttribute(expr::DatatypeRecordAttr()) << endl;
+      Debug("tuprec") << "setting to " << in.getAttribute(smt::BooleanTermAttr()).getType().getAttribute(expr::DatatypeRecordAttr()) << endl;
+      t.setAttribute(expr::DatatypeRecordAttr(), in.getAttribute(smt::BooleanTermAttr()).getType().getAttribute(expr::DatatypeRecordAttr()));
+    }
+  }
 
+  if( in.getKind()==EQUAL ){
+    Node nn;
+    std::vector< Node > rew;
+    if( DatatypesRewriter::checkClash(in[0], in[1], rew) ){
+      nn = NodeManager::currentNM()->mkConst(false);
+    }else{
+      nn = rew.size()==0 ? d_true :
+                ( rew.size()==1 ? rew[0] : NodeManager::currentNM()->mkNode( kind::AND, rew ) );
+    }
+    return nn;
+  }
 
-  Debug("tuprec") << "REWROTE " << in << " to " << n << std::endl;
+  // nothing to do
+  return in;
 
-  return n;
 }
 
 void TheoryDatatypes::addSharedTerm(TNode t) {
@@ -2123,9 +2078,7 @@ Node TheoryDatatypes::mkAnd( std::vector< TNode >& assumptions ) {
 }
 
 bool TheoryDatatypes::checkClashModEq( TNode n1, TNode n2, std::vector< Node >& exp, std::vector< std::pair< TNode, TNode > >& deq_cand ) {
-  if( (n1.getKind() == kind::APPLY_CONSTRUCTOR && n2.getKind() == kind::APPLY_CONSTRUCTOR) ||
-      (n1.getKind() == kind::TUPLE && n2.getKind() == kind::TUPLE) ||
-      (n1.getKind() == kind::RECORD && n2.getKind() == kind::RECORD) ) {
+  if( n1.getKind() == kind::APPLY_CONSTRUCTOR && n2.getKind() == kind::APPLY_CONSTRUCTOR ) {
     if( n1.getOperator() != n2.getOperator() ) {
       return true;
     } else {
diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h
index 8b723f43e..477ce6ba5 100644
--- a/src/theory/datatypes/theory_datatypes_type_rules.h
+++ b/src/theory/datatypes/theory_datatypes_type_rules.h
@@ -267,44 +267,6 @@ struct ConstructorProperties {
   }
 };/* struct ConstructorProperties */
 
-struct TupleTypeRule {
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) {
-    Assert(n.getKind() == kind::TUPLE);
-    std::vector<TypeNode> types;
-    for(TNode::iterator child_it = n.begin(), child_it_end = n.end();
-        child_it != child_it_end;
-        ++child_it) {
-      types.push_back((*child_it).getType(check));
-    }
-    return nodeManager->mkTupleType(types);
-  }
-};/* struct TupleTypeRule */
-
-struct TupleSelectTypeRule {
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) {
-    Assert(n.getKind() == kind::TUPLE_SELECT);
-    if(n.getOperator().getKind() != kind::TUPLE_SELECT_OP) {
-      throw TypeCheckingExceptionPrivate(n, "Tuple-select expression requires TupleSelect operator");
-    }
-    const TupleSelect& ts = n.getOperator().getConst<TupleSelect>();
-    TypeNode tupleType = n[0].getType(check);
-    if(!tupleType.isTuple()) {
-      if(!tupleType.hasAttribute(expr::DatatypeTupleAttr())) {
-        throw TypeCheckingExceptionPrivate(n, "Tuple-select expression formed over non-tuple");
-      }
-      tupleType = tupleType.getAttribute(expr::DatatypeTupleAttr());
-    }
-    if(ts.getIndex() >= tupleType.getNumChildren()) {
-      std::stringstream ss;
-      ss << "Tuple-select expression index `" << ts.getIndex()
-         << "' is not a valid index; tuple type only has "
-         << tupleType.getNumChildren() << " fields";
-      throw TypeCheckingExceptionPrivate(n, ss.str().c_str());
-    }
-    return tupleType[ts.getIndex()];
-  }
-};/* struct TupleSelectTypeRule */
-
 struct TupleUpdateTypeRule {
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) {
     Assert(n.getKind() == kind::TUPLE_UPDATE);
@@ -313,16 +275,14 @@ struct TupleUpdateTypeRule {
     TypeNode newValue = n[1].getType(check);
     if(check) {
       if(!tupleType.isTuple()) {
-        if(!tupleType.hasAttribute(expr::DatatypeTupleAttr())) {
-          throw TypeCheckingExceptionPrivate(n, "Tuple-update expression formed over non-tuple");
-        }
+        throw TypeCheckingExceptionPrivate(n, "Tuple-update expression formed over non-tuple");
         tupleType = tupleType.getAttribute(expr::DatatypeTupleAttr());
       }
-      if(tu.getIndex() >= tupleType.getNumChildren()) {
+      if(tu.getIndex() >= tupleType.getTupleLength()) {
         std::stringstream ss;
         ss << "Tuple-update expression index `" << tu.getIndex()
            << "' is not a valid index; tuple type only has "
-           << tupleType.getNumChildren() << " fields";
+           << tupleType.getTupleLength() << " fields";
         throw TypeCheckingExceptionPrivate(n, ss.str().c_str());
       }
     }
@@ -330,138 +290,6 @@ struct TupleUpdateTypeRule {
   }
 };/* struct TupleUpdateTypeRule */
 
-struct TupleProperties {
-  inline static Cardinality computeCardinality(TypeNode type) {
-    // Don't assert this; allow other theories to use this cardinality
-    // computation.
-    //
-    // Assert(type.getKind() == kind::TUPLE_TYPE);
-
-    Cardinality card(1);
-    for(TypeNode::iterator i = type.begin(),
-          i_end = type.end();
-        i != i_end;
-        ++i) {
-      card *= (*i).getCardinality();
-    }
-
-    return card;
-  }
-
-  inline static bool isWellFounded(TypeNode type) {
-    // Don't assert this; allow other theories to use this
-    // wellfoundedness computation.
-    //
-    // Assert(type.getKind() == kind::TUPLE_TYPE);
-
-    for(TypeNode::iterator i = type.begin(),
-          i_end = type.end();
-        i != i_end;
-        ++i) {
-      if(! (*i).isWellFounded()) {
-        return false;
-      }
-    }
-
-    return true;
-  }
-
-  inline static Node mkGroundTerm(TypeNode type) {
-    Assert(type.getKind() == kind::TUPLE_TYPE);
-
-    std::vector<Node> children;
-    for(TypeNode::iterator i = type.begin(),
-          i_end = type.end();
-        i != i_end;
-        ++i) {
-      children.push_back((*i).mkGroundTerm());
-    }
-
-    return NodeManager::currentNM()->mkNode(kind::TUPLE, children);
-  }
-
-  inline static bool computeIsConst(NodeManager* nodeManager, TNode n) {
-    Assert(n.getKind() == kind::TUPLE);
-    NodeManagerScope nms(nodeManager);
-
-    for(TNode::iterator i = n.begin(),
-          i_end = n.end();
-        i != i_end;
-        ++i) {
-      if(! (*i).isConst()) {
-        return false;
-      }
-    }
-
-    return true;
-  }
-};/* struct TupleProperties */
-
-struct RecordTypeRule {
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) {
-    Assert(n.getKind() == kind::RECORD);
-    NodeManagerScope nms(nodeManager);
-    const Record& rec = n.getOperator().getConst<Record>();
-    const Record::FieldVector& fields = rec.getFields();
-    if(check) {
-      Record::FieldVector::const_iterator i = fields.begin();
-      for(TNode::iterator child_it = n.begin(), child_it_end = n.end();
-          child_it != child_it_end;
-          ++child_it, ++i) {
-        if(i == fields.end()) {
-          throw TypeCheckingExceptionPrivate(n, "record description has different length than record literal");
-        }
-        if(!(*child_it).getType(check).isComparableTo(TypeNode::fromType((*i).second))) {
-          std::stringstream ss;
-          ss << "record description types differ from record literal types\nDescription type: " << (*child_it).getType() << "\nLiteral type: " << (*i).second;
-          throw TypeCheckingExceptionPrivate(n, ss.str());
-        }
-      }
-      if(i != fields.end()) {
-        throw TypeCheckingExceptionPrivate(n, "record description has different length than record literal");
-      }
-    }
-    return nodeManager->mkRecordType(rec);
-  }
-};/* struct RecordTypeRule */
-
-struct RecordSelectTypeRule {
-  inline static Record::FieldVector::const_iterator record_find(const Record::FieldVector& fields, std::string name){
-    for(Record::FieldVector::const_iterator i = fields.begin(), i_end = fields.end(); i != i_end; ++i){
-      if((*i).first == name) {
-        return i;
-      }
-    }
-    return fields.end();
-  }
-
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) {
-    Assert(n.getKind() == kind::RECORD_SELECT);
-    NodeManagerScope nms(nodeManager);
-    if(n.getOperator().getKind() != kind::RECORD_SELECT_OP) {
-      throw TypeCheckingExceptionPrivate(n, "Tuple-select expression requires TupleSelect operator");
-    }
-    const RecordSelect& rs = n.getOperator().getConst<RecordSelect>();
-    TypeNode recordType = n[0].getType(check);
-    if(!recordType.isRecord()) {
-      if(!recordType.hasAttribute(expr::DatatypeRecordAttr())) {
-        throw TypeCheckingExceptionPrivate(n, "Record-select expression formed over non-record");
-      }
-      recordType = recordType.getAttribute(expr::DatatypeRecordAttr());
-    }
-    const Record& rec = recordType.getRecord();
-    const Record::FieldVector& fields = rec.getFields();
-    Record::FieldVector::const_iterator field = record_find(fields, rs.getField());
-    if(field == fields.end()) {
-      std::stringstream ss;
-      ss << "Record-select field `" << rs.getField()
-         << "' is not a valid field name for the record type";
-      throw TypeCheckingExceptionPrivate(n, ss.str().c_str());
-    }
-    return TypeNode::fromType((*field).second);
-  }
-};/* struct RecordSelectTypeRule */
-
 struct RecordUpdateTypeRule {
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) {
     Assert(n.getKind() == kind::RECORD_UPDATE);
@@ -471,10 +299,7 @@ struct RecordUpdateTypeRule {
     TypeNode newValue = n[1].getType(check);
     if(check) {
       if(!recordType.isRecord()) {
-        if(!recordType.hasAttribute(expr::DatatypeRecordAttr())) {
-          throw TypeCheckingExceptionPrivate(n, "Record-update expression formed over non-record");
-        }
-        recordType = recordType.getAttribute(expr::DatatypeRecordAttr());
+        throw TypeCheckingExceptionPrivate(n, "Record-update expression formed over non-record");
       }
       const Record& rec = recordType.getRecord();
       if(!rec.contains(ru.getField())) {
@@ -491,33 +316,16 @@ struct RecordUpdateTypeRule {
 struct RecordProperties {
   inline static Node mkGroundTerm(TypeNode type) {
     Assert(type.getKind() == kind::RECORD_TYPE);
-
-    const Record& rec = type.getRecord();
-    const Record::FieldVector& fields = rec.getFields();
-    std::vector<Node> children;
-    for(Record::FieldVector::const_iterator i = fields.begin(),
-          i_end = fields.end();
-        i != i_end;
-        ++i) {
-      children.push_back((*i).second.mkGroundTerm());
-    }
-
-    return NodeManager::currentNM()->mkNode(NodeManager::currentNM()->mkConst(rec), children);
+    return Node::null();
   }
-
   inline static bool computeIsConst(NodeManager* nodeManager, TNode n) {
-    Assert(n.getKind() == kind::RECORD);
-    NodeManagerScope nms(nodeManager);
-
-    for(TNode::iterator i = n.begin(),
-          i_end = n.end();
-        i != i_end;
-        ++i) {
-      if(! (*i).isConst()) {
-        return false;
-      }
-    }
-
+    return true;
+  }
+  inline static Cardinality computeCardinality(TypeNode type) {
+    Cardinality card(1);
+    return card;
+  }
+  inline static bool isWellFounded(TypeNode type) {
     return true;
   }
 };/* struct RecordProperties */
diff --git a/src/theory/datatypes/type_enumerator.cpp b/src/theory/datatypes/type_enumerator.cpp
index 62446a937..77db1968a 100644
--- a/src/theory/datatypes/type_enumerator.cpp
+++ b/src/theory/datatypes/type_enumerator.cpp
@@ -221,3 +221,4 @@ Node DatatypesEnumerator::getTermEnum( TypeNode tn, unsigned i ){
    ++*this; //increment( d_ctor );
    AlwaysAssert( !isFinished() );
 }
+
diff --git a/src/theory/datatypes/type_enumerator.h b/src/theory/datatypes/type_enumerator.h
index 921ba403c..1f30498d6 100644
--- a/src/theory/datatypes/type_enumerator.h
+++ b/src/theory/datatypes/type_enumerator.h
@@ -177,90 +177,6 @@ public:
 
 };/* DatatypesEnumerator */
 
-class TupleEnumerator : public TypeEnumeratorBase<TupleEnumerator> {
-  TypeEnumeratorProperties * d_tep;
-  TypeEnumerator** d_enumerators;
-
-  /** Allocate and initialize the delegate enumerators */
-  void newEnumerators() {
-    d_enumerators = new TypeEnumerator*[getType().getNumChildren()];
-    for(size_t i = 0; i < getType().getNumChildren(); ++i) {
-      d_enumerators[i] = new TypeEnumerator(getType()[i], d_tep);
-    }
-  }
-
-  void deleteEnumerators() throw() {
-    if(d_enumerators != NULL) {
-      for(size_t i = 0; i < getType().getNumChildren(); ++i) {
-        delete d_enumerators[i];
-      }
-      delete [] d_enumerators;
-      d_enumerators = NULL;
-    }
-  }
-
-public:
-
-  TupleEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) throw() :
-    TypeEnumeratorBase<TupleEnumerator>(type), d_tep(tep) {
-    Assert(type.isTuple());
-    newEnumerators();
-  }
-
-  TupleEnumerator(const TupleEnumerator& te) throw() :
-    TypeEnumeratorBase<TupleEnumerator>(te.getType()),
-    d_tep(te.d_tep),
-    d_enumerators(NULL) {
-
-    if(te.d_enumerators != NULL) {
-      newEnumerators();
-      for(size_t i = 0; i < getType().getNumChildren(); ++i) {
-        *d_enumerators[i] = TypeEnumerator(*te.d_enumerators[i]);
-      }
-    }
-  }
-
-  virtual ~TupleEnumerator() throw() {
-    deleteEnumerators();
-  }
-
-  Node operator*() throw(NoMoreValuesException) {
-    if(isFinished()) {
-      throw NoMoreValuesException(getType());
-    }
-
-    NodeBuilder<> nb(kind::TUPLE);
-    for(size_t i = 0; i < getType().getNumChildren(); ++i) {
-      nb << **d_enumerators[i];
-    }
-    return Node(nb);
-  }
-
-  TupleEnumerator& operator++() throw() {
-    if(isFinished()) {
-      return *this;
-    }
-
-    size_t i;
-    for(i = 0; i < getType().getNumChildren(); ++i) {
-      if(d_enumerators[i]->isFinished()) {
-        *d_enumerators[i] = TypeEnumerator(getType()[i], d_tep);
-      } else {
-        ++*d_enumerators[i];
-        return *this;
-      }
-    }
-
-    deleteEnumerators();
-
-    return *this;
-  }
-
-  bool isFinished() throw() {
-    return d_enumerators == NULL;
-  }
-
-};/* TupleEnumerator */
 
 class RecordEnumerator : public TypeEnumeratorBase<RecordEnumerator> {
   TypeEnumeratorProperties * d_tep;
@@ -316,15 +232,8 @@ public:
       throw NoMoreValuesException(getType());
     }
 
-    NodeBuilder<> nb(kind::RECORD);
-    Debug("te") << "record enumerator: creating record of type " << getType() << std::endl;
-    nb << getType();
-    const Record& rec = getType().getConst<Record>();
-    for(size_t i = 0; i < rec.getNumFields(); ++i) {
-      Debug("te") << " - " << i << " " << std::flush << "=> " << **d_enumerators[i] << std::endl;
-      nb << **d_enumerators[i];
-    }
-    return Node(nb);
+
+    return Node::null();
   }
 
   RecordEnumerator& operator++() throw() {
diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp
index 00a5241f5..ff0da13e1 100644
--- a/src/theory/quantifiers/full_model_check.cpp
+++ b/src/theory/quantifiers/full_model_check.cpp
@@ -819,8 +819,8 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, No
       }
     }
     d_addedLemmas += addedLemmas;
-    Trace("fmc-exh") << "----Finished Exhaustive instantiate, lemmas = " << addedLemmas << std::endl;
-    return true;
+    Trace("fmc-exh") << "----Finished Exhaustive instantiate, lemmas = " << addedLemmas << ", incomplete=" << riter.d_incomplete << std::endl;
+    return addedLemmas>0 || !riter.d_incomplete;
   }else{
     Trace("fmc-exh") << "----Finished Exhaustive instantiate, failed." << std::endl;
     return false;
diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp
index fc1f052c3..bf91f74c6 100644
--- a/src/theory/quantifiers/quant_util.cpp
+++ b/src/theory/quantifiers/quant_util.cpp
@@ -349,6 +349,9 @@ void QuantPhaseReq::getPolarity( Node n, int child, bool hasPol, bool pol, bool&
   }else if( n.getKind()==ITE ){
     newHasPol = (child!=0) && hasPol;
     newPol = pol;
+  }else if( n.getKind()==FORALL ){
+    newHasPol = (child==1) && hasPol;
+    newPol = pol;
   }else{
     newHasPol = false;
     newPol = pol;
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index fc5b692b2..afe8cd598 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -391,7 +391,7 @@ Node QuantifiersRewriter::computeNNF( Node body ){
 void QuantifiersRewriter::computeDtTesterIteSplit( Node n, std::map< Node, Node >& pcons, std::map< Node, std::map< int, Node > >& ncons,
                                                    std::vector< Node >& conj ){
   if( n.getKind()==ITE && n[0].getKind()==APPLY_TESTER && n[1].getType().isBoolean() ){
-  Trace("quantifiers-rewrite-ite-debug") << "Split tester condition : " << n << std::endl;
+    Trace("quantifiers-rewrite-ite-debug") << "Split tester condition : " << n << std::endl;
     Node x = n[0][0];
     std::map< Node, Node >::iterator itp = pcons.find( x );
     if( itp!=pcons.end() ){
@@ -506,35 +506,42 @@ int getEntailedCond( Node n, std::map< Node, bool >& currCond ){
   return 0;
 }
 
-bool addEntailedCond( Node n, bool pol, std::map< Node, bool >& currCond, std::vector< Node >& new_cond ) {
+bool addEntailedCond( Node n, bool pol, std::map< Node, bool >& currCond, std::vector< Node >& new_cond, bool& conflict ) {
   std::map< Node, bool >::iterator it = currCond.find( n );
   if( it==currCond.end() ){
-    Trace("quantifiers-rewrite-ite-debug") << "ITE cond : " << n << " -> " << pol << std::endl;
+    Trace("quantifiers-rewrite-term-debug") << "cond : " << n << " -> " << pol << std::endl;
     new_cond.push_back( n );
     currCond[n] = pol;
     return true;
   }else{
-    Assert( it->second==pol );
+    if( it->second!=pol ){
+      Trace("quantifiers-rewrite-term-debug") << "CONFLICTING cond : " << n << " -> " << pol << std::endl;
+      conflict = true;
+    }
     return false;
   }
 }
 
-void setEntailedCond( Node n, bool pol, std::map< Node, bool >& currCond, std::vector< Node >& new_cond ) {
+void setEntailedCond( Node n, bool pol, std::map< Node, bool >& currCond, std::vector< Node >& new_cond, bool& conflict ) {
   if( ( n.getKind()==AND && pol ) || ( n.getKind()==OR && !pol ) ){
     for( unsigned i=0; i<n.getNumChildren(); i++ ){
-      setEntailedCond( n[i], pol, currCond, new_cond );
+      setEntailedCond( n[i], pol, currCond, new_cond, conflict );
+      if( conflict ){
+        break;
+      }
     }
   }else if( n.getKind()==NOT ){
-    setEntailedCond( n[0], !pol, currCond, new_cond );
+    setEntailedCond( n[0], !pol, currCond, new_cond, conflict );
+    return;
   }else if( n.getKind()==ITE ){
     int pol = getEntailedCond( n, currCond );
     if( pol==1 ){
-      setEntailedCond( n[1], pol, currCond, new_cond );
+      setEntailedCond( n[1], pol, currCond, new_cond, conflict );
     }else if( pol==-1 ){
-      setEntailedCond( n[2], pol, currCond, new_cond );
+      setEntailedCond( n[2], pol, currCond, new_cond, conflict );
     }
   }
-  if( addEntailedCond( n, pol, currCond, new_cond ) ){
+  if( addEntailedCond( n, pol, currCond, new_cond, conflict ) ){
     if( n.getKind()==APPLY_TESTER ){
       const Datatype& dt = Datatype::datatypeOf(n.getOperator().toExpr());
       unsigned index = Datatype::indexOf(n.getOperator().toExpr());
@@ -543,14 +550,14 @@ void setEntailedCond( Node n, bool pol, std::map< Node, bool >& currCond, std::v
         for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
           if( i!=index ){
             Node t = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[i].getTester() ), n[0] );
-            addEntailedCond( t, false, currCond, new_cond );
+            addEntailedCond( t, false, currCond, new_cond, conflict );
           }
         }
       }else{
         if( dt.getNumConstructors()==2 ){
           int oindex = 1-index;
           Node t = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[oindex].getTester() ), n[0] );
-          addEntailedCond( t, true, currCond, new_cond );
+          addEntailedCond( t, true, currCond, new_cond, conflict );
         }
       }
     }
@@ -577,59 +584,100 @@ Node QuantifiersRewriter::computeProcessTerms( Node body, std::vector< Node >& n
 Node QuantifiersRewriter::computeProcessTerms2( Node body, bool hasPol, bool pol, std::map< Node, bool >& currCond, int nCurrCond,
                                                 std::map< Node, Node >& cache, std::map< Node, Node >& icache,
                                                 std::vector< Node >& new_vars, std::vector< Node >& new_conds ) {
+  Trace("quantifiers-rewrite-term-debug2") << "computeProcessTerms " << body << " " << hasPol << " " << pol << std::endl;
   Node ret;
   std::map< Node, Node >::iterator iti = cache.find( body );
   if( iti!=cache.end() ){
     ret = iti->second;
+    Trace("quantifiers-rewrite-term-debug2") << "Return (cached) " << ret << " for " << body << std::endl;
   }else{
-    bool do_ite = false;
-    //only do context dependent processing up to ITE depth 8
-    if( body.getKind()==ITE && nCurrCond<8 ){
-      do_ite = true;
-      nCurrCond = nCurrCond + 1;
-    }
+    bool firstTimeCD = true;
     bool changed = false;
     std::vector< Node > children;
     for( size_t i=0; i<body.getNumChildren(); i++ ){
       std::vector< Node > new_cond;
-      if( do_ite && i>0 ){
-        setEntailedCond( children[0], i==1, currCond, new_cond );
-        cache.clear();
+      bool conflict = false;
+      //only do context dependent processing up to depth 8
+      if( nCurrCond<8 ){
+        if( firstTimeCD ){
+          firstTimeCD = false;
+          nCurrCond = nCurrCond + 1;
+        }
+        if( Trace.isOn("quantifiers-rewrite-term-debug") ){
+          //if( ( body.getKind()==ITE && i>0 ) || ( hasPol && ( ( body.getKind()==OR && pol ) || (body.getKind()==AND && !pol ) ) ) ){
+          if( ( body.getKind()==ITE && i>0 ) || body.getKind()==OR || body.getKind()==AND ){
+            Trace("quantifiers-rewrite-term-debug") << "---rewrite " << body[i] << " under conditions:----" << std::endl;
+          }
+        }
+        if( body.getKind()==ITE && i>0 ){
+          setEntailedCond( children[0], i==1, currCond, new_cond, conflict );
+          //should not conflict (entailment check failed) 
+          Assert( !conflict );
+        }
+        //if( hasPol && ( ( body.getKind()==OR && pol ) || ( body.getKind()==AND && !pol ) ) ){
+        //  bool use_pol = !pol;
+        if( body.getKind()==OR || body.getKind()==AND ){
+          bool use_pol = body.getKind()==AND;
+          for( unsigned j=0; j<body.getNumChildren(); j++ ){
+            if( j<i ){
+              setEntailedCond( children[j], use_pol, currCond, new_cond, conflict );
+            }else if( j>i ){
+              setEntailedCond( body[j], use_pol, currCond, new_cond, conflict );
+            }
+          }
+          if( conflict ){
+            Trace("quantifiers-rewrite-term-debug") << "-------conflict, return " << !use_pol << std::endl;
+            ret = NodeManager::currentNM()->mkConst( !use_pol );
+          }
+        }
+        if( !new_cond.empty() ){
+          cache.clear();
+        }
+        if( Trace.isOn("quantifiers-rewrite-term-debug") ){
+          //if( ( body.getKind()==ITE && i>0 ) || ( hasPol && ( ( body.getKind()==OR && pol ) || (body.getKind()==AND && !pol ) ) ) ){
+          if( ( body.getKind()==ITE && i>0 ) || body.getKind()==OR || body.getKind()==AND ){      
+            Trace("quantifiers-rewrite-term-debug") << "-------" << std::endl;
+          }
+        }
       }
-      bool newHasPol;
-      bool newPol;
-      QuantPhaseReq::getPolarity( body, i, hasPol, pol, newHasPol, newPol );
-      Node nn = computeProcessTerms2( body[i], newHasPol, newPol, currCond, nCurrCond, cache, icache, new_vars, new_conds );
-      if( body.getKind()==ITE ){
-        if( i==0 ){
+      if( !conflict ){
+        bool newHasPol;
+        bool newPol;
+        QuantPhaseReq::getPolarity( body, i, hasPol, pol, newHasPol, newPol );
+        Node nn = computeProcessTerms2( body[i], newHasPol, newPol, currCond, nCurrCond, cache, icache, new_vars, new_conds );
+        if( body.getKind()==ITE && i==0 ){
           int res = getEntailedCond( nn, currCond );
+          Trace("quantifiers-rewrite-term-debug") << "Condition for " << body << " is " << nn << ", entailment check=" << res << std::endl;
           if( res==1 ){
             ret = computeProcessTerms2( body[1], hasPol, pol, currCond, nCurrCond, cache, icache, new_vars, new_conds );
-            break;
           }else if( res==-1 ){
             ret = computeProcessTerms2( body[2], hasPol, pol, currCond, nCurrCond, cache, icache, new_vars, new_conds );
-            break;
-          }
-        }else{
-          if( !new_cond.empty() ){
-            for( unsigned j=0; j<new_cond.size(); j++ ){
-              currCond.erase( new_cond[j] );
-            }
-            cache.clear();
           }
         }
+        children.push_back( nn );
+        changed = changed || nn!=body[i];
+      }
+      if( !new_cond.empty() ){
+        for( unsigned j=0; j<new_cond.size(); j++ ){
+          currCond.erase( new_cond[j] );
+        }
+        cache.clear();
+      }
+      if( !ret.isNull() ){
+        break;
       }
-      children.push_back( nn );
-      changed = changed || nn!=body[i];
     }
-    if( ret.isNull() && changed ){
-      if( body.getMetaKind() == kind::metakind::PARAMETERIZED ){
-        children.insert( children.begin(), body.getOperator() );
+    if( ret.isNull() ){
+      if( changed ){
+        if( body.getMetaKind() == kind::metakind::PARAMETERIZED ){
+          children.insert( children.begin(), body.getOperator() );
+        }
+        ret = NodeManager::currentNM()->mkNode( body.getKind(), children );
+      }else{
+        ret = body;
       }
-      ret = NodeManager::currentNM()->mkNode( body.getKind(), children );
-    }else{
-      ret = body;
     }
+    Trace("quantifiers-rewrite-term-debug2") << "Returning " << ret << " for " << body << std::endl;
     cache[body] = ret;
   }
 
@@ -1737,6 +1785,18 @@ Node QuantifiersRewriter::preSkolemizeQuantifiers( Node n, bool polarity, std::v
   return n;
 }
 
+Node QuantifiersRewriter::preprocess( Node n, bool isInst ) {
+  if( options::preSkolemQuant() ){
+    if( !isInst || !options::preSkolemQuantNested() ){
+      //apply pre-skolemization to existential quantifiers
+      Trace("quantifiers-preprocess-debug") << "Pre-skolemize " << n << "..." << std::endl;
+      std::vector< TypeNode > fvTypes;
+      std::vector< TNode > fvs;
+      n = quantifiers::QuantifiersRewriter::preSkolemizeQuantifiers( n, true, fvTypes, fvs );
+    }
+  }
+  return n;
+}
 
 Node QuantifiersRewriter::computePurify2( Node body, std::vector< Node >& args, std::map< Node, Node >& visited, std::map< Node, Node >& var_to_term,
                                           std::map< Node, std::vector< int > >& var_parent, int parentId ){
diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h
index 38c1bdd58..47997f9a7 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.h
+++ b/src/theory/quantifiers/quantifiers_rewriter.h
@@ -91,10 +91,12 @@ public:
 private:
   /** options */
   static bool doOperation( Node f, bool isNested, int computeOption );
+private:
+  static Node preSkolemizeQuantifiers(Node n, bool polarity, std::vector< TypeNode >& fvTypes, std::vector<TNode>& fvs);
 public:
   static Node rewriteRewriteRule( Node r );
   static bool containsQuantifiers(Node n);
-  static Node preSkolemizeQuantifiers(Node n, bool polarity, std::vector< TypeNode >& fvTypes, std::vector<TNode>& fvs);
+  static Node preprocess( Node n, bool isInst = false );
 };/* class QuantifiersRewriter */
 
 }/* CVC4::theory::quantifiers namespace */
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 8bc9689bd..560f68810 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -976,6 +976,16 @@ Node TermDb::mkSkolemizedBody( Node f, Node n, std::vector< TypeNode >& argTypes
   if( f.hasAttribute(InstLevelAttribute()) ){
     theory::QuantifiersEngine::setInstantiationLevelAttr( ret, f.getAttribute(InstLevelAttribute()) );
   }
+
+  if( Trace.isOn("quantifiers-sk") ){
+    Trace("quantifiers-sk") << "Skolemize : ";
+    for( unsigned i=0; i<sk.size(); i++ ){
+      Trace("quantifiers-sk") << sk[i] << " ";
+    }
+    Trace("quantifiers-sk") << "for " << std::endl;
+    Trace("quantifiers-sk") << "   " << f << std::endl;
+  }
+
   return ret;
 }
 
@@ -1002,14 +1012,6 @@ Node TermDb::getSkolemizedBody( Node f ){
         d_quantEngine->getTheoryEngine()->getSortInference()->setSkolemVar( f, f[0][i], d_skolem_constants[f][i] );
       }
     }
-    if( Trace.isOn("quantifiers-sk") ){
-      Trace("quantifiers-sk") << "Skolemize : ";
-      for( unsigned i=0; i<d_skolem_constants[f].size(); i++ ){
-        Trace("quantifiers-sk") << d_skolem_constants[f][i] << " ";
-      }
-      Trace("quantifiers-sk") << "for " << std::endl;
-      Trace("quantifiers-sk") << "   " << f << std::endl;
-    }
   }
   return d_skolem_body[ f ];
 }
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 19d66165a..6fedc14f0 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -695,6 +695,8 @@ bool QuantifiersEngine::addInstantiationInternal( Node f, std::vector< Node >& v
     Trace("quant-vts-debug") << "            ...result: " << body_r << std::endl;
     body = body_r;
   }
+  body = quantifiers::QuantifiersRewriter::preprocess( body, true );
+  Trace("inst-debug") << "...preprocess to " << body << std::endl;
   Trace("inst-assert") << "(assert " << body << ")" << std::endl;
   //make the lemma
   Node lem = NodeManager::currentNM()->mkNode( kind::OR, f.negate(), body );
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index d024e0270..0eff9bd5d 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -784,9 +784,6 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
         continue;
       }
       TypeNode t = TypeSet::getType(it);
-      if(t.isTuple() || t.isRecord()) {
-        t = NodeManager::currentNM()->getDatatypeForTupleRecord(t);
-      }
       
       //get properties of this type
       bool isCorecursive = false;
diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp
index 9fceedc96..3ed1c4d40 100644
--- a/src/theory/uf/theory_uf_strong_solver.cpp
+++ b/src/theory/uf/theory_uf_strong_solver.cpp
@@ -26,6 +26,7 @@
 //#define ONE_SPLIT_REGION
 //#define DISABLE_QUICK_CLIQUE_CHECKS
 //#define COMBINE_REGIONS_SMALL_INTO_LARGE
+//#define LAZY_REL_EQC
 
 using namespace std;
 using namespace CVC4;
@@ -406,7 +407,7 @@ void StrongSolverTheoryUF::SortModel::Region::debugPrint( const char* c, bool in
 StrongSolverTheoryUF::SortModel::SortModel( Node n, context::Context* c, context::UserContext* u, StrongSolverTheoryUF* thss ) : d_type( n.getType() ),
           d_thss( thss ), d_regions_index( c, 0 ), d_regions_map( c ), d_split_score( c ), d_disequalities_index( c, 0 ),
           d_reps( c, 0 ), d_conflict( c, false ), d_cardinality( c, 1 ), d_aloc_cardinality( u, 0 ),
-          d_cardinality_assertions( c ), d_hasCard( c, false ), d_maxNegCard( c, 0 ), d_initialized( u, false ){
+          d_cardinality_assertions( c ), d_hasCard( c, false ), d_maxNegCard( c, 0 ), d_initialized( u, false ), d_lemma_cache( u ){
   d_cardinality_term = n;
   //if( d_type.isSort() ){
   //  TypeEnumerator te(tn);
@@ -1070,11 +1071,12 @@ void StrongSolverTheoryUF::SortModel::allocateCardinality( OutputChannel* out ){
     //add splitting lemma for cardinality constraint
     Assert( !d_cardinality_term.isNull() );
     Node lem = getCardinalityLiteral( d_aloc_cardinality );
-    Trace("uf-ss-lemma") << "*** Cardinality split on : " << lem << std::endl;
     lem = NodeManager::currentNM()->mkNode( OR, lem, lem.notNode() );
     d_cardinality_lemma[ d_aloc_cardinality ] = lem;
     //add as lemma to output channel
-    out->lemma( lem );
+    if( doSendLemma( lem ) ){
+      Trace("uf-ss-lemma") << "*** Cardinality split on : " << lem << std::endl;
+    }
     //require phase
     out->requirePhase( d_cardinality_literal[ d_aloc_cardinality ], true );
     //add the appropriate lemma, propagate as decision
@@ -1121,7 +1123,6 @@ int StrongSolverTheoryUF::SortModel::addSplit( Region* r, OutputChannel* out ){
   if (!s.isNull() ){
     //add lemma to output channel
     Assert( s.getKind()==EQUAL );
-    Trace("uf-ss-lemma") << "*** Split on " << s << std::endl;
     Node ss = Rewriter::rewrite( s );
     if( ss.getKind()!=EQUAL ){
       Node b_t = NodeManager::currentNM()->mkConst( true );
@@ -1150,10 +1151,13 @@ int StrongSolverTheoryUF::SortModel::addSplit( Region* r, OutputChannel* out ){
     //Trace("uf-ss-lemma") << s[0].getType() << " " << s[1].getType() << std::endl;
     //Notice() << "*** Split on " << s << std::endl;
     //split on the equality s
-    out->split( ss );
-    //tell the sat solver to explore the equals branch first
-    out->requirePhase( ss, true );
-    ++( d_thss->d_statistics.d_split_lemmas );
+    Node lem = NodeManager::currentNM()->mkNode( kind::OR, ss, ss.negate() );
+    if( doSendLemma( lem ) ){
+      Trace("uf-ss-lemma") << "*** Split on " << s << std::endl;
+      //tell the sat solver to explore the equals branch first
+      out->requirePhase( ss, true );
+      ++( d_thss->d_statistics.d_split_lemmas );
+    }
     return 1;
   }else{
     return 0;
@@ -1185,9 +1189,10 @@ void StrongSolverTheoryUF::SortModel::addCliqueLemma( std::vector< Node >& cliqu
     }
     eqs.push_back( d_cardinality_literal[ d_cardinality ].notNode() );
     Node lem = NodeManager::currentNM()->mkNode( OR, eqs );
-    Trace("uf-ss-lemma") << "*** Add clique lemma " << lem << std::endl;
-    ++( d_thss->d_statistics.d_clique_lemmas );
-    out->lemma( lem );
+    if( doSendLemma( lem ) ){
+      Trace("uf-ss-lemma") << "*** Add clique lemma " << lem << std::endl;
+      ++( d_thss->d_statistics.d_clique_lemmas );
+    }
   }else{
     //found a clique
     Debug("uf-ss-cliques") << "Found a clique (cardinality=" << d_cardinality << ") :" << std::endl;
@@ -1303,9 +1308,10 @@ void StrongSolverTheoryUF::SortModel::addCliqueLemma( std::vector< Node >& cliqu
       //Assert( hasValue );
       //Assert( value );
       conflictNode = NodeManager::currentNM()->mkNode( IMPLIES, conflictNode, cardNode.notNode() );
-      Trace("uf-ss-lemma") << "*** Add clique lemma " << conflictNode << std::endl;
-      out->lemma( conflictNode );
-      ++( d_thss->d_statistics.d_clique_lemmas );
+      if( doSendLemma( conflictNode ) ){
+        Trace("uf-ss-lemma") << "*** Add clique lemma " << conflictNode << std::endl;
+        ++( d_thss->d_statistics.d_clique_lemmas );
+      }
     }
 
     //DO_THIS: ensure that the same clique is not reported???  Check standard effort after assertDisequal can produce same clique.
@@ -1364,10 +1370,9 @@ void StrongSolverTheoryUF::SortModel::addTotalityAxiom( Node n, int cardinality,
 }
 
 void StrongSolverTheoryUF::SortModel::addClique( int c, std::vector< Node >& clique ) {
-
-  if( d_clique_trie[c].add( clique ) ){
-    d_cliques[ c ].push_back( clique );
-  }
+  //if( d_clique_trie[c].add( clique ) ){
+  //  d_cliques[ c ].push_back( clique );
+  //}
 }
 
 
@@ -1395,6 +1400,16 @@ void StrongSolverTheoryUF::SortModel::simpleCheckCardinality() {
   }
 }
 
+bool StrongSolverTheoryUF::SortModel::doSendLemma( Node lem ) {
+  if( d_lemma_cache.find( lem )==d_lemma_cache.end() ){
+    d_lemma_cache[lem] = true;
+    d_thss->getOutputChannel().lemma( lem );
+    return true;
+  }else{
+    return false;
+  }
+}
+
 void StrongSolverTheoryUF::SortModel::debugPrint( const char* c ){
   Debug( c ) << "--  Conflict Find:" << std::endl;
   Debug( c ) << "Number of reps = " << d_reps << std::endl;
@@ -1568,10 +1583,19 @@ bool StrongSolverTheoryUF::hasEqc( Node a ) {
 }
 
 /** new node */
-void StrongSolverTheoryUF::newEqClass( Node n ){
-  SortModel* c = getSortModel( n );
+void StrongSolverTheoryUF::newEqClass( Node a ){
+  SortModel* c = getSortModel( a );
   if( c ){
+#ifdef LAZY_REL_EQC
     //do nothing
+#else
+    Trace("uf-ss-solver") << "StrongSolverTheoryUF: New eq class " << a << " : " << a.getType() << std::endl;
+    c->newEqClass( a );
+    if( options::ufssSymBreak() ){
+      d_sym_break->newEqClass( a );
+    }
+    Trace("uf-ss-solver") << "StrongSolverTheoryUF: Done New eq class." << std::endl;
+#endif
   }
 }
 
@@ -1580,6 +1604,7 @@ void StrongSolverTheoryUF::merge( Node a, Node b ){
   //TODO: ensure they are relevant
   SortModel* c = getSortModel( a );
   if( c ){
+#ifdef LAZY_REL_EQC
     ensureEqc( c, a );
     if( hasEqc( b ) ){
       Trace("uf-ss-solver") << "StrongSolverTheoryUF: Merge " << a << " " << b << " : " << a.getType() << std::endl;
@@ -1589,6 +1614,11 @@ void StrongSolverTheoryUF::merge( Node a, Node b ){
       //c->assignEqClass( b, a );
       d_rel_eqc[b] = true;
     }
+#else
+    Trace("uf-ss-solver") << "StrongSolverTheoryUF: Merge " << a << " " << b << " : " << a.getType() << std::endl;
+    c->merge( a, b );
+    Trace("uf-ss-solver") << "StrongSolverTheoryUF: Done Merge." << std::endl;
+#endif
   }else{
     if( options::ufssDiseqPropagation() ){
       d_deq_prop->merge(a, b);
@@ -1600,8 +1630,10 @@ void StrongSolverTheoryUF::merge( Node a, Node b ){
 void StrongSolverTheoryUF::assertDisequal( Node a, Node b, Node reason ){
   SortModel* c = getSortModel( a );
   if( c ){
+#ifdef LAZY_REL_EQC
     ensureEqc( c, a );
     ensureEqc( c, b );
+#endif
     Trace("uf-ss-solver") << "StrongSolverTheoryUF: Assert disequal " << a << " " << b << " : " << a.getType() << std::endl;
     //Assert( d_th->d_equalityEngine.getRepresentative( a )==a );
     //Assert( d_th->d_equalityEngine.getRepresentative( b )==b );
@@ -1617,7 +1649,9 @@ void StrongSolverTheoryUF::assertDisequal( Node a, Node b, Node reason ){
 /** assert a node */
 void StrongSolverTheoryUF::assertNode( Node n, bool isDecision ){
   Trace("uf-ss") << "Assert " << n << " " << isDecision << std::endl;
+#ifdef LAZY_REL_EQC
   ensureEqcRec( n );
+#endif
   bool polarity = n.getKind() != kind::NOT;
   TNode lit = polarity ? n : n[0];
   if( lit.getKind()==CARDINALITY_CONSTRAINT ){
@@ -2042,6 +2076,7 @@ void StrongSolverTheoryUF::allocateCombinedCardinality() {
   d_com_card_literal[ d_aloc_com_card.get() ] = lem;
   lem = NodeManager::currentNM()->mkNode( OR, lem, lem.notNode() );
   //add as lemma to output channel
+  Trace("uf-ss-lemma") << "*** Combined cardinality split : " << lem << std::endl;
   getOutputChannel().lemma( lem );
   //require phase
   getOutputChannel().requirePhase( d_com_card_literal[ d_aloc_com_card.get() ], true );
diff --git a/src/theory/uf/theory_uf_strong_solver.h b/src/theory/uf/theory_uf_strong_solver.h
index 24d7f840f..db4c50423 100644
--- a/src/theory/uf/theory_uf_strong_solver.h
+++ b/src/theory/uf/theory_uf_strong_solver.h
@@ -244,6 +244,8 @@ public:
     std::vector< Node > d_fresh_aloc_reps;
     /** whether we are initialized */
     context::CDO< bool > d_initialized;
+    /** cache for lemmas */
+    NodeBoolMap d_lemma_cache;
   private:
     /** apply totality */
     bool applyTotality( int cardinality );
@@ -251,6 +253,8 @@ public:
     Node getTotalityLemmaTerm( int cardinality, int i );
     /** simple check cardinality */
     void simpleCheckCardinality();
+  private:
+    bool doSendLemma( Node lem );
   public:
     SortModel( Node n, context::Context* c, context::UserContext* u, StrongSolverTheoryUF* thss );
     virtual ~SortModel(){}
diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am
index 1759d2924..350a948aa 100644
--- a/test/regress/regress0/datatypes/Makefile.am
+++ b/test/regress/regress0/datatypes/Makefile.am
@@ -69,7 +69,8 @@ TESTS =	\
 	cdt-model-cade15.smt2 \
 	sc-cdt1.smt2  \
 	conqueue-dt-enum-iloop.smt2 \
-	coda_simp_model.smt2
+	coda_simp_model.smt2 \
+	Test1-tup-mp.cvc
 
 FAILING_TESTS = \
 	datatype-dump.cvc
diff --git a/test/regress/regress0/datatypes/Test1-tup-mp.cvc b/test/regress/regress0/datatypes/Test1-tup-mp.cvc
new file mode 100644
index 000000000..6f49496f3
--- /dev/null
+++ b/test/regress/regress0/datatypes/Test1-tup-mp.cvc
@@ -0,0 +1,10 @@
+% EXPECT: sat
+TEST : TYPE = INT -> [INT, INT];
+
+test: TEST;
+
+ASSERT test(5) = (2, 3);
+ASSERT test(7) = (3, 4);
+
+CHECKSAT;
+
diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am
index 48b732f26..8cff980a5 100644
--- a/test/regress/regress0/fmf/Makefile.am
+++ b/test/regress/regress0/fmf/Makefile.am
@@ -50,7 +50,7 @@ TESTS =	\
 	loopy_coda.smt2 \
 	fmc_unsound_model.smt2 \
 	am-bad-model.cvc \
-	nun-0208-to.cvc
+	nun-0208-to.smt2
 
 
 EXTRA_DIST = $(TESTS)
diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am
index 3fff9b0de..df146752e 100644
--- a/test/regress/regress0/quantifiers/Makefile.am
+++ b/test/regress/regress0/quantifiers/Makefile.am
@@ -65,7 +65,12 @@ TESTS =	\
 	ext-ex-deq-trigger.smt2 \
 	matching-lia-1arg.smt2 \
 	RND_4_16.smt2 \
-  cdt-0208-to.smt2
+  cdt-0208-to.smt2 \
+  psyco-196.smt2 \
+  agg-rew-test.smt2 \
+  agg-rew-test-cf.smt2 \
+  rew-to-0211-dd.smt2 \
+  rew-to-scala.smt2
 
 
 # regression can be solved with --finite-model-find --fmf-inst-engine
diff --git a/test/regress/regress0/quantifiers/agg-rew-test-cf.smt2 b/test/regress/regress0/quantifiers/agg-rew-test-cf.smt2
new file mode 100644
index 000000000..44f475d83
--- /dev/null
+++ b/test/regress/regress0/quantifiers/agg-rew-test-cf.smt2
@@ -0,0 +1,5 @@
+(set-logic UFLIA)
+(set-info :status sat)
+(declare-fun Q (Int Int) Bool)
+(assert (forall ((x Int)) (or (and (or (Q 0 x) (Q 1 x)) (Q 2 x)) (not (Q 2 x)) (not (Q 1 x)))))
+(check-sat)
diff --git a/test/regress/regress0/quantifiers/agg-rew-test.smt2 b/test/regress/regress0/quantifiers/agg-rew-test.smt2
new file mode 100644
index 000000000..d1159278e
--- /dev/null
+++ b/test/regress/regress0/quantifiers/agg-rew-test.smt2
@@ -0,0 +1,5 @@
+(set-logic UFLIA)
+(set-info :status sat)
+(declare-fun Q (Int Int) Bool)
+(assert (forall ((x Int)) (=> (Q 0 x) (or (ite (Q 0 x) (not (Q 2 x)) (Q 3 x)) (Q 2 x)))))
+(check-sat)
diff --git a/test/regress/regress0/quantifiers/psyco-196.smt2 b/test/regress/regress0/quantifiers/psyco-196.smt2
new file mode 100644
index 000000000..356e62752
--- /dev/null
+++ b/test/regress/regress0/quantifiers/psyco-196.smt2
@@ -0,0 +1,420 @@
+(set-logic LIA)
+(set-info :status sat)
+(declare-fun W_S1_V5 () Bool)
+(declare-fun W_S1_V4 () Bool)
+(declare-fun W_S1_V6 () Bool)
+(declare-fun W_S1_V1 () Bool)
+(declare-fun W_S1_V3 () Bool)
+(declare-fun W_S1_V2 () Bool)
+(declare-fun R_S1_V5 () Bool)
+(declare-fun R_S1_V4 () Bool)
+(declare-fun R_S1_V6 () Bool)
+(declare-fun R_S1_V1 () Bool)
+(declare-fun R_S1_V3 () Bool)
+(declare-fun R_S1_V2 () Bool)
+(declare-fun R_E2_V1 () Bool)
+(declare-fun R_E1_V1 () Bool)
+(declare-fun R_E1_V3 () Bool)
+(declare-fun R_E2_V3 () Bool)
+(assert
+ (let
+ (($x62242
+   (forall
+    ((V2_0 Int) (V6_0 Int) 
+     (V4_0 Int) (V5_0 Int) 
+     (S1_V3_!5556 Int) (S1_V3_!5562 Int) 
+     (S1_V3_!5571 Int) (S1_V3_!5577 Int) 
+     (E1_!5552 Int) (E1_!5567 Int) 
+     (E1_!5569 Int) (S1_V2_!5555 Int) 
+     (S1_V2_!5561 Int) (S1_V2_!5570 Int) 
+     (S1_V2_!5576 Int) (S1_V5_!5560 Int) 
+     (S1_V5_!5566 Int) (S1_V5_!5575 Int) 
+     (S1_V5_!5581 Int) (S1_V4_!5559 Int) 
+     (S1_V4_!5565 Int) (S1_V4_!5574 Int) 
+     (S1_V4_!5580 Int) (S1_V6_!5558 Int) 
+     (S1_V6_!5564 Int) (S1_V6_!5573 Int) 
+     (S1_V6_!5579 Int) (E2_!5553 Int) 
+     (E2_!5554 Int) (E2_!5568 Int) 
+     (S1_V1_!5557 Int) (S1_V1_!5563 Int) 
+     (S1_V1_!5572 Int) (S1_V1_!5578 Int))
+    (let (($x59864 (= S1_V5_!5566 S1_V5_!5581)))
+    (let (($x59925 (not W_S1_V5)))
+    (let (($x62779 (or $x59925 $x59864)))
+    (let (($x62200 (= S1_V4_!5565 S1_V4_!5580)))
+    (let (($x59923 (not W_S1_V4)))
+    (let (($x62447 (or $x59923 $x62200)))
+    (let (($x62602 (= S1_V6_!5564 S1_V6_!5579)))
+    (let (($x62610 (not W_S1_V6)))
+    (let (($x62230 (or $x62610 $x62602)))
+    (let (($x61214 (= S1_V1_!5563 S1_V1_!5578)))
+    (let (($x60986 (= S1_V3_!5562 S1_V3_!5577)))
+    (let (($x62444 (= S1_V2_!5561 S1_V2_!5576)))
+    (let (($x62507 (not W_S1_V2)))
+    (let (($x62441 (or $x62507 $x62444)))
+    (let
+    (($x62532
+      (and $x62441
+      (ite W_S1_V3 $x60986
+      (= (ite W_S1_V3 S1_V3_!5556 E2_!5554) (+ (- 1) E2_!5568)))
+      (ite W_S1_V1 $x61214
+      (= E1_!5552 (+ 1 (ite W_S1_V1 S1_V1_!5572 E1_!5569)))) $x62230 $x62447
+      $x62779)))
+    (let ((?x62367 (ite W_S1_V1 S1_V1_!5572 E1_!5569)))
+    (let ((?x60865 (+ 1 ?x62367)))
+    (let ((?x62511 (ite W_S1_V1 S1_V1_!5578 ?x60865)))
+    (let ((?x60218 (ite W_S1_V3 S1_V3_!5556 E2_!5554)))
+    (let ((?x60222 (+ 1 ?x60218)))
+    (let ((?x62533 (ite W_S1_V3 S1_V3_!5562 ?x60222)))
+    (let
+    (($x62746
+      (and (not (<= V4_0 E2_!5553)) 
+      (not (<= V2_0 E1_!5552)) 
+      (not (<= V4_0 E2_!5554))
+      (not (<= (ite W_S1_V4 S1_V4_!5559 V4_0) ?x60222))
+      (>= ?x62533 (+ (- 1) (ite W_S1_V4 S1_V4_!5565 V4_0)))
+      (>= (ite W_S1_V1 S1_V1_!5563 E1_!5552)
+      (+ (- 1) (ite W_S1_V2 S1_V2_!5561 V2_0))) 
+      (not (<= V2_0 E1_!5567)) 
+      (not (<= V4_0 E2_!5568)) 
+      (not (<= V2_0 E1_!5569))
+      (not (<= (ite W_S1_V2 S1_V2_!5570 V2_0) ?x60865))
+      (>= ?x62511 (+ (- 1) (ite W_S1_V2 S1_V2_!5576 V2_0)))
+      (>= (ite W_S1_V3 S1_V3_!5577 E2_!5568)
+      (+ (- 1) (ite W_S1_V4 S1_V4_!5580 V4_0))))))
+    (let (($x62780 (= S1_V1_!5578 S1_V1_!5572)))
+    (let (($x161 (not R_S1_V5)))
+    (let (($x62589 (or $x161 (= (ite W_S1_V5 S1_V5_!5575 V5_0) V5_0))))
+    (let (($x159 (not R_S1_V4)))
+    (let (($x62548 (or $x159 (= (ite W_S1_V4 S1_V4_!5574 V4_0) V4_0))))
+    (let (($x157 (not R_S1_V6)))
+    (let (($x62737 (or $x157 (= (ite W_S1_V6 S1_V6_!5573 V6_0) V6_0))))
+    (let (($x153 (not R_S1_V3)))
+    (let
+    (($x62224 (or $x153 (= (ite W_S1_V3 S1_V3_!5571 E2_!5568) E2_!5568))))
+    (let (($x151 (not R_S1_V2)))
+    (let (($x62641 (or $x151 (= (ite W_S1_V2 S1_V2_!5570 V2_0) V2_0))))
+    (let
+    (($x60228
+      (and $x62641 $x62224 
+      (or (not R_S1_V1) (= ?x62367 (+ (- 1) E1_!5569))) $x62737 $x62548
+      $x62589)))
+    (let (($x62356 (not $x60228)))
+    (let (($x62680 (= S1_V1_!5578 S1_V1_!5563)))
+    (let (($x62272 (or $x161 $x59925 (= S1_V5_!5575 S1_V5_!5560))))
+    (let (($x61083 (= S1_V4_!5574 S1_V4_!5559)))
+    (let (($x62455 (or $x159 $x59923 $x61083)))
+    (let (($x60917 (= S1_V6_!5573 S1_V6_!5558)))
+    (let (($x62584 (or $x157 $x62610 $x60917)))
+    (let (($x59905 (= S1_V2_!5570 S1_V2_!5555)))
+    (let (($x62549 (or $x151 $x62507 $x59905)))
+    (let
+    (($x62675
+      (and $x62549 (or $x153 (= (ite W_S1_V3 S1_V3_!5571 E2_!5568) ?x60222))
+      (or (not R_S1_V1)
+      (= ?x62367 (+ (- 1) (ite W_S1_V1 S1_V1_!5557 E1_!5552)))) $x62584
+      $x62455 $x62272)))
+    (let (($x59892 (= S1_V1_!5578 S1_V1_!5557)))
+    (let
+    (($x60942 (or $x153 (= (ite W_S1_V3 S1_V3_!5571 E2_!5568) E2_!5554))))
+    (let
+    (($x62564
+      (and $x62641 $x60942 
+      (or (not R_S1_V1) (= ?x62367 (+ (- 1) E1_!5552))) $x62737 $x62548
+      $x62589)))
+    (let (($x59819 (not $x62564)))
+    (let (($x60234 (= S1_V1_!5563 S1_V1_!5572)))
+    (let (($x61232 (or $x161 (= (ite W_S1_V5 S1_V5_!5560 V5_0) V5_0))))
+    (let (($x61254 (or $x159 (= (ite W_S1_V4 S1_V4_!5559 V4_0) V4_0))))
+    (let (($x59994 (or $x157 (= (ite W_S1_V6 S1_V6_!5558 V6_0) V6_0))))
+    (let (($x155 (not R_S1_V1)))
+    (let
+    (($x62420 (or $x155 (= (ite W_S1_V1 S1_V1_!5557 E1_!5552) E1_!5569))))
+    (let (($x62368 (or $x151 (= (ite W_S1_V2 S1_V2_!5555 V2_0) V2_0))))
+    (let
+    (($x62830
+      (not
+      (and $x62368 (or $x153 (= ?x60218 (+ (- 1) E2_!5568))) $x62420 $x59994
+      $x61254 $x61232))))
+    (let (($x62636 (= S1_V1_!5563 S1_V1_!5557)))
+    (let
+    (($x59733 (or $x155 (= (ite W_S1_V1 S1_V1_!5557 E1_!5552) E1_!5552))))
+    (let
+    (($x62306
+      (not
+      (and $x62368 (or $x153 (= ?x60218 (+ (- 1) E2_!5554))) $x59733 $x59994
+      $x61254 $x61232))))
+    (let (($x60134 (= S1_V1_!5557 S1_V1_!5572)))
+    (let
+    (($x59719
+      (not
+      (and (or $x153 (= E2_!5554 E2_!5568)) (or $x155 (= E1_!5552 E1_!5569))))))
+    (let (($x61406 (= E2_!5554 E2_!5568)))
+    (let (($x59878 (not (or (not R_E2_V1) (= E1_!5552 E1_!5567)))))
+    (let (($x59949 (or $x59878 $x61406)))
+    (let (($x62775 (or $x59878 (= E2_!5553 E2_!5568))))
+    (let (($x59743 (= E2_!5553 E2_!5554)))
+    (let (($x62428 (= S1_V6_!5573 S1_V6_!5579)))
+    (let (($x60152 (or $x161 (= V5_0 (ite W_S1_V5 S1_V5_!5575 V5_0)))))
+    (let (($x60212 (or $x159 (= V4_0 (ite W_S1_V4 S1_V4_!5574 V4_0)))))
+    (let (($x61260 (or $x157 (= V6_0 (ite W_S1_V6 S1_V6_!5573 V6_0)))))
+    (let
+    (($x60887 (or $x153 (= E2_!5568 (ite W_S1_V3 S1_V3_!5571 E2_!5568)))))
+    (let (($x62275 (or $x151 (= V2_0 (ite W_S1_V2 S1_V2_!5570 V2_0)))))
+    (let
+    (($x61258
+      (or
+      (not
+      (and $x62275 $x60887 
+      (or $x155 (= E1_!5569 ?x60865)) $x61260 $x60212 $x60152)) $x62428)))
+    (let
+    (($x61266
+      (not
+      (and (or $x153 (= E2_!5568 E2_!5554)) (or $x155 (= E1_!5569 E1_!5552))))))
+    (let (($x61122 (= S1_V5_!5560 S1_V5_!5575)))
+    (let (($x59790 (or $x161 $x59925 $x61122)))
+    (let (($x62797 (or $x159 $x59923 (= S1_V4_!5559 S1_V4_!5574))))
+    (let (($x62684 (or $x157 $x62610 (= S1_V6_!5558 S1_V6_!5573))))
+    (let (($x62354 (or $x151 $x62507 (= S1_V2_!5555 S1_V2_!5570))))
+    (let
+    (($x60910
+      (and $x62354
+      (or $x153 (= ?x60218 (+ (- 1) (ite W_S1_V3 S1_V3_!5571 E2_!5568))))
+      (or $x155 (= (ite W_S1_V1 S1_V1_!5557 E1_!5552) ?x60865)) $x62684
+      $x62797 $x59790)))
+    (let (($x59844 (not $x60910)))
+    (let (($x62494 (= S1_V5_!5560 S1_V5_!5581)))
+    (let
+    (($x62623 (or $x153 (= E2_!5554 (ite W_S1_V3 S1_V3_!5571 E2_!5568)))))
+    (let
+    (($x61100
+      (or
+      (not
+      (and $x62275 $x62623 
+      (or $x155 (= E1_!5552 ?x60865)) $x61260 $x60212 $x60152)) $x62494)))
+    (let (($x60862 (= S1_V5_!5560 S1_V5_!5566)))
+    (let (($x62353 (or $x161 (= V5_0 (ite W_S1_V5 S1_V5_!5560 V5_0)))))
+    (let (($x60875 (or $x159 (= V4_0 (ite W_S1_V4 S1_V4_!5559 V4_0)))))
+    (let (($x62491 (or $x157 (= V6_0 (ite W_S1_V6 S1_V6_!5558 V6_0)))))
+    (let
+    (($x62399 (or $x155 (= E1_!5552 (ite W_S1_V1 S1_V1_!5557 E1_!5552)))))
+    (let (($x62431 (or $x151 (= V2_0 (ite W_S1_V2 S1_V2_!5555 V2_0)))))
+    (let
+    (($x62297
+      (or
+      (not
+      (and $x62431 (or $x153 (= E2_!5554 ?x60222)) $x62399 $x62491 $x60875
+      $x62353)) $x60862)))
+    (let (($x60874 (= S1_V2_!5570 S1_V2_!5576)))
+    (let
+    (($x62369
+      (or
+      (not
+      (and $x62275 $x60887 
+      (or $x155 (= E1_!5569 ?x60865)) $x61260 $x60212 $x60152)) $x60874)))
+    (let (($x62594 (= S1_V2_!5555 S1_V2_!5576)))
+    (let
+    (($x59910
+      (or
+      (not
+      (and $x62275 $x62623 
+      (or $x155 (= E1_!5552 ?x60865)) $x61260 $x60212 $x60152)) $x62594)))
+    (let (($x62531 (= E1_!5569 E1_!5567)))
+    (let (($x59835 (= E1_!5552 E1_!5569)))
+    (let (($x62312 (= E1_!5552 E1_!5567)))
+    (let
+    (($x62715
+      (and (or $x59719 (= S1_V3_!5556 S1_V3_!5571))
+      (or $x62306 (= S1_V3_!5562 S1_V3_!5556))
+      (or $x62830 (= S1_V3_!5562 S1_V3_!5571))
+      (or $x59819 (= S1_V3_!5577 S1_V3_!5556))
+      (or (not $x62675) (= S1_V3_!5577 S1_V3_!5562))
+      (or $x62356 (= S1_V3_!5577 S1_V3_!5571)) $x62312 $x59835 $x62531
+      $x59910 (or $x62306 (= S1_V2_!5561 S1_V2_!5555))
+      (or $x62830 (= S1_V2_!5561 S1_V2_!5570)) 
+      (or $x59844 $x62444) 
+      (or $x61266 $x59905) $x62369 $x62297 
+      (or $x59719 $x61122) $x61100 
+      (or $x62830 (= S1_V5_!5566 S1_V5_!5575)) 
+      (or $x59844 $x59864) 
+      (or $x62356 (= S1_V5_!5581 S1_V5_!5575))
+      (or $x62306 (= S1_V4_!5565 S1_V4_!5559))
+      (or $x62830 (= S1_V4_!5565 S1_V4_!5574)) 
+      (or $x59844 $x62200) 
+      (or $x61266 $x61083) 
+      (or $x59819 (= S1_V4_!5580 S1_V4_!5559))
+      (or $x62356 (= S1_V4_!5580 S1_V4_!5574))
+      (or $x62306 (= S1_V6_!5564 S1_V6_!5558))
+      (or $x62830 (= S1_V6_!5564 S1_V6_!5573)) 
+      (or $x59844 $x62602) 
+      (or $x61266 $x60917) $x61258 
+      (or $x59819 (= S1_V6_!5579 S1_V6_!5558)) $x59743 $x62775 $x59949
+      (or $x59719 $x60134) 
+      (or $x62306 $x62636) 
+      (or $x62830 $x60234) 
+      (or $x59819 $x59892) 
+      (or (not $x62675) $x62680) 
+      (or $x62356 $x62780)))) 
+    (or (not $x62715) (not $x62746) $x62532)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+ (let (($x13 (or W_S1_V2 W_S1_V3 W_S1_V1 W_S1_V6 W_S1_V4 W_S1_V5)))
+ (let (($x65 (not R_E1_V1)))
+ (let (($x63 (not R_E1_V3)))
+ (let (($x84 (not R_E2_V3))) (and $x84 $x63 $x65 $x13 $x62242)))))))
+(assert (not (and (not W_S1_V4) (not W_S1_V3))))
+(assert (not (and (not W_S1_V1) (not W_S1_V2))))
+(assert (not (and (not R_S1_V3) (not R_S1_V1) (not W_S1_V4) (not W_S1_V2))))
+(assert
+ (let (($x62714 (not W_S1_V3)))
+ (let (($x161 (not R_S1_V5)))
+ (let (($x159 (not R_S1_V4)))
+ (let (($x157 (not R_S1_V6)))
+ (let (($x155 (not R_S1_V1)))
+ (let (($x151 (not R_S1_V2)))
+ (not (and $x151 $x155 $x157 $x159 $x161 $x62714)))))))))
+(assert
+ (let (($x62610 (not W_S1_V6)))
+ (let (($x62507 (not W_S1_V2)))
+ (let (($x59925 (not W_S1_V5)))
+ (let (($x159 (not R_S1_V4)))
+ (let (($x155 (not R_S1_V1)))
+ (let (($x153 (not R_S1_V3)))
+ (not (and $x153 $x155 $x159 $x59925 $x62507 $x62610)))))))))
+(assert
+ (let (($x161 (not R_S1_V5)))
+ (let (($x159 (not R_S1_V4)))
+ (let (($x157 (not R_S1_V6)))
+ (let (($x155 (not R_S1_V1)))
+ (let (($x153 (not R_S1_V3)))
+ (let (($x151 (not R_S1_V2)))
+ (not (and $x151 $x153 $x155 $x157 $x159 $x161)))))))))
+(assert (not (and W_S1_V3 (not R_S1_V3) (not R_S1_V1) (not W_S1_V2))))
+(assert (not (and W_S1_V3 W_S1_V1 (not R_S1_V3) (not R_S1_V1))))
+(assert
+ (let (($x62232 (not W_S1_V1)))
+ (let (($x59925 (not W_S1_V5)))
+ (let (($x159 (not R_S1_V4)))
+ (let (($x157 (not R_S1_V6)))
+ (let (($x153 (not R_S1_V3)))
+ (let (($x151 (not R_S1_V2)))
+ (not (and $x151 $x153 $x157 $x159 $x59925 $x62232)))))))))
+(assert
+ (let (($x62610 (not W_S1_V6)))
+ (let (($x62232 (not W_S1_V1)))
+ (let (($x59925 (not W_S1_V5)))
+ (let (($x159 (not R_S1_V4)))
+ (let (($x153 (not R_S1_V3)))
+ (let (($x151 (not R_S1_V2)))
+ (not (and $x151 $x153 $x159 $x59925 $x62232 $x62610)))))))))
+(assert
+ (let (($x62610 (not W_S1_V6)))
+ (let (($x59923 (not W_S1_V4)))
+ (let (($x161 (not R_S1_V5)))
+ (let (($x155 (not R_S1_V1)))
+ (let (($x153 (not R_S1_V3)))
+ (let (($x151 (not R_S1_V2)))
+ (not (and $x151 $x153 $x155 $x161 $x59923 $x62610)))))))))
+(assert
+ (let (($x62610 (not W_S1_V6)))
+ (let (($x62232 (not W_S1_V1)))
+ (let (($x161 (not R_S1_V5)))
+ (let (($x159 (not R_S1_V4)))
+ (let (($x153 (not R_S1_V3)))
+ (let (($x151 (not R_S1_V2)))
+ (not (and $x151 $x153 $x159 $x161 $x62232 $x62610)))))))))
+(assert
+ (let (($x62232 (not W_S1_V1)))
+ (let (($x59925 (not W_S1_V5)))
+ (let (($x59923 (not W_S1_V4)))
+ (let (($x157 (not R_S1_V6)))
+ (let (($x153 (not R_S1_V3)))
+ (let (($x151 (not R_S1_V2)))
+ (not (and $x151 $x153 $x157 $x59923 $x59925 $x62232)))))))))
+(assert
+ (let (($x62610 (not W_S1_V6)))
+ (let (($x59925 (not W_S1_V5)))
+ (let (($x59923 (not W_S1_V4)))
+ (let (($x155 (not R_S1_V1)))
+ (let (($x153 (not R_S1_V3)))
+ (let (($x151 (not R_S1_V2)))
+ (not (and $x151 $x153 $x155 $x59923 $x59925 $x62610)))))))))
+(assert
+ (let (($x59923 (not W_S1_V4)))
+ (let (($x161 (not R_S1_V5)))
+ (let (($x157 (not R_S1_V6)))
+ (let (($x155 (not R_S1_V1)))
+ (let (($x153 (not R_S1_V3)))
+ (let (($x151 (not R_S1_V2)))
+ (not (and $x151 $x153 $x155 $x157 $x161 $x59923)))))))))
+(assert
+ (let (($x62232 (not W_S1_V1)))
+ (let (($x59923 (not W_S1_V4)))
+ (let (($x161 (not R_S1_V5)))
+ (let (($x157 (not R_S1_V6)))
+ (let (($x153 (not R_S1_V3)))
+ (let (($x151 (not R_S1_V2)))
+ (not (and $x151 $x153 $x157 $x161 $x59923 $x62232)))))))))
+(assert
+ (let (($x62714 (not W_S1_V3)))
+ (let (($x62507 (not W_S1_V2)))
+ (let (($x161 (not R_S1_V5)))
+ (let (($x159 (not R_S1_V4)))
+ (let (($x157 (not R_S1_V6)))
+ (let (($x155 (not R_S1_V1)))
+ (not (and $x155 $x157 $x159 $x161 $x62507 $x62714)))))))))
+(assert
+ (let (($x62714 (not W_S1_V3)))
+ (let (($x62610 (not W_S1_V6)))
+ (let (($x161 (not R_S1_V5)))
+ (let (($x159 (not R_S1_V4)))
+ (let (($x155 (not R_S1_V1)))
+ (let (($x151 (not R_S1_V2)))
+ (not (and $x151 $x155 $x159 $x161 $x62610 $x62714)))))))))
+(assert
+ (let (($x62714 (not W_S1_V3)))
+ (let (($x62610 (not W_S1_V6)))
+ (let (($x62507 (not W_S1_V2)))
+ (let (($x161 (not R_S1_V5)))
+ (let (($x159 (not R_S1_V4)))
+ (let (($x155 (not R_S1_V1)))
+ (not (and $x155 $x159 $x161 $x62507 $x62610 $x62714)))))))))
+(assert
+ (let (($x62714 (not W_S1_V3)))
+ (let (($x59925 (not W_S1_V5)))
+ (let (($x159 (not R_S1_V4)))
+ (let (($x157 (not R_S1_V6)))
+ (let (($x155 (not R_S1_V1)))
+ (let (($x151 (not R_S1_V2)))
+ (not (and $x151 $x155 $x157 $x159 $x59925 $x62714)))))))))
+(assert
+ (let (($x62714 (not W_S1_V3)))
+ (let (($x62507 (not W_S1_V2)))
+ (let (($x59925 (not W_S1_V5)))
+ (let (($x159 (not R_S1_V4)))
+ (let (($x157 (not R_S1_V6)))
+ (let (($x155 (not R_S1_V1)))
+ (not (and $x155 $x157 $x159 $x59925 $x62507 $x62714)))))))))
+(assert
+ (let (($x62714 (not W_S1_V3)))
+ (let (($x62610 (not W_S1_V6)))
+ (let (($x59925 (not W_S1_V5)))
+ (let (($x159 (not R_S1_V4)))
+ (let (($x155 (not R_S1_V1)))
+ (let (($x151 (not R_S1_V2)))
+ (not (and $x151 $x155 $x159 $x59925 $x62610 $x62714)))))))))
+(assert
+ (let (($x62714 (not W_S1_V3)))
+ (let (($x62610 (not W_S1_V6)))
+ (let (($x62507 (not W_S1_V2)))
+ (let (($x59925 (not W_S1_V5)))
+ (let (($x159 (not R_S1_V4)))
+ (let (($x155 (not R_S1_V1)))
+ (not (and $x155 $x159 $x59925 $x62507 $x62610 $x62714)))))))))
+(assert
+ (let (($x62232 (not W_S1_V1)))
+ (let (($x161 (not R_S1_V5)))
+ (let (($x159 (not R_S1_V4)))
+ (let (($x157 (not R_S1_V6)))
+ (let (($x153 (not R_S1_V3)))
+ (let (($x151 (not R_S1_V2)))
+ (not (and $x151 $x153 $x157 $x159 $x161 $x62232)))))))))
+(check-sat)
+
diff --git a/test/regress/regress0/quantifiers/rew-to-0211-dd.smt2 b/test/regress/regress0/quantifiers/rew-to-0211-dd.smt2
new file mode 100644
index 000000000..ec49231e3
--- /dev/null
+++ b/test/regress/regress0/quantifiers/rew-to-0211-dd.smt2
@@ -0,0 +1,259 @@
+(set-logic UFLIA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "industrial")
+(set-info :status unsat)
+(declare-fun boolIff (Int Int) Int)
+(declare-fun PeerGroupPlaceholder_ () Int)
+(declare-fun intGreater (Int Int) Int)
+(declare-fun IfThenElse_ (Int Int Int) Int)
+(declare-fun System.IConvertible () Int)
+(declare-fun CONCVARSYM (Int) Int)
+(declare-fun throwException_in () Int)
+(declare-fun SharingMode_Unshared_ () Int)
+(declare-fun System.Reflection.IReflect () Int)
+(declare-fun result_0_ () Int)
+(declare-fun block3502_2_block3553_correct () Int)
+(declare-fun int_m2147483648 () Int)
+(declare-fun local0_0 () Int)
+(declare-fun System.Int32 () Int)
+(declare-fun local0_1 () Int)
+(declare-fun block3536_2_block3553_correct () Int)
+(declare-fun block3553_correct () Int)
+(declare-fun intAtMost (Int Int) Int)
+(declare-fun multiply (Int Int) Int)
+(declare-fun Is_ (Int Int) Int)
+(declare-fun Smt.true () Int)
+(declare-fun ElementType_ (Int) Int)
+(declare-fun divide (Int Int) Int)
+(declare-fun int_m9223372036854775808 () Int)
+(declare-fun divides (Int Int) Int)
+(declare-fun stack0b_0 () Int)
+(declare-fun select1 (Int Int) Int)
+(declare-fun stack0b_1 () Int)
+(declare-fun store1 (Int Int Int) Int)
+(declare-fun select2 (Int Int Int) Int)
+(declare-fun nullObject () Int)
+(declare-fun store2 (Int Int Int Int) Int)
+(declare-fun false3451to3468_correct () Int)
+(declare-fun modulo (Int Int) Int)
+(declare-fun System.IComparable () Int)
+(declare-fun ownerRef_ () Int)
+(declare-fun StructSet_ (Int Int Int) Int)
+(declare-fun AsDirectSubClass (Int Int) Int)
+(declare-fun System.IEquatable_1...System.String () Int)
+(declare-fun System.Boolean () Int)
+(declare-fun shl_ (Int Int) Int)
+(declare-fun DimLength_ (Int Int) Int)
+(declare-fun anyEqual (Int Int) Int)
+(declare-fun System.Array () Int)
+(declare-fun block3451_correct () Int)
+(declare-fun System.Collections.Generic.IEnumerable_1...System.Char () Int)
+(declare-fun System.Reflection.ICustomAttributeProvider () Int)
+(declare-fun SharingMode_LockProtected_ () Int)
+(declare-fun IsMemberlessType_ (Int) Int)
+(declare-fun PartOfLine () Int)
+(declare-fun System.UInt16 () Int)
+(declare-fun false3434to3451_correct () Int)
+(declare-fun ClassRepr (Int) Int)
+(declare-fun System.Runtime.InteropServices._Type () Int)
+(declare-fun boolNot (Int) Int)
+(declare-fun Microsoft.Contracts.ICheckedException () Int)
+(declare-fun System.Exception () Int)
+(declare-fun System.Runtime.InteropServices._MemberInfo () Int)
+(declare-fun boolAnd (Int Int) Int)
+(declare-fun boolImplies (Int Int) Int)
+(declare-fun Unbox (Int) Int)
+(declare-fun intAtLeast (Int Int) Int)
+(declare-fun ownerFrame_ () Int)
+(declare-fun int_4294967295 () Int)
+(declare-fun IsAllocated (Int Int) Int)
+(declare-fun TypeName (Int) Int)
+(declare-fun AsPeerField (Int) Int)
+(declare-fun int_9223372036854775807 () Int)
+(declare-fun AsRepField (Int Int) Int)
+(declare-fun System.Reflection.MemberInfo () Int)
+(declare-fun ArrayCategoryValue_ () Int)
+(declare-fun is (Int Int) Int)
+(declare-fun Microsoft.Contracts.GuardException () Int)
+(declare-fun InRange (Int Int) Bool)
+(declare-fun AsOwner (Int Int) Int)
+(declare-fun System.Int64 () Int)
+(declare-fun System.Runtime.InteropServices._Exception () Int)
+(declare-fun or_ (Int Int) Int)
+(declare-fun As_ (Int Int) Int)
+(declare-fun exposeVersion_ () Int)
+(declare-fun true3434to3536_correct () Int)
+(declare-fun System.Type () Int)
+(declare-fun intLess (Int Int) Int)
+(declare-fun AsImmutable_ (Int) Int)
+(declare-fun NonNullFieldsAreInitialized_ () Int)
+(declare-fun block3417_correct () Int)
+(declare-fun LBound_ (Int Int) Int)
+(declare-fun System.Object () Int)
+(declare-fun System.UInt32 () Int)
+(declare-fun localinv_ () Int)
+(declare-fun inv_ () Int)
+(declare-fun Interval () Int)
+(declare-fun stack50000o_0 () Int)
+(declare-fun stack50000o_1 () Int)
+(declare-fun Heap_0_ () Int)
+(declare-fun entry_correct () Int)
+(declare-fun FirstConsistentOwner_ () Int)
+(declare-fun UnboxedType (Int) Int)
+(declare-fun AsRefField (Int Int) Int)
+(declare-fun System.Byte () Int)
+(declare-fun this () Int)
+(declare-fun stack1o_0 () Int)
+(declare-fun int_2147483647 () Int)
+(declare-fun ArrayCategoryRef_ () Int)
+(declare-fun Interval.a () Int)
+(declare-fun Interval.b () Int)
+(declare-fun stack1i_0 () Int)
+(declare-fun Heap_ () Int)
+(declare-fun Length_ (Int) Int)
+(declare-fun System.Runtime.Serialization.ISerializable () Int)
+(declare-fun AsNonNullRefField (Int Int) Int)
+(declare-fun IsHeap (Int) Int)
+(declare-fun Heap_1_ () Int)
+(declare-fun UBound_ (Int Int) Int)
+(declare-fun Cell () Int)
+(declare-fun System.String () Int)
+(declare-fun System.String.IsInterned_System.String_notnull_ (Int) Int)
+(declare-fun Rank_ (Int) Int)
+(declare-fun UnknownRef_ () Int)
+(declare-fun RefArraySet (Int Int Int) Int)
+(declare-fun ValueArraySet (Int Int Int) Int)
+(declare-fun stack50000o () Int)
+(declare-fun boolOr (Int Int) Int)
+(declare-fun sharingMode_ () Int)
+(declare-fun subtypes (Int Int) Bool)
+(declare-fun System.IComparable_1...System.String () Int)
+(declare-fun System.String.Equals_System.String_System.String_ (Int Int) Int)
+(declare-fun block3434_correct () Int)
+(declare-fun anyNeq (Int Int) Int)
+(declare-fun IsStaticField (Int) Int)
+(declare-fun SS_Display.Return.Local_0 () Int)
+(declare-fun IsNotNull_ (Int Int) Int)
+(declare-fun typeof_ (Int) Int)
+(declare-fun ArrayCategoryNonNullRef_ () Int)
+(declare-fun RefArrayGet (Int Int) Int)
+(declare-fun ValueArrayGet (Int Int) Int)
+(declare-fun TypeObject (Int) Int)
+(declare-fun and_ (Int Int) Int)
+(declare-fun BoxTester (Int Int) Int)
+(declare-fun Microsoft.Contracts.ObjectInvariantException () Int)
+(declare-fun block3468_correct () Int)
+(declare-fun IsValueType_ (Int) Int)
+(declare-fun Heap_2_ () Int)
+(declare-fun AsRangeField (Int Int) Int)
+(declare-fun System.SByte () Int)
+(declare-fun BeingConstructed_ () Int)
+(declare-fun block3502_correct () Int)
+(declare-fun FieldDependsOnFCO_ (Int Int Int) Int)
+(declare-fun NonNullRefArray (Int Int) Int)
+(declare-fun RefArray (Int Int) Int)
+(declare-fun ArrayCategory_ (Int) Int)
+(declare-fun stack0b () Int)
+(declare-fun Cell.Value () Int)
+(declare-fun AsPureObject_ (Int) Int)
+(declare-fun System.String.Equals_System.String_ (Int Int) Int)
+(declare-fun System.Int16 () Int)
+(declare-fun block3536_correct () Int)
+(declare-fun AsMutable_ (Int) Int)
+(declare-fun System.Char () Int)
+(declare-fun System.UInt64 () Int)
+(declare-fun StructGet_ (Int Int) Int)
+(declare-fun OneClassDown (Int Int) Int)
+(declare-fun ArrayIndex (Int Int Int Int) Int)
+(declare-fun stack0o_0 () Int)
+(declare-fun Box (Int Int) Int)
+(declare-fun stack0o_1 () Int)
+(declare-fun int_18446744073709551615 () Int)
+(declare-fun shr_ (Int Int) Int)
+(declare-fun stack0i_0 () Int)
+(declare-fun block3553_2_GeneratedUnifiedExit_correct () Int)
+(declare-fun System.ICloneable () Int)
+(declare-fun IsDirectlyModifiableField (Int) Int)
+(declare-fun StringLength_ (Int) Int)
+(declare-fun allocated_ () Int)
+(declare-fun BaseClass_ (Int) Int)
+(declare-fun ValueArray (Int Int) Int)
+(declare-fun Smt.false () Int)
+(declare-fun true3451to3502_correct () Int)
+(declare-fun IsImmutable_ (Int) Int)
+(declare-fun elements_ () Int)
+(declare-fun DeclType (Int) Int)
+(declare-fun System.Collections.IEnumerable () Int)
+(declare-fun ReallyLastGeneratedExit_correct () Int)
+(assert (forall ((?o Int) (?T Int)) (! (= (= (IsNotNull_ ?o ?T) Smt.true) (and (not (= ?o nullObject)) (= (Is_ ?o ?T) Smt.true))) :pattern ((IsNotNull_ ?o ?T)) )))
+(assert (forall ((?h Int) (?o Int) (?f Int) (?T Int)) (! (=> (and (= (IsHeap ?h) Smt.true) (not (= ?o nullObject)) (or (not (= ?o BeingConstructed_)) (= (= (select2 ?h BeingConstructed_ NonNullFieldsAreInitialized_) Smt.true) true))) (not (= (select2 ?h ?o (AsNonNullRefField ?f ?T)) nullObject))) :pattern ((select2 ?h ?o (AsNonNullRefField ?f ?T))) )))
+(assert (forall ((?o Int) (?T Int)) (! (=> (and (not (= ?o nullObject)) (not (= ?o BeingConstructed_)) (subtypes (typeof_ ?o) (AsImmutable_ ?T))) (forall ((?h Int)) (! (let ((?v_0 (typeof_ ?o))) (=> (= (IsHeap ?h) Smt.true) (and (= (select2 ?h ?o inv_) ?v_0) (= (select2 ?h ?o localinv_) ?v_0) (= (select2 ?h ?o ownerFrame_) PeerGroupPlaceholder_) (= (AsOwner ?o (select2 ?h ?o ownerRef_)) ?o) (forall ((?t Int)) (! (=> (= (AsOwner ?o (select2 ?h ?t ownerRef_)) ?o) (or (= ?t ?o) (not (= (select2 ?h ?t ownerFrame_) PeerGroupPlaceholder_)))) :pattern ((AsOwner ?o (select2 ?h ?t ownerRef_))) ))))) :pattern ((IsHeap ?h)) ))) :pattern ((subtypes (typeof_ ?o) (AsImmutable_ ?T))) )))
+(assert (= (IsValueType_ System.SByte) Smt.true))
+(assert (= (IsValueType_ System.Byte) Smt.true))
+(assert (= (IsValueType_ System.Int16) Smt.true))
+(assert (= (IsValueType_ System.UInt16) Smt.true))
+(assert (= (IsValueType_ System.Int32) Smt.true))
+(assert (= (IsValueType_ System.UInt32) Smt.true))
+(assert (= (IsValueType_ System.Int64) Smt.true))
+(assert (= (IsValueType_ System.UInt64) Smt.true))
+(assert (= (IsValueType_ System.Char) Smt.true))
+(assert (< int_m9223372036854775808 int_m2147483648))
+(assert (< int_m2147483648 (- 0 100000)))
+(assert (< 100000 int_2147483647))
+(assert (< int_2147483647 int_4294967295))
+(assert (< int_4294967295 int_9223372036854775807))
+(assert (< int_9223372036854775807 int_18446744073709551615))
+(assert (not (= (IsStaticField Cell.Value) Smt.true)))
+(assert (= (IsDirectlyModifiableField Cell.Value) Smt.true))
+(assert (= (DeclType Cell.Value) Cell))
+(assert (= (AsRangeField Cell.Value System.Int32) Cell.Value))
+(assert (not (= (IsStaticField Interval.a) Smt.true)))
+(assert (= (IsDirectlyModifiableField Interval.a) Smt.true))
+(assert (= (AsRepField Interval.a Interval) Interval.a))
+(assert (= (DeclType Interval.a) Interval))
+(assert (= (AsNonNullRefField Interval.a Cell) Interval.a))
+(assert (not (= (IsStaticField Interval.b) Smt.true)))
+(assert (= (IsDirectlyModifiableField Interval.b) Smt.true))
+(assert (= (AsRepField Interval.b Interval) Interval.b))
+(assert (= (DeclType Interval.b) Interval))
+(assert (= (AsNonNullRefField Interval.b Cell) Interval.b))
+(assert (subtypes Cell Cell))
+(assert (= (BaseClass_ Cell) System.Object))
+(assert (subtypes Cell (BaseClass_ Cell)))
+(assert (= (AsDirectSubClass Cell (BaseClass_ Cell)) Cell))
+(assert (not (= (IsImmutable_ Cell) Smt.true)))
+(assert (= (AsMutable_ Cell) Cell))
+(assert (subtypes System.Type System.Type))
+(assert (subtypes System.Reflection.MemberInfo System.Reflection.MemberInfo))
+(assert (= (BaseClass_ System.Reflection.MemberInfo) System.Object))
+(assert (subtypes System.Reflection.MemberInfo (BaseClass_ System.Reflection.MemberInfo)))
+(assert (= (AsDirectSubClass System.Reflection.MemberInfo (BaseClass_ System.Reflection.MemberInfo)) System.Reflection.MemberInfo))
+(assert (= (IsImmutable_ System.Reflection.MemberInfo) Smt.true))
+(assert (= (AsImmutable_ System.Reflection.MemberInfo) System.Reflection.MemberInfo))
+(assert (subtypes System.Reflection.ICustomAttributeProvider System.Object))
+(assert (= (IsMemberlessType_ System.Reflection.ICustomAttributeProvider) Smt.true))
+(assert (subtypes System.Reflection.MemberInfo System.Reflection.ICustomAttributeProvider))
+(assert (subtypes System.Runtime.InteropServices._MemberInfo System.Object))
+(assert (= (IsMemberlessType_ System.Runtime.InteropServices._MemberInfo) Smt.true))
+(assert (subtypes System.Reflection.MemberInfo System.Runtime.InteropServices._MemberInfo))
+(assert (= (IsMemberlessType_ System.Reflection.MemberInfo) Smt.true))
+(assert (= (BaseClass_ System.Type) System.Reflection.MemberInfo))
+(assert (subtypes System.Type (BaseClass_ System.Type)))
+(assert (= (AsDirectSubClass System.Type (BaseClass_ System.Type)) System.Type))
+(assert (= (IsImmutable_ System.Type) Smt.true))
+(assert (= (AsImmutable_ System.Type) System.Type))
+(assert (subtypes System.Runtime.InteropServices._Type System.Object))
+(assert (= (IsMemberlessType_ System.Runtime.InteropServices._Type) Smt.true))
+(assert (subtypes System.Type System.Runtime.InteropServices._Type))
+(assert (subtypes System.Reflection.IReflect System.Object))
+(assert (= (IsMemberlessType_ System.Reflection.IReflect) Smt.true))
+(assert (subtypes System.Type System.Reflection.IReflect))
+(assert (= (IsMemberlessType_ System.Type) Smt.true))
+(assert (subtypes PartOfLine PartOfLine))
+(assert (= (BaseClass_ PartOfLine) System.Object))
+(assert (subtypes PartOfLine (BaseClass_ PartOfLine)))
+(assert (= (AsDirectSubClass PartOfLine (BaseClass_ PartOfLine)) PartOfLine))
+(assert (distinct Smt.false Smt.true))
+(assert (let ((?v_0 (select2 Heap_ this ownerFrame_)) (?v_1 (select2 Heap_ this ownerRef_)) (?v_2 (not (= this nullObject))) (?v_3 (not (= stack0o_0 nullObject))) (?v_4 (not (= stack1o_0 nullObject))) (?v_5 (forall ((?o_ Int)) (=> (and (not (= ?o_ nullObject)) (= (= (select2 Heap_ ?o_ allocated_) Smt.true) true)) (and (= (select2 Heap_ ?o_ ownerRef_) (select2 Heap_2_ ?o_ ownerRef_)) (= (select2 Heap_ ?o_ ownerFrame_) (select2 Heap_2_ ?o_ ownerFrame_)))))) (?v_12 (=> true true)) (?v_6 (= ReallyLastGeneratedExit_correct Smt.true)) (?v_7 (= block3553_2_GeneratedUnifiedExit_correct Smt.true)) (?v_15 (= block3553_correct Smt.true)) (?v_14 (= throwException_in Smt.true)) (?v_8 (not (= stack50000o_0 nullObject))) (?v_11 (typeof_ stack50000o_0)) (?v_9 (select2 Heap_1_ stack50000o_0 ownerFrame_)) (?v_10 (select2 Heap_1_ stack50000o_0 ownerRef_)) (?v_13 (= block3468_correct Smt.true)) (?v_19 (= false3451to3468_correct Smt.true))) (let ((?v_21 (=> true ?v_15)) (?v_16 (= block3502_2_block3553_correct Smt.true)) (?v_17 (= block3502_correct Smt.true)) (?v_18 (= true3451to3502_correct Smt.true)) (?v_20 (= block3451_correct Smt.true)) (?v_25 (= false3434to3451_correct Smt.true)) (?v_22 (= block3536_2_block3553_correct Smt.true)) (?v_23 (= block3536_correct Smt.true)) (?v_24 (= true3434to3536_correct Smt.true)) (?v_26 (= block3434_correct Smt.true)) (?v_27 (= block3417_correct Smt.true)) (?v_28 (= entry_correct Smt.true))) (not (=> (=> (=> true (=> (= (IsHeap Heap_) Smt.true) (=> true (=> (= BeingConstructed_ nullObject) (=> (and (or (= ?v_0 PeerGroupPlaceholder_) (not (subtypes (select2 Heap_ ?v_1 inv_) ?v_0)) (= (select2 Heap_ ?v_1 localinv_) (BaseClass_ ?v_0))) (forall ((?pc_ Int)) (let ((?v_29 (typeof_ ?pc_))) (=> (and (not (= ?pc_ nullObject)) (= (= (select2 Heap_ ?pc_ allocated_) Smt.true) true) (= (select2 Heap_ ?pc_ ownerRef_) ?v_1) (= (select2 Heap_ ?pc_ ownerFrame_) ?v_0)) (and (= (select2 Heap_ ?pc_ inv_) ?v_29) (= (select2 Heap_ ?pc_ localinv_) ?v_29)))))) (=> true (=> true (=> (= (IsNotNull_ this Interval) Smt.true) (=> (= (= (select2 Heap_ this allocated_) Smt.true) true) (=> true (=> (=> (=> true (=> true (=> true (=> (=> (=> true (=> true (and ?v_2 (=> ?v_2 (=> (= stack0o_0 (select2 Heap_ this Interval.a)) (and ?v_3 (=> ?v_3 (=> (= stack0i_0 (select2 Heap_ stack0o_0 Cell.Value)) (and ?v_2 (=> ?v_2 (=> (= stack1o_0 (select2 Heap_ this Interval.b)) (and ?v_4 (=> ?v_4 (=> (= stack1i_0 (select2 Heap_ stack1o_0 Cell.Value)) (=> true (=> (and (=> (=> true (=> true (=> true (=> (=> (=> true (=> (= SS_Display.Return.Local_0 local0_0) (=> (= result_0_ local0_0) (=> (= stack50000o_1 stack50000o) (=> (= stack0b_1 local0_0) (=> (= stack0o_1 stack0o_0) (=> (= local0_1 local0_0) (=> (= Heap_2_ Heap_) (=> (=> (=> true (and ?v_5 (=> ?v_5 ?v_12))) ?v_6) ?v_6))))))))) ?v_7) ?v_7)))) ?v_15) (=> (=> true (=> true (=> (> stack0i_0 stack1i_0) (=> true (=> (=> (=> true (=> true (=> true (=> (and (=> (=> true (=> true (=> ?v_14 (=> true (=> (=> (=> true (=> true (=> false (=> (and (= (= (select2 Heap_ stack50000o_0 allocated_) Smt.true) false) ?v_8 (= ?v_11 Microsoft.Contracts.ObjectInvariantException)) (=> (and (= (select2 Heap_ stack50000o_0 ownerRef_) stack50000o_0) (= (select2 Heap_ stack50000o_0 ownerFrame_) PeerGroupPlaceholder_)) (=> (= Heap_0_ (store2 Heap_ stack50000o_0 allocated_ Smt.true)) (and ?v_8 (=> ?v_8 (=> (= (IsHeap Heap_1_) Smt.true) (=> (and (or (= ?v_9 PeerGroupPlaceholder_) (not (subtypes (select2 Heap_1_ ?v_10 inv_) ?v_9)) (= (select2 Heap_1_ ?v_10 localinv_) (BaseClass_ ?v_9))) (= (select2 Heap_1_ stack50000o_0 inv_) Microsoft.Contracts.ObjectInvariantException) (= (select2 Heap_1_ stack50000o_0 localinv_) ?v_11)) (=> (and (= ?v_10 (select2 Heap_0_ stack50000o_0 ownerRef_)) (= ?v_9 (select2 Heap_0_ stack50000o_0 ownerFrame_))) (=> (= (select2 Heap_1_ stack50000o_0 sharingMode_) SharingMode_Unshared_) (=> (forall ((?o_ Int)) (let ((?v_30 (typeof_ ?o_))) (=> (and (not (= ?o_ nullObject)) (= (= (select2 Heap_0_ ?o_ allocated_) Smt.true) (not true)) (= (= (select2 Heap_1_ ?o_ allocated_) Smt.true) true)) (and (= (select2 Heap_1_ ?o_ inv_) ?v_30) (= (select2 Heap_1_ ?o_ localinv_) ?v_30))))) (=> (forall ((?o_ Int)) (! (let ((?v_31 (select2 Heap_0_ ?o_ FirstConsistentOwner_))) (=> (= (select2 Heap_0_ ?v_31 exposeVersion_) (select2 Heap_1_ ?v_31 exposeVersion_)) (= ?v_31 (select2 Heap_1_ ?o_ FirstConsistentOwner_)))) :pattern ((select2 Heap_1_ ?o_ FirstConsistentOwner_)) )) (=> (forall ((?o_ Int)) (=> (and (not (= ?o_ nullObject)) (= (= (select2 Heap_0_ ?o_ allocated_) Smt.true) true)) (and (= (select2 Heap_0_ ?o_ ownerRef_) (select2 Heap_1_ ?o_ ownerRef_)) (= (select2 Heap_0_ ?o_ ownerFrame_) (select2 Heap_1_ ?o_ ownerFrame_))))) (=> (forall ((?o_ Int) (?f_ Int)) (! (let ((?v_32 (select2 Heap_0_ ?o_ ownerFrame_)) (?v_33 (select2 Heap_0_ ?o_ ownerRef_))) (=> (and (not (= ?f_ inv_)) (not (= ?f_ localinv_)) (not (= ?f_ FirstConsistentOwner_)) (or (not (= (IsStaticField ?f_) Smt.true)) (not (= (IsDirectlyModifiableField ?f_) Smt.true))) (not (= ?o_ nullObject)) (= (= (select2 Heap_0_ ?o_ allocated_) Smt.true) true) (or (= ?v_32 PeerGroupPlaceholder_) (not (subtypes (select2 Heap_0_ ?v_33 inv_) ?v_32)) (= (select2 Heap_0_ ?v_33 localinv_) (BaseClass_ ?v_32))) (or (not (= ?o_ stack50000o_0)) (not (subtypes Microsoft.Contracts.ObjectInvariantException (DeclType ?f_)))) true) (= (select2 Heap_0_ ?o_ ?f_) (select2 Heap_1_ ?o_ ?f_)))) :pattern ((select2 Heap_1_ ?o_ ?f_)) )) (=> (forall ((?o_ Int)) (or (= ?o_ stack50000o_0) (and (= (select2 Heap_0_ ?o_ inv_) (select2 Heap_1_ ?o_ inv_)) (= (select2 Heap_0_ ?o_ localinv_) (select2 Heap_1_ ?o_ localinv_))) (= (= (select2 Heap_0_ ?o_ allocated_) Smt.true) (not true)))) (=> (and (forall ((?o_ Int)) (=> (= (= (select2 Heap_0_ ?o_ allocated_) Smt.true) true) (= (= (select2 Heap_1_ ?o_ allocated_) Smt.true) true))) (forall ((?ot_ Int)) (let ((?v_34 (select2 Heap_0_ ?ot_ ownerFrame_))) (=> (and (= (= (select2 Heap_0_ ?ot_ allocated_) Smt.true) true) (not (= ?v_34 PeerGroupPlaceholder_))) (and (= (select2 Heap_1_ ?ot_ ownerRef_) (select2 Heap_0_ ?ot_ ownerRef_)) (= (select2 Heap_1_ ?ot_ ownerFrame_) ?v_34))))) (= (= (select2 Heap_0_ BeingConstructed_ NonNullFieldsAreInitialized_) Smt.true) (= (select2 Heap_1_ BeingConstructed_ NonNullFieldsAreInitialized_) Smt.true))) (=> (forall ((?o_ Int)) (or (= ?o_ stack50000o_0) (= (select2 Heap_0_ ?o_ sharingMode_) (select2 Heap_1_ ?o_ sharingMode_)))) (and ?v_8 (=> ?v_8 (=> false (=> true ?v_12))))))))))))))))))))))) ?v_13) ?v_13))))) ?v_19) (=> (=> true (=> true (=> (not ?v_14) (=> true (=> (=> (=> true (=> true (=> true (=> (=> (=> true (=> (= stack0b_0 throwException_in) (=> (= local0_0 Smt.false) ?v_21))) ?v_16) ?v_16)))) ?v_17) ?v_17))))) ?v_18)) (and ?v_18 ?v_19))))) ?v_20) ?v_20))))) ?v_25) (=> (=> true (=> true (=> (<= stack0i_0 stack1i_0) (=> true (=> (=> (=> true (=> true (=> true (=> (=> (=> true (=> (= stack0b_0 stack0b) (=> (= local0_0 Smt.true) ?v_21))) ?v_22) ?v_22)))) ?v_23) ?v_23))))) ?v_24)) (and ?v_24 ?v_25))))))))))))))))) ?v_26) ?v_26)))) ?v_27) ?v_27))))))))))) ?v_28) ?v_28)))))
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/quantifiers/rew-to-scala.smt2 b/test/regress/regress0/quantifiers/rew-to-scala.smt2
new file mode 100644
index 000000000..1e29241eb
--- /dev/null
+++ b/test/regress/regress0/quantifiers/rew-to-scala.smt2
@@ -0,0 +1,13 @@
+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+(declare-datatypes () ((Formula!953 (And!954 (lhs!955 Formula!953) (rhs!956 Formula!953)) (Not!957 (f!958 Formula!953)) (Or!959 (lhs!960 Formula!953) (rhs!961 Formula!953)) (Variable!962 (id!963 (_ BitVec 32))))
+))
+(declare-fun error_value!964 () Bool)
+(declare-fun isNNF!208 (Formula!953) Bool)
+(declare-fun error_value!965 () Formula!953)
+(declare-fun nnf!206 (Formula!953) Formula!953)
+(declare-fun error_value!966 () Formula!953)
+(assert (forall ((f!207 Formula!953)) (= (isNNF!208 f!207) (ite (is-And!954 f!207) (and (and (isNNF!208 (lhs!955 f!207)) (isNNF!208 (lhs!955 f!207))) (isNNF!208 (rhs!956 f!207))) (ite (is-Or!959 f!207) (and (and (isNNF!208 (lhs!960 f!207)) (isNNF!208 (lhs!960 f!207))) (isNNF!208 (rhs!961 f!207))) (ite (is-Not!957 f!207) false (ite (is-Variable!962 f!207) true error_value!964))))) ))
+(assert (forall ((formula!205 Formula!953)) (= (nnf!206 formula!205) (ite (is-And!954 formula!205) (And!954 (nnf!206 (lhs!955 formula!205)) (nnf!206 (rhs!956 formula!205))) (ite (is-Or!959 formula!205) (Or!959 (nnf!206 (lhs!960 formula!205)) (nnf!206 (rhs!961 formula!205))) (ite (and (and (is-Not!957 formula!205) (is-Not!957 formula!205)) (is-And!954 (f!958 formula!205))) (Or!959 (nnf!206 (Not!957 (lhs!955 (f!958 formula!205)))) (nnf!206 (Not!957 (rhs!956 (f!958 formula!205))))) (ite (and (and (is-Not!957 formula!205) (is-Not!957 formula!205)) (is-Or!959 (f!958 formula!205))) (And!954 (nnf!206 (Not!957 (lhs!960 (f!958 formula!205)))) (nnf!206 (Not!957 (rhs!961 (f!958 formula!205))))) (ite (and (and (is-Not!957 formula!205) (is-Not!957 formula!205)) (is-Not!957 (f!958 formula!205))) (nnf!206 (f!958 (f!958 formula!205))) (ite (is-Not!957 formula!205) formula!205 (ite (is-Variable!962 formula!205) formula!205 error_value!965)))))))) ))
+(assert (exists ((formula!205 Formula!953)) (not (=> (is-Variable!962 formula!205) (isNNF!208 (ite (is-And!954 formula!205) (And!954 (nnf!206 (lhs!955 formula!205)) (nnf!206 (rhs!956 formula!205))) (ite (is-Or!959 formula!205) (Or!959 (nnf!206 (lhs!960 formula!205)) (nnf!206 (rhs!961 formula!205))) (ite (and (and (is-Not!957 formula!205) (is-Not!957 formula!205)) (is-And!954 (f!958 formula!205))) (Or!959 (nnf!206 (Not!957 (lhs!955 (f!958 formula!205)))) (nnf!206 (Not!957 (rhs!956 (f!958 formula!205))))) (ite (and (and (is-Not!957 formula!205) (is-Not!957 formula!205)) (is-Or!959 (f!958 formula!205))) (And!954 (nnf!206 (Not!957 (lhs!960 (f!958 formula!205)))) (nnf!206 (Not!957 (rhs!961 (f!958 formula!205))))) (ite (and (and (is-Not!957 formula!205) (is-Not!957 formula!205)) (is-Not!957 (f!958 formula!205))) (nnf!206 (f!958 (f!958 formula!205))) (ite (is-Not!957 formula!205) formula!205 (ite (is-Variable!962 formula!205) formula!205 error_value!966)))))))))) ))
+(check-sat)
diff --git a/test/unit/expr/expr_manager_public.h b/test/unit/expr/expr_manager_public.h
index 040bd7161..17efaf2a5 100644
--- a/test/unit/expr/expr_manager_public.h
+++ b/test/unit/expr/expr_manager_public.h
@@ -123,7 +123,7 @@ public:
 
   void testMkAssociativeBadKind() {
     std::vector<Expr> vars = mkVars(d_exprManager->integerType(), 10);
-    TS_ASSERT_THROWS( d_exprManager->mkAssociative(TUPLE,vars), IllegalArgumentException);
+    TS_ASSERT_THROWS( d_exprManager->mkAssociative(LEQ,vars), IllegalArgumentException);
   }
 
 };