Public interface review items:

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

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

20 files changed, 375 insertions, 196 deletions

diff --git a/src/util/Assert.cpp b/src/util/Assert.cpp
index 11745ad26..e299bef1d 100644
--- a/src/util/Assert.cpp
+++ b/src/util/Assert.cpp
@@ -27,7 +27,7 @@ using namespace std;
 namespace CVC4 {
 
 #ifdef CVC4_DEBUG
-CVC4_THREADLOCAL_PUBLIC(const char*) s_debugLastException = NULL;
+CVC4_THREADLOCAL(const char*) s_debugLastException = NULL;
 #endif /* CVC4_DEBUG */
 
 void AssertionException::construct(const char* header, const char* extra,
diff --git a/src/util/Assert.h b/src/util/Assert.h
index 3334de4a0..4a6fe4d3a 100644
--- a/src/util/Assert.h
+++ b/src/util/Assert.h
@@ -16,7 +16,7 @@
  ** Assertion utility classes, functions, exceptions, and macros.
  **/
 
-#include "cvc4_public.h"
+#include "cvc4_private.h"
 
 #ifndef __CVC4__ASSERT_H
 #define __CVC4__ASSERT_H
@@ -36,7 +36,7 @@
 
 namespace CVC4 {
 
-class CVC4_PUBLIC AssertionException : public Exception {
+class AssertionException : public Exception {
 protected:
   void construct(const char* header, const char* extra,
                  const char* function, const char* file,
@@ -75,7 +75,7 @@ public:
   }
 };/* class AssertionException */
 
-class CVC4_PUBLIC UnreachableCodeException : public AssertionException {
+class UnreachableCodeException : public AssertionException {
 protected:
   UnreachableCodeException() : AssertionException() {}
 
@@ -97,7 +97,7 @@ public:
   }
 };/* class UnreachableCodeException */
 
-class CVC4_PUBLIC UnhandledCaseException : public UnreachableCodeException {
+class UnhandledCaseException : public UnreachableCodeException {
 protected:
   UnhandledCaseException() : UnreachableCodeException() {}
 
@@ -129,7 +129,7 @@ public:
   }
 };/* class UnhandledCaseException */
 
-class CVC4_PUBLIC UnimplementedOperationException : public AssertionException {
+class UnimplementedOperationException : public AssertionException {
 protected:
   UnimplementedOperationException() : AssertionException() {}
 
@@ -151,14 +151,14 @@ public:
   }
 };/* class UnimplementedOperationException */
 
-class CVC4_PUBLIC IllegalArgumentException : public AssertionException {
+class AssertArgumentException : public AssertionException {
 protected:
-  IllegalArgumentException() : AssertionException() {}
+  AssertArgumentException() : AssertionException() {}
 
 public:
-  IllegalArgumentException(const char* argDesc, const char* function,
-                           const char* file, unsigned line,
-                           const char* fmt, ...) :
+  AssertArgumentException(const char* argDesc, const char* function,
+                          const char* file, unsigned line,
+                          const char* fmt, ...) :
     AssertionException() {
     va_list args;
     va_start(args, fmt);
@@ -168,17 +168,17 @@ public:
     va_end(args);
   }
 
-  IllegalArgumentException(const char* argDesc, const char* function,
-                           const char* file, unsigned line) :
+  AssertArgumentException(const char* argDesc, const char* function,
+                          const char* file, unsigned line) :
     AssertionException() {
     construct("Illegal argument detected",
               ( std::string("`") + argDesc + "' is a bad argument" ).c_str(),
               function, file, line);
   }
 
-  IllegalArgumentException(const char* condStr, const char* argDesc,
-                           const char* function, const char* file,
-                           unsigned line, const char* fmt, ...) :
+  AssertArgumentException(const char* condStr, const char* argDesc,
+                          const char* function, const char* file,
+                          unsigned line, const char* fmt, ...) :
     AssertionException() {
     va_list args;
     va_start(args, fmt);
@@ -189,18 +189,18 @@ public:
     va_end(args);
   }
 
-  IllegalArgumentException(const char* condStr, const char* argDesc,
-                           const char* function, const char* file,
-                           unsigned line) :
+  AssertArgumentException(const char* condStr, const char* argDesc,
+                          const char* function, const char* file,
+                          unsigned line) :
     AssertionException() {
     construct("Illegal argument detected",
               ( std::string("`") + argDesc + "' is a bad argument; expected " +
                 condStr + " to hold" ).c_str(),
               function, file, line);
   }
-};/* class IllegalArgumentException */
+};/* class AssertArgumentException */
 
-class CVC4_PUBLIC InternalErrorException : public AssertionException {
+class InternalErrorException : public AssertionException {
 protected:
   InternalErrorException() : AssertionException() {}
 
@@ -235,7 +235,7 @@ public:
 
 #ifdef CVC4_DEBUG
 
-extern CVC4_THREADLOCAL_PUBLIC(const char*) s_debugLastException;
+extern CVC4_THREADLOCAL(const char*) s_debugLastException;
 
 /**
  * Special assertion failure handling in debug mode; in non-debug
@@ -247,8 +247,7 @@ extern CVC4_THREADLOCAL_PUBLIC(const char*) s_debugLastException;
  * debug builds only; in debug builds, it handles all assertion
  * failures (even those that exist in non-debug builds).
  */
-void debugAssertionFailed(const AssertionException& thisException,
-                          const char* lastException) CVC4_PUBLIC;
+void debugAssertionFailed(const AssertionException& thisException, const char* lastException);
 
 // If we're currently handling an exception, print a warning instead;
 // otherwise std::terminate() is called by the runtime and we lose
@@ -283,22 +282,28 @@ void debugAssertionFailed(const AssertionException& thisException,
 #define InternalError(msg...) \
   throw ::CVC4::InternalErrorException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg)
 #define IllegalArgument(arg, msg...) \
-  throw ::CVC4::IllegalArgumentException(#arg, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg)
+  throw ::CVC4::IllegalArgumentException("", #arg, __PRETTY_FUNCTION__, ## msg)
 #define CheckArgument(cond, arg, msg...)         \
-  AlwaysAssertArgument(cond, arg, ## msg)
+  do { \
+    if(EXPECT_FALSE( ! (cond) )) { \
+      throw ::CVC4::IllegalArgumentException(#cond, #arg, __PRETTY_FUNCTION__, ## msg); \
+    } \
+  } while(0)
 #define AlwaysAssertArgument(cond, arg, msg...)  \
   do { \
     if(EXPECT_FALSE( ! (cond) )) { \
-      throw ::CVC4::IllegalArgumentException(#cond, #arg, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \
+      throw ::CVC4::AssertArgumentException(#cond, #arg, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \
     } \
   } while(0)
 
 #ifdef CVC4_ASSERTIONS
 #  define Assert(cond, msg...) AlwaysAssert(cond, ## msg)
 #  define AssertArgument(cond, arg, msg...) AlwaysAssertArgument(cond, arg, ## msg)
+#  define DebugCheckArgument(cond, arg, msg...) CheckArgument(cond, arg, ## msg)
 #else /* ! CVC4_ASSERTIONS */
 #  define Assert(cond, msg...) /*EXPECT_TRUE( cond )*/
 #  define AssertArgument(cond, arg, msg...) /*EXPECT_TRUE( cond )*/
+#  define DebugCheckArgument(cond, arg, msg...) /*EXPECT_TRUE( cond )*/
 #endif /* CVC4_ASSERTIONS */
 
 }/* CVC4 namespace */
diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index 7d9a055fd..fcbadf490 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -27,6 +27,7 @@ libutil_la_SOURCES = \
 	Makefile.in \
 	debug.h \
 	exception.h \
+	exception.cpp \
 	hash.h \
 	bool.h \
 	proof.h \
diff --git a/src/util/ascription_type.h b/src/util/ascription_type.h
index 579746332..4421d6ca7 100644
--- a/src/util/ascription_type.h
+++ b/src/util/ascription_type.h
@@ -46,7 +46,7 @@ public:
 };/* class AscriptionType */
 
 /**
- * A hash strategy for type ascription operators.
+ * A hash function for type ascription operators.
  */
 struct CVC4_PUBLIC AscriptionTypeHashFunction {
   inline size_t operator()(const AscriptionType& at) const {
diff --git a/src/util/bitvector.h b/src/util/bitvector.h
index 185bb55d9..a3d4f1b60 100644
--- a/src/util/bitvector.h
+++ b/src/util/bitvector.h
@@ -23,7 +23,7 @@
 #define __CVC4__BITVECTOR_H
 
 #include <iostream>
-#include "util/Assert.h"
+#include "util/exception.h"
 #include "util/integer.h"
 
 namespace CVC4 {
@@ -99,8 +99,8 @@ public:
     return d_value != y.d_value;
   }
 
-  BitVector equals(const BitVector&  y) const {
-    Assert(d_size == y.d_size);
+  BitVector equals(const BitVector& y) const {
+    CheckArgument(d_size == y.d_size, y);
     return d_value == y.d_value; 
   }
 
@@ -118,19 +118,19 @@ public:
 
   // xor
   BitVector operator ^(const BitVector& y) const {
-    Assert (d_size == y.d_size); 
+    CheckArgument(d_size == y.d_size, y);
     return BitVector(d_size, d_value.bitwiseXor(y.d_value)); 
   }
   
   // or
   BitVector operator |(const BitVector& y) const {
-    Assert (d_size == y.d_size); 
+    CheckArgument(d_size == y.d_size, y);
     return BitVector(d_size, d_value.bitwiseOr(y.d_value)); 
   }
   
   // and
   BitVector operator &(const BitVector& y) const {
-    Assert (d_size == y.d_size); 
+    CheckArgument(d_size == y.d_size, y);
     return BitVector(d_size, d_value.bitwiseAnd(y.d_value)); 
   }
 
@@ -162,13 +162,13 @@ public:
 
   
   BitVector operator +(const BitVector& y) const {
-    Assert (d_size == y.d_size);
+    CheckArgument(d_size == y.d_size, y);
     Integer sum = d_value +  y.d_value;
     return BitVector(d_size, sum);
   }
 
   BitVector operator -(const BitVector& y) const {
-    Assert (d_size == y.d_size);
+    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)); 
@@ -181,35 +181,38 @@ public:
   }
 
   BitVector operator *(const BitVector& y) const {
-    Assert (d_size == y.d_size);
+    CheckArgument(d_size == y.d_size, y);
     Integer prod = d_value * y.d_value;
     return BitVector(d_size, prod);
   }
   
   BitVector unsignedDiv (const BitVector& y) const {
-    Assert (d_size == y.d_size);
+    CheckArgument(d_size == y.d_size, y);
     // TODO: decide whether we really want these semantics
     if (y.d_value == 0) {
       return BitVector(d_size, Integer(0));
     }
-    Assert (d_value >= 0 && y.d_value > 0); 
+    CheckArgument(d_value >= 0, this);
+    CheckArgument(y.d_value > 0, y);
     return BitVector(d_size, d_value.floorDivideQuotient(y.d_value)); 
   }
 
   BitVector unsignedRem(const BitVector& y) const {
-    Assert (d_size == y.d_size);
+    CheckArgument(d_size == y.d_size, y);
     // TODO: decide whether we really want these semantics
     if (y.d_value == 0) {
       return BitVector(d_size, Integer(0));
     }
-    Assert (d_value >= 0 && y.d_value > 0); 
+    CheckArgument(d_value >= 0, this);
+    CheckArgument(y.d_value > 0, y);
     return BitVector(d_size, d_value.floorDivideRemainder(y.d_value)); 
   }
   
   
   bool signedLessThan(const BitVector& y) const {
-    Assert(d_size == y.d_size);
-    Assert(d_value >= 0 && y.d_value >= 0);
+    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(); 
     
@@ -217,14 +220,16 @@ public:
   }
 
   bool unsignedLessThan(const BitVector& y) const {
-    Assert(d_size == y.d_size);
-    Assert(d_value >= 0 && y.d_value >= 0);
+    CheckArgument(d_size == y.d_size, y);
+    CheckArgument(d_value >= 0, this);
+    CheckArgument(y.d_value >= 0, y);
     return d_value < y.d_value; 
   }
 
   bool signedLessThanEq(const BitVector& y) const {
-    Assert(d_size == y.d_size);
-    Assert(d_value >= 0 && y.d_value >= 0);
+    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(); 
     
@@ -232,8 +237,9 @@ public:
   }
 
   bool unsignedLessThanEq(const BitVector& y) const {
-    Assert(d_size == y.d_size);
-    Assert(d_value >= 0 && y.d_value >= 0);
+    CheckArgument(d_size == y.d_size, this);
+    CheckArgument(d_value >= 0, this);
+    CheckArgument(y.d_value >= 0, y);
     return d_value <= y.d_value; 
   }
 
@@ -269,7 +275,7 @@ public:
     }
 
     // making sure we don't lose information casting
-    Assert(y.d_value < Integer(1).multiplyByPow2(32));
+    CheckArgument(y.d_value < Integer(1).multiplyByPow2(32), y);
     uint32_t amount = y.d_value.toUnsignedInt(); 
     Integer res = d_value.multiplyByPow2(amount);
     return BitVector(d_size, res);
@@ -281,7 +287,7 @@ public:
     }
 
     // making sure we don't lose information casting
-    Assert(y.d_value < Integer(1).multiplyByPow2(32));
+    CheckArgument(y.d_value < Integer(1).multiplyByPow2(32), y);
     uint32_t amount = y.d_value.toUnsignedInt(); 
     Integer res = d_value.divByPow2(amount); 
     return BitVector(d_size, res);
@@ -302,7 +308,7 @@ public:
     }
 
     // making sure we don't lose information casting
-    Assert(y.d_value < Integer(1).multiplyByPow2(32));
+    CheckArgument(y.d_value < Integer(1).multiplyByPow2(32), y);
    
     uint32_t amount  = y.d_value.toUnsignedInt();
     Integer rest = d_value.divByPow2(amount);
@@ -310,7 +316,7 @@ public:
     if(sign_bit == Integer(0)) {
       return BitVector(d_size, rest); 
     }
-    Integer res = rest.oneExtend(d_size - amount, amount); 
+    Integer res = rest.oneExtend(d_size - amount, amount);
     return BitVector(d_size, res);
   }
   
@@ -358,17 +364,15 @@ public:
 
 
 inline BitVector::BitVector(const std::string& num, unsigned base) {
-  AlwaysAssert( base == 2 || base == 16 );
+  CheckArgument(base == 2 || base == 16, base);
 
   if( base == 2 ) {
     d_size = num.size();
-  } else if( base == 16 ) {
-    d_size = num.size() * 4;
   } else {
-    Unreachable("Unsupported base in BitVector(std::string&, unsigned int).");
+    d_size = num.size() * 4;
   }
 
-  d_value = Integer(num,base);
+  d_value = Integer(num, base);
 }/* BitVector::BitVector() */
 
 
diff --git a/src/util/cardinality.h b/src/util/cardinality.h
index 81a291006..17368c157 100644
--- a/src/util/cardinality.h
+++ b/src/util/cardinality.h
@@ -26,7 +26,7 @@
 #include <utility>
 
 #include "util/integer.h"
-#include "util/Assert.h"
+#include "util/exception.h"
 
 namespace CVC4 {
 
@@ -118,7 +118,6 @@ public:
     CheckArgument(card >= 0, card,
                   "Cardinality must be a nonnegative integer, not %ld.", card);
     d_card += 1;
-    Assert(isFinite());
   }
 
   /**
@@ -130,14 +129,12 @@ public:
                   "Cardinality must be a nonnegative integer, not %s.",
                   card.toString().c_str());
     d_card += 1;
-    Assert(isFinite());
   }
 
   /**
    * Construct an infinite cardinality equal to the given Beth number.
    */
   Cardinality(CardinalityBeth beth) : d_card(-beth.getNumber() - 1) {
-    Assert(!isFinite());
   }
 
   /**
diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp
index ec8c8e166..ee9c4e406 100644
--- a/src/util/datatype.cpp
+++ b/src/util/datatype.cpp
@@ -28,6 +28,7 @@
 #include "expr/node.h"
 #include "util/recursion_breaker.h"
 #include "util/matcher.h"
+#include "util/Assert.h"
 
 using namespace std;
 
@@ -67,11 +68,11 @@ const Datatype& Datatype::datatypeOf(Expr item) {
 
 size_t Datatype::indexOf(Expr item) {
   ExprManagerScope ems(item);
-  AssertArgument(item.getType().isConstructor() ||
-                 item.getType().isTester() ||
-                 item.getType().isSelector(),
-                 item,
-                 "arg must be a datatype constructor, selector, or tester");
+  CheckArgument(item.getType().isConstructor() ||
+                item.getType().isTester() ||
+                item.getType().isSelector(),
+                item,
+                "arg must be a datatype constructor, selector, or tester");
   TNode n = Node::fromExpr(item);
   if( item.getKind()==kind::APPLY_TYPE_ASCRIPTION ){
     return indexOf( item[0] );
@@ -87,29 +88,27 @@ void Datatype::resolve(ExprManager* em,
                        const std::vector<Type>& replacements,
                        const std::vector< SortConstructorType >& paramTypes,
                        const std::vector< DatatypeType >& paramReplacements)
-  throw(AssertionException, DatatypeResolutionException) {
+  throw(IllegalArgumentException, DatatypeResolutionException) {
 
-  AssertArgument(em != NULL, "cannot resolve a Datatype with a NULL expression manager");
-  CheckArgument(!d_resolved, "cannot resolve a Datatype twice");
-  AssertArgument(resolutions.find(d_name) != resolutions.end(),
+  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,
                 "Datatype::resolve(): resolutions doesn't contain me!");
-  AssertArgument(placeholders.size() == replacements.size(), placeholders,
+  CheckArgument(placeholders.size() == replacements.size(), placeholders,
                 "placeholders and replacements must be the same size");
-  AssertArgument(paramTypes.size() == paramReplacements.size(), paramTypes,
+  CheckArgument(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");
   DatatypeType self = (*resolutions.find(d_name)).second;
-  AssertArgument(&self.getDatatype() == this, "Datatype::resolve(): resolutions doesn't contain me!");
+  CheckArgument(&self.getDatatype() == this, resolutions, "Datatype::resolve(): resolutions doesn't contain me!");
   d_resolved = true;
   size_t index = 0;
   for(iterator i = begin(), i_end = end(); i != i_end; ++i) {
     (*i).resolve(em, self, resolutions, placeholders, replacements, paramTypes, paramReplacements);
-    Assert((*i).isResolved());
     Node::fromExpr((*i).d_constructor).setAttribute(DatatypeIndexAttr(), index);
     Node::fromExpr((*i).d_tester).setAttribute(DatatypeIndexAttr(), index++);
   }
   d_self = self;
-  Assert(index == getNumConstructors());
 }
 
 void Datatype::addConstructor(const DatatypeConstructor& c) {
@@ -118,7 +117,7 @@ void Datatype::addConstructor(const DatatypeConstructor& c) {
   d_constructors.push_back(c);
 }
 
-Cardinality Datatype::getCardinality() const throw(AssertionException) {
+Cardinality Datatype::getCardinality() const throw(IllegalArgumentException) {
   CheckArgument(isResolved(), this, "this datatype is not yet resolved");
   RecursionBreaker<const Datatype*, DatatypeHashFunction> breaker(__PRETTY_FUNCTION__, this);
   if(breaker.isRecursion()) {
@@ -131,7 +130,7 @@ Cardinality Datatype::getCardinality() const throw(AssertionException) {
   return c;
 }
 
-bool Datatype::isFinite() const throw(AssertionException) {
+bool Datatype::isFinite() const throw(IllegalArgumentException) {
   CheckArgument(isResolved(), this, "this datatype is not yet resolved");
 
   // we're using some internals, so we have to set up this library context
@@ -157,7 +156,7 @@ bool Datatype::isFinite() const throw(AssertionException) {
   return true;
 }
 
-bool Datatype::isWellFounded() const throw(AssertionException) {
+bool Datatype::isWellFounded() const throw(IllegalArgumentException) {
   CheckArgument(isResolved(), this, "this datatype is not yet resolved");
 
   // we're using some internals, so we have to set up this library context
@@ -191,7 +190,7 @@ bool Datatype::isWellFounded() const throw(AssertionException) {
   return false;
 }
 
-Expr Datatype::mkGroundTerm( Type t ) const throw(AssertionException) {
+Expr Datatype::mkGroundTerm( Type t ) const throw(IllegalArgumentException) {
   CheckArgument(isResolved(), this, "this datatype is not yet resolved");
 
   // we're using some internals, so we have to set up this library context
@@ -274,16 +273,16 @@ Expr Datatype::mkGroundTerm( Type t ) const throw(AssertionException) {
   }
 }
 
-DatatypeType Datatype::getDatatypeType() const throw(AssertionException) {
+DatatypeType Datatype::getDatatypeType() const throw(IllegalArgumentException) {
   CheckArgument(isResolved(), *this, "Datatype must be resolved to get its DatatypeType");
-  Assert(!d_self.isNull() && !DatatypeType(d_self).isParametric());
+  CheckArgument(!d_self.isNull() && !DatatypeType(d_self).isParametric(), this);
   return DatatypeType(d_self);
 }
 
 DatatypeType Datatype::getDatatypeType(const std::vector<Type>& params)
-  const throw(AssertionException) {
+  const throw(IllegalArgumentException) {
   CheckArgument(isResolved(), *this, "Datatype must be resolved to get its DatatypeType");
-  Assert(!d_self.isNull() && DatatypeType(d_self).isParametric());
+  CheckArgument(!d_self.isNull() && DatatypeType(d_self).isParametric(), this);
   return DatatypeType(d_self).instantiate(params);
 }
 
@@ -394,9 +393,9 @@ void DatatypeConstructor::resolve(ExprManager* em, DatatypeType self,
                                   const std::vector<Type>& replacements,
                                   const std::vector< SortConstructorType >& paramTypes,
                                   const std::vector< DatatypeType >& paramReplacements)
-  throw(AssertionException, DatatypeResolutionException) {
+  throw(IllegalArgumentException, DatatypeResolutionException) {
 
-  AssertArgument(em != NULL, "cannot resolve a Datatype with a NULL expression manager");
+  CheckArgument(em != NULL, em, "cannot resolve a Datatype with a NULL expression manager");
   CheckArgument(!isResolved(),
                 "cannot resolve a Datatype constructor twice; "
                 "perhaps the same constructor was added twice, "
@@ -577,7 +576,7 @@ Expr DatatypeConstructor::getTester() const {
   return d_tester;
 }
 
-Cardinality DatatypeConstructor::getCardinality() const throw(AssertionException) {
+Cardinality DatatypeConstructor::getCardinality() const throw(IllegalArgumentException) {
   CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
 
   Cardinality c = 1;
@@ -589,7 +588,7 @@ Cardinality DatatypeConstructor::getCardinality() const throw(AssertionException
   return c;
 }
 
-bool DatatypeConstructor::isFinite() const throw(AssertionException) {
+bool DatatypeConstructor::isFinite() const throw(IllegalArgumentException) {
   CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
 
   // we're using some internals, so we have to set up this library context
@@ -615,7 +614,7 @@ bool DatatypeConstructor::isFinite() const throw(AssertionException) {
   return true;
 }
 
-bool DatatypeConstructor::isWellFounded() const throw(AssertionException) {
+bool DatatypeConstructor::isWellFounded() const throw(IllegalArgumentException) {
   CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
 
   // we're using some internals, so we have to set up this library context
@@ -659,7 +658,7 @@ bool DatatypeConstructor::isWellFounded() const throw(AssertionException) {
   return true;
 }
 
-Expr DatatypeConstructor::mkGroundTerm( Type t ) const throw(AssertionException) {
+Expr DatatypeConstructor::mkGroundTerm( Type t ) const throw(IllegalArgumentException) {
   CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
 
   // we're using some internals, so we have to set up this library context
@@ -684,7 +683,7 @@ Expr DatatypeConstructor::mkGroundTerm( Type t ) const throw(AssertionException)
   groundTerms.push_back(getConstructor());
 
   // for each selector, get a ground term
-  Assert( t.isDatatype() );
+  CheckArgument( t.isDatatype(), t );
   std::vector< Type > instTypes;
   std::vector< Type > paramTypes;
   if( DatatypeType(t).isParametric() ){
diff --git a/src/util/datatype.h b/src/util/datatype.h
index 9853ba417..86bd1cfe3 100644
--- a/src/util/datatype.h
+++ b/src/util/datatype.h
@@ -35,7 +35,6 @@ namespace CVC4 {
 
 #include "expr/expr.h"
 #include "expr/type.h"
-#include "util/Assert.h"
 #include "util/output.h"
 #include "util/hash.h"
 #include "util/exception.h"
@@ -155,7 +154,7 @@ private:
                const std::vector<Type>& replacements,
                const std::vector< SortConstructorType >& paramTypes,
                const std::vector< DatatypeType >& paramReplacements)
-    throw(AssertionException, DatatypeResolutionException);
+    throw(IllegalArgumentException, DatatypeResolutionException);
   friend class Datatype;
 
   /** Helper function for resolving parametric datatypes.
@@ -260,28 +259,28 @@ public:
    * Return the cardinality of this constructor (the product of the
    * cardinalities of its arguments).
    */
-  Cardinality getCardinality() const throw(AssertionException);
+  Cardinality getCardinality() const throw(IllegalArgumentException);
 
   /**
    * Return true iff this constructor is finite (it is nullary or
    * each of its argument types are finite).  This function can
    * only be called for resolved constructors.
    */
-  bool isFinite() const throw(AssertionException);
+  bool isFinite() const throw(IllegalArgumentException);
 
   /**
    * Return true iff this constructor is well-founded (there exist
    * ground terms).  The constructor must be resolved or an
    * exception is thrown.
    */
-  bool isWellFounded() const throw(AssertionException);
+  bool isWellFounded() const throw(IllegalArgumentException);
 
   /**
    * Construct and return a ground term of this constructor.  The
    * constructor must be both resolved and well-founded, or else an
    * exception is thrown.
    */
-  Expr mkGroundTerm( Type t ) const throw(AssertionException);
+  Expr mkGroundTerm( Type t ) const throw(IllegalArgumentException);
 
   /**
    * Returns true iff this Datatype constructor has already been
@@ -441,7 +440,7 @@ private:
                const std::vector<Type>& replacements,
                const std::vector< SortConstructorType >& paramTypes,
                const std::vector< DatatypeType >& paramReplacements)
-    throw(AssertionException, DatatypeResolutionException);
+    throw(IllegalArgumentException, DatatypeResolutionException);
   friend class ExprManager;// for access to resolve()
 
 public:
@@ -484,7 +483,7 @@ public:
    * cardinalities of its constructors).  The Datatype must be
    * resolved.
    */
-  Cardinality getCardinality() const throw(AssertionException);
+  Cardinality getCardinality() const throw(IllegalArgumentException);
 
   /**
    * Return  true iff this  Datatype is  finite (all  constructors are
@@ -492,32 +491,32 @@ public:
    * datatype is  not well-founded, this function  returns false.  The
    * Datatype must be resolved or an exception is thrown.
    */
-  bool isFinite() const throw(AssertionException);
+  bool isFinite() const throw(IllegalArgumentException);
 
   /**
    * Return true iff this datatype is well-founded (there exist ground
    * terms).  The Datatype must be resolved or an exception is thrown.
    */
-  bool isWellFounded() const throw(AssertionException);
+  bool isWellFounded() const throw(IllegalArgumentException);
 
   /**
    * Construct and return a ground term of this Datatype.  The
    * Datatype must be both resolved and well-founded, or else an
    * exception is thrown.
    */
-  Expr mkGroundTerm( Type t ) const throw(AssertionException);
+  Expr mkGroundTerm( Type t ) const throw(IllegalArgumentException);
 
   /**
    * Get the DatatypeType associated to this Datatype.  Can only be
    * called post-resolution.
    */
-  DatatypeType getDatatypeType() const throw(AssertionException);
+  DatatypeType getDatatypeType() const throw(IllegalArgumentException);
 
   /**
    * Get the DatatypeType associated to this (parameterized) Datatype.  Can only be
    * called post-resolution.
    */
-  DatatypeType getDatatypeType(const std::vector<Type>& params) const throw(AssertionException);
+  DatatypeType getDatatypeType(const std::vector<Type>& params) const throw(IllegalArgumentException);
 
   /**
    * Return true iff the two Datatypes are the same.
diff --git a/src/util/exception.cpp b/src/util/exception.cpp
new file mode 100644
index 000000000..d31f52fe7
--- /dev/null
+++ b/src/util/exception.cpp
@@ -0,0 +1,102 @@
+/*********************                                                        */
+/*! \file exception.cpp
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief CVC4's exception base class and some associated utilities
+ **
+ ** CVC4's exception base class and some associated utilities.
+ **/
+
+#include "util/exception.h"
+#include <string>
+#include <cstdio>
+#include <cstdlib>
+#include <cstdarg>
+
+using namespace std;
+using namespace CVC4;
+
+void IllegalArgumentException::construct(const char* header, const char* extra,
+                                         const char* function, const char* fmt,
+                                         va_list args) {
+  // try building the exception msg with a smallish buffer first,
+  // then with a larger one if sprintf tells us to.
+  int n = 512;
+  char* buf;
+
+  for(;;) {
+    buf = new char[n];
+
+    int size;
+    if(extra == NULL) {
+      size = snprintf(buf, n, "%s\n%s\n",
+                      header, function);
+    } else {
+      size = snprintf(buf, n, "%s\n%s\n\n  %s\n",
+                      header, function, extra);
+    }
+
+    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) {
+      // try again with a buffer that's large enough
+      n = size + 1;
+      delete [] buf;
+    }
+  }
+
+  setMessage(string(buf));
+
+  delete [] buf;
+}
+
+void IllegalArgumentException::construct(const char* header, const char* extra,
+                                         const char* function) {
+  // try building the exception msg with a smallish buffer first,
+  // then with a larger one if sprintf tells us to.
+  int n = 256;
+  char* buf;
+
+  for(;;) {
+    buf = new char[n];
+
+    int size;
+    if(extra == NULL) {
+      size = snprintf(buf, n, "%s.\n%s\n",
+                      header, function);
+    } else {
+      size = snprintf(buf, n, "%s.\n%s\n\n  %s\n",
+                      header, function, extra);
+    }
+
+    if(size < n) {
+      break;
+    } else {
+      // try again with a buffer that's large enough
+      n = size + 1;
+      delete [] buf;
+    }
+  }
+
+  setMessage(string(buf));
+
+  delete [] buf;
+}
diff --git a/src/util/exception.h b/src/util/exception.h
index fe01eba36..89e42b6d1 100644
--- a/src/util/exception.h
+++ b/src/util/exception.h
@@ -11,7 +11,7 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
- ** \brief CVC4's exception base class and some associated utilities.
+ ** \brief CVC4's exception base class and some associated utilities
  **
  ** CVC4's exception base class and some associated utilities.
  **/
@@ -25,6 +25,8 @@
 #include <string>
 #include <sstream>
 #include <exception>
+#include <cstdlib>
+#include <cstdarg>
 
 namespace CVC4 {
 
@@ -75,6 +77,51 @@ public:
 
 };/* class Exception */
 
+class CVC4_PUBLIC IllegalArgumentException : public Exception {
+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);
+
+  void construct(const char* header, const char* extra,
+                 const char* function);
+
+public:
+  IllegalArgumentException(const char* condStr, const char* argDesc,
+                           const char* function, const char* fmt, ...) :
+    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);
+  }
+
+  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);
+  }
+};/* class IllegalArgumentException */
+
 inline std::ostream& operator<<(std::ostream& os, const Exception& e) throw() CVC4_PUBLIC;
 inline std::ostream& operator<<(std::ostream& os, const Exception& e) throw() {
   e.toStream(os);
@@ -83,4 +130,42 @@ inline std::ostream& operator<<(std::ostream& os, const Exception& e) throw() {
 
 }/* CVC4 namespace */
 
+#if defined(__BUILDING_CVC4LIB) || defined(__BUILDING_CVC4LIB_UNIT_TEST)
+#  include "util/Assert.h"
+#endif /* __BUILDING_CVC4LIB || __BUILDING_CVC4LIB_UNIT_TEST */
+
+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, ...) {
+  if(EXPECT_FALSE( !cond )) { \
+    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) {
+  if(EXPECT_FALSE( !cond )) { \
+    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(EXPECT_FALSE( !cond )) { \
+    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(EXPECT_FALSE( !cond )) { \
+    throw ::CVC4::IllegalArgumentException("", "", ""); \
+  } \
+}
+#endif /* DebugCheckArgument */
+
+}/* CVC4 namespace */
+
 #endif /* __CVC4__EXCEPTION_H */
diff --git a/src/util/integer_cln_imp.h b/src/util/integer_cln_imp.h
index 7fd6a2694..5dfcae6d2 100644
--- a/src/util/integer_cln_imp.h
+++ b/src/util/integer_cln_imp.h
@@ -31,7 +31,7 @@
 #include <cln/integer_io.h>
 #include <limits>
 
-#include "util/Assert.h"
+#include "util/exception.h"
 
 namespace CVC4 {
 
@@ -232,7 +232,7 @@ public:
   }
 
   Integer oneExtend(uint32_t size, uint32_t amount) const {
-    Assert((*this) < Integer(1).multiplyByPow2(size));
+    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);
@@ -291,7 +291,7 @@ public:
    * If y divides *this, then exactQuotient returns (this/y)
    */
   Integer exactQuotient(const Integer& y) const {
-    Assert(y.divides(*this));
+    DebugCheckArgument(y.divides(*this), y);
     return Integer( cln::exquo(d_value, y.d_value) );
   }
 
@@ -316,7 +316,7 @@ public:
     }else if(exp == 0){
       return Integer( 1 );
     }else{
-      Unimplemented();
+      throw Exception("Negative exponent in Integer::pow()");
     }
   }
 
@@ -367,8 +367,7 @@ public:
       fprinthexadecimal(ss,d_value);
       break;
     default:
-      Unhandled();
-      break;
+      throw Exception("Unhandled base in Integer::toString()");
     }
     std::string output = ss.str();
     for( unsigned i = 0; i <= output.length(); ++i){
@@ -382,7 +381,6 @@ public:
 
   int sgn() const {
     cln::cl_I sgn = cln::signum(d_value);
-    Assert(sgn == 0 || sgn == -1 || sgn == 1);
     return cln::cl_I_to_int(sgn);
   }
 
@@ -402,19 +400,19 @@ public:
 
   long getLong() const {
     // ensure there isn't overflow
-    AlwaysAssert(d_value <= std::numeric_limits<long>::max(),
-                 "Overflow detected in Integer::getLong()");
-    AlwaysAssert(d_value >= std::numeric_limits<long>::min(),
-                 "Overflow detected in Integer::getLong()");
+    CheckArgument(d_value <= std::numeric_limits<long>::max(), this,
+                  "Overflow detected in Integer::getLong()");
+    CheckArgument(d_value >= std::numeric_limits<long>::min(), this,
+                  "Overflow detected in Integer::getLong()");
     return cln::cl_I_to_long(d_value);
   }
 
   unsigned long getUnsignedLong() const {
     // ensure there isn't overflow
-    AlwaysAssert(d_value <= std::numeric_limits<unsigned long>::max(),
-                 "Overflow detected in Integer::getUnsignedLong()");
-    AlwaysAssert(d_value >= std::numeric_limits<unsigned long>::min(),
-                 "Overflow detected in Integer::getUnsignedLong()");
+    CheckArgument(d_value <= std::numeric_limits<unsigned long>::max(), this,
+                  "Overflow detected in Integer::getUnsignedLong()");
+    CheckArgument(d_value >= std::numeric_limits<unsigned long>::min(), this,
+                  "Overflow detected in Integer::getUnsignedLong()");
     return cln::cl_I_to_ulong(d_value);
   }
 
diff --git a/src/util/integer_gmp_imp.h b/src/util/integer_gmp_imp.h
index 5b6468a9e..66428ec41 100644
--- a/src/util/integer_gmp_imp.h
+++ b/src/util/integer_gmp_imp.h
@@ -25,8 +25,8 @@
 #include <string>
 #include <iostream>
 
-#include "util/Assert.h"
 #include "util/gmp_util.h"
+#include "util/exception.h"
 
 namespace CVC4 {
 
@@ -178,7 +178,7 @@ public:
    */
   Integer oneExtend(uint32_t size, uint32_t amount) const {
     // check that the size is accurate
-    Assert ((*this) < Integer(1).multiplyByPow2(size));
+    DebugCheckArgument((*this) < Integer(1).multiplyByPow2(size), size);
     mpz_class res = d_value;
 
     for (unsigned i = size; i < size + amount; ++i) {
@@ -251,7 +251,7 @@ public:
    * If y divides *this, then exactQuotient returns (this/y)
    */
   Integer exactQuotient(const Integer& y) const {
-    Assert(y.divides(*this));
+    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 );
@@ -346,15 +346,15 @@ public:
   long getLong() const {
     long si = d_value.get_si();
     // ensure there wasn't overflow
-    AlwaysAssert(mpz_cmp_si(d_value.get_mpz_t(), si) == 0,
+    CheckArgument(mpz_cmp_si(d_value.get_mpz_t(), si) == 0, this,
                  "Overflow detected in Integer::getLong()");
     return si;
   }
   unsigned long getUnsignedLong() const {
     unsigned long ui = d_value.get_ui();
     // ensure there wasn't overflow
-    AlwaysAssert(mpz_cmp_ui(d_value.get_mpz_t(), ui) == 0,
-                 "Overflow detected in Integer::getUnsignedLong()");
+    CheckArgument(mpz_cmp_ui(d_value.get_mpz_t(), ui) == 0, this,
+                  "Overflow detected in Integer::getUnsignedLong()");
     return ui;
   }
 
diff --git a/src/util/predicate.h b/src/util/predicate.h
index 18e0b8b70..ba050bd43 100644
--- a/src/util/predicate.h
+++ b/src/util/predicate.h
@@ -23,7 +23,7 @@
 #ifndef __CVC4__PREDICATE_H
 #define __CVC4__PREDICATE_H
 
-#include "util/Assert.h"
+#include "util/exception.h"
 
 namespace CVC4 {
 
diff --git a/src/util/rational_cln_imp.h b/src/util/rational_cln_imp.h
index 182e813cd..575f09ef5 100644
--- a/src/util/rational_cln_imp.h
+++ b/src/util/rational_cln_imp.h
@@ -25,6 +25,7 @@
 #include <gmp.h>
 #include <string>
 #include <sstream>
+#include <cassert>
 #include <cln/rational.h>
 #include <cln/input.h>
 #include <cln/io.h>
@@ -32,7 +33,7 @@
 #include <cln/rational_io.h>
 #include <cln/number_io.h>
 
-#include "util/Assert.h"
+#include "util/exception.h"
 #include "util/integer.h"
 
 namespace CVC4 {
@@ -213,7 +214,7 @@ public:
     }else if(cln::minusp(d_value)){
        return -1;
     }else{
-      Assert(cln::plusp(d_value));
+      assert(cln::plusp(d_value));
       return 1;
     }
   }
diff --git a/src/util/rational_gmp_imp.h b/src/util/rational_gmp_imp.h
index b86dc32f2..383f0fb2b 100644
--- a/src/util/rational_gmp_imp.h
+++ b/src/util/rational_gmp_imp.h
@@ -26,6 +26,7 @@
 #include <string>
 
 #include "util/integer.h"
+#include "util/exception.h"
 
 namespace CVC4 {
 
diff --git a/src/util/result.h b/src/util/result.h
index f0cf3f20e..0894007bc 100644
--- a/src/util/result.h
+++ b/src/util/result.h
@@ -24,16 +24,10 @@
 #include <iostream>
 #include <string>
 
-#include "util/Assert.h"
+#include "util/exception.h"
 
 namespace CVC4 {
 
-// TODO: either templatize Result on its Kind (Sat/Validity) or subclass.
-// TODO: INVALID/SAT provide models, etc?---perhaps just by linking back
-// into the SmtEngine that produced the Result?
-// TODO: make unconstructible except by SmtEngine?  That would ensure that
-// any Result in the system is bona fide.
-
 class Result;
 
 std::ostream& operator<<(std::ostream& out, const Result& r) CVC4_PUBLIC;
@@ -137,9 +131,9 @@ public:
     return d_which == TYPE_NONE;
   }
   enum UnknownExplanation whyUnknown() const {
-    AlwaysAssert( isUnknown(),
-                  "This result is not unknown, so the reason for "
-                  "being unknown cannot be inquired of it" );
+    CheckArgument( isUnknown(), this,
+                   "This result is not unknown, so the reason for "
+                   "being unknown cannot be inquired of it" );
     return d_unknownExplanation;
   }
 
diff --git a/src/util/sexpr.h b/src/util/sexpr.h
index 4feffc18f..345a6c132 100644
--- a/src/util/sexpr.h
+++ b/src/util/sexpr.h
@@ -28,7 +28,7 @@
 
 #include "util/integer.h"
 #include "util/rational.h"
-#include "util/Assert.h"
+#include "util/exception.h"
 
 namespace CVC4 {
 
@@ -182,7 +182,7 @@ inline bool SExpr::isKeyword() const {
 }
 
 inline std::string SExpr::getValue() const {
-  AlwaysAssert( isAtom() );
+  CheckArgument( isAtom(), this );
   switch(d_sexprType) {
   case SEXPR_INTEGER:
     return d_integerValue.toString();
@@ -198,24 +198,24 @@ inline std::string SExpr::getValue() const {
   case SEXPR_STRING:
   case SEXPR_KEYWORD:
     return d_stringValue;
-  default:
-    Unhandled(d_sexprType);
+  case SEXPR_NOT_ATOM:
+    return std::string();
   }
-  return d_stringValue;
+  return std::string();
 }
 
 inline const CVC4::Integer& SExpr::getIntegerValue() const {
-  AlwaysAssert( isInteger() );
+  CheckArgument( isInteger(), this );
   return d_integerValue;
 }
 
 inline const CVC4::Rational& SExpr::getRationalValue() const {
-  AlwaysAssert( isRational() );
+  CheckArgument( isRational(), this );
   return d_rationalValue;
 }
 
 inline const std::vector<SExpr>& SExpr::getChildren() const {
-  AlwaysAssert( !isAtom() );
+  CheckArgument( !isAtom(), this );
   return d_children;
 }
 
diff --git a/src/util/statistics_registry.cpp b/src/util/statistics_registry.cpp
index f2a698a48..48e1355ec 100644
--- a/src/util/statistics_registry.cpp
+++ b/src/util/statistics_registry.cpp
@@ -50,36 +50,38 @@ StatisticsRegistry* StatisticsRegistry::current() {
   return stats::getStatisticsRegistry(smt::currentSmtEngine());
 }
 
-void StatisticsRegistry::registerStat(Stat* s) throw(AssertionException) {
+void StatisticsRegistry::registerStat(Stat* s) throw(CVC4::IllegalArgumentException) {
 #ifdef CVC4_STATISTICS_ON
   StatSet& stats = current()->d_stats;
-  AlwaysAssert(stats.find(s) == stats.end(),
-               "Statistic `%s' was already registered with this registry.", s->getName().c_str());
+  CheckArgument(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() */
 
-void StatisticsRegistry::unregisterStat(Stat* s) throw(AssertionException) {
+void StatisticsRegistry::unregisterStat(Stat* s) throw(CVC4::IllegalArgumentException) {
 #ifdef CVC4_STATISTICS_ON
   StatSet& stats = current()->d_stats;
-  AlwaysAssert(stats.find(s) != stats.end(),
-               "Statistic `%s' was not registered with this registry.", s->getName().c_str());
+  CheckArgument(stats.find(s) != stats.end(), s,
+                "Statistic `%s' was not registered with this registry.",
+                s->getName().c_str());
   stats.erase(s);
 #endif /* CVC4_STATISTICS_ON */
 }/* StatisticsRegistry::unregisterStat() */
 
 #endif /* ! __BUILDING_STATISTICS_FOR_EXPORT */
 
-void StatisticsRegistry::registerStat_(Stat* s) throw(AssertionException) {
+void StatisticsRegistry::registerStat_(Stat* s) throw(CVC4::IllegalArgumentException) {
 #ifdef CVC4_STATISTICS_ON
-  AlwaysAssert(d_stats.find(s) == d_stats.end());
+  CheckArgument(d_stats.find(s) == d_stats.end(), s);
   d_stats.insert(s);
 #endif /* CVC4_STATISTICS_ON */
 }/* StatisticsRegistry::registerStat_() */
 
-void StatisticsRegistry::unregisterStat_(Stat* s) throw(AssertionException) {
+void StatisticsRegistry::unregisterStat_(Stat* s) throw(CVC4::IllegalArgumentException) {
 #ifdef CVC4_STATISTICS_ON
-  AlwaysAssert(d_stats.find(s) != d_stats.end());
+  CheckArgument(d_stats.find(s) != d_stats.end(), s);
   d_stats.erase(s);
 #endif /* CVC4_STATISTICS_ON */
 }/* StatisticsRegistry::unregisterStat_() */
@@ -98,7 +100,7 @@ void StatisticsRegistry::flushInformation(std::ostream &out) const {
 
 void TimerStat::start() {
   if(__CVC4_USE_STATISTICS) {
-    AlwaysAssert(!d_running);
+    CheckArgument(!d_running, *this, "timer already running");
     clock_gettime(CLOCK_MONOTONIC, &d_start);
     d_running = true;
   }
@@ -106,7 +108,7 @@ void TimerStat::start() {
 
 void TimerStat::stop() {
   if(__CVC4_USE_STATISTICS) {
-    AlwaysAssert(d_running);
+    CheckArgument(d_running, *this, "timer not running");
     ::timespec end;
     clock_gettime(CLOCK_MONOTONIC, &end);
     d_data += end - d_start;
diff --git a/src/util/statistics_registry.h b/src/util/statistics_registry.h
index 870a88d66..99168353f 100644
--- a/src/util/statistics_registry.h
+++ b/src/util/statistics_registry.h
@@ -30,8 +30,7 @@
 #include <ctime>
 #include <vector>
 #include <stdint.h>
-
-#include "util/Assert.h"
+#include <cassert>
 
 namespace CVC4 {
 
@@ -69,10 +68,11 @@ public:
    * will throw an assertion exception if the given name contains the
    * statistic delimiter string.
    */
-  Stat(const std::string& name) throw(CVC4::AssertionException) :
+  Stat(const std::string& name) throw(CVC4::IllegalArgumentException) :
     d_name(name) {
     if(__CVC4_USE_STATISTICS) {
-      AlwaysAssert(d_name.find(", ") == std::string::npos);
+      CheckArgument(d_name.find(", ") == std::string::npos, name,
+                    "Statistics names cannot include a comma (',')");
     }
   }
 
@@ -270,11 +270,7 @@ public:
 
   /** Get the value of the referenced data cell. */
   const T& getData() const {
-    if(__CVC4_USE_STATISTICS) {
-      return *d_data;
-    } else {
-      Unreachable();
-    }
+    return *d_data;
   }
 
 };/* class ReferenceStat<T> */
@@ -316,11 +312,7 @@ public:
 
   /** Get the underlying data value. */
   const T& getData() const {
-    if(__CVC4_USE_STATISTICS) {
-      return d_data;
-    } else {
-      Unreachable();
-    }
+    return d_data;
   }
 
 };/* class BackedStat<T> */
@@ -362,11 +354,7 @@ public:
 
   /** Get the data of the underlying (wrapped) statistic. */
   const T& getData() const {
-    if(__CVC4_USE_STATISTICS) {
-      return d_stat.getData();
-    } else {
-      Unreachable();
-    }
+    return d_stat.getData();
   }
 
   SExpr getValue() const {
@@ -569,11 +557,14 @@ public:
   StatisticsRegistry() {}
 
   /** Construct a statistics registry */
-  StatisticsRegistry(const std::string& name) throw(CVC4::AssertionException) :
+  StatisticsRegistry(const std::string& name)
+      throw(CVC4::IllegalArgumentException) :
     Stat(name) {
     d_prefix = name;
     if(__CVC4_USE_STATISTICS) {
-      AlwaysAssert(d_name.find(s_regDelim) == std::string::npos);
+      CheckArgument(d_name.find(s_regDelim) == std::string::npos, name,
+                    "StatisticsRegistry names cannot contain the string \"%s\"",
+                    s_regDelim.c_str());
     }
   }
 
@@ -608,17 +599,17 @@ public:
 
 #if (defined(__BUILDING_CVC4LIB) || defined(__BUILDING_CVC4LIB_UNIT_TEST)) && !defined(__BUILDING_STATISTICS_FOR_EXPORT)
   /** Register a new statistic, making it active. */
-  static void registerStat(Stat* s) throw(AssertionException);
+  static void registerStat(Stat* s) throw(CVC4::IllegalArgumentException);
 
   /** Unregister an active statistic, making it inactive. */
-  static void unregisterStat(Stat* s) throw(AssertionException);
+  static void unregisterStat(Stat* s) throw(CVC4::IllegalArgumentException);
 #endif /* (__BUILDING_CVC4LIB || __BUILDING_CVC4LIB) && ! __BUILDING_STATISTICS_FOR_EXPORT */
 
   /** Register a new statistic */
-  void registerStat_(Stat* s) throw(AssertionException);
+  void registerStat_(Stat* s) throw(CVC4::IllegalArgumentException);
 
   /** Unregister a new statistic */
-  void unregisterStat_(Stat* s) throw(AssertionException);
+  void unregisterStat_(Stat* s) throw(CVC4::IllegalArgumentException);
 
 };/* class StatisticsRegistry */
 
@@ -630,11 +621,11 @@ public:
 inline timespec& operator+=(timespec& a, const timespec& b) {
   // assumes a.tv_nsec and b.tv_nsec are in range
   const long nsec_per_sec = 1000000000L; // one thousand million
-  Assert(a.tv_nsec >= 0 && a.tv_nsec < nsec_per_sec);
-  Assert(b.tv_nsec >= 0 && b.tv_nsec < nsec_per_sec);
+  CheckArgument(a.tv_nsec >= 0 && a.tv_nsec < nsec_per_sec, a);
+  CheckArgument(b.tv_nsec >= 0 && b.tv_nsec < nsec_per_sec, b);
   a.tv_sec += b.tv_sec;
   long nsec = a.tv_nsec + b.tv_nsec;
-  Assert(nsec >= 0);
+  assert(nsec >= 0);
   if(nsec < 0) {
     nsec += nsec_per_sec;
     --a.tv_sec;
@@ -643,7 +634,7 @@ inline timespec& operator+=(timespec& a, const timespec& b) {
     nsec -= nsec_per_sec;
     ++a.tv_sec;
   }
-  Assert(nsec >= 0 && nsec < nsec_per_sec);
+  assert(nsec >= 0 && nsec < nsec_per_sec);
   a.tv_nsec = nsec;
   return a;
 }
@@ -652,8 +643,8 @@ inline timespec& operator+=(timespec& a, const timespec& b) {
 inline timespec& operator-=(timespec& a, const timespec& b) {
   // assumes a.tv_nsec and b.tv_nsec are in range
   const long nsec_per_sec = 1000000000L; // one thousand million
-  Assert(a.tv_nsec >= 0 && a.tv_nsec < nsec_per_sec);
-  Assert(b.tv_nsec >= 0 && b.tv_nsec < nsec_per_sec);
+  CheckArgument(a.tv_nsec >= 0 && a.tv_nsec < nsec_per_sec, a);
+  CheckArgument(b.tv_nsec >= 0 && b.tv_nsec < nsec_per_sec, b);
   a.tv_sec -= b.tv_sec;
   long nsec = a.tv_nsec - b.tv_nsec;
   if(nsec < 0) {
@@ -664,7 +655,7 @@ inline timespec& operator-=(timespec& a, const timespec& b) {
     nsec -= nsec_per_sec;
     ++a.tv_sec;
   }
-  Assert(nsec >= 0 && nsec < nsec_per_sec);
+  assert(nsec >= 0 && nsec < nsec_per_sec);
   a.tv_nsec = nsec;
   return a;
 }
@@ -855,9 +846,9 @@ public:
   RegisterStatistic(StatisticsRegistry* reg, Stat* stat) :
     d_reg(reg),
     d_stat(stat) {
-    Assert(d_reg != NULL,
-           "You need to specify a statistics registry"
-           "on which to set the statistic");
+    CheckArgument(reg != NULL, reg,
+                  "You need to specify a statistics registry"
+                  "on which to set the statistic");
     d_reg->registerStat_(d_stat);
   }
 
diff --git a/src/util/subrange_bound.h b/src/util/subrange_bound.h
index 5de17106d..ffb2a1eaf 100644
--- a/src/util/subrange_bound.h
+++ b/src/util/subrange_bound.h
@@ -23,7 +23,7 @@
 #define __CVC4__SUBRANGE_BOUND_H
 
 #include "util/integer.h"
-#include "util/Assert.h"
+#include "util/exception.h"
 
 #include <limits>
 
@@ -222,7 +222,7 @@ public:
    * precondition: joinIsBounded(a,b) is true
    */
   static SubrangeBounds join(const SubrangeBounds& a, const SubrangeBounds& b){
-    Assert(joinIsBounded(a,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);