Partial merge from kind-backend branch, including Minisat and CNF work to

support incrementality.

Some clean-up work will likely follow, but the CNF/Minisat stuff should be
left pretty much untouched.

Expected performance change negligible; slightly better on memory:
  http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3705&reference_id=3697&mode=&category=&p=5
Note that there are crashes, but that these are exhibited in the nightly
regression run too!

85 files changed, 3013 insertions, 416 deletions

diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp
index a30ccb27d..83c33c7ab 100644
--- a/src/compat/cvc3_compat.cpp
+++ b/src/compat/cvc3_compat.cpp
@@ -25,6 +25,8 @@
 #include "util/integer.h"
 #include "util/bitvector.h"
 #include "util/hash.h"
+#include "util/subrange_bound.h"
+#include "util/predicate.h"
 
 #include "parser/parser.h"
 #include "parser/parser_builder.h"
@@ -184,7 +186,7 @@ bool Type::isBool() const {
 }
 
 bool Type::isSubtype() const {
-  return false;
+  return isPredicateSubtype();
 }
 
 Cardinality Type::card() const {
@@ -980,11 +982,21 @@ Type ValidityChecker::intType() {
 }
 
 Type ValidityChecker::subrangeType(const Expr& l, const Expr& r) {
-  Unimplemented("Subranges not supported by CVC4 yet (sorry!)");
+  bool noLowerBound = l.getType().isString() && l.getConst<string>() == "_NEGINF";
+  bool noUpperBound = r.getType().isString() && r.getConst<string>() == "_POSINF";
+  CheckArgument(noLowerBound || l.getKind() == CVC4::kind::CONST_INTEGER, l);
+  CheckArgument(noUpperBound || r.getKind() == CVC4::kind::CONST_INTEGER, r);
+  CVC4::SubrangeBound bl = noLowerBound ? CVC4::SubrangeBound() : CVC4::SubrangeBound(l.getConst<Integer>());
+  CVC4::SubrangeBound br = noUpperBound ? CVC4::SubrangeBound() : CVC4::SubrangeBound(r.getConst<Integer>());
+  return d_em->mkSubrangeType(CVC4::SubrangeBounds(bl, br));
 }
 
 Type ValidityChecker::subtypeType(const Expr& pred, const Expr& witness) {
-  Unimplemented("Predicate subtyping not supported by CVC4 yet (sorry!)");
+  if(witness.isNull()) {
+    return d_em->mkPredicateSubtype(pred);
+  } else {
+    return d_em->mkPredicateSubtype(pred, witness);
+  }
 }
 
 Type ValidityChecker::tupleType(const Type& type0, const Type& type1) {
@@ -1172,15 +1184,29 @@ Type ValidityChecker::getType(const Expr& e) {
 }
 
 Type ValidityChecker::getBaseType(const Expr& e) {
-  Type t = d_em->getType(e);
-  return t.isInteger() ? Type(d_em->realType()) : t;
+  return getBaseType(e.getType());
 }
 
 Type ValidityChecker::getBaseType(const Type& t) {
-  return t.isInteger() ? Type(d_em->realType()) : t;
+  Type type = t;
+  while(type.isPredicateSubtype()) {
+    type = CVC4::PredicateSubtype(type).getBaseType();
+  }
+  // We might still be a (primitive) subtype.  Check the types that can
+  // form the base of such a type.
+  if(type.isReal()) {
+    return d_em->realType();
+  }
+  Assert(!type.isInteger());// should be handled by Real
+  if(type.isBoolean()) {
+    return d_em->booleanType();
+  }
+  return type;
 }
 
 Expr ValidityChecker::getTypePred(const Type&t, const Expr& e) {
+  // This function appears to be TCC-related---it doesn't just get the pred of a
+  // subtype predicate, but returns a predicate describing the type.
   Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
 }
 
@@ -1189,42 +1215,52 @@ Expr ValidityChecker::stringExpr(const std::string& str) {
 }
 
 Expr ValidityChecker::idExpr(const std::string& name) {
-  Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
+  // represent as a string expr, CVC4 doesn't have id exprs
+  return d_em->mkConst(name);
 }
 
 Expr ValidityChecker::listExpr(const std::vector<Expr>& kids) {
-  Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
+  // list exprs aren't supported by CVC4; make a tuple if two or more
+  CheckArgument(kids.size() > 0, kids);
+  return (kids.size() == 1) ? kids[0] : Expr(d_em->mkExpr(CVC4::kind::TUPLE, vector<CVC4::Expr>(kids.begin(), kids.end())));
 }
 
 Expr ValidityChecker::listExpr(const Expr& e1) {
-  Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
+  // list exprs aren't supported by CVC4; just return e1
+  return e1;
 }
 
 Expr ValidityChecker::listExpr(const Expr& e1, const Expr& e2) {
-  Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
+  // list exprs aren't supported by CVC4; just return a tuple
+  return d_em->mkExpr(CVC4::kind::TUPLE, e1, e2);
 }
 
 Expr ValidityChecker::listExpr(const Expr& e1, const Expr& e2, const Expr& e3) {
-  Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
+  // list exprs aren't supported by CVC4; just return a tuple
+  return d_em->mkExpr(CVC4::kind::TUPLE, e1, e2, e3);
 }
 
 Expr ValidityChecker::listExpr(const std::string& op,
                                const std::vector<Expr>& kids) {
-  Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
+  // list exprs aren't supported by CVC4; just return a tuple
+  return d_em->mkExpr(CVC4::kind::TUPLE, d_em->mkConst(op), vector<CVC4::Expr>(kids.begin(), kids.end()));
 }
 
 Expr ValidityChecker::listExpr(const std::string& op, const Expr& e1) {
-  Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
+  // list exprs aren't supported by CVC4; just return a tuple
+  return d_em->mkExpr(CVC4::kind::TUPLE, d_em->mkConst(op), e1);
 }
 
 Expr ValidityChecker::listExpr(const std::string& op, const Expr& e1,
                                const Expr& e2) {
-  Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
+  // list exprs aren't supported by CVC4; just return a tuple
+  return d_em->mkExpr(CVC4::kind::TUPLE, d_em->mkConst(op), e1, e2);
 }
 
 Expr ValidityChecker::listExpr(const std::string& op, const Expr& e1,
                                const Expr& e2, const Expr& e3) {
-  Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
+  // list exprs aren't supported by CVC4; just return a tuple
+  return d_em->mkExpr(CVC4::kind::TUPLE, d_em->mkConst(op), e1, e2, e3);
 }
 
 void ValidityChecker::printExpr(const Expr& e) {
@@ -1340,7 +1376,12 @@ Op ValidityChecker::createOp(const std::string& name, const Type& type) {
 
 Op ValidityChecker::createOp(const std::string& name, const Type& type,
                              const Expr& def) {
-  Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
+  CheckArgument(def.getType() == type, type,
+      "Type mismatch in ValidityChecker::createOp(): `%s' defined to an "
+      "expression of type %s but ascribed as type %s", name.c_str(),
+      def.getType().toString().c_str(), type.toString().c_str());
+  d_parserContext->defineFunction(name, def);
+  return def;
 }
 
 Op ValidityChecker::lookupOp(const std::string& name, Type* type) {
diff --git a/src/context/context.cpp b/src/context/context.cpp
index 2b220d5b4..abb1575d4 100644
--- a/src/context/context.cpp
+++ b/src/context/context.cpp
@@ -62,7 +62,7 @@ Context::~Context() throw(AssertionException) {
 
 void Context::push() {
   Trace("pushpop") << std::string(2 * getLevel(), ' ') << "Push [to "
-                   << getLevel() + 1 << "] {" << std::endl;
+                   << getLevel() + 1 << "] { " << this << std::endl;
 
   // Create a new memory region
   d_pCMM->push();
@@ -106,7 +106,7 @@ void Context::pop() {
   }
 
   Trace("pushpop") << std::string(2 * getLevel(), ' ') << "} Pop [to "
-                   << getLevel() << "]" << std::endl;
+                   << getLevel() << "] " << this << std::endl;
 }
 
 
diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index 8d089901b..3dac28e11 100644
--- a/src/expr/command.cpp
+++ b/src/expr/command.cpp
@@ -494,10 +494,14 @@ Expr DefineFunctionCommand::getFormula() const throw() {
 
 void DefineFunctionCommand::invoke(SmtEngine* smtEngine) throw() {
   //Dump("declarations") << *this << endl; -- done by SmtEngine
-  if(!d_func.isNull()) {
-    smtEngine->defineFunction(d_func, d_formals, d_formula);
+  try {
+    if(!d_func.isNull()) {
+      smtEngine->defineFunction(d_func, d_formals, d_formula);
+    }
+    d_commandStatus = CommandSuccess::instance();
+  } catch(exception& e) {
+    d_commandStatus = new CommandFailure(e.what());
   }
-  d_commandStatus = CommandSuccess::instance();
 }
 
 Command* DefineFunctionCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 46a7bb82c..533a4dd7f 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -97,24 +97,33 @@ ExprManager::ExprManager(const Options& options) :
 #endif
 }
 
-ExprManager::~ExprManager() {
-#ifdef CVC4_STATISTICS_ON
+ExprManager::~ExprManager() throw() {
   NodeManagerScope nms(d_nodeManager);
-  for (unsigned i = 0; i < kind::LAST_KIND; ++ i) {
-    if (d_exprStatistics[i] != NULL) {
-      StatisticsRegistry::unregisterStat(d_exprStatistics[i]);
-      delete d_exprStatistics[i];
+
+  try {
+
+#ifdef CVC4_STATISTICS_ON
+    for (unsigned i = 0; i < kind::LAST_KIND; ++ i) {
+      if (d_exprStatistics[i] != NULL) {
+        StatisticsRegistry::unregisterStat(d_exprStatistics[i]);
+        delete d_exprStatistics[i];
+      }
     }
-  }
-  for (unsigned i = 0; i <= LAST_TYPE; ++ i) {
-    if (d_exprStatisticsVars[i] != NULL) {
-      StatisticsRegistry::unregisterStat(d_exprStatisticsVars[i]);
-      delete d_exprStatisticsVars[i];
+    for (unsigned i = 0; i <= LAST_TYPE; ++ i) {
+      if (d_exprStatisticsVars[i] != NULL) {
+        StatisticsRegistry::unregisterStat(d_exprStatisticsVars[i]);
+        delete d_exprStatisticsVars[i];
+      }
     }
-  }
 #endif
-  delete d_nodeManager;
-  delete d_ctxt;
+
+    delete d_nodeManager;
+    delete d_ctxt;
+
+  } catch(Exception& e) {
+    Warning() << "CVC4 threw an exception during cleanup." << std::endl
+              << e << std::endl;
+  }
 }
 
 const Options* ExprManager::getOptions() const {
@@ -697,6 +706,39 @@ SortConstructorType ExprManager::mkSortConstructor(const std::string& name,
               new TypeNode(d_nodeManager->mkSortConstructor(name, arity))));
 }
 
+Type ExprManager::mkPredicateSubtype(Expr lambda)
+  throw(TypeCheckingException) {
+  NodeManagerScope nms(d_nodeManager);
+  try {
+    return PredicateSubtype(Type(d_nodeManager,
+                new TypeNode(d_nodeManager->mkPredicateSubtype(lambda))));
+  } catch (const TypeCheckingExceptionPrivate& e) {
+    throw TypeCheckingException(this, &e);
+  }
+}
+
+Type ExprManager::mkPredicateSubtype(Expr lambda, Expr witness)
+  throw(TypeCheckingException) {
+  NodeManagerScope nms(d_nodeManager);
+  try {
+    return PredicateSubtype(Type(d_nodeManager,
+                new TypeNode(d_nodeManager->mkPredicateSubtype(lambda, witness))));
+  } catch (const TypeCheckingExceptionPrivate& e) {
+    throw TypeCheckingException(this, &e);
+  }
+}
+
+Type ExprManager::mkSubrangeType(const SubrangeBounds& bounds)
+  throw(TypeCheckingException) {
+  NodeManagerScope nms(d_nodeManager);
+  try {
+    return SubrangeType(Type(d_nodeManager,
+                new TypeNode(d_nodeManager->mkSubrangeType(bounds))));
+  } catch (const TypeCheckingExceptionPrivate& e) {
+    throw TypeCheckingException(this, &e);
+  }
+}
+
 /**
  * Get the type for the given Expr and optionally do type checking.
  *
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index 2abd05821..bf9bfbb38 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -26,6 +26,7 @@
 #include "expr/kind.h"
 #include "expr/type.h"
 #include "expr/expr.h"
+#include "util/subrange_bound.h"
 
 ${includes}
 
@@ -33,7 +34,7 @@ ${includes}
 // compiler directs the user to the template file instead of the
 // generated one.  We don't want the user to modify the generated one,
 // since it'll get overwritten on a later build.
-#line 37 "${template}"
+#line 38 "${template}"
 
 namespace CVC4 {
 
@@ -119,7 +120,7 @@ public:
    * any expression references that used to be managed by this expression
    * manager and are left-over are bad.
    */
-  ~ExprManager();
+  ~ExprManager() throw();
 
   /** Get this node manager's options */
   const Options* getOptions() const;
@@ -403,9 +404,34 @@ public:
   SortConstructorType mkSortConstructor(const std::string& name,
                                         size_t arity) const;
 
+  /**
+   * Make a predicate subtype type defined by the given LAMBDA
+   * expression.  A TypeCheckingException can be thrown if lambda is
+   * not a LAMBDA, or is ill-typed, or if CVC4 fails at proving that
+   * the resulting predicate subtype is inhabited.
+   */
+  Type mkPredicateSubtype(Expr lambda)
+    throw(TypeCheckingException);
+
+  /**
+   * Make a predicate subtype type defined by the given LAMBDA
+   * expression and whose non-emptiness is witnessed by the given
+   * witness.  A TypeCheckingException can be thrown if lambda is not
+   * a LAMBDA, or is ill-typed, or if the witness is not a witness or
+   * ill-typed.
+   */
+  Type mkPredicateSubtype(Expr lambda, Expr witness)
+    throw(TypeCheckingException);
+
+  /**
+   * Make an integer subrange type as defined by the argument.
+   */
+  Type mkSubrangeType(const SubrangeBounds& bounds)
+    throw(TypeCheckingException);
+
   /** Get the type of an expression */
   Type getType(Expr e, bool check = false)
-    throw (TypeCheckingException);
+    throw(TypeCheckingException);
 
   // variables are special, because duplicates are permitted
   Expr mkVar(const std::string& name, Type type);
@@ -421,6 +447,7 @@ public:
 
   /** Returns the maximum arity of the given kind. */
   static unsigned maxArity(Kind kind);
+
 };/* class ExprManager */
 
 ${mkConst_instantiations}
diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index c510ce381..d0f5fde9e 100644
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -76,7 +76,8 @@ TypeCheckingException::~TypeCheckingException() throw() {
 }
 
 void TypeCheckingException::toStream(std::ostream& os) const throw() {
-  os << "Error type-checking " << d_expr << ": " << d_msg << endl << *d_expr;
+  os << "Error during type checking: " << d_msg << endl
+     << "The ill-typed expression: " << *d_expr;
 }
 
 Expr TypeCheckingException::getExpression() const throw() {
diff --git a/src/expr/node.cpp b/src/expr/node.cpp
index 695e572ab..e303a9e58 100644
--- a/src/expr/node.cpp
+++ b/src/expr/node.cpp
@@ -36,7 +36,7 @@ TypeCheckingExceptionPrivate::~TypeCheckingExceptionPrivate() throw () {
 }
 
 void TypeCheckingExceptionPrivate::toStream(std::ostream& os) const throw() {
-  os << "Error type-checking " << d_node << ": " << d_msg << std::endl << *d_node;
+  os << "Error during type checking: " << d_msg << std::endl << *d_node << endl << "The ill-typed expression: " << *d_node;
 }
 
 NodeTemplate<true> TypeCheckingExceptionPrivate::getNode() const throw() {
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index c647e128c..a2fddadfc 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -29,6 +29,7 @@
 
 #include <algorithm>
 #include <stack>
+#include <utility>
 #include <ext/hash_set>
 
 using namespace std;
@@ -235,14 +236,15 @@ void NodeManager::reclaimZombies() {
 }/* NodeManager::reclaimZombies() */
 
 TypeNode NodeManager::getType(TNode n, bool check)
-  throw (TypeCheckingExceptionPrivate, AssertionException) {
-  // Many theories' type checkers call Node::getType() directly.
-  // This is incorrect, since "this" might not be the caller's
-  // curent node manager.  Rather than force the individual typecheckers
-  // not to do this (by policy, which would be imperfect and lead
-  // to hard-to-find bugs, which it has in the past), we just
-  // set this node manager to be current for the duration of this
-  // check.
+  throw(TypeCheckingExceptionPrivate, AssertionException) {
+
+  // Many theories' type checkers call Node::getType() directly.  This
+  // is incorrect, since "this" might not be the caller's curent node
+  // manager.  Rather than force the individual typecheckers not to do
+  // this (by policy, which would be imperfect and lead to
+  // hard-to-find bugs, which it has in the past), we just set this
+  // node manager to be current for the duration of this check.
+  //
   NodeManagerScope nms(this);
 
   TypeNode typeNode;
@@ -321,4 +323,51 @@ TypeNode NodeManager::mkConstructorType(const DatatypeConstructor& constructor,
   return mkTypeNode(kind::CONSTRUCTOR_TYPE, sorts);
 }
 
+TypeNode NodeManager::mkPredicateSubtype(Expr lambda)
+  throw(TypeCheckingExceptionPrivate) {
+
+  Node lambdan = Node::fromExpr(lambda);
+
+  if(lambda.isNull()) {
+    throw TypeCheckingExceptionPrivate(lambdan, "cannot make a predicate subtype based on null expression");
+  }
+
+  TypeNode tn = lambdan.getType();
+  if(! tn.isPredicateLike() ||
+     tn.getArgTypes().size() != 1) {
+    std::stringstream ss;
+    ss << Expr::setlanguage(Options::current()->outputLanguage)
+       << "expected a predicate of one argument to define predicate subtype, but got type `" << tn << "'";
+    throw TypeCheckingExceptionPrivate(lambdan, ss.str());
+  }
+
+  return TypeNode(mkTypeConst(Predicate(lambda)));
+}
+
+TypeNode NodeManager::mkPredicateSubtype(Expr lambda, Expr witness)
+  throw(TypeCheckingExceptionPrivate) {
+
+  Node lambdan = Node::fromExpr(lambda);
+
+  if(lambda.isNull()) {
+    throw TypeCheckingExceptionPrivate(lambdan, "cannot make a predicate subtype based on null expression");
+  }
+
+  TypeNode tn = lambdan.getType();
+  if(! tn.isPredicateLike() ||
+     tn.getArgTypes().size() != 1) {
+    std::stringstream ss;
+    ss << Expr::setlanguage(Options::current()->outputLanguage)
+       << "expected a predicate of one argument to define predicate subtype, but got type `" << tn << "'";
+    throw TypeCheckingExceptionPrivate(lambdan, ss.str());
+  }
+
+  return TypeNode(mkTypeConst(Predicate(lambda, witness)));
+}
+
+TypeNode NodeManager::mkSubrangeType(const SubrangeBounds& bounds)
+  throw(TypeCheckingExceptionPrivate) {
+  return TypeNode(mkTypeConst(bounds));
+}
+
 }/* CVC4 namespace */
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 704e930b5..da999cc82 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -38,6 +38,7 @@
 #include "expr/metakind.h"
 #include "expr/node_value.h"
 #include "context/context.h"
+#include "util/subrange_bound.h"
 #include "util/configuration_private.h"
 #include "util/tls.h"
 #include "util/options.h"
@@ -662,6 +663,31 @@ public:
   inline TypeNode mkSortConstructor(const std::string& name, size_t arity);
 
   /**
+   * Make a predicate subtype type defined by the given LAMBDA
+   * expression.  A TypeCheckingExceptionPrivate can be thrown if
+   * lambda is not a LAMBDA, or is ill-typed, or if CVC4 fails at
+   * proving that the resulting predicate subtype is inhabited.
+   */
+  TypeNode mkPredicateSubtype(Expr lambda)
+    throw(TypeCheckingExceptionPrivate);
+
+  /**
+   * Make a predicate subtype type defined by the given LAMBDA
+   * expression and whose non-emptiness is witnessed by the given
+   * witness.  A TypeCheckingExceptionPrivate can be thrown if lambda
+   * is not a LAMBDA, or is ill-typed, or if the witness is not a
+   * witness or ill-typed.
+   */
+  TypeNode mkPredicateSubtype(Expr lambda, Expr witness)
+    throw(TypeCheckingExceptionPrivate);
+
+  /**
+   * Make an integer subrange type as defined by the argument.
+   */
+  TypeNode mkSubrangeType(const SubrangeBounds& bounds)
+    throw(TypeCheckingExceptionPrivate);
+
+  /**
    * Get the type for the given node and optionally do type checking.
    *
    * Initial type computation will be near-constant time if
@@ -687,7 +713,7 @@ public:
    * (default: false)
    */
   TypeNode getType(TNode n, bool check = false)
-    throw (TypeCheckingExceptionPrivate, AssertionException);
+    throw(TypeCheckingExceptionPrivate, AssertionException);
 
   /**
    * Convert a node to an expression.  Uses the ExprManager
@@ -944,10 +970,15 @@ inline TypeNode NodeManager::mkBitVectorType(unsigned size) {
 
 inline TypeNode NodeManager::mkArrayType(TypeNode indexType,
                                          TypeNode constituentType) {
-  CheckArgument(!indexType.isFunctionLike(), domain,
+  CheckArgument(!indexType.isNull(), indexType,
+                "unexpected NULL index type");
+  CheckArgument(!constituentType.isNull(), constituentType,
+                "unexpected NULL constituent type");
+  CheckArgument(!indexType.isFunctionLike(), indexType,
                 "cannot index arrays by a function-like type");
-  CheckArgument(!constituentType.isFunctionLike(), domain,
+  CheckArgument(!constituentType.isFunctionLike(), constituentType,
                 "cannot store function-like types in arrays");
+Debug("arrays") << "making array type " << indexType << " " << constituentType << std::endl;
   return mkTypeNode(kind::ARRAY_TYPE, indexType, constituentType);
 }
 
diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index a901af73a..eaf10ba20 100644
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -103,26 +103,32 @@ Type& Type::operator=(const Type& t) {
 }
 
 bool Type::operator==(const Type& t) const {
+  NodeManagerScope nms(d_nodeManager);
   return *d_typeNode == *t.d_typeNode;
 }
 
 bool Type::operator!=(const Type& t) const {
+  NodeManagerScope nms(d_nodeManager);
   return *d_typeNode != *t.d_typeNode;
 }
 
 bool Type::operator<(const Type& t) const {
+  NodeManagerScope nms(d_nodeManager);
   return *d_typeNode < *t.d_typeNode;
 }
 
 bool Type::operator<=(const Type& t) const {
+  NodeManagerScope nms(d_nodeManager);
   return *d_typeNode <= *t.d_typeNode;
 }
 
 bool Type::operator>(const Type& t) const {
+  NodeManagerScope nms(d_nodeManager);
   return *d_typeNode > *t.d_typeNode;
 }
 
 bool Type::operator>=(const Type& t) const {
+  NodeManagerScope nms(d_nodeManager);
   return *d_typeNode >= *t.d_typeNode;
 }
 
@@ -375,13 +381,39 @@ bool Type::isSortConstructor() const {
   return d_typeNode->isSortConstructor();
 }
 
-/** Cast to a sort type */
+/** Cast to a sort constructor type */
 Type::operator SortConstructorType() const throw(AssertionException) {
   NodeManagerScope nms(d_nodeManager);
   Assert(isNull() || isSortConstructor());
   return SortConstructorType(*this);
 }
 
+/** Is this a predicate subtype */
+bool Type::isPredicateSubtype() const {
+  NodeManagerScope nms(d_nodeManager);
+  return d_typeNode->isPredicateSubtype();
+}
+
+/** Cast to a predicate subtype */
+Type::operator PredicateSubtype() const throw(AssertionException) {
+  NodeManagerScope nms(d_nodeManager);
+  Assert(isNull() || isPredicateSubtype());
+  return PredicateSubtype(*this);
+}
+
+/** Is this an integer subrange */
+bool Type::isSubrange() const {
+  NodeManagerScope nms(d_nodeManager);
+  return d_typeNode->isSubrange();
+}
+
+/** Cast to a predicate subtype */
+Type::operator SubrangeType() const throw(AssertionException) {
+  NodeManagerScope nms(d_nodeManager);
+  Assert(isNull() || isSubrange());
+  return SubrangeType(*this);
+}
+
 /** Is this a kind type (i.e., the type of a type)? */
 bool Type::isKind() const {
   NodeManagerScope nms(d_nodeManager);
@@ -543,6 +575,18 @@ SortConstructorType::SortConstructorType(const Type& t)
   Assert(isNull() || isSortConstructor());
 }
 
+PredicateSubtype::PredicateSubtype(const Type& t)
+  throw(AssertionException) :
+  Type(t) {
+  Assert(isNull() || isPredicateSubtype());
+}
+
+SubrangeType::SubrangeType(const Type& t)
+  throw(AssertionException) :
+  Type(t) {
+  Assert(isNull() || isSubrange());
+}
+
 unsigned BitVectorType::getSize() const {
   return d_typeNode->getBitVectorSize();
 }
@@ -648,6 +692,21 @@ BooleanType TesterType::getRangeType() const {
   return BooleanType(makeType(d_nodeManager->booleanType()));
 }
 
+Expr PredicateSubtype::getPredicate() const {
+  NodeManagerScope nms(d_nodeManager);
+  return d_typeNode->getSubtypePredicate().toExpr();
+}
+
+Type PredicateSubtype::getBaseType() const {
+  NodeManagerScope nms(d_nodeManager);
+  return d_typeNode->getSubtypeBaseType().toType();
+}
+
+SubrangeBounds SubrangeType::getSubrangeBounds() const {
+  NodeManagerScope nms(d_nodeManager);
+  return d_typeNode->getSubrangeBounds();
+}
+
 size_t TypeHashFunction::operator()(const Type& t) const {
   return TypeNodeHashFunction()(NodeManager::fromType(t));
 }
diff --git a/src/expr/type.h b/src/expr/type.h
index 34cc925f6..76fccb37b 100644
--- a/src/expr/type.h
+++ b/src/expr/type.h
@@ -28,6 +28,7 @@
 
 #include "util/Assert.h"
 #include "util/cardinality.h"
+#include "util/subrange_bound.h"
 
 namespace CVC4 {
 
@@ -60,6 +61,8 @@ class TupleType;
 class KindType;
 class SortType;
 class SortConstructorType;
+class PredicateSubtype;
+class SubrangeType;
 class Type;
 
 /** Strategy for hashing Types */
@@ -405,6 +408,30 @@ public:
   operator SortConstructorType() const throw(AssertionException);
 
   /**
+   * Is this a predicate subtype?
+   * @return true if this is a predicate subtype
+   */
+  bool isPredicateSubtype() const;
+
+  /**
+   * Cast this type to a predicate subtype
+   * @return the predicate subtype
+   */
+  operator PredicateSubtype() const throw(AssertionException);
+
+  /**
+   * Is this an integer subrange type?
+   * @return true if this is an integer subrange type
+   */
+  bool isSubrange() const;
+
+  /**
+   * Cast this type to an integer subrange type
+   * @return the integer subrange type
+   */
+  operator SubrangeType() const throw(AssertionException);
+
+  /**
    * Is this a kind type (i.e., the type of a type)?
    * @return true if this is a kind type
    */
@@ -574,6 +601,39 @@ public:
 };/* class SortConstructorType */
 
 /**
+ * Class encapsulating a predicate subtype.
+ */
+class CVC4_PUBLIC PredicateSubtype : public Type {
+
+public:
+
+  /** Construct from the base type */
+  PredicateSubtype(const Type& type = Type()) throw(AssertionException);
+
+  /** Get the LAMBDA defining this predicate subtype */
+  Expr getPredicate() const;
+
+  /** Get the base type of this predicate subtype */
+  Type getBaseType() const;
+
+};/* class PredicateSubtype */
+
+/**
+ * Class encapsulating an integer subrange type.
+ */
+class CVC4_PUBLIC SubrangeType : public Type {
+
+public:
+
+  /** Construct from the base type */
+  SubrangeType(const Type& type = Type()) throw(AssertionException);
+
+  /** Get the bounds defining this integer subrange */
+  SubrangeBounds getSubrangeBounds() const;
+
+};/* class SubrangeType */
+
+/**
  * Class encapsulating the kind type (the type of types).
  */
 class CVC4_PUBLIC KindType : public Type {
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index 77203bbb5..8cfb6387a 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -71,68 +71,45 @@ Node TypeNode::mkGroundTerm() const {
   return kind::mkGroundTerm(*this);
 }
 
-bool TypeNode::isBoolean() const {
-  return getKind() == kind::TYPE_CONSTANT &&
-    ( getConst<TypeConstant>() == BOOLEAN_TYPE ||
-      getConst<TypeConstant>() == PSEUDOBOOLEAN_TYPE );
-}
-
-bool TypeNode::isInteger() const {
-  return getKind() == kind::TYPE_CONSTANT &&
-    ( getConst<TypeConstant>() == INTEGER_TYPE ||
-      getConst<TypeConstant>() == PSEUDOBOOLEAN_TYPE );
-}
-
-bool TypeNode::isReal() const {
-  return getKind() == kind::TYPE_CONSTANT &&
-    ( getConst<TypeConstant>() == REAL_TYPE ||
-      getConst<TypeConstant>() == INTEGER_TYPE ||
-      getConst<TypeConstant>() == PSEUDOBOOLEAN_TYPE );
-}
-
-bool TypeNode::isPseudoboolean() const {
-  return getKind() == kind::TYPE_CONSTANT &&
-    getConst<TypeConstant>() == PSEUDOBOOLEAN_TYPE;
-}
-
-bool TypeNode::isString() const {
-  return getKind() == kind::TYPE_CONSTANT &&
-    getConst<TypeConstant>() == STRING_TYPE;
-}
-
-bool TypeNode::isArray() const {
-  return getKind() == kind::ARRAY_TYPE;
-}
-
-TypeNode TypeNode::getArrayIndexType() const {
-  Assert(isArray());
-  return (*this)[0];
-}
-
-TypeNode TypeNode::getArrayConstituentType() const {
-  Assert(isArray());
-  return (*this)[1];
-}
-
-TypeNode TypeNode::getConstructorRangeType() const {
-  Assert(isConstructor());
-  return (*this)[getNumChildren()-1];
-}
-
-bool TypeNode::isFunction() const {
-  return getKind() == kind::FUNCTION_TYPE;
+bool TypeNode::isSubtypeOf(TypeNode t) const {
+  if(*this == t) {
+    return true;
+  }
+  if(getKind() == kind::TYPE_CONSTANT) {
+    switch(getConst<TypeConstant>()) {
+    case PSEUDOBOOLEAN_TYPE:
+      return t.getKind() == kind::TYPE_CONSTANT &&
+        ( t.getConst<TypeConstant>() == BOOLEAN_TYPE ||
+          t.getConst<TypeConstant>() == INTEGER_TYPE );
+    case INTEGER_TYPE:
+      return t.getKind() == kind::TYPE_CONSTANT && t.getConst<TypeConstant>() == REAL_TYPE;
+    default:
+      return false;
+    }
+  }
+  if(isSubrange()) {
+    if(t.isSubrange()) {
+      return t.getSubrangeBounds() <= getSubrangeBounds();
+    } else {
+      return t.getKind() == kind::TYPE_CONSTANT &&
+        ( t.getConst<TypeConstant>() == INTEGER_TYPE ||
+          t.getConst<TypeConstant>() == REAL_TYPE );
+    }
+  }
+  if(isPredicateSubtype()) {
+    return getSubtypeBaseType().isSubtypeOf(t);
+  }
+  return false;
 }
 
-bool TypeNode::isFunctionLike() const {
-  return
-    getKind() == kind::FUNCTION_TYPE ||
-    getKind() == kind::CONSTRUCTOR_TYPE ||
-    getKind() == kind::SELECTOR_TYPE ||
-    getKind() == kind::TESTER_TYPE;
+Node TypeNode::getSubtypePredicate() const {
+  Assert(isPredicateSubtype());
+  return Node::fromExpr(getConst<Predicate>());
 }
 
-bool TypeNode::isPredicate() const {
-  return isFunction() && getRangeType().isBoolean();
+TypeNode TypeNode::getSubtypeBaseType() const {
+  Assert(isPredicateSubtype());
+  return getSubtypePredicate().getType().getArgTypes()[0];
 }
 
 std::vector<TypeNode> TypeNode::getArgTypes() const {
@@ -158,19 +135,6 @@ std::vector<TypeNode> TypeNode::getParamTypes() const {
   return params;
 }
 
-TypeNode TypeNode::getRangeType() const {
-  if(isTester()) {
-    return NodeManager::currentNM()->booleanType();
-  }
-  Assert(isFunction() || isConstructor() || isSelector());
-  return (*this)[getNumChildren()-1];
-}
-
-/** Is this a tuple type? */
-bool TypeNode::isTuple() const {
-  return getKind() == kind::TUPLE_TYPE;
-}
-
 /** Is this a tuple type? */
 vector<TypeNode> TypeNode::getTupleTypes() const {
   Assert(isTuple());
@@ -181,37 +145,6 @@ vector<TypeNode> TypeNode::getTupleTypes() const {
   return types;
 }
 
-/** Is this a sort kind */
-bool TypeNode::isSort() const {
-  return getKind() == kind::SORT_TYPE && !hasAttribute(expr::SortArityAttr());
-}
-
-/** Is this a sort constructor kind */
-bool TypeNode::isSortConstructor() const {
-  return getKind() == kind::SORT_TYPE && hasAttribute(expr::SortArityAttr());
-}
-
-/** Is this a kind type (i.e., the type of a type)? */
-bool TypeNode::isKind() const {
-  return getKind() == kind::TYPE_CONSTANT &&
-    getConst<TypeConstant>() == KIND_TYPE;
-}
-
-/** Is this a bit-vector type */
-bool TypeNode::isBitVector() const {
-  return getKind() == kind::BITVECTOR_TYPE;
-}
-
-/** Is this a datatype type */
-bool TypeNode::isDatatype() const {
-  return getKind() == kind::DATATYPE_TYPE;
-}
-
-/** Is this a parametric datatype type */
-bool TypeNode::isParametricDatatype() const {
-  return getKind() == kind::PARAMETRIC_DATATYPE;
-}
-
 /** Is this an instantiated datatype type */
 bool TypeNode::isInstantiatedDatatype() const {
   if(getKind() == kind::DATATYPE_TYPE) {
@@ -239,31 +172,4 @@ bool TypeNode::isParameterInstantiatedDatatype(unsigned n) const {
   return TypeNode::fromType(dt.getParameter(n)) != (*this)[n + 1];
 }
 
-/** Is this a constructor type */
-bool TypeNode::isConstructor() const {
-  return getKind() == kind::CONSTRUCTOR_TYPE;
-}
-
-/** Is this a selector type */
-bool TypeNode::isSelector() const {
-  return getKind() == kind::SELECTOR_TYPE;
-}
-
-/** Is this a tester type */
-bool TypeNode::isTester() const {
-  return getKind() == kind::TESTER_TYPE;
-}
-
-/** Is this a bit-vector type of size <code>size</code> */
-bool TypeNode::isBitVector(unsigned size) const {
-  return getKind() == kind::BITVECTOR_TYPE &&
-    getConst<BitVectorSize>() == size;
-}
-
-/** Get the size of this bit-vector type */
-unsigned TypeNode::getBitVectorSize() const {
-  Assert(isBitVector());
-  return getConst<BitVectorSize>();
-}
-
 }/* CVC4 namespace */
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index c7da5ceb7..f59ce2dfe 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -447,6 +447,9 @@ public:
    */
   Node mkGroundTerm() const;
 
+  /** Is this type a subtype of the given type? */
+  bool isSubtypeOf(TypeNode t) const;
+
   /** Is this the Boolean type? */
   bool isBoolean() const;
 
@@ -519,6 +522,16 @@ public:
    */
   bool isPredicate() const;
 
+  /**
+   * Is this a predicate-LIKE type?  Predicate-like things
+   * (e.g. datatype testers) that aren't actually predicates ARE
+   * considered predicates, here.
+   *
+   * Arrays are explicitly *not* predicate-like for the purposes of
+   * this test.
+   */
+  bool isPredicateLike() const;
+
   /** Is this a tuple type? */
   bool isTuple() const;
 
@@ -561,6 +574,21 @@ public:
   /** Is this a sort constructor kind */
   bool isSortConstructor() const;
 
+  /** Is this a subtype predicate */
+  bool isPredicateSubtype() const;
+
+  /** Get the predicate defining this subtype */
+  Node getSubtypePredicate() const;
+
+  /** Get the base type of this subtype */
+  TypeNode getSubtypeBaseType() const;
+
+  /** Is this a subrange */
+  bool isSubrange() const;
+
+  /** Get the bounds defining this subrange */
+  const SubrangeBounds& getSubrangeBounds() const;
+
   /** Is this a kind type (i.e., the type of a type)? */
   bool isKind() const;
 
@@ -755,6 +783,172 @@ inline void TypeNode::printAst(std::ostream& out, int indent) const {
   d_nv->printAst(out, indent);
 }
 
+inline bool TypeNode::isBoolean() const {
+  return
+    ( getKind() == kind::TYPE_CONSTANT && getConst<TypeConstant>() == BOOLEAN_TYPE ) ||
+      isPseudoboolean() ||
+    ( isPredicateSubtype() && getSubtypeBaseType().isBoolean() );
+}
+
+inline bool TypeNode::isInteger() const {
+  return
+    ( getKind() == kind::TYPE_CONSTANT && getConst<TypeConstant>() == INTEGER_TYPE ) ||
+    isSubrange() ||
+    isPseudoboolean() ||
+    ( isPredicateSubtype() && getSubtypeBaseType().isInteger() );
+}
+
+inline bool TypeNode::isReal() const {
+  return
+    ( getKind() == kind::TYPE_CONSTANT && getConst<TypeConstant>() == REAL_TYPE ) ||
+    isInteger() ||
+    ( isPredicateSubtype() && getSubtypeBaseType().isReal() );
+}
+
+inline bool TypeNode::isPseudoboolean() const {
+  return
+    ( getKind() == kind::TYPE_CONSTANT && getConst<TypeConstant>() == PSEUDOBOOLEAN_TYPE ) ||
+    ( isPredicateSubtype() && getSubtypeBaseType().isPseudoboolean() );
+}
+
+inline bool TypeNode::isString() const {
+  return getKind() == kind::TYPE_CONSTANT &&
+    getConst<TypeConstant>() == STRING_TYPE;
+}
+
+inline bool TypeNode::isArray() const {
+  return getKind() == kind::ARRAY_TYPE ||
+    ( isPredicateSubtype() && getSubtypeBaseType().isPseudoboolean() );
+}
+
+inline TypeNode TypeNode::getArrayIndexType() const {
+  Assert(isArray());
+  return (*this)[0];
+}
+
+inline TypeNode TypeNode::getArrayConstituentType() const {
+  Assert(isArray());
+  return (*this)[1];
+}
+
+inline TypeNode TypeNode::getConstructorRangeType() const {
+  Assert(isConstructor());
+  return (*this)[getNumChildren()-1];
+}
+
+inline bool TypeNode::isFunction() const {
+  return getKind() == kind::FUNCTION_TYPE;
+}
+
+inline bool TypeNode::isFunctionLike() const {
+  return
+    getKind() == kind::FUNCTION_TYPE ||
+    getKind() == kind::CONSTRUCTOR_TYPE ||
+    getKind() == kind::SELECTOR_TYPE ||
+    getKind() == kind::TESTER_TYPE;
+}
+
+inline bool TypeNode::isPredicate() const {
+  return isFunction() && getRangeType().isBoolean();
+}
+
+inline bool TypeNode::isPredicateLike() const {
+  return isFunctionLike() && getRangeType().isBoolean();
+}
+
+inline TypeNode TypeNode::getRangeType() const {
+  if(isTester()) {
+    return NodeManager::currentNM()->booleanType();
+  }
+  Assert(isFunction() || isConstructor() || isSelector());
+  return (*this)[getNumChildren() - 1];
+}
+
+/** Is this a tuple type? */
+inline bool TypeNode::isTuple() const {
+  return getKind() == kind::TUPLE_TYPE ||
+    ( isPredicateSubtype() && getSubtypeBaseType().isTuple() );
+}
+
+/** Is this a sort kind */
+inline bool TypeNode::isSort() const {
+  return ( getKind() == kind::SORT_TYPE && !hasAttribute(expr::SortArityAttr()) ) ||
+    ( isPredicateSubtype() && getSubtypeBaseType().isSort() );
+}
+
+/** Is this a sort constructor kind */
+inline bool TypeNode::isSortConstructor() const {
+  return getKind() == kind::SORT_TYPE && hasAttribute(expr::SortArityAttr());
+}
+
+/** Is this a predicate subtype */
+inline bool TypeNode::isPredicateSubtype() const {
+  return getKind() == kind::SUBTYPE_TYPE;
+}
+
+/** Is this a subrange type */
+inline bool TypeNode::isSubrange() const {
+  return getKind() == kind::SUBRANGE_TYPE ||
+    ( isPredicateSubtype() && getSubtypeBaseType().isSubrange() );
+}
+
+/** Is this a kind type (i.e., the type of a type)? */
+inline bool TypeNode::isKind() const {
+  return getKind() == kind::TYPE_CONSTANT &&
+    getConst<TypeConstant>() == KIND_TYPE;
+}
+
+/** Is this a bit-vector type */
+inline bool TypeNode::isBitVector() const {
+  return getKind() == kind::BITVECTOR_TYPE ||
+    ( isPredicateSubtype() && getSubtypeBaseType().isBitVector() );
+}
+
+/** Is this a datatype type */
+inline bool TypeNode::isDatatype() const {
+  return getKind() == kind::DATATYPE_TYPE ||
+    ( isPredicateSubtype() && getSubtypeBaseType().isDatatype() );
+}
+
+/** Is this a parametric datatype type */
+inline bool TypeNode::isParametricDatatype() const {
+  return getKind() == kind::PARAMETRIC_DATATYPE ||
+    ( isPredicateSubtype() && getSubtypeBaseType().isParametricDatatype() );
+}
+
+/** Is this a constructor type */
+inline bool TypeNode::isConstructor() const {
+  return getKind() == kind::CONSTRUCTOR_TYPE;
+}
+
+/** Is this a selector type */
+inline bool TypeNode::isSelector() const {
+  return getKind() == kind::SELECTOR_TYPE;
+}
+
+/** Is this a tester type */
+inline bool TypeNode::isTester() const {
+  return getKind() == kind::TESTER_TYPE;
+}
+
+/** Is this a bit-vector type of size <code>size</code> */
+inline bool TypeNode::isBitVector(unsigned size) const {
+  return
+    ( getKind() == kind::BITVECTOR_TYPE && getConst<BitVectorSize>() == size ) ||
+    ( isPredicateSubtype() && getSubtypeBaseType().isBitVector(size) );
+}
+
+/** Get the size of this bit-vector type */
+inline unsigned TypeNode::getBitVectorSize() const {
+  Assert(isBitVector());
+  return getConst<BitVectorSize>();
+}
+
+inline const SubrangeBounds& TypeNode::getSubrangeBounds() const {
+  Assert(isSubrange());
+  return getConst<SubrangeBounds>();
+}
+
 #ifdef CVC4_DEBUG
 /**
  * Pretty printer for use within gdb.  This is not intended to be used
diff --git a/src/main/driver.cpp b/src/main/driver.cpp
index fa42e0b28..eb70f5c93 100644
--- a/src/main/driver.cpp
+++ b/src/main/driver.cpp
@@ -259,7 +259,7 @@ int runCvc4(int argc, char* argv[], Options& options) {
     ParserBuilder parserBuilder(&exprMgr, filename, options);
 
     if( inputFromStdin ) {
-      parserBuilder.withStreamInput(cin);
+      parserBuilder.withLineBufferedStreamInput(cin);
     }
 
     Parser *parser = parserBuilder.build();
diff --git a/src/main/driver_portfolio.cpp b/src/main/driver_portfolio.cpp
index d17d00c5d..363901c1d 100644
--- a/src/main/driver_portfolio.cpp
+++ b/src/main/driver_portfolio.cpp
@@ -428,7 +428,7 @@ int runCvc4(int argc, char *argv[], Options& options) {
         withOptions(options);
 
     if( inputFromStdin ) {
-      parserBuilder.withStreamInput(cin);
+      parserBuilder.withLineBufferedStreamInput(cin);
     }
 
     Parser *parser = parserBuilder.build();
diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp
index a63d6c67b..d8e7df2f2 100644
--- a/src/main/interactive_shell.cpp
+++ b/src/main/interactive_shell.cpp
@@ -83,7 +83,7 @@ InteractiveShell::InteractiveShell(ExprManager& exprManager,
                                    const Options& options) :
   d_in(*options.in),
   d_out(*options.out),
-  d_language(options.inputLanguage),
+  d_options(options),
   d_quit(false) {
   ParserBuilder parserBuilder(&exprManager, INPUT_FILENAME, options);
   /* Create parser with bogus input. */
@@ -95,7 +95,7 @@ InteractiveShell::InteractiveShell(ExprManager& exprManager,
     ::rl_completion_entry_function = commandGenerator;
     ::using_history();
 
-    switch(OutputLanguage lang = toOutputLanguage(d_language)) {
+    switch(OutputLanguage lang = toOutputLanguage(d_options.inputLanguage)) {
     case output::LANG_CVC4:
       d_historyFilename = string(getenv("HOME")) + "/.cvc4_history";
       commandsBegin = cvc_commands;
@@ -166,7 +166,7 @@ Command* InteractiveShell::readCommand() {
   /* Prompt the user for input. */
   if(d_usingReadline) {
 #if HAVE_LIBREADLINE
-    lineBuf = ::readline("CVC4> ");
+    lineBuf = ::readline(d_options.verbosity >= 0 ? "CVC4> " : "");
     if(lineBuf != NULL && lineBuf[0] != '\0') {
       ::add_history(lineBuf);
     }
@@ -174,7 +174,9 @@ Command* InteractiveShell::readCommand() {
     free(lineBuf);
 #endif /* HAVE_LIBREADLINE */
   } else {
-    d_out << "CVC4> " << flush;
+    if(d_options.verbosity >= 0) {
+      d_out << "CVC4> " << flush;
+    }
 
     /* Read a line */
     d_in.get(sb,'\n');
@@ -229,7 +231,7 @@ Command* InteractiveShell::readCommand() {
       input[n] = '\n';
       if(d_usingReadline) {
 #if HAVE_LIBREADLINE
-        lineBuf = ::readline("... > ");
+        lineBuf = ::readline(d_options.verbosity >= 0 ? "... > " : "");
         if(lineBuf != NULL && lineBuf[0] != '\0') {
           ::add_history(lineBuf);
         }
@@ -237,7 +239,9 @@ Command* InteractiveShell::readCommand() {
         free(lineBuf);
 #endif /* HAVE_LIBREADLINE */
       } else {
-        d_out << "... > " << flush;
+        if(d_options.verbosity >= 0) {
+          d_out << "... > " << flush;
+        }
 
         /* Read a line */
         d_in.get(sb,'\n');
@@ -250,7 +254,7 @@ Command* InteractiveShell::readCommand() {
     }
   }
 
-  d_parser->setInput(Input::newStringInput(d_language,input,INPUT_FILENAME));
+  d_parser->setInput(Input::newStringInput(d_options.inputLanguage, input, INPUT_FILENAME));
 
   /* There may be more than one command in the input. Build up a
      sequence. */
diff --git a/src/main/interactive_shell.h b/src/main/interactive_shell.h
index 65fea8494..7f17b88d7 100644
--- a/src/main/interactive_shell.h
+++ b/src/main/interactive_shell.h
@@ -36,7 +36,7 @@ class CVC4_PUBLIC InteractiveShell {
   std::istream& d_in;
   std::ostream& d_out;
   parser::Parser* d_parser;
-  const InputLanguage d_language;
+  const Options& d_options;
   bool d_quit;
   bool d_usingReadline;
 
diff --git a/src/parser/Makefile.am b/src/parser/Makefile.am
index 4f00cfb3d..f14941d01 100644
--- a/src/parser/Makefile.am
+++ b/src/parser/Makefile.am
@@ -45,6 +45,8 @@ libcvc4parser_la_SOURCES = \
 	antlr_input.h \
 	antlr_input.cpp \
 	antlr_input_imports.cpp \
+	antlr_line_buffered_input.h \
+	antlr_line_buffered_input.cpp \
 	bounded_token_buffer.h \
 	bounded_token_buffer.cpp \
 	bounded_token_factory.h \
@@ -64,6 +66,8 @@ libcvc4parser_noinst_la_SOURCES = \
 	antlr_input.h \
 	antlr_input.cpp \
 	antlr_input_imports.cpp \
+	antlr_line_buffered_input.h \
+	antlr_line_buffered_input.cpp \
 	bounded_token_buffer.h \
 	bounded_token_buffer.cpp \
 	bounded_token_factory.h \
diff --git a/src/parser/Makefile.antlr_tracing b/src/parser/Makefile.antlr_tracing
index 087554c52..fa79337b4 100644
--- a/src/parser/Makefile.antlr_tracing
+++ b/src/parser/Makefile.antlr_tracing
@@ -3,7 +3,8 @@
 # This makefile is included from parser directories in order to
 # do antlr tracing.  THIS IS VERY MUCH A HACK, and is only enabled
 # if CVC4_TRACE_ANTLR is defined (and not 0).  In ANTLR 3.2, we
-# have to #define 
+# have to #define "println" and "System," etc., because the
+# generator erroneously puts Java in C output!
 #
 
 ifeq ($(CVC4_TRACE_ANTLR),)
diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp
index e52145d4e..67d873a48 100644
--- a/src/parser/antlr_input.cpp
+++ b/src/parser/antlr_input.cpp
@@ -24,6 +24,7 @@
 #include "parser/input.h"
 #include "parser/bounded_token_buffer.h"
 #include "parser/bounded_token_factory.h"
+#include "parser/antlr_line_buffered_input.h"
 #include "parser/memory_mapped_input_buffer.h"
 #include "parser/parser_exception.h"
 #include "parser/parser.h"
@@ -60,8 +61,8 @@ pANTLR3_INPUT_STREAM AntlrInputStream::getAntlr3InputStream() const {
   return d_input;
 }
 
-AntlrInputStream* 
-AntlrInputStream::newFileInputStream(const std::string& name, 
+AntlrInputStream*
+AntlrInputStream::newFileInputStream(const std::string& name,
                                      bool useMmap)
   throw (InputStreamException, AssertionException) {
   pANTLR3_INPUT_STREAM input = NULL;
@@ -81,63 +82,84 @@ AntlrInputStream::newFileInputStream(const std::string& name,
   return new AntlrInputStream( name, input );
 }
 
-AntlrInputStream* 
-AntlrInputStream::newStreamInputStream(std::istream& input, 
-                                       const std::string& name)
+AntlrInputStream*
+AntlrInputStream::newStreamInputStream(std::istream& input,
+                                       const std::string& name,
+                                       bool lineBuffered)
   throw (InputStreamException, AssertionException) {
 
-  // Since these are all NULL on entry, realloc will be called
-  char *basep = NULL, *boundp = NULL, *cp = NULL;
-  /* 64KB seems like a reasonable default size. */
-  size_t bufSize = 0x10000;
+  pANTLR3_INPUT_STREAM inputStream = NULL;
 
-  /* Keep going until we can't go no more. */
-  while( !input.eof() && !input.fail() ) {
+  if(lineBuffered) {
+#ifdef CVC4_ANTLR3_OLD_INPUT_STREAM
+    inputStream =
+      antlr3LineBufferedStreamNew(input,
+                                  0,
+                                  (pANTLR3_UINT8) strdup(name.c_str()));
+#else /* CVC4_ANTLR3_OLD_INPUT_STREAM */
+    inputStream =
+      antlr3LineBufferedStreamNew(input,
+                                  ANTLR3_ENC_8BIT,
+                                  (pANTLR3_UINT8) strdup(name.c_str()));
+#endif /* CVC4_ANTLR3_OLD_INPUT_STREAM */
+  } else {
 
-    if( cp == boundp ) {
-      /* We ran out of room in the buffer. Realloc at double the size. */
-      ptrdiff_t offset = cp - basep;
-      basep = (char *) realloc(basep, bufSize);
-      if( basep == NULL ) {
-        throw InputStreamException("Failed buffering input stream: " + name);
+    // Since these are all NULL on entry, realloc will be called
+    char *basep = NULL, *boundp = NULL, *cp = NULL;
+    /* 64KB seems like a reasonable default size. */
+    size_t bufSize = 0x10000;
+
+    /* Keep going until we can't go no more. */
+    while( !input.eof() && !input.fail() ) {
+
+      if( cp == boundp ) {
+        /* We ran out of room in the buffer. Realloc at double the size. */
+        ptrdiff_t offset = cp - basep;
+        basep = (char *) realloc(basep, bufSize);
+        if( basep == NULL ) {
+          throw InputStreamException("Failed buffering input stream: " + name);
+        }
+        cp = basep + offset;
+        boundp = basep + bufSize;
+        bufSize *= 2;
       }
-      cp = basep + offset;
-      boundp = basep + bufSize;
-      bufSize *= 2;
-    }
 
-    /* Read as much as we have room for. */
-    input.read( cp, boundp - cp );
-    cp += input.gcount();
-  }
+      /* Read as much as we have room for. */
+      input.read( cp, boundp - cp );
+      cp += input.gcount();
+    }
 
-  /* Make sure the fail bit didn't get set. */
-  if( !input.eof() ) {
-    throw InputStreamException("Stream input failed: " + name);
-  }
+    /* Make sure the fail bit didn't get set. */
+    if( !input.eof() ) {
+      throw InputStreamException("Stream input failed: " + name);
+    }
 
-  /* Create an ANTLR input backed by the buffer. */
+    /* Create an ANTLR input backed by the buffer. */
 #ifdef CVC4_ANTLR3_OLD_INPUT_STREAM
-  pANTLR3_INPUT_STREAM inputStream =
+    inputStream =
       antlr3NewAsciiStringInPlaceStream((pANTLR3_UINT8) basep,
                                         cp - basep,
                                         (pANTLR3_UINT8) strdup(name.c_str()));
 #else /* CVC4_ANTLR3_OLD_INPUT_STREAM */
-  pANTLR3_INPUT_STREAM inputStream =
+    inputStream =
       antlr3StringStreamNew((pANTLR3_UINT8) basep,
                             ANTLR3_ENC_8BIT,
                             cp - basep,
                             (pANTLR3_UINT8) strdup(name.c_str()));
 #endif /* CVC4_ANTLR3_OLD_INPUT_STREAM */
-  if( inputStream==NULL ) {
+
+  }
+
+  if( inputStream == NULL ) {
     throw InputStreamException("Couldn't initialize input: " + name);
   }
+
   return new AntlrInputStream( name, inputStream );
 }
 
 
-AntlrInputStream* 
-AntlrInputStream::newStringInputStream(const std::string& input, 
+AntlrInputStream*
+AntlrInputStream::newStringInputStream(const std::string& input,
                                        const std::string& name)
   throw (InputStreamException, AssertionException) {
   char* inputStr = strdup(input.c_str());
@@ -309,6 +331,5 @@ void AntlrInput::setAntlr3Parser(pANTLR3_PARSER pParser) {
       d_parser->rec->mismatch;
 }
 
-
 }/* CVC4::parser namespace */
 }/* CVC4 namespace */
diff --git a/src/parser/antlr_input.h b/src/parser/antlr_input.h
index dca26ab75..a39defd14 100644
--- a/src/parser/antlr_input.h
+++ b/src/parser/antlr_input.h
@@ -77,7 +77,8 @@ public:
 
   /** Create an input from an istream. */
   static AntlrInputStream* newStreamInputStream(std::istream& input, 
-                                                const std::string& name)
+                                                const std::string& name,
+                                                bool lineBuffered = false)
     throw (InputStreamException, AssertionException);
 
   /** Create a string input.
@@ -88,7 +89,7 @@ public:
   static AntlrInputStream* newStringInputStream(const std::string& input, 
                                                 const std::string& name)
     throw (InputStreamException, AssertionException);
-};
+};/* class AntlrInputStream */
 
 class Parser;
 
@@ -209,7 +210,7 @@ protected:
 
   /** Set the Parser object for this input. */
   virtual void setParser(Parser& parser);
-};
+};/* class AntlrInput */
 
 inline std::string AntlrInput::getUnparsedText() {
   const char *base = (const char *)d_antlr3InputStream->data;
diff --git a/src/parser/antlr_line_buffered_input.cpp b/src/parser/antlr_line_buffered_input.cpp
new file mode 100644
index 000000000..b42562f72
--- /dev/null
+++ b/src/parser/antlr_line_buffered_input.cpp
@@ -0,0 +1,379 @@
+/*********************                                                        */
+/*! \file antlr_line_buffered_input.cpp
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include <antlr3.h>
+#include <iostream>
+#include <string>
+
+#include "util/output.h"
+#include "util/Assert.h"
+
+namespace CVC4 {
+namespace parser {
+
+typedef struct ANTLR3_LINE_BUFFERED_INPUT_STREAM {
+  ANTLR3_INPUT_STREAM antlr;
+  std::istream* in;
+} *pANTLR3_LINE_BUFFERED_INPUT_STREAM;
+
+static pANTLR3_INPUT_STREAM    antlr3CreateLineBufferedStream(std::istream& in);
+
+static void
+setupInputStream(pANTLR3_INPUT_STREAM input)
+{
+#if 0
+    ANTLR3_BOOLEAN  isBigEndian;
+
+    // Used to determine the endianness of the machine we are currently
+    // running on.
+    //
+    ANTLR3_UINT16 bomTest = 0xFEFF;
+
+    // What endianess is the machine we are running on? If the incoming
+    // encoding endianess is the same as this machine's natural byte order
+    // then we can use more efficient API calls.
+    //
+    if  (*((pANTLR3_UINT8)(&bomTest)) == 0xFE)
+    {
+        isBigEndian = ANTLR3_TRUE;
+    }
+    else
+    {
+        isBigEndian = ANTLR3_FALSE;
+    }
+
+    // What encoding did the user tell us {s}he thought it was? I am going
+    // to get sick of the questions on antlr-interest, I know I am.
+    //
+    switch  (input->encoding)
+    {
+        case    ANTLR3_ENC_UTF8:
+
+            // See if there is a BOM at the start of this UTF-8 sequence
+            // and just eat it if there is. Windows .TXT files have this for instance
+            // as it identifies UTF-8 even though it is of no consequence for byte order
+            // as UTF-8 does not have a byte order.
+            //
+            if  (       (ANTLR3_UINT8)(*((pANTLR3_UINT8)input->nextChar))      == 0xEF
+                    &&  (ANTLR3_UINT8)(*((pANTLR3_UINT8)input->nextChar+1))    == 0xBB
+                    &&  (ANTLR3_UINT8)(*((pANTLR3_UINT8)input->nextChar+2))    == 0xBF
+                )
+            {
+                // The UTF8 BOM is present so skip it
+                //
+                input->nextChar = (void *)((pANTLR3_UINT8)input->nextChar + 3);
+            }
+
+            // Install the UTF8 input routines
+            //
+            antlr3UTF8SetupStream(input);
+            break;
+
+        case    ANTLR3_ENC_UTF16:
+
+            // See if there is a BOM at the start of the input. If not then
+            // we assume that the byte order is the natural order of this
+            // machine (or it is really UCS2). If there is a BOM we determine if the encoding
+            // is the same as the natural order of this machine.
+            //
+            if  (       (ANTLR3_UINT8)(*((pANTLR3_UINT8)input->nextChar))      == 0xFE
+                    &&  (ANTLR3_UINT8)(*((pANTLR3_UINT8)input->nextChar+1))    == 0xFF
+                )
+            {
+                // BOM Present, indicates Big Endian
+                //
+                input->nextChar = (void *)((pANTLR3_UINT8)input->nextChar + 2);
+
+                antlr3UTF16SetupStream(input, isBigEndian, ANTLR3_TRUE);
+            }
+            else if  (      (ANTLR3_UINT8)(*((pANTLR3_UINT8)input->nextChar))      == 0xFF
+                        &&  (ANTLR3_UINT8)(*((pANTLR3_UINT8)input->nextChar+1))    == 0xFE
+                )
+            {
+                // BOM present, indicates Little Endian
+                //
+                input->nextChar = (void *)((pANTLR3_UINT8)input->nextChar + 2);
+
+                antlr3UTF16SetupStream(input, isBigEndian, ANTLR3_FALSE);
+            }
+            else
+            {
+                // No BOM present, assume local computer byte order
+                //
+                antlr3UTF16SetupStream(input, isBigEndian, isBigEndian);
+            }
+            break;
+
+        case    ANTLR3_ENC_UTF32:
+
+            // See if there is a BOM at the start of the input. If not then
+            // we assume that the byte order is the natural order of this
+            // machine. If there is we determine if the encoding
+            // is the same as the natural order of this machine.
+            //
+            if  (       (ANTLR3_UINT8)(*((pANTLR3_UINT8)input->nextChar))      == 0x00
+                    &&  (ANTLR3_UINT8)(*((pANTLR3_UINT8)input->nextChar+1))    == 0x00
+                    &&  (ANTLR3_UINT8)(*((pANTLR3_UINT8)input->nextChar+2))    == 0xFE
+                    &&  (ANTLR3_UINT8)(*((pANTLR3_UINT8)input->nextChar+3))    == 0xFF
+                )
+            {
+                // BOM Present, indicates Big Endian
+                //
+                input->nextChar = (void *)((pANTLR3_UINT8)input->nextChar + 4);
+
+                antlr3UTF32SetupStream(input, isBigEndian, ANTLR3_TRUE);
+            }
+            else if  (      (ANTLR3_UINT8)(*((pANTLR3_UINT8)input->nextChar))      == 0xFF
+                        &&  (ANTLR3_UINT8)(*((pANTLR3_UINT8)input->nextChar+1))    == 0xFE
+                        &&  (ANTLR3_UINT8)(*((pANTLR3_UINT8)input->nextChar+1))    == 0x00
+                        &&  (ANTLR3_UINT8)(*((pANTLR3_UINT8)input->nextChar+1))    == 0x00
+                )
+            {
+                // BOM present, indicates Little Endian
+                //
+                input->nextChar = (void *)((pANTLR3_UINT8)input->nextChar + 4);
+
+                antlr3UTF32SetupStream(input, isBigEndian, ANTLR3_FALSE);
+            }
+            else
+            {
+                // No BOM present, assume local computer byte order
+                //
+                antlr3UTF32SetupStream(input, isBigEndian, isBigEndian);
+            }
+            break;
+
+        case    ANTLR3_ENC_UTF16BE:
+
+            // Encoding is definately Big Endian with no BOM
+            //
+            antlr3UTF16SetupStream(input, isBigEndian, ANTLR3_TRUE);
+            break;
+
+        case    ANTLR3_ENC_UTF16LE:
+
+            // Encoding is definately Little Endian with no BOM
+            //
+            antlr3UTF16SetupStream(input, isBigEndian, ANTLR3_FALSE);
+            break;
+
+        case    ANTLR3_ENC_UTF32BE:
+
+            // Encoding is definately Big Endian with no BOM
+            //
+            antlr3UTF32SetupStream(input, isBigEndian, ANTLR3_TRUE);
+            break;
+
+        case    ANTLR3_ENC_UTF32LE:
+
+            // Encoding is definately Little Endian with no BOM
+            //
+            antlr3UTF32SetupStream(input, isBigEndian, ANTLR3_FALSE);
+            break;
+
+        case    ANTLR3_ENC_EBCDIC:
+
+            // EBCDIC is basically the same as ASCII but with an on the
+            // fly translation to ASCII
+            //
+            antlr3EBCDICSetupStream(input);
+            break;
+
+        case    ANTLR3_ENC_8BIT:
+        default:
+
+            // Standard 8bit/ASCII
+            //
+            antlr38BitSetupStream(input);
+            break;
+    }
+#endif /* 0 */
+}
+
+static ANTLR3_UCHAR
+myLA(pANTLR3_INT_STREAM is, ANTLR3_INT32 la) {
+    pANTLR3_INPUT_STREAM input;
+
+    input   = ((pANTLR3_INPUT_STREAM) (is->super));
+
+    Debug("pipe") << "LA" << std::endl;
+    if	(( ((pANTLR3_UINT8)input->nextChar) + la - 1) >= (((pANTLR3_UINT8)input->data) + input->sizeBuf))
+    {
+      std::istream& in = *((pANTLR3_LINE_BUFFERED_INPUT_STREAM)input)->in;
+      if(!in) {
+        Debug("pipe") << "EOF" << std::endl;
+        return	ANTLR3_CHARSTREAM_EOF;
+      }
+      Debug("pipe") << "READ" << std::endl;
+      if(input->data == NULL) {
+        Debug("pipe") << "ALLOC" << std::endl;
+        input->data = malloc(1024);
+        input->nextChar = input->data;
+      } else {
+        Debug("pipe") << "REALLOC" << std::endl;
+        size_t pos = (char*)input->nextChar - (char*)input->data;
+        input->data = realloc(input->data, input->sizeBuf + 1024);
+        input->nextChar = (char*)input->data + pos;
+      }
+      in.getline((((char*)input->data) + input->sizeBuf), 1024);
+      while(in.fail() && !in.eof()) {
+        Debug("pipe") << "input string too long, reallocating" << std::endl;
+        input->sizeBuf += strlen(((char*)input->data) + input->sizeBuf);
+        size_t pos = (char*)input->nextChar - (char*)input->data;
+        input->data = realloc(input->data, input->sizeBuf + 1024);
+        input->nextChar = (char*)input->data + pos;
+        in.clear();
+        in.getline((((char*)input->data) + input->sizeBuf), 1024);
+      }
+      input->sizeBuf += strlen(((char*)input->data) + input->sizeBuf);
+      Assert(*(((char*)input->data) + input->sizeBuf) == '\0');
+      Debug("pipe") << "SIZEBUF now " << input->sizeBuf << std::endl;
+      *(((char*)input->data) + input->sizeBuf) = '\n';
+      ++input->sizeBuf;
+    }
+
+    Debug("pipe") << "READ POINTER[" << la << "] AT: >>" << std::string(((char*)input->nextChar), input->sizeBuf - (((char*)input->nextChar) - (char*)input->data) + 1) << "<< returning '" << (char)(*((pANTLR3_UINT8)input->nextChar + la - 1)) << "' (" << (unsigned)(*((pANTLR3_UINT8)input->nextChar + la - 1)) << ")" << std::endl;
+    return	(ANTLR3_UCHAR)(*((pANTLR3_UINT8)input->nextChar + la - 1));
+}
+
+
+static void
+myConsume(pANTLR3_INT_STREAM is)
+{
+    pANTLR3_INPUT_STREAM input;
+
+    input   = ((pANTLR3_INPUT_STREAM) (is->super));
+
+    Debug("pipe") << "consume! '" << *(char*)input->nextChar << "' (" << (unsigned)*(char*)input->nextChar << ")" << std::endl;
+    if	((pANTLR3_UINT8)(input->nextChar) < (((pANTLR3_UINT8)input->data) + input->sizeBuf))
+    {
+	/* Indicate one more character in this line
+	 */
+	input->charPositionInLine++;
+
+	if  ((ANTLR3_UCHAR)(*((pANTLR3_UINT8)input->nextChar)) == input->newlineChar)
+	{
+	    /* Reset for start of a new line of input
+	     */
+	    input->line++;
+	    input->charPositionInLine	= 0;
+	    input->currentLine		= (void *)(((pANTLR3_UINT8)input->nextChar) + 1);
+            Debug("pipe") << "-- newline!" << std::endl;
+	}
+
+	/* Increment to next character position
+	 */
+	input->nextChar = (void *)(((pANTLR3_UINT8)input->nextChar) + 1);
+        Debug("pipe") << "-- advance nextChar! looking at '" << *(char*)input->nextChar << "' (" << (unsigned)*(char*)input->nextChar << ")" << std::endl;
+    } else Debug("pipe") << "-- nothing!" << std::endl;
+}
+
+pANTLR3_INPUT_STREAM
+antlr3LineBufferedStreamNew(std::istream& in, ANTLR3_UINT32 encoding, pANTLR3_UINT8 name)
+{
+    pANTLR3_INPUT_STREAM    input;
+
+    if(!in) {
+      return NULL;
+    }
+
+    // First order of business is to set up the stream and install the data pointer.
+    // Then we will work out the encoding and byte order and adjust the API functions that are installed for the
+    // default 8Bit stream accordingly.
+    //
+    input   = antlr3CreateLineBufferedStream(in);
+    if  (input == NULL)
+    {
+        return NULL;
+    }
+
+    // Size (in bytes) of the given 'string'
+    //
+    input->sizeBuf		= 0;
+
+    input->istream->_LA		= myLA;
+    input->istream->consume	= myConsume;
+
+#ifndef CVC4_ANTLR3_OLD_INPUT_STREAM
+    // We have the data in memory now so we can deal with it according to
+    // the encoding scheme we were given by the user.
+    //
+    input->encoding = encoding;
+#endif /* ! CVC4_ANTLR3_OLD_INPUT_STREAM */
+
+    // Now we need to work out the endian type and install any
+    // API functions that differ from 8Bit
+    //
+    setupInputStream(input);
+
+    // Now we can set up the file name
+    //
+    input->istream->streamName	= input->strFactory->newStr8(input->strFactory, name);
+    input->fileName		= input->istream->streamName;
+
+    return input;
+}
+
+static pANTLR3_INPUT_STREAM
+antlr3CreateLineBufferedStream(std::istream& in)
+{
+	// Pointer to the input stream we are going to create
+	//
+	pANTLR3_INPUT_STREAM    input;
+
+	if	(!in)
+	{
+		return NULL;
+	}
+
+	// Allocate memory for the input stream structure
+	//
+	input   = (pANTLR3_INPUT_STREAM)
+		ANTLR3_CALLOC(1, sizeof(ANTLR3_LINE_BUFFERED_INPUT_STREAM));
+
+	if	(input == NULL)
+	{
+		return	NULL;
+	}
+
+	// Structure was allocated correctly, now we can install the pointer
+	//
+        input->data             = malloc(1024);
+        input->isAllocated	= ANTLR3_FALSE;
+
+        ((pANTLR3_LINE_BUFFERED_INPUT_STREAM)input)->in = &in;
+
+	// Call the common 8 bit input stream handler
+	// initialization.
+	//
+#ifdef CVC4_ANTLR3_OLD_INPUT_STREAM
+	antlr3AsciiSetupStream(input, ANTLR3_CHARSTREAM);
+#else /* CVC4_ANTLR3_OLD_INPUT_STREAM */
+	antlr38BitSetupStream(input);
+        // In some libantlr3c 3.4-beta versions, this call is not included in the above.
+        // This is probably an erroneously-deleted line in the libantlr3c source since 3.2.
+	antlr3GenericSetupStream(input);
+#endif /* CVC4_ANTLR3_OLD_INPUT_STREAM */
+
+        return  input;
+}
+
+}/* CVC4::parser namespace */
+}/* CVC4 namespace */
+
diff --git a/src/parser/antlr_line_buffered_input.h b/src/parser/antlr_line_buffered_input.h
new file mode 100644
index 000000000..b59645dd7
--- /dev/null
+++ b/src/parser/antlr_line_buffered_input.h
@@ -0,0 +1,36 @@
+/*********************                                                        */
+/*! \file antlr_line_buffered_input.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "cvc4parser_private.h"
+
+#ifndef __CVC4__PARSER__ANTLR_LINE_BUFFERED_INPUT_H
+#define __CVC4__PARSER__ANTLR_LINE_BUFFERED_INPUT_H
+
+#include <antlr3.h>
+
+namespace CVC4 {
+namespace parser {
+
+pANTLR3_INPUT_STREAM
+antlr3LineBufferedStreamNew(std::istream& in, ANTLR3_UINT32 encoding, pANTLR3_UINT8 name);
+
+}/* CVC4::parser namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__PARSER__ANTLR_LINE_BUFFERED_INPUT_H */
diff --git a/src/parser/antlr_tracing.h b/src/parser/antlr_tracing.h
index 2c3e66c12..95f6100f4 100644
--- a/src/parser/antlr_tracing.h
+++ b/src/parser/antlr_tracing.h
@@ -54,7 +54,7 @@ static struct __Cvc4System {
   struct JavaPrinter {
     template <class T>
     JavaPrinter operator+(const T& t) const {
-      ::CVC4::Message() << t;
+      Message() << t;
       return JavaPrinter();
     }
   };/* struct JavaPrinter */
@@ -67,7 +67,7 @@ static struct __Cvc4System {
      * to the call-by-value semantics of C.  All that's left to
      * do is print the newline.
      */
-    void println(JavaPrinter) { ::CVC4::Message() << std::endl; }
+    void println(JavaPrinter) { Message() << std::endl; }
   } out;
 } System;
 
diff --git a/src/parser/bounded_token_buffer.cpp b/src/parser/bounded_token_buffer.cpp
index d77f72bfa..d63d3afe0 100644
--- a/src/parser/bounded_token_buffer.cpp
+++ b/src/parser/bounded_token_buffer.cpp
@@ -308,19 +308,19 @@ setTokenSource	(   pANTLR3_TOKEN_STREAM ts,
 static pANTLR3_STRING	    
 toString    (pANTLR3_TOKEN_STREAM ts)
 {
-  Unreachable();
+  Unimplemented("toString(ts)");
 }
 
 static pANTLR3_STRING
 toStringSS(pANTLR3_TOKEN_STREAM ts, ANTLR3_UINT32 start, ANTLR3_UINT32 stop)
 {
-  Unreachable();
+  Unimplemented("toStringSS(ts, %u, %u)", start, stop);
 }
 
 static pANTLR3_STRING	    
 toStringTT  (pANTLR3_TOKEN_STREAM ts, pANTLR3_COMMON_TOKEN start, pANTLR3_COMMON_TOKEN stop)
 {
-  Unreachable();
+  Unimplemented("toStringTT(ts, %u, %u)", start, stop);
 }
 
 /** Move the input pointer to the next incoming token.  The stream
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 9f0c2cddb..657a2fe2c 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -132,9 +132,6 @@ tokens {
   PARENHASH = '(#';
   HASHPAREN = '#)';
 
-  //DOT = '.';
-  DOTDOT = '..';
-
   // Operators
 
   ARROW_TOK = '->';
@@ -198,6 +195,12 @@ tokens {
   BVSGT_TOK = 'BVSGT';
   BVSLE_TOK = 'BVSLE';
   BVSGE_TOK = 'BVSGE';
+
+  // these are parsed by special NUMBER_OR_RANGEOP rule, below
+  DECIMAL_LITERAL;
+  INTEGER_LITERAL;
+  DOT;
+  DOTDOT;
 }/* tokens */
 
 @parser::members {
@@ -312,7 +315,8 @@ Kind getOperatorKind(int type, bool& negate) {
   case PLUS_TOK: return kind::PLUS;
   case MINUS_TOK: return kind::MINUS;
   case STAR_TOK: return kind::MULT;
-  case INTDIV_TOK: Unhandled(CvcParserTokenNames[type]);
+  case INTDIV_TOK: return kind::INTS_DIVISION;
+  case MOD_TOK: return kind::INTS_MODULUS;
   case DIV_TOK: return kind::DIVISION;
   case EXP_TOK: Unhandled(CvcParserTokenNames[type]);
 
@@ -363,9 +367,14 @@ Expr createPrecedenceTree(ExprManager* em,
   unsigned pivot = findPivot(operators, startIndex, stopIndex - 1);
   //Debug("prec") << "pivot[" << startIndex << "," << stopIndex - 1 << "] at " << pivot << std::endl;
   bool negate;
-  Expr e = em->mkExpr(getOperatorKind(operators[pivot], negate),
-                      createPrecedenceTree(em, expressions, operators, startIndex, pivot),
-                      createPrecedenceTree(em, expressions, operators, pivot + 1, stopIndex));
+  Kind k = getOperatorKind(operators[pivot], negate);
+  Expr lhs = createPrecedenceTree(em, expressions, operators, startIndex, pivot);
+  Expr rhs = createPrecedenceTree(em, expressions, operators, pivot + 1, stopIndex);
+  if(k == kind::EQUAL && lhs.getType().isBoolean()) {
+    WarningOnce() << "Warning: converting BOOL = BOOL to BOOL <=> BOOL" << std::endl;
+    k = kind::IFF;
+  }
+  Expr e = em->mkExpr(k, lhs, rhs);
   return negate ? em->mkExpr(kind::NOT, e) : e;
 }/* createPrecedenceTree() recursive variant */
 
@@ -497,6 +506,8 @@ namespace CVC4 {
 #include "util/output.h"
 
 #include <vector>
+#include <string>
+#include <sstream>
 
 #define REPEAT_COMMAND(k, CommandCtor)                      \
   ({                                                        \
@@ -691,8 +702,8 @@ mainCommand[CVC4::Command*& cmd]
     { UNSUPPORTED("CALL command"); }
 
   | ECHO_TOK
-    ( ( str[s] | IDENTIFIER { s = AntlrInput::tokenText($IDENTIFIER); } )
-      { Message() << s << std::endl; }
+    ( simpleSymbolicExpr[sexpr]
+      { Message() << sexpr << std::endl; }
     | { Message() << std::endl; }
     )
 
@@ -732,17 +743,30 @@ mainCommand[CVC4::Command*& cmd]
   | toplevelDeclaration[cmd]
   ;
 
-symbolicExpr[CVC4::SExpr& sexpr]
+simpleSymbolicExpr[CVC4::SExpr& sexpr]
 @declarations {
-  std::vector<SExpr> children;
   std::string s;
+  CVC4::Rational r;
 }
-  : INTEGER_LITERAL ('.' DIGIT+)?
-    { sexpr = SExpr((const char*)$symbolicExpr.text->chars); }
+  : INTEGER_LITERAL
+    { sexpr = SExpr(AntlrInput::tokenText($INTEGER_LITERAL)); }
+  | DECIMAL_LITERAL
+    { sexpr = SExpr(AntlrInput::tokenText($DECIMAL_LITERAL)); }
+  | HEX_LITERAL
+    { sexpr = SExpr(AntlrInput::tokenText($HEX_LITERAL)); }
+  | BINARY_LITERAL
+    { sexpr = SExpr(AntlrInput::tokenText($BINARY_LITERAL)); }
   | str[s]
     { sexpr = SExpr(s); }
   | IDENTIFIER
     { sexpr = SExpr(AntlrInput::tokenText($IDENTIFIER)); }
+  ;
+
+symbolicExpr[CVC4::SExpr& sexpr]
+@declarations {
+  std::vector<SExpr> children;
+}
+  : simpleSymbolicExpr[sexpr]
   | LPAREN (symbolicExpr[sexpr] { children.push_back(sexpr); } )* RPAREN
     { sexpr = SExpr(children); }
   ;
@@ -1020,9 +1044,12 @@ restrictedTypePossiblyFunctionLHS[CVC4::Type& t,
                                   bool& lhs]
 @init {
   Type t2;
-  Expr f;
+  Expr f, f2;
   std::string id;
   std::vector<Type> types;
+  std::vector< std::pair<std::string, Type> > typeIds;
+  DeclarationScope* declScope;
+  Parser* parser;
   lhs = false;
 }
     /* named types */
@@ -1056,24 +1083,33 @@ restrictedTypePossiblyFunctionLHS[CVC4::Type& t,
     { t = EXPR_MANAGER->mkArrayType(t, t2); }
 
     /* subtypes */
-  | SUBTYPE_TOK LPAREN formula[f] ( COMMA formula[f] )? RPAREN
-    { UNSUPPORTED("subtypes not supported yet");
-      t = Type(); }
+  | SUBTYPE_TOK LPAREN
+    /* A bit tricky: this LAMBDA expression cannot refer to constants
+     * declared in the outer context.  What follows isn't quite right,
+     * though, since type aliases and function definitions should be
+     * retained in the set of current declarations. */
+    { /*declScope = PARSER_STATE->getDeclarationScope();
+      PARSER_STATE->useDeclarationsFrom(new DeclarationScope());*/ }
+    formula[f] ( COMMA formula[f2] )? RPAREN
+    { /*DeclarationScope* old = PARSER_STATE->getDeclarationScope();
+      PARSER_STATE->useDeclarationsFrom(declScope);
+      delete old;*/
+      t = f2.isNull() ?
+        EXPR_MANAGER->mkPredicateSubtype(f) :
+        EXPR_MANAGER->mkPredicateSubtype(f, f2);
+    }
 
     /* subrange types */
   | LBRACKET k1=bound DOTDOT k2=bound RBRACKET
-    { std::stringstream ss;
-      ss << "subranges not supported yet: [" << k1 << ":" << k2 << ']';
-      UNSUPPORTED(ss.str());
-      if(k1.hasBound() && k2.hasBound() &&
+    { if(k1.hasBound() && k2.hasBound() &&
          k1.getBound() > k2.getBound()) {
-        ss.str("");
+        std::stringstream ss;
         ss << "Subrange [" << k1.getBound() << ".." << k2.getBound()
            << "] inappropriate: range must be nonempty!";
         PARSER_STATE->parseError(ss.str());
       }
-      Debug("subranges") << ss.str() << std::endl;
-      t = Type(); }
+      t = EXPR_MANAGER->mkSubrangeType(SubrangeBounds(k1, k2));
+    }
 
     /* tuple types / old-style function types */
   | LBRACKET type[t,check] { types.push_back(t); }
@@ -1087,15 +1123,14 @@ restrictedTypePossiblyFunctionLHS[CVC4::Type& t,
         }
       } else {
         // tuple type [ T, U, V... ]
-        t = EXPR_MANAGER->mkTupleType(types);
+        t = PARSER_STATE->mkTupleType(types);
       }
     }
 
     /* record types */
-  | SQHASH identifier[id,CHECK_NONE,SYM_SORT] COLON type[t,check]
-    ( COMMA identifier[id,CHECK_NONE,SYM_SORT] COLON type[t,check] )* HASHSQ
-    { UNSUPPORTED("records not supported yet");
-      t = Type(); }
+  | SQHASH identifier[id,CHECK_NONE,SYM_SORT] COLON type[t,check] { typeIds.push_back(std::make_pair(id, t)); }
+    ( COMMA identifier[id,CHECK_NONE,SYM_SORT] COLON type[t,check] { typeIds.push_back(std::make_pair(id, t)); } )* HASHSQ
+    { t = PARSER_STATE->mkRecordType(typeIds); }
 
     /* bitvector types */
   | BITVECTOR_TOK LPAREN k=numeral RPAREN
@@ -1321,14 +1356,20 @@ arithmeticBinop[unsigned& op]
   | MINUS_TOK
   | STAR_TOK
   | INTDIV_TOK
+  | MOD_TOK
   | DIV_TOK
   | EXP_TOK
   ;
 
-/** Parses an array assignment term. */
+/** Parses an array/tuple/record assignment term. */
 storeTerm[CVC4::Expr& f]
   : uminusTerm[f]
-    ( WITH_TOK arrayStore[f] ( COMMA arrayStore[f] )* )*
+    ( WITH_TOK
+      ( arrayStore[f] ( COMMA arrayStore[f] )*
+      | DOT ( tupleStore[f] ( COMMA DOT tupleStore[f] )*
+            | recordStore[f] ( COMMA DOT recordStore[f] )* ) )
+    | /* nothing */
+    )
   ;
 
 /**
@@ -1361,6 +1402,84 @@ arrayStore[CVC4::Expr& f]
     }
   ;
 
+/**
+ * Parses just part of the tuple assignment (and constructs
+ * the store terms).
+ */
+tupleStore[CVC4::Expr& f]
+@init {
+  Expr f2;
+}
+  : k=numeral ASSIGN_TOK uminusTerm[f2]
+    { 
+      Type t = f.getType();
+      if(! t.isDatatype()) {
+        PARSER_STATE->parseError("tuple-update applied to non-tuple");
+      }
+      Datatype tuple = DatatypeType(f.getType()).getDatatype();
+      if(tuple.getName() != "__cvc4_tuple") {
+        PARSER_STATE->parseError("tuple-update applied to non-tuple");
+      }
+      if(k < tuple[0].getNumArgs()) {
+        std::vector<Expr> args;
+        for(unsigned i = 0; i < tuple[0].getNumArgs(); ++i) {
+          if(i == k) {
+            args.push_back(f2);
+          } else {
+            Expr selectorOp = tuple[0][i].getSelector();
+            Expr select = MK_EXPR(CVC4::kind::APPLY_SELECTOR, selectorOp, f);
+            args.push_back(select);
+          }
+        }
+        f = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, tuple[0].getConstructor(), args);
+      } else {
+        std::stringstream ss;
+        ss << "tuple is of length " << tuple[0].getNumArgs() << "; cannot update index " << k;
+        PARSER_STATE->parseError(ss.str());
+      }
+    }
+  ;
+
+/**
+ * Parses just part of the record assignment (and constructs
+ * the store terms).
+ */
+recordStore[CVC4::Expr& f]
+@init {
+  std::string id;
+  Expr f2;
+}
+  : identifier[id,CHECK_NONE,SYM_VARIABLE] ASSIGN_TOK uminusTerm[f2]
+    { 
+      Type t = f.getType();
+      if(! t.isDatatype()) {
+        PARSER_STATE->parseError("record-update applied to non-record");
+      }
+      Datatype record = DatatypeType(f.getType()).getDatatype();
+      if(record.getName() != "__cvc4_record") {
+        PARSER_STATE->parseError("record-update applied to non-record");
+      }
+      const DatatypeConstructorArg* updateArg;
+      try {
+        updateArg = &record[0][id];
+      } catch(IllegalArgumentException& e) {
+        PARSER_STATE->parseError(std::string("no such field `") + id + "' in record");
+      }
+      std::vector<Expr> args;
+      for(unsigned i = 0; i < record[0].getNumArgs(); ++i) {
+        const DatatypeConstructorArg* thisArg = &record[0][i];
+        if(thisArg == updateArg) {
+          args.push_back(f2);
+        } else {
+          Expr selectorOp = record[0][i].getSelector();
+          Expr select = MK_EXPR(CVC4::kind::APPLY_SELECTOR, selectorOp, f);
+          args.push_back(select);
+        }
+      }
+      f = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, record[0].getConstructor(), args);
+    }
+  ;
+
 /** Parses a unary minus term. */
 uminusTerm[CVC4::Expr& f]
 @init {
@@ -1469,20 +1588,42 @@ postfixTerm[CVC4::Expr& f]
       }
 
       /* record / tuple select */
-    // FIXME - clash in lexer between tuple-select and real; can
-    // resolve with syntactic predicate in ANTLR 3.3, but broken in
-    // 3.2 ?
-    /*| DOT
+    | DOT
       ( identifier[id,CHECK_NONE,SYM_VARIABLE]
-        { UNSUPPORTED("record select not implemented yet");
-          f = Expr(); }
+        { Type t = f.getType();
+          if(! t.isDatatype()) {
+            PARSER_STATE->parseError("record-select applied to non-record");
+          }
+          Datatype record = DatatypeType(f.getType()).getDatatype();
+          if(record.getName() != "__cvc4_record") {
+            PARSER_STATE->parseError("record-select applied to non-record");
+          }
+          try {
+            Expr selectorOp = record[0][id].getSelector();
+            f = MK_EXPR(CVC4::kind::APPLY_SELECTOR, selectorOp, f);
+          } catch(IllegalArgumentException& e) {
+            PARSER_STATE->parseError(std::string("no such field `") + id + "' in record");
+          }
+        }
       | k=numeral
-        { UNSUPPORTED("tuple select not implemented yet");
-          // This will assert-fail if k too big or f not a tuple
-          // that's ok for now, once a TUPLE_SELECT operator exists,
-          // that will do any necessary type checking
-          f = EXPR_MANAGER->mkVar(TupleType(f.getType()).getTypes()[k]); }
-      )*/
+        { Type t = f.getType();
+          if(! t.isDatatype()) {
+            PARSER_STATE->parseError("tuple-select applied to non-tuple");
+          }
+          Datatype tuple = DatatypeType(f.getType()).getDatatype();
+          if(tuple.getName() != "__cvc4_tuple") {
+            PARSER_STATE->parseError("tuple-select applied to non-tuple");
+          }
+          try {
+            Expr selectorOp = tuple[0][k].getSelector();
+            f = MK_EXPR(CVC4::kind::APPLY_SELECTOR, selectorOp, f);
+          } catch(IllegalArgumentException& e) {
+            std::stringstream ss;
+            ss << "tuple is of length " << tuple[0].getNumArgs() << "; cannot access index " << k;
+            PARSER_STATE->parseError(ss.str());
+          }
+        }
+      )
     )*
     ( typeAscription[f, t]
       { if(f.getKind() == CVC4::kind::APPLY_CONSTRUCTOR && t.isDatatype()) {
@@ -1641,6 +1782,8 @@ simpleTerm[CVC4::Expr& f]
 @init {
   std::string name;
   std::vector<Expr> args;
+  std::vector<std::string> names;
+  Expr e;
   Debug("parser-extra") << "term: " << AntlrInput::tokenText(LT(1)) << std::endl;
   Type t;
 }
@@ -1654,7 +1797,12 @@ simpleTerm[CVC4::Expr& f]
         /* If args has elements, we must be a tuple literal.
          * Otherwise, f is already the sub-formula, and
          * there's nothing to do */
-        f = EXPR_MANAGER->mkExpr(kind::TUPLE, args);
+        std::vector<Type> types;
+        for(std::vector<Expr>::const_iterator i = args.begin(); i != args.end(); ++i) {
+          types.push_back((*i).getType());
+        }
+        DatatypeType t = PARSER_STATE->mkTupleType(types);
+        f = EXPR_MANAGER->mkExpr(kind::APPLY_CONSTRUCTOR, t.getDatatype()[0].getConstructor(), args);
       }
     }
 
@@ -1677,9 +1825,16 @@ simpleTerm[CVC4::Expr& f]
       std::string binString = AntlrInput::tokenTextSubstr($BINARY_LITERAL, 4);
       f = MK_CONST( BitVector(binString, 2) ); }
     /* record literals */
-  | PARENHASH recordEntry (COMMA recordEntry)+ HASHPAREN
-    { UNSUPPORTED("records not implemented yet");
-      f = Expr(); }
+  | PARENHASH recordEntry[name,e] { names.push_back(name); args.push_back(e); }
+    ( COMMA recordEntry[name,e] { names.push_back(name); args.push_back(e); } )* HASHPAREN
+    { std::vector< std::pair<std::string, Type> > typeIds;
+      Assert(names.size() == args.size());
+      for(unsigned i = 0; i < names.size(); ++i) {
+        typeIds.push_back(std::make_pair(names[i], args[i].getType()));
+      }
+      DatatypeType t = PARSER_STATE->mkRecordType(typeIds);
+      f = EXPR_MANAGER->mkExpr(kind::APPLY_CONSTRUCTOR, t.getDatatype()[0].getConstructor(), args);
+    }
 
     /* variable / zero-ary constructor application */
   | identifier[name,CHECK_DECLARED,SYM_VARIABLE]
@@ -1707,12 +1862,8 @@ typeAscription[const CVC4::Expr& f, CVC4::Type& t]
 /**
  * Matches an entry in a record literal.
  */
-recordEntry
-@init {
-  std::string id;
-  Expr f;
-}
-  : identifier[id,CHECK_DECLARED,SYM_VARIABLE] ASSIGN_TOK formula[f]
+recordEntry[std::string& name, CVC4::Expr& ex]
+  : identifier[name,CHECK_NONE,SYM_VARIABLE] ASSIGN_TOK formula[ex]
   ;
 
 /**
@@ -1824,22 +1975,6 @@ selector[CVC4::DatatypeConstructor& ctor]
 IDENTIFIER : (ALPHA | '_') (ALPHA | DIGIT | '_' | '\'' | '\\' | '?' | '$' | '~')*;
 
 /**
- * Matches an integer literal.
- */
-INTEGER_LITERAL
-  : ( '0'
-    | '1'..'9' DIGIT*
-    )
-  ;
-
-/**
- * Matches a decimal literal.
- */
-DECIMAL_LITERAL
-  : INTEGER_LITERAL '.' DIGIT+
-  ;
-
-/**
  * Same as an integer literal converted to an unsigned int, but
  * slightly more convenient AND works around a strange ANTLR bug (?)
  * in the BVPLUS/BVMINUS/BVMULT rules where $INTEGER_LITERAL was
@@ -1901,6 +2036,32 @@ fragment ALPHA : 'a'..'z' | 'A'..'Z';
  */
 fragment DIGIT : '0'..'9';
 
+// This rule adapted from http://www.antlr.org/wiki/pages/viewpage.action?pageId=13828121
+// which reportedly comes from Tapestry (http://tapestry.apache.org/tapestry5/)
+//
+// Special rule that uses parsing tricks to identify numbers and ranges; it's all about
+// the dot ('.').
+// Recognizes:
+// '.' as DOT
+// '..' as DOTDOT
+// INTEGER_LITERAL (digit+)
+// DECIMAL_LITERAL (digit* . digit+)
+// Has to watch out for embedded rangeop (i.e. "1..10" is not "1." and ".10").
+//
+// This doesn't ever generate the NUMBER_OR_RANGEOP token, it
+// manipulates the $type inside to return the right token.
+NUMBER_OR_RANGEOP
+  : DIGIT+
+    (
+      { LA(2) != '.' }? => '.' DIGIT* { $type = DECIMAL_LITERAL; }
+      | { $type = INTEGER_LITERAL; }
+    )
+  | '.'
+    ( '.' {$type = DOTDOT; }
+    | {$type = DOT; }
+    )
+  ;
+
 /**
  * Matches the hexidecimal digits (0-9, a-f, A-F)
  */
diff --git a/src/parser/input.cpp b/src/parser/input.cpp
index 70c887371..76aa47812 100644
--- a/src/parser/input.cpp
+++ b/src/parser/input.cpp
@@ -59,25 +59,26 @@ Input* Input::newFileInput(InputLanguage lang,
                            bool useMmap)
   throw (InputStreamException, AssertionException) {
   AntlrInputStream *inputStream = 
-    AntlrInputStream::newFileInputStream(filename,useMmap);
-  return AntlrInput::newInput(lang,*inputStream);
+    AntlrInputStream::newFileInputStream(filename, useMmap);
+  return AntlrInput::newInput(lang, *inputStream);
 }
 
 Input* Input::newStreamInput(InputLanguage lang, 
                              std::istream& input, 
-                             const std::string& name) 
+                             const std::string& name,
+                             bool lineBuffered)
   throw (InputStreamException, AssertionException) {
   AntlrInputStream *inputStream = 
-    AntlrInputStream::newStreamInputStream(input,name);
-  return AntlrInput::newInput(lang,*inputStream);
+    AntlrInputStream::newStreamInputStream(input, name, lineBuffered);
+  return AntlrInput::newInput(lang, *inputStream);
 }
 
 Input* Input::newStringInput(InputLanguage lang,
                              const std::string& str,
                              const std::string& name)
   throw (InputStreamException, AssertionException) {
-  AntlrInputStream *inputStream = AntlrInputStream::newStringInputStream(str,name);
-  return AntlrInput::newInput(lang,*inputStream);
+  AntlrInputStream *inputStream = AntlrInputStream::newStringInputStream(str, name);
+  return AntlrInput::newInput(lang, *inputStream);
 }
 
 }/* CVC4::parser namespace */
diff --git a/src/parser/input.h b/src/parser/input.h
index 25023e1a8..8fa51a095 100644
--- a/src/parser/input.h
+++ b/src/parser/input.h
@@ -110,7 +110,7 @@ public:
     */
   static Input* newFileInput(InputLanguage lang, 
                              const std::string& filename, 
-                             bool useMmap=false)
+                             bool useMmap = false)
     throw (InputStreamException, AssertionException);
 
   /** Create an input for the given stream.
@@ -121,7 +121,8 @@ public:
    */
   static Input* newStreamInput(InputLanguage lang, 
                                std::istream& input, 
-                               const std::string& name) 
+                               const std::string& name,
+                               bool lineBuffered = false)
     throw (InputStreamException, AssertionException);
 
   /** Create an input for the given string
@@ -182,6 +183,7 @@ protected:
 
   /** Set the Parser object for this input. */
   virtual void setParser(Parser& parser) = 0;
+
 };/* class Input */
 
 }/* CVC4::parser namespace */
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 4418ea18f..3efc315cc 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -54,6 +54,7 @@ Parser::Parser(ExprManager* exprManager, Input* input, bool strictMode, bool par
 }
 
 Expr Parser::getSymbol(const std::string& name, SymbolType type) {
+  checkDeclaration(name, CHECK_DECLARED, type);
   Assert( isDeclared(name, type) );
 
   switch( type ) {
@@ -77,12 +78,14 @@ Expr Parser::getFunction(const std::string& name) {
 
 Type Parser::getType(const std::string& var_name,
                      SymbolType type) {
+  checkDeclaration(var_name, CHECK_DECLARED, type);
   Assert( isDeclared(var_name, type) );
   Type t = getSymbol(var_name, type).getType();
   return t;
 }
 
 Type Parser::getSort(const std::string& name) {
+  checkDeclaration(name, CHECK_DECLARED, SYM_SORT);
   Assert( isDeclared(name, SYM_SORT) );
   Type t = d_declScope->lookupType(name);
   return t;
@@ -90,12 +93,14 @@ Type Parser::getSort(const std::string& name) {
 
 Type Parser::getSort(const std::string& name,
                      const std::vector<Type>& params) {
+  checkDeclaration(name, CHECK_DECLARED, SYM_SORT);
   Assert( isDeclared(name, SYM_SORT) );
   Type t = d_declScope->lookupType(name, params);
   return t;
 }
 
 size_t Parser::getArity(const std::string& sort_name){
+  checkDeclaration(sort_name, CHECK_DECLARED, SYM_SORT);
   Assert( isDeclared(sort_name, SYM_SORT) );
   return d_declScope->lookupArity(sort_name);
 }
@@ -236,7 +241,7 @@ SortType Parser::mkUnresolvedType(const std::string& name) {
 SortConstructorType
 Parser::mkUnresolvedTypeConstructor(const std::string& name,
                                     size_t arity) {
-  SortConstructorType unresolved = mkSortConstructor(name,arity);
+  SortConstructorType unresolved = mkSortConstructor(name, arity);
   d_unresolved.insert(unresolved);
   return unresolved;
 }
@@ -325,6 +330,37 @@ Parser::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes) {
   return types;
 }
 
+DatatypeType Parser::mkRecordType(const std::vector< std::pair<std::string, Type> >& typeIds) {
+  DatatypeType& dtt = d_recordTypes[typeIds];
+  if(dtt.isNull()) {
+    Datatype dt("__cvc4_record");
+Debug("datatypes") << "make new record_ctor" << std::endl;
+    DatatypeConstructor c("__cvc4_record_ctor");
+    for(std::vector< std::pair<std::string, Type> >::const_iterator i = typeIds.begin(); i != typeIds.end(); ++i) {
+      c.addArg((*i).first, (*i).second);
+    }
+    dt.addConstructor(c);
+    dtt = d_exprManager->mkDatatypeType(dt);
+  } else {
+Debug("datatypes") << "use old record_ctor" << std::endl;
+}
+  return dtt;
+}
+
+DatatypeType Parser::mkTupleType(const std::vector<Type>& types) {
+  DatatypeType& dtt = d_tupleTypes[types];
+  if(dtt.isNull()) {
+    Datatype dt("__cvc4_tuple");
+    DatatypeConstructor c("__cvc4_tuple_ctor");
+    for(std::vector<Type>::const_iterator i = types.begin(); i != types.end(); ++i) {
+      c.addArg("__cvc4_tuple_stor", *i);
+    }
+    dt.addConstructor(c);
+    dtt = d_exprManager->mkDatatypeType(dt);
+  }
+  return dtt;
+}
+
 bool Parser::isDeclared(const std::string& name, SymbolType type) {
   switch(type) {
   case SYM_VARIABLE:
diff --git a/src/parser/parser.h b/src/parser/parser.h
index 70bd45c31..405e397b8 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -142,6 +142,20 @@ class CVC4_PUBLIC Parser {
   /** Are we only parsing? */
   bool d_parseOnly;
 
+  /**
+   * We might see the same record type multiple times; we have
+   * to match always to the same Type.  This map contains all the
+   * record types we have.
+   */
+  std::map<std::vector< std::pair<std::string, Type> >, DatatypeType> d_recordTypes;
+
+  /**
+   * We might see the same tuple type multiple times; we have
+   * to match always to the same Type.  This map contains all the
+   * tuple types we have.
+   */
+  std::map<std::vector<Type>, DatatypeType> d_tupleTypes;
+
   /** The set of operators available in the current logic. */
   std::set<Kind> d_logicOperators;
 
@@ -399,6 +413,16 @@ public:
   mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes);
 
   /**
+   * Create a record type, or if there's already a matching one, return that one.
+   */
+  DatatypeType mkRecordType(const std::vector< std::pair<std::string, Type> >& typeIds);
+
+  /**
+   * Create a tuple type, or if there's already a matching one, return that one.
+   */
+  DatatypeType mkTupleType(const std::vector<Type>& types);
+
+  /**
    * Add an operator to the current legal set.
    *
    * @param kind the built-in operator to add
@@ -494,6 +518,14 @@ public:
     }
   }
 
+  inline void useDeclarationsFrom(DeclarationScope* scope) {
+    d_declScope = scope;
+  }
+
+  inline DeclarationScope* getDeclarationScope() const {
+    return d_declScope;
+  }
+
   /**
    * Gets the current declaration level.
    */
diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp
index c17956e62..dff5b93ac 100644
--- a/src/parser/parser_builder.cpp
+++ b/src/parser/parser_builder.cpp
@@ -66,6 +66,11 @@ Parser* ParserBuilder::build()
   case FILE_INPUT:
     input = Input::newFileInput(d_lang, d_filename, d_mmap);
     break;
+  case LINE_BUFFERED_STREAM_INPUT:
+    AlwaysAssert( d_streamInput != NULL,
+                  "Uninitialized stream input in ParserBuilder::build()" );
+    input = Input::newStreamInput(d_lang, *d_streamInput, d_filename, true);
+    break;
   case STREAM_INPUT:
     AlwaysAssert( d_streamInput != NULL,
                   "Uninitialized stream input in ParserBuilder::build()" );
@@ -155,6 +160,12 @@ ParserBuilder& ParserBuilder::withStreamInput(std::istream& input) {
   return *this;
 }
 
+ParserBuilder& ParserBuilder::withLineBufferedStreamInput(std::istream& input) {
+  d_inputType = LINE_BUFFERED_STREAM_INPUT;
+  d_streamInput = &input;
+  return *this;
+}
+
 ParserBuilder& ParserBuilder::withStringInput(const std::string& input) {
   d_inputType = STRING_INPUT;
   d_stringInput = input;
diff --git a/src/parser/parser_builder.h b/src/parser/parser_builder.h
index ce01d3c53..095769ab5 100644
--- a/src/parser/parser_builder.h
+++ b/src/parser/parser_builder.h
@@ -44,6 +44,7 @@ class Parser;
 class CVC4_PUBLIC ParserBuilder {
   enum InputType {
     FILE_INPUT,
+    LINE_BUFFERED_STREAM_INPUT,
     STREAM_INPUT,
     STRING_INPUT
   };
@@ -90,7 +91,7 @@ public:
                 const Options& options);
 
   /** Build the parser, using the current settings. */
-  Parser *build() throw (InputStreamException,AssertionException);
+  Parser *build() throw (InputStreamException, AssertionException);
 
   /** Should semantic checks be enabled in the parser? (Default: yes) */
   ParserBuilder& withChecks(bool flag = true);
@@ -150,6 +151,9 @@ public:
   /** Set the parser to use the given stream for its input. */
   ParserBuilder& withStreamInput(std::istream& input);
 
+  /** Set the parser to use the given stream for its input. */
+  ParserBuilder& withLineBufferedStreamInput(std::istream& input);
+
   /** Set the parser to use the given string for its input. */
   ParserBuilder& withStringInput(const std::string& input);
 };/* class ParserBuilder */
diff --git a/src/parser/smt/smt.cpp b/src/parser/smt/smt.cpp
index 0ee6944d4..508bfe352 100644
--- a/src/parser/smt/smt.cpp
+++ b/src/parser/smt/smt.cpp
@@ -41,6 +41,9 @@ std::hash_map<const std::string, Smt::Logic, CVC4::StringHashFunction> Smt::newL
   logicMap["QF_UFIDL"] = QF_UFIDL;
   logicMap["QF_UFLRA"] = QF_UFLRA;
   logicMap["QF_UFLIA"] = QF_UFLIA;
+  logicMap["QF_UFLIRA"] = QF_UFLIRA;
+  logicMap["QF_UFNIA"] = QF_UFNIA;
+  logicMap["QF_UFNIRA"] = QF_UFNIRA;
   logicMap["QF_AUFLIA"] = QF_AUFLIA;
   logicMap["QF_AUFLIRA"] = QF_AUFLIRA;
   return logicMap;
@@ -159,6 +162,7 @@ void Smt::setLogic(const std::string& name) {
 
   case QF_UFIDL:
   case QF_UFLIA:
+  case QF_UFNIA:// nonstandard logic
     addTheory(THEORY_INTS);
     addUf();
     break;
@@ -169,6 +173,13 @@ void Smt::setLogic(const std::string& name) {
     addUf();
     break;
 
+  case QF_UFLIRA:// nonstandard logic
+  case QF_UFNIRA:// nonstandard logic
+    addTheory(THEORY_INTS);
+    addTheory(THEORY_REALS);
+    addUf();
+    break;
+
   case QF_UF:
     addUf();
     break;
diff --git a/src/parser/smt/smt.h b/src/parser/smt/smt.h
index a99f81998..62bb24336 100644
--- a/src/parser/smt/smt.h
+++ b/src/parser/smt/smt.h
@@ -54,7 +54,10 @@ public:
     QF_UF,
     QF_UFIDL,
     QF_UFLIA,
+    QF_UFNIA, // nonstandard
     QF_UFLRA,
+    QF_UFLIRA, // nonstandard
+    QF_UFNIRA, // nonstandard
     QF_UFNRA,
     UFNIA
   };
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 791e550b9..926ce1718 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -67,7 +67,6 @@ options {
 
 #include "parser/smt2/smt2.h"
 #include "parser/antlr_input.h"
-#include "parser/antlr_tracing.h"
 
 using namespace CVC4;
 using namespace CVC4::parser;
@@ -79,6 +78,7 @@ using namespace CVC4::parser;
 @parser::includes {
 #include "expr/command.h"
 #include "parser/parser.h"
+#include "parser/antlr_tracing.h"
 
 namespace CVC4 {
   class Expr;
@@ -358,7 +358,12 @@ command returns [CVC4::Command* cmd = NULL]
 extendedCommand[CVC4::Command*& cmd]
 @declarations {
   std::vector<CVC4::Datatype> dts;
+  Type t;
   Expr e;
+  SExpr sexpr;
+  std::string name;
+  std::vector<std::string> names;
+  std::vector<Type> sorts;
 }
     /* Z3's extended SMT-LIBv2 set of commands syntax */
   : DECLARE_DATATYPES_TOK
@@ -368,33 +373,43 @@ extendedCommand[CVC4::Command*& cmd]
     { PARSER_STATE->popScope();
       cmd = new DatatypeDeclarationCommand(PARSER_STATE->mkMutualDatatypeTypes(dts)); }
 
-    
   | DECLARE_SORTS_TOK
   | DECLARE_FUNS_TOK
+    LPAREN_TOK
+    ( LPAREN_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] nonemptySortList[sorts] RPAREN_TOK )+
+    RPAREN_TOK
   | DECLARE_PREDS_TOK
-  | DEFINE_TOK
+    LPAREN_TOK
+    ( LPAREN_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] sortList[sorts] RPAREN_TOK )+
+    RPAREN_TOK
+  | DEFINE_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] term[e]
   | DEFINE_SORTS_TOK
-  | DECLARE_CONST_TOK
-    
+    LPAREN_TOK
+    ( LPAREN_TOK ( symbol[name,CHECK_UNDECLARED,SYM_SORT] LPAREN_TOK symbolList[names,CHECK_NONE,SYM_SORT] RPAREN_TOK |
+                   symbol[name,CHECK_UNDECLARED,SYM_SORT] symbol[name,CHECK_NONE,SYM_SORT] ) RPAREN_TOK RPAREN_TOK )+
+    RPAREN_TOK
+  | DECLARE_CONST_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] sortSymbol[t,CHECK_DECLARED]
+
   | SIMPLIFY_TOK term[e]
     { cmd = new SimplifyCommand(e); }
   | ECHO_TOK
-    ( STRING_LITERAL
-      { Message() << AntlrInput::tokenText($STRING_LITERAL) << std::endl; }
+    ( simpleSymbolicExpr[sexpr]
+      { Message() << sexpr << std::endl; }
     | { Message() << std::endl; } )
+    { cmd = new EmptyCommand; }
   ;
 
-symbolicExpr[CVC4::SExpr& sexpr]
+simpleSymbolicExpr[CVC4::SExpr& sexpr]
 @declarations {
-  std::vector<SExpr> children;
   CVC4::Kind k;
+  std::string s;
 }
   : INTEGER_LITERAL
     { sexpr = SExpr(AntlrInput::tokenText($INTEGER_LITERAL)); }
   | DECIMAL_LITERAL
     { sexpr = SExpr(AntlrInput::tokenText($DECIMAL_LITERAL)); }
-  | STRING_LITERAL
-    { sexpr = SExpr(AntlrInput::tokenText($STRING_LITERAL)); }
+  | str[s]
+    { sexpr = SExpr(s); }
   | SYMBOL
     { sexpr = SExpr(AntlrInput::tokenText($SYMBOL)); }
   | builtinOp[k]
@@ -404,6 +419,13 @@ symbolicExpr[CVC4::SExpr& sexpr]
     }
   | KEYWORD
     { sexpr = SExpr(AntlrInput::tokenText($KEYWORD)); }
+  ;
+
+symbolicExpr[CVC4::SExpr& sexpr]
+@declarations {
+  std::vector<SExpr> children;
+}
+  : simpleSymbolicExpr[sexpr]
   | LPAREN_TOK
     (symbolicExpr[sexpr] { children.push_back(sexpr); } )*
   	RPAREN_TOK
@@ -611,6 +633,17 @@ termList[std::vector<CVC4::Expr>& formulas, CVC4::Expr& expr]
   ;
 
 /**
+ * Matches a string, and strips off the quotes.
+ */
+str[std::string& s]
+  : STRING_LITERAL
+    { s = AntlrInput::tokenText($STRING_LITERAL);
+      /* strip off the quotes */
+      s = s.substr(1, s.size() - 2);
+    }
+  ;
+
+/**
 * Matches a builtin operator symbol and sets kind to its associated Expr kind.
 */
 builtinOp[CVC4::Kind& kind]
@@ -637,6 +670,8 @@ builtinOp[CVC4::Kind& kind]
   | MINUS_TOK    { $kind = CVC4::kind::MINUS; }
   | STAR_TOK     { $kind = CVC4::kind::MULT; }
   | DIV_TOK      { $kind = CVC4::kind::DIVISION; }
+  | INTS_DIV_TOK      { $kind = CVC4::kind::INTS_DIVISION; }
+  | INTS_MOD_TOK      { $kind = CVC4::kind::INTS_MODULUS; }
 
   | SELECT_TOK   { $kind = CVC4::kind::SELECT; }
   | STORE_TOK    { $kind = CVC4::kind::STORE; }
@@ -705,6 +740,13 @@ sortList[std::vector<CVC4::Type>& sorts]
   : ( sortSymbol[t,CHECK_DECLARED] { sorts.push_back(t); } )*
   ;
 
+nonemptySortList[std::vector<CVC4::Type>& sorts]
+@declarations {
+  Type t;
+}
+  : ( sortSymbol[t,CHECK_DECLARED] { sorts.push_back(t); } )+
+  ;
+
 /**
  * Matches a sequence of (variable,sort) symbol pairs and fills them
  * into the given vector.
@@ -937,6 +979,9 @@ STORE_TOK         : 'store';
 // TILDE_TOK         : '~';
 XOR_TOK           : 'xor';
 
+INTS_DIV_TOK : 'div';
+INTS_MOD_TOK : 'mod';
+
 CONCAT_TOK : 'concat';
 BVNOT_TOK : 'bvnot';
 BVAND_TOK : 'bvand';
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 7d6f27aa5..39eaf5b95 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -127,6 +127,7 @@ void Smt2::setLogic(const std::string& name) {
 
   case Smt::QF_UFIDL:
   case Smt::QF_UFLIA:
+  case Smt::QF_UFNIA:// nonstandard logic
     addTheory(THEORY_INTS);
     addOperator(kind::APPLY_UF);
     break;
@@ -137,6 +138,13 @@ void Smt2::setLogic(const std::string& name) {
     addOperator(kind::APPLY_UF);
     break;
 
+  case Smt::QF_UFLIRA:// nonstandard logic
+  case Smt::QF_UFNIRA:// nonstandard logic
+    addOperator(kind::APPLY_UF);
+    addTheory(THEORY_INTS);
+    addTheory(THEORY_REALS);
+    break;
+
   case Smt::QF_BV:
     addTheory(THEORY_BITVECTORS);
     break;
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 283cdd725..04690f500 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -94,7 +94,11 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
       break;
     case kind::CONST_RATIONAL: {
       const Rational& rat = n.getConst<Rational>();
-      out << '(' << rat.getNumerator() << '/' << rat.getDenominator() << ')';
+      if(rat.getDenominator() == 1) {
+        out << rat.getNumerator();
+      } else {
+        out << '(' << rat.getNumerator() << '/' << rat.getDenominator() << ')';
+      }
       break;
     }
     case kind::CONST_INTEGER: {
@@ -107,6 +111,12 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
       out << num;
       break;
     }
+    case kind::SUBRANGE_TYPE:
+      out << '[' << n.getConst<SubrangeBounds>() << ']';
+      break;
+    case kind::SUBTYPE_TYPE:
+      out << "SUBTYPE(" << n.getConst<Predicate>() << ")";
+      break;
     case kind::TYPE_CONSTANT:
       switch(TypeConstant tc = n.getConst<TypeConstant>()) {
       case REAL_TYPE:
@@ -129,6 +139,7 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
         break;
       }
       break;
+
     default:
       Warning() << "Constant printing not implemented for the case of " << n.getKind() << endl;
       out << n.getKind();
@@ -340,6 +351,14 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
       op << '/';
       opType = INFIX;
       break;
+    case kind::INTS_DIVISION:
+      op << "DIV";
+      opType = INFIX;
+      break;
+    case kind::INTS_MODULUS:
+      op << "MOD";
+      opType = INFIX;
+      break;
     case kind::LT:
       op << '<';
       opType = INFIX;
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 393ad664b..691e96ed7 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -127,6 +127,19 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
       break;
     }
 
+    case kind::SUBRANGE_TYPE: {
+      const SubrangeBounds& bounds = n.getConst<SubrangeBounds>();
+      // No way to represent subranges in SMT-LIBv2; this is inspired
+      // by yices format (but isn't identical to it).
+      out << "(subrange " << bounds.lower << ' ' << bounds.upper << ')';
+      break;
+    }
+    case kind::SUBTYPE_TYPE:
+      // No way to represent predicate subtypes in SMT-LIBv2; this is
+      // inspired by yices format (but isn't identical to it).
+      out << "(subtype " << n.getConst<Predicate>() << ')';
+      break;
+
     default:
       // fall back on whatever operator<< does on underlying type; we
       // might luck out and be SMT-LIB v2 compliant
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index 9f49d81a2..396454fac 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -50,9 +50,19 @@ CnfStream::CnfStream(SatSolverInterface *satSolver, Registrar* registrar, bool f
   d_registrar(registrar) {
 }
 
-void CnfStream::recordTranslation(TNode node) {
+void CnfStream::recordTranslation(TNode node, bool alwaysRecord) {
+  Debug("cnf") << "recordTranslation(" << alwaysRecord << "," << d_removable << "): " << node << std::endl;
   if (!d_removable) {
-    d_translationTrail.push_back(stripNot(node));
+    node = stripNot(node);
+    if(d_translationCache.find(node)->second.recorded) {
+      Debug("cnf") << "--> Already recorded, not recording again." << std::endl;
+    } else {
+      Debug("cnf") << "--> Recorded at position " << d_translationTrail.size() << ". (level " << d_translationCache.find(node)->second.level << ")" << std::endl;
+      Assert(d_translationTrail.empty() || d_translationCache.find(node)->second.level >= d_translationCache.find(d_translationTrail.back())->second.level, "levels on the translation trail should be monotonically increasing ?!");
+      d_translationTrail.push_back(node);
+      d_translationCache.find(node)->second.recorded = true;
+      d_translationCache.find(node.notNode())->second.recorded = true;
+    }
   }
 }
 
@@ -112,7 +122,8 @@ bool CnfStream::hasLiteral(TNode n) const {
 void TseitinCnfStream::ensureLiteral(TNode n) {
   if(hasLiteral(n)) {
     // Already a literal!
-    SatLiteral lit = getLiteral(n);
+    // newLiteral() may be necessary to renew a previously-extant literal
+    SatLiteral lit = isTranslated(n) ? getLiteral(n) : newLiteral(n, true);
     NodeCache::iterator i = d_nodeCache.find(lit);
     if(i == d_nodeCache.end()) {
       // Store backward-mappings
@@ -158,11 +169,12 @@ void TseitinCnfStream::ensureLiteral(TNode n) {
 
 SatLiteral CnfStream::newLiteral(TNode node, bool theoryLiteral) {
   Debug("cnf") << "newLiteral(" << node << ", " << theoryLiteral << ")" << endl;
+  Assert(node.getKind() != kind::NOT);
 
   // Get the literal for this node
   SatLiteral lit;
   if (!hasLiteral(node)) {
-    // If no literal, well make one
+    // If no literal, we'll make one
     lit = SatLiteral(d_satSolver->newVar(theoryLiteral));
     d_translationCache[node].literal = lit;
     d_translationCache[node.notNode()].literal = ~lit;
@@ -174,13 +186,15 @@ SatLiteral CnfStream::newLiteral(TNode node, bool theoryLiteral) {
 
   // We will translate clauses, so remember the level
   int level = d_satSolver->getAssertionLevel();
+  d_translationCache[node].recorded = false;
+  d_translationCache[node.notNode()].recorded = false;
   d_translationCache[node].level = level;
   d_translationCache[node.notNode()].level = level;
 
   // If it's a theory literal, need to store it for back queries
   if ( theoryLiteral || d_fullLitToNodeMap ||
        ( CVC4_USE_REPLAY && Options::current()->replayLog != NULL ) ||
-       Dump.isOn("clauses") ) {
+       (Dump.isOn("clauses")) ) {
     d_nodeCache[lit] = node;
     d_nodeCache[~lit] = node.notNode();
   }
@@ -223,6 +237,11 @@ SatLiteral CnfStream::convertAtom(TNode node) {
     }
   }
 
+  // We have a literal, so it has to be recorded.  The definitional clauses
+  // go away on user-pop, so this literal will have to be re-vivified if it's
+  // used subsequently.
+  recordTranslation(node, true);
+
   return lit;
 }
 
@@ -250,6 +269,11 @@ SatLiteral TseitinCnfStream::handleXor(TNode xorNode) {
   assertClause(xorNode, a, ~b, xorLit);
   assertClause(xorNode, ~a, b, xorLit);
 
+  // We have a literal, so it has to be recorded.  The definitional clauses
+  // go away on user-pop, so this literal will have to be re-vivified if it's
+  // used subsequently.
+  recordTranslation(xorNode, true);
+
   return xorLit;
 }
 
@@ -285,6 +309,11 @@ SatLiteral TseitinCnfStream::handleOr(TNode orNode) {
   // This needs to go last, as the clause might get modified by the SAT solver
   assertClause(orNode, clause);
 
+  // We have a literal, so it has to be recorded.  The definitional clauses
+  // go away on user-pop, so this literal will have to be re-vivified if it's
+  // used subsequently.
+  recordTranslation(orNode, true);
+
   // Return the literal
   return orLit;
 }
@@ -321,6 +350,12 @@ SatLiteral TseitinCnfStream::handleAnd(TNode andNode) {
   clause[n_children] = andLit;
   // This needs to go last, as the clause might get modified by the SAT solver
   assertClause(andNode, clause);
+
+  // We have a literal, so it has to be recorded.  The definitional clauses
+  // go away on user-pop, so this literal will have to be re-vivified if it's
+  // used subsequently.
+  recordTranslation(andNode, true);
+
   return andLit;
 }
 
@@ -345,6 +380,11 @@ SatLiteral TseitinCnfStream::handleImplies(TNode impliesNode) {
   assertClause(impliesNode, a, impliesLit);
   assertClause(impliesNode, ~b, impliesLit);
 
+  // We have a literal, so it has to be recorded.  The definitional clauses
+  // go away on user-pop, so this literal will have to be re-vivified if it's
+  // used subsequently.
+  recordTranslation(impliesNode, true);
+
   return impliesLit;
 }
 
@@ -377,6 +417,11 @@ SatLiteral TseitinCnfStream::handleIff(TNode iffNode) {
   assertClause(iffNode, ~a, ~b, iffLit);
   assertClause(iffNode, a, b, iffLit);
 
+  // We have a literal, so it has to be recorded.  The definitional clauses
+  // go away on user-pop, so this literal will have to be re-vivified if it's
+  // used subsequently.
+  recordTranslation(iffNode, true);
+
   return iffLit;
 }
 
@@ -423,6 +468,11 @@ SatLiteral TseitinCnfStream::handleIte(TNode iteNode) {
   assertClause(iteNode, iteLit, ~condLit, ~thenLit);
   assertClause(iteNode, iteLit, condLit, ~elseLit);
 
+  // We have a literal, so it has to be recorded.  The definitional clauses
+  // go away on user-pop, so this literal will have to be re-vivified if it's
+  // used subsequently.
+  recordTranslation(iteNode, true);
+
   return iteLit;
 }
 
@@ -435,6 +485,7 @@ SatLiteral TseitinCnfStream::toCNF(TNode node, bool negated) {
 
   // If the non-negated node has already been translated, get the translation
   if(isTranslated(node)) {
+    Debug("cnf") << "toCNF(): already translated" << endl;
     nodeLit = getLiteral(node);
   } else {
     // Handle each Boolean operator case
@@ -690,15 +741,19 @@ void TseitinCnfStream::convertAndAssert(TNode node, bool negated) {
 
 void CnfStream::removeClausesAboveLevel(int level) {
   while (d_translationTrail.size() > 0) {
+    Debug("cnf") << "Considering translation trail position " << d_translationTrail.size() << std::endl;
     TNode node = d_translationTrail.back();
+    // Get the translation information
+    TranslationInfo& infoPos = d_translationCache.find(node)->second;
+    // If the level of the node is less or equal to given we are done
+    if (infoPos.level >= 0 && infoPos.level <= level) {
+      Debug("cnf") << "Node is " << node << " level " << infoPos.level << ", we're done." << std::endl;
+      break;
+    }
     Debug("cnf") << "Removing node " << node << " from CNF translation" << endl;
     d_translationTrail.pop_back();
-    // Get the translation informations
-    TranslationInfo& infoPos = d_translationCache.find(node)->second;
     // If already untranslated, we're done
     if (infoPos.level == -1) continue;
-    // If the level of the node is less or equal to given we are done
-    if (infoPos.level <= level) break;
     // Otherwise we have to undo the translation
     undoTranslate(node, level);
   }
@@ -734,6 +789,7 @@ void CnfStream::undoTranslate(TNode node, int level) {
 
   // Untranslate
   infoPos.level = -1;
+  infoPos.recorded = false;
 
   // Untranslate the negation node
   // If not a not node, unregister it from sat and untranslate the negation
@@ -747,6 +803,7 @@ void CnfStream::undoTranslate(TNode node, int level) {
     Assert(it != d_translationCache.end());
     TranslationInfo& infoNeg = (*it).second;
     infoNeg.level = -1;
+    infoNeg.recorded = false;
   }
 
   // undoTranslate the children
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index c9306952b..4812c6a21 100644
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -52,6 +52,7 @@ public:
 
   /** Per node translation information */
   struct TranslationInfo {
+    bool recorded;
     /** The level at which this node was translated (negative if not translated) */
     int level;
     /** The literal of this node */
@@ -109,7 +110,7 @@ protected:
   }
 
   /** Record this translation */
-  void recordTranslation(TNode node);
+  void recordTranslation(TNode node, bool alwaysRecord = false);
 
   /**
    * Moves the node and all of it's parents to level 0.
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 3fe9db10c..678fe28dc 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -714,10 +714,11 @@ CRef Solver::propagate(TheoryCheckType type)
 }
 
 void Solver::propagateTheory() {
-
-  SatClause propagatedLiteralsClause; 
+  SatClause propagatedLiteralsClause;
+  // Doesn't actually call propagate(); that's done in theoryCheck() now that combination
+  // is online.  This just incorporates those propagations previously discovered.
   proxy->theoryPropagate(propagatedLiteralsClause);
-  
+
   vec<Lit> propagatedLiterals;
   DPLLMinisatSatSolver::toMinisatClause(propagatedLiteralsClause, propagatedLiterals); 
 
@@ -885,10 +886,22 @@ void Solver::removeClausesAboveLevel(vec<CRef>& cs, int level)
     for (i = j = 0; i < cs.size(); i++){
         Clause& c = ca[cs[i]];
         if (c.level() > level) {
-            Debug("minisat") << "removeClausesAboveLevel(" << level << "): removing level-" << c.level() << " clause: " << c << std::endl;
+            if(Debug.isOn("minisat")) {
+              Debug("minisat") << "removeClausesAboveLevel(" << level << "): removing level-" << c.level() << " clause: " << c << ":";
+              for(int i = 0; i < c.size(); ++i) {
+                Debug("minisat") << " " << c[i];
+              }
+              Debug("minisat") << std::endl;
+            }
             removeClause(cs[i]);
         } else {
-            Debug("minisat") << "removeClausesAboveLevel(" << level << "): leaving level-" << c.level() << " clause: " << c << std::endl;
+            if(Debug.isOn("minisat")) {
+              Debug("minisat") << "removeClausesAboveLevel(" << level << "): leaving level-" << c.level() << " clause: " << c << ":";
+              for(int i = 0; i < c.size(); ++i) {
+                Debug("minisat") << " " << c[i];
+              }
+              Debug("minisat") << std::endl;
+            }
             cs[j++] = cs[i];
         }
     }
@@ -1328,16 +1341,25 @@ void Solver::push()
   Debug("minisat") << "in user push, increasing assertion level to " << assertionLevel << std::endl;
   trail_user.push(lit_Undef);
   trail_ok.push(ok);
+  trail_user_lim.push(trail.size());
+  assert(trail_user_lim.size() == assertionLevel);
+  Debug("minisat") << "MINISAT PUSH assertionLevel is " << assertionLevel << ", trail.size is " << trail.size() << std::endl;
 }
 
 void Solver::pop()
 {
   assert(enable_incremental);
 
+  Debug("minisat") << "MINISAT POP at level " << decisionLevel() << " (context " << context->getLevel() << "), popping trail..." << std::endl;
   popTrail();
+  Debug("minisat") << "MINISAT POP now at   " << decisionLevel() << " (context " << context->getLevel() << ")" << std::endl;
+ 
+  assert(decisionLevel() == 0);
+  assert(trail_user_lim.size() == assertionLevel);
 
   --assertionLevel;
 
+  Debug("minisat") << "MINISAT POP assertionLevel is now down to " << assertionLevel << ", trail.size is " << trail.size() << ", need to get down to " << trail_user_lim.last() << std::endl;
   Debug("minisat") << "in user pop, reducing assertion level to " << assertionLevel << " and removing clauses above this from db" << std::endl;
 
   // Remove all the clauses asserted (and implied) above the new base level
@@ -1346,6 +1368,23 @@ void Solver::pop()
 
   Debug("minisat") << "in user pop, at " << trail_lim.size() << " : " << assertionLevel << std::endl;
 
+  int downto = trail_user_lim.last();
+  while(downto < trail.size()) {
+    Debug("minisat") << "== unassigning " << trail.last() << std::endl;
+    Var      x  = var(trail.last());
+    if(intro_level(x) != -1) {// might be unregistered
+      assigns [x] = l_Undef;
+      vardata[x].trail_index = -1;
+      polarity[x] = sign(trail.last());
+      insertVarOrder(x);
+    }
+    trail.pop();
+  }
+  qhead = trail.size();
+  Debug("minisat") << "MINISAT POP assertionLevel is now down to " << assertionLevel << ", trail.size is " << trail.size() << ", should be at " << trail_user_lim.last() << std::endl;
+  assert(trail_user_lim.last() == qhead);
+  trail_user_lim.pop();
+
   // Unset any units learned or added at this level
   Debug("minisat") << "in user pop, unsetting level units for level " << assertionLevel << std::endl;
   while(trail_user.last() != lit_Undef) {
diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h
index 426268b4b..c0dd00166 100644
--- a/src/prop/minisat/core/Solver.h
+++ b/src/prop/minisat/core/Solver.h
@@ -191,6 +191,10 @@ public:
     int     nVars      ()      const;       // The current number of variables.
     int     nFreeVars  ()      const;
 
+    // Debugging SMT explanations
+    //
+    bool    properExplanation(Lit l, Lit expl) const; // returns true if expl can be used to explain l---i.e., both assigned and trail_index(expl) < trail_index(l)
+
     // Resource contraints:
     //
     void    setConfBudget(int64_t x);
@@ -282,6 +286,7 @@ protected:
     vec<Lit>            trail;              // Assignment stack; stores all assigments made in the order they were made.
     vec<int>            trail_lim;          // Separator indices for different decision levels in 'trail'.
     vec<Lit>            trail_user;         // Stack of assignments to UNdo on user pop.
+    vec<int>            trail_user_lim;     // Separator indices for different user levels in 'trail'.
     vec<bool>           trail_ok;           // Stack of "whether we're in conflict" flags.
     vec<VarData>        vardata;            // Stores reason and level for each variable.
     int                 qhead;              // Head of queue (as index into the trail -- no more explicit propagation queue in MiniSat).
@@ -462,6 +467,7 @@ inline int      Solver::nClauses      ()      const   { return clauses_persisten
 inline int      Solver::nLearnts      ()      const   { return clauses_removable.size(); }
 inline int      Solver::nVars         ()      const   { return vardata.size(); }
 inline int      Solver::nFreeVars     ()      const   { return (int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]); }
+inline bool     Solver::properExplanation(Lit l, Lit expl) const { return value(l) == l_True && value(expl) == l_True && trail_index(var(expl)) < trail_index(var(l)); }
 inline void     Solver::setPolarity   (Var v, bool b) { polarity[v] = b; }
 inline void     Solver::setDecisionVar(Var v, bool b) 
 { 
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 7d0353122..2538e6d0c 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -232,6 +232,10 @@ void PropEngine::pop() {
   Debug("prop") << "pop()" << endl;
 }
 
+bool PropEngine::isRunning() const {
+  return d_inCheckSat;
+}
+
 void PropEngine::interrupt() throw(ModalException) {
   if(! d_inCheckSat) {
     throw ModalException("SAT solver is not currently solving anything; "
@@ -247,5 +251,49 @@ void PropEngine::spendResource() throw() {
   // TODO implement me
 }
 
+bool PropEngine::properExplanation(TNode node, TNode expl) const {
+  if(! d_cnfStream->hasLiteral(node)) {
+    Trace("properExplanation") << "properExplanation(): Failing because node "
+                               << "being explained doesn't have a SAT literal ?!" << std::endl
+                               << "properExplanation(): The node is: " << node << std::endl;
+    return false;
+  }
+
+  SatLiteral nodeLit = d_cnfStream->getLiteral(node);
+
+  for(TNode::kinded_iterator i = expl.begin(kind::AND),
+        i_end = expl.end(kind::AND);
+      i != i_end;
+      ++i) {
+    if(! d_cnfStream->hasLiteral(*i)) {
+      Trace("properExplanation") << "properExplanation(): Failing because one of explanation "
+                                 << "nodes doesn't have a SAT literal" << std::endl
+                                 << "properExplanation(): The explanation node is: " << *i << std::endl;
+      return false;
+    }
+
+    SatLiteral iLit = d_cnfStream->getLiteral(*i);
+
+    if(iLit == nodeLit) {
+      Trace("properExplanation") << "properExplanation(): Failing because the node" << std::endl
+                                 << "properExplanation(): " << node << std::endl
+                                 << "properExplanation(): cannot be made to explain itself!" << std::endl;
+      return false;
+    }
+
+    if(! d_satSolver->properExplanation(nodeLit, iLit)) {
+      Trace("properExplanation") << "properExplanation(): SAT solver told us that node" << std::endl
+                                 << "properExplanation(): " << *i << std::endl
+                                 << "properExplanation(): is not part of a proper explanation node for" << std::endl
+                                 << "properExplanation(): " << node << std::endl
+                                 << "properExplanation(): Perhaps it one of the two isn't assigned or the explanation" << std::endl
+                                 << "properExplanation(): node wasn't propagated before the node being explained" << std::endl;
+      return false;
+    }
+  }
+
+  return true;
+}
+
 }/* CVC4::prop namespace */
 }/* CVC4 namespace */
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index 4f83888fc..91b9a61e6 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -242,6 +242,12 @@ public:
   void pop();
 
   /**
+   * Return true if we are currently searching (either in this or
+   * another thread).
+   */
+  bool isRunning() const;
+
+  /**
    * Check the current time budget.
    */
   void checkTime();
@@ -258,11 +264,23 @@ public:
    */
   void spendResource() throw();
 
+  /**
+   * For debugging.  Return true if "expl" is a well-formed
+   * explanation for "node," meaning:
+   *
+   * 1. expl is either a SAT literal or an AND of SAT literals
+   *    currently assigned true;
+   * 2. node is assigned true;
+   * 3. node does not appear in expl; and
+   * 4. node was assigned after all of the literals in expl
+   */
+  bool properExplanation(TNode node, TNode expl) const;
+
 };/* class PropEngine */
 
 
 inline void SatTimer::check() {
-  if(expired()) {
+  if(d_propEngine.isRunning() && expired()) {
     Trace("limit") << "SatTimer::check(): interrupt!" << std::endl;
     d_propEngine.interrupt();
   }
diff --git a/src/prop/sat.h b/src/prop/sat.h
index a6bdcb309..14b42e445 100644
--- a/src/prop/sat.h
+++ b/src/prop/sat.h
@@ -49,6 +49,30 @@ class PropEngine;
 class CnfStream;
 
 /* Definitions of abstract types and conversion functions for SAT interface */
+/*
+inline SatLiteral variableToLiteral(SatVariable var) {
+  return Minisat::mkLit(var);
+}
+
+inline bool literalSign(SatLiteral lit) {
+  return Minisat::sign(lit);
+}
+
+static inline size_t
+hashSatLiteral(const SatLiteral& literal) {
+  return (size_t) Minisat::toInt(literal);
+}
+
+inline std::string stringOfLiteralValue(SatLiteralValue val) {
+  if( val == l_False ) {
+    return "0";
+  } else if (val == l_True ) {
+    return "1";
+  } else { // unknown
+    return "_";
+  }
+}
+*/
 
 /**
  * The proxy class that allows the SatSolver to communicate with the theories
diff --git a/src/prop/sat_module.cpp b/src/prop/sat_module.cpp
index 9391acbe5..db911f488 100644
--- a/src/prop/sat_module.cpp
+++ b/src/prop/sat_module.cpp
@@ -383,6 +383,9 @@ SatLiteralValue DPLLMinisatSatSolver::modelValue(SatLiteral l){
   return toSatLiteralValue(d_minisat->modelValue(toMinisatLit(l)));
 }
 
+bool DPLLMinisatSatSolver::properExplanation(SatLiteral lit, SatLiteral expl) const {
+  return true;
+}
 
 /** Incremental interface */ 
   
diff --git a/src/prop/sat_module.h b/src/prop/sat_module.h
index 320dfe09b..9c49c7d67 100644
--- a/src/prop/sat_module.h
+++ b/src/prop/sat_module.h
@@ -152,6 +152,8 @@ public:
 
   virtual void pop() = 0;
 
+  virtual bool properExplanation(SatLiteral lit, SatLiteral expl) const = 0;
+
 }; 
 
 // toodo add ifdef
@@ -179,11 +181,11 @@ public:
   SatLiteralValue value(SatLiteral l);
   SatLiteralValue modelValue(SatLiteral l);
 
-
   void unregisterVar(SatLiteral lit);
   void renewVar(SatLiteral lit, int level = -1);
   int getAssertionLevel() const;
 
+
   // helper methods for converting from the internal Minisat representation
 
   static SatVariable     toSatVariable(BVMinisat::Var var); 
@@ -254,6 +256,8 @@ public:
 
   SatLiteralValue modelValue(SatLiteral l);
 
+  bool properExplanation(SatLiteral lit, SatLiteral expl) const;
+
   /** Incremental interface */ 
   
   int getAssertionLevel() const;
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 7bf22c2c0..3c320b814 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -18,8 +18,10 @@
 
 #include <vector>
 #include <string>
+#include <iterator>
 #include <utility>
 #include <sstream>
+#include <stack>
 #include <ext/hash_map>
 
 #include "context/cdlist.h"
@@ -27,6 +29,8 @@
 #include "context/context.h"
 #include "expr/command.h"
 #include "expr/expr.h"
+#include "expr/kind.h"
+#include "expr/metakind.h"
 #include "expr/node_builder.h"
 #include "prop/prop_engine.h"
 #include "smt/bad_option_exception.h"
@@ -120,6 +124,17 @@ class SmtEnginePrivate {
   theory::SubstitutionMap d_topLevelSubstitutions;
 
   /**
+   * The last substition that the SAT layer was told about.
+   * In incremental settings, substitutions cannot be performed
+   * "backward," only forward.  So SAT needs to be told of all
+   * substitutions that are going to be done.  This iterator
+   * holds the last substitution from d_topLevelSubstitutions
+   * that was pushed out to SAT.
+   * If d_lastSubstitutionPos == d_topLevelSubstitutions.end(),
+   * then nothing has been pushed out yet. */
+  context::CDO<theory::SubstitutionMap::iterator> d_lastSubstitutionPos;
+
+  /**
    * Runs the nonclausal solver and tries to solve all the assigned
    * theory literals.
    */
@@ -136,6 +151,14 @@ class SmtEnginePrivate {
   void removeITEs();
 
   /**
+   * Any variable in a assertion that is declared as a subtype type
+   * (predicate subtype or integer subrange type) must be constrained
+   * to be in that type.
+   */
+  void constrainSubtypes(TNode n, std::vector<Node>& assertions)
+    throw(AssertionException);
+
+  /**
    * Perform non-clausal simplification of a Node.  This involves
    * Theory implementations, but does NOT involve the SAT solver in
    * any way.
@@ -148,7 +171,8 @@ public:
     d_smt(smt),
     d_nonClausalLearnedLiterals(),
     d_propagator(smt.d_userContext, d_nonClausalLearnedLiterals, true, true),
-    d_topLevelSubstitutions(smt.d_userContext) {
+    d_topLevelSubstitutions(smt.d_userContext),
+    d_lastSubstitutionPos(smt.d_userContext, d_topLevelSubstitutions.end()) {
   }
 
   Node applySubstitutions(TNode node) const {
@@ -161,6 +185,17 @@ public:
   void processAssertions();
 
   /**
+   * Process a user pop.  Clears out the non-context-dependent stuff in this
+   * SmtEnginePrivate.  Necessary to clear out our assertion vectors in case
+   * someone does a push-assert-pop without a check-sat.
+   */
+  void notifyPop() {
+    d_assertionsToPreprocess.clear();
+    d_nonClausalLearnedLiterals.clear();
+    d_assertionsToCheck.clear();
+  }
+
+  /**
    * Adds a formula to the current context.  Action here depends on
    * the SimplificationMode (in the current Options scope); the
    * formula might be pushed out to the propositional layer
@@ -175,6 +210,7 @@ public:
    */
   Node expandDefinitions(TNode n, hash_map<TNode, Node, TNodeHashFunction>& cache)
     throw(NoSuchFunctionException, AssertionException);
+
 };/* class SmtEnginePrivate */
 
 }/* namespace CVC4::smt */
@@ -231,7 +267,14 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) :
 
   d_definedFunctions = new(true) DefinedFunctionMap(d_userContext);
 
-  if(Options::current()->interactive) {
+  // [MGD 10/20/2011] keep around in incremental mode, due to a
+  // cleanup ordering issue and Nodes/TNodes.  If SAT is popped
+  // first, some user-context-dependent TNodes might still exist
+  // with rc == 0.
+  if(Options::current()->interactive ||
+     Options::current()->incrementalSolving) {
+    // In the case of incremental solving, we appear to need these to
+    // ensure the relevant Nodes remain live.
     d_assertionList = new(true) AssertionList(d_userContext);
   }
 
@@ -265,31 +308,39 @@ void SmtEngine::shutdown() {
   d_theoryEngine->shutdown();
 }
 
-SmtEngine::~SmtEngine() {
+SmtEngine::~SmtEngine() throw() {
   NodeManagerScope nms(d_nodeManager);
 
-  shutdown();
+  try {
+    while(Options::current()->incrementalSolving && d_userContext->getLevel() > 0) {
+      internalPop();
+    }
+
+    shutdown();
 
-  if(d_assignments != NULL) {
-    d_assignments->deleteSelf();
-  }
+    if(d_assignments != NULL) {
+      d_assignments->deleteSelf();
+    }
 
-  if(d_assertionList != NULL) {
-    d_assertionList->deleteSelf();
-  }
+    if(d_assertionList != NULL) {
+      d_assertionList->deleteSelf();
+    }
 
-  d_definedFunctions->deleteSelf();
+    d_definedFunctions->deleteSelf();
 
-  StatisticsRegistry::unregisterStat(&d_definitionExpansionTime);
-  StatisticsRegistry::unregisterStat(&d_nonclausalSimplificationTime);
-  StatisticsRegistry::unregisterStat(&d_staticLearningTime);
+    StatisticsRegistry::unregisterStat(&d_definitionExpansionTime);
+    StatisticsRegistry::unregisterStat(&d_nonclausalSimplificationTime);
+    StatisticsRegistry::unregisterStat(&d_staticLearningTime);
 
-  // Deletion order error: circuit propagator has some unsafe TNodes ?!
-  // delete d_private;
-  delete d_userContext;
+    delete d_private;
+    delete d_userContext;
 
-  delete d_theoryEngine;
-  delete d_propEngine;
+    delete d_theoryEngine;
+    delete d_propEngine;
+  } catch(Exception& e) {
+    Warning() << "CVC4 threw an exception during cleanup." << endl
+              << e << endl;
+  }
 }
 
 void SmtEngine::setLogic(const std::string& s) throw(ModalException) {
@@ -415,7 +466,11 @@ void SmtEngine::setOption(const std::string& key, const SExpr& value)
   }
 
   if(key == ":print-success") {
-    throw BadOptionException();
+    if(value.isAtom() && value.getValue() == "false") {
+      // fine; don't need to do anything
+    } else {
+      throw BadOptionException();
+    }
   } else if(key == ":expand-definitions") {
     throw BadOptionException();
   } else if(key == ":interactive-mode") {
@@ -641,17 +696,17 @@ void SmtEnginePrivate::nonClausalSimplify() {
   Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
                     << "applying substitutions" << endl;
   for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) {
-    Trace("simplify") << "applying to " << d_assertionsToPreprocess[i] << std::endl;
+    Trace("simplify") << "applying to " << d_assertionsToPreprocess[i] << endl;
     d_assertionsToPreprocess[i] =
       theory::Rewriter::rewrite(d_topLevelSubstitutions.apply(d_assertionsToPreprocess[i]));
-    Trace("simplify") << "  got " << d_assertionsToPreprocess[i] << std::endl;
+    Trace("simplify") << "  got " << d_assertionsToPreprocess[i] << endl;
   }
 
   // Assert all the assertions to the propagator
   Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
                     << "asserting to propagator" << endl;
   for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) {
-    Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): asserting " << d_assertionsToPreprocess[i] << std::endl;
+    Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): asserting " << d_assertionsToPreprocess[i] << endl;
     d_propagator.assert(d_assertionsToPreprocess[i]);
   }
 
@@ -691,6 +746,7 @@ void SmtEnginePrivate::nonClausalSimplify() {
                         << "solving " << learnedLiteral << endl;
       Theory::PPAssertStatus solveStatus =
         d_smt.d_theoryEngine->solve(learnedLiteral, d_topLevelSubstitutions);
+
       switch (solveStatus) {
       case Theory::PP_ASSERT_STATUS_CONFLICT:
         // If in conflict, we return false
@@ -711,6 +767,27 @@ void SmtEnginePrivate::nonClausalSimplify() {
         d_nonClausalLearnedLiterals[j++] = d_nonClausalLearnedLiterals[i];
         break;
       }
+
+      if( Options::current()->incrementalSolving ||
+          Options::current()->simplificationMode == Options::SIMPLIFICATION_MODE_INCREMENTAL ) {
+        // Tell PropEngine about new substitutions
+        SubstitutionMap::iterator pos = d_lastSubstitutionPos;
+        if(pos == d_topLevelSubstitutions.end()) {
+           pos = d_topLevelSubstitutions.begin();
+        } else {
+          ++pos;
+        }
+
+        while(pos != d_topLevelSubstitutions.end()) {
+          // Push out this substitution
+          TNode lhs = (*pos).first, rhs = (*pos).second;
+          Node n = NodeManager::currentNM()->mkNode(lhs.getType().isBoolean() ? kind::IFF : kind::EQUAL, lhs, rhs);
+          d_assertionsToCheck.push_back(n);
+          Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): will notify SAT layer of substitution: " << n << endl;
+          d_lastSubstitutionPos = pos;
+          ++pos;
+        }
+      }
     }
     // Resize the learnt
     d_nonClausalLearnedLiterals.resize(j);
@@ -733,6 +810,63 @@ void SmtEnginePrivate::nonClausalSimplify() {
   d_assertionsToPreprocess.clear();
 }
 
+void SmtEnginePrivate::constrainSubtypes(TNode top, std::vector<Node>& assertions)
+  throw(AssertionException) {
+
+  Trace("constrainSubtypes") << "constrainSubtypes(): looking at " << top << endl;
+
+  set<TNode> done;
+  stack<TNode> worklist;
+  worklist.push(top);
+  done.insert(top);
+
+  do {
+    TNode n = worklist.top();
+    worklist.pop();
+
+    TypeNode t = n.getType();
+    if(t.isPredicateSubtype()) {
+      WarningOnce() << "Warning: CVC4 doesn't yet do checking that predicate subtypes are nonempty domains" << endl;
+      Node pred = t.getSubtypePredicate();
+      Kind k;
+      // pred can be a LAMBDA, a function constant, or a datatype tester
+      Trace("constrainSubtypes") << "constrainSubtypes(): pred.getType() == " << pred.getType() << endl;
+      if(d_smt.d_definedFunctions->find(pred) != d_smt.d_definedFunctions->end()) {
+        k = kind::APPLY;
+      } else if(pred.getType().isTester()) {
+        k = kind::APPLY_TESTER;
+      } else {
+        k = kind::APPLY_UF;
+      }
+      Node app = NodeManager::currentNM()->mkNode(k, pred, n);
+      Trace("constrainSubtypes") << "constrainSubtypes(): assert(" << k << ") " << app << endl;
+      assertions.push_back(app);
+    } else if(t.isSubrange()) {
+      SubrangeBounds bounds = t.getSubrangeBounds();
+      Trace("constrainSubtypes") << "constrainSubtypes(): got bounds " << bounds << endl;
+      if(bounds.lower.hasBound()) {
+        Node c = NodeManager::currentNM()->mkConst(bounds.lower.getBound());
+        Node lb = NodeManager::currentNM()->mkNode(kind::LEQ, c, n);
+        Trace("constrainSubtypes") << "constrainSubtypes(): assert " << lb << endl;
+        assertions.push_back(lb);
+      }
+      if(bounds.upper.hasBound()) {
+        Node c = NodeManager::currentNM()->mkConst(bounds.upper.getBound());
+        Node ub = NodeManager::currentNM()->mkNode(kind::LEQ, n, c);
+        Trace("constrainSubtypes") << "constrainSubtypes(): assert " << ub << endl;
+        assertions.push_back(ub);
+      }
+    }
+
+    for(TNode::iterator i = n.begin(); i != n.end(); ++i) {
+      if(done.find(*i) == done.end()) {
+        worklist.push(*i);
+        done.insert(*i);
+      }
+    }
+  } while(! worklist.empty());
+}
+
 void SmtEnginePrivate::simplifyAssertions()
   throw(NoSuchFunctionException, AssertionException) {
   try {
@@ -821,7 +955,7 @@ Result SmtEngine::check() {
   d_cumulativeResourceUsed += resource;
 
   Trace("limit") << "SmtEngine::check(): cumulative millis " << d_cumulativeTimeUsed
-                 << ", conflicts " << d_cumulativeResourceUsed << std::endl;
+                 << ", conflicts " << d_cumulativeResourceUsed << endl;
 
   return result;
 }
@@ -835,9 +969,28 @@ void SmtEnginePrivate::processAssertions() {
 
   Trace("smt") << "SmtEnginePrivate::processAssertions()" << endl;
 
+  Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
+  Debug("smt") << " d_assertionsToCheck     : " << d_assertionsToCheck.size() << endl;
+
+  // Any variables of subtype types need to be constrained properly.
+  // Careful, here: constrainSubtypes() adds to the back of
+  // d_assertionsToPreprocess, but we don't need to reprocess those.
+  // We also can't use an iterator, because the vector may be moved in
+  // memory during this loop.
+  for(unsigned i = 0, i_end = d_assertionsToPreprocess.size(); i != i_end; ++i) {
+    constrainSubtypes(d_assertionsToPreprocess[i], d_assertionsToPreprocess);
+  }
+
+  Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
+  Debug("smt") << " d_assertionsToCheck     : " << d_assertionsToCheck.size() << endl;
+
   // Simplify the assertions
   simplifyAssertions();
 
+  Trace("smt") << "SmtEnginePrivate::processAssertions() POST SIMPLIFICATION" << endl;
+  Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
+  Debug("smt") << " d_assertionsToCheck     : " << d_assertionsToCheck.size() << endl;
+
   if(Dump.isOn("assertions")) {
     // Push the simplified assertions to the dump output stream
     for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) {
@@ -1201,6 +1354,7 @@ size_t SmtEngine::getStackLevel() const {
 void SmtEngine::push() {
   NodeManagerScope nms(d_nodeManager);
   Trace("smt") << "SMT push()" << endl;
+  d_private->processAssertions();
   if(Dump.isOn("benchmark")) {
     Dump("benchmark") << PushCommand() << endl;
   }
@@ -1245,6 +1399,9 @@ void SmtEngine::pop() {
   }
   d_userLevels.pop_back();
 
+  // Clear out assertion queues etc., in case anything is still in there
+  d_private->notifyPop();
+
   Trace("userpushpop") << "SmtEngine: popped to level "
                        << d_userContext->getLevel() << endl;
   // FIXME: should we reset d_status here?
@@ -1258,6 +1415,7 @@ void SmtEngine::internalPush() {
   if(Options::current()->incrementalSolving) {
     d_private->processAssertions();
     d_userContext->push();
+    d_context->push();
     d_propEngine->push();
   }
 }
@@ -1266,6 +1424,7 @@ void SmtEngine::internalPop() {
   Trace("smt") << "SmtEngine::internalPop()" << endl;
   if(Options::current()->incrementalSolving) {
     d_propEngine->pop();
+    d_context->pop();
     d_userContext->pop();
   }
 }
@@ -1276,20 +1435,20 @@ void SmtEngine::interrupt() throw(ModalException) {
 
 void SmtEngine::setResourceLimit(unsigned long units, bool cumulative) {
   if(cumulative) {
-    Trace("limit") << "SmtEngine: setting cumulative resource limit to " << units << std::endl;
+    Trace("limit") << "SmtEngine: setting cumulative resource limit to " << units << endl;
     d_resourceBudgetCumulative = (units == 0) ? 0 : (d_cumulativeResourceUsed + units);
   } else {
-    Trace("limit") << "SmtEngine: setting per-call resource limit to " << units << std::endl;
+    Trace("limit") << "SmtEngine: setting per-call resource limit to " << units << endl;
     d_resourceBudgetPerCall = units;
   }
 }
 
 void SmtEngine::setTimeLimit(unsigned long millis, bool cumulative) {
   if(cumulative) {
-    Trace("limit") << "SmtEngine: setting cumulative time limit to " << millis << " ms" << std::endl;
+    Trace("limit") << "SmtEngine: setting cumulative time limit to " << millis << " ms" << endl;
     d_timeBudgetCumulative = (millis == 0) ? 0 : (d_cumulativeTimeUsed + millis);
   } else {
-    Trace("limit") << "SmtEngine: setting per-call time limit to " << millis << " ms" << std::endl;
+    Trace("limit") << "SmtEngine: setting per-call time limit to " << millis << " ms" << endl;
     d_timeBudgetPerCall = millis;
   }
 }
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 17717e440..84d6d1a73 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -231,7 +231,7 @@ public:
   /**
    * Destruct the SMT engine.
    */
-  ~SmtEngine();
+  ~SmtEngine() throw();
 
   /**
    * Set the logic of the script.
diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index a309b9403..c0ef02ec4 100644
--- a/src/theory/arith/arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -93,6 +93,21 @@ RewriteResponse ArithRewriter::preRewriteTerm(TNode t){
     return preRewritePlus(t);
   }else if(t.getKind() == kind::MULT){
     return preRewriteMult(t);
+  }else if(t.getKind() == kind::INTS_DIVISION){
+    Integer intOne(1);
+    if(t[1].getKind()== kind::CONST_INTEGER && t[1].getConst<Integer>() == intOne){
+      return RewriteResponse(REWRITE_AGAIN, t[0]);
+    }else{
+      return RewriteResponse(REWRITE_DONE, t);
+    }
+  }else if(t.getKind() == kind::INTS_MODULUS){
+    Integer intOne(1);
+    if(t[1].getKind()== kind::CONST_INTEGER && t[1].getConst<Integer>() == intOne){
+      Integer intZero(0);
+      return RewriteResponse(REWRITE_AGAIN, mkIntegerNode(intZero));
+    }else{
+      return RewriteResponse(REWRITE_DONE, t);
+    }
   }else{
     Unreachable();
   }
@@ -112,6 +127,10 @@ RewriteResponse ArithRewriter::postRewriteTerm(TNode t){
     return postRewritePlus(t);
   }else if(t.getKind() == kind::MULT){
     return postRewriteMult(t);
+  }else if(t.getKind() == kind::INTS_DIVISION){
+    return RewriteResponse(REWRITE_DONE, t);
+  }else if(t.getKind() == kind::INTS_MODULUS){
+    return RewriteResponse(REWRITE_DONE, t);
   }else{
     Unreachable();
   }
diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds
index bf5ea24c1..95d7d6ed1 100644
--- a/src/theory/arith/kinds
+++ b/src/theory/arith/kinds
@@ -17,7 +17,9 @@ operator PLUS 2: "arithmetic addition"
 operator MULT 2: "arithmetic multiplication"
 operator MINUS 2 "arithmetic binary subtraction operator"
 operator UMINUS 1 "arithmetic unary negation"
-operator DIVISION 2 "arithmetic division"
+operator DIVISION 2 "real division"
+operator INTS_DIVISION 2 "ints division"
+operator INTS_MODULUS 2 "ints modulus"
 operator POW 2 "arithmetic power"
 
 sort REAL_TYPE \
@@ -39,6 +41,19 @@ sort PSEUDOBOOLEAN_TYPE \
         "expr/node_manager.h" \
     "Pseudoboolean type"
 
+constant SUBRANGE_TYPE \
+    ::CVC4::SubrangeBounds \
+    ::CVC4::SubrangeBoundsHashStrategy \
+    "util/subrange_bound.h" \
+    "the type of an integer subrange"
+cardinality SUBRANGE_TYPE \
+    "::CVC4::theory::arith::SubrangeProperties::computeCardinality(%TYPE%)" \
+    "theory/arith/theory_arith_type_rules.h"
+well-founded SUBRANGE_TYPE \
+    true \
+    "::CVC4::theory::arith::SubrangeProperties::mkGroundTerm(%TYPE%)" \
+    "theory/arith/theory_arith_type_rules.h"
+
 constant CONST_RATIONAL \
     ::CVC4::Rational \
     ::CVC4::RationalHashStrategy \
@@ -75,4 +90,7 @@ typerule LEQ ::CVC4::theory::arith::ArithPredicateTypeRule
 typerule GT ::CVC4::theory::arith::ArithPredicateTypeRule
 typerule GEQ ::CVC4::theory::arith::ArithPredicateTypeRule
 
+typerule INTS_DIVISION ::CVC4::theory::arith::ArithOperatorTypeRule
+typerule INTS_MODULUS ::CVC4::theory::arith::ArithOperatorTypeRule
+
 endtheory
diff --git a/src/theory/arith/theory_arith_type_rules.h b/src/theory/arith/theory_arith_type_rules.h
index 511982d48..8d0d79f0a 100644
--- a/src/theory/arith/theory_arith_type_rules.h
+++ b/src/theory/arith/theory_arith_type_rules.h
@@ -21,6 +21,8 @@
 #ifndef __CVC4__THEORY__ARITH__THEORY_ARITH_TYPE_RULES_H
 #define __CVC4__THEORY__ARITH__THEORY_ARITH_TYPE_RULES_H
 
+#include "util/subrange_bound.h"
+
 namespace CVC4 {
 namespace theory {
 namespace arith {
@@ -33,7 +35,7 @@ public:
     if (n.getKind() == kind::CONST_RATIONAL) return nodeManager->realType();
     return nodeManager->integerType();
   }
-};
+};/* class ArithConstantTypeRule */
 
 class ArithOperatorTypeRule {
 public:
@@ -60,7 +62,7 @@ public:
     }
     return (isInteger ? integerType : realType);
   }
-};
+};/* class ArithOperatorTypeRule */
 
 class ArithPredicateTypeRule {
 public:
@@ -80,7 +82,33 @@ public:
     }
     return nodeManager->booleanType();
   }
-};
+};/* class ArithPredicateTypeRule */
+
+class SubrangeProperties {
+public:
+  inline static Cardinality computeCardinality(TypeNode type) {
+    Assert(type.getKind() == kind::SUBRANGE_TYPE);
+
+    const SubrangeBounds& bounds = type.getConst<SubrangeBounds>();
+    if(!bounds.lower.hasBound() || !bounds.upper.hasBound()) {
+      return Cardinality::INTEGERS;
+    }
+    return Cardinality(bounds.upper.getBound() - bounds.lower.getBound());
+  }
+
+  inline static Node mkGroundTerm(TypeNode type) {
+    Assert(type.getKind() == kind::SUBRANGE_TYPE);
+
+    const SubrangeBounds& bounds = type.getConst<SubrangeBounds>();
+    if(bounds.lower.hasBound()) {
+      return NodeManager::currentNM()->mkConst(bounds.lower.getBound());
+    }
+    if(bounds.upper.hasBound()) {
+      return NodeManager::currentNM()->mkConst(bounds.upper.getBound());
+    }
+    return NodeManager::currentNM()->mkConst(Integer(0));
+  }
+};/* class SubrangeProperties */
 
 }/* CVC4::theory::arith namespace */
 }/* CVC4::theory namespace */
diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds
index 61abfbfaf..519536c81 100644
--- a/src/theory/builtin/kinds
+++ b/src/theory/builtin/kinds
@@ -325,4 +325,17 @@ typerule EQUAL ::CVC4::theory::builtin::EqualityTypeRule
 typerule DISTINCT ::CVC4::theory::builtin::DistinctTypeRule
 typerule TUPLE ::CVC4::theory::builtin::TupleTypeRule
 
+constant SUBTYPE_TYPE \
+    ::CVC4::Predicate \
+    ::CVC4::PredicateHashStrategy \
+    "util/predicate.h" \
+    "predicate subtype"
+cardinality SUBTYPE_TYPE \
+    "::CVC4::theory::builtin::SubtypeProperties::computeCardinality(%TYPE%)" \
+    "theory/builtin/theory_builtin_type_rules.h"
+well-founded SUBTYPE_TYPE \
+    "::CVC4::theory::builtin::SubtypeProperties::isWellFounded(%TYPE%)" \
+    "::CVC4::theory::builtin::SubtypeProperties::mkGroundTerm(%TYPE%)" \
+    "theory/builtin/theory_builtin_type_rules.h"
+
 endtheory
diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h
index cd3e1437f..706196f8b 100644
--- a/src/theory/builtin/theory_builtin_type_rules.h
+++ b/src/theory/builtin/theory_builtin_type_rules.h
@@ -227,6 +227,26 @@ public:
   }
 };/* class TupleProperties */
 
+class SubtypeProperties {
+public:
+
+  inline static Cardinality computeCardinality(TypeNode type) {
+    Assert(type.getKind() == kind::SUBTYPE_TYPE);
+    Unimplemented("Computing the cardinality for predicate subtype not yet supported.");
+  }
+
+  inline static bool isWellFounded(TypeNode type) {
+    Assert(type.getKind() == kind::SUBTYPE_TYPE);
+    Unimplemented("Computing the well-foundedness for predicate subtype not yet supported.");
+  }
+
+  inline static Node mkGroundTerm(TypeNode type) {
+    Assert(type.getKind() == kind::SUBTYPE_TYPE);
+    Unimplemented("Constructing a ground term for predicate subtype not yet supported.");
+  }
+
+};/* class SubtypeProperties */
+
 }/* CVC4::theory::builtin namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/substitutions.cpp b/src/theory/substitutions.cpp
index 301cb8d60..caf7566b9 100644
--- a/src/theory/substitutions.cpp
+++ b/src/theory/substitutions.cpp
@@ -173,4 +173,9 @@ void SubstitutionMap::print(ostream& out) const {
 }
 
 }/* CVC4::theory namespace */
+
+std::ostream& operator<<(std::ostream& out, const theory::SubstitutionMap::iterator& i) {
+  return out << "[CDMap-iterator]";
+}
+
 }/* CVC4 namespace */
diff --git a/src/theory/substitutions.h b/src/theory/substitutions.h
index c03baa1ac..1ade4815d 100644
--- a/src/theory/substitutions.h
+++ b/src/theory/substitutions.h
@@ -48,6 +48,9 @@ public:
 
   typedef context::CDMap<Node, Node, NodeHashFunction> NodeMap;
 
+  typedef NodeMap::iterator iterator;
+  typedef NodeMap::const_iterator const_iterator;
+
 private:
 
   typedef std::hash_map<Node, Node, NodeHashFunction> NodeCache;
@@ -115,6 +118,22 @@ public:
     return const_cast<SubstitutionMap*>(this)->apply(t);
   }
 
+  iterator begin() {
+    return d_substitutions.begin();
+  }
+
+  iterator end() {
+    return d_substitutions.end();
+  }
+
+  const_iterator begin() const {
+    return d_substitutions.begin();
+  }
+
+  const_iterator end() const {
+    return d_substitutions.end();
+  }
+
   // NOTE [MGD]: removed clear() and swap() from the interface
   // when this data structure became context-dependent
   // because they weren't used---and it's not clear how they
@@ -134,6 +153,9 @@ inline std::ostream& operator << (std::ostream& out, const SubstitutionMap& subs
 }
 
 }/* CVC4::theory namespace */
+
+std::ostream& operator<<(std::ostream& out, const theory::SubstitutionMap::iterator& i);
+
 }/* CVC4 namespace */
 
 #endif /* __CVC4__THEORY__SUBSTITUTIONS_H */
diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index 1998498f5..76aabeb1f 100644
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -76,5 +76,14 @@ void Theory::computeCareGraph(CareGraph& careGraph) {
   }
 }
 
+void Theory::printFacts(std::ostream& os) const {
+  unsigned i, n = d_facts.size();
+  for(i = 0; i < n; i++){
+    const Assertion& a_i = d_facts[i];
+    Node assertion  = a_i;
+    os << d_id << '[' << i << ']' << " " << assertion << endl;
+  }
+}
+
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/theory.h b/src/theory/theory.h
index b0f5e4e53..35c81239f 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -142,7 +142,7 @@ private:
 
 protected:
 
-  /** 
+  /**
    * A list of shared terms that the theory has.
    */
   context::CDList<TNode> d_sharedTerms;
@@ -210,6 +210,9 @@ protected:
    */
   static TheoryId s_uninterpretedSortOwner;
 
+  void printFacts(std::ostream& os) const;
+
+
 public:
 
   /**
@@ -218,6 +221,9 @@ public:
   static inline TheoryId theoryOf(TypeNode typeNode) {
     Trace("theory") << "theoryOf(" << typeNode << ")" << std::endl;
     TheoryId id;
+    while (typeNode.isPredicateSubtype()) {
+      typeNode = typeNode.getSubtypeBaseType();
+    }
     if (typeNode.getKind() == kind::TYPE_CONSTANT) {
       id = typeConstantToTheoryId(typeNode.getConst<TypeConstant>());
     } else {
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 91d6beead..2950ad413 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -575,8 +575,10 @@ void TheoryEngine::assertFact(TNode node)
   // Get the atom
   TNode atom = node.getKind() == kind::NOT ? node[0] : node;
 
-  // Assert the fact to the apropriate theory
-  theoryOf(atom)->assertFact(node, true);
+  // Assert the fact to the appropriate theory and mark it active
+  Theory* theory = theoryOf(atom);
+  theory->assertFact(node, true);
+  markActive(Theory::setInsert(theory->getId()));
 
   // If any shared terms, notify the theories
   if (d_sharedTerms.hasSharedTerms(atom)) {
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index ceefa88e8..72244a573 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -91,7 +91,7 @@ class TheoryEngine {
 
   /**
    * A bitmap of theories that are "active" for the current run.  We
-   * mark a theory active when we firt see a term or type belonging to
+   * mark a theory active when we first see a term or type belonging to
    * it.  This is important because we can optimize for single-theory
    * runs (no sharing), can reduce the cost of walking the DAG on
    * registration, etc.
diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index e24184ad2..e8d33fbd4 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -57,6 +57,8 @@ libutil_la_SOURCES = \
 	ntuple.h \
 	recursion_breaker.h \
 	subrange_bound.h \
+	predicate.h \
+	predicate.cpp \
 	cardinality.h \
 	cardinality.cpp \
 	cache.h \
diff --git a/src/util/configuration.cpp b/src/util/configuration.cpp
index 211a1127b..8942c049b 100644
--- a/src/util/configuration.cpp
+++ b/src/util/configuration.cpp
@@ -190,7 +190,7 @@ string Configuration::getSubversionId() {
   return ss.str();
 }
 
-string Configuration::getCompiler() {
+std::string Configuration::getCompiler() {
   stringstream ss;
 #ifdef __GNUC__
   ss << "GCC";
@@ -205,4 +205,8 @@ string Configuration::getCompiler() {
   return ss.str();
 }
 
+std::string Configuration::getCompiledDateTime() {
+  return __DATE__ " " __TIME__;
+}
+
 }/* CVC4 namespace */
diff --git a/src/util/configuration.h b/src/util/configuration.h
index 1a57af62b..1bd48999e 100644
--- a/src/util/configuration.h
+++ b/src/util/configuration.h
@@ -102,6 +102,7 @@ public:
   static std::string getSubversionId();
 
   static std::string getCompiler();
+  static std::string getCompiledDateTime();
 
 };/* class Configuration */
 
diff --git a/src/util/configuration_private.h b/src/util/configuration_private.h
index fc0915f28..b93a6dd5e 100644
--- a/src/util/configuration_private.h
+++ b/src/util/configuration_private.h
@@ -121,7 +121,8 @@ This is CVC4 version " CVC4_RELEASE_STRING ) + \
         ? ( ::std::string(" [") + ::CVC4::Configuration::getSubversionId() + "]" ) \
         : ::std::string("") \
     ) + "\n\
-compiled with " + ::CVC4::Configuration::getCompiler() + "\n\n\
+compiled with " + ::CVC4::Configuration::getCompiler() + "\n\
+on " + ::CVC4::Configuration::getCompiledDateTime() + "\n\n\
 Copyright (C) 2009, 2010, 2011, 2012\n\
   The ACSys Group\n\
   Courant Institute of Mathematical Sciences\n\
diff --git a/src/util/datatype.i b/src/util/datatype.i
index 056c15004..2b2a96030 100644
--- a/src/util/datatype.i
+++ b/src/util/datatype.i
@@ -11,6 +11,8 @@
   %ignore to_array();// ocaml
   %ignore vector(size_type);// java/python
   %ignore resize(size_type);// java/python
+  %ignore set(int i, const CVC4::Datatype& x);
+  %ignore to_array();
 };
 %template(vectorDatatype) std::vector< CVC4::Datatype >;
 
@@ -23,6 +25,8 @@
   %ignore to_array();// ocaml
   %ignore vector(size_type);// java/python
   %ignore resize(size_type);// java/python
+  %ignore set(int i, const CVC4::Datatype::Constructor& x);
+  %ignore to_array();
 };
 %template(vectorDatatypeConstructor) std::vector< CVC4::DatatypeConstructor >;
 
diff --git a/src/util/integer_gmp_imp.h b/src/util/integer_gmp_imp.h
index 161666df5..a02f5d2c1 100644
--- a/src/util/integer_gmp_imp.h
+++ b/src/util/integer_gmp_imp.h
@@ -268,14 +268,14 @@ public:
     long si = d_value.get_si();
     // ensure there wasn't overflow
     AlwaysAssert(mpz_cmp_si(d_value.get_mpz_t(), si) == 0,
-                 "Overflow detected in Integer::getLong()");
+                 "Overflow when extracting long from multiprecision integer");
     return si;
   }
   unsigned long getUnsignedLong() const {
     unsigned long ui = d_value.get_ui();
     // ensure there wasn't overflow
     AlwaysAssert(mpz_cmp_ui(d_value.get_mpz_t(), ui) == 0,
-                 "Overflow detected in Integer::getUnsignedLong()");
+                 "Overflow when extracting unsigned long from multiprecision integer");
     return ui;
   }
 
diff --git a/src/util/options.cpp b/src/util/options.cpp
index e33fbc263..d21df27ac 100644
--- a/src/util/options.cpp
+++ b/src/util/options.cpp
@@ -23,6 +23,7 @@
 #include <string.h>
 #include <stdint.h>
 #include <time.h>
+#include <sstream>
 
 #include <getopt.h>
 
@@ -274,10 +275,10 @@ Dump modes can be combined with multiple uses of --dump.  Generally you want\n\
 one from the assertions category (either asertions, learned, or clauses), and\n\
 perhaps one or more stateful or non-stateful modes for checking correctness\n\
 and completeness of decision procedure implementations.  Stateful modes dump\n\
-the contextual assertions made by the core solver (all decisions and propagations\n\
-as assertions; that affects the validity of the resulting correctness and\n\
-completeness queries, so of course stateful and non-stateful modes cannot\n\
-be mixed in the same run.\n\
+the contextual assertions made by the core solver (all decisions and\n\
+propagations as assertions; that affects the validity of the resulting\n\
+correctness and completeness queries, so of course stateful and non-stateful\n\
+modes cannot be mixed in the same run.\n\
 \n\
 The --output-language option controls the language used for dumping, and\n\
 this allows you to connect CVC4 to another solver implementation via a UNIX\n\
@@ -983,7 +984,12 @@ throw(OptionException) {
       break; 
 
     case ':':
-      throw OptionException(string("option `") + argv[optind - 1] + "' missing its required argument");
+      // This can be a long or short option, and the way to get at the name of it is different.
+      if(optopt == 0) { // was a long option
+        throw OptionException(string("option `") + argv[optind - 1] + "' missing its required argument");
+      } else { // was a short option
+        throw OptionException(string("option `-") + char(optopt) + "' missing its required argument");
+      }
 
     case '?':
     default:
@@ -1004,7 +1010,13 @@ throw(OptionException) {
         }
         break;
       }
-      throw OptionException(string("can't understand option `") + argv[optind - 1] + "'");
+
+      // This can be a long or short option, and the way to get at the name of it is different.
+      if(optopt == 0) { // was a long option
+        throw OptionException(string("can't understand option `") + argv[optind - 1] + "'");
+      } else { // was a short option
+        throw OptionException(string("can't understand option `-") + char(optopt) + "'");
+      }
     }
   }
 
diff --git a/src/util/output.h b/src/util/output.h
index 8a90ef136..8afb4e05a 100644
--- a/src/util/output.h
+++ b/src/util/output.h
@@ -28,6 +28,7 @@
 #include <cstdio>
 #include <cstdarg>
 #include <set>
+#include <utility>
 
 namespace CVC4 {
 
@@ -167,6 +168,20 @@ CVC4ostream& CVC4ostream::operator<<(T const& t) {
   return *this;
 }
 
+/**
+ * Does nothing; designed for compilation of non-debug/non-trace
+ * builds.  None of these should ever be called in such builds, but we
+ * offer this to the compiler so it doesn't complain.
+ */
+class CVC4_PUBLIC NullC {
+public:
+  operator bool() { return false; }
+  operator CVC4ostream() { return CVC4ostream(); }
+  operator std::ostream&() { return null_os; }
+};/* class NullC */
+
+extern NullC nullCvc4Stream CVC4_PUBLIC;
+
 /** The debug output class */
 class CVC4_PUBLIC DebugC {
   std::set<std::string> d_tags;
@@ -208,6 +223,7 @@ public:
 
 /** The warning output class */
 class CVC4_PUBLIC WarningC {
+  std::set< std::pair<const char*, size_t> > d_alreadyWarned;
   std::ostream* d_os;
 
 public:
@@ -221,6 +237,22 @@ public:
   std::ostream& getStream() { return *d_os; }
 
   bool isOn() const { return d_os != &null_os; }
+
+  // This function supports the WarningOnce() macro, which allows you
+  // to easily indicate that a warning should be emitted, but only
+  // once for a given run of CVC4.
+  bool warnOnce(const char* file, size_t line) {
+    std::pair<const char*, size_t> pr = std::make_pair(file, line);
+    if(d_alreadyWarned.find(pr) != d_alreadyWarned.end()) {
+      // signal caller not to warn again
+      return false;
+    }
+
+    // okay warn this time, but don't do it again
+    d_alreadyWarned.insert(pr);
+    return true;
+  }
+
 };/* class WarningC */
 
 /** The message output class */
@@ -378,6 +410,7 @@ extern DumpC DumpChannel CVC4_PUBLIC;
 
 #  define Debug ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::DebugChannel
 #  define Warning ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::WarningChannel
+#  define WarningOnce ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::WarningChannel
 #  define Message ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::MessageChannel
 #  define Notice ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::NoticeChannel
 #  define Chat ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::ChatChannel
@@ -405,6 +438,7 @@ inline int DebugC::printf(const char* tag, const char* fmt, ...) { return 0; }
 inline int DebugC::printf(std::string tag, const char* fmt, ...) { return 0; }
 #  endif /* CVC4_DEBUG */
 #  define Warning (! ::CVC4::WarningChannel.isOn()) ? ::CVC4::nullCvc4Stream : ::CVC4::WarningChannel
+#  define WarningOnce (! ::CVC4::WarningChannel.isOn() || ! ::CVC4::WarningChannel.warnOnce(__FILE__,__LINE__)) ? ::CVC4::nullCvc4Stream : ::CVC4::WarningChannel
 #  define Message (! ::CVC4::MessageChannel.isOn()) ? ::CVC4::nullCvc4Stream : ::CVC4::MessageChannel
 #  define Notice (! ::CVC4::NoticeChannel.isOn()) ? ::CVC4::nullCvc4Stream : ::CVC4::NoticeChannel
 #  define Chat (! ::CVC4::ChatChannel.isOn()) ? ::CVC4::nullCvc4Stream : ::CVC4::ChatChannel
@@ -533,20 +567,6 @@ public:
 #endif /* CVC4_TRACING */
 
 /**
- * Does nothing; designed for compilation of non-debug/non-trace
- * builds.  None of these should ever be called in such builds, but we
- * offer this to the compiler so it doesn't complain.
- */
-class CVC4_PUBLIC NullC {
-public:
-  operator bool() { return false; }
-  operator CVC4ostream() { return CVC4ostream(); }
-  operator std::ostream&() { return null_os; }
-};/* class NullC */
-
-extern NullC nullCvc4Stream CVC4_PUBLIC;
-
-/**
  * Pushes an indentation level on construction, pop on destruction.
  * Useful for tracing recursive functions especially, but also can be
  * used for clearly separating different phases of an algorithm,
diff --git a/src/util/predicate.cpp b/src/util/predicate.cpp
new file mode 100644
index 000000000..1868f557d
--- /dev/null
+++ b/src/util/predicate.cpp
@@ -0,0 +1,57 @@
+/*********************                                                        */
+/*! \file predicate.cpp
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Representation of predicates for predicate subtyping
+ **
+ ** Simple class to represent predicates for predicate subtyping.
+ ** Instances of this class are carried as the payload of
+ ** the CONSTANT-metakinded SUBTYPE_TYPE types.
+ **/
+
+#include "expr/expr.h"
+#include "util/predicate.h"
+#include "util/Assert.h"
+
+using namespace std;
+
+namespace CVC4 {
+
+Predicate::Predicate(Expr e, Expr w) throw(IllegalArgumentException) : d_predicate(e), d_witness(w) {
+  CheckArgument(! e.isNull(), e, "Predicate cannot be null");
+  CheckArgument(e.getType().isPredicate(), e, "Expression given is not predicate");
+  CheckArgument(FunctionType(e.getType()).getArgTypes().size() == 1, e, "Expression given is not predicate of a single argument");
+}
+
+Predicate::operator Expr() const {
+  return d_predicate;
+}
+
+bool Predicate::operator==(const Predicate& p) const {
+  return d_predicate == p.d_predicate && d_witness == p.d_witness;
+}
+
+std::ostream&
+operator<<(std::ostream& out, const Predicate& p) {
+  out << p.d_predicate;
+  if(! p.d_witness.isNull()) {
+    out << " : " << p.d_witness;
+  }
+  return out;
+}
+
+size_t PredicateHashStrategy::hash(const Predicate& p) {
+  ExprHashFunction h;
+  return h(p.d_witness) * 5039 + h(p.d_predicate);
+}
+
+}/* CVC4 namespace */
diff --git a/src/util/predicate.h b/src/util/predicate.h
new file mode 100644
index 000000000..94a685177
--- /dev/null
+++ b/src/util/predicate.h
@@ -0,0 +1,64 @@
+/*********************                                                        */
+/*! \file predicate.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Representation of predicates for predicate subtyping
+ **
+ ** Simple class to represent predicates for predicate subtyping.
+ ** Instances of this class are carried as the payload of
+ ** the CONSTANT-metakinded SUBTYPE_TYPE types.
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__PREDICATE_H
+#define __CVC4__PREDICATE_H
+
+#include "util/Assert.h"
+
+namespace CVC4 {
+
+class Predicate;
+
+std::ostream& operator<<(std::ostream& out, const Predicate& p) CVC4_PUBLIC;
+
+struct CVC4_PUBLIC PredicateHashStrategy {
+  static size_t hash(const Predicate& p);
+};/* class PredicateHashStrategy */
+
+}/* CVC4 namespace */
+
+#include "expr/expr.h"
+
+namespace CVC4 {
+
+class CVC4_PUBLIC Predicate {
+
+  Expr d_predicate;
+  Expr d_witness;
+
+public:
+
+  Predicate(Expr e, Expr w = Expr()) throw(IllegalArgumentException);
+
+  operator Expr() const;
+
+  bool operator==(const Predicate& p) const;
+
+  friend std::ostream& operator<<(std::ostream& out, const Predicate& p);
+  friend size_t PredicateHashStrategy::hash(const Predicate& p);
+
+};/* class Predicate */
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__PREDICATE_H */
diff --git a/src/util/subrange_bound.h b/src/util/subrange_bound.h
index 0c84b214e..9d4d446bd 100644
--- a/src/util/subrange_bound.h
+++ b/src/util/subrange_bound.h
@@ -25,6 +25,8 @@
 #include "util/integer.h"
 #include "util/Assert.h"
 
+#include <limits>
+
 namespace CVC4 {
 
 /**
@@ -76,8 +78,132 @@ public:
     return !(*this == b);
   }
 
+  /**
+   * Is this SubrangeBound "less than" another?  For two
+   * SubrangeBounds that "have bounds," this is defined as expected.
+   * For a finite SubrangeBound b1 and a SubrangeBounds b2 without a
+   * bound, b1 < b2 (but note also that b1 > b2).  This strange
+   * behavior is due to the fact that a SubrangeBound without a bound
+   * is the representation for both +infinity and -infinity.
+   */
+  bool operator<(const SubrangeBound& b) const throw() {
+    return (!hasBound() && b.hasBound()) || (hasBound() && !b.hasBound()) ||
+      ( hasBound() && b.hasBound() && getBound() < b.getBound() );
+  }
+
+  /**
+   * Is this SubrangeBound "less than or equal to" another?  For two
+   * SubrangeBounds that "have bounds," this is defined as expected.
+   * For a finite SubrangeBound b1 and a SubrangeBounds b2 without a
+   * bound, b1 < b2 (but note also that b1 > b2).  This strange
+   * behavior is due to the fact that a SubrangeBound without a bound
+   * is the representation for both +infinity and -infinity.
+   */
+  bool operator<=(const SubrangeBound& b) const throw() {
+    return !hasBound() || !b.hasBound() ||
+      ( hasBound() && b.hasBound() && getBound() <= b.getBound() );
+  }
+
+  /**
+   * Is this SubrangeBound "greater than" another?  For two
+   * SubrangeBounds that "have bounds," this is defined as expected.
+   * For a finite SubrangeBound b1 and a SubrangeBounds b2 without a
+   * bound, b1 > b2 (but note also that b1 < b2).  This strange
+   * behavior is due to the fact that a SubrangeBound without a bound
+   * is the representation for both +infinity and -infinity.
+   */
+  bool operator>(const SubrangeBound& b) const throw() {
+    return (!hasBound() && b.hasBound()) || (hasBound() && !b.hasBound()) ||
+      ( hasBound() && b.hasBound() && getBound() < b.getBound() );
+  }
+
+  /**
+   * Is this SubrangeBound "greater than or equal to" another?  For
+   * two SubrangeBounds that "have bounds," this is defined as
+   * expected.  For a finite SubrangeBound b1 and a SubrangeBounds b2
+   * without a bound, b1 > b2 (but note also that b1 < b2).  This
+   * strange behavior is due to the fact that a SubrangeBound without
+   * a bound is the representation for both +infinity and -infinity.
+   */
+  bool operator>=(const SubrangeBound& b) const throw() {
+    return !hasBound() || !b.hasBound() ||
+      ( hasBound() && b.hasBound() && getBound() <= b.getBound() );
+  }
+
 };/* class SubrangeBound */
 
+class CVC4_PUBLIC SubrangeBounds {
+public:
+
+  SubrangeBound lower;
+  SubrangeBound upper;
+
+  SubrangeBounds(const SubrangeBound& l, const SubrangeBound& u) :
+    lower(l),
+    upper(u) {
+    CheckArgument(!l.hasBound() || !u.hasBound() ||
+                  l.getBound() <= u.getBound(),
+                  l, "Bad subrange bounds specified");
+  }
+
+  bool operator==(const SubrangeBounds& bounds) const {
+    return lower == bounds.lower && upper == bounds.upper;
+  }
+
+  bool operator!=(const SubrangeBounds& bounds) const {
+    return !(*this == bounds);
+  }
+
+  /**
+   * Is this pair of SubrangeBounds "less than" (contained inside) the
+   * given pair of SubrangeBounds?  Think of this as a subtype
+   * relation, e.g., [0,2] < [0,3]
+   */
+  bool operator<(const SubrangeBounds& bounds) const {
+    return (lower > bounds.lower && upper <= bounds.upper) ||
+      (lower >= bounds.lower && upper < bounds.upper);
+  }
+
+  /**
+   * Is this pair of SubrangeBounds "less than or equal" (contained
+   * inside) the given pair of SubrangeBounds?  Think of this as a
+   * subtype relation, e.g., [0,2] < [0,3]
+   */
+  bool operator<=(const SubrangeBounds& bounds) const {
+    return lower >= bounds.lower && upper <= bounds.upper;
+  }
+
+  /**
+   * Is this pair of SubrangeBounds "greater than" (does it contain)
+   * the given pair of SubrangeBounds?  Think of this as a supertype
+   * relation, e.g., [0,3] > [0,2]
+   */
+  bool operator>(const SubrangeBounds& bounds) const {
+    return (lower < bounds.lower && upper >= bounds.upper) ||
+      (lower <= bounds.lower && upper > bounds.upper);
+  }
+
+  /**
+   * Is this pair of SubrangeBounds "greater than" (does it contain)
+   * the given pair of SubrangeBounds?  Think of this as a supertype
+   * relation, e.g., [0,3] > [0,2]
+   */
+  bool operator>=(const SubrangeBounds& bounds) const {
+    return lower <= bounds.lower && upper >= bounds.upper;
+  }
+
+};/* class SubrangeBounds */
+
+struct CVC4_PUBLIC SubrangeBoundsHashStrategy {
+  static inline size_t hash(const SubrangeBounds& bounds) {
+    // We use Integer::hash() rather than Integer::getUnsignedLong()
+    // because the latter might overflow and throw an exception
+    size_t l = bounds.lower.hasBound() ? bounds.lower.getBound().hash() : std::numeric_limits<size_t>::max();
+    size_t u = bounds.upper.hasBound() ? bounds.upper.getBound().hash() : std::numeric_limits<size_t>::max();
+    return l + 0x9e3779b9 + (u << 6) + (u >> 2);
+  }
+};/* struct SubrangeBoundsHashStrategy */
+
 inline std::ostream&
 operator<<(std::ostream& out, const SubrangeBound& bound) throw() CVC4_PUBLIC;
 
@@ -92,6 +218,16 @@ operator<<(std::ostream& out, const SubrangeBound& bound) throw() {
   return out;
 }
 
+inline std::ostream&
+operator<<(std::ostream& out, const SubrangeBounds& bounds) throw() CVC4_PUBLIC;
+
+inline std::ostream&
+operator<<(std::ostream& out, const SubrangeBounds& bounds) throw() {
+  out << bounds.lower << ".." << bounds.upper;
+
+  return out;
+}
+
 }/* CVC4 namespace */
 
 #endif /* __CVC4__SUBRANGE_BOUND_H */
diff --git a/test/Makefile.am b/test/Makefile.am
index 4f7818ade..2bcb283d7 100644
--- a/test/Makefile.am
+++ b/test/Makefile.am
@@ -35,6 +35,7 @@ subdirs_to_check = \
 	regress/regress0/arith/integers \
 	regress/regress0/uf \
 	regress/regress0/uflra \
+	regress/regress0/uflia \
 	regress/regress0/bv \
 	regress/regress0/bv/core \
 	regress/regress0/arrays \
@@ -43,6 +44,7 @@ subdirs_to_check = \
 	regress/regress0/push-pop \
 	regress/regress0/precedence \
 	regress/regress0/preprocess \
+	regress/regress0/subtypes \
 	regress/regress1 \
 	regress/regress2 \
 	regress/regress3
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 1c4071c00..016bf6e2a 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -41,7 +41,8 @@ SMT2_TESTS = \
 	ite4.smt2 \
 	simple-lra.smt2 \
 	simple-rdl.smt2 \
-	simple-uf.smt2
+	simple-uf.smt2 \
+	simplification_bug4.smt2
 
 # Regression tests for PL inputs
 CVC_TESTS = \
@@ -105,7 +106,8 @@ EXTRA_DIST = $(TESTS) \
 	bug216.smt2.expect \
 	bug288b.smt \
 	bug288c.smt \
-	bug288.smt
+	bug288.smt \
+	simplification_bug4.smt2.expect
 
 if CVC4_BUILD_PROFILE_COMPETITION
 else
diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am
index c4a4e2fdd..581897535 100644
--- a/test/regress/regress0/datatypes/Makefile.am
+++ b/test/regress/regress0/datatypes/Makefile.am
@@ -12,6 +12,10 @@ MAKEFLAGS = -k
 # If a test shouldn't be run in e.g. competition mode,
 # put it below in "TESTS +="
 TESTS =	\
+	tuple.cvc \
+	rec1.cvc \
+	rec2.cvc \
+	rec5.cvc \
 	datatype.cvc \
 	datatype0.cvc \
 	datatype1.cvc \
@@ -45,7 +49,8 @@ endif
 
 # and make sure to distribute it
 EXTRA_DIST += \
-	error.cvc
+	error.cvc \
+	rec4.cvc
 
 # synonyms for "check"
 .PHONY: regress regress0 test
diff --git a/test/regress/regress0/datatypes/rec1.cvc b/test/regress/regress0/datatypes/rec1.cvc
new file mode 100644
index 000000000..25e14eac0
--- /dev/null
+++ b/test/regress/regress0/datatypes/rec1.cvc
@@ -0,0 +1,8 @@
+% EXPECT: valid
+% EXIT: 20
+c : BOOLEAN;
+a17 : BOOLEAN = ((# _a := 2, _b := 2 #) = (
+          IF c THEN (# _a := 3, _b := 2 #)
+          ELSE (# _a := 1, _b := 2 #)
+          ENDIF WITH ._a := 2));
+QUERY a17;
diff --git a/test/regress/regress0/datatypes/rec2.cvc b/test/regress/regress0/datatypes/rec2.cvc
new file mode 100644
index 000000000..80aecfe25
--- /dev/null
+++ b/test/regress/regress0/datatypes/rec2.cvc
@@ -0,0 +1,12 @@
+% EXPECT: valid
+% EXIT: 20
+c : BOOLEAN;
+a16 : [# _a : REAL, _b : REAL #] = (
+        IF c THEN (# _a := 3, _b := 2 #)
+        ELSE (# _a := 1, _b := 5 #)
+        ENDIF WITH ._a := 2);
+a21 : BOOLEAN = 
+        IF c THEN ((# _a := 2, _b := 2 #) = a16)
+        ELSE ((# _a := 2, _b := 5 #) = a16)
+        ENDIF;
+QUERY a21;
diff --git a/test/regress/regress0/datatypes/rec4.cvc b/test/regress/regress0/datatypes/rec4.cvc
new file mode 100644
index 000000000..c474502d5
--- /dev/null
+++ b/test/regress/regress0/datatypes/rec4.cvc
@@ -0,0 +1,11 @@
+% EXPECT: valid
+% EXIT: 20
+a : BOOLEAN;
+a49 : BOOLEAN = (
+          IF a THEN (# _a := 1 #)
+          ELSE (# _a := 2 #)
+          ENDIF = (# _a := 
+          IF a THEN 1
+          ELSE 2
+          ENDIF #));
+QUERY a49;
diff --git a/test/regress/regress0/datatypes/rec5.cvc b/test/regress/regress0/datatypes/rec5.cvc
new file mode 100644
index 000000000..d52174b8e
--- /dev/null
+++ b/test/regress/regress0/datatypes/rec5.cvc
@@ -0,0 +1,205 @@
+% EXPECT: invalid
+% EXIT: 10
+bit__ty: TYPE = [0..1];
+bc1553__lru_name: TYPE = [0..11];
+bus__inputs__type: TYPE;
+bus__word_index: TYPE = INT;
+cartesian__position: TYPE = [# x: INT, y: INT, z: INT #];
+ibit__phase: TYPE = [0..6];
+measuretypes__meter: TYPE = INT;
+bc1553__asi: [0..11];
+bc1553__barometer: [0..11];
+bc1553__compass: [0..11];
+bc1553__destruct: [0..11];
+bc1553__fins: [0..11];
+bc1553__fuel: [0..11];
+bc1553__fuze: [0..11];
+bc1553__infrared: [0..11];
+bc1553__ins: [0..11];
+bc1553__lru_name__base__first: [0..11];
+bc1553__lru_name__base__last: [0..11];
+bc1553__lru_name__first: [0..11];
+bc1553__lru_name__last: [0..11];
+bc1553__lru_name__size: INT;
+bc1553__motor: [0..11];
+bc1553__radar: [0..11];
+bc1553__warhead: [0..11];
+bus__all_msg_index__base__first: INT;
+bus__all_msg_index__base__last: INT;
+bus__all_msg_index__first: INT;
+bus__all_msg_index__last: INT;
+bus__all_msg_index__size: INT;
+bus__lru_subaddress_index__base__first: INT;
+bus__lru_subaddress_index__base__last: INT;
+bus__lru_subaddress_index__first: INT;
+bus__lru_subaddress_index__last: INT;
+bus__lru_subaddress_index__size: INT;
+bus__word__base__first: INT;
+bus__word__base__last: INT;
+bus__word__first: INT;
+bus__word__last: INT;
+bus__word__size: INT;
+bus__word_index__base__first: INT;
+bus__word_index__base__last: INT;
+bus__word_index__first: INT;
+bus__word_index__last: INT;
+bus__word_index__size: INT;
+bus_id: [0..11];
+ibit__fail: [0..6];
+ibit__in_progress: [0..6];
+ibit__off: [0..6];
+ibit__pass: [0..6];
+ibit__phase__base__first: [0..6];
+ibit__phase__base__last: [0..6];
+ibit__phase__first: [0..6];
+ibit__phase__last: [0..6];
+ibit__phase__size: INT;
+ibit__request_start: [0..6];
+ibit__request_stop: [0..6];
+ibit__timeout: [0..6];
+integer__base__first: INT;
+integer__base__last: INT;
+integer__first: INT;
+integer__last: INT;
+integer__size: INT;
+measuretypes__meter__base__first: INT;
+measuretypes__meter__base__last: INT;
+measuretypes__meter__first: INT;
+measuretypes__meter__last: INT;
+measuretypes__meter__size: INT;
+systemtypes__unsigned16__base__first: INT;
+systemtypes__unsigned16__base__last: INT;
+systemtypes__unsigned16__first: INT;
+systemtypes__unsigned16__last: INT;
+systemtypes__unsigned16__size: INT;
+bus__inputs: bus__inputs__type;
+bus__inputs__tilde: bus__inputs__type;
+ibit_request: [0..6];
+ibit_request__5: [0..6];
+ibit_request__5__tilde: [0..6];
+ibit_request__tilde: [0..6];
+last_position: [# x: INT, y: INT, z: INT #];
+last_position__1: [# x: INT, y: INT, z: INT #];
+last_position__1__tilde: [# x: INT, y: INT, z: INT #];
+last_position__2: [# x: INT, y: INT, z: INT #];
+last_position__2__tilde: [# x: INT, y: INT, z: INT #];
+last_position__3: [# x: INT, y: INT, z: INT #];
+last_position__3__tilde: [# x: INT, y: INT, z: INT #];
+last_position__tilde: [# x: INT, y: INT, z: INT #];
+word: INT;
+word__4: INT;
+word__4__tilde: INT;
+word__tilde: INT;
+bc1553__is_fresh: ([0..11], INT, bus__inputs__type) ->  BOOLEAN;
+bc1553__is_valid: ([0..11], INT, bus__inputs__type) ->  BOOLEAN;
+bc1553__lru_name__LE: ([0..11], [0..11]) ->  BOOLEAN;
+bc1553__lru_name__pos: [0..11] ->  INT;
+bc1553__lru_name__pred: [0..11] ->  [0..11];
+bc1553__lru_name__succ: [0..11] ->  [0..11];
+bc1553__lru_name__val: INT ->  [0..11];
+character__pos: INT ->  INT;
+character__val: INT ->  INT;
+ibit__phase__LE: ([0..6], [0..6]) ->  BOOLEAN;
+ibit__phase__pos: [0..6] ->  INT;
+ibit__phase__pred: [0..6] ->  [0..6];
+ibit__phase__succ: [0..6] ->  [0..6];
+ibit__phase__val: INT ->  [0..6];
+integer__pred: INT ->  INT;
+integer__succ: INT ->  INT;
+round__: REAL ->  INT;
+int__div: (INT, INT) ->  INT;
+int__mod: (INT, INT) ->  INT;
+ASSERT (bus_id = bc1553__ins);
+ASSERT (0 <= integer__size);
+ASSERT (integer__first = -(2147483647));
+ASSERT (integer__last = 2147483647);
+ASSERT (integer__base__first = -(2147483647));
+ASSERT (integer__base__last = 2147483647);
+ASSERT (0 <= systemtypes__unsigned16__size);
+ASSERT (systemtypes__unsigned16__first = 0);
+ASSERT (systemtypes__unsigned16__last = 65535);
+ASSERT (systemtypes__unsigned16__base__first = -(2147483647));
+ASSERT (systemtypes__unsigned16__base__last = 2147483647);
+ASSERT (0 <= measuretypes__meter__size);
+ASSERT (measuretypes__meter__first = -(200000));
+ASSERT (measuretypes__meter__last = 200000);
+ASSERT (measuretypes__meter__base__first = -(2147483647));
+ASSERT (measuretypes__meter__base__last = 2147483647);
+ASSERT (0 <= bus__word_index__size);
+ASSERT (bus__word_index__first = 1);
+ASSERT (bus__word_index__last = 31);
+ASSERT (bus__word_index__base__first <= bus__word_index__base__last);
+ASSERT (bus__word_index__base__first <= bus__word_index__first);
+ASSERT (bus__word_index__last <= bus__word_index__base__last);
+ASSERT (0 <= bus__word__size);
+ASSERT (bus__word__first = 0);
+ASSERT (bus__word__last = 65535);
+ASSERT (bus__word__base__first = -(2147483647));
+ASSERT (bus__word__base__last = 2147483647);
+ASSERT (0 <= bus__all_msg_index__size);
+ASSERT (bus__all_msg_index__first = 0);
+ASSERT (bus__all_msg_index__last = 63);
+ASSERT (bus__all_msg_index__base__first = -(32768));
+ASSERT (bus__all_msg_index__base__last = 32767);
+ASSERT (0 <= bus__lru_subaddress_index__size);
+ASSERT (bus__lru_subaddress_index__first = 1);
+ASSERT (bus__lru_subaddress_index__last = 8);
+ASSERT (bus__lru_subaddress_index__base__first = -(32768));
+ASSERT (bus__lru_subaddress_index__base__last = 32767);
+ASSERT (0 <= bc1553__lru_name__size);
+ASSERT (bc1553__lru_name__first = bc1553__barometer);
+ASSERT (bc1553__lru_name__last = bc1553__warhead);
+ASSERT (bc1553__lru_name__base__first = bc1553__barometer);
+ASSERT (bc1553__lru_name__base__last = bc1553__warhead);
+ASSERT (0 <= ibit__phase__size);
+ASSERT (ibit__phase__first = ibit__off);
+ASSERT (ibit__phase__last = ibit__timeout);
+ASSERT (ibit__phase__base__first = ibit__off);
+ASSERT (ibit__phase__base__last = ibit__timeout);
+ASSERT (bc1553__barometer = 0);
+ASSERT (bc1553__asi = 1);
+ASSERT (bc1553__ins = 2);
+ASSERT (bc1553__compass = 3);
+ASSERT (bc1553__fuel = 4);
+ASSERT (bc1553__fuze = 5);
+ASSERT (bc1553__radar = 6);
+ASSERT (bc1553__infrared = 7);
+ASSERT (bc1553__fins = 8);
+ASSERT (bc1553__motor = 9);
+ASSERT (bc1553__destruct = 10);
+ASSERT (bc1553__warhead = 11);
+ASSERT (ibit__off = 0);
+ASSERT (ibit__request_start = 1);
+ASSERT (ibit__in_progress = 2);
+ASSERT (ibit__request_stop = 3);
+ASSERT (ibit__pass = 4);
+ASSERT (ibit__fail = 5);
+ASSERT (ibit__timeout = 6);
+ASSERT TRUE;
+ASSERT (measuretypes__meter__first <= (last_position).z);
+ASSERT ((last_position).z <= measuretypes__meter__last);
+ASSERT (measuretypes__meter__first <= (last_position).y);
+ASSERT ((last_position).y <= measuretypes__meter__last);
+ASSERT (measuretypes__meter__first <= (last_position).x);
+ASSERT ((last_position).x <= measuretypes__meter__last);
+ASSERT TRUE;
+ASSERT (ibit__phase__first <= ibit_request);
+ASSERT (ibit_request <= ibit__phase__last);
+ASSERT (bus__lru_subaddress_index__first <= 1);
+ASSERT (1 <= bus__lru_subaddress_index__last);
+ASSERT (bc1553__lru_name__first <= bus_id);
+ASSERT (bus_id <= bc1553__lru_name__last);
+ASSERT TRUE;
+ASSERT (bc1553__is_valid(bus_id, 1, bus__inputs) => ((bus__lru_subaddress_index__first <= 1) AND (1 <= bus__lru_subaddress_index__last)));
+ASSERT (bc1553__is_valid(bus_id, 1, bus__inputs) => ((bc1553__lru_name__first <= bus_id) AND (bus_id <= bc1553__lru_name__last)));
+ASSERT (bc1553__is_valid(bus_id, 1, bus__inputs) => TRUE);
+ASSERT bc1553__is_valid(bus_id, 1, bus__inputs);
+ASSERT bc1553__is_fresh(bus_id, 1, bus__inputs);
+ASSERT (bus__word_index__first <= 2);
+ASSERT (2 <= bus__word_index__last);
+ASSERT (bus__word_index__first <= 1);
+ASSERT (1 <= bus__word_index__last);
+ASSERT (measuretypes__meter__first <= (last_position__1).x);
+ASSERT ((last_position__1).x <= measuretypes__meter__last);
+ASSERT ((last_position__1).y = (last_position).y);
+QUERY (last_position = last_position__1);
diff --git a/test/regress/regress0/datatypes/tuple.cvc b/test/regress/regress0/datatypes/tuple.cvc
new file mode 100644
index 000000000..1def5d14e
--- /dev/null
+++ b/test/regress/regress0/datatypes/tuple.cvc
@@ -0,0 +1,11 @@
+% EXPECT: valid
+% EXIT: 20
+x: [REAL,INT,REAL] = ( 4/5, 9, 11/9 );
+first_elem: REAL = x.0;
+third_elem: REAL = x.2;
+
+Tup: TYPE = [REAL,INT,REAL];
+y:  Tup = ( 4/5, 9, 11/9 );
+y1: Tup = y WITH .1 := 3; 
+
+QUERY x=y AND first_elem = y1.0 AND third_elem = y1.2 AND y1.1 = 3;
diff --git a/test/regress/regress0/push-pop/Makefile.am b/test/regress/regress0/push-pop/Makefile.am
index aedf03470..f43a4d183 100644
--- a/test/regress/regress0/push-pop/Makefile.am
+++ b/test/regress/regress0/push-pop/Makefile.am
@@ -20,6 +20,9 @@ CVC_TESTS = \
 	units.cvc \
 	incremental-subst-bug.cvc
 
+SMT2_TESTS = \
+	tiny_bug.smt2
+
 TESTS =	$(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS)
 
 EXTRA_DIST = $(TESTS) 
diff --git a/test/regress/regress0/push-pop/tiny_bug.smt2 b/test/regress/regress0/push-pop/tiny_bug.smt2
new file mode 100644
index 000000000..83ccca49e
--- /dev/null
+++ b/test/regress/regress0/push-pop/tiny_bug.smt2
@@ -0,0 +1,28 @@
+; COMMAND-LINE: --incremental --simplification=none
+; EXPECT: sat
+; EXPECT: unsat
+; EXIT: 20
+(set-logic QF_UFLIA)
+(declare-fun base () Int)
+(declare-fun n () Int)
+
+(declare-fun g (Int) Bool)
+(declare-fun f (Int) Bool)
+
+(push 1)
+(assert (<= 0 n))
+(assert (f n))
+(assert (= (f n) (or (= (- n base) 1) (g n))))
+(check-sat)
+(pop 1)
+
+(push 1)
+(assert (<= 0 n))
+
+(assert (or (= (- n base) 1) (g n)))
+(assert (not (g n)))
+(assert (= base (- 2)))
+
+(check-sat)
+(pop 1)
+
diff --git a/test/regress/regress0/simplification_bug4.smt2 b/test/regress/regress0/simplification_bug4.smt2
new file mode 100644
index 000000000..0d62d6921
--- /dev/null
+++ b/test/regress/regress0/simplification_bug4.smt2
@@ -0,0 +1,295 @@
+(set-logic QF_LIA)
+;; Simplified benchmark, derived from NuSMV output durationThm_1.bmc_k100.smt2
+;;
+;; Original version generated by Alberto Griggio <griggio@fbk.eu>
+;; on Fri Feb  4 15:56:12 2011
+(declare-fun sb_0__AT0 () Bool)
+(declare-fun si_0__AT0 () Int)
+(declare-fun si_1__AT0 () Int)
+(declare-fun sb_1__AT0 () Bool)
+(declare-fun si_2__AT0 () Int)
+(declare-fun si_3__AT0 () Int)
+(declare-fun sb_2__AT0 () Bool)
+(declare-fun si_4__AT0 () Int)
+(declare-fun si_5__AT0 () Int)
+(declare-fun sb_3__AT0 () Bool)
+(declare-fun sb_4__AT0 () Bool)
+(declare-fun sb_5__AT0 () Bool)
+(declare-fun si_6__AT0 () Int)
+(declare-fun si_7__AT0 () Int)
+(declare-fun si_8__AT0 () Int)
+(declare-fun si_9__AT0 () Int)
+(declare-fun si_10__AT0 () Int)
+(declare-fun si_11__AT0 () Int)
+(declare-fun sb_6__AT0 () Bool)
+(declare-fun sb_7__AT0 () Bool)
+(declare-fun si_12__AT0 () Int)
+(declare-fun si_13__AT0 () Int)
+(declare-fun si_14__AT0 () Int)
+(assert (let ((.def_61 (= si_2__AT0 si_4__AT0)))
+(let ((.def_60 (= si_3__AT0 si_5__AT0)))
+(let ((.def_62 (and .def_60 .def_61)))
+(let ((.def_63 (and sb_2__AT0 .def_62)))
+(let ((.def_59 (= si_8__AT0 0)))
+(let ((.def_64 (and .def_59 .def_63)))
+(let ((.def_58 (= si_11__AT0 0)))
+(let ((.def_65 (and .def_58 .def_64)))
+(let ((.def_53 (<= 1 si_0__AT0)))
+(let ((.def_52 (<= 1 si_1__AT0)))
+(let ((.def_54 (and .def_52 .def_53)))
+(let ((.def_48 (<= si_0__AT0 si_6__AT0)))
+(let ((.def_49 (not .def_48)))
+(let ((.def_50 (or sb_4__AT0 .def_49)))
+(let ((.def_55 (and .def_50 .def_54)))
+(let ((.def_45 (<= si_1__AT0 si_9__AT0)))
+(let ((.def_46 (not .def_45)))
+(let ((.def_47 (or sb_5__AT0 .def_46)))
+(let ((.def_56 (and .def_47 .def_55)))
+(let ((.def_57 (= sb_7__AT0 .def_56)))
+(let ((.def_66 (and .def_57 .def_65)))
+(let ((.def_44 (= si_14__AT0 0)))
+(let ((.def_67 (and .def_44 .def_66)))
+(let ((.def_33 (not sb_1__AT0)))
+(let ((.def_34 (or sb_2__AT0 .def_33)))
+(let ((.def_35 (= sb_0__AT0 .def_34)))
+(let ((.def_32 (= si_0__AT0 si_2__AT0)))
+(let ((.def_36 (and .def_32 .def_35)))
+(let ((.def_31 (= si_1__AT0 si_3__AT0)))
+(let ((.def_37 (and .def_31 .def_36)))
+(let ((.def_30 (= sb_1__AT0 sb_6__AT0)))
+(let ((.def_38 (and .def_30 .def_37)))
+(let ((.def_29 (= si_6__AT0 si_8__AT0)))
+(let ((.def_39 (and .def_29 .def_38)))
+(let ((.def_28 (= si_9__AT0 si_11__AT0)))
+(let ((.def_40 (and .def_28 .def_39)))
+(let ((.def_27 (= sb_6__AT0 sb_7__AT0)))
+(let ((.def_41 (and .def_27 .def_40)))
+(let ((.def_26 (= si_12__AT0 si_14__AT0)))
+(let ((.def_42 (and .def_26 .def_41)))
+(let ((.def_68 (and .def_42 .def_67)))
+.def_68
+))))))))))))))))))))))))))))))))))))))))))
+
+; (push 1)
+; (assert (let ((.def_69 (not sb_0__AT0)))
+; .def_69
+; ))
+; (check-sat)
+; (pop 1)
+
+(declare-fun sb_0__AT1 () Bool)
+(declare-fun si_0__AT1 () Int)
+(declare-fun si_1__AT1 () Int)
+(declare-fun sb_1__AT1 () Bool)
+(declare-fun si_2__AT1 () Int)
+(declare-fun si_3__AT1 () Int)
+(declare-fun sb_2__AT1 () Bool)
+(declare-fun si_4__AT1 () Int)
+(declare-fun si_5__AT1 () Int)
+(declare-fun sb_3__AT1 () Bool)
+(declare-fun sb_4__AT1 () Bool)
+(declare-fun sb_5__AT1 () Bool)
+(declare-fun si_6__AT1 () Int)
+(declare-fun si_7__AT1 () Int)
+(declare-fun si_8__AT1 () Int)
+(declare-fun si_9__AT1 () Int)
+(declare-fun si_10__AT1 () Int)
+(declare-fun si_11__AT1 () Int)
+(declare-fun sb_6__AT1 () Bool)
+(declare-fun sb_7__AT1 () Bool)
+(declare-fun si_12__AT1 () Int)
+(declare-fun si_13__AT1 () Int)
+(declare-fun si_14__AT1 () Int)
+(assert (let ((.def_163 (= si_0__AT0 si_2__AT1)))
+(let ((.def_162 (= si_1__AT0 si_3__AT1)))
+(let ((.def_164 (and .def_162 .def_163)))
+(let ((.def_155 (* (- 1) si_12__AT1)))
+(let ((.def_156 (+ si_1__AT1 .def_155)))
+(let ((.def_157 (+ si_0__AT1 .def_156)))
+(let ((.def_158 (<= .def_157 0)))
+(let ((.def_159 (not .def_158)))
+(let ((.def_160 (or sb_5__AT1 .def_159)))
+(let ((.def_161 (= sb_2__AT1 .def_160)))
+(let ((.def_165 (and .def_161 .def_164)))
+(let ((.def_147 (* (- 1) si_7__AT1)))
+(let ((.def_148 (+ si_6__AT0 .def_147)))
+(let ((.def_149 (= .def_148 (- 1))))
+(let ((.def_142 (not sb_3__AT0)))
+(let ((.def_150 (or .def_142 .def_149)))
+(let ((.def_144 (= si_7__AT1 0)))
+(let ((.def_145 (or sb_3__AT0 .def_144)))
+(let ((.def_151 (and .def_145 .def_150)))
+(let ((.def_139 (* (- 1) si_13__AT1)))
+(let ((.def_140 (+ si_12__AT0 .def_139)))
+(let ((.def_141 (= .def_140 (- 1))))
+(let ((.def_143 (or .def_141 .def_142)))
+(let ((.def_152 (and .def_143 .def_151)))
+(let ((.def_136 (= si_13__AT1 0)))
+(let ((.def_137 (or sb_3__AT0 .def_136)))
+(let ((.def_153 (and .def_137 .def_152)))
+(let ((.def_166 (and .def_153 .def_165)))
+(let ((.def_133 (not sb_4__AT0)))
+(let ((.def_130 (* (- 1) si_10__AT1)))
+(let ((.def_131 (+ si_9__AT0 .def_130)))
+(let ((.def_132 (= .def_131 (- 1))))
+(let ((.def_134 (or .def_132 .def_133)))
+(let ((.def_126 (= si_10__AT1 0)))
+(let ((.def_127 (or sb_4__AT0 .def_126)))
+(let ((.def_135 (and .def_127 .def_134)))
+(let ((.def_167 (and .def_135 .def_166)))
+(let ((.def_125 (= si_7__AT1 si_8__AT1)))
+(let ((.def_168 (and .def_125 .def_167)))
+(let ((.def_124 (= si_10__AT1 si_11__AT1)))
+(let ((.def_169 (and .def_124 .def_168)))
+(let ((.def_118 (<= 1 si_0__AT1)))
+(let ((.def_117 (<= 1 si_1__AT1)))
+(let ((.def_119 (and .def_117 .def_118)))
+(let ((.def_114 (<= si_0__AT1 si_6__AT1)))
+(let ((.def_115 (not .def_114)))
+(let ((.def_116 (or sb_4__AT1 .def_115)))
+(let ((.def_120 (and .def_116 .def_119)))
+(let ((.def_111 (<= si_1__AT1 si_9__AT1)))
+(let ((.def_112 (not .def_111)))
+(let ((.def_113 (or sb_5__AT1 .def_112)))
+(let ((.def_121 (and .def_113 .def_120)))
+(let ((.def_122 (and sb_6__AT0 .def_121)))
+(let ((.def_123 (= sb_7__AT1 .def_122)))
+(let ((.def_170 (and .def_123 .def_169)))
+(let ((.def_110 (= si_13__AT1 si_14__AT1)))
+(let ((.def_171 (and .def_110 .def_170)))
+(let ((.def_100 (not sb_1__AT1)))
+(let ((.def_101 (or sb_2__AT1 .def_100)))
+(let ((.def_102 (= sb_0__AT1 .def_101)))
+(let ((.def_99 (= si_0__AT1 si_2__AT1)))
+(let ((.def_103 (and .def_99 .def_102)))
+(let ((.def_98 (= si_1__AT1 si_3__AT1)))
+(let ((.def_104 (and .def_98 .def_103)))
+(let ((.def_97 (= sb_1__AT1 sb_6__AT1)))
+(let ((.def_105 (and .def_97 .def_104)))
+(let ((.def_96 (= si_6__AT1 si_8__AT1)))
+(let ((.def_106 (and .def_96 .def_105)))
+(let ((.def_95 (= si_9__AT1 si_11__AT1)))
+(let ((.def_107 (and .def_95 .def_106)))
+(let ((.def_94 (= sb_6__AT1 sb_7__AT1)))
+(let ((.def_108 (and .def_94 .def_107)))
+(let ((.def_93 (= si_12__AT1 si_14__AT1)))
+(let ((.def_109 (and .def_93 .def_108)))
+(let ((.def_172 (and .def_109 .def_171)))
+(let ((.def_173 (and sb_0__AT0 .def_172)))
+.def_173
+)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+
+; (push 1)
+; (assert (let ((.def_174 (not sb_0__AT1)))
+; .def_174
+; ))
+; (check-sat)
+; (pop 1)
+
+(declare-fun sb_0__AT2 () Bool)
+(declare-fun si_0__AT2 () Int)
+(declare-fun si_1__AT2 () Int)
+(declare-fun sb_1__AT2 () Bool)
+(declare-fun si_2__AT2 () Int)
+(declare-fun si_3__AT2 () Int)
+(declare-fun sb_2__AT2 () Bool)
+(declare-fun si_4__AT2 () Int)
+(declare-fun si_5__AT2 () Int)
+(declare-fun sb_3__AT2 () Bool)
+(declare-fun sb_4__AT2 () Bool)
+(declare-fun sb_5__AT2 () Bool)
+(declare-fun si_6__AT2 () Int)
+(declare-fun si_7__AT2 () Int)
+(declare-fun si_8__AT2 () Int)
+(declare-fun si_9__AT2 () Int)
+(declare-fun si_10__AT2 () Int)
+(declare-fun si_11__AT2 () Int)
+(declare-fun sb_6__AT2 () Bool)
+(declare-fun sb_7__AT2 () Bool)
+(declare-fun si_12__AT2 () Int)
+(declare-fun si_13__AT2 () Int)
+(declare-fun si_14__AT2 () Int)
+(assert (let ((.def_267 (= si_0__AT1 si_2__AT2)))
+(let ((.def_266 (= si_1__AT1 si_3__AT2)))
+(let ((.def_268 (and .def_266 .def_267)))
+(let ((.def_259 (* (- 1) si_12__AT2)))
+(let ((.def_260 (+ si_1__AT2 .def_259)))
+(let ((.def_261 (+ si_0__AT2 .def_260)))
+(let ((.def_262 (<= .def_261 0)))
+(let ((.def_263 (not .def_262)))
+(let ((.def_264 (or sb_5__AT2 .def_263)))
+(let ((.def_265 (= sb_2__AT2 .def_264)))
+(let ((.def_269 (and .def_265 .def_268)))
+(let ((.def_251 (* (- 1) si_7__AT2)))
+(let ((.def_252 (+ si_6__AT1 .def_251)))
+(let ((.def_253 (= .def_252 (- 1))))
+(let ((.def_246 (not sb_3__AT1)))
+(let ((.def_254 (or .def_246 .def_253)))
+(let ((.def_248 (= si_7__AT2 0)))
+(let ((.def_249 (or sb_3__AT1 .def_248)))
+(let ((.def_255 (and .def_249 .def_254)))
+(let ((.def_243 (* (- 1) si_13__AT2)))
+(let ((.def_244 (+ si_12__AT1 .def_243)))
+(let ((.def_245 (= .def_244 (- 1))))
+(let ((.def_247 (or .def_245 .def_246)))
+(let ((.def_256 (and .def_247 .def_255)))
+(let ((.def_240 (= si_13__AT2 0)))
+(let ((.def_241 (or sb_3__AT1 .def_240)))
+(let ((.def_257 (and .def_241 .def_256)))
+(let ((.def_270 (and .def_257 .def_269)))
+(let ((.def_237 (not sb_4__AT1)))
+(let ((.def_234 (* (- 1) si_10__AT2)))
+(let ((.def_235 (+ si_9__AT1 .def_234)))
+(let ((.def_236 (= .def_235 (- 1))))
+(let ((.def_238 (or .def_236 .def_237)))
+(let ((.def_231 (= si_10__AT2 0)))
+(let ((.def_232 (or sb_4__AT1 .def_231)))
+(let ((.def_239 (and .def_232 .def_238)))
+(let ((.def_271 (and .def_239 .def_270)))
+(let ((.def_230 (= si_7__AT2 si_8__AT2)))
+(let ((.def_272 (and .def_230 .def_271)))
+(let ((.def_229 (= si_10__AT2 si_11__AT2)))
+(let ((.def_273 (and .def_229 .def_272)))
+(let ((.def_223 (<= 1 si_0__AT2)))
+(let ((.def_222 (<= 1 si_1__AT2)))
+(let ((.def_224 (and .def_222 .def_223)))
+(let ((.def_219 (<= si_0__AT2 si_6__AT2)))
+(let ((.def_220 (not .def_219)))
+(let ((.def_221 (or sb_4__AT2 .def_220)))
+(let ((.def_225 (and .def_221 .def_224)))
+(let ((.def_216 (<= si_1__AT2 si_9__AT2)))
+(let ((.def_217 (not .def_216)))
+(let ((.def_218 (or sb_5__AT2 .def_217)))
+(let ((.def_226 (and .def_218 .def_225)))
+(let ((.def_227 (and sb_6__AT1 .def_226)))
+(let ((.def_228 (= sb_7__AT2 .def_227)))
+(let ((.def_274 (and .def_228 .def_273)))
+(let ((.def_215 (= si_13__AT2 si_14__AT2)))
+(let ((.def_275 (and .def_215 .def_274)))
+(let ((.def_205 (not sb_1__AT2)))
+(let ((.def_206 (or sb_2__AT2 .def_205)))
+(let ((.def_207 (= sb_0__AT2 .def_206)))
+(let ((.def_204 (= si_0__AT2 si_2__AT2)))
+(let ((.def_208 (and .def_204 .def_207)))
+(let ((.def_203 (= si_1__AT2 si_3__AT2)))
+(let ((.def_209 (and .def_203 .def_208)))
+(let ((.def_202 (= sb_1__AT2 sb_6__AT2)))
+(let ((.def_210 (and .def_202 .def_209)))
+(let ((.def_201 (= si_6__AT2 si_8__AT2)))
+(let ((.def_211 (and .def_201 .def_210)))
+(let ((.def_200 (= si_9__AT2 si_11__AT2)))
+(let ((.def_212 (and .def_200 .def_211)))
+(let ((.def_199 (= sb_6__AT2 sb_7__AT2)))
+(let ((.def_213 (and .def_199 .def_212)))
+(let ((.def_198 (= si_12__AT2 si_14__AT2)))
+(let ((.def_214 (and .def_198 .def_213)))
+(let ((.def_276 (and .def_214 .def_275)))
+(let ((.def_277 (and sb_0__AT1 .def_276)))
+.def_277
+)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+
+(push 1)
+(assert (not sb_0__AT2))
+(check-sat)
+(pop 1)
+
diff --git a/test/regress/regress0/simplification_bug4.smt2.expect b/test/regress/regress0/simplification_bug4.smt2.expect
new file mode 100644
index 000000000..ef44f9b74
--- /dev/null
+++ b/test/regress/regress0/simplification_bug4.smt2.expect
@@ -0,0 +1,3 @@
+% COMMAND-LINE: --incremental
+% EXPECT: unsat
+% EXIT: 20
diff --git a/test/regress/run_regression b/test/regress/run_regression
index 6c06175d2..75d81b938 100755
--- a/test/regress/run_regression
+++ b/test/regress/run_regression
@@ -102,12 +102,12 @@ elif expr "$benchmark" : '.*\.smt2$' &>/dev/null; then
     if [ -z "$expected_exit_status" ]; then
       error "cannot determine expected exit status of \`$benchmark': please use \`% EXIT:' gesture"
     fi
-  elif grep -q '^% \(PROOF\|EXPECT\|EXPECT-ERROR\|EXIT\|COMMAND-LINE\): ' "$benchmark" "$benchmark"; then
-    expected_proof=`grep -q '^% PROOF' "$benchmark" && echo yes`
-    expected_output=`grep '^% EXPECT: ' "$benchmark" | sed 's,^% EXPECT: ,,'`
-    expected_error=`grep '^% EXPECT-ERROR: ' "$benchmark" | sed 's,^% EXPECT-ERROR: ,,'`
-    expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark" | perl -pe 's,^% EXIT: ,,;s,\r,,'`
-    command_line=`grep '^% COMMAND-LINE: ' "$benchmark" | sed 's,^% COMMAND-LINE: ,,'`
+  elif grep -q '^\(%\|;\) \(EXPECT\|EXPECT-ERROR\|EXIT\|COMMAND-LINE\): ' "$benchmark" "$benchmark"; then
+    expected_proof=`grep -q '^[%;] PROOF' "$benchmark" && echo yes`
+    expected_output=`grep '^[%;] EXPECT: ' "$benchmark" | sed 's,^[%;] EXPECT: ,,'`
+    expected_error=`grep '^[%;] EXPECT-ERROR: ' "$benchmark" | sed 's,^[%;] EXPECT-ERROR: ,,'`
+    expected_exit_status=`grep -m 1 '^[%;] EXIT: ' "$benchmark" | perl -pe 's,^[%;] EXIT: ,,;s,\r,,'`
+    command_line=`grep '^[%;] COMMAND-LINE: ' "$benchmark" | sed 's,^[%;] COMMAND-LINE: ,,'`
     # old mktemp from coreutils 7.x is broken, can't do XXXX in the middle
     # this frustrates our auto-language-detection
     gettemp tmpbenchmark cvc4_benchmark.smt2.$$.XXXXXXXXXX
diff --git a/test/unit/prop/cnf_stream_black.h b/test/unit/prop/cnf_stream_black.h
index 99e8b087c..e9cba5f9c 100644
--- a/test/unit/prop/cnf_stream_black.h
+++ b/test/unit/prop/cnf_stream_black.h
@@ -100,7 +100,11 @@ public:
     return SatValUnknown;
   }
 
-};
+  bool properExplanation(SatLiteral lit, SatLiteral expl) const {
+    return true;
+  }
+
+};/* class FakeSatSolver */
 
 class CnfStreamBlack : public CxxTest::TestSuite {
   /** The SAT solver proxy */