Improved compatibility layer, now supports quantifiers. Also incorporates

numerous bugfixes, and the cvc3 system test is enabled.

21 files changed, 348 insertions, 187 deletions

diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp
index 62885f55f..96cef406f 100644
--- a/src/compat/cvc3_compat.cpp
+++ b/src/compat/cvc3_compat.cpp
@@ -45,6 +45,11 @@ using namespace std;
 
 namespace CVC3 {
 
+// Connects ExprManagers to ValidityCheckers.  Needed to clean up the
+// emmcs on ValidityChecker destruction (which are used for
+// ExprManager-to-ExprManager import).
+static std::map<CVC4::ExprManager*, ValidityChecker*> s_validityCheckers;
+
 static std::hash_map<Type, Expr, CVC4::TypeHashFunction> s_typeToExpr;
 static std::hash_map<Expr, Type, CVC4::ExprHashFunction> s_exprToType;
 
@@ -174,6 +179,7 @@ Expr Type::getExpr() const {
   Expr e = getExprManager()->mkVar("compatibility-layer-expr-type", *this);
   s_typeToExpr[*this] = e;
   s_exprToType[e] = *this;
+  s_validityCheckers[e.getExprManager()]->d_exprTypeMapRemove.push_back(e);
   return e;
 }
 
@@ -198,7 +204,7 @@ Cardinality Type::card() const {
 }
 
 Expr Type::enumerateFinite(Unsigned n) const {
-  Unimplemented();
+  Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
 }
 
 Unsigned Type::sizeFinite() const {
@@ -326,7 +332,7 @@ bool Expr::isVar() const {
 }
 
 bool Expr::isString() const {
-  return false;
+  return getType().isString();
 }
 
 bool Expr::isBoundVar() const {
@@ -334,15 +340,16 @@ bool Expr::isBoundVar() const {
 }
 
 bool Expr::isLambda() const {
-  Unimplemented();
+  // when implemented, also fix isClosure() below
+  Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
 }
 
 bool Expr::isClosure() const {
-  Unimplemented();
+  return isQuantifier();
 }
 
 bool Expr::isQuantifier() const {
-  Unimplemented();
+  return getKind() == CVC4::kind::FORALL || getKind() == CVC4::kind::EXISTS;
 }
 
 bool Expr::isApply() const {
@@ -424,7 +431,22 @@ Expr Expr::getExpr() const {
 }
 
 std::vector< std::vector<Expr> > Expr::getTriggers() const {
-  return vector< vector<Expr> >();
+  CheckArgument(isClosure(), *this, __PRETTY_FUNCTION__, "getTriggers() called on non-closure expr");
+  if(getNumChildren() < 3) {
+    // no triggers for this quantifier
+    return vector< vector<Expr> >();
+  } else {
+    // get the triggers from the third child
+    Expr triggers = (*this)[2];
+    vector< vector<Expr> > v;
+    for(const_iterator i = triggers.begin(); i != triggers.end(); ++i) {
+      v.push_back(vector<Expr>());
+      for(const_iterator j = (*i).begin(); j != (*i).end(); ++j) {
+        v.back().push_back(*j);
+      }
+    }
+    return v;
+  }
 }
 
 ExprManager* Expr::getEM() const {
@@ -711,12 +733,14 @@ void CLFlags::setFlag(const std::string& name,
 
 void ValidityChecker::setUpOptions(CVC4::Options& options, const CLFlags& clflags) {
   // always incremental and model-producing in CVC3 compatibility mode
+  // also incrementally-simplifying and interactive
   d_smt->setOption("incremental", string("true"));
   d_smt->setOption("produce-models", string("true"));
+  d_smt->setOption("simplification-mode", string("incremental"));
+  d_smt->setOption("interactive-mode", string("true"));// support SmtEngine::getAssertions()
 
   d_smt->setOption("statistics", string(clflags["stats"].getBool() ? "true" : "false"));
   d_smt->setOption("random-seed", int2string(clflags["seed"].getInt()));
-  d_smt->setOption("interactive-mode", string(clflags["interactive"].getBool() ? "true" : "false"));
   d_smt->setOption("parse-only", string(clflags["parse-only"].getBool() ? "true" : "false"));
   d_smt->setOption("input-language", clflags["lang"].getString());
   if(clflags["output-lang"].getString() == "") {
@@ -730,24 +754,54 @@ void ValidityChecker::setUpOptions(CVC4::Options& options, const CLFlags& clflag
 
 ValidityChecker::ValidityChecker() :
   d_clflags(new CLFlags()),
-  d_options() {
-  setUpOptions(d_options, *d_clflags);
+  d_options(),
+  d_em(NULL),
+  d_emmc(),
+  d_reverseEmmc(),
+  d_smt(NULL),
+  d_parserContext(NULL),
+  d_exprTypeMapRemove(),
+  d_constructors(),
+  d_selectors() {
   d_em = reinterpret_cast<ExprManager*>(new CVC4::ExprManager(d_options));
+  s_validityCheckers[d_em] = this;
   d_smt = new CVC4::SmtEngine(d_em);
+  setUpOptions(d_options, *d_clflags);
   d_parserContext = CVC4::parser::ParserBuilder(d_em, "<internal>").withInputLanguage(CVC4::language::input::LANG_CVC4).withStringInput("").build();
 }
 
 ValidityChecker::ValidityChecker(const CLFlags& clflags) :
   d_clflags(new CLFlags(clflags)),
-  d_options() {
-  setUpOptions(d_options, *d_clflags);
+  d_options(),
+  d_em(NULL),
+  d_emmc(),
+  d_reverseEmmc(),
+  d_smt(NULL),
+  d_parserContext(NULL),
+  d_exprTypeMapRemove(),
+  d_constructors(),
+  d_selectors() {
   d_em = reinterpret_cast<ExprManager*>(new CVC4::ExprManager(d_options));
+  s_validityCheckers[d_em] = this;
   d_smt = new CVC4::SmtEngine(d_em);
+  setUpOptions(d_options, *d_clflags);
   d_parserContext = CVC4::parser::ParserBuilder(d_em, "<internal>").withInputLanguage(CVC4::language::input::LANG_CVC4).withStringInput("").build();
 }
 
 ValidityChecker::~ValidityChecker() {
+  for(vector<Expr>::iterator i = d_exprTypeMapRemove.begin(); i != d_exprTypeMapRemove.end(); ++i) {
+    s_typeToExpr.erase(s_exprToType[*i]);
+    s_exprToType.erase(*i);
+  }
   delete d_parserContext;
+  delete d_smt;
+  d_emmc.clear();
+  for(set<ValidityChecker*>::iterator i = d_reverseEmmc.begin(); i != d_reverseEmmc.end(); ++i) {
+    (*i)->d_emmc.erase(d_em);
+  }
+  d_reverseEmmc.clear();
+  s_validityCheckers.erase(d_em);
+  delete d_em;
   delete d_clflags;
 }
 
@@ -1067,7 +1121,7 @@ Type ValidityChecker::dataType(const std::string& name,
                                const std::string& constructor,
                                const std::vector<std::string>& selectors,
                                const std::vector<Expr>& types) {
-  AlwaysAssert(selectors.size() == types.size());
+  CheckArgument(selectors.size() == types.size(), types, "expected selectors and types vectors to be of equal length");
   vector<string> cv;
   vector< vector<string> > sv;
   vector< vector<Expr> > tv;
@@ -1081,8 +1135,8 @@ Type ValidityChecker::dataType(const std::string& name,
                                const std::vector<std::string>& constructors,
                                const std::vector<std::vector<std::string> >& selectors,
                                const std::vector<std::vector<Expr> >& types) {
-  AlwaysAssert(constructors.size() == selectors.size());
-  AlwaysAssert(constructors.size() == types.size());
+  CheckArgument(constructors.size() == selectors.size(), selectors, "expected constructors and selectors vectors to be of equal length");
+  CheckArgument(constructors.size() == types.size(), types, "expected constructors and types vectors to be of equal length");
   vector<string> nv;
   vector< vector<string> > cv;
   vector< vector< vector<string> > > sv;
@@ -1103,19 +1157,19 @@ void ValidityChecker::dataType(const std::vector<std::string>& names,
                                const std::vector<std::vector<std::vector<Expr> > >& types,
                                std::vector<Type>& returnTypes) {
 
-  AlwaysAssert(names.size() == constructors.size());
-  AlwaysAssert(names.size() == selectors.size());
-  AlwaysAssert(names.size() == types.size());
+  CheckArgument(names.size() == constructors.size(), constructors, "expected names and constructors vectors to be of equal length");
+  CheckArgument(names.size() == selectors.size(), selectors, "expected names and selectors vectors to be of equal length");
+  CheckArgument(names.size() == types.size(), types, "expected names and types vectors to be of equal length");
   vector<CVC4::Datatype> dv;
 
   // Set up the datatype specifications.
   for(unsigned i = 0; i < names.size(); ++i) {
     CVC4::Datatype dt(names[i]);
-    AlwaysAssert(constructors[i].size() == selectors[i].size());
-    AlwaysAssert(constructors[i].size() == types[i].size());
+    CheckArgument(constructors[i].size() == selectors[i].size(), "expected sub-vectors in constructors and selectors vectors to match in size");
+    CheckArgument(constructors[i].size() == types[i].size(), "expected sub-vectors in constructors and types vectors to match in size");
     for(unsigned j = 0; j < constructors[i].size(); ++j) {
       CVC4::DatatypeConstructor ctor(constructors[i][j]);
-      AlwaysAssert(selectors[i][j].size() == types[i][j].size());
+      CheckArgument(selectors[i][j].size() == types[i][j].size(), types, "expected sub-vectors in selectors and types vectors to match in size");
       for(unsigned k = 0; k < selectors[i][j].size(); ++k) {
         if(types[i][j][k].getType().isString()) {
           ctor.addArg(selectors[i][j][k], CVC4::DatatypeUnresolvedType(types[i][j][k].getConst<string>()));
@@ -1137,12 +1191,17 @@ void ValidityChecker::dataType(const std::vector<std::string>& names,
   for(vector<CVC4::DatatypeType>::iterator i = dtts.begin(); i != dtts.end(); ++i) {
     // For each datatype...
     const CVC4::Datatype& dt = (*i).getDatatype();
+    // ensure it's well-founded (the check is done here because
+    // that's how it is in CVC3)
+    if(!dt.isWellFounded()) {
+      throw TypecheckException(d_em->mkConst(dt), "datatype is not well-founded");
+    }
     for(CVC4::Datatype::const_iterator j = dt.begin(); j != dt.end(); ++j) {
       // For each constructor, register its name and its selectors names.
-      AlwaysAssert(d_constructors.find((*j).getName()) == d_constructors.end(), "cannot have two constructors with the same name in a ValidityChecker");
+      CheckArgument(d_constructors.find((*j).getName()) == d_constructors.end(), constructors, "cannot have two constructors with the same name in a ValidityChecker");
       d_constructors[(*j).getName()] = &dt;
       for(CVC4::DatatypeConstructor::const_iterator k = (*j).begin(); k != (*j).end(); ++k) {
-        AlwaysAssert(d_selectors.find((*k).getName()) == d_selectors.end(), "cannot have two selectors with the same name in a ValidityChecker");
+        CheckArgument(d_selectors.find((*k).getName()) == d_selectors.end(), selectors, "cannot have two selectors with the same name in a ValidityChecker");
         d_selectors[(*k).getName()] = make_pair(&dt, (*j).getName());
       }
     }
@@ -1306,11 +1365,21 @@ Type ValidityChecker::parseType(const Expr& e) {
 }
 
 Expr ValidityChecker::importExpr(const Expr& e) {
-  Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
+  if(e.getExprManager() == d_em) {
+    return e;
+  }
+
+  s_validityCheckers[e.getExprManager()]->d_reverseEmmc.insert(this);
+  return e.exportTo(d_em, d_emmc[e.getExprManager()]);
 }
 
 Type ValidityChecker::importType(const Type& t) {
-  Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
+  if(t.getExprManager() == d_em) {
+    return t;
+  }
+
+  s_validityCheckers[t.getExprManager()]->d_reverseEmmc.insert(this);
+  return t.exportTo(d_em, d_emmc[t.getExprManager()]);
 }
 
 void ValidityChecker::cmdsFromString(const std::string& s, InputLanguage lang) {
@@ -1355,9 +1424,9 @@ Expr ValidityChecker::andExpr(const Expr& left, const Expr& right) {
 }
 
 Expr ValidityChecker::andExpr(const std::vector<Expr>& children) {
-  const vector<CVC4::Expr>& v =
-    *reinterpret_cast<const vector<CVC4::Expr>*>(&children);
-  return d_em->mkExpr(CVC4::kind::AND, v);
+  // AND must have at least 2 children
+  CheckArgument(children.size() > 0, children);
+  return (children.size() == 1) ? children[0] : Expr(d_em->mkExpr(CVC4::kind::AND, *reinterpret_cast<const vector<CVC4::Expr>*>(&children)));
 }
 
 Expr ValidityChecker::orExpr(const Expr& left, const Expr& right) {
@@ -1365,9 +1434,9 @@ Expr ValidityChecker::orExpr(const Expr& left, const Expr& right) {
 }
 
 Expr ValidityChecker::orExpr(const std::vector<Expr>& children) {
-  const vector<CVC4::Expr>& v =
-    *reinterpret_cast<const vector<CVC4::Expr>*>(&children);
-  return d_em->mkExpr(CVC4::kind::OR, v);
+  // OR must have at least 2 children
+  CheckArgument(children.size() > 0, children);
+  return (children.size() == 1) ? children[0] : Expr(d_em->mkExpr(CVC4::kind::OR, *reinterpret_cast<const vector<CVC4::Expr>*>(&children)));
 }
 
 Expr ValidityChecker::impliesExpr(const Expr& hyp, const Expr& conc) {
@@ -1388,6 +1457,7 @@ Expr ValidityChecker::iteExpr(const Expr& ifpart, const Expr& thenpart,
 }
 
 Expr ValidityChecker::distinctExpr(const std::vector<Expr>& children) {
+  CheckArgument(children.size() > 1, children, "it makes no sense to create a `distinct' expression with only one child");
   const vector<CVC4::Expr>& v =
     *reinterpret_cast<const vector<CVC4::Expr>*>(&children);
   return d_em->mkExpr(CVC4::kind::DISTINCT, v);
@@ -1446,7 +1516,12 @@ Expr ValidityChecker::ratExpr(const std::string& n, const std::string& d, int ba
 }
 
 Expr ValidityChecker::ratExpr(const std::string& n, int base) {
-  return d_em->mkConst(Rational(n, base));
+  if(n.find(".") == string::npos) {
+    return d_em->mkConst(Rational(n, base));
+  } else {
+    CheckArgument(base == 10, base, "unsupported base for decimal parsing");
+    return d_em->mkConst(Rational::fromDecimal(n));
+  }
 }
 
 Expr ValidityChecker::uminusExpr(const Expr& child) {
@@ -1458,9 +1533,9 @@ Expr ValidityChecker::plusExpr(const Expr& left, const Expr& right) {
 }
 
 Expr ValidityChecker::plusExpr(const std::vector<Expr>& children) {
-  const vector<CVC4::Expr>& v =
-    *reinterpret_cast<const vector<CVC4::Expr>*>(&children);
-  return d_em->mkExpr(CVC4::kind::PLUS, v);
+  // PLUS must have at least 2 children
+  CheckArgument(children.size() > 0, children);
+  return (children.size() == 1) ? children[0] : Expr(d_em->mkExpr(CVC4::kind::PLUS, *reinterpret_cast<const vector<CVC4::Expr>*>(&children)));
 }
 
 Expr ValidityChecker::minusExpr(const Expr& left, const Expr& right) {
@@ -1608,8 +1683,14 @@ Expr ValidityChecker::newBVAndExpr(const Expr& t1, const Expr& t2) {
 }
 
 Expr ValidityChecker::newBVAndExpr(const std::vector<Expr>& kids) {
-  // BVAND is not N-ary
-  Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
+  // BITVECTOR_AND is not N-ary in CVC4
+  CheckArgument(kids.size() > 1, kids, "BITVECTOR_AND must have at least 2 children");
+  std::vector<Expr>::const_reverse_iterator i = kids.rbegin();
+  Expr e = *i++;
+  while(i != kids.rend()) {
+    e = d_em->mkExpr(CVC4::kind::BITVECTOR_AND, *i++, e);
+  }
+  return e;
 }
 
 Expr ValidityChecker::newBVOrExpr(const Expr& t1, const Expr& t2) {
@@ -1619,8 +1700,14 @@ Expr ValidityChecker::newBVOrExpr(const Expr& t1, const Expr& t2) {
 }
 
 Expr ValidityChecker::newBVOrExpr(const std::vector<Expr>& kids) {
-  // BVOR is not N-ary
-  Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
+  // BITVECTOR_OR is not N-ary in CVC4
+  CheckArgument(kids.size() > 1, kids, "BITVECTOR_OR must have at least 2 children");
+  std::vector<Expr>::const_reverse_iterator i = kids.rbegin();
+  Expr e = *i++;
+  while(i != kids.rend()) {
+    e = d_em->mkExpr(CVC4::kind::BITVECTOR_OR, *i++, e);
+  }
+  return e;
 }
 
 Expr ValidityChecker::newBVXorExpr(const Expr& t1, const Expr& t2) {
@@ -1630,8 +1717,14 @@ Expr ValidityChecker::newBVXorExpr(const Expr& t1, const Expr& t2) {
 }
 
 Expr ValidityChecker::newBVXorExpr(const std::vector<Expr>& kids) {
-  // BVXOR is not N-ary
-  Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
+  // BITVECTOR_XOR is not N-ary in CVC4
+  CheckArgument(kids.size() > 1, kids, "BITVECTOR_XOR must have at least 2 children");
+  std::vector<Expr>::const_reverse_iterator i = kids.rbegin();
+  Expr e = *i++;
+  while(i != kids.rend()) {
+    e = d_em->mkExpr(CVC4::kind::BITVECTOR_XOR, *i++, e);
+  }
+  return e;
 }
 
 Expr ValidityChecker::newBVXnorExpr(const Expr& t1, const Expr& t2) {
@@ -1641,8 +1734,14 @@ Expr ValidityChecker::newBVXnorExpr(const Expr& t1, const Expr& t2) {
 }
 
 Expr ValidityChecker::newBVXnorExpr(const std::vector<Expr>& kids) {
-  // BVXNOR is not N-ary
-  Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
+  // BITVECTOR_XNOR is not N-ary in CVC4
+  CheckArgument(kids.size() > 1, kids, "BITVECTOR_XNOR must have at least 2 children");
+  std::vector<Expr>::const_reverse_iterator i = kids.rbegin();
+  Expr e = *i++;
+  while(i != kids.rend()) {
+    e = d_em->mkExpr(CVC4::kind::BITVECTOR_XNOR, *i++, e);
+  }
+  return e;
 }
 
 Expr ValidityChecker::newBVNandExpr(const Expr& t1, const Expr& t2) {
@@ -1707,18 +1806,48 @@ Expr ValidityChecker::newBVSubExpr(const Expr& t1, const Expr& t2) {
   return d_em->mkExpr(CVC4::kind::BITVECTOR_SUB, t1, t2);
 }
 
-Expr ValidityChecker::newBVPlusExpr(int numbits, const std::vector<Expr>& k) {
-  // BVPLUS is not N-ary
-  Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
+// Copied from CVC3's bitvector theory: makes bitvector expression "e"
+// into "len" bits, by zero-padding, or extracting least-significant bits.
+Expr ValidityChecker::bvpad(int len, const Expr& e) {
+  CheckArgument(len >= 0, len,
+                "padding length must be a non-negative integer, not %d", len);
+  CheckArgument(e.getType().isBitVector(), e,
+                "input to bitvector operation must be a bitvector");
+
+  unsigned size = CVC4::BitVectorType(e.getType()).getSize();
+  Expr res;
+  if(size == len) {
+    res = e;
+  } else if(len < size) {
+    res = d_em->mkExpr(d_em->mkConst(CVC4::BitVectorExtract(len - 1, 0)), e);
+  } else {
+    // size < len
+    Expr zero = d_em->mkConst(CVC4::BitVector(len - size, 0u));
+    res = d_em->mkExpr(CVC4::kind::BITVECTOR_CONCAT, zero, e);
+  }
+  return res;
+}
+
+Expr ValidityChecker::newBVPlusExpr(int numbits, const std::vector<Expr>& kids) {
+  // BITVECTOR_PLUS is not N-ary in CVC4
+  CheckArgument(kids.size() > 1, kids, "BITVECTOR_PLUS must have at least 2 children");
+  std::vector<Expr>::const_reverse_iterator i = kids.rbegin();
+  Expr e = *i++;
+  while(i != kids.rend()) {
+    e = d_em->mkExpr(CVC4::kind::BITVECTOR_PLUS, bvpad(numbits, *i++), e);
+  }
+  unsigned size = CVC4::BitVectorType(e.getType()).getSize();
+  CheckArgument(unsigned(numbits) == size, numbits,
+                "argument must match computed size of bitvector sum: "
+                "passed size == %u, computed size == %u", numbits, size);
+  return e;
 }
 
 Expr ValidityChecker::newBVPlusExpr(int numbits, const Expr& t1, const Expr& t2) {
   CheckArgument(t1.getType().isBitVector(), t1, "can only bvplus a bitvector, not a `%s'", t1.getType().toString().c_str());
   CheckArgument(t2.getType().isBitVector(), t2, "can only bvplus a bitvector, not a `%s'", t2.getType().toString().c_str());
-  Expr e = d_em->mkExpr(CVC4::kind::BITVECTOR_PLUS, t1, t2);
+  Expr e = d_em->mkExpr(CVC4::kind::BITVECTOR_PLUS, bvpad(numbits, t1), bvpad(numbits, t2));
   unsigned size = CVC4::BitVectorType(e.getType()).getSize();
-  CheckArgument(numbits > 0, numbits,
-                "argument must be positive integer, not %u", numbits);
   CheckArgument(unsigned(numbits) == size, numbits,
                 "argument must match computed size of bitvector sum: "
                 "passed size == %u, computed size == %u", numbits, size);
@@ -1728,10 +1857,8 @@ Expr ValidityChecker::newBVPlusExpr(int numbits, const Expr& t1, const Expr& t2)
 Expr ValidityChecker::newBVMultExpr(int numbits, const Expr& t1, const Expr& t2) {
   CheckArgument(t1.getType().isBitVector(), t1, "can only bvmult a bitvector, not a `%s'", t1.getType().toString().c_str());
   CheckArgument(t2.getType().isBitVector(), t2, "can only bvmult by a bitvector, not a `%s'", t2.getType().toString().c_str());
-  Expr e = d_em->mkExpr(CVC4::kind::BITVECTOR_MULT, t1, t2);
+  Expr e = d_em->mkExpr(CVC4::kind::BITVECTOR_MULT, bvpad(numbits, t1), bvpad(numbits, t2));
   unsigned size = CVC4::BitVectorType(e.getType()).getSize();
-  CheckArgument(numbits > 0, numbits,
-                "argument must be positive integer, not %u", numbits);
   CheckArgument(unsigned(numbits) == size, numbits,
                 "argument must match computed size of bitvector product: "
                 "passed size == %u, computed size == %u", numbits, size);
@@ -1861,42 +1988,61 @@ Expr ValidityChecker::boundVarExpr(const std::string& name, const std::string& u
 }
 
 Expr ValidityChecker::forallExpr(const std::vector<Expr>& vars, const Expr& body) {
-  Unimplemented("Quantifiers not supported by CVC4 yet (sorry!)");
+  Expr boundVarList = d_em->mkExpr(CVC4::kind::BOUND_VAR_LIST, *reinterpret_cast<const std::vector<CVC4::Expr>*>(&vars));
+  return d_em->mkExpr(CVC4::kind::FORALL, boundVarList, body);
 }
 
 Expr ValidityChecker::forallExpr(const std::vector<Expr>& vars, const Expr& body,
                                  const Expr& trigger) {
-  Unimplemented("Quantifiers not supported by CVC4 yet (sorry!)");
+  // trigger
+  Expr boundVarList = d_em->mkExpr(CVC4::kind::BOUND_VAR_LIST, *reinterpret_cast<const std::vector<CVC4::Expr>*>(&vars));
+  Expr triggerList = d_em->mkExpr(CVC4::kind::INST_PATTERN_LIST, d_em->mkExpr(CVC4::kind::INST_PATTERN, trigger));
+  return d_em->mkExpr(CVC4::kind::FORALL, boundVarList, body, triggerList);
 }
 
 Expr ValidityChecker::forallExpr(const std::vector<Expr>& vars, const Expr& body,
                                  const std::vector<Expr>& triggers) {
-  Unimplemented("Quantifiers not supported by CVC4 yet (sorry!)");
+  // set of triggers
+  Expr boundVarList = d_em->mkExpr(CVC4::kind::BOUND_VAR_LIST, *reinterpret_cast<const std::vector<CVC4::Expr>*>(&vars));
+  std::vector<CVC4::Expr> pats;
+  for(std::vector<Expr>::const_iterator i = triggers.begin(); i != triggers.end(); ++i) {
+    pats.push_back(d_em->mkExpr(CVC4::kind::INST_PATTERN, *i));
+  }
+  Expr triggerList = d_em->mkExpr(CVC4::kind::INST_PATTERN_LIST, pats);
+  return d_em->mkExpr(CVC4::kind::FORALL, boundVarList, body, triggerList);
 }
 
 Expr ValidityChecker::forallExpr(const std::vector<Expr>& vars, const Expr& body,
                                  const std::vector<std::vector<Expr> >& triggers) {
-  Unimplemented("Quantifiers not supported by CVC4 yet (sorry!)");
+  // set of multi-triggers
+  Expr boundVarList = d_em->mkExpr(CVC4::kind::BOUND_VAR_LIST, *reinterpret_cast<const std::vector<CVC4::Expr>*>(&vars));
+  std::vector<CVC4::Expr> pats;
+  for(std::vector< std::vector<Expr> >::const_iterator i = triggers.begin(); i != triggers.end(); ++i) {
+    pats.push_back(d_em->mkExpr(CVC4::kind::INST_PATTERN, *reinterpret_cast<const std::vector<CVC4::Expr>*>(&*i)));
+  }
+  Expr triggerList = d_em->mkExpr(CVC4::kind::INST_PATTERN_LIST, pats);
+  return d_em->mkExpr(CVC4::kind::FORALL, boundVarList, body, triggerList);
 }
 
 void ValidityChecker::setTriggers(const Expr& e, const std::vector<std::vector<Expr> > & triggers) {
-  Unimplemented("Quantifiers not supported by CVC4 yet (sorry!)");
+  Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
 }
 
 void ValidityChecker::setTriggers(const Expr& e, const std::vector<Expr>& triggers) {
-  Unimplemented("Quantifiers not supported by CVC4 yet (sorry!)");
+  Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
 }
 
 void ValidityChecker::setTrigger(const Expr& e, const Expr& trigger) {
-  Unimplemented("Quantifiers not supported by CVC4 yet (sorry!)");
+  Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
 }
 
 void ValidityChecker::setMultiTrigger(const Expr& e, const std::vector<Expr>& multiTrigger) {
-  Unimplemented("Quantifiers not supported by CVC4 yet (sorry!)");
+  Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
 }
 
 Expr ValidityChecker::existsExpr(const std::vector<Expr>& vars, const Expr& body) {
-  Unimplemented("Quantifiers not supported by CVC4 yet (sorry!)");
+  Expr boundVarList = d_em->mkExpr(CVC4::kind::BOUND_VAR_LIST, *reinterpret_cast<const std::vector<CVC4::Expr>*>(&vars));
+  return d_em->mkExpr(CVC4::kind::EXISTS, boundVarList, body);
 }
 
 Op ValidityChecker::lambdaExpr(const std::vector<Expr>& vars, const Expr& body) {
@@ -1914,11 +2060,16 @@ Expr ValidityChecker::simulateExpr(const Expr& f, const Expr& s0,
 }
 
 void ValidityChecker::setResourceLimit(unsigned limit) {
-  Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
+  // Set a resource limit for CVC4, cumulative (rather than
+  // per-query), starting from now.
+  d_smt->setResourceLimit(limit, true);
 }
 
 void ValidityChecker::setTimeLimit(unsigned limit) {
-  Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
+  // Set a time limit for CVC4, cumulative (rather than per-query),
+  // starting from now.  Note that CVC3 uses tenths of a second,
+  // while CVC4 uses milliseconds.
+  d_smt->setTimeLimit(limit * 100, true);
 }
 
 void ValidityChecker::assertFormula(const Expr& e) {
@@ -2031,11 +2182,17 @@ Expr ValidityChecker::getValue(const Expr& e) {
 }
 
 bool ValidityChecker::inconsistent(std::vector<Expr>& assumptions) {
-  Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
+  CheckArgument(assumptions.empty(), assumptions, "assumptions vector should be empty on entry");
+  if(d_smt->checkSat() == CVC4::Result::UNSAT) {
+    // supposed to be a minimal set, but CVC4 doesn't support that
+    d_smt->getAssertions().swap(*reinterpret_cast<std::vector<CVC4::Expr>*>(&assumptions));
+    return true;
+  }
+  return false;
 }
 
 bool ValidityChecker::inconsistent() {
-  Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
+  return d_smt->checkSat() == CVC4::Result::UNSAT;
 }
 
 bool ValidityChecker::incomplete() {
diff --git a/src/compat/cvc3_compat.h b/src/compat/cvc3_compat.h
index 3ef40636a..83465775b 100644
--- a/src/compat/cvc3_compat.h
+++ b/src/compat/cvc3_compat.h
@@ -526,8 +526,13 @@ class CVC4_PUBLIC ValidityChecker {
   CLFlags* d_clflags;
   CVC4::Options d_options;
   CVC3::ExprManager* d_em;
+  std::map<CVC4::ExprManager*, CVC4::ExprManagerMapCollection> d_emmc;
+  std::set<ValidityChecker*> d_reverseEmmc;
   CVC4::SmtEngine* d_smt;
   CVC4::parser::Parser* d_parserContext;
+  std::vector<Expr> d_exprTypeMapRemove;
+
+  friend class Type; // to reach in to d_exprTypeMapRemove
 
   typedef std::hash_map<std::string, const CVC4::Datatype*, CVC4::StringHashFunction> ConstructorMap;
   typedef std::hash_map<std::string, std::pair<const CVC4::Datatype*, std::string>, CVC4::StringHashFunction> SelectorMap;
@@ -539,6 +544,9 @@ class CVC4_PUBLIC ValidityChecker {
 
   void setUpOptions(CVC4::Options& options, const CLFlags& clflags);
 
+  // helper function for bitvectors
+  Expr bvpad(int len, const Expr& e);
+
 public:
   //! Constructor
   ValidityChecker();
diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index b0364348c..365dc050f 100644
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -120,7 +120,7 @@ Node exportInternal(TNode n, ExprManager* from, ExprManager* to, ExprManagerMapC
     Expr from_e(from, new Node(n));
     Expr& to_e = vmap.d_typeMap[from_e];
     if(! to_e.isNull()) {
-Debug("export") << "+ mapped `" << from_e << "' to `" << to_e << "'" << std::endl;
+      Debug("export") << "+ mapped `" << from_e << "' to `" << to_e << "'" << std::endl;
       return to_e.getNode();
     } else {
       // construct new variable in other manager:
@@ -128,11 +128,17 @@ Debug("export") << "+ mapped `" << from_e << "' to `" << to_e << "'" << std::end
       std::string name;
       Type type = from->exportType(from_e.getType(), to, vmap);
       if(Node::fromExpr(from_e).getAttribute(VarNameAttr(), name)) {
+        // temporarily set the node manager to NULL; this gets around
+        // a check that mkVar isn't called internally
+        NodeManagerScope nullScope(NULL);
         to_e = to->mkVar(name, type);// FIXME thread safety
-Debug("export") << "+ exported var `" << from_e << "'[" << from_e.getId() << "] with name `" << name << "' and type `" << from_e.getType() << "' to `" << to_e << "'[" << to_e.getId() << "] with type `" << type << "'" << std::endl;
+        Debug("export") << "+ exported var `" << from_e << "'[" << from_e.getId() << "] with name `" << name << "' and type `" << from_e.getType() << "' to `" << to_e << "'[" << to_e.getId() << "] with type `" << type << "'" << std::endl;
       } else {
+        // temporarily set the node manager to NULL; this gets around
+        // a check that mkVar isn't called internally
+        NodeManagerScope nullScope(NULL);
         to_e = to->mkVar(type);// FIXME thread safety
-Debug("export") << "+ exported unnamed var `" << from_e << "' with type `" << from_e.getType() << "' to `" << to_e << "' with type `" << type << "'" << std::endl;
+        Debug("export") << "+ exported unnamed var `" << from_e << "' with type `" << from_e.getType() << "' to `" << to_e << "' with type `" << type << "'" << std::endl;
       }
       uint64_t to_int = (uint64_t)(to_e.getNode().d_nv);
       uint64_t from_int = (uint64_t)(from_e.getNode().d_nv);
@@ -143,16 +149,16 @@ Debug("export") << "+ exported unnamed var `" << from_e << "' with type `" << fr
     }
   } else {
     std::vector<Node> children;
-Debug("export") << "n: " << n << std::endl;
+    Debug("export") << "n: " << n << std::endl;
     if(n.getMetaKind() == kind::metakind::PARAMETERIZED) {
-Debug("export") << "+ parameterized, op is " << n.getOperator() << std::endl;
+      Debug("export") << "+ parameterized, op is " << n.getOperator() << std::endl;
       children.reserve(n.getNumChildren() + 1);
       children.push_back(exportInternal(n.getOperator(), from, to, vmap));
     } else {
       children.reserve(n.getNumChildren());
     }
     for(TNode::iterator i = n.begin(), i_end = n.end(); i != i_end; ++i) {
-Debug("export") << "+ child: " << *i << std::endl;
+      Debug("export") << "+ child: " << *i << std::endl;
       children.push_back(exportInternal(*i, from, to, vmap));
     }
     if(Debug.isOn("export")) {
@@ -281,6 +287,7 @@ Type Expr::getType(bool check) const throw (TypeCheckingException) {
 }
 
 Expr Expr::substitute(Expr e, Expr replacement) const {
+  ExprManagerScope ems(*this);
   return Expr(d_exprManager, new Node(d_node->substitute(TNode(*e.d_node), TNode(*replacement.d_node))));
 }
 
@@ -304,6 +311,7 @@ static inline NodeIteratorAdaptor<Iterator> mkNodeIteratorAdaptor(Iterator i) {
 
 Expr Expr::substitute(const std::vector<Expr> exes,
                       const std::vector<Expr>& replacements) const {
+  ExprManagerScope ems(*this);
   return Expr(d_exprManager,
               new Node(d_node->substitute(mkNodeIteratorAdaptor(exes.begin()),
                                           mkNodeIteratorAdaptor(exes.end()),
@@ -330,31 +338,39 @@ static inline NodePairIteratorAdaptor<Iterator> mkNodePairIteratorAdaptor(Iterat
 }
 
 Expr Expr::substitute(const std::hash_map<Expr, Expr, ExprHashFunction> map) const {
+  ExprManagerScope ems(*this);
   return Expr(d_exprManager, new Node(d_node->substitute(mkNodePairIteratorAdaptor(map.begin()), mkNodePairIteratorAdaptor(map.end()))));
 }
 
 Expr::const_iterator::const_iterator() :
   d_iterator(NULL) {
 }
-Expr::const_iterator::const_iterator(void* v) :
+Expr::const_iterator::const_iterator(ExprManager* em, void* v) :
+  d_exprManager(em),
   d_iterator(v) {
 }
 Expr::const_iterator::const_iterator(const const_iterator& it) {
   if(it.d_iterator == NULL) {
     d_iterator = NULL;
   } else {
+    d_exprManager = it.d_exprManager;
+    ExprManagerScope ems(*d_exprManager);
     d_iterator = new Node::iterator(*reinterpret_cast<Node::iterator*>(it.d_iterator));
   }
 }
 Expr::const_iterator& Expr::const_iterator::operator=(const const_iterator& it) {
   if(d_iterator != NULL) {
+    ExprManagerScope ems(*d_exprManager);
     delete reinterpret_cast<Node::iterator*>(d_iterator);
   }
+  d_exprManager = it.d_exprManager;
+  ExprManagerScope ems(*d_exprManager);
   d_iterator = new Node::iterator(*reinterpret_cast<Node::iterator*>(it.d_iterator));
   return *this;
 }
 Expr::const_iterator::~const_iterator() {
   if(d_iterator != NULL) {
+    ExprManagerScope ems(*d_exprManager);
     delete reinterpret_cast<Node::iterator*>(d_iterator);
   }
 }
@@ -367,26 +383,31 @@ bool Expr::const_iterator::operator==(const const_iterator& it) const {
 }
 Expr::const_iterator& Expr::const_iterator::operator++() {
   Assert(d_iterator != NULL);
+  ExprManagerScope ems(*d_exprManager);
   ++*reinterpret_cast<Node::iterator*>(d_iterator);
   return *this;
 }
 Expr::const_iterator Expr::const_iterator::operator++(int) {
   Assert(d_iterator != NULL);
+  ExprManagerScope ems(*d_exprManager);
   const_iterator it = *this;
   ++*reinterpret_cast<Node::iterator*>(d_iterator);
   return it;
 }
 Expr Expr::const_iterator::operator*() const {
   Assert(d_iterator != NULL);
+  ExprManagerScope ems(*d_exprManager);
   return (**reinterpret_cast<Node::iterator*>(d_iterator)).toExpr();
 }
 
 Expr::const_iterator Expr::begin() const {
-  return Expr::const_iterator(new Node::iterator(d_node->begin()));
+  ExprManagerScope ems(*d_exprManager);
+  return Expr::const_iterator(d_exprManager, new Node::iterator(d_node->begin()));
 }
 
 Expr::const_iterator Expr::end() const {
-  return Expr::const_iterator(new Node::iterator(d_node->end()));
+  ExprManagerScope ems(*d_exprManager);
+  return Expr::const_iterator(d_exprManager, new Node::iterator(d_node->end()));
 }
 
 std::string Expr::toString() const {
diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index e1b5cc4e6..395bdff3a 100644
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -102,12 +102,13 @@ private:
 protected:
 
   TypeCheckingException() throw() : Exception() {}
-  TypeCheckingException(const Expr& expr, std::string message) throw();
   TypeCheckingException(ExprManager* em,
                         const TypeCheckingExceptionPrivate* exc) throw();
 
 public:
 
+  TypeCheckingException(const Expr& expr, std::string message) throw();
+
   /** Copy constructor */
   TypeCheckingException(const TypeCheckingException& t) throw();
 
@@ -299,8 +300,10 @@ public:
    * Iterator type for the children of an Expr.
    */
   class const_iterator : public std::iterator<std::input_iterator_tag, Expr> {
+    ExprManager* d_exprManager;
     void* d_iterator;
-    explicit const_iterator(void*);
+
+    explicit const_iterator(ExprManager*, void*);
 
     friend class Expr;// to access void* constructor
 
@@ -957,7 +960,7 @@ public:
 
 ${getConst_instantiations}
 
-#line 961 "${template}"
+#line 964 "${template}"
 
 namespace expr {
 
diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index bd8e29a44..d67aa1fe3 100644
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -178,7 +178,7 @@ ExprManager* Type::getExprManager() const {
   return d_nodeManager->toExprManager();
 }
 
-Type Type::exportTo(ExprManager* exprManager, ExprManagerMapCollection& vmap) {
+Type Type::exportTo(ExprManager* exprManager, ExprManagerMapCollection& vmap) const {
   return ExprManager::exportType(*this, exprManager, vmap);
 }
 
diff --git a/src/expr/type.h b/src/expr/type.h
index bd6a6a298..29b0ac128 100644
--- a/src/expr/type.h
+++ b/src/expr/type.h
@@ -185,7 +185,7 @@ public:
   /**
    * Exports this type into a different ExprManager.
    */
-  Type exportTo(ExprManager* exprManager, ExprManagerMapCollection& vmap);
+  Type exportTo(ExprManager* exprManager, ExprManagerMapCollection& vmap) const;
 
   /**
    * Assignment operator.
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index 7b093d11a..e35d55e28 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -239,7 +239,7 @@ TypeNode TypeNode::leastCommonTypeNode(TypeNode t0, TypeNode t1){
       case kind::FUNCTION_TYPE:
         return TypeNode(); // Not sure if this is right
       case kind::TUPLE_TYPE:
-        Unimplemented();
+        Unimplemented("haven't implemented leastCommonType for tuples yet");
         return TypeNode(); // Not sure if this is right
       case kind::SUBTYPE_TYPE:
         if(t1.isPredicateSubtype()){
@@ -278,8 +278,11 @@ TypeNode TypeNode::leastCommonTypeNode(TypeNode t0, TypeNode t1){
           Assert(t1.isInteger());
           return TypeNode();
         }
+      case kind::DATATYPE_TYPE:
+        // two datatypes that aren't == have no common ancestors
+        return TypeNode();
       default:
-        Unimplemented();
+        Unimplemented("don't have a leastCommonType for types `%s' and `%s'", t0.toString().c_str(), t1.toString().c_str());
         return TypeNode();
       }
     }
diff --git a/src/options/Makefile.am b/src/options/Makefile.am
index 088c972b3..eb1a2c498 100644
--- a/src/options/Makefile.am
+++ b/src/options/Makefile.am
@@ -156,9 +156,9 @@ endif
 # expression (no |, no \<, ...).
 Debug_tags.tmp Trace_tags.tmp:
 	$(AM_V_GEN)\
-	grep '\<$(@:_tags.tmp=) *( *\".*\" *)' \
+	grep '\<$(@:_tags.tmp=)\(\.isOn\)* *( *\".*\" *)' \
 		`find @srcdir@/../ -name "*.cpp" -or -name "*.h" -or -name "*.cc" -or -name "*.g"` | \
-	sed 's/^$(@:_tags.tmp=) *( *\"\([^"]*\)\".*/\1/;s/.*[^a-zA-Z0-9_]$(@:_tags.tmp=) *( *\"\([^"]*\)\".*/\1/' | sort | uniq >"$@"
+	sed 's/^$(@:_tags.tmp=)\(\.isOn\)* *( *\"\([^"]*\)\".*/\2/;s/.*[^a-zA-Z0-9_]$(@:_tags.tmp=)\(\.isOn\)* *( *\"\([^"]*\)\".*/\2/' | LC_ALL=C sort | uniq >"$@"
 
 MOSTLYCLEANFILES = \
 	Debug_tags \
diff --git a/src/options/base_options b/src/options/base_options
index 10ad564e6..59fadf40b 100644
--- a/src/options/base_options
+++ b/src/options/base_options
@@ -71,9 +71,9 @@ option in std::istream* :default &std::cin :include <iostream>
 option out std::ostream* :default &std::cout :include <iostream>
 option err std::ostream* :default &std::cerr :include <iostream>
 
-common-option inputLanguage -L --lang=LANG InputLanguage :handler CVC4::options::stringToInputLanguage :include "util/language.h" :default language::input::LANG_AUTO :read-write
+common-option inputLanguage input-language -L --lang=LANG InputLanguage :handler CVC4::options::stringToInputLanguage :include "util/language.h" :default language::input::LANG_AUTO :read-write
  force input language (default is "auto"; see --lang help)
-common-option outputLanguage --output-lang=LANG OutputLanguage :handler CVC4::options::stringToOutputLanguage :include "util/language.h" :default language::output::LANG_AUTO :read-write
+common-option outputLanguage output-language --output-lang=LANG OutputLanguage :handler CVC4::options::stringToOutputLanguage :include "util/language.h" :default language::output::LANG_AUTO :read-write
  force input language (default is "auto"; see --lang help)
 option languageHelp bool
 
@@ -84,7 +84,7 @@ common-option - -v --verbose void :handler CVC4::options::increaseVerbosity
 common-option - -q --quiet void :handler CVC4::options::decreaseVerbosity
  decrease verbosity (may be repeated)
 
-common-option statistics stats --stats bool
+common-option statistics statistics --stats bool
  give statistics on exit
 
 common-option parseOnly parse-only --parse-only bool :read-write
diff --git a/src/options/base_options_handlers.h b/src/options/base_options_handlers.h
index 5f82280da..6cb74c637 100644
--- a/src/options/base_options_handlers.h
+++ b/src/options/base_options_handlers.h
@@ -38,22 +38,22 @@ inline void decreaseVerbosity(std::string option, SmtEngine* smt) {
 }
 
 inline OutputLanguage stringToOutputLanguage(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
-  if(optarg == "cvc4" || optarg == "pl") {
+  if(optarg == "cvc4" || optarg == "pl" || optarg == "presentation" || optarg == "LANG_CVC4") {
     return language::output::LANG_CVC4;
-  } else if(optarg == "smtlib" || optarg == "smt") {
+  } else if(optarg == "smtlib" || optarg == "smt" || optarg == "LANG_SMTLIB") {
     return language::output::LANG_SMTLIB;
-  } else if(optarg == "smtlib2" || optarg == "smt2") {
+  } else if(optarg == "smtlib2" || optarg == "smt2" || optarg == "LANG_SMTLIB_V2") {
     return language::output::LANG_SMTLIB_V2;
-  } else if(optarg == "tptp") {
+  } else if(optarg == "tptp" || optarg == "LANG_TPTP") {
     return language::output::LANG_TPTP;
-  } else if(optarg == "ast") {
+  } else if(optarg == "ast" || optarg == "LANG_AST") {
     return language::output::LANG_AST;
-  } else if(optarg == "auto") {
+  } else if(optarg == "auto" || optarg == "LANG_AUTO") {
     return language::output::LANG_AUTO;
   }
 
   if(optarg != "help") {
-    throw OptionException(std::string("unknown language for --output-lang: `") +
+    throw OptionException(std::string("unknown language for ") + option + ": `" +
                           optarg + "'.  Try --output-lang help.");
   }
 
@@ -62,20 +62,20 @@ inline OutputLanguage stringToOutputLanguage(std::string option, std::string opt
 }
 
 inline InputLanguage stringToInputLanguage(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
-  if(optarg == "cvc4" || optarg == "pl" || optarg == "presentation") {
+  if(optarg == "cvc4" || optarg == "pl" || optarg == "presentation" || optarg == "LANG_CVC4") {
     return language::input::LANG_CVC4;
-  } else if(optarg == "smtlib" || optarg == "smt") {
+  } else if(optarg == "smtlib" || optarg == "smt" || optarg == "LANG_SMTLIB") {
     return language::input::LANG_SMTLIB;
-  } else if(optarg == "smtlib2" || optarg == "smt2") {
+  } else if(optarg == "smtlib2" || optarg == "smt2" || optarg == "LANG_SMTLIB_V2") {
     return language::input::LANG_SMTLIB_V2;
-  } else if(optarg == "tptp") {
+  } else if(optarg == "tptp" || optarg == "LANG_TPTP") {
     return language::input::LANG_TPTP;
-  } else if(optarg == "auto") {
+  } else if(optarg == "auto" || optarg == "LANG_AUTO") {
     return language::input::LANG_AUTO;
   }
 
   if(optarg != "help") {
-    throw OptionException(std::string("unknown language for --lang: `") +
+    throw OptionException(std::string("unknown language for ") + option + ": `" +
                           optarg + "'.  Try --lang help.");
   }
 
diff --git a/src/options/option_exception.h b/src/options/option_exception.h
index 657bc7568..6aaa7d7e2 100644
--- a/src/options/option_exception.h
+++ b/src/options/option_exception.h
@@ -49,7 +49,7 @@ public:
   }
 
   UnrecognizedOptionException(const std::string& msg) :
-    CVC4::OptionException(msg) {
+    CVC4::OptionException("Unrecognized informational or option key or setting: " + msg) {
   }
 };/* class UnrecognizedOptionException */
 
diff --git a/src/smt/options b/src/smt/options
index 13b3b51f3..fea609bb5 100644
--- a/src/smt/options
+++ b/src/smt/options
@@ -21,7 +21,7 @@ common-option - --dump-to=FILE argument :handler CVC4::smt::dumpToFile :handler-
 expert-option lazyDefinitionExpansion --lazy-definition-expansion bool
  expand define-funs/LAMBDAs lazily
 
-option simplificationMode --simplification=MODE SimplificationMode :handler CVC4::smt::stringToSimplificationMode :default SIMPLIFICATION_MODE_BATCH :read-write :include "smt/simplification_mode.h" :handler-include "smt/options_handlers.h"
+option simplificationMode simplification-mode --simplification=MODE SimplificationMode :handler CVC4::smt::stringToSimplificationMode :default SIMPLIFICATION_MODE_BATCH :read-write :include "smt/simplification_mode.h" :handler-include "smt/options_handlers.h"
  choose simplification mode, see --simplification=help
 alias --no-simplification = --simplification=none
  turn off all simplification (same as --simplification=none)
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index bcd7cc6d2..d450319b1 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -310,6 +310,16 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) :
   d_context->push();
 
   d_definedFunctions = new(true) DefinedFunctionMap(d_userContext);
+}
+
+void SmtEngine::finishInit() {
+  d_decisionEngine = new DecisionEngine(d_context, d_userContext);
+  d_decisionEngine->init();   // enable appropriate strategies
+
+  d_propEngine = new PropEngine(d_theoryEngine, d_decisionEngine, d_context);
+
+  d_theoryEngine->setPropEngine(d_propEngine);
+  d_theoryEngine->setDecisionEngine(d_decisionEngine);
 
   // [MGD 10/20/2011] keep around in incremental mode, due to a
   // cleanup ordering issue and Nodes/TNodes.  If SAT is popped
@@ -336,16 +346,6 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) :
   }
 }
 
-void SmtEngine::finishInit() {
-  d_decisionEngine = new DecisionEngine(d_context, d_userContext);
-  d_decisionEngine->init();   // enable appropriate strategies
-
-  d_propEngine = new PropEngine(d_theoryEngine, d_decisionEngine, d_context);
-
-  d_theoryEngine->setPropEngine(d_propEngine);
-  d_theoryEngine->setDecisionEngine(d_decisionEngine);
-}
-
 void SmtEngine::finalOptionsAreSet() {
   if(d_fullyInited) {
     return;
@@ -1534,7 +1534,7 @@ void SmtEnginePrivate::addFormula(TNode n)
   }
 }
 
-void SmtEngine::ensureBoolean(const BoolExpr& e) {
+void SmtEngine::ensureBoolean(const BoolExpr& e) throw(TypeCheckingException) {
   Type type = e.getType(options::typeChecking());
   Type boolType = d_exprManager->booleanType();
   if(type != boolType) {
@@ -1546,7 +1546,7 @@ void SmtEngine::ensureBoolean(const BoolExpr& e) {
   }
 }
 
-Result SmtEngine::checkSat(const BoolExpr& e) {
+Result SmtEngine::checkSat(const BoolExpr& e) throw(TypeCheckingException) {
 
   Assert(e.isNull() || e.getExprManager() == d_exprManager);
 
@@ -1608,7 +1608,7 @@ Result SmtEngine::checkSat(const BoolExpr& e) {
   return r;
 }
 
-Result SmtEngine::query(const BoolExpr& e) {
+Result SmtEngine::query(const BoolExpr& e) throw(TypeCheckingException) {
 
   Assert(!e.isNull());
   Assert(e.getExprManager() == d_exprManager);
@@ -1667,7 +1667,7 @@ Result SmtEngine::query(const BoolExpr& e) {
   return r;
 }
 
-Result SmtEngine::assertFormula(const BoolExpr& e) {
+Result SmtEngine::assertFormula(const BoolExpr& e) throw(TypeCheckingException) {
   Assert(e.getExprManager() == d_exprManager);
   SmtScope smts(this);
   finalOptionsAreSet();
@@ -1680,7 +1680,7 @@ Result SmtEngine::assertFormula(const BoolExpr& e) {
   return quickCheck().asValidityResult();
 }
 
-Expr SmtEngine::simplify(const Expr& e) {
+Expr SmtEngine::simplify(const Expr& e) throw(TypeCheckingException) {
   Assert(e.getExprManager() == d_exprManager);
   SmtScope smts(this);
   finalOptionsAreSet();
@@ -1691,6 +1691,9 @@ Expr SmtEngine::simplify(const Expr& e) {
   if(Dump.isOn("benchmark")) {
     Dump("benchmark") << SimplifyCommand(e);
   }
+  // Make sure we've done simple preprocessing, unit detection, etc.
+  Trace("smt") << "SmtEngine::check(): processing assertions" << endl;
+  d_private->processAssertions();
   return d_private->applySubstitutions(e).toExpr();
 }
 
@@ -1912,6 +1915,7 @@ vector<Expr> SmtEngine::getAssertions()
     throw ModalException(msg);
   }
   Assert(d_assertionList != NULL);
+  // copy the result out
   return vector<Expr>(d_assertionList->begin(), d_assertionList->end());
 }
 
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 43a7ee58d..25800f5b3 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -234,7 +234,7 @@ class CVC4_PUBLIC SmtEngine {
    * Fully type-check the argument, and also type-check that it's
    * actually Boolean.
    */
-  void ensureBoolean(const BoolExpr& e);
+  void ensureBoolean(const BoolExpr& e) throw(TypeCheckingException);
 
   void internalPush();
 
@@ -337,20 +337,20 @@ public:
    * literals and conjunction of literals.  Returns false iff
    * inconsistent.
    */
-  Result assertFormula(const BoolExpr& e);
+  Result assertFormula(const BoolExpr& e) throw(TypeCheckingException);
 
   /**
    * Check validity of an expression with respect to the current set
    * of assertions by asserting the query expression's negation and
    * calling check().  Returns valid, invalid, or unknown result.
    */
-  Result query(const BoolExpr& e);
+  Result query(const BoolExpr& e) throw(TypeCheckingException);
 
   /**
    * Assert a formula (if provided) to the current context and call
    * check().  Returns sat, unsat, or unknown result.
    */
-  Result checkSat(const BoolExpr& e = BoolExpr());
+  Result checkSat(const BoolExpr& e = BoolExpr()) throw(TypeCheckingException);
 
   /**
    * Simplify a formula without doing "much" work.  Does not involve
@@ -361,7 +361,7 @@ public:
    * @todo (design) is this meant to give an equivalent or an
    * equisatisfiable formula?
    */
-  Expr simplify(const Expr& e);
+  Expr simplify(const Expr& e) throw(TypeCheckingException);
 
   /**
    * Get the assigned value of an expr (only if immediately preceded
diff --git a/src/smt/smt_options_template.cpp b/src/smt/smt_options_template.cpp
index b254a3b30..1af029f17 100644
--- a/src/smt/smt_options_template.cpp
+++ b/src/smt/smt_options_template.cpp
@@ -52,7 +52,7 @@ void SmtEngine::setOption(const std::string& key, const CVC4::SExpr& value)
 
 #line 54 "${template}"
 
-  throw UnrecognizedOptionException();
+  throw UnrecognizedOptionException(key);
 }
 
 CVC4::SExpr SmtEngine::getOption(const std::string& key) const
@@ -69,7 +69,7 @@ CVC4::SExpr SmtEngine::getOption(const std::string& key) const
 
 #line 71 "${template}"
 
-  throw UnrecognizedOptionException();
+  throw UnrecognizedOptionException(key);
 }
 
 }/* CVC4 namespace */
diff --git a/src/theory/arrays/kinds b/src/theory/arrays/kinds
index 986654cd3..3850fab98 100644
--- a/src/theory/arrays/kinds
+++ b/src/theory/arrays/kinds
@@ -15,9 +15,12 @@ rewriter ::CVC4::theory::arrays::TheoryArraysRewriter "theory/arrays/theory_arra
 
 operator ARRAY_TYPE 2 "array type"
 cardinality ARRAY_TYPE \
-    "::CVC4::theory::arrays::CardinalityComputer::computeCardinality(%TYPE%)" \
+    "::CVC4::theory::arrays::ArraysProperties::computeCardinality(%TYPE%)" \
+    "theory/arrays/theory_arrays_type_rules.h"
+well-founded ARRAY_TYPE \
+    "::CVC4::theory::arrays::ArraysProperties::isWellFounded(%TYPE%)" \
+    "::CVC4::theory::arrays::ArraysProperties::mkGroundTerm(%TYPE%)" \
     "theory/arrays/theory_arrays_type_rules.h"
-well-founded ARRAY_TYPE false
 
 enumerator ARRAY_TYPE \
     "::CVC4::theory::arrays::ArrayEnumerator" \
diff --git a/src/theory/arrays/theory_arrays_type_rules.h b/src/theory/arrays/theory_arrays_type_rules.h
index 8b31a31f9..854b5449f 100644
--- a/src/theory/arrays/theory_arrays_type_rules.h
+++ b/src/theory/arrays/theory_arrays_type_rules.h
@@ -22,6 +22,7 @@
 #define __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_TYPE_RULES_H
 
 #include "theory/arrays/theory_arrays_rewriter.h" // for array-constant attributes
+#include "theory/type_enumerator.h"
 
 namespace CVC4 {
 namespace theory {
@@ -37,7 +38,7 @@ struct ArraySelectTypeRule {
         throw TypeCheckingExceptionPrivate(n, "array select operating on non-array");
       }
       TypeNode indexType = n[1].getType(check);
-      if(!indexType.isSubtypeOf(arrayType.getArrayIndexType())){
+      if(!indexType.isComparableTo(arrayType.getArrayIndexType())){
         throw TypeCheckingExceptionPrivate(n, "array select not indexed with correct type for array");
       }
     }
@@ -56,10 +57,10 @@ struct ArrayStoreTypeRule {
         }
         TypeNode indexType = n[1].getType(check);
         TypeNode valueType = n[2].getType(check);
-        if(!indexType.isSubtypeOf(arrayType.getArrayIndexType())){
+        if(!indexType.isComparableTo(arrayType.getArrayIndexType())){
           throw TypeCheckingExceptionPrivate(n, "array store not indexed with correct type for array");
         }
-        if(!valueType.isSubtypeOf(arrayType.getArrayConstituentType())){
+        if(!valueType.isComparableTo(arrayType.getArrayConstituentType())){
           Debug("array-types") << "array type: "<< arrayType.getArrayConstituentType() << std::endl;
           Debug("array-types") << "value types: " << valueType << std::endl;
           throw TypeCheckingExceptionPrivate(n, "array store not assigned with correct type for array");
@@ -167,11 +168,11 @@ struct ArrayTableFunTypeRule {
         throw TypeCheckingExceptionPrivate(n, "array table fun arg 1 is non-array");
       }
       TypeNode indexType = n[2].getType(check);
-      if(!indexType.isSubtypeOf(arrayType.getArrayIndexType())){
+      if(!indexType.isComparableTo(arrayType.getArrayIndexType())){
         throw TypeCheckingExceptionPrivate(n, "array table fun arg 2 does not match type of array");
       }
       indexType = n[3].getType(check);
-      if(!indexType.isSubtypeOf(arrayType.getArrayIndexType())){
+      if(!indexType.isComparableTo(arrayType.getArrayIndexType())){
         throw TypeCheckingExceptionPrivate(n, "array table fun arg 3 does not match type of array");
       }
     }
@@ -179,7 +180,7 @@ struct ArrayTableFunTypeRule {
   }
 };/* struct ArrayTableFunTypeRule */
 
-struct CardinalityComputer {
+struct ArraysProperties {
   inline static Cardinality computeCardinality(TypeNode type) {
     Assert(type.getKind() == kind::ARRAY_TYPE);
 
@@ -188,7 +189,15 @@ struct CardinalityComputer {
 
     return valueCard ^ indexCard;
   }
-};/* struct CardinalityComputer */
+
+  inline static bool isWellFounded(TypeNode type) {
+    return type[0].isWellFounded() && type[1].isWellFounded();
+  }
+
+  inline static Node mkGroundTerm(TypeNode type) {
+    return *TypeEnumerator(type);
+  }
+};/* struct ArraysProperties */
 
 }/* CVC4::theory::arrays namespace */
 }/* CVC4::theory namespace */
diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds
index 765f6bc59..65500fe91 100644
--- a/src/theory/bv/kinds
+++ b/src/theory/bv/kinds
@@ -31,6 +31,11 @@ enumerator BITVECTOR_TYPE \
     "::CVC4::theory::bv::BitVectorEnumerator" \
     "theory/bv/type_enumerator.h"
 
+well-founded BITVECTOR_TYPE \
+    true \
+    "(*CVC4::theory::TypeEnumerator(%TYPE%))" \
+    "theory/type_enumerator.h"
+
 operator BITVECTOR_CONCAT 2: "bit-vector concatenation"
 operator BITVECTOR_AND 2: "bitwise and"
 operator BITVECTOR_OR 2: "bitwise or"
diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index 432e6ef26..7d3664d47 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -89,52 +89,6 @@ BUILT_SOURCES = \
 	rational.h \
 	integer.h \
 	tls.h
-if CVC4_DEBUG
-if CVC4_TRACING
-# listing Debug_tags too ensures that make doesn't auto-remove it
-# after building (if it does, we don't get the "cached" effect with
-# the .tmp files below, and we have to re-compile and re-link each
-# time, even when there are no changes).
-BUILT_SOURCES += \
-	Debug_tags.h \
-	Debug_tags
-endif
-endif
-if CVC4_TRACING
-# listing Trace_tags too ensures that make doesn't auto-remove it
-# after building (if it does, we don't get the "cached" effect with
-# the .tmp files below, and we have to re-compile and re-link each
-# time, even when there are no changes).
-BUILT_SOURCES += \
-	Trace_tags.h \
-	Trace_tags
-endif
-
-%_tags.h: %_tags
-	$(AM_V_GEN)( \
-	  echo 'static char const* const $^[] = {'; \
-	  for tag in `cat $^`; do \
-	    echo "\"$$tag\","; \
-	  done; \
-	  echo 'NULL'; \
-	  echo '};' \
-	) >"$@"
-
-# This .tmp business is to keep from having to re-compile options.cpp
-# (and then re-link the libraries) if nothing has changed.
-%_tags: %_tags.tmp
-	$(AM_V_GEN)\
-	diff -q "$^" "$@" &>/dev/null || mv "$^" "$@" || true
-# .PHONY ensures the .tmp version is always rebuilt (to check for any changes)
-.PHONY: Debug_tags.tmp Trace_tags.tmp
-# The "sed" invocation below is particularly obnoxious, but it works around
-# inconsistencies in REs on different platforms, using only a basic regular
-# expression (no |, no \<, ...).
-Debug_tags.tmp Trace_tags.tmp:
-	$(AM_V_GEN)\
-	grep '\<$(@:_tags.tmp=)\(\.isOn\)* *( *\".*\" *)' \
-		`find @srcdir@/../ -name "*.cpp" -or -name "*.h" -or -name "*.cc" -or -name "*.g"` | \
-	sed 's/^$(@:_tags.tmp=)\(\.isOn\)* *( *\"\([^"]*\)\".*/\2/;s/.*[^a-zA-Z0-9_]$(@:_tags.tmp=)\(\.isOn\)* *( *\"\([^"]*\)\".*/\2/' | LC_ALL=C sort | uniq >"$@"
 
 if CVC4_CLN_IMP
 libutil_la_SOURCES += \
@@ -181,10 +135,4 @@ DISTCLEANFILES = \
 	tls.h.tmp \
 	integer.h \
 	rational.h \
-	tls.h \
-	Debug_tags.tmp \
-	Debug_tags.h \
-	Debug_tags \
-	Trace_tags.tmp \
-	Trace_tags.h \
-	Trace_tags
+	tls.h
diff --git a/src/util/rational_cln_imp.h b/src/util/rational_cln_imp.h
index 258060e02..969a8b5eb 100644
--- a/src/util/rational_cln_imp.h
+++ b/src/util/rational_cln_imp.h
@@ -87,7 +87,7 @@ public:
    * For more information about what is a valid rational string,
    * see GMP's documentation for mpq_set_str().
    */
-  explicit Rational(const char * s, int base = 10) throw (std::invalid_argument){
+  explicit Rational(const char* s, unsigned base = 10) throw (std::invalid_argument){
     cln::cl_read_flags flags;
 
     flags.syntax = cln::syntax_rational;
@@ -101,7 +101,7 @@ public:
       throw std::invalid_argument(ss.str());
     }
   }
-  Rational(const std::string& s, int base = 10) throw (std::invalid_argument){
+  Rational(const std::string& s, unsigned base = 10) throw (std::invalid_argument){
     cln::cl_read_flags flags;
 
     flags.syntax = cln::syntax_rational;
diff --git a/src/util/rational_gmp_imp.h b/src/util/rational_gmp_imp.h
index 22f1e91b2..0c8a46f33 100644
--- a/src/util/rational_gmp_imp.h
+++ b/src/util/rational_gmp_imp.h
@@ -81,7 +81,7 @@ public:
    * For more information about what is a valid rational string,
    * see GMP's documentation for mpq_set_str().
    */
-  explicit Rational(const char * s, int base = 10): d_value(s,base) {
+  explicit Rational(const char* s, unsigned base = 10): d_value(s, base) {
     d_value.canonicalize();
   }
   Rational(const std::string& s, unsigned base = 10) : d_value(s, base) {