From: Tim King <taking@google.com>
Date: Thu, 24 Dec 2015 10:38:43 +0000 (-0500)
Subject: Miscellaneous fixes
X-Git-Tag: cvc5-1.0.0~6129
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a39ad6584c1d61e22e72b53c3838f4f675ed2e19;p=cvc5.git

Miscellaneous fixes
- Splitting the two instances of CheckArgument. The template version is now always defined in base/exception.h and is available in a cvc4_public header. This version has lost its variadic version (due to swig not supporting va_list's). The CPP macro version has been renamed PrettyCheckArgument. (Taking suggestions for a better name.) This is now only defined in base/cvc4_assert.h. Only use this in cvc4_private headers and in .cpp files that can use cvc4_private headers. To use a variadic version of CheckArguments, outside of this scope, you need to duplicate this macro locally. See cvc3_compat.cpp for an example.
- Making fitsSignedInt() and fitsUnsignedInt() work more robustly for CLN on 32 bit systems.
- Refactoring ArrayStoreAll to avoid potential problems with circular header inclusions.
- Changing some headers to use iosfwd when possible.
---

diff --git a/src/base/cvc4_assert.h b/src/base/cvc4_assert.h
index 6dca5c81d..6b47de8cc 100644
--- a/src/base/cvc4_assert.h
+++ b/src/base/cvc4_assert.h
@@ -282,11 +282,15 @@ void debugAssertionFailed(const AssertionException& thisException, const char* l
 #define InternalError(msg...) \
   throw ::CVC4::InternalErrorException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg)
 #define IllegalArgument(arg, msg...) \
-  throw ::CVC4::IllegalArgumentException("", #arg, __PRETTY_FUNCTION__, ## msg)
-#define CheckArgument(cond, arg, msg...)         \
+  throw ::CVC4::IllegalArgumentException("", #arg, __PRETTY_FUNCTION__, \
+                                         ::CVC4::IllegalArgumentException::formatVariadic(msg).c_str());
+// This cannot use check argument directly as this forces
+// CheckArgument to use a va_list. This is unsupported in Swig.
+#define PrettyCheckArgument(cond, arg, msg...)         \
   do { \
     if(__builtin_expect( ( ! (cond) ), false )) { \
-      throw ::CVC4::IllegalArgumentException(#cond, #arg, __PRETTY_FUNCTION__, ## msg); \
+      throw ::CVC4::IllegalArgumentException(#cond, #arg, __PRETTY_FUNCTION__, \
+                                             ::CVC4::IllegalArgumentException::formatVariadic(msg).c_str()); \
     } \
   } while(0)
 #define AlwaysAssertArgument(cond, arg, msg...)  \
diff --git a/src/base/exception.cpp b/src/base/exception.cpp
index d8eee50bc..87bdfcfa5 100644
--- a/src/base/exception.cpp
+++ b/src/base/exception.cpp
@@ -15,6 +15,7 @@
  **/
 
 #include "base/exception.h"
+
 #include <string>
 #include <cstdio>
 #include <cstdlib>
@@ -24,12 +25,58 @@
 
 using namespace std;
 
-#warning "TODO: Remove the second definition of CheckArgument and DebugCheckArgument."
-
 namespace CVC4 {
+
+char* IllegalArgumentException::s_header = "Illegal argument detected";
+
+std::string IllegalArgumentException::formatVariadic() {
+  return std::string();
+}
+
+std::string IllegalArgumentException::formatVariadic(const char* format, ...) {
+  va_list args;
+  va_start(args, format);
+
+  int n = 512;
+  char* buf = NULL;
+
+  for (int i = 0; i < 2; ++i){
+    Assert(n > 0);
+    if(buf != NULL){
+      delete [] buf;
+    }
+    buf = new char[n];
+
+    va_list args_copy;
+    va_copy(args_copy, args);
+    int size = vsnprintf(buf, n, format, args);
+    va_end(args_copy);
+
+    if(size >= n){
+      buf[n-1] = '\0';
+      n = size + 1;
+    } else {
+      break;
+    }
+  }
+  // buf is not NULL is an invariant.
+  // buf is also 0 terminated.
+  Assert(buf != NULL);
+  std::string result(buf);
+  delete [] buf;
+  va_end(args);
+  return result;
+}
+
+std::string IllegalArgumentException::format_extra(const char* condStr, const char* argDesc){
+  return ( std::string("`") + argDesc + "' is a bad argument"
+           + (*condStr == '\0' ? std::string() :
+              ( std::string("; expected ") +
+                condStr + " to hold" )) );
+}
+
 void IllegalArgumentException::construct(const char* header, const char* extra,
-                                         const char* function, const char* fmt,
-                                         va_list args) {
+                                         const char* function, const char* tail) {
   // try building the exception msg with a smallish buffer first,
   // then with a larger one if sprintf tells us to.
   int n = 512;
@@ -40,25 +87,17 @@ void IllegalArgumentException::construct(const char* header, const char* extra,
 
     int size;
     if(extra == NULL) {
-      size = snprintf(buf, n, "%s\n%s\n",
-                      header, function);
+      size = snprintf(buf, n, "%s\n%s\n%s",
+                      header, function, tail);
     } else {
-      size = snprintf(buf, n, "%s\n%s\n\n  %s\n",
-                      header, function, extra);
+      size = snprintf(buf, n, "%s\n%s\n\n  %s\n%s",
+                      header, function, extra, tail);
     }
 
     if(size < n) {
-      va_list args_copy;
-      va_copy(args_copy, args);
-      size += vsnprintf(buf + size, n - size, fmt, args_copy);
-      va_end(args_copy);
-
-      if(size < n) {
-        break;
-      }
-    }
-
-    if(size >= n) {
+      break;
+    } else {
+      // size >= n
       // try again with a buffer that's large enough
       n = size + 1;
       delete [] buf;
diff --git a/src/base/exception.h b/src/base/exception.h
index 78bb160cc..84872b9b1 100644
--- a/src/base/exception.h
+++ b/src/base/exception.h
@@ -19,13 +19,13 @@
 #ifndef __CVC4__EXCEPTION_H
 #define __CVC4__EXCEPTION_H
 
-#include <iostream>
-#include <string>
+#include <cstdarg>
+#include <cstdlib>
+#include <exception>
+#include <iosfwd>
 #include <sstream>
 #include <stdexcept>
-#include <exception>
-#include <cstdlib>
-#include <cstdarg>
+#include <string>
 
 namespace CVC4 {
 
@@ -81,44 +81,37 @@ protected:
   IllegalArgumentException() : Exception() {}
 
   void construct(const char* header, const char* extra,
-                 const char* function, const char* fmt, ...) {
-    va_list args;
-    va_start(args, fmt);
-    construct(header, extra, function, fmt, args);
-    va_end(args);
-  }
-
-  void construct(const char* header, const char* extra,
-                 const char* function, const char* fmt, va_list args);
+                 const char* function, const char* tail);
 
   void construct(const char* header, const char* extra,
                  const char* function);
 
+  static std::string format_extra(const char* condStr, const char* argDesc);
+
+  static char* s_header;
+
 public:
+
   IllegalArgumentException(const char* condStr, const char* argDesc,
-                           const char* function, const char* fmt, ...) :
+                           const char* function, const char* tail) :
     Exception() {
-    va_list args;
-    va_start(args, fmt);
-    construct("Illegal argument detected",
-              ( std::string("`") + argDesc + "' is a bad argument"
-                + (*condStr == '\0' ? std::string() :
-                    ( std::string("; expected ") +
-                        condStr + " to hold" )) ).c_str(),
-              function, fmt, args);
-    va_end(args);
+    construct(s_header, format_extra(condStr, argDesc).c_str(), function, tail);
   }
 
   IllegalArgumentException(const char* condStr, const char* argDesc,
                            const char* function) :
     Exception() {
-    construct("Illegal argument detected",
-              ( std::string("`") + argDesc + "' is a bad argument"
-                + (*condStr == '\0' ? std::string() :
-                    ( std::string("; expected ") +
-                        condStr + " to hold" )) ).c_str(),
-              function);
+    construct(s_header, format_extra(condStr, argDesc).c_str(), function);
   }
+
+  /**
+   * This is a convenience function for building usages that are variadic.
+   *
+   * Having IllegalArgumentException itself be variadic is problematic for
+   * making sure calls to IllegalArgumentException clean up memory.
+   */
+  static std::string formatVariadic();
+  static std::string formatVariadic(const char* format, ...);
 };/* class IllegalArgumentException */
 
 inline std::ostream& operator<<(std::ostream& os, const Exception& e) throw() CVC4_PUBLIC;
@@ -127,43 +120,22 @@ inline std::ostream& operator<<(std::ostream& os, const Exception& e) throw() {
   return os;
 }
 
-}/* CVC4 namespace */
-
-#if (defined(__BUILDING_CVC4LIB) || defined(__BUILDING_CVC4LIB_UNIT_TEST)) && !defined(__BUILDING_STATISTICS_FOR_EXPORT)
-#  include "base/cvc4_assert.h"
-#endif /* (__BUILDING_CVC4LIB || __BUILDING_CVC4LIB_UNIT_TEST) && !__BUILDING_STATISTICS_FOR_EXPORT */
-
-namespace CVC4 {
-
-#ifndef CheckArgument
-template <class T> inline void CheckArgument(bool cond, const T& arg, const char* fmt, ...) CVC4_PUBLIC;
-template <class T> inline void CheckArgument(bool cond, const T& arg, const char* fmt, ...) {
+template <class T> inline void CheckArgument(bool cond, const T& arg,
+                                             const char* tail) CVC4_PUBLIC;
+template <class T> inline void CheckArgument(bool cond, const T& arg,
+                                             const char* tail) {
   if(__builtin_expect( ( !cond ), false )) { \
     throw ::CVC4::IllegalArgumentException("", "", ""); \
   } \
 }
-template <class T> inline void CheckArgument(bool cond, const T& arg) CVC4_PUBLIC;
+template <class T> inline void CheckArgument(bool cond, const T& arg)
+  CVC4_PUBLIC;
 template <class T> inline void CheckArgument(bool cond, const T& arg) {
   if(__builtin_expect( ( !cond ), false )) { \
     throw ::CVC4::IllegalArgumentException("", "", ""); \
   } \
 }
-#endif /* CheckArgument */
 
-#ifndef DebugCheckArgument
-template <class T> inline void DebugCheckArgument(bool cond, const T& arg, const char* fmt, ...) CVC4_PUBLIC;
-template <class T> inline void DebugCheckArgument(bool cond, const T& arg, const char* fmt, ...) {
-  if(__builtin_expect( ( !cond ), false )) { \
-    throw ::CVC4::IllegalArgumentException("", "", ""); \
-  } \
-}
-template <class T> inline void DebugCheckArgument(bool cond, const T& arg) CVC4_PUBLIC;
-template <class T> inline void DebugCheckArgument(bool cond, const T& arg) {
-  if(__builtin_expect( ( !cond ), false )) { \
-    throw ::CVC4::IllegalArgumentException("", "", ""); \
-  } \
-}
-#endif /* DebugCheckArgument */
 
 }/* CVC4 namespace */
 
diff --git a/src/bindings/java_stream_adapters.h b/src/bindings/java_stream_adapters.h
index b4a311ad0..c198b95aa 100644
--- a/src/bindings/java_stream_adapters.h
+++ b/src/bindings/java_stream_adapters.h
@@ -33,7 +33,7 @@
 #include <sstream>
 #include <set>
 #include <cassert>
-#include <iostream>
+#include <iosfwd>
 #include <string>
 #include <jni.h>
 
diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp
index d44bae7ee..3fa790f3e 100644
--- a/src/compat/cvc3_compat.cpp
+++ b/src/compat/cvc3_compat.cpp
@@ -18,11 +18,12 @@
 
 #include <algorithm>
 #include <cassert>
-#include <iostream>
+#include <iosfwd>
 #include <iterator>
 #include <sstream>
 #include <string>
 
+#include "base/exception.h"
 #include "base/output.h"
 #include "expr/kind.h"
 #include "expr/predicate.h"
@@ -43,6 +44,16 @@
 
 using namespace std;
 
+// Matches base/cvc4_assert.h's PrettyCheckArgument.
+// base/cvc4_assert.h cannot be directly included.
+#define CompatCheckArgument(cond, arg, msg...)         \
+  do { \
+    if(__builtin_expect( ( ! (cond) ), false )) { \
+      throw ::CVC4::IllegalArgumentException(#cond, #arg, __PRETTY_FUNCTION__, \
+                                             ::CVC4::IllegalArgumentException::formatVariadic(msg).c_str()); \
+    } \
+  } while(0)
+
 #define Unimplemented(str) throw Exception(str)
 
 namespace CVC3 {
@@ -474,12 +485,12 @@ std::string Expr::getUid() const {
 }
 
 std::string Expr::getString() const {
-  CVC4::CheckArgument(getKind() == CVC4::kind::CONST_STRING, *this, "CVC3::Expr::getString(): not a string Expr: `%s'", toString().c_str());
+  CompatCheckArgument(getKind() == CVC4::kind::CONST_STRING, *this, "CVC3::Expr::getString(): not a string Expr: `%s'", toString().c_str());
   return getConst<CVC4::String>().toString();
 }
 
 std::vector<Expr> Expr::getVars() const {
-  CVC4::CheckArgument(isClosure(), *this, "CVC3::Expr::getVars(): not a closure Expr: `%s'", toString().c_str());
+  CompatCheckArgument(isClosure(), *this, "CVC3::Expr::getVars(): not a closure Expr: `%s'", toString().c_str());
   const vector<CVC4::Expr>& kids = (*this)[0].getChildren();
   vector<Expr> v;
   for(vector<CVC4::Expr>::const_iterator i = kids.begin(); i != kids.end(); ++i) {
@@ -497,7 +508,7 @@ int Expr::getBoundIndex() const {
 }
 
 Expr Expr::getBody() const {
-  CVC4::CheckArgument(isClosure(), *this, "CVC3::Expr::getBody(): not a closure Expr: `%s'", toString().c_str());
+  CompatCheckArgument(isClosure(), *this, "CVC3::Expr::getBody(): not a closure Expr: `%s'", toString().c_str());
   return (*this)[1];
 }
 
@@ -546,7 +557,7 @@ bool Expr::isSkolem() const {
 }
 
 const Rational& Expr::getRational() const {
-  CVC4::CheckArgument(isRational(), *this, "CVC3::Expr::getRational(): not a rational Expr: `%s'", toString().c_str());
+  CompatCheckArgument(isRational(), *this, "CVC3::Expr::getRational(): not a rational Expr: `%s'", toString().c_str());
   return getConst<CVC4::Rational>();
 }
 
@@ -573,7 +584,8 @@ Expr Expr::getExpr() const {
 }
 
 std::vector< std::vector<Expr> > Expr::getTriggers() const {
-  CVC4::CheckArgument(isClosure(), *this, "getTriggers() called on non-closure expr");
+  CompatCheckArgument(isClosure(), *this,
+                      "getTriggers() called on non-closure expr");
   if(getNumChildren() < 3) {
     // no triggers for this quantifier
     return vector< vector<Expr> >();
@@ -756,37 +768,37 @@ CLFlag& CLFlag::operator=(const CLFlag& f) {
 }
 
 CLFlag& CLFlag::operator=(bool b) {
-  CVC4::CheckArgument(d_tp == CLFLAG_BOOL, this);
+  CompatCheckArgument(d_tp == CLFLAG_BOOL, this);
   d_data.b = b;
   return *this;
 }
 
 CLFlag& CLFlag::operator=(int i) {
-  CVC4::CheckArgument(d_tp == CLFLAG_INT, this);
+  CompatCheckArgument(d_tp == CLFLAG_INT, this);
   d_data.i = i;
   return *this;
 }
 
 CLFlag& CLFlag::operator=(const std::string& s) {
-  CVC4::CheckArgument(d_tp == CLFLAG_STRING, this);
+  CompatCheckArgument(d_tp == CLFLAG_STRING, this);
   *d_data.s = s;
   return *this;
 }
 
 CLFlag& CLFlag::operator=(const char* s) {
-  CVC4::CheckArgument(d_tp == CLFLAG_STRING, this);
+  CompatCheckArgument(d_tp == CLFLAG_STRING, this);
   *d_data.s = s;
   return *this;
 }
 
 CLFlag& CLFlag::operator=(const std::pair<string, bool>& p) {
-  CVC4::CheckArgument(d_tp == CLFLAG_STRVEC, this);
+  CompatCheckArgument(d_tp == CLFLAG_STRVEC, this);
   d_data.sv->push_back(p);
   return *this;
 }
 
 CLFlag& CLFlag::operator=(const std::vector<std::pair<string, bool> >& sv) {
-  CVC4::CheckArgument(d_tp == CLFLAG_STRVEC, this);
+  CompatCheckArgument(d_tp == CLFLAG_STRVEC, this);
   *d_data.sv = sv;
   return *this;
 }
@@ -804,22 +816,22 @@ bool CLFlag::display() const {
 }
 
 const bool& CLFlag::getBool() const {
-  CVC4::CheckArgument(d_tp == CLFLAG_BOOL, this);
+  CompatCheckArgument(d_tp == CLFLAG_BOOL, this);
   return d_data.b;
 }
 
 const int& CLFlag::getInt() const {
-  CVC4::CheckArgument(d_tp == CLFLAG_INT, this);
+  CompatCheckArgument(d_tp == CLFLAG_INT, this);
   return d_data.i;
 }
 
 const std::string& CLFlag::getString() const {
-  CVC4::CheckArgument(d_tp == CLFLAG_STRING, this);
+  CompatCheckArgument(d_tp == CLFLAG_STRING, this);
   return *d_data.s;
 }
 
 const std::vector<std::pair<string, bool> >& CLFlag::getStrVec() const {
-  CVC4::CheckArgument(d_tp == CLFLAG_STRVEC, this);
+  CompatCheckArgument(d_tp == CLFLAG_STRVEC, this);
   return *d_data.sv;
 }
 
@@ -842,7 +854,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);
-  CVC4::CheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported.");
+  CompatCheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported.");
   return (*i).second;
 }
 
@@ -852,8 +864,8 @@ 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);
-  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,
+  CompatCheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported.");
+  CompatCheckArgument((*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(),
@@ -863,38 +875,38 @@ void CLFlags::setFlag(const std::string& name, const CLFlag& f) {
 
 void CLFlags::setFlag(const std::string& name, bool b) {
   FlagMap::iterator i = d_map.find(name);
-  CVC4::CheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported.");
+  CompatCheckArgument(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);
-  CVC4::CheckArgument(it != d_map.end(), name, "No command-line flag by that name, or not supported.");
+  CompatCheckArgument(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);
-  CVC4::CheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported.");
+  CompatCheckArgument(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);
-  CVC4::CheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported.");
+  CompatCheckArgument(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);
-  CVC4::CheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported.");
+  CompatCheckArgument(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);
-  CVC4::CheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported.");
+  CompatCheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported.");
   (*i).second = sv;
 }
 
@@ -1233,8 +1245,8 @@ Type ValidityChecker::intType() {
 Type ValidityChecker::subrangeType(const Expr& l, const Expr& r) {
   bool noLowerBound = l.getType().isString() && l.getConst<CVC4::String>() == "_NEGINF";
   bool noUpperBound = r.getType().isString() && r.getConst<CVC4::String>() == "_POSINF";
-  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);
+  CompatCheckArgument(noLowerBound || (l.getKind() == CVC4::kind::CONST_RATIONAL && l.getConst<Rational>().isIntegral()), l);
+  CompatCheckArgument(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));
@@ -1298,7 +1310,7 @@ Type ValidityChecker::recordType(const std::string& field0, const Type& type0,
 
 Type ValidityChecker::recordType(const std::vector<std::string>& fields,
                                  const std::vector<Type>& types) {
-  CVC4::CheckArgument(fields.size() == types.size() && fields.size() > 0,
+  CompatCheckArgument(fields.size() == types.size() && fields.size() > 0,
                       "invalid vector length(s) in recordType()");
   std::vector< std::pair<std::string, CVC4::Type> > fieldSpecs;
   for(unsigned i = 0; i < fields.size(); ++i) {
@@ -1311,7 +1323,9 @@ Type ValidityChecker::dataType(const std::string& name,
                                const std::string& constructor,
                                const std::vector<std::string>& selectors,
                                const std::vector<Expr>& types) {
-  CVC4::CheckArgument(selectors.size() == types.size(), types, "expected selectors and types vectors to be of equal length");
+  CompatCheckArgument(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;
@@ -1325,8 +1339,12 @@ 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) {
-  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");
+  CompatCheckArgument(constructors.size() == selectors.size(), selectors,
+                      "Expected constructors and selectors vectors to be of "
+                      "equal length.");
+  CompatCheckArgument(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;
@@ -1347,22 +1365,36 @@ void ValidityChecker::dataType(const std::vector<std::string>& names,
                                const std::vector<std::vector<std::vector<Expr> > >& types,
                                std::vector<Type>& returnTypes) {
 
-  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");
+  CompatCheckArgument(names.size() == constructors.size(), constructors,
+                      "Expected names and constructors vectors to be of equal "
+                      "length.");
+  CompatCheckArgument(names.size() == selectors.size(), selectors,
+                      "Expected names and selectors vectors to be of equal "
+                      "length.");
+  CompatCheckArgument(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], false);
-    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");
+    CompatCheckArgument(constructors[i].size() == selectors[i].size(),
+                        "Expected sub-vectors in constructors and selectors "
+                        "vectors to match in size.");
+    CompatCheckArgument(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]);
-      CVC4::CheckArgument(selectors[i][j].size() == types[i][j].size(), types, "expected sub-vectors in selectors and types vectors to match in size");
+      CompatCheckArgument(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<CVC4::String>().toString()));
+          CVC4::DatatypeUnresolvedType unresolvedName = 
+            types[i][j][k].getConst<CVC4::String>().toString();
+          ctor.addArg(selectors[i][j][k], unresolvedName);
         } else {
           ctor.addArg(selectors[i][j][k], exprToType(types[i][j][k]));
         }
@@ -1388,10 +1420,17 @@ 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.
-      CVC4::CheckArgument(d_constructors.find((*j).getName()) == d_constructors.end(), constructors, "cannot have two constructors with the same name in a ValidityChecker");
+      CompatCheckArgument(
+          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) {
-        CVC4::CheckArgument(d_selectors.find((*k).getName()) == d_selectors.end(), selectors, "cannot have two selectors with the same name in a ValidityChecker");
+        CompatCheckArgument(
+            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());
       }
     }
@@ -1407,7 +1446,8 @@ Type ValidityChecker::arrayType(const Type& typeIndex, const Type& typeData) {
 }
 
 Type ValidityChecker::bitvecType(int n) {
-  CVC4::CheckArgument(n >= 0, n, "cannot construct a bitvector type of negative size");
+  CompatCheckArgument(n >= 0, n,
+                      "Cannot construct a bitvector type of negative size.");
   return d_em->mkBitVectorType(n);
 }
 
@@ -1444,7 +1484,7 @@ Expr ValidityChecker::varExpr(const std::string& name, const Type& type) {
 
 Expr ValidityChecker::varExpr(const std::string& name, const Type& type,
                               const Expr& def) {
-  CVC4::CheckArgument(def.getType() == type, def, "expected types to match");
+  CompatCheckArgument(def.getType() == type, def, "expected types to match");
   d_parserContext->defineVar(name, def);
   return def;
 }
@@ -1595,7 +1635,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
-  CVC4::CheckArgument(children.size() > 0, children);
+  CompatCheckArgument(children.size() > 0, children);
   return (children.size() == 1) ? children[0] : Expr(d_em->mkExpr(CVC4::kind::AND, *reinterpret_cast<const vector<CVC4::Expr>*>(&children)));
 }
 
@@ -1605,7 +1645,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
-  CVC4::CheckArgument(children.size() > 0, children);
+  CompatCheckArgument(children.size() > 0, children);
   return (children.size() == 1) ? children[0] : Expr(d_em->mkExpr(CVC4::kind::OR, *reinterpret_cast<const vector<CVC4::Expr>*>(&children)));
 }
 
@@ -1627,7 +1667,7 @@ Expr ValidityChecker::iteExpr(const Expr& ifpart, const Expr& thenpart,
 }
 
 Expr ValidityChecker::distinctExpr(const std::vector<Expr>& children) {
-  CVC4::CheckArgument(children.size() > 1, children, "it makes no sense to create a `distinct' expression with only one child");
+  CompatCheckArgument(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);
@@ -1639,7 +1679,7 @@ Op ValidityChecker::createOp(const std::string& name, const Type& type) {
 
 Op ValidityChecker::createOp(const std::string& name, const Type& type,
                              const Expr& def) {
-  CVC4::CheckArgument(def.getType() == type, type,
+  CompatCheckArgument(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());
@@ -1689,7 +1729,7 @@ Expr ValidityChecker::ratExpr(const std::string& n, int base) {
   if(n.find(".") == string::npos) {
     return d_em->mkConst(Rational(n, base));
   } else {
-    CVC4::CheckArgument(base == 10, base, "unsupported base for decimal parsing");
+    CompatCheckArgument(base == 10, base, "unsupported base for decimal parsing");
     return d_em->mkConst(Rational::fromDecimal(n));
   }
 }
@@ -1704,7 +1744,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
-  CVC4::CheckArgument(children.size() > 0, children);
+  CompatCheckArgument(children.size() > 0, children);
   return (children.size() == 1) ? children[0] : Expr(d_em->mkExpr(CVC4::kind::PLUS, *reinterpret_cast<const vector<CVC4::Expr>*>(&children)));
 }
 
@@ -1806,10 +1846,11 @@ Expr ValidityChecker::newBVConstExpr(const std::vector<bool>& bits) {
 Expr ValidityChecker::newBVConstExpr(const Rational& r, int len) {
   // implementation based on CVC3's TheoryBitvector::newBVConstExpr()
 
-  CVC4::CheckArgument(r.getDenominator() == 1, r, "ValidityChecker::newBVConstExpr: "
-                "not an integer: `%s'", r.toString().c_str());
-  CVC4::CheckArgument(len > 0, len, "ValidityChecker::newBVConstExpr: "
-                "len = %d", len);
+  CompatCheckArgument(r.getDenominator() == 1, r,
+                      "ValidityChecker::newBVConstExpr: "
+                      "not an integer: `%s'", r.toString().c_str());
+  CompatCheckArgument(len > 0, len, "ValidityChecker::newBVConstExpr: "
+                      "len = %d", len);
 
   string s(r.toString(2));
   size_t strsize = s.size();
@@ -1831,8 +1872,8 @@ Expr ValidityChecker::newBVConstExpr(const Rational& r, int len) {
 }
 
 Expr ValidityChecker::newConcatExpr(const Expr& t1, const Expr& t2) {
-  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());
+  CompatCheckArgument(t1.getType().isBitVector(), t1, "can only concat a bitvector, not a `%s'", t1.getType().toString().c_str());
+  CompatCheckArgument(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);
 }
 
@@ -1843,29 +1884,43 @@ Expr ValidityChecker::newConcatExpr(const std::vector<Expr>& kids) {
 }
 
 Expr ValidityChecker::newBVExtractExpr(const Expr& e, int hi, int 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);
+  CompatCheckArgument(e.getType().isBitVector(), e,
+                      "can only bvextract from a bitvector, not a `%s'",
+                      e.getType().toString().c_str());
+  CompatCheckArgument(hi >= low, hi,
+                      "extraction [%d:%d] is bad; possibly inverted?", hi, low);
+  CompatCheckArgument(low >= 0, low,
+                      "extraction [%d:%d] is bad (negative)", hi, low);
+  CompatCheckArgument(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);
+                      d_em->mkConst(CVC4::BitVectorExtract(hi, low)), e);
 }
 
 Expr ValidityChecker::newBVNegExpr(const Expr& t1) {
   // CVC3's BVNEG => SMT-LIBv2 bvnot
-  CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only bvneg a bitvector, not a `%s'", t1.getType().toString().c_str());
+  CompatCheckArgument(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) {
-  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());
+  CompatCheckArgument(t1.getType().isBitVector(), t1,
+                      "can only bvand a bitvector, not a `%s'",
+                      t1.getType().toString().c_str());
+  CompatCheckArgument(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
-  CVC4::CheckArgument(kids.size() > 1, kids, "BITVECTOR_AND must have at least 2 children");
+  CompatCheckArgument(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()) {
@@ -1875,14 +1930,19 @@ Expr ValidityChecker::newBVAndExpr(const std::vector<Expr>& kids) {
 }
 
 Expr ValidityChecker::newBVOrExpr(const Expr& t1, const Expr& t2) {
-  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());
+  CompatCheckArgument(t1.getType().isBitVector(), t1,
+                      "can only bvor a bitvector, not a `%s'",
+                      t1.getType().toString().c_str());
+  CompatCheckArgument(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
-  CVC4::CheckArgument(kids.size() > 1, kids, "BITVECTOR_OR must have at least 2 children");
+  CompatCheckArgument(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()) {
@@ -1892,14 +1952,19 @@ Expr ValidityChecker::newBVOrExpr(const std::vector<Expr>& kids) {
 }
 
 Expr ValidityChecker::newBVXorExpr(const Expr& t1, const Expr& t2) {
-  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());
+  CompatCheckArgument(t1.getType().isBitVector(), t1,
+                      "can only bvxor a bitvector, not a `%s'",
+                      t1.getType().toString().c_str());
+  CompatCheckArgument(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
-  CVC4::CheckArgument(kids.size() > 1, kids, "BITVECTOR_XOR must have at least 2 children");
+  CompatCheckArgument(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()) {
@@ -1909,14 +1974,19 @@ Expr ValidityChecker::newBVXorExpr(const std::vector<Expr>& kids) {
 }
 
 Expr ValidityChecker::newBVXnorExpr(const Expr& t1, const Expr& t2) {
-  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());
+  CompatCheckArgument(t1.getType().isBitVector(), t1,
+                      "can only bvxnor a bitvector, not a `%s'",
+                      t1.getType().toString().c_str());
+  CompatCheckArgument(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
-  CVC4::CheckArgument(kids.size() > 1, kids, "BITVECTOR_XNOR must have at least 2 children");
+  CompatCheckArgument(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()) {
@@ -1926,73 +1996,81 @@ Expr ValidityChecker::newBVXnorExpr(const std::vector<Expr>& kids) {
 }
 
 Expr ValidityChecker::newBVNandExpr(const Expr& t1, const Expr& t2) {
-  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());
+  CompatCheckArgument(t1.getType().isBitVector(), t1,
+                      "can only bvnand a bitvector, not a `%s'",
+                      t1.getType().toString().c_str());
+  CompatCheckArgument(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) {
-  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());
+  CompatCheckArgument(t1.getType().isBitVector(), t1,
+                      "can only bvnor a bitvector, not a `%s'",
+                      t1.getType().toString().c_str());
+  CompatCheckArgument(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) {
-  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());
+  CompatCheckArgument(t1.getType().isBitVector(), t1, "can only bvcomp a bitvector, not a `%s'", t1.getType().toString().c_str());
+  CompatCheckArgument(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) {
-  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());
+  CompatCheckArgument(t1.getType().isBitVector(), t1, "can only bvlt a bitvector, not a `%s'", t1.getType().toString().c_str());
+  CompatCheckArgument(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) {
-  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());
+  CompatCheckArgument(t1.getType().isBitVector(), t1, "can only bvle a bitvector, not a `%s'", t1.getType().toString().c_str());
+  CompatCheckArgument(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) {
-  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());
+  CompatCheckArgument(t1.getType().isBitVector(), t1, "can only bvslt a bitvector, not a `%s'", t1.getType().toString().c_str());
+  CompatCheckArgument(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) {
-  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());
+  CompatCheckArgument(t1.getType().isBitVector(), t1, "can only bvsle a bitvector, not a `%s'", t1.getType().toString().c_str());
+  CompatCheckArgument(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) {
-  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());
+  CompatCheckArgument(t1.getType().isBitVector(), t1, "can only sx a bitvector, not a `%s'", t1.getType().toString().c_str());
+  CompatCheckArgument(len >= 0, len, "must sx by a positive integer");
+  CompatCheckArgument(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
-  CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only bvuminus a bitvector, not a `%s'", t1.getType().toString().c_str());
+  CompatCheckArgument(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) {
-  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());
+  CompatCheckArgument(t1.getType().isBitVector(), t1, "can only bvsub a bitvector, not a `%s'", t1.getType().toString().c_str());
+  CompatCheckArgument(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) {
-  CVC4::CheckArgument(len >= 0, len,
+  CompatCheckArgument(len >= 0, len,
                 "padding length must be a non-negative integer, not %d", len);
-  CVC4::CheckArgument(e.getType().isBitVector(), e,
+  CompatCheckArgument(e.getType().isBitVector(), e,
                 "input to bitvector operation must be a bitvector");
 
   unsigned size = CVC4::BitVectorType(e.getType()).getSize();
@@ -2011,89 +2089,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
-  CVC4::CheckArgument(kids.size() > 1, kids, "BITVECTOR_PLUS must have at least 2 children");
+  CompatCheckArgument(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();
-  CVC4::CheckArgument(unsigned(numbits) == size, numbits,
+  CompatCheckArgument(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) {
-  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());
+  CompatCheckArgument(t1.getType().isBitVector(), t1, "can only bvplus a bitvector, not a `%s'", t1.getType().toString().c_str());
+  CompatCheckArgument(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();
-  CVC4::CheckArgument(unsigned(numbits) == size, numbits,
+  CompatCheckArgument(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) {
-  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());
+  CompatCheckArgument(t1.getType().isBitVector(), t1, "can only bvmult a bitvector, not a `%s'", t1.getType().toString().c_str());
+  CompatCheckArgument(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();
-  CVC4::CheckArgument(unsigned(numbits) == size, numbits,
+  CompatCheckArgument(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) {
-  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());
+  CompatCheckArgument(t1.getType().isBitVector(), t1, "can only bvudiv a bitvector, not a `%s'", t1.getType().toString().c_str());
+  CompatCheckArgument(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) {
-  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());
+  CompatCheckArgument(t1.getType().isBitVector(), t1, "can only bvurem a bitvector, not a `%s'", t1.getType().toString().c_str());
+  CompatCheckArgument(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) {
-  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());
+  CompatCheckArgument(t1.getType().isBitVector(), t1, "can only bvsdiv a bitvector, not a `%s'", t1.getType().toString().c_str());
+  CompatCheckArgument(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) {
-  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());
+  CompatCheckArgument(t1.getType().isBitVector(), t1, "can only bvsrem a bitvector, not a `%s'", t1.getType().toString().c_str());
+  CompatCheckArgument(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) {
-  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());
+  CompatCheckArgument(t1.getType().isBitVector(), t1, "can only bvsmod a bitvector, not a `%s'", t1.getType().toString().c_str());
+  CompatCheckArgument(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) {
-  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);
+  CompatCheckArgument(t1.getType().isBitVector(), t1, "can only left-shift a bitvector, not a `%s'", t1.getType().toString().c_str());
+  CompatCheckArgument(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) {
-  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);
+  CompatCheckArgument(t1.getType().isBitVector(), t1, "can only right-shift a bitvector, not a `%s'", t1.getType().toString().c_str());
+  CompatCheckArgument(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) {
-  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);
+  CompatCheckArgument(t1.getType().isBitVector(), t1, "can only right-shift a bitvector, not a `%s'", t1.getType().toString().c_str());
+  CompatCheckArgument(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.
@@ -2101,20 +2179,20 @@ Expr ValidityChecker::newFixedRightShiftExpr(const Expr& t1, int r) {
 }
 
 Expr ValidityChecker::newBVSHL(const Expr& t1, const Expr& t2) {
-  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());
+  CompatCheckArgument(t1.getType().isBitVector(), t1, "can only right-shift a bitvector, not a `%s'", t1.getType().toString().c_str());
+  CompatCheckArgument(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) {
-  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());
+  CompatCheckArgument(t1.getType().isBitVector(), t1, "can only right-shift a bitvector, not a `%s'", t1.getType().toString().c_str());
+  CompatCheckArgument(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) {
-  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());
+  CompatCheckArgument(t1.getType().isBitVector(), t1, "can only right-shift a bitvector, not a `%s'", t1.getType().toString().c_str());
+  CompatCheckArgument(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);
 }
 
@@ -2129,30 +2207,30 @@ Expr ValidityChecker::tupleExpr(const std::vector<Expr>& exprs) {
 }
 
 Expr ValidityChecker::tupleSelectExpr(const Expr& tuple, int index) {
-  CVC4::CheckArgument(index >= 0 && index < tuple.getNumChildren(),
+  CompatCheckArgument(index >= 0 && index < tuple.getNumChildren(),
                       "invalid index in tuple select");
   return d_em->mkExpr(d_em->mkConst(CVC4::TupleSelect(index)), tuple);
 }
 
 Expr ValidityChecker::tupleUpdateExpr(const Expr& tuple, int index,
                                       const Expr& newValue) {
-  CVC4::CheckArgument(index >= 0 && index < tuple.getNumChildren(),
+  CompatCheckArgument(index >= 0 && index < tuple.getNumChildren(),
                       "invalid index in tuple update");
   return d_em->mkExpr(d_em->mkConst(CVC4::TupleUpdate(index)), tuple, newValue);
 }
 
 Expr ValidityChecker::datatypeConsExpr(const std::string& constructor, const std::vector<Expr>& args) {
   ConstructorMap::const_iterator i = d_constructors.find(constructor);
-  CVC4::CheckArgument(i != d_constructors.end(), constructor, "no such constructor");
+  CompatCheckArgument(i != d_constructors.end(), constructor, "no such constructor");
   const CVC4::Datatype& dt = *(*i).second;
   const CVC4::DatatypeConstructor& ctor = dt[constructor];
-  CVC4::CheckArgument(ctor.getNumArgs() == args.size(), args, "arity mismatch in constructor application");
+  CompatCheckArgument(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);
-  CVC4::CheckArgument(i != d_selectors.end(), selector, "no such selector");
+  CompatCheckArgument(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];
@@ -2161,7 +2239,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);
-  CVC4::CheckArgument(i != d_constructors.end(), constructor, "no such constructor");
+  CompatCheckArgument(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);
@@ -2314,7 +2392,7 @@ void ValidityChecker::returnFromCheck() {
 }
 
 void ValidityChecker::getUserAssumptions(std::vector<Expr>& assumptions) {
-  CVC4::CheckArgument(assumptions.empty(), assumptions, "assumptions arg must be empty");
+  CompatCheckArgument(assumptions.empty(), assumptions, "assumptions arg must be empty");
   vector<CVC4::Expr> v = d_smt->getAssertions();
   assumptions.swap(*reinterpret_cast<vector<Expr>*>(&v));
 }
@@ -2349,7 +2427,7 @@ QueryResult ValidityChecker::tryModelGeneration() {
 }
 
 FormulaValue ValidityChecker::value(const Expr& e) {
-  CVC4::CheckArgument(e.getType() == d_em->booleanType(), e, "argument must be a formula");
+  CompatCheckArgument(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) {
@@ -2367,7 +2445,7 @@ Expr ValidityChecker::getValue(const Expr& e) {
 }
 
 bool ValidityChecker::inconsistent(std::vector<Expr>& assumptions) {
-  CVC4::CheckArgument(assumptions.empty(), assumptions, "assumptions vector should be empty on entry");
+  CompatCheckArgument(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));
@@ -2427,9 +2505,9 @@ void ValidityChecker::pop() {
 }
 
 void ValidityChecker::popto(int stackLevel) {
-  CVC4::CheckArgument(stackLevel >= 0, stackLevel,
+  CompatCheckArgument(stackLevel >= 0, stackLevel,
                       "Cannot pop to a negative stack level %d", stackLevel);
-  CVC4::CheckArgument(unsigned(stackLevel) <= d_stackLevel, stackLevel,
+  CompatCheckArgument(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);
@@ -2451,9 +2529,9 @@ void ValidityChecker::popScope() {
 }
 
 void ValidityChecker::poptoScope(int scopeLevel) {
-  CVC4::CheckArgument(scopeLevel >= 0, scopeLevel,
+  CompatCheckArgument(scopeLevel >= 0, scopeLevel,
                       "Cannot pop to a negative scope level %d", scopeLevel);
-  CVC4::CheckArgument(unsigned(scopeLevel) <= d_parserContext->scopeLevel(),
+  CompatCheckArgument(unsigned(scopeLevel) <= d_parserContext->scopeLevel(),
                       scopeLevel,
                       "Cannot pop to a scope level higher than the current one!  "
                       "At scope level %u, user requested scope level %d",
diff --git a/src/cvc4.i b/src/cvc4.i
index ad042d398..6ee0c7572 100644
--- a/src/cvc4.i
+++ b/src/cvc4.i
@@ -40,13 +40,13 @@ namespace std {
 namespace CVC4 {}
 using namespace CVC4;
 
-#include <iostream>
-#include <vector>
+#include <cassert>
+#include <ext/hash_map>
+#include <iosfwd>
 #include <set>
 #include <string>
-#include <ext/hash_map>
 #include <typeinfo>
-#include <cassert>
+#include <vector>
 
 #include "base/exception.h"
 #include "base/modal_exception.h"
diff --git a/src/expr/array_store_all.cpp b/src/expr/array_store_all.cpp
index 62c8ec978..d9d0a5f8d 100644
--- a/src/expr/array_store_all.cpp
+++ b/src/expr/array_store_all.cpp
@@ -20,12 +20,85 @@
 
 #include <iostream>
 
+#include "base/cvc4_assert.h"
+#include "expr/expr.h"
+#include "expr/type.h"
+
 using namespace std;
 
 namespace CVC4 {
 
+ArrayStoreAll::ArrayStoreAll(const ArrayStoreAll& other)
+    : d_type(new ArrayType(other.getType()))
+    , d_expr(new Expr(other.getExpr())) {}
+
+ArrayStoreAll::~ArrayStoreAll() throw() {
+  delete d_expr;
+  delete d_type;
+}
+
+ArrayStoreAll& ArrayStoreAll::operator=(const ArrayStoreAll& other){
+  (*d_type) = other.getType();
+  (*d_expr) = other.getExpr();
+}
+
+ArrayStoreAll::ArrayStoreAll(const ArrayType& type, const Expr& expr)
+    throw(IllegalArgumentException)
+    : d_type(new ArrayType(type))
+    , d_expr(new Expr(expr))
+{
+  // this check is stronger than the assertion check in the expr manager that ArrayTypes are actually array types
+  // because this check is done in production builds too
+  PrettyCheckArgument(
+      type.isArray(),
+      type,
+      "array store-all constants can only be created for array types, not `%s'",
+      type.toString().c_str());
+
+  PrettyCheckArgument(
+      expr.getType().isComparableTo(type.getConstituentType()),
+      expr,
+      "expr type `%s' does not match constituent type of array type `%s'",
+      expr.getType().toString().c_str(),
+      type.toString().c_str());
+
+  PrettyCheckArgument(
+      expr.isConst(),
+      expr,
+      "ArrayStoreAll requires a constant expression");
+}
+
+
+const ArrayType& ArrayStoreAll::getType() const throw() {
+  return *d_type;
+}
+
+const Expr& ArrayStoreAll::getExpr() const throw() {
+  return *d_expr;
+}
+
+bool ArrayStoreAll::operator==(const ArrayStoreAll& asa) const throw() {
+  return getType() == asa.getType() && getExpr() == asa.getExpr();
+}
+
+
+bool ArrayStoreAll::operator<(const ArrayStoreAll& asa) const throw() {
+  return (getType() < asa.getType()) ||
+      (getType() == asa.getType() && getExpr() < asa.getExpr());
+}
+
+bool ArrayStoreAll::operator<=(const ArrayStoreAll& asa) const throw() {
+  return (getType() < asa.getType()) ||
+      (getType() == asa.getType() && getExpr() <= asa.getExpr());
+}
+
 std::ostream& operator<<(std::ostream& out, const ArrayStoreAll& asa) {
   return out << "__array_store_all__(" << asa.getType() << ", " << asa.getExpr() << ')';
 }
 
+size_t ArrayStoreAllHashFunction::operator()(const ArrayStoreAll& asa) const {
+  return TypeHashFunction()(asa.getType()) * ExprHashFunction()(asa.getExpr());
+}
+
+
 }/* CVC4 namespace */
diff --git a/src/expr/array_store_all.h b/src/expr/array_store_all.h
index b1d624266..293b785a9 100644
--- a/src/expr/array_store_all.h
+++ b/src/expr/array_store_all.h
@@ -20,61 +20,43 @@
 
 #pragma once
 
+#include <iosfwd>
+
+#include "base/exception.h"
+
 namespace CVC4 {
   // messy; Expr needs ArrayStoreAll (because it's the payload of a
   // CONSTANT-kinded expression), and ArrayStoreAll needs Expr.
-  class CVC4_PUBLIC ArrayStoreAll;
+  class Expr;
+  class ArrayType;
 }/* CVC4 namespace */
 
-#include "expr/expr.h"
-#include "expr/type.h"
-#include <iostream>
 
 namespace CVC4 {
 
 class CVC4_PUBLIC ArrayStoreAll {
-  const ArrayType d_type;
-  const Expr d_expr;
-
 public:
+  ArrayStoreAll(const ArrayStoreAll& other);
 
-  ArrayStoreAll(ArrayType type, Expr expr) throw(IllegalArgumentException) :
-    d_type(type),
-    d_expr(expr) {
+  ArrayStoreAll& operator=(const ArrayStoreAll& other);
 
-    // this check is stronger than the assertion check in the expr manager that ArrayTypes are actually array types
-    // because this check is done in production builds too
-    CheckArgument(type.isArray(), type, "array store-all constants can only be created for array types, not `%s'", type.toString().c_str());
+  ArrayStoreAll(const ArrayType& type, const Expr& expr)
+      throw(IllegalArgumentException);
 
-    CheckArgument(expr.getType().isComparableTo(type.getConstituentType()), expr, "expr type `%s' does not match constituent type of array type `%s'", expr.getType().toString().c_str(), type.toString().c_str());
-    CheckArgument(expr.isConst(), expr, "ArrayStoreAll requires a constant expression");
-  }
+  ~ArrayStoreAll() throw();
 
-  ~ArrayStoreAll() throw() {
-  }
+  const ArrayType& getType() const throw();
 
-  ArrayType getType() const throw() {
-    return d_type;
-  }
-  Expr getExpr() const throw() {
-    return d_expr;
-  }
+  const Expr& getExpr() const throw();
+
+  bool operator==(const ArrayStoreAll& asa) const throw();
 
-  bool operator==(const ArrayStoreAll& asa) const throw() {
-    return d_type == asa.d_type && d_expr == asa.d_expr;
-  }
   bool operator!=(const ArrayStoreAll& asa) const throw() {
     return !(*this == asa);
   }
 
-  bool operator<(const ArrayStoreAll& asa) const throw() {
-    return d_type < asa.d_type ||
-           (d_type == asa.d_type && d_expr < asa.d_expr);
-  }
-  bool operator<=(const ArrayStoreAll& asa) const throw() {
-    return d_type < asa.d_type ||
-           (d_type == asa.d_type && d_expr <= asa.d_expr);
-  }
+  bool operator<(const ArrayStoreAll& asa) const throw();
+  bool operator<=(const ArrayStoreAll& asa) const throw();
   bool operator>(const ArrayStoreAll& asa) const throw() {
     return !(*this <= asa);
   }
@@ -82,6 +64,9 @@ public:
     return !(*this < asa);
   }
 
+private:
+  ArrayType* d_type;
+  Expr* d_expr;
 };/* class ArrayStoreAll */
 
 std::ostream& operator<<(std::ostream& out, const ArrayStoreAll& asa) CVC4_PUBLIC;
@@ -90,9 +75,7 @@ std::ostream& operator<<(std::ostream& out, const ArrayStoreAll& asa) CVC4_PUBLI
  * Hash function for the ArrayStoreAll constants.
  */
 struct CVC4_PUBLIC ArrayStoreAllHashFunction {
-  inline size_t operator()(const ArrayStoreAll& asa) const {
-    return TypeHashFunction()(asa.getType()) * ExprHashFunction()(asa.getExpr());
-  }
+  size_t operator()(const ArrayStoreAll& asa) const;
 };/* struct ArrayStoreAllHashFunction */
 
 }/* CVC4 namespace */
diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp
index 4ebc5071f..b9870afb4 100644
--- a/src/expr/datatype.cpp
+++ b/src/expr/datatype.cpp
@@ -67,7 +67,7 @@ const Datatype& Datatype::datatypeOf(Expr item) {
 
 size_t Datatype::indexOf(Expr item) {
   ExprManagerScope ems(item);
-  CheckArgument(item.getType().isConstructor() ||
+  PrettyCheckArgument(item.getType().isConstructor() ||
                 item.getType().isTester() ||
                 item.getType().isSelector(),
                 item,
@@ -83,7 +83,7 @@ size_t Datatype::indexOf(Expr item) {
 
 size_t Datatype::cindexOf(Expr item) {
   ExprManagerScope ems(item);
-  CheckArgument(item.getType().isSelector(),
+  PrettyCheckArgument(item.getType().isSelector(),
                 item,
                 "arg must be a datatype selector");
   TNode n = Node::fromExpr(item);
@@ -103,17 +103,17 @@ void Datatype::resolve(ExprManager* em,
                        const std::vector< DatatypeType >& paramReplacements)
   throw(IllegalArgumentException, DatatypeResolutionException) {
 
-  CheckArgument(em != NULL, em, "cannot resolve a Datatype with a NULL expression manager");
-  CheckArgument(!d_resolved, this, "cannot resolve a Datatype twice");
-  CheckArgument(resolutions.find(d_name) != resolutions.end(), resolutions,
+  PrettyCheckArgument(em != NULL, em, "cannot resolve a Datatype with a NULL expression manager");
+  PrettyCheckArgument(!d_resolved, this, "cannot resolve a Datatype twice");
+  PrettyCheckArgument(resolutions.find(d_name) != resolutions.end(), resolutions,
                 "Datatype::resolve(): resolutions doesn't contain me!");
-  CheckArgument(placeholders.size() == replacements.size(), placeholders,
+  PrettyCheckArgument(placeholders.size() == replacements.size(), placeholders,
                 "placeholders and replacements must be the same size");
-  CheckArgument(paramTypes.size() == paramReplacements.size(), paramTypes,
+  PrettyCheckArgument(paramTypes.size() == paramReplacements.size(), paramTypes,
                 "paramTypes and paramReplacements must be the same size");
-  CheckArgument(getNumConstructors() > 0, *this, "cannot resolve a Datatype that has no constructors");
+  PrettyCheckArgument(getNumConstructors() > 0, *this, "cannot resolve a Datatype that has no constructors");
   DatatypeType self = (*resolutions.find(d_name)).second;
-  CheckArgument(&self.getDatatype() == this, resolutions, "Datatype::resolve(): resolutions doesn't contain me!");
+  PrettyCheckArgument(&self.getDatatype() == this, resolutions, "Datatype::resolve(): resolutions doesn't contain me!");
   d_resolved = true;
   size_t index = 0;
   for(std::vector<DatatypeConstructor>::iterator i = d_constructors.begin(), i_end = d_constructors.end(); i != i_end; ++i) {
@@ -136,14 +136,14 @@ void Datatype::resolve(ExprManager* em,
 }
 
 void Datatype::addConstructor(const DatatypeConstructor& c) {
-  CheckArgument(!d_resolved, this,
+  PrettyCheckArgument(!d_resolved, this,
                 "cannot add a constructor to a finalized Datatype");
   d_constructors.push_back(c);
 }
 
 
 void Datatype::setSygus( Type st, Expr bvl, bool allow_const, bool allow_all ){
-  CheckArgument(!d_resolved, this,
+  PrettyCheckArgument(!d_resolved, this,
                 "cannot set sygus type to a finalized Datatype");
   d_sygus_type = st;
   d_sygus_bvl = bvl;
@@ -153,14 +153,14 @@ void Datatype::setSygus( Type st, Expr bvl, bool allow_const, bool allow_all ){
 
 
 Cardinality Datatype::getCardinality() const throw(IllegalArgumentException) {
-  CheckArgument(isResolved(), this, "this datatype is not yet resolved");
+  PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
   std::vector< Type > processing;
   computeCardinality( processing );
   return d_card;
 }
 
 Cardinality Datatype::computeCardinality( std::vector< Type >& processing ) const throw(IllegalArgumentException){
-  CheckArgument(isResolved(), this, "this datatype is not yet resolved");
+  PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
   if( std::find( processing.begin(), processing.end(), d_self )!=processing.end() ){
     d_card = Cardinality::INTEGERS;
   }else{
@@ -176,7 +176,7 @@ Cardinality Datatype::computeCardinality( std::vector< Type >& processing ) cons
 }
 
 bool Datatype::isRecursiveSingleton() const throw(IllegalArgumentException) {
-  CheckArgument(isResolved(), this, "this datatype is not yet resolved");
+  PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
   if( d_card_rec_singleton==0 ){
     Assert( d_card_u_assume.empty() );
     std::vector< Type > processing;
@@ -251,7 +251,8 @@ bool Datatype::computeCardinalityRecSingleton( std::vector< Type >& processing,
 }
 
 bool Datatype::isFinite() const throw(IllegalArgumentException) {
-  CheckArgument(isResolved(), this, "this datatype is not yet resolved");
+  PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
+
   // we're using some internals, so we have to set up this library context
   ExprManagerScope ems(d_self);
   TypeNode self = TypeNode::fromType(d_self);
@@ -272,7 +273,7 @@ bool Datatype::isFinite() const throw(IllegalArgumentException) {
 }
 
 bool Datatype::isUFinite() const throw(IllegalArgumentException) {
-  CheckArgument(isResolved(), this, "this datatype is not yet resolved");
+  PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
   // we're using some internals, so we have to set up this library context
   ExprManagerScope ems(d_self);
   TypeNode self = TypeNode::fromType(d_self);
@@ -293,7 +294,7 @@ bool Datatype::isUFinite() const throw(IllegalArgumentException) {
 }
 
 bool Datatype::isWellFounded() const throw(IllegalArgumentException) {
-  CheckArgument(isResolved(), this, "this datatype is not yet resolved");
+  PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
   if( d_well_founded==0 ){
     // we're using some internals, so we have to set up this library context
     ExprManagerScope ems(d_self);
@@ -308,7 +309,7 @@ bool Datatype::isWellFounded() const throw(IllegalArgumentException) {
 }
 
 bool Datatype::computeWellFounded( std::vector< Type >& processing ) const throw(IllegalArgumentException) {
-  CheckArgument(isResolved(), this, "this datatype is not yet resolved");
+  PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
   if( std::find( processing.begin(), processing.end(), d_self )!=processing.end() ){
     return d_isCo;
   }else{
@@ -328,7 +329,7 @@ bool Datatype::computeWellFounded( std::vector< Type >& processing ) const throw
 }
 
 Expr Datatype::mkGroundTerm( Type t ) const throw(IllegalArgumentException) {
-  CheckArgument(isResolved(), this, "this datatype is not yet resolved");
+  PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
   ExprManagerScope ems(d_self);
 
 
@@ -348,7 +349,7 @@ Expr Datatype::mkGroundTerm( Type t ) const throw(IllegalArgumentException) {
     if( groundTerm.isNull() ){
       if( !d_isCo ){
         // if we get all the way here, we aren't well-founded
-        CheckArgument(false, *this, "datatype is not well-founded, cannot construct a ground term!");
+        IllegalArgument(*this, "datatype is not well-founded, cannot construct a ground term!");
       }else{
         return groundTerm;
       }
@@ -404,15 +405,15 @@ Expr Datatype::computeGroundTerm( Type t, std::vector< Type >& processing ) cons
 }
 
 DatatypeType Datatype::getDatatypeType() const throw(IllegalArgumentException) {
-  CheckArgument(isResolved(), *this, "Datatype must be resolved to get its DatatypeType");
-  CheckArgument(!d_self.isNull(), *this);
+  PrettyCheckArgument(isResolved(), *this, "Datatype must be resolved to get its DatatypeType");
+  PrettyCheckArgument(!d_self.isNull(), *this);
   return DatatypeType(d_self);
 }
 
 DatatypeType Datatype::getDatatypeType(const std::vector<Type>& params)
   const throw(IllegalArgumentException) {
-  CheckArgument(isResolved(), *this, "Datatype must be resolved to get its DatatypeType");
-  CheckArgument(!d_self.isNull() && DatatypeType(d_self).isParametric(), this);
+  PrettyCheckArgument(isResolved(), *this, "Datatype must be resolved to get its DatatypeType");
+  PrettyCheckArgument(!d_self.isNull() && DatatypeType(d_self).isParametric(), this);
   return DatatypeType(d_self).instantiate(params);
 }
 
@@ -491,7 +492,7 @@ bool Datatype::operator==(const Datatype& other) const throw() {
 }
 
 const DatatypeConstructor& Datatype::operator[](size_t index) const {
-  CheckArgument(index < getNumConstructors(), index, "index out of bounds");
+  PrettyCheckArgument(index < getNumConstructors(), index, "index out of bounds");
   return d_constructors[index];
 }
 
@@ -501,7 +502,7 @@ const DatatypeConstructor& Datatype::operator[](std::string name) const {
       return *i;
     }
   }
-  CheckArgument(false, name, "No such constructor `%s' of datatype `%s'", name.c_str(), d_name.c_str());
+  IllegalArgument(name, "No such constructor `%s' of datatype `%s'", name.c_str(), d_name.c_str());
 }
 
 Expr Datatype::getConstructor(std::string name) const {
@@ -540,8 +541,8 @@ void DatatypeConstructor::resolve(ExprManager* em, DatatypeType self,
                                   const std::vector< DatatypeType >& paramReplacements, size_t cindex)
   throw(IllegalArgumentException, DatatypeResolutionException) {
 
-  CheckArgument(em != NULL, em, "cannot resolve a Datatype with a NULL expression manager");
-  CheckArgument(!isResolved(),
+  PrettyCheckArgument(em != NULL, em, "cannot resolve a Datatype with a NULL expression manager");
+  PrettyCheckArgument(!isResolved(),
                 "cannot resolve a Datatype constructor twice; "
                 "perhaps the same constructor was added twice, "
                 "or to two datatypes?");
@@ -640,7 +641,7 @@ DatatypeConstructor::DatatypeConstructor(std::string name) :
   d_name(name + '\0' + "is_" + name), // default tester name is "is_FOO"
   d_tester(),
   d_args() {
-  CheckArgument(name != "", name, "cannot construct a datatype constructor without a name");
+  PrettyCheckArgument(name != "", name, "cannot construct a datatype constructor without a name");
 }
 
 DatatypeConstructor::DatatypeConstructor(std::string name, std::string tester) :
@@ -651,8 +652,8 @@ DatatypeConstructor::DatatypeConstructor(std::string name, std::string tester) :
   d_name(name + '\0' + tester),
   d_tester(),
   d_args() {
-  CheckArgument(name != "", name, "cannot construct a datatype constructor without a name");
-  CheckArgument(!tester.empty(), tester, "cannot construct a datatype constructor without a tester");
+  PrettyCheckArgument(name != "", name, "cannot construct a datatype constructor without a name");
+  PrettyCheckArgument(!tester.empty(), tester, "cannot construct a datatype constructor without a tester");
 }
 
 void DatatypeConstructor::setSygus( Expr op, Expr let_body, std::vector< Expr >& let_args, unsigned num_let_input_args ){
@@ -668,8 +669,8 @@ void DatatypeConstructor::addArg(std::string selectorName, Type selectorType) {
   // we're going to be a constant stuffed inside a node.  So we stow
   // the selector type away inside a var until resolution (when we can
   // create the proper selector type)
-  CheckArgument(!isResolved(), this, "cannot modify a finalized Datatype constructor");
-  CheckArgument(!selectorType.isNull(), selectorType, "cannot add a null selector type");
+  PrettyCheckArgument(!isResolved(), this, "cannot modify a finalized Datatype constructor");
+  PrettyCheckArgument(!selectorType.isNull(), selectorType, "cannot add a null selector type");
 
   // we're using some internals, so we have to set up this library context
   ExprManagerScope ems(selectorType);
@@ -684,8 +685,8 @@ void DatatypeConstructor::addArg(std::string selectorName, DatatypeUnresolvedTyp
   // we're going to be a constant stuffed inside a node.  So we stow
   // the selector type away after a NUL in the name string until
   // resolution (when we can create the proper selector type)
-  CheckArgument(!isResolved(), this, "cannot modify a finalized Datatype constructor");
-  CheckArgument(selectorType.getName() != "", selectorType, "cannot add a null selector type");
+  PrettyCheckArgument(!isResolved(), this, "cannot modify a finalized Datatype constructor");
+  PrettyCheckArgument(selectorType.getName() != "", selectorType, "cannot add a null selector type");
   d_args.push_back(DatatypeConstructorArg(selectorName + '\0' + selectorType.getName(), Expr()));
 }
 
@@ -695,7 +696,7 @@ void DatatypeConstructor::addArg(std::string selectorName, DatatypeSelfType) {
   // the name string with a NUL to indicate that we have a
   // self-selecting selector until resolution (when we can create the
   // proper selector type)
-  CheckArgument(!isResolved(), this, "cannot modify a finalized Datatype constructor");
+  PrettyCheckArgument(!isResolved(), this, "cannot modify a finalized Datatype constructor");
   d_args.push_back(DatatypeConstructorArg(selectorName + '\0', Expr()));
 }
 
@@ -708,15 +709,15 @@ std::string DatatypeConstructor::getTesterName() const throw() {
 }
 
 Expr DatatypeConstructor::getConstructor() const {
-  CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
+  PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
   return d_constructor;
 }
 
 Type DatatypeConstructor::getSpecializedConstructorType(Type returnType) const {
-  CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
+  PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
   ExprManagerScope ems(d_constructor);
   const Datatype& dt = Datatype::datatypeOf(d_constructor);
-  CheckArgument(dt.isParametric(), this, "this datatype constructor is not parametric");
+  PrettyCheckArgument(dt.isParametric(), this, "this datatype constructor is not parametric");
   DatatypeType dtt = dt.getDatatypeType();
   Matcher m(dtt);
   m.doMatching( TypeNode::fromType(dtt), TypeNode::fromType(returnType) );
@@ -727,42 +728,42 @@ Type DatatypeConstructor::getSpecializedConstructorType(Type returnType) const {
 }
 
 Expr DatatypeConstructor::getTester() const {
-  CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
+  PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
   return d_tester;
 }
 
 Expr DatatypeConstructor::getSygusOp() const {
-  CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
+  PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
   return d_sygus_op;
 }
 
 Expr DatatypeConstructor::getSygusLetBody() const {
-  CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
+  PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
   return d_sygus_let_body;
 }
 
 unsigned DatatypeConstructor::getNumSygusLetArgs() const {
-  CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
+  PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
   return d_sygus_let_args.size();
 }
 
 Expr DatatypeConstructor::getSygusLetArg( unsigned i ) const {
-  CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
+  PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
   return d_sygus_let_args[i];
 }
 
 unsigned DatatypeConstructor::getNumSygusLetInputArgs() const {
-  CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
+  PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
   return d_sygus_num_let_input_args;
 }
 
 bool DatatypeConstructor::isSygusIdFunc() const {
-  CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
+  PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
   return d_sygus_let_args.size()==1 && d_sygus_let_args[0]==d_sygus_let_body;
 }
 
 Cardinality DatatypeConstructor::getCardinality() const throw(IllegalArgumentException) {
-  CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
+  PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
 
   Cardinality c = 1;
 
@@ -803,7 +804,8 @@ bool DatatypeConstructor::computeWellFounded( std::vector< Type >& processing )
 
 
 bool DatatypeConstructor::isFinite() const throw(IllegalArgumentException) {
-  CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
+  PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
+
   // we're using some internals, so we have to set up this library context
   ExprManagerScope ems(d_constructor);
   TNode self = Node::fromExpr(d_constructor);
@@ -822,8 +824,9 @@ bool DatatypeConstructor::isFinite() const throw(IllegalArgumentException) {
   self.setAttribute(DatatypeFiniteAttr(), true);
   return true;
 }
+
 bool DatatypeConstructor::isUFinite() const throw(IllegalArgumentException) {
-  CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
+  PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
   // we're using some internals, so we have to set up this library context
   ExprManagerScope ems(d_constructor);
   TNode self = Node::fromExpr(d_constructor);
@@ -899,7 +902,7 @@ Expr DatatypeConstructor::computeGroundTerm( Type t, std::vector< Type >& proces
 
 
 const DatatypeConstructorArg& DatatypeConstructor::operator[](size_t index) const {
-  CheckArgument(index < getNumArgs(), index, "index out of bounds");
+  PrettyCheckArgument(index < getNumArgs(), index, "index out of bounds");
   return d_args[index];
 }
 
@@ -909,7 +912,7 @@ const DatatypeConstructorArg& DatatypeConstructor::operator[](std::string name)
       return *i;
     }
   }
-  CheckArgument(false, name, "No such arg `%s' of constructor `%s'", name.c_str(), d_name.c_str());
+  IllegalArgument(name, "No such arg `%s' of constructor `%s'", name.c_str(), d_name.c_str());
 }
 
 Expr DatatypeConstructor::getSelector(std::string name) const {
@@ -938,7 +941,7 @@ DatatypeConstructorArg::DatatypeConstructorArg(std::string name, Expr selector)
   d_name(name),
   d_selector(selector),
   d_resolved(false) {
-  CheckArgument(name != "", name, "cannot construct a datatype constructor arg without a name");
+  PrettyCheckArgument(name != "", name, "cannot construct a datatype constructor arg without a name");
 }
 
 std::string DatatypeConstructorArg::getName() const throw() {
@@ -951,12 +954,12 @@ std::string DatatypeConstructorArg::getName() const throw() {
 }
 
 Expr DatatypeConstructorArg::getSelector() const {
-  CheckArgument(isResolved(), this, "cannot get a selector for an unresolved datatype constructor");
+  PrettyCheckArgument(isResolved(), this, "cannot get a selector for an unresolved datatype constructor");
   return d_selector;
 }
 
 Expr DatatypeConstructorArg::getConstructor() const {
-  CheckArgument(isResolved(), this,
+  PrettyCheckArgument(isResolved(), this,
                 "cannot get a associated constructor for argument of an unresolved datatype constructor");
   return d_constructor;
 }
diff --git a/src/expr/datatype.h b/src/expr/datatype.h
index 1ea9fd6be..5f80c54f7 100644
--- a/src/expr/datatype.h
+++ b/src/expr/datatype.h
@@ -798,13 +798,16 @@ inline size_t Datatype::getNumParameters() const throw() {
 }
 
 inline Type Datatype::getParameter( unsigned int i ) const {
-  CheckArgument(isParametric(), this, "cannot get type parameter of a non-parametric datatype");
-  CheckArgument(i < d_params.size(), i, "type parameter index out of range for datatype");
+  CheckArgument(isParametric(), this,
+                "Cannot get type parameter of a non-parametric datatype.");
+  CheckArgument(i < d_params.size(), i,
+                "Type parameter index out of range for datatype.");
   return d_params[i];
 }
 
 inline std::vector<Type> Datatype::getParameters() const {
-  CheckArgument(isParametric(), this, "cannot get type parameters of a non-parametric datatype");
+  CheckArgument(isParametric(), this,
+                "Cannot get type parameters of a non-parametric datatype.");
   return d_params;
 }
 
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index e7088a395..59f423e3c 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -29,7 +29,7 @@ ${includes}
 // compiler directs the user to the template file instead of the
 // generated one.  We don't want the user to modify the generated one,
 // since it'll get overwritten on a later build.
-#line 32 "${template}"
+#line 33 "${template}"
 
 #ifdef CVC4_STATISTICS_ON
   #define INC_STAT(kind) \
@@ -164,16 +164,18 @@ RoundingModeType ExprManager::roundingModeType() const {
 Expr ExprManager::mkExpr(Kind kind, Expr child1) {
   const kind::MetaKind mk = kind::metaKindOf(kind);
   const unsigned n = 1 - (mk == kind::metakind::PARAMETERIZED ? 1 : 0);
-  CheckArgument(mk == kind::metakind::PARAMETERIZED ||
-                mk == kind::metakind::OPERATOR, kind,
-                "Only operator-style expressions are made with mkExpr(); "
-                "to make variables and constants, see mkVar(), mkBoundVar(), "
-                "and mkConst().");
-  CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
-                "Exprs with kind %s must have at least %u children and "
-                "at most %u children (the one under construction has %u)",
-                kind::kindToString(kind).c_str(),
-                minArity(kind), maxArity(kind), n);
+  PrettyCheckArgument(
+      mk == kind::metakind::PARAMETERIZED ||
+      mk == kind::metakind::OPERATOR, kind,
+      "Only operator-style expressions are made with mkExpr(); "
+      "to make variables and constants, see mkVar(), mkBoundVar(), "
+      "and mkConst().");
+  PrettyCheckArgument(
+      n >= minArity(kind) && n <= maxArity(kind), kind,
+      "Exprs with kind %s must have at least %u children and "
+      "at most %u children (the one under construction has %u)",
+      kind::kindToString(kind).c_str(),
+      minArity(kind), maxArity(kind), n);
   NodeManagerScope nms(d_nodeManager);
   try {
     INC_STAT(kind);
@@ -186,16 +188,18 @@ Expr ExprManager::mkExpr(Kind kind, Expr child1) {
 Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2) {
   const kind::MetaKind mk = kind::metaKindOf(kind);
   const unsigned n = 2 - (mk == kind::metakind::PARAMETERIZED ? 1 : 0);
-  CheckArgument(mk == kind::metakind::PARAMETERIZED ||
-                mk == kind::metakind::OPERATOR, kind,
-                "Only operator-style expressions are made with mkExpr(); "
-                "to make variables and constants, see mkVar(), mkBoundVar(), "
-                "and mkConst().");
-  CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
-                "Exprs with kind %s must have at least %u children and "
-                "at most %u children (the one under construction has %u)",
-                kind::kindToString(kind).c_str(),
-                minArity(kind), maxArity(kind), n);
+  PrettyCheckArgument(
+      mk == kind::metakind::PARAMETERIZED ||
+      mk == kind::metakind::OPERATOR, kind,
+      "Only operator-style expressions are made with mkExpr(); "
+      "to make variables and constants, see mkVar(), mkBoundVar(), "
+      "and mkConst().");
+  PrettyCheckArgument(
+      n >= minArity(kind) && n <= maxArity(kind), kind,
+      "Exprs with kind %s must have at least %u children and "
+      "at most %u children (the one under construction has %u)",
+      kind::kindToString(kind).c_str(),
+      minArity(kind), maxArity(kind), n);
   NodeManagerScope nms(d_nodeManager);
   try {
     INC_STAT(kind);
@@ -210,16 +214,18 @@ Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2) {
 Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2, Expr child3) {
   const kind::MetaKind mk = kind::metaKindOf(kind);
   const unsigned n = 3 - (mk == kind::metakind::PARAMETERIZED ? 1 : 0);
-  CheckArgument(mk == kind::metakind::PARAMETERIZED ||
-                mk == kind::metakind::OPERATOR, kind,
-                "Only operator-style expressions are made with mkExpr(); "
-                "to make variables and constants, see mkVar(), mkBoundVar(), "
-                "and mkConst().");
-  CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
-                "Exprs with kind %s must have at least %u children and "
-                "at most %u children (the one under construction has %u)",
-                kind::kindToString(kind).c_str(),
-                minArity(kind), maxArity(kind), n);
+  PrettyCheckArgument(
+      mk == kind::metakind::PARAMETERIZED ||
+      mk == kind::metakind::OPERATOR, kind,
+      "Only operator-style expressions are made with mkExpr(); "
+      "to make variables and constants, see mkVar(), mkBoundVar(), "
+      "and mkConst().");
+  PrettyCheckArgument(
+      n >= minArity(kind) && n <= maxArity(kind), kind,
+      "Exprs with kind %s must have at least %u children and "
+      "at most %u children (the one under construction has %u)",
+      kind::kindToString(kind).c_str(),
+      minArity(kind), maxArity(kind), n);
   NodeManagerScope nms(d_nodeManager);
   try {
     INC_STAT(kind);
@@ -236,16 +242,18 @@ Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2, Expr child3,
                          Expr child4) {
   const kind::MetaKind mk = kind::metaKindOf(kind);
   const unsigned n = 4 - (mk == kind::metakind::PARAMETERIZED ? 1 : 0);
-  CheckArgument(mk == kind::metakind::PARAMETERIZED ||
-                mk == kind::metakind::OPERATOR, kind,
-                "Only operator-style expressions are made with mkExpr(); "
-                "to make variables and constants, see mkVar(), mkBoundVar(), "
-                "and mkConst().");
-  CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
-                "Exprs with kind %s must have at least %u children and "
-                "at most %u children (the one under construction has %u)",
-                kind::kindToString(kind).c_str(),
-                minArity(kind), maxArity(kind), n);
+  PrettyCheckArgument(
+      mk == kind::metakind::PARAMETERIZED ||
+      mk == kind::metakind::OPERATOR, kind,
+      "Only operator-style expressions are made with mkExpr(); "
+      "to make variables and constants, see mkVar(), mkBoundVar(), "
+      "and mkConst().");
+  PrettyCheckArgument(
+      n >= minArity(kind) && n <= maxArity(kind), kind,
+      "Exprs with kind %s must have at least %u children and "
+      "at most %u children (the one under construction has %u)",
+      kind::kindToString(kind).c_str(),
+      minArity(kind), maxArity(kind), n);
   NodeManagerScope nms(d_nodeManager);
   try {
     INC_STAT(kind);
@@ -263,16 +271,18 @@ Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2, Expr child3,
                          Expr child4, Expr child5) {
   const kind::MetaKind mk = kind::metaKindOf(kind);
   const unsigned n = 5 - (mk == kind::metakind::PARAMETERIZED ? 1 : 0);
-  CheckArgument(mk == kind::metakind::PARAMETERIZED ||
-                mk == kind::metakind::OPERATOR, kind,
-                "Only operator-style expressions are made with mkExpr(); "
-                "to make variables and constants, see mkVar(), mkBoundVar(), "
-                "and mkConst().");
-  CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
-                "Exprs with kind %s must have at least %u children and "
-                "at most %u children (the one under construction has %u)",
-                kind::kindToString(kind).c_str(),
-                minArity(kind), maxArity(kind), n);
+  PrettyCheckArgument(
+      mk == kind::metakind::PARAMETERIZED ||
+      mk == kind::metakind::OPERATOR, kind,
+      "Only operator-style expressions are made with mkExpr(); "
+      "to make variables and constants, see mkVar(), mkBoundVar(), "
+      "and mkConst().");
+  PrettyCheckArgument(
+      n >= minArity(kind) && n <= maxArity(kind), kind,
+      "Exprs with kind %s must have at least %u children and "
+      "at most %u children (the one under construction has %u)",
+      kind::kindToString(kind).c_str(),
+      minArity(kind), maxArity(kind), n);
   NodeManagerScope nms(d_nodeManager);
   try {
     INC_STAT(kind);
@@ -290,16 +300,18 @@ Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2, Expr child3,
 Expr ExprManager::mkExpr(Kind kind, const std::vector<Expr>& children) {
   const kind::MetaKind mk = kind::metaKindOf(kind);
   const unsigned n = children.size() - (mk == kind::metakind::PARAMETERIZED ? 1 : 0);
-  CheckArgument(mk == kind::metakind::PARAMETERIZED ||
-                mk == kind::metakind::OPERATOR, kind,
-                "Only operator-style expressions are made with mkExpr(); "
-                "to make variables and constants, see mkVar(), mkBoundVar(), "
-                "and mkConst().");
-  CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
-                "Exprs with kind %s must have at least %u children and "
-                "at most %u children (the one under construction has %u)",
-                kind::kindToString(kind).c_str(),
-                minArity(kind), maxArity(kind), n);
+  PrettyCheckArgument(
+      mk == kind::metakind::PARAMETERIZED ||
+      mk == kind::metakind::OPERATOR, kind,
+      "Only operator-style expressions are made with mkExpr(); "
+      "to make variables and constants, see mkVar(), mkBoundVar(), "
+      "and mkConst().");
+  PrettyCheckArgument(
+      n >= minArity(kind) && n <= maxArity(kind), kind,
+      "Exprs with kind %s must have at least %u children and "
+      "at most %u children (the one under construction has %u)",
+      kind::kindToString(kind).c_str(),
+      minArity(kind), maxArity(kind), n);
 
   NodeManagerScope nms(d_nodeManager);
 
@@ -321,17 +333,20 @@ Expr ExprManager::mkExpr(Kind kind, const std::vector<Expr>& children) {
 Expr ExprManager::mkExpr(Kind kind, Expr child1,
                          const std::vector<Expr>& otherChildren) {
   const kind::MetaKind mk = kind::metaKindOf(kind);
-  const unsigned n = otherChildren.size() - (mk == kind::metakind::PARAMETERIZED ? 1 : 0) + 1;
-  CheckArgument(mk == kind::metakind::PARAMETERIZED ||
-                mk == kind::metakind::OPERATOR, kind,
-                "Only operator-style expressions are made with mkExpr(); "
-                "to make variables and constants, see mkVar(), mkBoundVar(), "
-                "and mkConst().");
-  CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
-                "Exprs with kind %s must have at least %u children and "
-                "at most %u children (the one under construction has %u)",
-                kind::kindToString(kind).c_str(),
-                minArity(kind), maxArity(kind), n);
+  const unsigned n =
+      otherChildren.size() - (mk == kind::metakind::PARAMETERIZED ? 1 : 0) + 1;
+  PrettyCheckArgument(
+      mk == kind::metakind::PARAMETERIZED ||
+      mk == kind::metakind::OPERATOR, kind,
+      "Only operator-style expressions are made with mkExpr(); "
+      "to make variables and constants, see mkVar(), mkBoundVar(), "
+      "and mkConst().");
+  PrettyCheckArgument(
+      n >= minArity(kind) && n <= maxArity(kind), kind,
+      "Exprs with kind %s must have at least %u children and "
+      "at most %u children (the one under construction has %u)",
+      kind::kindToString(kind).c_str(),
+      minArity(kind), maxArity(kind), n);
 
   NodeManagerScope nms(d_nodeManager);
 
@@ -355,13 +370,16 @@ Expr ExprManager::mkExpr(Kind kind, Expr child1,
 Expr ExprManager::mkExpr(Expr opExpr) {
   const unsigned n = 0;
   Kind kind = NodeManager::operatorToKind(opExpr.getNode());
-  CheckArgument(opExpr.getKind() == kind::BUILTIN || kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
-                "This Expr constructor is for parameterized kinds only");
-  CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
-                "Exprs with kind %s must have at least %u children and "
-                "at most %u children (the one under construction has %u)",
-                kind::kindToString(kind).c_str(),
-                minArity(kind), maxArity(kind), n);
+  PrettyCheckArgument(
+      opExpr.getKind() == kind::BUILTIN ||
+      kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
+      "This Expr constructor is for parameterized kinds only");
+  PrettyCheckArgument(
+      n >= minArity(kind) && n <= maxArity(kind), kind,
+      "Exprs with kind %s must have at least %u children and "
+      "at most %u children (the one under construction has %u)",
+      kind::kindToString(kind).c_str(),
+      minArity(kind), maxArity(kind), n);
   NodeManagerScope nms(d_nodeManager);
   try {
     INC_STAT(kind);
@@ -374,13 +392,16 @@ Expr ExprManager::mkExpr(Expr opExpr) {
 Expr ExprManager::mkExpr(Expr opExpr, Expr child1) {
   const unsigned n = 1;
   Kind kind = NodeManager::operatorToKind(opExpr.getNode());
-  CheckArgument(opExpr.getKind() == kind::BUILTIN || kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
-                "This Expr constructor is for parameterized kinds only");
-  CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
-                "Exprs with kind %s must have at least %u children and "
-                "at most %u children (the one under construction has %u)",
-                kind::kindToString(kind).c_str(),
-                minArity(kind), maxArity(kind), n);
+  PrettyCheckArgument(
+      (opExpr.getKind() == kind::BUILTIN ||
+       kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED), opExpr,
+      "This Expr constructor is for parameterized kinds only");
+  PrettyCheckArgument(
+      n >= minArity(kind) && n <= maxArity(kind), kind,
+      "Exprs with kind %s must have at least %u children and "
+      "at most %u children (the one under construction has %u)",
+      kind::kindToString(kind).c_str(),
+      minArity(kind), maxArity(kind), n);
   NodeManagerScope nms(d_nodeManager);
   try {
     INC_STAT(kind);
@@ -393,13 +414,16 @@ Expr ExprManager::mkExpr(Expr opExpr, Expr child1) {
 Expr ExprManager::mkExpr(Expr opExpr, Expr child1, Expr child2) {
   const unsigned n = 2;
   Kind kind = NodeManager::operatorToKind(opExpr.getNode());
-  CheckArgument(opExpr.getKind() == kind::BUILTIN || kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
-                "This Expr constructor is for parameterized kinds only");
-  CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
-                "Exprs with kind %s must have at least %u children and "
-                "at most %u children (the one under construction has %u)",
-                kind::kindToString(kind).c_str(),
-                minArity(kind), maxArity(kind), n);
+  PrettyCheckArgument(
+      (opExpr.getKind() == kind::BUILTIN ||
+       kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED), opExpr,
+      "This Expr constructor is for parameterized kinds only");
+  PrettyCheckArgument(
+      n >= minArity(kind) && n <= maxArity(kind), kind,
+      "Exprs with kind %s must have at least %u children and "
+      "at most %u children (the one under construction has %u)",
+      kind::kindToString(kind).c_str(),
+      minArity(kind), maxArity(kind), n);
   NodeManagerScope nms(d_nodeManager);
   try {
     INC_STAT(kind);
@@ -414,9 +438,11 @@ Expr ExprManager::mkExpr(Expr opExpr, Expr child1, Expr child2) {
 Expr ExprManager::mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3) {
   const unsigned n = 3;
   Kind kind = NodeManager::operatorToKind(opExpr.getNode());
-  CheckArgument(opExpr.getKind() == kind::BUILTIN || kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
+  PrettyCheckArgument(
+      (opExpr.getKind() == kind::BUILTIN ||
+       kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED), opExpr,
                 "This Expr constructor is for parameterized kinds only");
-  CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
+  PrettyCheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
                 "Exprs with kind %s must have at least %u children and "
                 "at most %u children (the one under construction has %u)",
                 kind::kindToString(kind).c_str(),
@@ -437,13 +463,18 @@ Expr ExprManager::mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3,
                          Expr child4) {
   const unsigned n = 4;
   Kind kind = NodeManager::operatorToKind(opExpr.getNode());
-  CheckArgument(opExpr.getKind() == kind::BUILTIN || kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
-                "This Expr constructor is for parameterized kinds only");
-  CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
-                "Exprs with kind %s must have at least %u children and "
-                "at most %u children (the one under construction has %u)",
-                kind::kindToString(kind).c_str(),
-                minArity(kind), maxArity(kind), n);
+  PrettyCheckArgument(
+      (opExpr.getKind() == kind::BUILTIN ||
+       kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED), opExpr,
+      "This Expr constructor is for parameterized kinds only");
+
+  PrettyCheckArgument(
+      n >= minArity(kind) && n <= maxArity(kind), kind,
+      "Exprs with kind %s must have at least %u children and "
+      "at most %u children (the one under construction has %u)",
+      kind::kindToString(kind).c_str(),
+      minArity(kind), maxArity(kind), n);
+
   NodeManagerScope nms(d_nodeManager);
   try {
     INC_STAT(kind);
@@ -461,13 +492,16 @@ Expr ExprManager::mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3,
                          Expr child4, Expr child5) {
   const unsigned n = 5;
   Kind kind = NodeManager::operatorToKind(opExpr.getNode());
-  CheckArgument(opExpr.getKind() == kind::BUILTIN || kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
-                "This Expr constructor is for parameterized kinds only");
-  CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
-                "Exprs with kind %s must have at least %u children and "
-                "at most %u children (the one under construction has %u)",
-                kind::kindToString(kind).c_str(),
-                minArity(kind), maxArity(kind), n);
+  PrettyCheckArgument(
+      (opExpr.getKind() == kind::BUILTIN ||
+       kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED), opExpr,
+      "This Expr constructor is for parameterized kinds only");
+  PrettyCheckArgument(
+      n >= minArity(kind) && n <= maxArity(kind), kind,
+      "Exprs with kind %s must have at least %u children and "
+      "at most %u children (the one under construction has %u)",
+      kind::kindToString(kind).c_str(),
+      minArity(kind), maxArity(kind), n);
   NodeManagerScope nms(d_nodeManager);
   try {
     INC_STAT(kind);
@@ -485,13 +519,16 @@ Expr ExprManager::mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3,
 Expr ExprManager::mkExpr(Expr opExpr, const std::vector<Expr>& children) {
   const unsigned n = children.size();
   Kind kind = NodeManager::operatorToKind(opExpr.getNode());
-  CheckArgument(opExpr.getKind() == kind::BUILTIN || kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
-                "This Expr constructor is for parameterized kinds only");
-  CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
-                "Exprs with kind %s must have at least %u children and "
-                "at most %u children (the one under construction has %u)",
-                kind::kindToString(kind).c_str(),
-                minArity(kind), maxArity(kind), n);
+  PrettyCheckArgument(
+      (opExpr.getKind() == kind::BUILTIN ||
+       kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED), opExpr,
+      "This Expr constructor is for parameterized kinds only");
+  PrettyCheckArgument(
+      n >= minArity(kind) && n <= maxArity(kind), kind,
+      "Exprs with kind %s must have at least %u children and "
+      "at most %u children (the one under construction has %u)",
+      kind::kindToString(kind).c_str(),
+      minArity(kind), maxArity(kind), n);
 
   NodeManagerScope nms(d_nodeManager);
 
@@ -652,11 +689,12 @@ ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes,
     }
     Type type(d_nodeManager, typeNode);
     DatatypeType dtt(type);
-    CheckArgument(nameResolutions.find((*i).getName()) == nameResolutions.end(),
-                  datatypes,
-                  "cannot construct two datatypes at the same time "
-                  "with the same name `%s'",
-                  (*i).getName().c_str());
+    PrettyCheckArgument(
+        nameResolutions.find((*i).getName()) == nameResolutions.end(),
+        datatypes,
+        "cannot construct two datatypes at the same time "
+        "with the same name `%s'",
+        (*i).getName().c_str());
     nameResolutions.insert(std::make_pair((*i).getName(), dtt));
     dtts.push_back(dtt);
   }
@@ -687,10 +725,11 @@ ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes,
     }
     std::map<std::string, DatatypeType>::const_iterator resolver =
       nameResolutions.find(name);
-    CheckArgument(resolver != nameResolutions.end(),
-                  unresolvedTypes,
-                  "cannot resolve type `%s'; it's not among "
-                  "the datatypes being defined", name.c_str());
+    PrettyCheckArgument(
+        resolver != nameResolutions.end(),
+        unresolvedTypes,
+        "cannot resolve type `%s'; it's not among "
+        "the datatypes being defined", name.c_str());
     // We will instruct the Datatype to substitute "*i" (the
     // unresolved SortType used as a placeholder in complex types)
     // with "(*resolver).second" (the DatatypeType we created in the
@@ -902,9 +941,10 @@ Expr ExprManager::mkBoundVar(Type type) {
 
 Expr ExprManager::mkAssociative(Kind kind,
                                 const std::vector<Expr>& children) {
-  CheckArgument( kind::isAssociative(kind), kind,
-                 "Illegal kind in mkAssociative: %s",
-                 kind::kindToString(kind).c_str());
+  PrettyCheckArgument(
+      kind::isAssociative(kind), kind,
+      "Illegal kind in mkAssociative: %s",
+      kind::kindToString(kind).c_str());
 
   NodeManagerScope nms(d_nodeManager);
   const unsigned int max = maxArity(kind);
diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index dbd7c049b..dfbe179be 100644
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -13,18 +13,18 @@
  **
  ** Public-facing expression interface, implementation.
  **/
+#include "expr/expr.h"
+
+#include <iterator>
+#include <utility>
+#include <vector>
 
 #include "base/cvc4_assert.h"
-#include "expr/expr.h"
 #include "expr/node.h"
 #include "expr/expr_manager_scope.h"
 #include "expr/variable_type_map.h"
 #include "expr/node_manager_attributes.h"
 
-#include <vector>
-#include <iterator>
-#include <utility>
-
 ${includes}
 
 // This is a hack, but an important one: if there's an error, the
@@ -326,15 +326,16 @@ bool Expr::hasOperator() const {
 Expr Expr::getOperator() const {
   ExprManagerScope ems(*this);
   Assert(d_node != NULL, "Unexpected NULL expression pointer!");
-  CheckArgument(d_node->hasOperator(), *this,
-                "Expr::getOperator() called on an Expr with no operator");
+  PrettyCheckArgument(d_node->hasOperator(), *this,
+                      "Expr::getOperator() called on an Expr with no operator");
   return Expr(d_exprManager, new Node(d_node->getOperator()));
 }
 
 Type Expr::getType(bool check) const throw (TypeCheckingException) {
   ExprManagerScope ems(*this);
   Assert(d_node != NULL, "Unexpected NULL expression pointer!");
-  CheckArgument(!d_node->isNull(), this, "Can't get type of null expression!");
+  PrettyCheckArgument(!d_node->isNull(), this,
+                      "Can't get type of null expression!");
   return d_exprManager->getType(*this, check);
 }
 
@@ -509,40 +510,40 @@ Expr Expr::notExpr() const {
 Expr Expr::andExpr(const Expr& e) const {
   Assert(d_exprManager != NULL,
          "Don't have an expression manager for this expression!");
-  CheckArgument(d_exprManager == e.d_exprManager, e,
-                "Different expression managers!");
+  PrettyCheckArgument(d_exprManager == e.d_exprManager, e,
+                      "Different expression managers!");
   return d_exprManager->mkExpr(AND, *this, e);
 }
 
 Expr Expr::orExpr(const Expr& e) const {
   Assert(d_exprManager != NULL,
          "Don't have an expression manager for this expression!");
-  CheckArgument(d_exprManager == e.d_exprManager, e,
-                "Different expression managers!");
+  PrettyCheckArgument(d_exprManager == e.d_exprManager, e,
+                      "Different expression managers!");
   return d_exprManager->mkExpr(OR, *this, e);
 }
 
 Expr Expr::xorExpr(const Expr& e) const {
   Assert(d_exprManager != NULL,
          "Don't have an expression manager for this expression!");
-  CheckArgument(d_exprManager == e.d_exprManager, e,
-                "Different expression managers!");
+  PrettyCheckArgument(d_exprManager == e.d_exprManager, e,
+                      "Different expression managers!");
   return d_exprManager->mkExpr(XOR, *this, e);
 }
 
 Expr Expr::iffExpr(const Expr& e) const {
   Assert(d_exprManager != NULL,
          "Don't have an expression manager for this expression!");
-  CheckArgument(d_exprManager == e.d_exprManager, e,
-                "Different expression managers!");
+  PrettyCheckArgument(d_exprManager == e.d_exprManager, e,
+                      "Different expression managers!");
   return d_exprManager->mkExpr(IFF, *this, e);
 }
 
 Expr Expr::impExpr(const Expr& e) const {
   Assert(d_exprManager != NULL,
          "Don't have an expression manager for this expression!");
-  CheckArgument(d_exprManager == e.d_exprManager, e,
-                "Different expression managers!");
+  PrettyCheckArgument(d_exprManager == e.d_exprManager, e,
+                      "Different expression managers!");
   return d_exprManager->mkExpr(IMPLIES, *this, e);
 }
 
@@ -550,10 +551,10 @@ Expr Expr::iteExpr(const Expr& then_e,
                            const Expr& else_e) const {
   Assert(d_exprManager != NULL,
          "Don't have an expression manager for this expression!");
-  CheckArgument(d_exprManager == then_e.d_exprManager, then_e,
-                "Different expression managers!");
-  CheckArgument(d_exprManager == else_e.d_exprManager, else_e,
-                "Different expression managers!");
+  PrettyCheckArgument(d_exprManager == then_e.d_exprManager, then_e,
+                      "Different expression managers!");
+  PrettyCheckArgument(d_exprManager == else_e.d_exprManager, else_e,
+                      "Different expression managers!");
   return d_exprManager->mkExpr(ITE, *this, then_e, else_e);
 }
 
diff --git a/src/expr/kind_map.h b/src/expr/kind_map.h
index d3ed43e1c..02e9728f0 100644
--- a/src/expr/kind_map.h
+++ b/src/expr/kind_map.h
@@ -23,6 +23,7 @@
 #include <stdint.h>
 #include <iterator>
 
+#include "base/cvc4_assert.h"
 #include "expr/kind.h"
 
 namespace CVC4 {
diff --git a/src/expr/kind_template.h b/src/expr/kind_template.h
index c2ccb6b5e..799d1ac33 100644
--- a/src/expr/kind_template.h
+++ b/src/expr/kind_template.h
@@ -19,7 +19,7 @@
 #ifndef __CVC4__KIND_H
 #define __CVC4__KIND_H
 
-#include <iostream>
+#include <iosfwd>
 #include <sstream>
 
 #include "base/exception.h"
diff --git a/src/expr/matcher.h b/src/expr/matcher.h
index 92b1ce109..8cb092a64 100644
--- a/src/expr/matcher.h
+++ b/src/expr/matcher.h
@@ -19,7 +19,7 @@
 #ifndef __CVC4__MATCHER_H
 #define __CVC4__MATCHER_H
 
-#include <iostream>
+#include <iosfwd>
 #include <string>
 #include <vector>
 #include <map>
diff --git a/src/expr/mkexpr b/src/expr/mkexpr
index 068063c05..4717b611d 100755
--- a/src/expr/mkexpr
+++ b/src/expr/mkexpr
@@ -239,7 +239,7 @@ template <> $2 const & Expr::getConst< $2 >() const;
 #line $lineno \"$kf\"
 template <> $2 const & Expr::getConst() const {
 #line $lineno \"$kf\"
-  CheckArgument(getKind() == ::CVC4::kind::$1, *this, \"Improper kind for getConst<$2>()\");
+  PrettyCheckArgument(getKind() == ::CVC4::kind::$1, *this, \"Improper kind for getConst<$2>()\");
 #line $lineno \"$kf\"
   return d_node->getConst< $2 >();
 }
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 17524a3c0..c9e6866d4 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -393,8 +393,8 @@ TypeNode NodeManager::mkConstructorType(const DatatypeConstructor& constructor,
     sorts.push_back(sort);
   }
   Debug("datatypes") << "ctor range: " << range << endl;
-  CheckArgument(!range.isFunctionLike(), range,
-                "cannot create higher-order function types");
+  PrettyCheckArgument(!range.isFunctionLike(), range,
+                      "cannot create higher-order function types");
   sorts.push_back(range);
   return mkTypeNode(kind::CONSTRUCTOR_TYPE, sorts);
 }
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 390af8967..870408939 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -1098,7 +1098,8 @@ inline TypeNode NodeManager::mkArrayType(TypeNode indexType,
                 "cannot index arrays by a function-like type");
   CheckArgument(!constituentType.isFunctionLike(), constituentType,
                 "cannot store function-like types in arrays");
-  Debug("arrays") << "making array type " << indexType << " " << constituentType << std::endl;
+  Debug("arrays") << "making array type " << indexType << " "
+                  << constituentType << std::endl;
   return mkTypeNode(kind::ARRAY_TYPE, indexType, constituentType);
 }
 
diff --git a/src/expr/predicate.cpp b/src/expr/predicate.cpp
index a4dd29592..5ccc3484a 100644
--- a/src/expr/predicate.cpp
+++ b/src/expr/predicate.cpp
@@ -34,9 +34,11 @@ Predicate::Predicate(const Expr& e) throw(IllegalArgumentException)
     : d_predicate(new Expr(e))
     , d_witness(new Expr())
 {
-  CheckArgument(! e.isNull(), e, "Predicate cannot be null");
-  CheckArgument(e.getType().isPredicate(), e, "Expression given is not predicate");
-  CheckArgument(FunctionType(e.getType()).getArgTypes().size() == 1, e, "Expression given is not predicate of a single argument");
+  PrettyCheckArgument(! e.isNull(), e, "Predicate cannot be null");
+  PrettyCheckArgument(e.getType().isPredicate(), e,
+                      "Expression given is not predicate");
+  PrettyCheckArgument(FunctionType(e.getType()).getArgTypes().size() == 1, e,
+                      "Expression given is not predicate of a single argument");
 }
 
 Predicate::Predicate(const Expr& e, const Expr& w)
@@ -44,9 +46,11 @@ Predicate::Predicate(const Expr& e, const Expr& w)
     : d_predicate(new Expr(e))
     , d_witness(new Expr(w))
 {
-  CheckArgument(! e.isNull(), e, "Predicate cannot be null");
-  CheckArgument(e.getType().isPredicate(), e, "Expression given is not predicate");
-  CheckArgument(FunctionType(e.getType()).getArgTypes().size() == 1, e, "Expression given is not predicate of a single argument");
+  PrettyCheckArgument(! e.isNull(), e, "Predicate cannot be null");
+  PrettyCheckArgument(e.getType().isPredicate(), e,
+                      "Expression given is not predicate");
+  PrettyCheckArgument(FunctionType(e.getType()).getArgTypes().size() == 1, e,
+                      "Expression given is not predicate of a single argument");
 }
 
 Predicate::~Predicate() {
diff --git a/src/expr/record.cpp b/src/expr/record.cpp
index 2dee03dbf..ec5ef96f1 100644
--- a/src/expr/record.cpp
+++ b/src/expr/record.cpp
@@ -68,8 +68,9 @@ bool Record::contains(const std::string& name) const {
 
 size_t Record::getIndex(std::string name) const {
   FieldVector::const_iterator i = find(*d_fields, name);
-  CheckArgument(i != d_fields->end(), name,
-                  "requested field `%s' does not exist in record", name.c_str());
+  PrettyCheckArgument(i != d_fields->end(), name,
+                      "requested field `%s' does not exist in record",
+                      name.c_str());
   return i - d_fields->begin();
 }
 
@@ -115,7 +116,8 @@ std::ostream& operator<<(std::ostream& out, const RecordUpdate& t) {
 
 
 const std::pair<std::string, Type>& Record::operator[](size_t index) const {
-  CheckArgument(index < d_fields->size(), index, "index out of bounds for record type");
+  PrettyCheckArgument(index < d_fields->size(), index,
+                      "index out of bounds for record type");
   return (*d_fields)[index];
 }
 
diff --git a/src/expr/result.cpp b/src/expr/result.cpp
index 95e382b98..aeb62b0c3 100644
--- a/src/expr/result.cpp
+++ b/src/expr/result.cpp
@@ -29,6 +29,62 @@ using namespace std;
 
 namespace CVC4 {
 
+Result::Result()
+    : d_sat(SAT_UNKNOWN)
+    , d_validity(VALIDITY_UNKNOWN)
+    , d_which(TYPE_NONE)
+    , d_unknownExplanation(UNKNOWN_REASON)
+    , d_inputName("")
+{ }
+
+
+Result::Result(enum Sat s, std::string inputName)
+    : d_sat(s)
+    , d_validity(VALIDITY_UNKNOWN)
+    , d_which(TYPE_SAT)
+    , d_unknownExplanation(UNKNOWN_REASON)
+    , d_inputName(inputName)
+{
+  PrettyCheckArgument(s != SAT_UNKNOWN,
+                      "Must provide a reason for satisfiability being unknown");
+}
+
+Result::Result(enum Validity v, std::string inputName)
+    : d_sat(SAT_UNKNOWN)
+    , d_validity(v)
+    , d_which(TYPE_VALIDITY)
+    , d_unknownExplanation(UNKNOWN_REASON)
+    , d_inputName(inputName)
+{
+  PrettyCheckArgument(v != VALIDITY_UNKNOWN,
+                      "Must provide a reason for validity being unknown");
+}
+
+
+Result::Result(enum Sat s, enum UnknownExplanation unknownExplanation,
+               std::string inputName)
+    : d_sat(s)
+    , d_validity(VALIDITY_UNKNOWN)
+    , d_which(TYPE_SAT)
+    , d_unknownExplanation(unknownExplanation)
+    , d_inputName(inputName)
+{
+  PrettyCheckArgument(s == SAT_UNKNOWN,
+                      "improper use of unknown-result constructor");
+}
+
+Result::Result(enum Validity v, enum UnknownExplanation unknownExplanation,
+               std::string inputName)
+    : d_sat(SAT_UNKNOWN)
+    , d_validity(v)
+    , d_which(TYPE_VALIDITY)
+    , d_unknownExplanation(unknownExplanation)
+    , d_inputName(inputName)
+{
+  PrettyCheckArgument(v == VALIDITY_UNKNOWN,
+                      "improper use of unknown-result constructor");
+}
+
 Result::Result(const std::string& instr, std::string inputName) :
   d_sat(SAT_UNKNOWN),
   d_validity(VALIDITY_UNKNOWN),
@@ -78,6 +134,13 @@ Result::Result(const std::string& instr, std::string inputName) :
   }
 }
 
+Result::UnknownExplanation Result::whyUnknown() const {
+  PrettyCheckArgument( isUnknown(), this,
+                       "This result is not unknown, so the reason for "
+                       "being unknown cannot be inquired of it" );
+  return d_unknownExplanation;
+}
+
 bool Result::operator==(const Result& r) const throw() {
   if(d_which != r.d_which) {
     return false;
diff --git a/src/expr/result.h b/src/expr/result.h
index 74697eba6..8069f7ef9 100644
--- a/src/expr/result.h
+++ b/src/expr/result.h
@@ -75,49 +75,20 @@ private:
   std::string d_inputName;
 
 public:
-  Result() :
-    d_sat(SAT_UNKNOWN),
-    d_validity(VALIDITY_UNKNOWN),
-    d_which(TYPE_NONE),
-    d_unknownExplanation(UNKNOWN_REASON),
-    d_inputName("") {
-  }
-  Result(enum Sat s, std::string inputName = "") :
-    d_sat(s),
-    d_validity(VALIDITY_UNKNOWN),
-    d_which(TYPE_SAT),
-    d_unknownExplanation(UNKNOWN_REASON),
-    d_inputName(inputName) {
-    CheckArgument(s != SAT_UNKNOWN,
-                  "Must provide a reason for satisfiability being unknown");
-  }
-  Result(enum Validity v, std::string inputName = "") :
-    d_sat(SAT_UNKNOWN),
-    d_validity(v),
-    d_which(TYPE_VALIDITY),
-    d_unknownExplanation(UNKNOWN_REASON),
-    d_inputName(inputName) {
-    CheckArgument(v != VALIDITY_UNKNOWN,
-                  "Must provide a reason for validity being unknown");
-  }
-  Result(enum Sat s, enum UnknownExplanation unknownExplanation, std::string inputName = "") :
-    d_sat(s),
-    d_validity(VALIDITY_UNKNOWN),
-    d_which(TYPE_SAT),
-    d_unknownExplanation(unknownExplanation),
-    d_inputName(inputName) {
-    CheckArgument(s == SAT_UNKNOWN,
-                  "improper use of unknown-result constructor");
-  }
-  Result(enum Validity v, enum UnknownExplanation unknownExplanation, std::string inputName = "") :
-    d_sat(SAT_UNKNOWN),
-    d_validity(v),
-    d_which(TYPE_VALIDITY),
-    d_unknownExplanation(unknownExplanation),
-    d_inputName(inputName) {
-    CheckArgument(v == VALIDITY_UNKNOWN,
-                  "improper use of unknown-result constructor");
-  }
+
+  Result();
+
+  Result(enum Sat s, std::string inputName = "");
+
+  Result(enum Validity v, std::string inputName = "");
+
+  Result(enum Sat s,
+         enum UnknownExplanation unknownExplanation,
+         std::string inputName = "");
+
+  Result(enum Validity v, enum UnknownExplanation unknownExplanation,
+         std::string inputName = "");
+
   Result(const std::string& s, std::string inputName = "");
 
   Result(const Result& r, std::string inputName) {
@@ -128,24 +99,24 @@ public:
   enum Sat isSat() const {
     return d_which == TYPE_SAT ? d_sat : SAT_UNKNOWN;
   }
+
   enum Validity isValid() const {
     return d_which == TYPE_VALIDITY ? d_validity : VALIDITY_UNKNOWN;
   }
+
   bool isUnknown() const {
     return isSat() == SAT_UNKNOWN && isValid() == VALIDITY_UNKNOWN;
   }
+
   Type getType() const {
     return d_which;
   }
+
   bool isNull() const {
     return d_which == TYPE_NONE;
   }
-  enum UnknownExplanation whyUnknown() const {
-    CheckArgument( isUnknown(), this,
-                   "This result is not unknown, so the reason for "
-                   "being unknown cannot be inquired of it" );
-    return d_unknownExplanation;
-  }
+
+  enum UnknownExplanation whyUnknown() const;
 
   bool operator==(const Result& r) const throw();
   inline bool operator!=(const Result& r) const throw();
diff --git a/src/expr/sexpr.cpp b/src/expr/sexpr.cpp
index 0c0828616..69741859f 100644
--- a/src/expr/sexpr.cpp
+++ b/src/expr/sexpr.cpp
@@ -311,7 +311,7 @@ bool SExpr::languageQuotesKeywords(OutputLanguage language) {
 
 
 std::string SExpr::getValue() const {
-  CheckArgument( isAtom(), this );
+  PrettyCheckArgument( isAtom(), this );
   switch(d_sexprType) {
   case SEXPR_INTEGER:
     return d_integerValue.toString();
@@ -335,17 +335,17 @@ std::string SExpr::getValue() const {
 }
 
 const CVC4::Integer& SExpr::getIntegerValue() const {
-  CheckArgument( isInteger(), this );
+  PrettyCheckArgument( isInteger(), this );
   return d_integerValue;
 }
 
 const CVC4::Rational& SExpr::getRationalValue() const {
-  CheckArgument( isRational(), this );
+  PrettyCheckArgument( isRational(), this );
   return d_rationalValue;
 }
 
 const std::vector<SExpr>& SExpr::getChildren() const {
-  CheckArgument( !isAtom(), this );
+  PrettyCheckArgument( !isAtom(), this );
   Assert( d_children != NULL );
   return *d_children;
 }
diff --git a/src/expr/statistics_registry.cpp b/src/expr/statistics_registry.cpp
index c1db992c5..bf36236f7 100644
--- a/src/expr/statistics_registry.cpp
+++ b/src/expr/statistics_registry.cpp
@@ -17,6 +17,7 @@
 
 #include "expr/statistics_registry.h"
 
+#include "base/cvc4_assert.h"
 #include "expr/expr_manager.h"
 #include "lib/clock_gettime.h"
 #include "smt/smt_engine.h"
@@ -36,6 +37,19 @@
 
 namespace CVC4 {
 
+/** Construct a statistics registry */
+StatisticsRegistry::StatisticsRegistry(const std::string& name)
+  throw(CVC4::IllegalArgumentException) :
+  Stat(name) {
+
+  d_prefix = name;
+  if(__CVC4_USE_STATISTICS) {
+    PrettyCheckArgument(d_name.find(s_regDelim) == std::string::npos, name,
+                        "StatisticsRegistry names cannot contain the string \"%s\"",
+                    s_regDelim.c_str());
+  }
+}
+
 namespace stats {
 
 // This is a friend of SmtEngine, just to reach in and get it.
@@ -60,9 +74,9 @@ StatisticsRegistry* StatisticsRegistry::current() {
 void StatisticsRegistry::registerStat(Stat* s) throw(CVC4::IllegalArgumentException) {
 #ifdef CVC4_STATISTICS_ON
   StatSet& stats = current()->d_stats;
-  CheckArgument(stats.find(s) == stats.end(), s,
-                "Statistic `%s' was already registered with this registry.",
-                s->getName().c_str());
+  PrettyCheckArgument(stats.find(s) == stats.end(), s,
+                      "Statistic `%s' was already registered with this registry.",
+                      s->getName().c_str());
   stats.insert(s);
 #endif /* CVC4_STATISTICS_ON */
 }/* StatisticsRegistry::registerStat() */
@@ -70,7 +84,7 @@ void StatisticsRegistry::registerStat(Stat* s) throw(CVC4::IllegalArgumentExcept
 void StatisticsRegistry::unregisterStat(Stat* s) throw(CVC4::IllegalArgumentException) {
 #ifdef CVC4_STATISTICS_ON
   StatSet& stats = current()->d_stats;
-  CheckArgument(stats.find(s) != stats.end(), s,
+  PrettyCheckArgument(stats.find(s) != stats.end(), s,
                 "Statistic `%s' was not registered with this registry.",
                 s->getName().c_str());
   stats.erase(s);
@@ -81,14 +95,14 @@ void StatisticsRegistry::unregisterStat(Stat* s) throw(CVC4::IllegalArgumentExce
 
 void StatisticsRegistry::registerStat_(Stat* s) throw(CVC4::IllegalArgumentException) {
 #ifdef CVC4_STATISTICS_ON
-  CheckArgument(d_stats.find(s) == d_stats.end(), s);
+  PrettyCheckArgument(d_stats.find(s) == d_stats.end(), s);
   d_stats.insert(s);
 #endif /* CVC4_STATISTICS_ON */
 }/* StatisticsRegistry::registerStat_() */
 
 void StatisticsRegistry::unregisterStat_(Stat* s) throw(CVC4::IllegalArgumentException) {
 #ifdef CVC4_STATISTICS_ON
-  CheckArgument(d_stats.find(s) != d_stats.end(), s);
+  PrettyCheckArgument(d_stats.find(s) != d_stats.end(), s);
   d_stats.erase(s);
 #endif /* CVC4_STATISTICS_ON */
 }/* StatisticsRegistry::unregisterStat_() */
@@ -107,7 +121,7 @@ void StatisticsRegistry::flushInformation(std::ostream &out) const {
 
 void TimerStat::start() {
   if(__CVC4_USE_STATISTICS) {
-    CheckArgument(!d_running, *this, "timer already running");
+    PrettyCheckArgument(!d_running, *this, "timer already running");
     clock_gettime(CLOCK_MONOTONIC, &d_start);
     d_running = true;
   }
@@ -115,7 +129,7 @@ void TimerStat::start() {
 
 void TimerStat::stop() {
   if(__CVC4_USE_STATISTICS) {
-    CheckArgument(d_running, *this, "timer not running");
+    PrettyCheckArgument(d_running, *this, "timer not running");
     ::timespec end;
     clock_gettime(CLOCK_MONOTONIC, &end);
     d_data += end - d_start;
diff --git a/src/expr/statistics_registry.h b/src/expr/statistics_registry.h
index 89efe4021..4793f1301 100644
--- a/src/expr/statistics_registry.h
+++ b/src/expr/statistics_registry.h
@@ -607,15 +607,7 @@ public:
 
   /** Construct a statistics registry */
   StatisticsRegistry(const std::string& name)
-      throw(CVC4::IllegalArgumentException) :
-    Stat(name) {
-    d_prefix = name;
-    if(__CVC4_USE_STATISTICS) {
-      CheckArgument(d_name.find(s_regDelim) == std::string::npos, name,
-                    "StatisticsRegistry names cannot contain the string \"%s\"",
-                    s_regDelim.c_str());
-    }
-  }
+    throw(CVC4::IllegalArgumentException);
 
   /**
    * Set the name of this statistic registry, used as prefix during
diff --git a/src/expr/symbol_table.cpp b/src/expr/symbol_table.cpp
index 3d53f2e44..c0a80b7ce 100644
--- a/src/expr/symbol_table.cpp
+++ b/src/expr/symbol_table.cpp
@@ -17,17 +17,18 @@
  **/
 
 #include "expr/symbol_table.h"
-#include "expr/expr.h"
-#include "expr/type.h"
-#include "expr/expr_manager_scope.h"
+
+#include <string>
+#include <utility>
+
 #include "context/cdhashmap.h"
 #include "context/cdhashset.h"
 #include "context/context.h"
+#include "expr/expr.h"
+#include "expr/expr_manager_scope.h"
+#include "expr/type.h"
 
-#include <string>
-#include <utility>
 
-using namespace CVC4;
 using namespace CVC4::context;
 using namespace std;
 
@@ -49,7 +50,7 @@ SymbolTable::~SymbolTable() {
 
 void SymbolTable::bind(const std::string& name, Expr obj,
                        bool levelZero) throw() {
-  CheckArgument(!obj.isNull(), obj, "cannot bind to a null Expr");
+  PrettyCheckArgument(!obj.isNull(), obj, "cannot bind to a null Expr");
   ExprManagerScope ems(obj);
   if(levelZero) d_exprMap->insertAtContextLevelZero(name, obj);
   else d_exprMap->insert(name, obj);
@@ -57,7 +58,7 @@ void SymbolTable::bind(const std::string& name, Expr obj,
 
 void SymbolTable::bindDefinedFunction(const std::string& name, Expr obj,
                                       bool levelZero) throw() {
-  CheckArgument(!obj.isNull(), obj, "cannot bind to a null Expr");
+  PrettyCheckArgument(!obj.isNull(), obj, "cannot bind to a null Expr");
   ExprManagerScope ems(obj);
   if(levelZero){
     d_exprMap->insertAtContextLevelZero(name, obj);
@@ -121,7 +122,7 @@ bool SymbolTable::isBoundType(const std::string& name) const throw() {
 
 Type SymbolTable::lookupType(const std::string& name) const throw() {
   pair<vector<Type>, Type> p = (*d_typeMap->find(name)).second;
-  CheckArgument(p.first.size() == 0, name,
+  PrettyCheckArgument(p.first.size() == 0, name,
                 "type constructor arity is wrong: "
                 "`%s' requires %u parameters but was provided 0",
                 name.c_str(), p.first.size());
@@ -131,12 +132,12 @@ Type SymbolTable::lookupType(const std::string& name) const throw() {
 Type SymbolTable::lookupType(const std::string& name,
                              const std::vector<Type>& params) const throw() {
   pair<vector<Type>, Type> p = (*d_typeMap->find(name)).second;
-  CheckArgument(p.first.size() == params.size(), params,
+  PrettyCheckArgument(p.first.size() == params.size(), params,
                 "type constructor arity is wrong: "
                 "`%s' requires %u parameters but was provided %u",
          name.c_str(), p.first.size(), params.size());
   if(p.first.size() == 0) {
-    CheckArgument(p.second.isSort(), name);
+    PrettyCheckArgument(p.second.isSort(), name.c_str());
     return p.second;
   }
   if(p.second.isSortConstructor()) {
@@ -161,7 +162,7 @@ Type SymbolTable::lookupType(const std::string& name,
 
     return instantiation;
   } else if(p.second.isDatatype()) {
-    CheckArgument(DatatypeType(p.second).isParametric(), name, "expected parametric datatype");
+    PrettyCheckArgument(DatatypeType(p.second).isParametric(), name, "expected parametric datatype");
     return DatatypeType(p.second).instantiate(params);
   } else {
     if(Debug.isOn("sort")) {
diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index 327be72eb..99d04d658 100644
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -92,8 +92,8 @@ Type Type::getBaseType() const {
 }
 
 Type& Type::operator=(const Type& t) {
-  CheckArgument(d_typeNode != NULL, this, "Unexpected NULL typenode pointer!");
-  CheckArgument(t.d_typeNode != NULL, t, "Unexpected NULL typenode pointer!");
+  PrettyCheckArgument(d_typeNode != NULL, this, "Unexpected NULL typenode pointer!");
+  PrettyCheckArgument(t.d_typeNode != NULL, t, "Unexpected NULL typenode pointer!");
 
   if(this != &t) {
     if(d_nodeManager == t.d_nodeManager) {
@@ -354,7 +354,7 @@ vector<Type> FunctionType::getArgTypes() const {
 
 Type FunctionType::getRangeType() const {
   NodeManagerScope nms(d_nodeManager);
-  CheckArgument(isNull() || isFunction(), this);
+  PrettyCheckArgument(isNull() || isFunction(), this);
   return makeType(d_typeNode->getRangeType());
 }
 
@@ -430,112 +430,112 @@ SortType SortConstructorType::instantiate(const std::vector<Type>& params) const
 
 BooleanType::BooleanType(const Type& t) throw(IllegalArgumentException) :
   Type(t) {
-  CheckArgument(isNull() || isBoolean(), this);
+  PrettyCheckArgument(isNull() || isBoolean(), this);
 }
 
 IntegerType::IntegerType(const Type& t) throw(IllegalArgumentException) :
   Type(t) {
-  CheckArgument(isNull() || isInteger(), this);
+  PrettyCheckArgument(isNull() || isInteger(), this);
 }
 
 RealType::RealType(const Type& t) throw(IllegalArgumentException) :
   Type(t) {
-  CheckArgument(isNull() || isReal(), this);
+  PrettyCheckArgument(isNull() || isReal(), this);
 }
 
 StringType::StringType(const Type& t) throw(IllegalArgumentException) :
   Type(t) {
-  CheckArgument(isNull() || isString(), this);
+  PrettyCheckArgument(isNull() || isString(), this);
 }
 
 RoundingModeType::RoundingModeType(const Type& t) throw(IllegalArgumentException) :
   Type(t) {
-  CheckArgument(isNull() || isRoundingMode(), this);
+  PrettyCheckArgument(isNull() || isRoundingMode(), this);
 }
 
 BitVectorType::BitVectorType(const Type& t) throw(IllegalArgumentException) :
   Type(t) {
-  CheckArgument(isNull() || isBitVector(), this);
+  PrettyCheckArgument(isNull() || isBitVector(), this);
 }
 
 FloatingPointType::FloatingPointType(const Type& t) throw(IllegalArgumentException) :
   Type(t) {
-  CheckArgument(isNull() || isFloatingPoint(), this);
+  PrettyCheckArgument(isNull() || isFloatingPoint(), this);
 }
 
 DatatypeType::DatatypeType(const Type& t) throw(IllegalArgumentException) :
   Type(t) {
-  CheckArgument(isNull() || isDatatype(), this);
+  PrettyCheckArgument(isNull() || isDatatype(), this);
 }
 
 ConstructorType::ConstructorType(const Type& t) throw(IllegalArgumentException) :
   Type(t) {
-  CheckArgument(isNull() || isConstructor(), this);
+  PrettyCheckArgument(isNull() || isConstructor(), this);
 }
 
 SelectorType::SelectorType(const Type& t) throw(IllegalArgumentException) :
   Type(t) {
-  CheckArgument(isNull() || isSelector(), this);
+  PrettyCheckArgument(isNull() || isSelector(), this);
 }
 
-TesterType::TesterType(const Type& t) throw(IllegalArgumentException) :
-  Type(t) {
-  CheckArgument(isNull() || isTester(), this);
+TesterType::TesterType(const Type& t) throw(IllegalArgumentException)
+    : Type(t) {
+  PrettyCheckArgument(isNull() || isTester(), this);
 }
 
-FunctionType::FunctionType(const Type& t) throw(IllegalArgumentException) :
-  Type(t) {
-  CheckArgument(isNull() || isFunction(), this);
+FunctionType::FunctionType(const Type& t) throw(IllegalArgumentException)
+    : Type(t) {
+  PrettyCheckArgument(isNull() || isFunction(), this);
 }
 
-TupleType::TupleType(const Type& t) throw(IllegalArgumentException) :
-  Type(t) {
-  CheckArgument(isNull() || isTuple(), this);
+TupleType::TupleType(const Type& t) throw(IllegalArgumentException)
+    : Type(t) {
+  PrettyCheckArgument(isNull() || isTuple(), this);
 }
 
-RecordType::RecordType(const Type& t) throw(IllegalArgumentException) :
-  Type(t) {
-  CheckArgument(isNull() || isRecord(), this);
+RecordType::RecordType(const Type& t) throw(IllegalArgumentException)
+    : Type(t) {
+  PrettyCheckArgument(isNull() || isRecord(), this);
 }
 
-SExprType::SExprType(const Type& t) throw(IllegalArgumentException) :
-  Type(t) {
-  CheckArgument(isNull() || isSExpr(), this);
+SExprType::SExprType(const Type& t) throw(IllegalArgumentException)
+    : Type(t) {
+  PrettyCheckArgument(isNull() || isSExpr(), this);
 }
 
-ArrayType::ArrayType(const Type& t) throw(IllegalArgumentException) :
-  Type(t) {
-  CheckArgument(isNull() || isArray(), this);
+ArrayType::ArrayType(const Type& t) throw(IllegalArgumentException)
+    : Type(t) {
+  PrettyCheckArgument(isNull() || isArray(), this);
 }
 
-SetType::SetType(const Type& t) throw(IllegalArgumentException) :
-  Type(t) {
-  CheckArgument(isNull() || isSet(), this);
+SetType::SetType(const Type& t) throw(IllegalArgumentException)
+    : Type(t) {
+  PrettyCheckArgument(isNull() || isSet(), this);
 }
 
-SortType::SortType(const Type& t) throw(IllegalArgumentException) :
-  Type(t) {
-  CheckArgument(isNull() || isSort(), this);
+SortType::SortType(const Type& t) throw(IllegalArgumentException)
+    : Type(t) {
+  PrettyCheckArgument(isNull() || isSort(), this);
 }
 
 SortConstructorType::SortConstructorType(const Type& t)
-  throw(IllegalArgumentException) :
-  Type(t) {
-  CheckArgument(isNull() || isSortConstructor(), this);
+  throw(IllegalArgumentException)
+    : Type(t) {
+  PrettyCheckArgument(isNull() || isSortConstructor(), this);
 }
 
 /* - not in release 1.0
 PredicateSubtype::PredicateSubtype(const Type& t)
   throw(IllegalArgumentException) :
   Type(t) {
-  CheckArgument(isNull() || isPredicateSubtype(), this);
+  PrettyCheckArgument(isNull() || isPredicateSubtype(), this);
 }
 */
 
 SubrangeType::SubrangeType(const Type& t)
   throw(IllegalArgumentException) :
   Type(t) {
-  CheckArgument(isNull() || isSubrange(), this);
+  PrettyCheckArgument(isNull() || isSubrange(), this);
 }
 
 unsigned BitVectorType::getSize() const {
@@ -585,7 +585,7 @@ std::vector<Type> ConstructorType::getArgTypes() const {
 const Datatype& DatatypeType::getDatatype() const {
   NodeManagerScope nms(d_nodeManager);
   if( d_typeNode->isParametricDatatype() ) {
-    CheckArgument( (*d_typeNode)[0].getKind() == kind::DATATYPE_TYPE, this);
+    PrettyCheckArgument( (*d_typeNode)[0].getKind() == kind::DATATYPE_TYPE, this);
     const Datatype& dt = (*d_typeNode)[0].getConst<Datatype>();
     return dt;
   } else {
diff --git a/src/expr/uninterpreted_constant.cpp b/src/expr/uninterpreted_constant.cpp
index d41ab1045..97bc3ae4b 100644
--- a/src/expr/uninterpreted_constant.cpp
+++ b/src/expr/uninterpreted_constant.cpp
@@ -20,10 +20,20 @@
 #include <sstream>
 #include <string>
 
+#include "base/cvc4_assert.h"
+
 using namespace std;
 
 namespace CVC4 {
 
+UninterpretedConstant::UninterpretedConstant(Type type, Integer index) throw(IllegalArgumentException)
+    : d_type(type)
+    , d_index(index)
+{
+  //PrettyCheckArgument(type.isSort(), type, "uninterpreted constants can only be created for uninterpreted sorts, not `%s'", type.toString().c_str());
+  PrettyCheckArgument(index >= 0, index, "index >= 0 required for uninterpreted constant index, not `%s'", index.toString().c_str());
+}
+
 std::ostream& operator<<(std::ostream& out, const UninterpretedConstant& uc) {
   stringstream ss;
   ss << uc.getType();
diff --git a/src/expr/uninterpreted_constant.h b/src/expr/uninterpreted_constant.h
index 13a80a19d..5b2293df6 100644
--- a/src/expr/uninterpreted_constant.h
+++ b/src/expr/uninterpreted_constant.h
@@ -18,26 +18,18 @@
 
 #pragma once
 
+#include <iosfwd>
+
 #include "expr/type.h"
-#include <iostream>
 
 namespace CVC4 {
 
 class CVC4_PUBLIC UninterpretedConstant {
-  const Type d_type;
-  const Integer d_index;
-
 public:
 
-  UninterpretedConstant(Type type, Integer index) throw(IllegalArgumentException) :
-    d_type(type),
-    d_index(index) {
-    //CheckArgument(type.isSort(), type, "uninterpreted constants can only be created for uninterpreted sorts, not `%s'", type.toString().c_str());
-    CheckArgument(index >= 0, index, "index >= 0 required for uninterpreted constant index, not `%s'", index.toString().c_str());
-  }
+  UninterpretedConstant(Type type, Integer index) throw(IllegalArgumentException);
 
-  ~UninterpretedConstant() throw() {
-  }
+  ~UninterpretedConstant() throw() { }
 
   Type getType() const throw() {
     return d_type;
@@ -68,6 +60,9 @@ public:
     return !(*this < uc);
   }
 
+private:
+  const Type d_type;
+  const Integer d_index;
 };/* class UninterpretedConstant */
 
 std::ostream& operator<<(std::ostream& out, const UninterpretedConstant& uc) CVC4_PUBLIC;
diff --git a/src/main/command_executor.h b/src/main/command_executor.h
index 49d18a153..8ef1a6a5f 100644
--- a/src/main/command_executor.h
+++ b/src/main/command_executor.h
@@ -15,7 +15,7 @@
 #ifndef __CVC4__MAIN__COMMAND_EXECUTOR_H
 #define __CVC4__MAIN__COMMAND_EXECUTOR_H
 
-#include <iostream>
+#include <iosfwd>
 #include <string>
 
 #include "expr/expr_manager.h"
diff --git a/src/main/command_executor_portfolio.h b/src/main/command_executor_portfolio.h
index b3532cea4..ee2b270fb 100644
--- a/src/main/command_executor_portfolio.h
+++ b/src/main/command_executor_portfolio.h
@@ -21,10 +21,10 @@
 #include "main/command_executor.h"
 #include "main/portfolio_util.h"
 
-#include <vector>
-#include <string>
-#include <iostream>
+#include <iosfwd>
 #include <sstream>
+#include <string>
+#include <vector>
 
 namespace CVC4 {
 
diff --git a/src/main/interactive_shell.h b/src/main/interactive_shell.h
index 1b1031776..844fddf45 100644
--- a/src/main/interactive_shell.h
+++ b/src/main/interactive_shell.h
@@ -15,7 +15,7 @@
 #ifndef __CVC4__INTERACTIVE_SHELL_H
 #define __CVC4__INTERACTIVE_SHELL_H
 
-#include <iostream>
+#include <iosfwd>
 #include <string>
 
 #include "options/language.h"
diff --git a/src/options/base_options b/src/options/base_options
index 588220817..edbef801d 100644
--- a/src/options/base_options
+++ b/src/options/base_options
@@ -81,9 +81,9 @@ module BASE "options/base_options.h" Base
 
 option binary_name std::string
 
-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>
+option in std::istream* :default &std::cin :include <iosfwd>
+option out std::ostream* :default &std::cout :include <iosfwd>
+option err std::ostream* :default &std::cerr :include <iosfwd>
 
 common-option inputLanguage input-language -L --lang=LANG InputLanguage :handler CVC4::options::stringToInputLanguage :include "options/language.h" :default language::input::LANG_AUTO :read-write
  force input language (default is "auto"; see --lang help)
diff --git a/src/options/boolean_term_conversion_mode.cpp b/src/options/boolean_term_conversion_mode.cpp
index efeb3ab16..d1466ae14 100644
--- a/src/options/boolean_term_conversion_mode.cpp
+++ b/src/options/boolean_term_conversion_mode.cpp
@@ -18,7 +18,6 @@
 
 #include <iostream>
 
-
 namespace CVC4 {
 
 std::ostream& operator<<(std::ostream& out, theory::booleans::BooleanTermConversionMode mode) {
diff --git a/src/options/boolean_term_conversion_mode.h b/src/options/boolean_term_conversion_mode.h
index 5671dea13..65cc7a8a5 100644
--- a/src/options/boolean_term_conversion_mode.h
+++ b/src/options/boolean_term_conversion_mode.h
@@ -20,7 +20,7 @@
 #ifndef __CVC4__THEORY__BOOLEANS__BOOLEAN_TERM_CONVERSION_MODE_H
 #define __CVC4__THEORY__BOOLEANS__BOOLEAN_TERM_CONVERSION_MODE_H
 
-#include <iostream>
+#include <iosfwd>
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/options/bv_bitblast_mode.cpp b/src/options/bv_bitblast_mode.cpp
index 9576134f6..99ceb41ee 100644
--- a/src/options/bv_bitblast_mode.cpp
+++ b/src/options/bv_bitblast_mode.cpp
@@ -16,6 +16,8 @@
 
 #include "options/bv_bitblast_mode.h"
 
+#include <iostream>
+
 namespace CVC4 {
 
 std::ostream& operator<<(std::ostream& out, theory::bv::BitblastMode mode) {
diff --git a/src/options/bv_bitblast_mode.h b/src/options/bv_bitblast_mode.h
index 89ecdc381..08a6e4077 100644
--- a/src/options/bv_bitblast_mode.h
+++ b/src/options/bv_bitblast_mode.h
@@ -19,7 +19,7 @@
 #ifndef __CVC4__THEORY__BV__BITBLAST_MODE_H
 #define __CVC4__THEORY__BV__BITBLAST_MODE_H
 
-#include <iostream>
+#include <iosfwd>
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/options/options_handler_interface.cpp b/src/options/options_handler_interface.cpp
index d803fced0..bce3643aa 100644
--- a/src/options/options_handler_interface.cpp
+++ b/src/options/options_handler_interface.cpp
@@ -44,313 +44,313 @@ static const char* s_third_argument_warning =
 
 // theory/arith/options_handlers.h
 ArithUnateLemmaMode stringToArithUnateLemmaMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) {
-  CheckArgument(handler != NULL, handler, s_third_argument_warning);
+  PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
   return handler->stringToArithUnateLemmaMode(option, optarg);
 }
 ArithPropagationMode stringToArithPropagationMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) {
-  CheckArgument(handler != NULL, handler, s_third_argument_warning);
+  PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
   return handler->stringToArithPropagationMode(option, optarg);
 }
 ErrorSelectionRule stringToErrorSelectionRule(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) {
-  CheckArgument(handler != NULL, handler, s_third_argument_warning);
+  PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
   return handler->stringToErrorSelectionRule(option, optarg);
 }
 
 // theory/quantifiers/options_handlers.h
 theory::quantifiers::InstWhenMode stringToInstWhenMode(std::string option, std::string optarg,  OptionsHandler* handler) throw(OptionException) {
-  CheckArgument(handler != NULL, handler, s_third_argument_warning);
+  PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
   return handler->stringToInstWhenMode(option, optarg);
 }
 void checkInstWhenMode(std::string option, theory::quantifiers::InstWhenMode mode,  OptionsHandler* handler) throw(OptionException) {
-  CheckArgument(handler != NULL, handler, s_third_argument_warning);
+  PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
   handler->checkInstWhenMode(option, mode);
 }
 theory::quantifiers::LiteralMatchMode stringToLiteralMatchMode(std::string option, std::string optarg,  OptionsHandler* handler) throw(OptionException) {
-  CheckArgument(handler != NULL, handler, s_third_argument_warning);
+  PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
   return handler->stringToLiteralMatchMode(option, optarg);
 }
 void checkLiteralMatchMode(std::string option, theory::quantifiers::LiteralMatchMode mode,  OptionsHandler* handler) throw(OptionException) {
-  CheckArgument(handler != NULL, handler, s_third_argument_warning);
+  PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
   handler->checkLiteralMatchMode(option, mode);
 }
 theory::quantifiers::MbqiMode stringToMbqiMode(std::string option, std::string optarg,  OptionsHandler* handler) throw(OptionException) {
-  CheckArgument(handler != NULL, handler, s_third_argument_warning);
+  PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
   return handler->stringToMbqiMode(option, optarg);
 }
 void checkMbqiMode(std::string option, theory::quantifiers::MbqiMode mode,  OptionsHandler* handler) throw(OptionException) {
-  CheckArgument(handler != NULL, handler, s_third_argument_warning);
+  PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
   handler->checkMbqiMode(option, mode);
 }
 theory::quantifiers::QcfWhenMode stringToQcfWhenMode(std::string option, std::string optarg,  OptionsHandler* handler) throw(OptionException) {
-  CheckArgument(handler != NULL, handler, s_third_argument_warning);
+  PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
   return handler->stringToQcfWhenMode(option, optarg);
 }
 theory::quantifiers::QcfMode stringToQcfMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) {
-  CheckArgument(handler != NULL, handler, s_third_argument_warning);
+  PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
   return handler->stringToQcfMode(option, optarg);
 }
 theory::quantifiers::UserPatMode stringToUserPatMode(std::string option, std::string optarg,  OptionsHandler* handler) throw(OptionException) {
-  CheckArgument(handler != NULL, handler, s_third_argument_warning);
+  PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
   return handler->stringToUserPatMode(option, optarg);
 }
 theory::quantifiers::TriggerSelMode stringToTriggerSelMode(std::string option, std::string optarg,  OptionsHandler* handler) throw(OptionException) {
-  CheckArgument(handler != NULL, handler, s_third_argument_warning);
+  PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
   return handler->stringToTriggerSelMode(option, optarg);
 }
 theory::quantifiers::PrenexQuantMode stringToPrenexQuantMode(std::string option, std::string optarg,  OptionsHandler* handler) throw(OptionException) {
-  CheckArgument(handler != NULL, handler, s_third_argument_warning);
+  PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
   return handler->stringToPrenexQuantMode(option, optarg);
 }
 theory::quantifiers::CegqiFairMode stringToCegqiFairMode(std::string option, std::string optarg,  OptionsHandler* handler) throw(OptionException) {
-  CheckArgument(handler != NULL, handler, s_third_argument_warning);
+  PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
   return handler->stringToCegqiFairMode(option, optarg);
 }
 theory::quantifiers::TermDbMode stringToTermDbMode(std::string option, std::string optarg,  OptionsHandler* handler) throw(OptionException) {
-  CheckArgument(handler != NULL, handler, s_third_argument_warning);
+  PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
   return handler-> stringToTermDbMode(option, optarg);
 }
 theory::quantifiers::IteLiftQuantMode stringToIteLiftQuantMode(std::string option, std::string optarg,  OptionsHandler* handler) throw(OptionException) {
-  CheckArgument(handler != NULL, handler, s_third_argument_warning);
+  PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
   return handler->stringToIteLiftQuantMode(option, optarg);
 }
 theory::quantifiers::SygusInvTemplMode stringToSygusInvTemplMode(std::string option, std::string optarg,  OptionsHandler* handler) throw(OptionException) {
-  CheckArgument(handler != NULL, handler, s_third_argument_warning);
+  PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
   return handler->stringToSygusInvTemplMode(option, optarg);
 }
 theory::quantifiers::MacrosQuantMode stringToMacrosQuantMode(std::string option, std::string optarg,  OptionsHandler* handler) throw(OptionException) {
-  CheckArgument(handler != NULL, handler, s_third_argument_warning);
+  PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
   return handler->stringToMacrosQuantMode(option, optarg);
 }
 
 
 // theory/bv/options_handlers.h
 void abcEnabledBuild(std::string option, bool value, OptionsHandler* handler) throw(OptionException) {
-  CheckArgument(handler != NULL, handler, s_third_argument_warning);
+  PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
   handler->abcEnabledBuild(option, value);
 }
 void abcEnabledBuild(std::string option, std::string value, OptionsHandler* handler) throw(OptionException) {
-  CheckArgument(handler != NULL, handler, s_third_argument_warning);
+  PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
   handler->abcEnabledBuild(option, value);
 }
 theory::bv::BitblastMode stringToBitblastMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) {
-  CheckArgument(handler != NULL, handler, s_third_argument_warning);
+  PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
   return handler->stringToBitblastMode(option, optarg);
 }
 theory::bv::BvSlicerMode stringToBvSlicerMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) {
-  CheckArgument(handler != NULL, handler, s_third_argument_warning);
+  PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
   return handler->stringToBvSlicerMode(option, optarg);
 }
 void setBitblastAig(std::string option, bool arg, OptionsHandler* handler) throw(OptionException) {
-  CheckArgument(handler != NULL, handler, s_third_argument_warning);
+  PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
   handler->setBitblastAig(option, arg);
 }
 
 
 // theory/booleans/options_handlers.h
 theory::booleans::BooleanTermConversionMode stringToBooleanTermConversionMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) {
-  CheckArgument(handler != NULL, handler, s_third_argument_warning);
+  PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
   return handler->stringToBooleanTermConversionMode( option, optarg);
 }
 
 // theory/uf/options_handlers.h
 theory::uf::UfssMode stringToUfssMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) {
-  CheckArgument(handler != NULL, handler, s_third_argument_warning);
+  PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
   return handler->stringToUfssMode(option, optarg);
 }
 
 // theory/options_handlers.h
 theory::TheoryOfMode stringToTheoryOfMode(std::string option, std::string optarg, OptionsHandler* handler) {
-  CheckArgument(handler != NULL, handler, s_third_argument_warning);
+  PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
   return handler->stringToTheoryOfMode(option, optarg);
 }
 void useTheory(std::string option, std::string optarg, OptionsHandler* handler) {
-  CheckArgument(handler != NULL, handler, s_third_argument_warning);
+  PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
   return handler->useTheory(option, optarg);
 }
 
 // printer/options_handlers.h
 ModelFormatMode stringToModelFormatMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) {
-  CheckArgument(handler != NULL, handler, s_third_argument_warning);
+  PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
   return handler->stringToModelFormatMode(option, optarg);
 }
 
 InstFormatMode stringToInstFormatMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) {
-  CheckArgument(handler != NULL, handler, s_third_argument_warning);
+  PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
   return handler->stringToInstFormatMode(option, optarg);
 }
 
 
 // decision/options_handlers.h
 decision::DecisionMode stringToDecisionMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) {
-  CheckArgument(handler != NULL, handler, s_third_argument_warning);
+  PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
   return handler->stringToDecisionMode(option, optarg);
 }
 
 decision::DecisionWeightInternal stringToDecisionWeightInternal(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) {
-  CheckArgument(handler != NULL, handler, s_third_argument_warning);
+  PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
   return handler->stringToDecisionWeightInternal(option, optarg);
 }
 
 
 /* options/base_options_handlers.h */
 void setVerbosity(std::string option, int value, OptionsHandler* handler) throw(OptionException) {
-  CheckArgument(handler != NULL, handler, s_third_argument_warning);
+  PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
   handler->setVerbosity(option, value);
 }
 void increaseVerbosity(std::string option, OptionsHandler* handler) {
-  CheckArgument(handler != NULL, handler, s_third_argument_warning);
+  PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
   handler->increaseVerbosity(option);
 }
 void decreaseVerbosity(std::string option, OptionsHandler* handler) {
-  CheckArgument(handler != NULL, handler, s_third_argument_warning);
+  PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
   handler->decreaseVerbosity(option);
 }
 
 OutputLanguage stringToOutputLanguage(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) {
-  CheckArgument(handler != NULL, handler, s_third_argument_warning);
+  PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
   return handler->stringToOutputLanguage(option, optarg);
 }
 
 InputLanguage stringToInputLanguage(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) {
-  CheckArgument(handler != NULL, handler, s_third_argument_warning);
+  PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
   return handler->stringToInputLanguage(option, optarg);
 }
 
 void addTraceTag(std::string option, std::string optarg, OptionsHandler* handler) {
-  CheckArgument(handler != NULL, handler, s_third_argument_warning);
+  PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
   handler->addTraceTag(option, optarg);
 }
 
 void addDebugTag(std::string option, std::string optarg, OptionsHandler* handler) {
-  CheckArgument(handler != NULL, handler, s_third_argument_warning);
+  PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
   handler->addDebugTag(option, optarg);
 }
 
 void setPrintSuccess(std::string option, bool value, OptionsHandler* handler) {
-  CheckArgument(handler != NULL, handler, s_third_argument_warning);
+  PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
   handler->setPrintSuccess(option, value);
 }
 
 
 /* main/options_handlers.h */
 void showConfiguration(std::string option, OptionsHandler* handler) {
-  CheckArgument(handler != NULL, handler, s_third_argument_warning);
+  PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
   handler->showConfiguration(option);
 }
 
 void showDebugTags(std::string option, OptionsHandler* handler) {
-  CheckArgument(handler != NULL, handler, s_third_argument_warning);
+  PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
   handler->showDebugTags(option);
 }
 
 void showTraceTags(std::string option, OptionsHandler* handler) {
-  CheckArgument(handler != NULL, handler, s_third_argument_warning);
+  PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
   handler->showTraceTags(option);
 }
 
 void threadN(std::string option, OptionsHandler* handler){
-  CheckArgument(handler != NULL, handler, s_third_argument_warning);
+  PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
   handler->threadN(option);
 }
 
 /* expr/options_handlers.h */
 void setDefaultExprDepth(std::string option, int depth, OptionsHandler* handler){
-  CheckArgument(handler != NULL, handler, s_third_argument_warning);
+  PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
   handler->setDefaultExprDepth(option, depth);
 }
 
 void setDefaultDagThresh(std::string option, int dag, OptionsHandler* handler){
-  CheckArgument(handler != NULL, handler, s_third_argument_warning);
+  PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
   handler->setDefaultDagThresh(option, dag);
 }
 
 void setPrintExprTypes(std::string option, OptionsHandler* handler) {
-  CheckArgument(handler != NULL, handler, s_third_argument_warning);
+  PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
   handler->setPrintExprTypes(option);
 }
 
 
 /* smt/options_handlers.h */
 void dumpMode(std::string option, std::string optarg, OptionsHandler* handler) {
-  CheckArgument(handler != NULL, handler, s_third_argument_warning);
+  PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
   handler->dumpMode(option, optarg);
 }
 
 LogicInfo* stringToLogicInfo(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException){
-  CheckArgument(handler != NULL, handler, s_third_argument_warning);
+  PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
   return handler->stringToLogicInfo(option, optarg);
 }
 
 SimplificationMode stringToSimplificationMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException){
-  CheckArgument(handler != NULL, handler, s_third_argument_warning);
+  PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
   return handler->stringToSimplificationMode(option, optarg);
 }
 
 // ensure we haven't started search yet
 void beforeSearch(std::string option, bool value, OptionsHandler* handler) throw(ModalException){
-  CheckArgument(handler != NULL, handler, s_third_argument_warning);
+  PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
   handler->beforeSearch(option, value);
 }
 
 void setProduceAssertions(std::string option, bool value, OptionsHandler* handler) throw() {
-  CheckArgument(handler != NULL, handler, s_third_argument_warning);
+  PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
   handler->setProduceAssertions(option, value);
 }
 
 // ensure we are a proof-enabled build of CVC4
 void proofEnabledBuild(std::string option, bool value, OptionsHandler* handler) throw(OptionException) {
-  CheckArgument(handler != NULL, handler, s_third_argument_warning);
+  PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
   handler->proofEnabledBuild(option, value);
 }
 
 void dumpToFile(std::string option, std::string optarg, OptionsHandler* handler) {
-  CheckArgument(handler != NULL, handler, s_third_argument_warning);
+  PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
   handler->dumpToFile(option, optarg);
 }
 
 void setRegularOutputChannel(std::string option, std::string optarg, OptionsHandler* handler) {
-  CheckArgument(handler != NULL, handler, s_third_argument_warning);
+  PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
   handler->setRegularOutputChannel(option, optarg);
 }
 
 void setDiagnosticOutputChannel(std::string option, std::string optarg, OptionsHandler* handler) {
-  CheckArgument(handler != NULL, handler, s_third_argument_warning);
+  PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
   handler->setDiagnosticOutputChannel(option, optarg);
 }
 
 std::string checkReplayFilename(std::string option, std::string optarg, OptionsHandler* handler) {
-  CheckArgument(handler != NULL, handler, s_third_argument_warning);
+  PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
   return handler->checkReplayFilename(option, optarg);
 }
 
 std::ostream* checkReplayLogFilename(std::string option, std::string optarg, OptionsHandler* handler) {
-  CheckArgument(handler != NULL, handler, s_third_argument_warning);
+  PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
   return handler->checkReplayLogFilename(option, optarg);
 }
 
 // ensure we are a stats-enabled build of CVC4
 void statsEnabledBuild(std::string option, bool value, OptionsHandler* handler) throw(OptionException) {
-  CheckArgument(handler != NULL, handler, s_third_argument_warning);
+  PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
   return handler->statsEnabledBuild(option, value);
 }
 
 unsigned long tlimitHandler(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) {
-  CheckArgument(handler != NULL, handler, s_third_argument_warning);
+  PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
   return handler->tlimitHandler(option, optarg);
 }
 
 unsigned long tlimitPerHandler(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) {
-  CheckArgument(handler != NULL, handler, s_third_argument_warning);
+  PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
   return handler-> tlimitPerHandler(option, optarg);
 }
 
 unsigned long rlimitHandler(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) {
-  CheckArgument(handler != NULL, handler, s_third_argument_warning);
+  PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
   return handler->rlimitHandler(option, optarg);
 }
 
 unsigned long rlimitPerHandler(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) {
-  CheckArgument(handler != NULL, handler, s_third_argument_warning);
+  PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
   return handler->rlimitPerHandler(option, optarg);
 }
 
diff --git a/src/options/simplification_mode.cpp b/src/options/simplification_mode.cpp
index 08f961c15..ab7851ef9 100644
--- a/src/options/simplification_mode.cpp
+++ b/src/options/simplification_mode.cpp
@@ -17,6 +17,8 @@
 
 #include "options/simplification_mode.h"
 
+#include <iostream>
+
 namespace CVC4 {
 
 std::ostream& operator<<(std::ostream& out, SimplificationMode mode) {
diff --git a/src/options/simplification_mode.h b/src/options/simplification_mode.h
index b0b78d318..dd02ada5c 100644
--- a/src/options/simplification_mode.h
+++ b/src/options/simplification_mode.h
@@ -20,7 +20,7 @@
 #ifndef __CVC4__SMT__SIMPLIFICATION_MODE_H
 #define __CVC4__SMT__SIMPLIFICATION_MODE_H
 
-#include <iostream>
+#include <iosfwd>
 
 namespace CVC4 {
 
diff --git a/src/proof/cnf_proof.h b/src/proof/cnf_proof.h
index c1d245716..d3e59ef93 100644
--- a/src/proof/cnf_proof.h
+++ b/src/proof/cnf_proof.h
@@ -16,16 +16,17 @@
  **
  **/
 
+#include "cvc4_private.h"
+
 #ifndef __CVC4__CNF_PROOF_H
 #define __CVC4__CNF_PROOF_H
 
-#include "cvc4_private.h"
-#include "util/proof.h"
-#include "proof/sat_proof.h"
-
-#include <ext/hash_set>
 #include <ext/hash_map>
-#include <iostream>
+#include <ext/hash_set>
+#include <iosfwd>
+
+#include "proof/sat_proof.h"
+#include "util/proof.h"
 
 namespace CVC4 {
 namespace prop {
diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h
index 4bab86745..6864eca3d 100644
--- a/src/proof/proof_manager.h
+++ b/src/proof/proof_manager.h
@@ -19,13 +19,14 @@
 #ifndef __CVC4__PROOF_MANAGER_H
 #define __CVC4__PROOF_MANAGER_H
 
-#include <iostream>
+#include <iosfwd>
 #include <map>
-#include "proof/proof.h"
-#include "util/proof.h"
+
 #include "expr/node.h"
+#include "proof/proof.h"
 #include "theory/logic_info.h"
 #include "theory/substitutions.h"
+#include "util/proof.h"
 
 
 namespace CVC4 {
diff --git a/src/proof/sat_proof.h b/src/proof/sat_proof.h
index a9793e784..52319431c 100644
--- a/src/proof/sat_proof.h
+++ b/src/proof/sat_proof.h
@@ -19,13 +19,15 @@
 #ifndef __CVC4__SAT__PROOF_H
 #define __CVC4__SAT__PROOF_H
 
-#include <iostream>
 #include <stdint.h>
-#include <vector>
-#include <set>
+
 #include <ext/hash_map>
 #include <ext/hash_set>
+#include <iosfwd>
+#include <set>
 #include <sstream>
+#include <vector>
+
 #include "expr/expr.h"
 #include "proof/proof_manager.h"
 
diff --git a/src/proof/theory_proof.h b/src/proof/theory_proof.h
index d69ec5db9..375ec8205 100644
--- a/src/proof/theory_proof.h
+++ b/src/proof/theory_proof.h
@@ -16,15 +16,16 @@
  **
  **/
 
+#include "cvc4_private.h"
 
 #ifndef __CVC4__THEORY_PROOF_H
 #define __CVC4__THEORY_PROOF_H
 
-#include "cvc4_private.h"
-#include "util/proof.h"
-#include "expr/expr.h"
 #include <ext/hash_set>
-#include <iostream>
+#include <iosfwd>
+
+#include "expr/expr.h"
+#include "util/proof.h"
 
 namespace CVC4 {
 
diff --git a/src/proof/unsat_core.h b/src/proof/unsat_core.h
index 644f56509..8e92fe3d1 100644
--- a/src/proof/unsat_core.h
+++ b/src/proof/unsat_core.h
@@ -20,8 +20,9 @@
 #ifndef __CVC4__UNSAT_CORE_H
 #define __CVC4__UNSAT_CORE_H
 
-#include <iostream>
+#include <iosfwd>
 #include <vector>
+
 #include "expr/expr.h"
 
 namespace CVC4 {
diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h
index 3ed828f7c..3be6b1b22 100644
--- a/src/prop/minisat/core/Solver.h
+++ b/src/prop/minisat/core/Solver.h
@@ -23,7 +23,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 
 #include "cvc4_private.h"
 
-#include <iostream>
+#include <iosfwd>
 
 #include "base/output.h"
 #include "context/context.h"
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 1bd2b059b..000cc167f 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -4001,18 +4001,20 @@ bool SmtEngine::addToAssignment(const Expr& ex) throw() {
   Expr e = d_private->substituteAbstractValues(Node::fromExpr(ex)).toExpr();
   Type type = e.getType(options::typeChecking());
   // must be Boolean
-  CheckArgument( type.isBoolean(), e,
-                 "expected Boolean-typed variable or function application "
-                 "in addToAssignment()" );
+  PrettyCheckArgument(
+      type.isBoolean(), e,
+      "expected Boolean-typed variable or function application "
+      "in addToAssignment()" );
   Node n = e.getNode();
   // must be an APPLY of a zero-ary defined function, or a variable
-  CheckArgument( ( ( n.getKind() == kind::APPLY &&
-                     ( d_definedFunctions->find(n.getOperator()) !=
-                       d_definedFunctions->end() ) &&
-                     n.getNumChildren() == 0 ) ||
-                   n.isVar() ), e,
-                 "expected variable or defined-function application "
-                 "in addToAssignment(),\ngot %s", e.toString().c_str() );
+  PrettyCheckArgument(
+      ( ( n.getKind() == kind::APPLY &&
+          ( d_definedFunctions->find(n.getOperator()) !=
+            d_definedFunctions->end() ) &&
+          n.getNumChildren() == 0 ) ||
+        n.isVar() ), e,
+      "expected variable or defined-function application "
+      "in addToAssignment(),\ngot %s", e.toString().c_str() );
   if(!options::produceAssignments()) {
     return false;
   }
diff --git a/src/smt_util/command.cpp b/src/smt_util/command.cpp
index 464a2e0aa..ae4e1f1f0 100644
--- a/src/smt_util/command.cpp
+++ b/src/smt_util/command.cpp
@@ -23,6 +23,7 @@
 #include <utility>
 #include <vector>
 
+#include "base/cvc4_assert.h"
 #include "base/output.h"
 #include "expr/node.h"
 #include "expr/sexpr.h"
@@ -939,7 +940,8 @@ GetValueCommand::GetValueCommand(Expr term) throw() :
 
 GetValueCommand::GetValueCommand(const std::vector<Expr>& terms) throw() :
   d_terms(terms) {
-  CheckArgument(terms.size() >= 1, terms, "cannot get-value of an empty set of terms");
+  PrettyCheckArgument(terms.size() >= 1, terms,
+                      "cannot get-value of an empty set of terms");
 }
 
 const std::vector<Expr>& GetValueCommand::getTerms() const throw() {
diff --git a/src/smt_util/command.h b/src/smt_util/command.h
index b35fb7a7f..17d65beb2 100644
--- a/src/smt_util/command.h
+++ b/src/smt_util/command.h
@@ -22,11 +22,11 @@
 #ifndef __CVC4__COMMAND_H
 #define __CVC4__COMMAND_H
 
-#include <iostream>
+#include <iosfwd>
+#include <map>
 #include <sstream>
 #include <string>
 #include <vector>
-#include <map>
 
 #include "expr/datatype.h"
 #include "expr/expr.h"
diff --git a/src/smt_util/model.h b/src/smt_util/model.h
index 98794a53d..33a9312a6 100644
--- a/src/smt_util/model.h
+++ b/src/smt_util/model.h
@@ -17,7 +17,7 @@
 #ifndef __CVC4__MODEL_H
 #define __CVC4__MODEL_H
 
-#include <iostream>
+#include <iosfwd>
 #include <vector>
 
 #include "expr/expr.h"
diff --git a/src/theory/arith/cut_log.h b/src/theory/arith/cut_log.h
index bbed13418..f4d392995 100644
--- a/src/theory/arith/cut_log.h
+++ b/src/theory/arith/cut_log.h
@@ -234,7 +234,7 @@ std::ostream& operator<<(std::ostream& os, const NodeLog& nl);
 class ApproximateSimplex;
 class TreeLog {
 private:
-  ApproximateSimplex* d_generator;
+  ApproximateSimplex* d_generator CVC4_UNUSED;
 
   int next_exec_ord;
   typedef std::map<int, NodeLog> ToNodeMap;
diff --git a/src/theory/arith/delta_rational.h b/src/theory/arith/delta_rational.h
index 5f67847d8..39d5a9d64 100644
--- a/src/theory/arith/delta_rational.h
+++ b/src/theory/arith/delta_rational.h
@@ -22,6 +22,7 @@
 #include <ostream>
 
 #include "base/exception.h"
+#include "base/cvc4_assert.h"
 #include "util/integer.h"
 #include "util/rational.h"
 
diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp
index 15600fefc..02eeefcaf 100644
--- a/src/theory/logic_info.cpp
+++ b/src/theory/logic_info.cpp
@@ -78,8 +78,167 @@ LogicInfo::LogicInfo(const char* logicString) throw(IllegalArgumentException) :
   lock();
 }
 
+/** Is sharing enabled for this logic? */
+bool LogicInfo::isSharingEnabled() const {
+  PrettyCheckArgument(d_locked, *this,
+                      "This LogicInfo isn't locked yet, and cannot be queried");
+  return d_sharingTheories > 1;
+}
+
+
+/** Is the given theory module active in this logic? */
+bool LogicInfo::isTheoryEnabled(theory::TheoryId theory) const {
+  PrettyCheckArgument(d_locked, *this,
+                      "This LogicInfo isn't locked yet, and cannot be queried");
+  return d_theories[theory];
+}
+
+/** Is this a quantified logic? */
+bool LogicInfo::isQuantified() const {
+  PrettyCheckArgument(d_locked, *this,
+                      "This LogicInfo isn't locked yet, and cannot be queried");
+  return isTheoryEnabled(theory::THEORY_QUANTIFIERS);
+}
+
+/** Is this the all-inclusive logic? */
+bool LogicInfo::hasEverything() const {
+  PrettyCheckArgument(d_locked, *this,
+                      "This LogicInfo isn't locked yet, and cannot be queried");
+  LogicInfo everything;
+  everything.lock();
+  return *this == everything;
+}
+
+/** Is this the all-exclusive logic?  (Here, that means propositional logic) */
+bool LogicInfo::hasNothing() const {
+  PrettyCheckArgument(d_locked, *this,
+                      "This LogicInfo isn't locked yet, and cannot be queried");
+  LogicInfo nothing("");
+  nothing.lock();
+  return *this == nothing;
+}
+
+bool LogicInfo::isPure(theory::TheoryId theory) const {
+  PrettyCheckArgument(d_locked, *this,
+                      "This LogicInfo isn't locked yet, and cannot be queried");
+  // the third and fourth conjucts are really just to rule out the misleading
+  // case where you ask isPure(THEORY_BOOL) and get true even in e.g. QF_LIA
+  return isTheoryEnabled(theory) && !isSharingEnabled() &&
+      ( !isTrueTheory(theory) || d_sharingTheories == 1 ) &&
+      ( isTrueTheory(theory) || d_sharingTheories == 0 );
+}
+
+bool LogicInfo::areIntegersUsed() const {
+  PrettyCheckArgument(d_locked, *this,
+                      "This LogicInfo isn't locked yet, and cannot be queried");
+  PrettyCheckArgument(
+      isTheoryEnabled(theory::THEORY_ARITH), *this,
+      "Arithmetic not used in this LogicInfo; cannot ask whether integers are used");
+  return d_integers;
+}
+
+bool LogicInfo::areRealsUsed() const {
+  PrettyCheckArgument(d_locked, *this,
+                      "This LogicInfo isn't locked yet, and cannot be queried");
+  PrettyCheckArgument(
+      isTheoryEnabled(theory::THEORY_ARITH), *this,
+      "Arithmetic not used in this LogicInfo; cannot ask whether reals are used");
+  return d_reals;
+}
+
+bool LogicInfo::isLinear() const {
+  PrettyCheckArgument(d_locked, *this,
+                      "This LogicInfo isn't locked yet, and cannot be queried");
+  PrettyCheckArgument(
+      isTheoryEnabled(theory::THEORY_ARITH), *this,
+      "Arithmetic not used in this LogicInfo; cannot ask whether it's linear");
+  return d_linear || d_differenceLogic;
+}
+
+bool LogicInfo::isDifferenceLogic() const {
+  PrettyCheckArgument(d_locked, *this,
+                      "This LogicInfo isn't locked yet, and cannot be queried");
+  PrettyCheckArgument(
+      isTheoryEnabled(theory::THEORY_ARITH), *this,
+      "Arithmetic not used in this LogicInfo; cannot ask whether it's difference logic");
+  return d_differenceLogic;
+}
+
+bool LogicInfo::hasCardinalityConstraints() const {
+  PrettyCheckArgument(d_locked, *this,
+                      "This LogicInfo isn't locked yet, and cannot be queried");
+  return d_cardinalityConstraints;
+}
+
+
+bool LogicInfo::operator==(const LogicInfo& other) const {
+  PrettyCheckArgument(isLocked() && other.isLocked(), *this,
+                      "This LogicInfo isn't locked yet, and cannot be queried");
+  for(theory::TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST; ++id) {
+    if(d_theories[id] != other.d_theories[id]) {
+      return false;
+    }
+  }
+
+  PrettyCheckArgument(d_sharingTheories == other.d_sharingTheories, *this,
+                      "LogicInfo internal inconsistency");
+  if(isTheoryEnabled(theory::THEORY_ARITH)) {
+    return
+        d_integers == other.d_integers &&
+        d_reals == other.d_reals &&
+        d_linear == other.d_linear &&
+        d_differenceLogic == other.d_differenceLogic;
+  } else {
+    return true;
+  }
+}
+
+bool LogicInfo::operator<=(const LogicInfo& other) const {
+  PrettyCheckArgument(isLocked() && other.isLocked(), *this,
+                      "This LogicInfo isn't locked yet, and cannot be queried");
+  for(theory::TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST; ++id) {
+    if(d_theories[id] && !other.d_theories[id]) {
+      return false;
+    }
+  }
+  PrettyCheckArgument(d_sharingTheories <= other.d_sharingTheories, *this,
+                      "LogicInfo internal inconsistency");
+  if(isTheoryEnabled(theory::THEORY_ARITH) && other.isTheoryEnabled(theory::THEORY_ARITH)) {
+    return
+        (!d_integers || other.d_integers) &&
+        (!d_reals || other.d_reals) &&
+        (d_linear || !other.d_linear) &&
+        (d_differenceLogic || !other.d_differenceLogic);
+  } else {
+    return true;
+  }
+}
+
+bool LogicInfo::operator>=(const LogicInfo& other) const {
+  PrettyCheckArgument(isLocked() && other.isLocked(), *this,
+                      "This LogicInfo isn't locked yet, and cannot be queried");
+  for(theory::TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST; ++id) {
+    if(!d_theories[id] && other.d_theories[id]) {
+      return false;
+    }
+  }
+  PrettyCheckArgument(d_sharingTheories >= other.d_sharingTheories, *this,
+                      "LogicInfo internal inconsistency");
+  if(isTheoryEnabled(theory::THEORY_ARITH) && other.isTheoryEnabled(theory::THEORY_ARITH)) {
+    return
+        (d_integers || !other.d_integers) &&
+        (d_reals || !other.d_reals) &&
+        (!d_linear || other.d_linear) &&
+        (!d_differenceLogic || other.d_differenceLogic);
+    } else {
+    return true;
+  }
+}
+
 std::string LogicInfo::getLogicString() const {
-  CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried");
+  PrettyCheckArgument(
+      d_locked, *this,
+      "This LogicInfo isn't locked yet, and cannot be queried");
   if(d_logicString == "") {
     LogicInfo qf_all_supported;
     qf_all_supported.disableQuantifiers();
@@ -156,7 +315,8 @@ std::string LogicInfo::getLogicString() const {
 }
 
 void LogicInfo::setLogicString(std::string logicString) throw(IllegalArgumentException) {
-  CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
+  PrettyCheckArgument(!d_locked, *this,
+                      "This LogicInfo is locked, and cannot be modified");
   for(TheoryId id = THEORY_FIRST; id < THEORY_LAST; ++id) {
     d_theories[id] = false;// ensure it's cleared
   }
@@ -299,17 +459,17 @@ void LogicInfo::setLogicString(std::string logicString) throw(IllegalArgumentExc
 }
 
 void LogicInfo::enableEverything() {
-  CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
+  PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
   *this = LogicInfo();
 }
 
 void LogicInfo::disableEverything() {
-  CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
+  PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
   *this = LogicInfo("");
 }
 
 void LogicInfo::enableTheory(theory::TheoryId theory) {
-  CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
+  PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
   if(!d_theories[theory]) {
     if(isTrueTheory(theory)) {
       ++d_sharingTheories;
@@ -320,7 +480,7 @@ void LogicInfo::enableTheory(theory::TheoryId theory) {
 }
 
 void LogicInfo::disableTheory(theory::TheoryId theory) {
-  CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
+  PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
   if(d_theories[theory]) {
     if(isTrueTheory(theory)) {
       Assert(d_sharingTheories > 0);
@@ -336,14 +496,14 @@ void LogicInfo::disableTheory(theory::TheoryId theory) {
 }
 
 void LogicInfo::enableIntegers() {
-  CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
+  PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
   d_logicString = "";
   enableTheory(THEORY_ARITH);
   d_integers = true;
 }
 
 void LogicInfo::disableIntegers() {
-  CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
+  PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
   d_logicString = "";
   d_integers = false;
   if(!d_reals) {
@@ -352,14 +512,14 @@ void LogicInfo::disableIntegers() {
 }
 
 void LogicInfo::enableReals() {
-  CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
+  PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
   d_logicString = "";
   enableTheory(THEORY_ARITH);
   d_reals = true;
 }
 
 void LogicInfo::disableReals() {
-  CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
+  PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
   d_logicString = "";
   d_reals = false;
   if(!d_integers) {
@@ -368,21 +528,21 @@ void LogicInfo::disableReals() {
 }
 
 void LogicInfo::arithOnlyDifference() {
-  CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
+  PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
   d_logicString = "";
   d_linear = true;
   d_differenceLogic = true;
 }
 
 void LogicInfo::arithOnlyLinear() {
-  CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
+  PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
   d_logicString = "";
   d_linear = true;
   d_differenceLogic = false;
 }
 
 void LogicInfo::arithNonLinear() {
-  CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
+  PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
   d_logicString = "";
   d_linear = false;
   d_differenceLogic = false;
diff --git a/src/theory/logic_info.h b/src/theory/logic_info.h
index 9cecc88b7..54b735114 100644
--- a/src/theory/logic_info.h
+++ b/src/theory/logic_info.h
@@ -104,84 +104,43 @@ public:
   std::string getLogicString() const;
 
   /** Is sharing enabled for this logic? */
-  bool isSharingEnabled() const {
-    CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried");
-    return d_sharingTheories > 1;
-  }
+  bool isSharingEnabled() const;
 
   /** Is the given theory module active in this logic? */
-  bool isTheoryEnabled(theory::TheoryId theory) const {
-    CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried");
-    return d_theories[theory];
-  }
+  bool isTheoryEnabled(theory::TheoryId theory) const;
 
   /** Is this a quantified logic? */
-  bool isQuantified() const {
-    CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried");
-    return isTheoryEnabled(theory::THEORY_QUANTIFIERS);
-  }
+  bool isQuantified() const;
 
   /** Is this the all-inclusive logic? */
-  bool hasEverything() const {
-    CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried");
-    LogicInfo everything;
-    everything.lock();
-    return *this == everything;
-  }
+  bool hasEverything() const;
 
   /** Is this the all-exclusive logic?  (Here, that means propositional logic) */
-  bool hasNothing() const {
-    CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried");
-    LogicInfo nothing("");
-    nothing.lock();
-    return *this == nothing;
-  }
+  bool hasNothing() const;
 
   /**
    * Is this a pure logic (only one "true" background theory).  Quantifiers
    * can exist in such logics though; to test for quantifier-free purity,
    * use "isPure(theory) && !isQuantified()".
    */
-  bool isPure(theory::TheoryId theory) const {
-    CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried");
-    // the third and fourth conjucts are really just to rule out the misleading
-    // case where you ask isPure(THEORY_BOOL) and get true even in e.g. QF_LIA
-    return isTheoryEnabled(theory) && !isSharingEnabled() &&
-      ( !isTrueTheory(theory) || d_sharingTheories == 1 ) &&
-      ( isTrueTheory(theory) || d_sharingTheories == 0 );
-  }
+  bool isPure(theory::TheoryId theory) const;
 
   // these are for arithmetic
 
   /** Are integers in this logic? */
-  bool areIntegersUsed() const {
-    CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried");
-    CheckArgument(isTheoryEnabled(theory::THEORY_ARITH), *this, "Arithmetic not used in this LogicInfo; cannot ask whether integers are used");
-    return d_integers;
-  }
+  bool areIntegersUsed() const;
+
   /** Are reals in this logic? */
-  bool areRealsUsed() const {
-    CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried");
-    CheckArgument(isTheoryEnabled(theory::THEORY_ARITH), *this, "Arithmetic not used in this LogicInfo; cannot ask whether reals are used");
-    return d_reals;
-  }
+  bool areRealsUsed() const;
+
   /** Does this logic only linear arithmetic? */
-  bool isLinear() const {
-    CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried");
-    CheckArgument(isTheoryEnabled(theory::THEORY_ARITH), *this, "Arithmetic not used in this LogicInfo; cannot ask whether it's linear");
-    return d_linear || d_differenceLogic;
-  }
+  bool isLinear() const;
+
   /** Does this logic only permit difference reasoning? (implies linear) */
-  bool isDifferenceLogic() const {
-    CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried");
-    CheckArgument(isTheoryEnabled(theory::THEORY_ARITH), *this, "Arithmetic not used in this LogicInfo; cannot ask whether it's difference logic");
-    return d_differenceLogic;
-  }
+  bool isDifferenceLogic() const;
+
   /** Does this logic allow cardinality constraints? */
-  bool hasCardinalityConstraints() const {
-    CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried");
-    return d_cardinalityConstraints;
-  }
+  bool hasCardinalityConstraints() const;
 
   // MUTATORS
 
@@ -258,74 +217,27 @@ public:
   // COMPARISON
 
   /** Are these two LogicInfos equal? */
-  bool operator==(const LogicInfo& other) const {
-    CheckArgument(isLocked() && other.isLocked(), *this, "This LogicInfo isn't locked yet, and cannot be queried");
-    for(theory::TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST; ++id) {
-      if(d_theories[id] != other.d_theories[id]) {
-        return false;
-      }
-    }
-    CheckArgument(d_sharingTheories == other.d_sharingTheories, *this, "LogicInfo internal inconsistency");
-    if(isTheoryEnabled(theory::THEORY_ARITH)) {
-      return
-        d_integers == other.d_integers &&
-        d_reals == other.d_reals &&
-        d_linear == other.d_linear &&
-        d_differenceLogic == other.d_differenceLogic;
-    } else {
-      return true;
-    }
-  }
+  bool operator==(const LogicInfo& other) const;
+
   /** Are these two LogicInfos disequal? */
   bool operator!=(const LogicInfo& other) const {
     return !(*this == other);
   }
+
   /** Is this LogicInfo "greater than" (does it contain everything and more) the other? */
   bool operator>(const LogicInfo& other) const {
     return *this >= other && *this != other;
   }
+
   /** Is this LogicInfo "less than" (does it contain strictly less) the other? */
   bool operator<(const LogicInfo& other) const {
     return *this <= other && *this != other;
   }
   /** Is this LogicInfo "less than or equal" the other? */
-  bool operator<=(const LogicInfo& other) const {
-    CheckArgument(isLocked() && other.isLocked(), *this, "This LogicInfo isn't locked yet, and cannot be queried");
-    for(theory::TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST; ++id) {
-      if(d_theories[id] && !other.d_theories[id]) {
-        return false;
-      }
-    }
-    CheckArgument(d_sharingTheories <= other.d_sharingTheories, *this, "LogicInfo internal inconsistency");
-    if(isTheoryEnabled(theory::THEORY_ARITH) && other.isTheoryEnabled(theory::THEORY_ARITH)) {
-      return
-        (!d_integers || other.d_integers) &&
-        (!d_reals || other.d_reals) &&
-        (d_linear || !other.d_linear) &&
-        (d_differenceLogic || !other.d_differenceLogic);
-    } else {
-      return true;
-    }
-  }
+  bool operator<=(const LogicInfo& other) const;
+
   /** Is this LogicInfo "greater than or equal" the other? */
-  bool operator>=(const LogicInfo& other) const {
-    CheckArgument(isLocked() && other.isLocked(), *this, "This LogicInfo isn't locked yet, and cannot be queried");
-    for(theory::TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST; ++id) {
-      if(!d_theories[id] && other.d_theories[id]) {
-        return false;
-      }
-    }
-    CheckArgument(d_sharingTheories >= other.d_sharingTheories, *this, "LogicInfo internal inconsistency");
-    if(isTheoryEnabled(theory::THEORY_ARITH) && other.isTheoryEnabled(theory::THEORY_ARITH)) {
-      return
-        (d_integers || !other.d_integers) &&
-        (d_reals || !other.d_reals) &&
-        (!d_linear || other.d_linear) &&
-        (!d_differenceLogic || other.d_differenceLogic);
-    } else {
-      return true;
-    }
-  }
+  bool operator>=(const LogicInfo& other) const;
 
   /** Are two LogicInfos comparable?  That is, is one of <= or > true? */
   bool isComparableTo(const LogicInfo& other) const {
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 798576ec3..b92d72ef4 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -1817,11 +1817,9 @@ void QuantifiersRewriter::computePurifyExpand( Node body, std::vector< Node >& c
     std::map< int, std::vector< Node > > disj;
     std::map< int, std::vector< Node > > fvs;
     for( unsigned i=0; i<body.getNumChildren(); i++ ){
-      int pid = getPurifyIdLit( body[i] );
-      
+      int pid CVC4_UNUSED = getPurifyIdLit( body[i] );
     }
     //mark as an attribute
     //Node attr = NodeManager::currentNM()->mkNode( INST_ATTRIBUTE, body );
-    
   }
 }
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index a39d74bb0..fb5fb0f0c 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -22,10 +22,11 @@
 #include "theory/uf/theory_uf_model.h"
 
 using namespace std;
-using namespace CVC4;
 using namespace CVC4::kind;
 using namespace CVC4::context;
-using namespace CVC4::theory;
+
+namespace CVC4 {
+namespace theory {
 
 TheoryModel::TheoryModel(context::Context* c, std::string name, bool enableFuncModels) :
   d_substitutions(c, false), d_modelBuilt(c, false), d_enableFuncModels(enableFuncModels)
@@ -963,3 +964,6 @@ void TheoryEngineModelBuilder::processBuildModel(TheoryModel* m, bool fullModel)
     }
   }
 }
+
+} /* namespace CVC4::theory */
+} /* namespace CVC4 */
diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index 914d6e7d2..55f1a14da 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -45,6 +45,7 @@ libutil_la_SOURCES = \
 	regexp.h \
 	smt2_quote_string.cpp \
 	smt2_quote_string.h \
+	subrange_bound.cpp \
 	subrange_bound.h \
 	tuple.h \
 	unsafe_interrupt_exception.h \
diff --git a/src/util/abstract_value.cpp b/src/util/abstract_value.cpp
index e401661eb..c9dc0251d 100644
--- a/src/util/abstract_value.cpp
+++ b/src/util/abstract_value.cpp
@@ -15,10 +15,13 @@
  **/
 
 #include "util/abstract_value.h"
+
 #include <iostream>
 #include <sstream>
 #include <string>
 
+#include "base/cvc4_assert.h"
+
 using namespace std;
 
 namespace CVC4 {
@@ -29,7 +32,7 @@ std::ostream& operator<<(std::ostream& out, const AbstractValue& val) {
 
 AbstractValue::AbstractValue(Integer index) throw(IllegalArgumentException) :
     d_index(index) {
-    CheckArgument(index >= 1, index, "index >= 1 required for abstract value, not `%s'", index.toString().c_str());
+    PrettyCheckArgument(index >= 1, index, "index >= 1 required for abstract value, not `%s'", index.toString().c_str());
 }
 
 }/* CVC4 namespace */
diff --git a/src/util/abstract_value.h b/src/util/abstract_value.h
index d597edc8b..f02df2e66 100644
--- a/src/util/abstract_value.h
+++ b/src/util/abstract_value.h
@@ -18,7 +18,7 @@
 
 #pragma once
 
-#include <iostream>
+#include <iosfwd>
 
 #include "util/integer.h"
 
diff --git a/src/util/bin_heap.h b/src/util/bin_heap.h
index d057bcf84..ed6192cf7 100644
--- a/src/util/bin_heap.h
+++ b/src/util/bin_heap.h
@@ -26,6 +26,7 @@
 #include <limits>
 #include <functional>
 
+#include "base/cvc4_assert.h"
 #include "base/exception.h"
 
 namespace CVC4 {
diff --git a/src/util/bitvector.h b/src/util/bitvector.h
index 762753795..041cae38e 100644
--- a/src/util/bitvector.h
+++ b/src/util/bitvector.h
@@ -20,7 +20,7 @@
 #ifndef __CVC4__BITVECTOR_H
 #define __CVC4__BITVECTOR_H
 
-#include <iostream>
+#include <iosfwd>
 
 #include "base/exception.h"
 #include "util/integer.h"
@@ -28,34 +28,13 @@
 namespace CVC4 {
 
 class CVC4_PUBLIC BitVector {
-
-private:
-
-  /*
-    Class invariants:
-    * no overflows: 2^d_size < d_value
-    * no negative numbers: d_value >= 0
-   */
-  unsigned d_size;
-  Integer d_value;
-
-  Integer toSignedInt() const {
-    // returns Integer corresponding to two's complement interpretation of bv 
-    unsigned size = d_size; 
-    Integer sign_bit = d_value.extractBitRange(1,size-1);
-    Integer val = d_value.extractBitRange(size-1, 0); 
-    Integer res = Integer(-1) * sign_bit.multiplyByPow2(size - 1) + val;
-    return res; 
-  }
-  
- 
 public:
 
   BitVector(unsigned size, const Integer& val):
     d_size(size),
     d_value(val.modByPow2(size))
       {}
-  
+
   BitVector(unsigned size = 0)
     : d_size(size), d_value(0) {}
 
@@ -63,7 +42,7 @@ public:
     : d_size(size), d_value(z) {
     d_value = d_value.modByPow2(size);
   }
-  
+
   BitVector(unsigned size, unsigned long int z)
     : d_size(size), d_value(z) {
     d_value = d_value.modByPow2(size);
@@ -71,7 +50,7 @@ public:
 
   BitVector(unsigned size, const BitVector& q)
     : d_size(size), d_value(q.d_value) {}
-  
+
   BitVector(const std::string& num, unsigned base = 2);
 
   ~BitVector() {}
@@ -79,7 +58,7 @@ public:
   Integer toInteger() const {
     return d_value;
   }
-  
+
   BitVector& operator =(const BitVector& x) {
     if(this == &x)
       return *this;
@@ -89,12 +68,12 @@ public:
   }
 
   bool operator ==(const BitVector& y) const {
-    if (d_size != y.d_size) return false; 
+    if (d_size != y.d_size) return false;
     return d_value == y.d_value;
   }
 
   bool operator !=(const BitVector& y) const {
-    if (d_size != y.d_size) return true; 
+    if (d_size != y.d_size) return true;
     return d_value != y.d_value;
   }
 
@@ -113,24 +92,24 @@ public:
   // xor
   BitVector operator ^(const BitVector& y) const {
     CheckArgument(d_size == y.d_size, y);
-    return BitVector(d_size, d_value.bitwiseXor(y.d_value)); 
+    return BitVector(d_size, d_value.bitwiseXor(y.d_value));
   }
-  
+
   // or
   BitVector operator |(const BitVector& y) const {
     CheckArgument(d_size == y.d_size, y);
-    return BitVector(d_size, d_value.bitwiseOr(y.d_value)); 
+    return BitVector(d_size, d_value.bitwiseOr(y.d_value));
   }
-  
+
   // and
   BitVector operator &(const BitVector& y) const {
     CheckArgument(d_size == y.d_size, y);
-    return BitVector(d_size, d_value.bitwiseAnd(y.d_value)); 
+    return BitVector(d_size, d_value.bitwiseAnd(y.d_value));
   }
 
   // not
   BitVector operator ~() const {
-    return BitVector(d_size, d_value.bitwiseNot()); 
+    return BitVector(d_size, d_value.bitwiseNot());
   }
 
   /*
@@ -139,7 +118,7 @@ public:
 
 
   bool operator <(const BitVector& y) const {
-    return d_value < y.d_value; 
+    return d_value < y.d_value;
   }
 
   bool operator >(const BitVector& y) const {
@@ -147,14 +126,14 @@ public:
   }
 
   bool operator <=(const BitVector& y) const {
-    return d_value <= y.d_value; 
+    return d_value <= y.d_value;
   }
-  
+
   bool operator >=(const BitVector& y) const {
     return d_value >= y.d_value ;
   }
 
-  
+
   BitVector operator +(const BitVector& y) const {
     CheckArgument(d_size == y.d_size, y);
     Integer sum = d_value +  y.d_value;
@@ -165,12 +144,12 @@ public:
     CheckArgument(d_size == y.d_size, y);
     // to maintain the invariant that we are only adding BitVectors of the
     // same size
-    BitVector one(d_size, Integer(1)); 
+    BitVector one(d_size, Integer(1));
     return *this + ~y + one;
   }
 
   BitVector operator -() const {
-    BitVector one(d_size, Integer(1)); 
+    BitVector one(d_size, Integer(1));
     return ~(*this) + one;
   }
 
@@ -183,16 +162,16 @@ public:
   BitVector setBit(uint32_t i) const {
     CheckArgument(i < d_size, i);
     Integer res = d_value.setBit(i);
-    return BitVector(d_size, res); 
+    return BitVector(d_size, res);
   }
 
   bool isBitSet(uint32_t i) const {
-    CheckArgument(i < d_size, i); 
-    return d_value.isBitSet(i); 
+    CheckArgument(i < d_size, i);
+    return d_value.isBitSet(i);
   }
-  
-  /** 
-   * Total division function that returns 0 when the denominator is 0.  
+
+  /**
+   * Total division function that returns 0 when the denominator is 0.
    */
   BitVector unsignedDivTotal (const BitVector& y) const {
 
@@ -203,11 +182,11 @@ public:
     }
     CheckArgument(d_value >= 0, this);
     CheckArgument(y.d_value > 0, y);
-    return BitVector(d_size, d_value.floorDivideQuotient(y.d_value)); 
+    return BitVector(d_size, d_value.floorDivideQuotient(y.d_value));
   }
-  
-  /** 
-   * Total division function that returns 0 when the denominator is 0.  
+
+  /**
+   * Total division function that returns 0 when the denominator is 0.
    */
   BitVector unsignedRemTotal(const BitVector& y) const {
     CheckArgument(d_size == y.d_size, y);
@@ -216,25 +195,25 @@ public:
     }
     CheckArgument(d_value >= 0, this);
     CheckArgument(y.d_value > 0, y);
-    return BitVector(d_size, d_value.floorDivideRemainder(y.d_value)); 
+    return BitVector(d_size, d_value.floorDivideRemainder(y.d_value));
   }
-  
-  
+
+
   bool signedLessThan(const BitVector& y) const {
     CheckArgument(d_size == y.d_size, y);
     CheckArgument(d_value >= 0, this);
     CheckArgument(y.d_value >= 0, y);
     Integer a = (*this).toSignedInt();
-    Integer b = y.toSignedInt(); 
-    
-    return a < b; 
+    Integer b = y.toSignedInt();
+
+    return a < b;
   }
 
   bool unsignedLessThan(const BitVector& y) const {
     CheckArgument(d_size == y.d_size, y);
     CheckArgument(d_value >= 0, this);
     CheckArgument(y.d_value >= 0, y);
-    return d_value < y.d_value; 
+    return d_value < y.d_value;
   }
 
   bool signedLessThanEq(const BitVector& y) const {
@@ -242,100 +221,98 @@ public:
     CheckArgument(d_value >= 0, this);
     CheckArgument(y.d_value >= 0, y);
     Integer a = (*this).toSignedInt();
-    Integer b = y.toSignedInt(); 
-    
-    return a <= b; 
+    Integer b = y.toSignedInt();
+
+    return a <= b;
   }
 
   bool unsignedLessThanEq(const BitVector& y) const {
     CheckArgument(d_size == y.d_size, this);
     CheckArgument(d_value >= 0, this);
     CheckArgument(y.d_value >= 0, y);
-    return d_value <= y.d_value; 
+    return d_value <= y.d_value;
   }
 
-  
+
   /*
     Extend operations
    */
-
   BitVector zeroExtend(unsigned amount) const {
-    return BitVector(d_size + amount, d_value); 
+    return BitVector(d_size + amount, d_value);
   }
 
   BitVector signExtend(unsigned amount) const {
     Integer sign_bit = d_value.extractBitRange(1, d_size -1);
     if(sign_bit == Integer(0)) {
-      return BitVector(d_size + amount, d_value); 
+      return BitVector(d_size + amount, d_value);
     } else {
       Integer val = d_value.oneExtend(d_size, amount);
       return BitVector(d_size+ amount, val);
     }
   }
-  
+
   /*
     Shifts on BitVectors
    */
-
   BitVector leftShift(const BitVector& y) const {
     if (y.d_value > Integer(d_size)) {
-      return BitVector(d_size, Integer(0)); 
+      return BitVector(d_size, Integer(0));
     }
     if (y.d_value == 0) {
-      return *this; 
+      return *this;
     }
 
     // making sure we don't lose information casting
     CheckArgument(y.d_value < Integer(1).multiplyByPow2(32), y);
-    uint32_t amount = y.d_value.toUnsignedInt(); 
+    uint32_t amount = y.d_value.toUnsignedInt();
     Integer res = d_value.multiplyByPow2(amount);
     return BitVector(d_size, res);
   }
 
   BitVector logicalRightShift(const BitVector& y) const {
     if(y.d_value > Integer(d_size)) {
-      return BitVector(d_size, Integer(0)); 
+      return BitVector(d_size, Integer(0));
     }
 
     // making sure we don't lose information casting
     CheckArgument(y.d_value < Integer(1).multiplyByPow2(32), y);
-    uint32_t amount = y.d_value.toUnsignedInt(); 
-    Integer res = d_value.divByPow2(amount); 
+    uint32_t amount = y.d_value.toUnsignedInt();
+    Integer res = d_value.divByPow2(amount);
     return BitVector(d_size, res);
   }
 
   BitVector arithRightShift(const BitVector& y) const {
-    Integer sign_bit = d_value.extractBitRange(1, d_size - 1); 
+    Integer sign_bit = d_value.extractBitRange(1, d_size - 1);
     if(y.d_value > Integer(d_size)) {
       if(sign_bit == Integer(0)) {
-        return BitVector(d_size, Integer(0)); 
+        return BitVector(d_size, Integer(0));
       } else {
-        return BitVector(d_size, Integer(d_size).multiplyByPow2(d_size) -1 ); 
+        return BitVector(d_size, Integer(d_size).multiplyByPow2(d_size) -1 );
       }
     }
-    
+
     if (y.d_value == 0) {
-      return *this; 
+      return *this;
     }
 
     // making sure we don't lose information casting
     CheckArgument(y.d_value < Integer(1).multiplyByPow2(32), y);
-   
+
     uint32_t amount  = y.d_value.toUnsignedInt();
     Integer rest = d_value.divByPow2(amount);
-    
+
     if(sign_bit == Integer(0)) {
-      return BitVector(d_size, rest); 
+      return BitVector(d_size, rest);
     }
     Integer res = rest.oneExtend(d_size - amount, amount);
     return BitVector(d_size, res);
   }
-  
+
 
   /*
     Convenience functions
    */
-  
+
   size_t hash() const {
     return d_value.hash() + d_size;
   }
@@ -367,9 +344,26 @@ public:
    @return k if the integer is equal to 2^{k-1} and zero otherwise
    */
   unsigned isPow2() {
-    return d_value.isPow2(); 
+    return d_value.isPow2();
   }
 
+private:
+  /*
+    Class invariants:
+    * no overflows: 2^d_size < d_value
+    * no negative numbers: d_value >= 0
+   */
+  unsigned d_size;
+  Integer d_value;
+
+  Integer toSignedInt() const {
+    // returns Integer corresponding to two's complement interpretation of bv
+    unsigned size = d_size;
+    Integer sign_bit = d_value.extractBitRange(1,size-1);
+    Integer val = d_value.extractBitRange(size-1, 0);
+    Integer res = Integer(-1) * sign_bit.multiplyByPow2(size - 1) + val;
+    return res;
+  }
 };/* class BitVector */
 
 
@@ -428,7 +422,7 @@ struct CVC4_PUBLIC BitVectorExtractHashFunction {
 
 
 /**
- * The structure representing the extraction of one Boolean bit. 
+ * The structure representing the extraction of one Boolean bit.
  */
 struct CVC4_PUBLIC BitVectorBitOf {
   /** The index of the bit */
@@ -437,7 +431,7 @@ struct CVC4_PUBLIC BitVectorBitOf {
     : bitIndex(i) {}
 
   bool operator == (const BitVectorBitOf& other) const {
-    return bitIndex == other.bitIndex; 
+    return bitIndex == other.bitIndex;
   }
 };/* struct BitVectorBitOf */
 
diff --git a/src/util/cardinality.cpp b/src/util/cardinality.cpp
index dfee0aae2..07e094a38 100644
--- a/src/util/cardinality.cpp
+++ b/src/util/cardinality.cpp
@@ -16,6 +16,9 @@
 
 #include "util/cardinality.h"
 
+#include "base/cvc4_assert.h"
+
+
 namespace CVC4 {
 
 const Integer Cardinality::s_unknownCard(0);
@@ -27,6 +30,45 @@ const Cardinality Cardinality::INTEGERS(CardinalityBeth(0));
 const Cardinality Cardinality::REALS(CardinalityBeth(1));
 const Cardinality Cardinality::UNKNOWN_CARD((CardinalityUnknown()));
 
+CardinalityBeth::CardinalityBeth(const Integer& beth)
+    : d_index(beth)
+{
+  PrettyCheckArgument(beth >= 0, beth,
+                      "Beth index must be a nonnegative integer, not %s.",
+                      beth.toString().c_str());
+}
+
+Cardinality::Cardinality(long card)
+    : d_card(card)
+{
+  PrettyCheckArgument(card >= 0, card,
+                      "Cardinality must be a nonnegative integer, not %ld.",
+                      card);
+  d_card += 1;
+}
+
+Cardinality::Cardinality(const Integer& card)
+    : d_card(card)
+{
+  PrettyCheckArgument(card >= 0, card,
+                      "Cardinality must be a nonnegative integer, not %s.",
+                      card.toString().c_str());
+  d_card += 1;
+}
+
+
+Integer Cardinality::getFiniteCardinality() const throw(IllegalArgumentException) {
+  PrettyCheckArgument(isFinite(), *this, "This cardinality is not finite.");
+  PrettyCheckArgument(!isLargeFinite(), *this, "This cardinality is finite, but too large to represent.");
+  return d_card - 1;
+}
+
+Integer Cardinality::getBethNumber() const throw(IllegalArgumentException) {
+  PrettyCheckArgument(!isFinite() && !isUnknown(), *this,
+                      "This cardinality is not infinite (or is unknown).");
+  return -d_card - 1;
+}
+
 Cardinality& Cardinality::operator+=(const Cardinality& c) throw() {
   if(isUnknown()) {
     return *this;
diff --git a/src/util/cardinality.h b/src/util/cardinality.h
index 1cb4454e0..8b0d85980 100644
--- a/src/util/cardinality.h
+++ b/src/util/cardinality.h
@@ -36,11 +36,7 @@ class CVC4_PUBLIC CardinalityBeth {
   Integer d_index;
 
 public:
-  CardinalityBeth(const Integer& beth) : d_index(beth) {
-    CheckArgument(beth >= 0, beth,
-                  "Beth index must be a nonnegative integer, not %s.",
-                  beth.toString().c_str());
-  }
+  CardinalityBeth(const Integer& beth);
 
   const Integer& getNumber() const throw() {
     return d_index;
@@ -112,22 +108,13 @@ public:
    * "unsigned" argument to enforce the restriction, we mask some
    * errors that automatically convert, like "Cardinality(-1)".
    */
-  Cardinality(long card) : d_card(card) {
-    CheckArgument(card >= 0, card,
-                  "Cardinality must be a nonnegative integer, not %ld.", card);
-    d_card += 1;
-  }
+  Cardinality(long card);
 
   /**
    * Construct a finite cardinality equal to the integer argument.
    * The argument must be nonnegative.
    */
-  Cardinality(const Integer& card) : d_card(card) {
-    CheckArgument(card >= 0, card,
-                  "Cardinality must be a nonnegative integer, not %s.",
-                  card.toString().c_str());
-    d_card += 1;
-  }
+  Cardinality(const Integer& card);
 
   /**
    * Construct an infinite cardinality equal to the given Beth number.
@@ -187,22 +174,14 @@ public:
    * cardinality.  (If this cardinality is infinite, this function
    * throws an IllegalArgumentException.)
    */
-  Integer getFiniteCardinality() const throw(IllegalArgumentException) {
-    CheckArgument(isFinite(), *this, "This cardinality is not finite.");
-    CheckArgument(!isLargeFinite(), *this, "This cardinality is finite, but too large to represent.");
-    return d_card - 1;
-  }
+  Integer getFiniteCardinality() const throw(IllegalArgumentException);
 
   /**
    * In the case that this cardinality is infinite, return its Beth
    * number.  (If this cardinality is finite, this function throws an
    * IllegalArgumentException.)
    */
-  Integer getBethNumber() const throw(IllegalArgumentException) {
-    CheckArgument(!isFinite() && !isUnknown(), *this,
-                  "This cardinality is not infinite (or is unknown).");
-    return -d_card - 1;
-  }
+  Integer getBethNumber() const throw(IllegalArgumentException);
 
   /** Assigning addition of this cardinality with another. */
   Cardinality& operator+=(const Cardinality& c) throw();
diff --git a/src/util/divisible.cpp b/src/util/divisible.cpp
index 4a8b7a2e7..85824a77f 100644
--- a/src/util/divisible.cpp
+++ b/src/util/divisible.cpp
@@ -17,6 +17,7 @@
 
 #include "util/divisible.h"
 
+#include "base/cvc4_assert.h"
 #include "base/exception.h"
 
 using namespace std;
@@ -24,7 +25,7 @@ using namespace std;
 namespace CVC4 {
 
 Divisible::Divisible(const Integer& n) : k(n) {
-  CheckArgument(n > 0, n, "Divisible predicate must be constructed over positive N");
+  PrettyCheckArgument(n > 0, n, "Divisible predicate must be constructed over positive N");
 }
 
 }/* CVC4 namespace */
diff --git a/src/util/divisible.h b/src/util/divisible.h
index 5f62def02..56178e604 100644
--- a/src/util/divisible.h
+++ b/src/util/divisible.h
@@ -20,7 +20,7 @@
 #ifndef __CVC4__DIVISIBLE_H
 #define __CVC4__DIVISIBLE_H
 
-#include <iostream>
+#include <iosfwd>
 
 #include "base/exception.h"
 #include "util/integer.h"
diff --git a/src/util/floatingpoint.cpp b/src/util/floatingpoint.cpp
index d3bb1967a..d1164133a 100644
--- a/src/util/floatingpoint.cpp
+++ b/src/util/floatingpoint.cpp
@@ -19,20 +19,20 @@
 
 namespace CVC4 {
 
-  FloatingPointSize::FloatingPointSize (unsigned _e, unsigned _s) : e(_e), s(_s)
-  {
-    CheckArgument(validExponentSize(_e),_e,"Invalid exponent size : %d",_e);
-    CheckArgument(validSignificandSize(_s),_s,"Invalid significand size : %d",_s);
-  }
+FloatingPointSize::FloatingPointSize (unsigned _e, unsigned _s) : e(_e), s(_s)
+{
+  PrettyCheckArgument(validExponentSize(_e),_e,"Invalid exponent size : %d",_e);
+  PrettyCheckArgument(validSignificandSize(_s),_s,"Invalid significand size : %d",_s);
+}
 
-  FloatingPointSize::FloatingPointSize (const FloatingPointSize &old) : e(old.e), s(old.s)
-  {
-    CheckArgument(validExponentSize(e),e,"Invalid exponent size : %d",e);
-    CheckArgument(validSignificandSize(s),s,"Invalid significand size : %d",s);
-  }
+FloatingPointSize::FloatingPointSize (const FloatingPointSize &old) : e(old.e), s(old.s)
+{
+  PrettyCheckArgument(validExponentSize(e),e,"Invalid exponent size : %d",e);
+  PrettyCheckArgument(validSignificandSize(s),s,"Invalid significand size : %d",s);
+}
 
-  void FloatingPointLiteral::unfinished (void) const {
-    Unimplemented("Floating-point literals not yet implemented.");
-  }
+void FloatingPointLiteral::unfinished (void) const {
+  Unimplemented("Floating-point literals not yet implemented.");
+}
 
 }/* CVC4 namespace */
diff --git a/src/util/integer_cln_imp.cpp b/src/util/integer_cln_imp.cpp
index 1cb4349eb..27a4b7d06 100644
--- a/src/util/integer_cln_imp.cpp
+++ b/src/util/integer_cln_imp.cpp
@@ -26,8 +26,34 @@
 #  error "This source should only ever be built if CVC4_CLN_IMP is on !"
 #endif /* CVC4_CLN_IMP */
 
+#include "base/cvc4_assert.h"
+
 using namespace std;
-using namespace CVC4;
+
+namespace CVC4 {
+
+signed int Integer::s_fastSignedIntMin = -(1<<29);
+signed int Integer::s_fastSignedIntMax = (1<<29)-1;
+signed long Integer::s_slowSignedIntMin = (signed long) std::numeric_limits<signed int>::min();
+signed long Integer::s_slowSignedIntMax =  (signed long) std::numeric_limits<signed int>::max();
+
+unsigned int Integer::s_fastUnsignedIntMax = (1<<29)-1;
+unsigned long Integer::s_slowUnsignedIntMax =  (unsigned long) std::numeric_limits<unsigned int>::max();
+
+Integer Integer::oneExtend(uint32_t size, uint32_t amount) const {
+  DebugCheckArgument((*this) < Integer(1).multiplyByPow2(size), size);
+  cln::cl_byte range(amount, size);
+  cln::cl_I allones = (cln::cl_I(1) << (size + amount))- 1; // 2^size - 1
+  Integer temp(allones);
+
+  return Integer(cln::deposit_field(allones, d_value, range));
+}
+
+
+Integer Integer::exactQuotient(const Integer& y) const {
+  DebugCheckArgument(y.divides(*this), y);
+  return Integer( cln::exquo(d_value, y.d_value) );
+}
 
 
 void Integer::parseInt(const std::string& s, unsigned base) throw(std::invalid_argument) {
@@ -78,14 +104,21 @@ void Integer::readInt(const cln::cl_read_flags& flags, const std::string& s, uns
 }
 
 bool Integer::fitsSignedInt() const {
+  // http://www.ginac.de/CLN/cln.html#Conversions
   // TODO improve performance
-  return d_value <= std::numeric_limits<signed int>::max() &&
-    d_value >= std::numeric_limits<signed int>::min();
+  Assert(s_slowSignedIntMin <= s_fastSignedIntMin);
+  Assert(s_fastSignedIntMin <= s_fastSignedIntMax);
+  Assert(s_fastSignedIntMax <= s_slowSignedIntMax);
+
+  return (d_value <= s_fastSignedIntMax || d_value <= s_slowSignedIntMax) &&
+    (d_value >= s_fastSignedIntMin || d_value >= s_slowSignedIntMax);
 }
 
 bool Integer::fitsUnsignedInt() const {
   // TODO improve performance
-  return sgn() >= 0 && d_value <= std::numeric_limits<unsigned int>::max();
+  Assert(s_fastUnsignedIntMax <= s_slowUnsignedIntMax);
+  return sgn() >= 0 &&
+    (d_value <= s_fastUnsignedIntMax || d_value <= s_slowUnsignedIntMax);
 }
 
 signed int Integer::getSignedInt() const {
@@ -99,3 +132,5 @@ unsigned int Integer::getUnsignedInt() const {
   CheckArgument(fitsUnsignedInt(), this, "Overflow detected in Integer::getUnsignedInt()");
   return cln::cl_I_to_uint(d_value);
 }
+
+} /* namespace CVC4 */
diff --git a/src/util/integer_cln_imp.h b/src/util/integer_cln_imp.h
index 6df8d3b8e..9e5e6c2ae 100644
--- a/src/util/integer_cln_imp.h
+++ b/src/util/integer_cln_imp.h
@@ -20,14 +20,13 @@
 #ifndef __CVC4__INTEGER_H
 #define __CVC4__INTEGER_H
 
-#include <string>
-#include <sstream>
-#include <iostream>
-
-#include <cln/integer.h>
 #include <cln/input.h>
+#include <cln/integer.h>
 #include <cln/integer_io.h>
+#include <iostream>
 #include <limits>
+#include <sstream>
+#include <string>
 
 #include "base/exception.h"
 
@@ -57,6 +56,17 @@ private:
 
   void parseInt(const std::string& s, unsigned base) throw(std::invalid_argument);
 
+
+  // These constants are to help with CLN conversion in 32 bit.
+  // See http://www.ginac.de/CLN/cln.html#Conversions
+  static signed int s_fastSignedIntMax; /*  2^29 - 1 */
+  static signed int s_fastSignedIntMin; /* -2^29 */
+  static unsigned int s_fastUnsignedIntMax; /* 2^29 - 1 */
+
+  static signed long s_slowSignedIntMax; /*  std::numeric_limits<signed int>::max() */
+  static signed long s_slowSignedIntMin; /*  std::numeric_limits<signed int>::min() */
+  static unsigned long s_slowUnsignedIntMax; /*  std::numeric_limits<unsigned int>::max() */
+
 public:
 
   /** Constructs a rational with the value 0. */
@@ -186,14 +196,7 @@ public:
     return Integer(cln::logior(d_value, mask));
   }
 
-  Integer oneExtend(uint32_t size, uint32_t amount) const {
-    DebugCheckArgument((*this) < Integer(1).multiplyByPow2(size), size);
-    cln::cl_byte range(amount, size);
-    cln::cl_I allones = (cln::cl_I(1) << (size + amount))- 1; // 2^size - 1
-    Integer temp(allones);
-
-    return Integer(cln::deposit_field(allones, d_value, range));
-  }
+  Integer oneExtend(uint32_t size, uint32_t amount) const;
 
   uint32_t toUnsignedInt() const {
     return cln::cl_I_to_uint(d_value);
@@ -300,10 +303,7 @@ public:
   /**
    * If y divides *this, then exactQuotient returns (this/y)
    */
-  Integer exactQuotient(const Integer& y) const {
-    DebugCheckArgument(y.divides(*this), y);
-    return Integer( cln::exquo(d_value, y.d_value) );
-  }
+  Integer exactQuotient(const Integer& y) const;
 
   Integer modByPow2(uint32_t exp) const {
     cln::cl_byte range(exp, 0);
diff --git a/src/util/integer_gmp_imp.cpp b/src/util/integer_gmp_imp.cpp
index bde759219..df1bd297a 100644
--- a/src/util/integer_gmp_imp.cpp
+++ b/src/util/integer_gmp_imp.cpp
@@ -21,16 +21,18 @@
 #include <string>
 
 #include "cvc4autoconfig.h"
+
+#include "base/cvc4_assert.h"
 #include "util/rational.h"
 
 #ifndef CVC4_GMP_IMP
 #  error "This source should only ever be built if CVC4_GMP_IMP is on !"
 #endif /* CVC4_GMP_IMP */
 
-using namespace std;
-using namespace CVC4;
 
+using namespace std;
 
+namespace CVC4 {
 
 Integer::Integer(const char* s, unsigned base)
   : d_value(s, base)
@@ -52,10 +54,11 @@ bool Integer::fitsUnsignedInt() const {
 signed int Integer::getSignedInt() const {
   // ensure there isn't overflow
   CheckArgument(d_value <= std::numeric_limits<int>::max(), this,
-                "Overflow detected in Integer::getSignedInt()");
+                "Overflow detected in Integer::getSignedInt().");
   CheckArgument(d_value >= std::numeric_limits<int>::min(), this,
-                "Overflow detected in Integer::getSignedInt()");
-  CheckArgument(fitsSignedInt(), this, "Overflow detected in Integer::getSignedInt()");
+                "Overflow detected in Integer::getSignedInt().");
+  CheckArgument(fitsSignedInt(), this,
+                "Overflow detected in Integer::getSignedInt().");
   return (signed int) d_value.get_si();
 }
 
@@ -65,6 +68,28 @@ unsigned int Integer::getUnsignedInt() const {
                 "Overflow detected in Integer::getUnsignedInt()");
   CheckArgument(d_value >= std::numeric_limits<unsigned int>::min(), this,
                 "Overflow detected in Integer::getUnsignedInt()");
-  CheckArgument(fitsSignedInt(), this, "Overflow detected in Integer::getUnsignedInt()");
+  CheckArgument(fitsSignedInt(), this,
+                "Overflow detected in Integer::getUnsignedInt()");
   return (unsigned int) d_value.get_ui();
 }
+
+Integer Integer::oneExtend(uint32_t size, uint32_t amount) const {
+  // check that the size is accurate
+  DebugCheckArgument((*this) < Integer(1).multiplyByPow2(size), size);
+  mpz_class res = d_value;
+
+  for (unsigned i = size; i < size + amount; ++i) {
+    mpz_setbit(res.get_mpz_t(), i);
+  }
+
+  return Integer(res);
+}
+
+Integer Integer::exactQuotient(const Integer& y) const {
+  DebugCheckArgument(y.divides(*this), y);
+  mpz_class q;
+  mpz_divexact(q.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t());
+  return Integer( q );
+}
+
+} /* namespace CVC4 */
diff --git a/src/util/integer_gmp_imp.h b/src/util/integer_gmp_imp.h
index 0d3122cd8..9cae16222 100644
--- a/src/util/integer_gmp_imp.h
+++ b/src/util/integer_gmp_imp.h
@@ -21,7 +21,7 @@
 #define __CVC4__INTEGER_H
 
 #include <string>
-#include <iostream>
+#include <iosfwd>
 #include <limits>
 
 #include "base/exception.h"
@@ -190,17 +190,7 @@ public:
    * Returns the integer with the binary representation of size bits
    * extended with amount 1's
    */
-  Integer oneExtend(uint32_t size, uint32_t amount) const {
-    // check that the size is accurate
-    DebugCheckArgument((*this) < Integer(1).multiplyByPow2(size), size);
-    mpz_class res = d_value;
-
-    for (unsigned i = size; i < size + amount; ++i) {
-      mpz_setbit(res.get_mpz_t(), i);
-    }
-
-    return Integer(res);
-  }
+  Integer oneExtend(uint32_t size, uint32_t amount) const;
 
   uint32_t toUnsignedInt() const {
     return  mpz_get_ui(d_value.get_mpz_t());
@@ -319,12 +309,7 @@ public:
   /**
    * If y divides *this, then exactQuotient returns (this/y)
    */
-  Integer exactQuotient(const Integer& y) const {
-    DebugCheckArgument(y.divides(*this), y);
-    mpz_class q;
-    mpz_divexact(q.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t());
-    return Integer( q );
-  }
+  Integer exactQuotient(const Integer& y) const;
 
   /**
    * Returns y mod 2^exp
@@ -430,14 +415,15 @@ public:
     long si = d_value.get_si();
     // ensure there wasn't overflow
     CheckArgument(mpz_cmp_si(d_value.get_mpz_t(), si) == 0, this,
-                 "Overflow detected in Integer::getLong()");
+                 "Overflow detected in Integer::getLong().");
     return si;
   }
+
   unsigned long getUnsignedLong() const {
     unsigned long ui = d_value.get_ui();
     // ensure there wasn't overflow
     CheckArgument(mpz_cmp_ui(d_value.get_mpz_t(), ui) == 0, this,
-                  "Overflow detected in Integer::getUnsignedLong()");
+                  "Overflow detected in Integer::getUnsignedLong().");
     return ui;
   }
 
diff --git a/src/util/proof.h b/src/util/proof.h
index be1e2a8e2..22d9f97d5 100644
--- a/src/util/proof.h
+++ b/src/util/proof.h
@@ -20,7 +20,7 @@
 #ifndef __CVC4__PROOF_H
 #define __CVC4__PROOF_H
 
-#include <iostream>
+#include <iosfwd>
 
 namespace CVC4 {
 
diff --git a/src/util/rational_cln_imp.cpp b/src/util/rational_cln_imp.cpp
index 5044aff18..608b33f2b 100644
--- a/src/util/rational_cln_imp.cpp
+++ b/src/util/rational_cln_imp.cpp
@@ -24,8 +24,11 @@
 #  error "This source should only ever be built if CVC4_CLN_IMP is on !"
 #endif /* CVC4_CLN_IMP */
 
+#include "base/cvc4_assert.h"
+
 using namespace std;
-using namespace CVC4;
+
+namespace CVC4 {
 
 /* Computes a rational given a decimal string. The rational
  * version of <code>xxx.yyy</code> is <code>xxxyyy/(10^3)</code>.
@@ -48,7 +51,7 @@ Rational Rational::fromDecimal(const std::string& dec) {
   }
 }
 
-std::ostream& CVC4::operator<<(std::ostream& os, const Rational& q){
+std::ostream& operator<<(std::ostream& os, const Rational& q){
   return os << q.toString();
 }
 
@@ -105,3 +108,5 @@ RationalFromDoubleException::RationalFromDoubleException(double d) throw()
   ss << ")";
   setMessage(ss.str());
 }
+
+} /* namespace CVC4 */
diff --git a/src/util/rational_gmp_imp.cpp b/src/util/rational_gmp_imp.cpp
index f0f7d46eb..63fb8e05c 100644
--- a/src/util/rational_gmp_imp.cpp
+++ b/src/util/rational_gmp_imp.cpp
@@ -21,15 +21,18 @@
 
 #include "cvc4autoconfig.h"
 
-#ifndef CVC4_GMP_IMP
+#ifndef CVC4_GMP_IMP // Make sure this comes after cvc4autoconfig.h
 #  error "This source should only ever be built if CVC4_GMP_IMP is on !"
 #endif /* CVC4_GMP_IMP */
 
-std::ostream& CVC4::operator<<(std::ostream& os, const Rational& q){
+#include "base/cvc4_assert.h"
+
+namespace CVC4 {
+
+std::ostream& operator<<(std::ostream& os, const Rational& q){
   return os << q.toString();
 }
 
-namespace CVC4 {
 
 /* Computes a rational given a decimal string. The rational
  * version of <code>xxx.yyy</code> is <code>xxxyyy/(10^3)</code>.
diff --git a/src/util/subrange_bound.cpp b/src/util/subrange_bound.cpp
new file mode 100644
index 000000000..5d66b75ad
--- /dev/null
+++ b/src/util/subrange_bound.cpp
@@ -0,0 +1,63 @@
+/*********************                                                        */
+/*! \file subrange_bound.cpp
+ ** \verbatim
+ ** Original author: Tim King
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2015  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Representation of subrange bounds
+ **
+ ** Simple class to represent a subrange bound, either infinite
+ ** (no bound) or finite (an arbitrary precision integer).
+ **/
+
+#include "util/subrange_bound.h"
+
+#include <limits>
+
+#include "base/cvc4_assert.h"
+#include "base/exception.h"
+#include "util/integer.h"
+
+namespace CVC4 {
+
+std::ostream& operator<<(std::ostream& out, const SubrangeBounds& bounds)
+throw() {
+  out << bounds.lower << ".." << bounds.upper;
+
+  return out;
+}
+
+/** Get the finite SubrangeBound, failing an assertion if infinite. */
+const Integer& SubrangeBound::getBound() const throw(IllegalArgumentException) {
+  PrettyCheckArgument(!d_nobound, this, "SubrangeBound is infinite");
+  return d_bound;
+}
+
+SubrangeBounds::SubrangeBounds(const SubrangeBound& l,
+                               const SubrangeBound& u)
+    : lower(l)
+    , upper(u)
+{
+  PrettyCheckArgument(!l.hasBound() || !u.hasBound() ||
+                      l.getBound() <= u.getBound(),
+                      l, "Bad subrange bounds specified");
+}
+
+bool SubrangeBounds::joinIsBounded(const SubrangeBounds& a, const SubrangeBounds& b){
+  return (a.lower.hasBound() && b.lower.hasBound()) ||
+    (a.upper.hasBound() && b.upper.hasBound());
+}
+
+SubrangeBounds SubrangeBounds::join(const SubrangeBounds& a, const SubrangeBounds& b){
+  DebugCheckArgument(joinIsBounded(a,b), a);
+  SubrangeBound newLower = SubrangeBound::min(a.lower, b.lower);
+  SubrangeBound newUpper = SubrangeBound::max(a.upper, b.upper);
+  return SubrangeBounds(newLower, newUpper);
+}
+
+} /* namespace CVC4 */
diff --git a/src/util/subrange_bound.h b/src/util/subrange_bound.h
index 6cff7133c..d5b50bf4c 100644
--- a/src/util/subrange_bound.h
+++ b/src/util/subrange_bound.h
@@ -34,9 +34,6 @@ namespace CVC4 {
  * has a lower bound of -5 and an infinite upper bound.
  */
 class CVC4_PUBLIC SubrangeBound {
-  bool d_nobound;
-  Integer d_bound;
-
 public:
 
   /** Construct an infinite SubrangeBound. */
@@ -55,10 +52,7 @@ public:
   }
 
   /** Get the finite SubrangeBound, failing an assertion if infinite. */
-  const Integer& getBound() const throw(IllegalArgumentException) {
-    CheckArgument(!d_nobound, this, "SubrangeBound is infinite");
-    return d_bound;
-  }
+  const Integer& getBound() const throw(IllegalArgumentException);
 
   /** Returns true iff this is a finite SubrangeBound. */
   bool hasBound() const throw() {
@@ -145,6 +139,9 @@ public:
     }
  }
 
+private:
+  bool d_nobound;
+  Integer d_bound;
 };/* class SubrangeBound */
 
 class CVC4_PUBLIC SubrangeBounds {
@@ -153,13 +150,7 @@ public:
   SubrangeBound lower;
   SubrangeBound upper;
 
-  SubrangeBounds(const SubrangeBound& l, const SubrangeBound& u) :
-    lower(l),
-    upper(u) {
-    CheckArgument(!l.hasBound() || !u.hasBound() ||
-                  l.getBound() <= u.getBound(),
-                  l, "Bad subrange bounds specified");
-  }
+  SubrangeBounds(const SubrangeBound& l, const SubrangeBound& u);
 
   bool operator==(const SubrangeBounds& bounds) const {
     return lower == bounds.lower && upper == bounds.upper;
@@ -210,21 +201,13 @@ public:
   /**
    * Returns true if the join of two subranges is not (- infinity, + infinity).
    */
-  static bool joinIsBounded(const SubrangeBounds& a, const SubrangeBounds& b){
-    return (a.lower.hasBound() && b.lower.hasBound()) ||
-      (a.upper.hasBound() && b.upper.hasBound());
-  }
+  static bool joinIsBounded(const SubrangeBounds& a, const SubrangeBounds& b);
 
   /**
    * Returns the join of two subranges, a and b.
    * precondition: joinIsBounded(a,b) is true
    */
-  static SubrangeBounds join(const SubrangeBounds& a, const SubrangeBounds& b){
-    DebugCheckArgument(joinIsBounded(a,b), a);
-    SubrangeBound newLower = SubrangeBound::min(a.lower, b.lower);
-    SubrangeBound newUpper = SubrangeBound::max(a.upper, b.upper);
-    return SubrangeBounds(newLower, newUpper);
-  }
+  static SubrangeBounds join(const SubrangeBounds& a, const SubrangeBounds& b);
 
 };/* class SubrangeBounds */
 
@@ -252,15 +235,8 @@ operator<<(std::ostream& out, const SubrangeBound& bound) throw() {
   return out;
 }
 
-inline std::ostream&
-operator<<(std::ostream& out, const SubrangeBounds& bounds) throw() CVC4_PUBLIC;
-
-inline std::ostream&
-operator<<(std::ostream& out, const SubrangeBounds& bounds) throw() {
-  out << bounds.lower << ".." << bounds.upper;
-
-  return out;
-}
+std::ostream& operator<<(std::ostream& out, const SubrangeBounds& bounds)
+throw() CVC4_PUBLIC;
 
 }/* CVC4 namespace */
 
diff --git a/test/unit/expr/attribute_black.h b/test/unit/expr/attribute_black.h
index 5f9a7ebce..d162171d6 100644
--- a/test/unit/expr/attribute_black.h
+++ b/test/unit/expr/attribute_black.h
@@ -145,7 +145,7 @@ public:
   }
 
   class Foo {
-    int blah;
+    int blah CVC4_UNUSED;
   public:
     Foo(int b) : blah(b) {}
   };