Public interface review items:

* Internal uses of CheckArgument changed to AssertArgument/AlwaysAssertArgument()
* Make util/Assert.h cvc4_private instead of public, so AssertionException and friends are now internal-only
* CheckArgument() throws non-AssertionException
* things outside the core library (parsers, driver) use regular C-style assert,
  or a public exception type.
* auto-generated documentation for Smt options and internal options

Also, a small fix to SMT-LIBv1 QF_ABV and QF_AUFBV definitions, which were nonstandard.

2 files changed, 146 insertions, 153 deletions

diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp
index b7c7013d2..95417845f 100644
--- a/src/compat/cvc3_compat.cpp
+++ b/src/compat/cvc3_compat.cpp
@@ -40,9 +40,12 @@
 #include <sstream>
 #include <algorithm>
 #include <iterator>
+#include <cassert>
 
 using namespace std;
 
+#define Unimplemented(str) throw Exception(str)
+
 namespace CVC3 {
 
 // Connects ExprManagers to ValidityCheckers.  Needed to clean up the
@@ -60,13 +63,13 @@ static bool typeHasExpr(const Type& t) {
 
 static Expr typeToExpr(const Type& t) {
   std::hash_map<Type, Expr, CVC4::TypeHashFunction>::const_iterator i = s_typeToExpr.find(t);
-  AlwaysAssert(i != s_typeToExpr.end());
+  assert(i != s_typeToExpr.end());
   return (*i).second;
 }
 
 static Type exprToType(const Expr& e) {
   std::hash_map<Expr, Type, CVC4::ExprHashFunction>::const_iterator i = s_exprToType.find(e);
-  AlwaysAssert(i != s_exprToType.end());
+  assert(i != s_exprToType.end());
   return (*i).second;
 }
 
@@ -145,7 +148,7 @@ bool operator==(const Cardinality& c, CVC3CardinalityKind d) {
     return c.isUnknown();
   }
 
-  Unhandled(d);
+  throw Exception("internal error: CVC3 cardinality kind unhandled");
 }
 
 bool operator==(CVC3CardinalityKind d, const Cardinality& c) {
@@ -431,7 +434,7 @@ Expr Expr::getExpr() const {
 }
 
 std::vector< std::vector<Expr> > Expr::getTriggers() const {
-  CheckArgument(isClosure(), *this, __PRETTY_FUNCTION__, "getTriggers() called on non-closure expr");
+  CVC4::CheckArgument(isClosure(), *this, "getTriggers() called on non-closure expr");
   if(getNumChildren() < 3) {
     // no triggers for this quantifier
     return vector< vector<Expr> >();
@@ -589,37 +592,37 @@ CLFlag& CLFlag::operator=(const CLFlag& f) {
 }
 
 CLFlag& CLFlag::operator=(bool b) {
-  CheckArgument(d_tp == CLFLAG_BOOL, this);
+  CVC4::CheckArgument(d_tp == CLFLAG_BOOL, this);
   d_data.b = b;
   return *this;
 }
 
 CLFlag& CLFlag::operator=(int i) {
-  CheckArgument(d_tp == CLFLAG_INT, this);
+  CVC4::CheckArgument(d_tp == CLFLAG_INT, this);
   d_data.i = i;
   return *this;
 }
 
 CLFlag& CLFlag::operator=(const std::string& s) {
-  CheckArgument(d_tp == CLFLAG_STRING, this);
+  CVC4::CheckArgument(d_tp == CLFLAG_STRING, this);
   *d_data.s = s;
   return *this;
 }
 
 CLFlag& CLFlag::operator=(const char* s) {
-  CheckArgument(d_tp == CLFLAG_STRING, this);
+  CVC4::CheckArgument(d_tp == CLFLAG_STRING, this);
   *d_data.s = s;
   return *this;
 }
 
 CLFlag& CLFlag::operator=(const std::pair<string, bool>& p) {
-  CheckArgument(d_tp == CLFLAG_STRVEC, this);
+  CVC4::CheckArgument(d_tp == CLFLAG_STRVEC, this);
   d_data.sv->push_back(p);
   return *this;
 }
 
 CLFlag& CLFlag::operator=(const std::vector<std::pair<string, bool> >& sv) {
-  CheckArgument(d_tp == CLFLAG_STRVEC, this);
+  CVC4::CheckArgument(d_tp == CLFLAG_STRVEC, this);
   *d_data.sv = sv;
   return *this;
 }
@@ -637,22 +640,22 @@ bool CLFlag::display() const {
 }
 
 const bool& CLFlag::getBool() const {
-  CheckArgument(d_tp == CLFLAG_BOOL, this);
+  CVC4::CheckArgument(d_tp == CLFLAG_BOOL, this);
   return d_data.b;
 }
 
 const int& CLFlag::getInt() const {
-  CheckArgument(d_tp == CLFLAG_INT, this);
+  CVC4::CheckArgument(d_tp == CLFLAG_INT, this);
   return d_data.i;
 }
 
 const std::string& CLFlag::getString() const {
-  CheckArgument(d_tp == CLFLAG_STRING, this);
+  CVC4::CheckArgument(d_tp == CLFLAG_STRING, this);
   return *d_data.s;
 }
 
 const std::vector<std::pair<string, bool> >& CLFlag::getStrVec() const {
-  CheckArgument(d_tp == CLFLAG_STRVEC, this);
+  CVC4::CheckArgument(d_tp == CLFLAG_STRVEC, this);
   return *d_data.sv;
 }
 
@@ -675,7 +678,7 @@ size_t CLFlags::countFlags(const std::string& name,
 
 const CLFlag& CLFlags::getFlag(const std::string& name) const {
   FlagMap::const_iterator i = d_map.find(name);
-  CheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported.");
+  CVC4::CheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported.");
   return (*i).second;
 }
 
@@ -685,49 +688,49 @@ const CLFlag& CLFlags::operator[](const std::string& name) const {
 
 void CLFlags::setFlag(const std::string& name, const CLFlag& f) {
   FlagMap::iterator i = d_map.find(name);
-  CheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported.");
-  CheckArgument((*i).second.getType() == f.getType(), f,
-                "Command-line flag `%s' has type %s, but caller tried to set to a %s.",
-                name.c_str(),
-                toString((*i).second.getType()).c_str(),
-                toString(f.getType()).c_str());
+  CVC4::CheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported.");
+  CVC4::CheckArgument((*i).second.getType() == f.getType(), f,
+                      "Command-line flag `%s' has type %s, but caller tried to set to a %s.",
+                      name.c_str(),
+                      toString((*i).second.getType()).c_str(),
+                      toString(f.getType()).c_str());
   (*i).second = f;
 }
 
 void CLFlags::setFlag(const std::string& name, bool b) {
   FlagMap::iterator i = d_map.find(name);
-  CheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported.");
+  CVC4::CheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported.");
   (*i).second = b;
 }
 
 void CLFlags::setFlag(const std::string& name, int i) {
   FlagMap::iterator it = d_map.find(name);
-  CheckArgument(it != d_map.end(), name, "No command-line flag by that name, or not supported.");
+  CVC4::CheckArgument(it != d_map.end(), name, "No command-line flag by that name, or not supported.");
   (*it).second = i;
 }
 
 void CLFlags::setFlag(const std::string& name, const std::string& s) {
   FlagMap::iterator i = d_map.find(name);
-  CheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported.");
+  CVC4::CheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported.");
   (*i).second = s;
 }
 
 void CLFlags::setFlag(const std::string& name, const char* s) {
   FlagMap::iterator i = d_map.find(name);
-  CheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported.");
+  CVC4::CheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported.");
   (*i).second = s;
 }
 
 void CLFlags::setFlag(const std::string& name, const std::pair<string, bool>& p) {
   FlagMap::iterator i = d_map.find(name);
-  CheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported.");
+  CVC4::CheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported.");
   (*i).second = p;
 }
 
 void CLFlags::setFlag(const std::string& name,
                       const std::vector<std::pair<string, bool> >& sv) {
   FlagMap::iterator i = d_map.find(name);
-  CheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported.");
+  CVC4::CheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported.");
   (*i).second = sv;
 }
 
@@ -1063,8 +1066,8 @@ Type ValidityChecker::intType() {
 Type ValidityChecker::subrangeType(const Expr& l, const Expr& r) {
   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_RATIONAL && l.getConst<Rational>().isIntegral()), l);
-  CheckArgument(noUpperBound || (r.getKind() == CVC4::kind::CONST_RATIONAL && r.getConst<Rational>().isIntegral()), r);
+  CVC4::CheckArgument(noLowerBound || (l.getKind() == CVC4::kind::CONST_RATIONAL && l.getConst<Rational>().isIntegral()), l);
+  CVC4::CheckArgument(noUpperBound || (r.getKind() == CVC4::kind::CONST_RATIONAL && r.getConst<Rational>().isIntegral()), r);
   CVC4::SubrangeBound bl = noLowerBound ? CVC4::SubrangeBound() : CVC4::SubrangeBound(l.getConst<Rational>().getNumerator());
   CVC4::SubrangeBound br = noUpperBound ? CVC4::SubrangeBound() : CVC4::SubrangeBound(r.getConst<Rational>().getNumerator());
   return d_em->mkSubrangeType(CVC4::SubrangeBounds(bl, br));
@@ -1123,7 +1126,7 @@ Type ValidityChecker::dataType(const std::string& name,
                                const std::string& constructor,
                                const std::vector<std::string>& selectors,
                                const std::vector<Expr>& types) {
-  CheckArgument(selectors.size() == types.size(), types, "expected selectors and types vectors to be of equal length");
+  CVC4::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;
@@ -1137,8 +1140,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) {
-  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");
+  CVC4::CheckArgument(constructors.size() == selectors.size(), selectors, "expected constructors and selectors vectors to be of equal length");
+  CVC4::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;
@@ -1149,7 +1152,7 @@ Type ValidityChecker::dataType(const std::string& name,
   tv.push_back(types);
   vector<Type> dtts;
   dataType(nv, cv, sv, tv, dtts);
-  AlwaysAssert(dtts.size() == 1);
+  assert(dtts.size() == 1);
   return dtts[0];
 }
 
@@ -1159,19 +1162,19 @@ void ValidityChecker::dataType(const std::vector<std::string>& names,
                                const std::vector<std::vector<std::vector<Expr> > >& types,
                                std::vector<Type>& returnTypes) {
 
-  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");
+  CVC4::CheckArgument(names.size() == constructors.size(), constructors, "expected names and constructors vectors to be of equal length");
+  CVC4::CheckArgument(names.size() == selectors.size(), selectors, "expected names and selectors vectors to be of equal length");
+  CVC4::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]);
-    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");
+    CVC4::CheckArgument(constructors[i].size() == selectors[i].size(), "expected sub-vectors in constructors and selectors vectors to match in size");
+    CVC4::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]);
-      CheckArgument(selectors[i][j].size() == types[i][j].size(), types, "expected sub-vectors in selectors and types vectors to match in size");
+      CVC4::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>()));
@@ -1200,10 +1203,10 @@ void ValidityChecker::dataType(const std::vector<std::string>& names,
     }
     for(CVC4::Datatype::const_iterator j = dt.begin(); j != dt.end(); ++j) {
       // For each constructor, register its name and its selectors names.
-      CheckArgument(d_constructors.find((*j).getName()) == d_constructors.end(), constructors, "cannot have two constructors with the same name in a ValidityChecker");
+      CVC4::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) {
-        CheckArgument(d_selectors.find((*k).getName()) == d_selectors.end(), selectors, "cannot have two selectors with the same name in a ValidityChecker");
+        CVC4::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());
       }
     }
@@ -1219,7 +1222,7 @@ Type ValidityChecker::arrayType(const Type& typeIndex, const Type& typeData) {
 }
 
 Type ValidityChecker::bitvecType(int n) {
-  CheckArgument(n >= 0, n, "cannot construct a bitvector type of negative size");
+  CVC4::CheckArgument(n >= 0, n, "cannot construct a bitvector type of negative size");
   return d_em->mkBitVectorType(n);
 }
 
@@ -1255,7 +1258,7 @@ Expr ValidityChecker::varExpr(const std::string& name, const Type& type) {
 
 Expr ValidityChecker::varExpr(const std::string& name, const Type& type,
                               const Expr& def) {
-  FatalAssert(def.getType() == type, "expected types to match");
+  CVC4::CheckArgument(def.getType() == type, def, "expected types to match");
   d_parserContext->defineVar(name, def);
 }
 
@@ -1281,7 +1284,7 @@ Type ValidityChecker::getBaseType(const Type& t) {
   if(type.isReal()) {
     return d_em->realType();
   }
-  Assert(!type.isInteger());// should be handled by Real
+  assert(!type.isInteger());// should be handled by Real
   if(type.isBoolean()) {
     return d_em->booleanType();
   }
@@ -1418,7 +1421,7 @@ Expr ValidityChecker::andExpr(const Expr& left, const Expr& right) {
 
 Expr ValidityChecker::andExpr(const std::vector<Expr>& children) {
   // AND must have at least 2 children
-  CheckArgument(children.size() > 0, children);
+  CVC4::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)));
 }
 
@@ -1428,7 +1431,7 @@ Expr ValidityChecker::orExpr(const Expr& left, const Expr& right) {
 
 Expr ValidityChecker::orExpr(const std::vector<Expr>& children) {
   // OR must have at least 2 children
-  CheckArgument(children.size() > 0, children);
+  CVC4::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)));
 }
 
@@ -1450,7 +1453,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");
+  CVC4::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);
@@ -1462,7 +1465,7 @@ Op ValidityChecker::createOp(const std::string& name, const Type& type) {
 
 Op ValidityChecker::createOp(const std::string& name, const Type& type,
                              const Expr& def) {
-  CheckArgument(def.getType() == type, type,
+  CVC4::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());
@@ -1512,7 +1515,7 @@ Expr ValidityChecker::ratExpr(const std::string& n, int base) {
   if(n.find(".") == string::npos) {
     return d_em->mkConst(Rational(n, base));
   } else {
-    CheckArgument(base == 10, base, "unsupported base for decimal parsing");
+    CVC4::CheckArgument(base == 10, base, "unsupported base for decimal parsing");
     return d_em->mkConst(Rational::fromDecimal(n));
   }
 }
@@ -1527,7 +1530,7 @@ Expr ValidityChecker::plusExpr(const Expr& left, const Expr& right) {
 
 Expr ValidityChecker::plusExpr(const std::vector<Expr>& children) {
   // PLUS must have at least 2 children
-  CheckArgument(children.size() > 0, children);
+  CVC4::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)));
 }
 
@@ -1618,9 +1621,9 @@ Expr ValidityChecker::newBVConstExpr(const std::vector<bool>& bits) {
 Expr ValidityChecker::newBVConstExpr(const Rational& r, int len) {
   // implementation based on CVC3's TheoryBitvector::newBVConstExpr()
 
-  CheckArgument(r.getDenominator() == 1, r, "ValidityChecker::newBVConstExpr: "
+  CVC4::CheckArgument(r.getDenominator() == 1, r, "ValidityChecker::newBVConstExpr: "
                 "not an integer: `%s'", r.toString().c_str());
-  CheckArgument(len > 0, len, "ValidityChecker::newBVConstExpr: "
+  CVC4::CheckArgument(len > 0, len, "ValidityChecker::newBVConstExpr: "
                 "len = %d", len);
 
   string s(r.toString(2));
@@ -1643,8 +1646,8 @@ Expr ValidityChecker::newBVConstExpr(const Rational& r, int len) {
 }
 
 Expr ValidityChecker::newConcatExpr(const Expr& t1, const Expr& t2) {
-  CheckArgument(t1.getType().isBitVector(), t1, "can only concat a bitvector, not a `%s'", t1.getType().toString().c_str());
-  CheckArgument(t2.getType().isBitVector(), t2, "can only concat a bitvector, not a `%s'", t2.getType().toString().c_str());
+  CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only concat a bitvector, not a `%s'", t1.getType().toString().c_str());
+  CVC4::CheckArgument(t2.getType().isBitVector(), t2, "can only concat a bitvector, not a `%s'", t2.getType().toString().c_str());
   return d_em->mkExpr(CVC4::kind::BITVECTOR_CONCAT, t1, t2);
 }
 
@@ -1655,29 +1658,29 @@ Expr ValidityChecker::newConcatExpr(const std::vector<Expr>& kids) {
 }
 
 Expr ValidityChecker::newBVExtractExpr(const Expr& e, int hi, int low) {
-  CheckArgument(e.getType().isBitVector(), e, "can only bvextract from a bitvector, not a `%s'", e.getType().toString().c_str());
-  CheckArgument(hi >= low, hi, "extraction [%d:%d] is bad; possibly inverted?", hi, low);
-  CheckArgument(low >= 0, low, "extraction [%d:%d] is bad (negative)", hi, low);
-  CheckArgument(CVC4::BitVectorType(e.getType()).getSize() > unsigned(hi), hi, "bitvector is of size %u, extraction [%d:%d] is off-the-end", CVC4::BitVectorType(e.getType()).getSize(), hi, low);
+  CVC4::CheckArgument(e.getType().isBitVector(), e, "can only bvextract from a bitvector, not a `%s'", e.getType().toString().c_str());
+  CVC4::CheckArgument(hi >= low, hi, "extraction [%d:%d] is bad; possibly inverted?", hi, low);
+  CVC4::CheckArgument(low >= 0, low, "extraction [%d:%d] is bad (negative)", hi, low);
+  CVC4::CheckArgument(CVC4::BitVectorType(e.getType()).getSize() > unsigned(hi), hi, "bitvector is of size %u, extraction [%d:%d] is off-the-end", CVC4::BitVectorType(e.getType()).getSize(), hi, low);
   return d_em->mkExpr(CVC4::kind::BITVECTOR_EXTRACT,
                      d_em->mkConst(CVC4::BitVectorExtract(hi, low)), e);
 }
 
 Expr ValidityChecker::newBVNegExpr(const Expr& t1) {
   // CVC3's BVNEG => SMT-LIBv2 bvnot
-  CheckArgument(t1.getType().isBitVector(), t1, "can only bvneg a bitvector, not a `%s'", t1.getType().toString().c_str());
+  CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only bvneg a bitvector, not a `%s'", t1.getType().toString().c_str());
   return d_em->mkExpr(CVC4::kind::BITVECTOR_NOT, t1);
 }
 
 Expr ValidityChecker::newBVAndExpr(const Expr& t1, const Expr& t2) {
-  CheckArgument(t1.getType().isBitVector(), t1, "can only bvand a bitvector, not a `%s'", t1.getType().toString().c_str());
-  CheckArgument(t2.getType().isBitVector(), t2, "can only bvand a bitvector, not a `%s'", t2.getType().toString().c_str());
+  CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only bvand a bitvector, not a `%s'", t1.getType().toString().c_str());
+  CVC4::CheckArgument(t2.getType().isBitVector(), t2, "can only bvand a bitvector, not a `%s'", t2.getType().toString().c_str());
   return d_em->mkExpr(CVC4::kind::BITVECTOR_AND, t1, t2);
 }
 
 Expr ValidityChecker::newBVAndExpr(const std::vector<Expr>& kids) {
   // BITVECTOR_AND is not N-ary in CVC4
-  CheckArgument(kids.size() > 1, kids, "BITVECTOR_AND must have at least 2 children");
+  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()) {
@@ -1687,14 +1690,14 @@ Expr ValidityChecker::newBVAndExpr(const std::vector<Expr>& kids) {
 }
 
 Expr ValidityChecker::newBVOrExpr(const Expr& t1, const Expr& t2) {
-  CheckArgument(t1.getType().isBitVector(), t1, "can only bvor a bitvector, not a `%s'", t1.getType().toString().c_str());
-  CheckArgument(t2.getType().isBitVector(), t2, "can only bvor a bitvector, not a `%s'", t2.getType().toString().c_str());
+  CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only bvor a bitvector, not a `%s'", t1.getType().toString().c_str());
+  CVC4::CheckArgument(t2.getType().isBitVector(), t2, "can only bvor a bitvector, not a `%s'", t2.getType().toString().c_str());
   return d_em->mkExpr(CVC4::kind::BITVECTOR_OR, t1, t2);
 }
 
 Expr ValidityChecker::newBVOrExpr(const std::vector<Expr>& kids) {
   // BITVECTOR_OR is not N-ary in CVC4
-  CheckArgument(kids.size() > 1, kids, "BITVECTOR_OR must have at least 2 children");
+  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()) {
@@ -1704,14 +1707,14 @@ Expr ValidityChecker::newBVOrExpr(const std::vector<Expr>& kids) {
 }
 
 Expr ValidityChecker::newBVXorExpr(const Expr& t1, const Expr& t2) {
-  CheckArgument(t1.getType().isBitVector(), t1, "can only bvxor a bitvector, not a `%s'", t1.getType().toString().c_str());
-  CheckArgument(t2.getType().isBitVector(), t2, "can only bvxor a bitvector, not a `%s'", t2.getType().toString().c_str());
+  CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only bvxor a bitvector, not a `%s'", t1.getType().toString().c_str());
+  CVC4::CheckArgument(t2.getType().isBitVector(), t2, "can only bvxor a bitvector, not a `%s'", t2.getType().toString().c_str());
   return d_em->mkExpr(CVC4::kind::BITVECTOR_XOR, t1, t2);
 }
 
 Expr ValidityChecker::newBVXorExpr(const std::vector<Expr>& kids) {
   // BITVECTOR_XOR is not N-ary in CVC4
-  CheckArgument(kids.size() > 1, kids, "BITVECTOR_XOR must have at least 2 children");
+  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()) {
@@ -1721,14 +1724,14 @@ Expr ValidityChecker::newBVXorExpr(const std::vector<Expr>& kids) {
 }
 
 Expr ValidityChecker::newBVXnorExpr(const Expr& t1, const Expr& t2) {
-  CheckArgument(t1.getType().isBitVector(), t1, "can only bvxnor a bitvector, not a `%s'", t1.getType().toString().c_str());
-  CheckArgument(t2.getType().isBitVector(), t2, "can only bvxnor a bitvector, not a `%s'", t2.getType().toString().c_str());
+  CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only bvxnor a bitvector, not a `%s'", t1.getType().toString().c_str());
+  CVC4::CheckArgument(t2.getType().isBitVector(), t2, "can only bvxnor a bitvector, not a `%s'", t2.getType().toString().c_str());
   return d_em->mkExpr(CVC4::kind::BITVECTOR_XNOR, t1, t2);
 }
 
 Expr ValidityChecker::newBVXnorExpr(const std::vector<Expr>& kids) {
   // BITVECTOR_XNOR is not N-ary in CVC4
-  CheckArgument(kids.size() > 1, kids, "BITVECTOR_XNOR must have at least 2 children");
+  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()) {
@@ -1738,73 +1741,73 @@ Expr ValidityChecker::newBVXnorExpr(const std::vector<Expr>& kids) {
 }
 
 Expr ValidityChecker::newBVNandExpr(const Expr& t1, const Expr& t2) {
-  CheckArgument(t1.getType().isBitVector(), t1, "can only bvnand a bitvector, not a `%s'", t1.getType().toString().c_str());
-  CheckArgument(t2.getType().isBitVector(), t2, "can only bvnand a bitvector, not a `%s'", t2.getType().toString().c_str());
+  CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only bvnand a bitvector, not a `%s'", t1.getType().toString().c_str());
+  CVC4::CheckArgument(t2.getType().isBitVector(), t2, "can only bvnand a bitvector, not a `%s'", t2.getType().toString().c_str());
   return d_em->mkExpr(CVC4::kind::BITVECTOR_NAND, t1, t2);
 }
 
 Expr ValidityChecker::newBVNorExpr(const Expr& t1, const Expr& t2) {
-  CheckArgument(t1.getType().isBitVector(), t1, "can only bvnor a bitvector, not a `%s'", t1.getType().toString().c_str());
-  CheckArgument(t2.getType().isBitVector(), t2, "can only bvnor a bitvector, not a `%s'", t2.getType().toString().c_str());
+  CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only bvnor a bitvector, not a `%s'", t1.getType().toString().c_str());
+  CVC4::CheckArgument(t2.getType().isBitVector(), t2, "can only bvnor a bitvector, not a `%s'", t2.getType().toString().c_str());
   return d_em->mkExpr(CVC4::kind::BITVECTOR_NOR, t1, t2);
 }
 
 Expr ValidityChecker::newBVCompExpr(const Expr& t1, const Expr& t2) {
-  CheckArgument(t1.getType().isBitVector(), t1, "can only bvcomp a bitvector, not a `%s'", t1.getType().toString().c_str());
-  CheckArgument(t2.getType().isBitVector(), t2, "can only bvcomp a bitvector, not a `%s'", t2.getType().toString().c_str());
+  CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only bvcomp a bitvector, not a `%s'", t1.getType().toString().c_str());
+  CVC4::CheckArgument(t2.getType().isBitVector(), t2, "can only bvcomp a bitvector, not a `%s'", t2.getType().toString().c_str());
   return d_em->mkExpr(CVC4::kind::BITVECTOR_COMP, t1, t2);
 }
 
 Expr ValidityChecker::newBVLTExpr(const Expr& t1, const Expr& t2) {
-  CheckArgument(t1.getType().isBitVector(), t1, "can only bvlt a bitvector, not a `%s'", t1.getType().toString().c_str());
-  CheckArgument(t2.getType().isBitVector(), t2, "can only bvlt a bitvector, not a `%s'", t2.getType().toString().c_str());
+  CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only bvlt a bitvector, not a `%s'", t1.getType().toString().c_str());
+  CVC4::CheckArgument(t2.getType().isBitVector(), t2, "can only bvlt a bitvector, not a `%s'", t2.getType().toString().c_str());
   return d_em->mkExpr(CVC4::kind::BITVECTOR_ULT, t1, t2);
 }
 
 Expr ValidityChecker::newBVLEExpr(const Expr& t1, const Expr& t2) {
-  CheckArgument(t1.getType().isBitVector(), t1, "can only bvle a bitvector, not a `%s'", t1.getType().toString().c_str());
-  CheckArgument(t2.getType().isBitVector(), t2, "can only bvle a bitvector, not a `%s'", t2.getType().toString().c_str());
+  CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only bvle a bitvector, not a `%s'", t1.getType().toString().c_str());
+  CVC4::CheckArgument(t2.getType().isBitVector(), t2, "can only bvle a bitvector, not a `%s'", t2.getType().toString().c_str());
   return d_em->mkExpr(CVC4::kind::BITVECTOR_ULE, t1, t2);
 }
 
 Expr ValidityChecker::newBVSLTExpr(const Expr& t1, const Expr& t2) {
-  CheckArgument(t1.getType().isBitVector(), t1, "can only bvslt a bitvector, not a `%s'", t1.getType().toString().c_str());
-  CheckArgument(t2.getType().isBitVector(), t2, "can only bvslt a bitvector, not a `%s'", t2.getType().toString().c_str());
+  CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only bvslt a bitvector, not a `%s'", t1.getType().toString().c_str());
+  CVC4::CheckArgument(t2.getType().isBitVector(), t2, "can only bvslt a bitvector, not a `%s'", t2.getType().toString().c_str());
   return d_em->mkExpr(CVC4::kind::BITVECTOR_SLT, t1, t2);
 }
 
 Expr ValidityChecker::newBVSLEExpr(const Expr& t1, const Expr& t2) {
-  CheckArgument(t1.getType().isBitVector(), t1, "can only bvsle a bitvector, not a `%s'", t1.getType().toString().c_str());
-  CheckArgument(t2.getType().isBitVector(), t2, "can only bvsle a bitvector, not a `%s'", t2.getType().toString().c_str());
+  CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only bvsle a bitvector, not a `%s'", t1.getType().toString().c_str());
+  CVC4::CheckArgument(t2.getType().isBitVector(), t2, "can only bvsle a bitvector, not a `%s'", t2.getType().toString().c_str());
   return d_em->mkExpr(CVC4::kind::BITVECTOR_SLE, t1, t2);
 }
 
 Expr ValidityChecker::newSXExpr(const Expr& t1, int len) {
-  CheckArgument(t1.getType().isBitVector(), t1, "can only sx a bitvector, not a `%s'", t1.getType().toString().c_str());
-  CheckArgument(len >= 0, len, "must sx by a positive integer");
-  CheckArgument(unsigned(len) >= CVC4::BitVectorType(t1.getType()).getSize(), len, "cannot sx by something smaller than the bitvector (%d < %u)", len, CVC4::BitVectorType(t1.getType()).getSize());
+  CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only sx a bitvector, not a `%s'", t1.getType().toString().c_str());
+  CVC4::CheckArgument(len >= 0, len, "must sx by a positive integer");
+  CVC4::CheckArgument(unsigned(len) >= CVC4::BitVectorType(t1.getType()).getSize(), len, "cannot sx by something smaller than the bitvector (%d < %u)", len, CVC4::BitVectorType(t1.getType()).getSize());
   return d_em->mkExpr(CVC4::kind::BITVECTOR_SIGN_EXTEND,
                      d_em->mkConst(CVC4::BitVectorSignExtend(len)), t1);
 }
 
 Expr ValidityChecker::newBVUminusExpr(const Expr& t1) {
   // CVC3's BVUMINUS => SMT-LIBv2 bvneg
-  CheckArgument(t1.getType().isBitVector(), t1, "can only bvuminus a bitvector, not a `%s'", t1.getType().toString().c_str());
+  CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only bvuminus a bitvector, not a `%s'", t1.getType().toString().c_str());
   return d_em->mkExpr(CVC4::kind::BITVECTOR_NEG, t1);
 }
 
 Expr ValidityChecker::newBVSubExpr(const Expr& t1, const Expr& t2) {
-  CheckArgument(t1.getType().isBitVector(), t1, "can only bvsub a bitvector, not a `%s'", t1.getType().toString().c_str());
-  CheckArgument(t2.getType().isBitVector(), t2, "can only bvsub by a bitvector, not a `%s'", t2.getType().toString().c_str());
+  CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only bvsub a bitvector, not a `%s'", t1.getType().toString().c_str());
+  CVC4::CheckArgument(t2.getType().isBitVector(), t2, "can only bvsub by a bitvector, not a `%s'", t2.getType().toString().c_str());
   return d_em->mkExpr(CVC4::kind::BITVECTOR_SUB, t1, t2);
 }
 
 // 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,
+  CVC4::CheckArgument(len >= 0, len,
                 "padding length must be a non-negative integer, not %d", len);
-  CheckArgument(e.getType().isBitVector(), e,
+  CVC4::CheckArgument(e.getType().isBitVector(), e,
                 "input to bitvector operation must be a bitvector");
 
   unsigned size = CVC4::BitVectorType(e.getType()).getSize();
@@ -1823,89 +1826,89 @@ Expr ValidityChecker::bvpad(int len, const Expr& e) {
 
 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");
+  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,
+  CVC4::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());
+  CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only bvplus a bitvector, not a `%s'", t1.getType().toString().c_str());
+  CVC4::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, bvpad(numbits, t1), bvpad(numbits, t2));
   unsigned size = CVC4::BitVectorType(e.getType()).getSize();
-  CheckArgument(unsigned(numbits) == size, numbits,
+  CVC4::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::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());
+  CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only bvmult a bitvector, not a `%s'", t1.getType().toString().c_str());
+  CVC4::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, bvpad(numbits, t1), bvpad(numbits, t2));
   unsigned size = CVC4::BitVectorType(e.getType()).getSize();
-  CheckArgument(unsigned(numbits) == size, numbits,
+  CVC4::CheckArgument(unsigned(numbits) == size, numbits,
                 "argument must match computed size of bitvector product: "
                 "passed size == %u, computed size == %u", numbits, size);
   return e;
 }
 
 Expr ValidityChecker::newBVUDivExpr(const Expr& t1, const Expr& t2) {
-  CheckArgument(t1.getType().isBitVector(), t1, "can only bvudiv a bitvector, not a `%s'", t1.getType().toString().c_str());
-  CheckArgument(t2.getType().isBitVector(), t2, "can only bvudiv by a bitvector, not a `%s'", t2.getType().toString().c_str());
+  CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only bvudiv a bitvector, not a `%s'", t1.getType().toString().c_str());
+  CVC4::CheckArgument(t2.getType().isBitVector(), t2, "can only bvudiv by a bitvector, not a `%s'", t2.getType().toString().c_str());
   return d_em->mkExpr(CVC4::kind::BITVECTOR_UDIV, t1, t2);
 }
 
 Expr ValidityChecker::newBVURemExpr(const Expr& t1, const Expr& t2) {
-  CheckArgument(t1.getType().isBitVector(), t1, "can only bvurem a bitvector, not a `%s'", t1.getType().toString().c_str());
-  CheckArgument(t2.getType().isBitVector(), t2, "can only bvurem by a bitvector, not a `%s'", t2.getType().toString().c_str());
+  CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only bvurem a bitvector, not a `%s'", t1.getType().toString().c_str());
+  CVC4::CheckArgument(t2.getType().isBitVector(), t2, "can only bvurem by a bitvector, not a `%s'", t2.getType().toString().c_str());
   return d_em->mkExpr(CVC4::kind::BITVECTOR_UREM, t1, t2);
 }
 
 Expr ValidityChecker::newBVSDivExpr(const Expr& t1, const Expr& t2) {
-  CheckArgument(t1.getType().isBitVector(), t1, "can only bvsdiv a bitvector, not a `%s'", t1.getType().toString().c_str());
-  CheckArgument(t2.getType().isBitVector(), t2, "can only bvsdiv by a bitvector, not a `%s'", t2.getType().toString().c_str());
+  CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only bvsdiv a bitvector, not a `%s'", t1.getType().toString().c_str());
+  CVC4::CheckArgument(t2.getType().isBitVector(), t2, "can only bvsdiv by a bitvector, not a `%s'", t2.getType().toString().c_str());
   return d_em->mkExpr(CVC4::kind::BITVECTOR_SDIV, t1, t2);
 }
 
 Expr ValidityChecker::newBVSRemExpr(const Expr& t1, const Expr& t2) {
-  CheckArgument(t1.getType().isBitVector(), t1, "can only bvsrem a bitvector, not a `%s'", t1.getType().toString().c_str());
-  CheckArgument(t2.getType().isBitVector(), t2, "can only bvsrem by a bitvector, not a `%s'", t2.getType().toString().c_str());
+  CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only bvsrem a bitvector, not a `%s'", t1.getType().toString().c_str());
+  CVC4::CheckArgument(t2.getType().isBitVector(), t2, "can only bvsrem by a bitvector, not a `%s'", t2.getType().toString().c_str());
   return d_em->mkExpr(CVC4::kind::BITVECTOR_SREM, t1, t2);
 }
 
 Expr ValidityChecker::newBVSModExpr(const Expr& t1, const Expr& t2) {
-  CheckArgument(t1.getType().isBitVector(), t1, "can only bvsmod a bitvector, not a `%s'", t1.getType().toString().c_str());
-  CheckArgument(t2.getType().isBitVector(), t2, "can only bvsmod by a bitvector, not a `%s'", t2.getType().toString().c_str());
+  CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only bvsmod a bitvector, not a `%s'", t1.getType().toString().c_str());
+  CVC4::CheckArgument(t2.getType().isBitVector(), t2, "can only bvsmod by a bitvector, not a `%s'", t2.getType().toString().c_str());
   return d_em->mkExpr(CVC4::kind::BITVECTOR_SMOD, t1, t2);
 }
 
 Expr ValidityChecker::newFixedLeftShiftExpr(const Expr& t1, int r) {
-  CheckArgument(t1.getType().isBitVector(), t1, "can only left-shift a bitvector, not a `%s'", t1.getType().toString().c_str());
-  CheckArgument(r >= 0, r, "left shift amount must be >= 0 (you passed %d)", r);
+  CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only left-shift a bitvector, not a `%s'", t1.getType().toString().c_str());
+  CVC4::CheckArgument(r >= 0, r, "left shift amount must be >= 0 (you passed %d)", r);
   // Defined in:
   // http://www.cs.nyu.edu/acsys/cvc3/doc/user_doc.html#user_doc_pres_lang_expr_bit
   return d_em->mkExpr(CVC4::kind::BITVECTOR_CONCAT, t1, d_em->mkConst(CVC4::BitVector(r)));
 }
 
 Expr ValidityChecker::newFixedConstWidthLeftShiftExpr(const Expr& t1, int r) {
-  CheckArgument(t1.getType().isBitVector(), t1, "can only right-shift a bitvector, not a `%s'", t1.getType().toString().c_str());
-  CheckArgument(r >= 0, r, "const-width left shift amount must be >= 0 (you passed %d)", r);
+  CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only right-shift a bitvector, not a `%s'", t1.getType().toString().c_str());
+  CVC4::CheckArgument(r >= 0, r, "const-width left shift amount must be >= 0 (you passed %d)", r);
   // just turn it into a BVSHL
   return d_em->mkExpr(CVC4::kind::BITVECTOR_SHL, t1, d_em->mkConst(CVC4::BitVector(CVC4::BitVectorType(t1.getType()).getSize(), unsigned(r))));
 }
 
 Expr ValidityChecker::newFixedRightShiftExpr(const Expr& t1, int r) {
-  CheckArgument(t1.getType().isBitVector(), t1, "can only right-shift a bitvector, not a `%s'", t1.getType().toString().c_str());
-  CheckArgument(r >= 0, r, "right shift amount must be >= 0 (you passed %d)", r);
+  CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only right-shift a bitvector, not a `%s'", t1.getType().toString().c_str());
+  CVC4::CheckArgument(r >= 0, r, "right shift amount must be >= 0 (you passed %d)", r);
   // Defined in:
   // http://www.cs.nyu.edu/acsys/cvc3/doc/user_doc.html#user_doc_pres_lang_expr_bit
   // Should be equivalent to a BVLSHR; just turn it into that.
@@ -1913,20 +1916,20 @@ Expr ValidityChecker::newFixedRightShiftExpr(const Expr& t1, int r) {
 }
 
 Expr ValidityChecker::newBVSHL(const Expr& t1, const Expr& t2) {
-  CheckArgument(t1.getType().isBitVector(), t1, "can only right-shift a bitvector, not a `%s'", t1.getType().toString().c_str());
-  CheckArgument(t2.getType().isBitVector(), t2, "can only right-shift by a bitvector, not a `%s'", t2.getType().toString().c_str());
+  CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only right-shift a bitvector, not a `%s'", t1.getType().toString().c_str());
+  CVC4::CheckArgument(t2.getType().isBitVector(), t2, "can only right-shift by a bitvector, not a `%s'", t2.getType().toString().c_str());
   return d_em->mkExpr(CVC4::kind::BITVECTOR_SHL, t1, t2);
 }
 
 Expr ValidityChecker::newBVLSHR(const Expr& t1, const Expr& t2) {
-  CheckArgument(t1.getType().isBitVector(), t1, "can only right-shift a bitvector, not a `%s'", t1.getType().toString().c_str());
-  CheckArgument(t2.getType().isBitVector(), t2, "can only right-shift by a bitvector, not a `%s'", t2.getType().toString().c_str());
+  CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only right-shift a bitvector, not a `%s'", t1.getType().toString().c_str());
+  CVC4::CheckArgument(t2.getType().isBitVector(), t2, "can only right-shift by a bitvector, not a `%s'", t2.getType().toString().c_str());
   return d_em->mkExpr(CVC4::kind::BITVECTOR_LSHR, t1, t2);
 }
 
 Expr ValidityChecker::newBVASHR(const Expr& t1, const Expr& t2) {
-  CheckArgument(t1.getType().isBitVector(), t1, "can only right-shift a bitvector, not a `%s'", t1.getType().toString().c_str());
-  CheckArgument(t2.getType().isBitVector(), t2, "can only right-shift by a bitvector, not a `%s'", t2.getType().toString().c_str());
+  CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only right-shift a bitvector, not a `%s'", t1.getType().toString().c_str());
+  CVC4::CheckArgument(t2.getType().isBitVector(), t2, "can only right-shift by a bitvector, not a `%s'", t2.getType().toString().c_str());
   return d_em->mkExpr(CVC4::kind::BITVECTOR_ASHR, t1, t2);
 }
 
@@ -1951,16 +1954,16 @@ Expr ValidityChecker::tupleUpdateExpr(const Expr& tuple, int index,
 
 Expr ValidityChecker::datatypeConsExpr(const std::string& constructor, const std::vector<Expr>& args) {
   ConstructorMap::const_iterator i = d_constructors.find(constructor);
-  AlwaysAssert(i != d_constructors.end(), "no such constructor");
+  CVC4::CheckArgument(i != d_constructors.end(), constructor, "no such constructor");
   const CVC4::Datatype& dt = *(*i).second;
   const CVC4::DatatypeConstructor& ctor = dt[constructor];
-  AlwaysAssert(ctor.getNumArgs() == args.size(), "arity mismatch in constructor application");
+  CVC4::CheckArgument(ctor.getNumArgs() == args.size(), args, "arity mismatch in constructor application");
   return d_em->mkExpr(CVC4::kind::APPLY_CONSTRUCTOR, ctor.getConstructor(), vector<CVC4::Expr>(args.begin(), args.end()));
 }
 
 Expr ValidityChecker::datatypeSelExpr(const std::string& selector, const Expr& arg) {
   SelectorMap::const_iterator i = d_selectors.find(selector);
-  AlwaysAssert(i != d_selectors.end(), "no such selector");
+  CVC4::CheckArgument(i != d_selectors.end(), selector, "no such selector");
   const CVC4::Datatype& dt = *(*i).second.first;
   string constructor = (*i).second.second;
   const CVC4::DatatypeConstructor& ctor = dt[constructor];
@@ -1969,7 +1972,7 @@ Expr ValidityChecker::datatypeSelExpr(const std::string& selector, const Expr& a
 
 Expr ValidityChecker::datatypeTestExpr(const std::string& constructor, const Expr& arg) {
   ConstructorMap::const_iterator i = d_constructors.find(constructor);
-  AlwaysAssert(i != d_constructors.end(), "no such constructor");
+  CVC4::CheckArgument(i != d_constructors.end(), constructor, "no such constructor");
   const CVC4::Datatype& dt = *(*i).second;
   const CVC4::DatatypeConstructor& ctor = dt[constructor];
   return d_em->mkExpr(CVC4::kind::APPLY_TESTER, ctor.getTester(), arg);
@@ -2122,7 +2125,7 @@ void ValidityChecker::returnFromCheck() {
 }
 
 void ValidityChecker::getUserAssumptions(std::vector<Expr>& assumptions) {
-  CheckArgument(assumptions.empty(), assumptions, "assumptions arg must be empty");
+  CVC4::CheckArgument(assumptions.empty(), assumptions, "assumptions arg must be empty");
   vector<CVC4::Expr> v = d_smt->getAssertions();
   assumptions.swap(*reinterpret_cast<vector<Expr>*>(&v));
 }
@@ -2157,7 +2160,7 @@ QueryResult ValidityChecker::tryModelGeneration() {
 }
 
 FormulaValue ValidityChecker::value(const Expr& e) {
-  CheckArgument(e.getType() == d_em->booleanType(), e, "argument must be a formula");
+  CVC4::CheckArgument(e.getType() == d_em->booleanType(), e, "argument must be a formula");
   try {
     return d_smt->getValue(e).getConst<bool>() ? TRUE_VAL : FALSE_VAL;
   } catch(CVC4::Exception& e) {
@@ -2175,7 +2178,7 @@ Expr ValidityChecker::getValue(const Expr& e) {
 }
 
 bool ValidityChecker::inconsistent(std::vector<Expr>& assumptions) {
-  CheckArgument(assumptions.empty(), assumptions, "assumptions vector should be empty on entry");
+  CVC4::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));
@@ -2235,12 +2238,12 @@ void ValidityChecker::pop() {
 }
 
 void ValidityChecker::popto(int stackLevel) {
-  CheckArgument(stackLevel >= 0, stackLevel,
-                "Cannot pop to a negative stack level %d", stackLevel);
-  CheckArgument(unsigned(stackLevel) <= d_stackLevel, stackLevel,
-                "Cannot pop to a stack level higher than the current one!  "
-                "At stack level %u, user requested stack level %d",
-                d_stackLevel, stackLevel);
+  CVC4::CheckArgument(stackLevel >= 0, stackLevel,
+                      "Cannot pop to a negative stack level %d", stackLevel);
+  CVC4::CheckArgument(unsigned(stackLevel) <= d_stackLevel, stackLevel,
+                      "Cannot pop to a stack level higher than the current one!  "
+                      "At stack level %u, user requested stack level %d",
+                      d_stackLevel, stackLevel);
   while(unsigned(stackLevel) < d_stackLevel) {
     pop();
   }
@@ -2259,13 +2262,13 @@ void ValidityChecker::popScope() {
 }
 
 void ValidityChecker::poptoScope(int scopeLevel) {
-  CheckArgument(scopeLevel >= 0, scopeLevel,
-                "Cannot pop to a negative scope level %d", scopeLevel);
-  CheckArgument(unsigned(scopeLevel) <= d_parserContext->getDeclarationLevel(),
-                scopeLevel,
-                "Cannot pop to a scope level higher than the current one!  "
-                "At scope level %u, user requested scope level %d",
-                d_parserContext->getDeclarationLevel(), scopeLevel);
+  CVC4::CheckArgument(scopeLevel >= 0, scopeLevel,
+                      "Cannot pop to a negative scope level %d", scopeLevel);
+  CVC4::CheckArgument(unsigned(scopeLevel) <= d_parserContext->getDeclarationLevel(),
+                      scopeLevel,
+                      "Cannot pop to a scope level higher than the current one!  "
+                      "At scope level %u, user requested scope level %d",
+                      d_parserContext->getDeclarationLevel(), scopeLevel);
   while(unsigned(scopeLevel) < d_parserContext->getDeclarationLevel()) {
     popScope();
   }
diff --git a/src/compat/cvc3_compat.h b/src/compat/cvc3_compat.h
index 31d914b58..911e967ca 100644
--- a/src/compat/cvc3_compat.h
+++ b/src/compat/cvc3_compat.h
@@ -68,16 +68,6 @@
 #include <map>
 #include <utility>
 
-// some #defines that CVC3 exported to userspace :(
-#ifdef CVC4_DEBUG
-#  define DebugAssert(cond, str) Assert((cond), "CVC3-style assertion failed: %s", std::string(str).c_str());
-#  define IF_DEBUG(x) x
-#else
-#  define DebugAssert(...)
-#  define IF_DEBUG(x)
-#endif
-#define FatalAssert(cond, str) AlwaysAssert((cond), "CVC3-style assertion failed: %s", std::string(str).c_str());
-
 //class CInterface;
 
 namespace CVC3 {