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.

5 files changed, 135 insertions, 127 deletions

diff --git a/src/expr/kind_template.h b/src/expr/kind_template.h
index fc7d838a1..2857dc5d8 100644
--- a/src/expr/kind_template.h
+++ b/src/expr/kind_template.h
@@ -24,7 +24,7 @@
 #include <iostream>
 #include <sstream>
 
-#include "util/Assert.h"
+#include "util/exception.h"
 
 namespace CVC4 {
 namespace kind {
@@ -100,6 +100,7 @@ struct KindHashFunction {
  */
 enum TypeConstant {
 ${type_constant_list}
+#line 104 "${template}"
   LAST_TYPE
 };/* enum TypeConstant */
 
@@ -115,6 +116,7 @@ struct TypeConstantHashFunction {
 inline std::ostream& operator<<(std::ostream& out, TypeConstant typeConstant) {
   switch(typeConstant) {
 ${type_constant_descriptions}
+#line 120 "${template}"
   default:
     out << "UNKNOWN_TYPE_CONSTANT";
     break;
@@ -126,8 +128,9 @@ namespace theory {
 
 enum TheoryId {
 ${theory_enum}
+#line 132 "${template}"
   THEORY_LAST
-};
+};/* enum TheoryId */
 
 const TheoryId THEORY_FIRST = static_cast<TheoryId>(0);
 const TheoryId THEORY_SAT_SOLVER = THEORY_LAST;
@@ -139,6 +142,7 @@ inline TheoryId& operator ++ (TheoryId& id) {
 inline std::ostream& operator<<(std::ostream& out, TheoryId theoryId) {
   switch(theoryId) {
 ${theory_descriptions}
+#line 146 "${template}"
   default:
     out << "UNKNOWN_THEORY";
     break;
@@ -148,23 +152,28 @@ ${theory_descriptions}
 
 inline TheoryId kindToTheoryId(::CVC4::Kind k) {
   switch(k) {
+  case kind::UNDEFINED_KIND:
+  case kind::NULL_EXPR:
+    break;
 ${kind_to_theory_id}
-  default:
-    Unhandled(k);
+#line 160 "${template}"
+  case kind::LAST_KIND:
+    break;
   }
+  throw IllegalArgumentException("", "k", __PRETTY_FUNCTION__, "bad kind");
 }
 
 inline TheoryId typeConstantToTheoryId(::CVC4::TypeConstant typeConstant) {
   switch(typeConstant) {
 ${type_constant_to_theory_id}
-  default:
-    Unhandled(typeConstant);
+#line 170 "${template}"
+  case LAST_TYPE:
+    break;
   }
+  throw IllegalArgumentException("", "k", __PRETTY_FUNCTION__, "bad type constant");
 }
 
-}/* theory namespace */
-
-
+}/* CVC4::theory namespace */
 }/* CVC4 namespace */
 
 #endif /* __CVC4__KIND_H */
diff --git a/src/expr/symbol_table.cpp b/src/expr/symbol_table.cpp
index e3bd898ef..71745f649 100644
--- a/src/expr/symbol_table.cpp
+++ b/src/expr/symbol_table.cpp
@@ -50,7 +50,7 @@ SymbolTable::~SymbolTable() {
 }
 
 void SymbolTable::bind(const std::string& name, Expr obj,
-                       bool levelZero) throw(AssertionException) {
+                       bool levelZero) throw() {
   CheckArgument(!obj.isNull(), obj, "cannot bind to a null Expr");
   ExprManagerScope ems(obj);
   if(levelZero) d_exprMap->insertAtContextLevelZero(name, obj);
@@ -58,7 +58,7 @@ void SymbolTable::bind(const std::string& name, Expr obj,
 }
 
 void SymbolTable::bindDefinedFunction(const std::string& name, Expr obj,
-                                      bool levelZero) throw(AssertionException) {
+                                      bool levelZero) throw() {
   CheckArgument(!obj.isNull(), obj, "cannot bind to a null Expr");
   ExprManagerScope ems(obj);
   if(levelZero){
@@ -84,7 +84,7 @@ bool SymbolTable::isBoundDefinedFunction(Expr func) const throw() {
   return d_functions->contains(func);
 }
 
-Expr SymbolTable::lookup(const std::string& name) const throw(AssertionException) {
+Expr SymbolTable::lookup(const std::string& name) const throw() {
   return (*d_exprMap->find(name)).second;
 }
 
@@ -121,7 +121,7 @@ bool SymbolTable::isBoundType(const std::string& name) const throw() {
   return d_typeMap->find(name) != d_typeMap->end();
 }
 
-Type SymbolTable::lookupType(const std::string& name) const throw(AssertionException) {
+Type SymbolTable::lookupType(const std::string& name) const throw() {
   pair<vector<Type>, Type> p = (*d_typeMap->find(name)).second;
   Assert(p.first.size() == 0,
          "type constructor arity is wrong: "
@@ -131,7 +131,7 @@ Type SymbolTable::lookupType(const std::string& name) const throw(AssertionExcep
 }
 
 Type SymbolTable::lookupType(const std::string& name,
-                             const std::vector<Type>& params) const throw(AssertionException) {
+                             const std::vector<Type>& params) const throw() {
   pair<vector<Type>, Type> p = (*d_typeMap->find(name)).second;
   Assert(p.first.size() == params.size(),
          "type constructor arity is wrong: "
diff --git a/src/expr/symbol_table.h b/src/expr/symbol_table.h
index 3f24d10f8..6db335ded 100644
--- a/src/expr/symbol_table.h
+++ b/src/expr/symbol_table.h
@@ -79,7 +79,7 @@ public:
    * @param obj the expression to bind to <code>name</code>
    * @param levelZero set if the binding must be done at level 0
    */
-  void bind(const std::string& name, Expr obj, bool levelZero = false) throw(AssertionException);
+  void bind(const std::string& name, Expr obj, bool levelZero = false) throw();
 
   /**
    * Bind a function body to a name in the current scope.  If
@@ -93,7 +93,7 @@ public:
    * @param obj the expression to bind to <code>name</code>
    * @param levelZero set if the binding must be done at level 0
    */
-  void bindDefinedFunction(const std::string& name, Expr obj, bool levelZero = false) throw(AssertionException);
+  void bindDefinedFunction(const std::string& name, Expr obj, bool levelZero = false) throw();
 
   /**
    * Bind a type to a name in the current scope.  If <code>name</code>
@@ -159,7 +159,7 @@ public:
    * @param name the identifier to lookup
    * @returns the expression bound to <code>name</code> in the current scope.
    */
-  Expr lookup(const std::string& name) const throw(AssertionException);
+  Expr lookup(const std::string& name) const throw();
 
   /**
    * Lookup a bound type.
@@ -167,7 +167,7 @@ public:
    * @param name the type identifier to lookup
    * @returns the type bound to <code>name</code> in the current scope.
    */
-  Type lookupType(const std::string& name) const throw(AssertionException);
+  Type lookupType(const std::string& name) const throw();
 
   /**
    * Lookup a bound parameterized type.
@@ -178,7 +178,7 @@ public:
    * the current scope.
    */
   Type lookupType(const std::string& name,
-                  const std::vector<Type>& params) const throw(AssertionException);
+                  const std::vector<Type>& params) const throw();
 
   /**
    * Lookup the arity of a bound parameterized type.
diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index 5a00a538c..c94094b2b 100644
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -23,7 +23,7 @@
 #include "expr/node_manager.h"
 #include "expr/type.h"
 #include "expr/type_node.h"
-#include "util/Assert.h"
+#include "util/exception.h"
 
 using namespace std;
 
@@ -88,8 +88,8 @@ bool Type::isComparableTo(Type t) const {
 }
 
 Type& Type::operator=(const Type& t) {
-  Assert(d_typeNode != NULL, "Unexpected NULL typenode pointer!");
-  Assert(t.d_typeNode != NULL, "Unexpected NULL typenode pointer!");
+  CheckArgument(d_typeNode != NULL, this, "Unexpected NULL typenode pointer!");
+  CheckArgument(t.d_typeNode != NULL, t, "Unexpected NULL typenode pointer!");
 
   if(this != &t) {
     if(d_nodeManager == t.d_nodeManager) {
@@ -202,9 +202,9 @@ bool Type::isBoolean() const {
 }
 
 /** Cast to a Boolean type */
-Type::operator BooleanType() const throw(AssertionException) {
+Type::operator BooleanType() const throw(IllegalArgumentException) {
   NodeManagerScope nms(d_nodeManager);
-  Assert(isNull() || isBoolean());
+  CheckArgument(isNull() || isBoolean(), this);
   return BooleanType(*this);
 }
 
@@ -215,9 +215,9 @@ bool Type::isInteger() const {
 }
 
 /** Cast to a integer type */
-Type::operator IntegerType() const throw(AssertionException) {
+Type::operator IntegerType() const throw(IllegalArgumentException) {
   NodeManagerScope nms(d_nodeManager);
-  Assert(isNull() || isInteger());
+  CheckArgument(isNull() || isInteger(), this);
   return IntegerType(*this);
 }
 
@@ -228,9 +228,9 @@ bool Type::isReal() const {
 }
 
 /** Cast to a real type */
-Type::operator RealType() const throw(AssertionException) {
+Type::operator RealType() const throw(IllegalArgumentException) {
   NodeManagerScope nms(d_nodeManager);
-  Assert(isNull() || isReal());
+  CheckArgument(isNull() || isReal(), this);
   return RealType(*this);
 }
 
@@ -241,9 +241,9 @@ bool Type::isString() const {
 }
 
 /** Cast to a string type */
-Type::operator StringType() const throw(AssertionException) {
+Type::operator StringType() const throw(IllegalArgumentException) {
   NodeManagerScope nms(d_nodeManager);
-  Assert(isNull() || isString());
+  CheckArgument(isNull() || isString(), this);
   return StringType(*this);
 }
 
@@ -254,16 +254,16 @@ bool Type::isBitVector() const {
 }
 
 /** Cast to a bit-vector type */
-Type::operator BitVectorType() const throw(AssertionException) {
+Type::operator BitVectorType() const throw(IllegalArgumentException) {
   NodeManagerScope nms(d_nodeManager);
-  Assert(isNull() || isBitVector());
+  CheckArgument(isNull() || isBitVector(), this);
   return BitVectorType(*this);
 }
 
 /** Cast to a Constructor type */
-Type::operator DatatypeType() const throw(AssertionException) {
+Type::operator DatatypeType() const throw(IllegalArgumentException) {
   NodeManagerScope nms(d_nodeManager);
-  Assert(isNull() || isDatatype());
+  CheckArgument(isNull() || isDatatype(), this);
   return DatatypeType(*this);
 }
 
@@ -274,9 +274,9 @@ bool Type::isDatatype() const {
 }
 
 /** Cast to a Constructor type */
-Type::operator ConstructorType() const throw(AssertionException) {
+Type::operator ConstructorType() const throw(IllegalArgumentException) {
   NodeManagerScope nms(d_nodeManager);
-  Assert(isNull() || isConstructor());
+  CheckArgument(isNull() || isConstructor(), this);
   return ConstructorType(*this);
 }
 
@@ -287,9 +287,9 @@ bool Type::isConstructor() const {
 }
 
 /** Cast to a Selector type */
-Type::operator SelectorType() const throw(AssertionException) {
+Type::operator SelectorType() const throw(IllegalArgumentException) {
   NodeManagerScope nms(d_nodeManager);
-  Assert(isNull() || isSelector());
+  CheckArgument(isNull() || isSelector(), this);
   return SelectorType(*this);
 }
 
@@ -300,9 +300,9 @@ bool Type::isSelector() const {
 }
 
 /** Cast to a Tester type */
-Type::operator TesterType() const throw(AssertionException) {
+Type::operator TesterType() const throw(IllegalArgumentException) {
   NodeManagerScope nms(d_nodeManager);
-  Assert(isNull() || isTester());
+  CheckArgument(isNull() || isTester(), this);
   return TesterType(*this);
 }
 
@@ -328,9 +328,9 @@ bool Type::isPredicate() const {
 }
 
 /** Cast to a function type */
-Type::operator FunctionType() const throw(AssertionException) {
+Type::operator FunctionType() const throw(IllegalArgumentException) {
   NodeManagerScope nms(d_nodeManager);
-  Assert(isNull() || isFunction());
+  CheckArgument(isNull() || isFunction(), this);
   return FunctionType(*this);
 }
 
@@ -341,9 +341,9 @@ bool Type::isTuple() const {
 }
 
 /** Cast to a tuple type */
-Type::operator TupleType() const throw(AssertionException) {
+Type::operator TupleType() const throw(IllegalArgumentException) {
   NodeManagerScope nms(d_nodeManager);
-  Assert(isNull() || isTuple());
+  CheckArgument(isNull() || isTuple(), this);
   return TupleType(*this);
 }
 
@@ -354,9 +354,9 @@ bool Type::isSExpr() const {
 }
 
 /** Cast to a symbolic expression type */
-Type::operator SExprType() const throw(AssertionException) {
+Type::operator SExprType() const throw(IllegalArgumentException) {
   NodeManagerScope nms(d_nodeManager);
-  Assert(isNull() || isSExpr());
+  CheckArgument(isNull() || isSExpr(), this);
   return SExprType(*this);
 }
 
@@ -367,7 +367,7 @@ bool Type::isArray() const {
 }
 
 /** Cast to an array type */
-Type::operator ArrayType() const throw(AssertionException) {
+Type::operator ArrayType() const throw(IllegalArgumentException) {
   NodeManagerScope nms(d_nodeManager);
   return ArrayType(*this);
 }
@@ -379,9 +379,9 @@ bool Type::isSort() const {
 }
 
 /** Cast to a sort type */
-Type::operator SortType() const throw(AssertionException) {
+Type::operator SortType() const throw(IllegalArgumentException) {
   NodeManagerScope nms(d_nodeManager);
-  Assert(isNull() || isSort());
+  CheckArgument(isNull() || isSort(), this);
   return SortType(*this);
 }
 
@@ -392,9 +392,9 @@ bool Type::isSortConstructor() const {
 }
 
 /** Cast to a sort constructor type */
-Type::operator SortConstructorType() const throw(AssertionException) {
+Type::operator SortConstructorType() const throw(IllegalArgumentException) {
   NodeManagerScope nms(d_nodeManager);
-  Assert(isNull() || isSortConstructor());
+  CheckArgument(isNull() || isSortConstructor(), this);
   return SortConstructorType(*this);
 }
 
@@ -405,9 +405,9 @@ bool Type::isPredicateSubtype() const {
 }
 
 /** Cast to a predicate subtype */
-Type::operator PredicateSubtype() const throw(AssertionException) {
+Type::operator PredicateSubtype() const throw(IllegalArgumentException) {
   NodeManagerScope nms(d_nodeManager);
-  Assert(isNull() || isPredicateSubtype());
+  CheckArgument(isNull() || isPredicateSubtype(), this);
   return PredicateSubtype(*this);
 }
 
@@ -418,9 +418,9 @@ bool Type::isSubrange() const {
 }
 
 /** Cast to a predicate subtype */
-Type::operator SubrangeType() const throw(AssertionException) {
+Type::operator SubrangeType() const throw(IllegalArgumentException) {
   NodeManagerScope nms(d_nodeManager);
-  Assert(isNull() || isSubrange());
+  CheckArgument(isNull() || isSubrange(), this);
   return SubrangeType(*this);
 }
 
@@ -438,7 +438,7 @@ vector<Type> FunctionType::getArgTypes() const {
 
 Type FunctionType::getRangeType() const {
   NodeManagerScope nms(d_nodeManager);
-  Assert(isNull() || isFunction());
+  CheckArgument(isNull() || isFunction(), this);
   return makeType(d_typeNode->getRangeType());
 }
 
@@ -503,92 +503,92 @@ SortType SortConstructorType::instantiate(const std::vector<Type>& params) const
   return SortType(makeType(d_nodeManager->mkSort(*d_typeNode, paramsNodes)));
 }
 
-BooleanType::BooleanType(const Type& t) throw(AssertionException) :
+BooleanType::BooleanType(const Type& t) throw(IllegalArgumentException) :
   Type(t) {
-  Assert(isNull() || isBoolean());
+  CheckArgument(isNull() || isBoolean(), this);
 }
 
-IntegerType::IntegerType(const Type& t) throw(AssertionException) :
+IntegerType::IntegerType(const Type& t) throw(IllegalArgumentException) :
   Type(t) {
-  Assert(isNull() || isInteger());
+  CheckArgument(isNull() || isInteger(), this);
 }
 
-RealType::RealType(const Type& t) throw(AssertionException) :
+RealType::RealType(const Type& t) throw(IllegalArgumentException) :
   Type(t) {
-  Assert(isNull() || isReal());
+  CheckArgument(isNull() || isReal(), this);
 }
 
-StringType::StringType(const Type& t) throw(AssertionException) :
+StringType::StringType(const Type& t) throw(IllegalArgumentException) :
   Type(t) {
-  Assert(isNull() || isString());
+  CheckArgument(isNull() || isString(), this);
 }
 
-BitVectorType::BitVectorType(const Type& t) throw(AssertionException) :
+BitVectorType::BitVectorType(const Type& t) throw(IllegalArgumentException) :
   Type(t) {
-  Assert(isNull() || isBitVector());
+  CheckArgument(isNull() || isBitVector(), this);
 }
 
-DatatypeType::DatatypeType(const Type& t) throw(AssertionException) :
+DatatypeType::DatatypeType(const Type& t) throw(IllegalArgumentException) :
   Type(t) {
-  Assert(isNull() || isDatatype());
+  CheckArgument(isNull() || isDatatype(), this);
 }
 
-ConstructorType::ConstructorType(const Type& t) throw(AssertionException) :
+ConstructorType::ConstructorType(const Type& t) throw(IllegalArgumentException) :
   Type(t) {
-  Assert(isNull() || isConstructor());
+  CheckArgument(isNull() || isConstructor(), this);
 }
 
-SelectorType::SelectorType(const Type& t) throw(AssertionException) :
+SelectorType::SelectorType(const Type& t) throw(IllegalArgumentException) :
   Type(t) {
-  Assert(isNull() || isSelector());
+  CheckArgument(isNull() || isSelector(), this);
 }
 
-TesterType::TesterType(const Type& t) throw(AssertionException) :
+TesterType::TesterType(const Type& t) throw(IllegalArgumentException) :
   Type(t) {
-  Assert(isNull() || isTester());
+  CheckArgument(isNull() || isTester(), this);
 }
 
-FunctionType::FunctionType(const Type& t) throw(AssertionException) :
+FunctionType::FunctionType(const Type& t) throw(IllegalArgumentException) :
   Type(t) {
-  Assert(isNull() || isFunction());
+  CheckArgument(isNull() || isFunction(), this);
 }
 
-TupleType::TupleType(const Type& t) throw(AssertionException) :
+TupleType::TupleType(const Type& t) throw(IllegalArgumentException) :
   Type(t) {
-  Assert(isNull() || isTuple());
+  CheckArgument(isNull() || isTuple(), this);
 }
 
-SExprType::SExprType(const Type& t) throw(AssertionException) :
+SExprType::SExprType(const Type& t) throw(IllegalArgumentException) :
   Type(t) {
-  Assert(isNull() || isSExpr());
+  CheckArgument(isNull() || isSExpr(), this);
 }
 
-ArrayType::ArrayType(const Type& t) throw(AssertionException) :
+ArrayType::ArrayType(const Type& t) throw(IllegalArgumentException) :
   Type(t) {
-  Assert(isNull() || isArray());
+  CheckArgument(isNull() || isArray(), this);
 }
 
-SortType::SortType(const Type& t) throw(AssertionException) :
+SortType::SortType(const Type& t) throw(IllegalArgumentException) :
   Type(t) {
-  Assert(isNull() || isSort());
+  CheckArgument(isNull() || isSort(), this);
 }
 
 SortConstructorType::SortConstructorType(const Type& t)
-  throw(AssertionException) :
+  throw(IllegalArgumentException) :
   Type(t) {
-  Assert(isNull() || isSortConstructor());
+  CheckArgument(isNull() || isSortConstructor(), this);
 }
 
 PredicateSubtype::PredicateSubtype(const Type& t)
-  throw(AssertionException) :
+  throw(IllegalArgumentException) :
   Type(t) {
-  Assert(isNull() || isPredicateSubtype());
+  CheckArgument(isNull() || isPredicateSubtype(), this);
 }
 
 SubrangeType::SubrangeType(const Type& t)
-  throw(AssertionException) :
+  throw(IllegalArgumentException) :
   Type(t) {
-  Assert(isNull() || isSubrange());
+  CheckArgument(isNull() || isSubrange(), this);
 }
 
 unsigned BitVectorType::getSize() const {
@@ -625,7 +625,7 @@ std::vector<Type> ConstructorType::getArgTypes() const {
 
 const Datatype& DatatypeType::getDatatype() const {
   if( d_typeNode->isParametricDatatype() ) {
-    Assert( (*d_typeNode)[0].getKind() == kind::DATATYPE_TYPE );
+    CheckArgument( (*d_typeNode)[0].getKind() == kind::DATATYPE_TYPE, this);
     const Datatype& dt = (*d_typeNode)[0].getConst<Datatype>();
     return dt;
   } else {
diff --git a/src/expr/type.h b/src/expr/type.h
index caaf256f5..39d50fd31 100644
--- a/src/expr/type.h
+++ b/src/expr/type.h
@@ -26,7 +26,6 @@
 #include <limits.h>
 #include <stdint.h>
 
-#include "util/Assert.h"
 #include "util/cardinality.h"
 #include "util/subrange_bound.h"
 
@@ -64,7 +63,7 @@ class PredicateSubtype;
 class SubrangeType;
 class Type;
 
-/** Strategy for hashing Types */
+/** Hash function for Types */
 struct CVC4_PUBLIC TypeHashFunction {
   /** Return a hash code for type t */
   size_t operator()(const CVC4::Type& t) const;
@@ -238,7 +237,7 @@ public:
    * Cast this type to a Boolean type
    * @return the BooleanType
    */
-  operator BooleanType() const throw(AssertionException);
+  operator BooleanType() const throw(IllegalArgumentException);
 
   /**
    * Is this the integer type?
@@ -250,7 +249,7 @@ public:
    * Cast this type to a integer type
    * @return the IntegerType
    */
-  operator IntegerType() const throw(AssertionException);
+  operator IntegerType() const throw(IllegalArgumentException);
 
   /**
    * Is this the real type?
@@ -262,7 +261,7 @@ public:
    * Cast this type to a real type
    * @return the RealType
    */
-  operator RealType() const throw(AssertionException);
+  operator RealType() const throw(IllegalArgumentException);
 
   /**
    * Is this the string type?
@@ -274,7 +273,7 @@ public:
    * Cast this type to a string type
    * @return the StringType
    */
-  operator StringType() const throw(AssertionException);
+  operator StringType() const throw(IllegalArgumentException);
 
   /**
    * Is this the bit-vector type?
@@ -286,7 +285,7 @@ public:
    * Cast this type to a bit-vector type
    * @return the BitVectorType
    */
-  operator BitVectorType() const throw(AssertionException);
+  operator BitVectorType() const throw(IllegalArgumentException);
 
   /**
    * Is this a function type?
@@ -305,7 +304,7 @@ public:
    * Cast this type to a function type
    * @return the FunctionType
    */
-  operator FunctionType() const throw(AssertionException);
+  operator FunctionType() const throw(IllegalArgumentException);
 
   /**
    * Is this a tuple type?
@@ -317,7 +316,7 @@ public:
    * Cast this type to a tuple type
    * @return the TupleType
    */
-  operator TupleType() const throw(AssertionException);
+  operator TupleType() const throw(IllegalArgumentException);
 
   /**
    * Is this a symbolic expression type?
@@ -329,7 +328,7 @@ public:
    * Cast this type to a symbolic expression type
    * @return the SExprType
    */
-  operator SExprType() const throw(AssertionException);
+  operator SExprType() const throw(IllegalArgumentException);
 
   /**
    * Is this an array type?
@@ -341,7 +340,7 @@ public:
    * Cast this type to an array type
    * @return the ArrayType
    */
-  operator ArrayType() const throw(AssertionException);
+  operator ArrayType() const throw(IllegalArgumentException);
 
   /**
    * Is this a datatype type?
@@ -353,7 +352,7 @@ public:
    * Cast this type to a datatype type
    * @return the DatatypeType
    */
-  operator DatatypeType() const throw(AssertionException);
+  operator DatatypeType() const throw(IllegalArgumentException);
 
   /**
    * Is this a constructor type?
@@ -365,7 +364,7 @@ public:
    * Cast this type to a constructor type
    * @return the ConstructorType
    */
-  operator ConstructorType() const throw(AssertionException);
+  operator ConstructorType() const throw(IllegalArgumentException);
 
   /**
    * Is this a selector type?
@@ -377,7 +376,7 @@ public:
    * Cast this type to a selector type
    * @return the SelectorType
    */
-  operator SelectorType() const throw(AssertionException);
+  operator SelectorType() const throw(IllegalArgumentException);
 
   /**
    * Is this a tester type?
@@ -389,7 +388,7 @@ public:
    * Cast this type to a tester type
    * @return the TesterType
    */
-  operator TesterType() const throw(AssertionException);
+  operator TesterType() const throw(IllegalArgumentException);
 
   /**
    * Is this a sort kind?
@@ -401,7 +400,7 @@ public:
    * Cast this type to a sort type
    * @return the sort type
    */
-  operator SortType() const throw(AssertionException);
+  operator SortType() const throw(IllegalArgumentException);
 
   /**
    * Is this a sort constructor kind?
@@ -413,7 +412,7 @@ public:
    * Cast this type to a sort constructor type
    * @return the sort constructor type
    */
-  operator SortConstructorType() const throw(AssertionException);
+  operator SortConstructorType() const throw(IllegalArgumentException);
 
   /**
    * Is this a predicate subtype?
@@ -425,7 +424,7 @@ public:
    * Cast this type to a predicate subtype
    * @return the predicate subtype
    */
-  operator PredicateSubtype() const throw(AssertionException);
+  operator PredicateSubtype() const throw(IllegalArgumentException);
 
   /**
    * Is this an integer subrange type?
@@ -437,7 +436,7 @@ public:
    * Cast this type to an integer subrange type
    * @return the integer subrange type
    */
-  operator SubrangeType() const throw(AssertionException);
+  operator SubrangeType() const throw(IllegalArgumentException);
 
   /**
    * Outputs a string representation of this type to the stream.
@@ -459,7 +458,7 @@ class CVC4_PUBLIC BooleanType : public Type {
 public:
 
   /** Construct from the base type */
-  BooleanType(const Type& type = Type()) throw(AssertionException);
+  BooleanType(const Type& type = Type()) throw(IllegalArgumentException);
 };/* class BooleanType */
 
 /**
@@ -470,7 +469,7 @@ class CVC4_PUBLIC IntegerType : public Type {
 public:
 
   /** Construct from the base type */
-  IntegerType(const Type& type = Type()) throw(AssertionException);
+  IntegerType(const Type& type = Type()) throw(IllegalArgumentException);
 };/* class IntegerType */
 
 /**
@@ -481,7 +480,7 @@ class CVC4_PUBLIC RealType : public Type {
 public:
 
   /** Construct from the base type */
-  RealType(const Type& type = Type()) throw(AssertionException);
+  RealType(const Type& type = Type()) throw(IllegalArgumentException);
 };/* class RealType */
 
 /**
@@ -492,7 +491,7 @@ class CVC4_PUBLIC StringType : public Type {
 public:
 
   /** Construct from the base type */
-  StringType(const Type& type) throw(AssertionException);
+  StringType(const Type& type) throw(IllegalArgumentException);
 };/* class StringType */
 
 /**
@@ -503,7 +502,7 @@ class CVC4_PUBLIC FunctionType : public Type {
 public:
 
   /** Construct from the base type */
-  FunctionType(const Type& type = Type()) throw(AssertionException);
+  FunctionType(const Type& type = Type()) throw(IllegalArgumentException);
 
   /** Get the argument types */
   std::vector<Type> getArgTypes() const;
@@ -520,7 +519,7 @@ class CVC4_PUBLIC TupleType : public Type {
 public:
 
   /** Construct from the base type */
-  TupleType(const Type& type = Type()) throw(AssertionException);
+  TupleType(const Type& type = Type()) throw(IllegalArgumentException);
 
   /** Get the constituent types */
   std::vector<Type> getTypes() const;
@@ -534,7 +533,7 @@ class CVC4_PUBLIC SExprType : public Type {
 public:
 
   /** Construct from the base type */
-  SExprType(const Type& type = Type()) throw(AssertionException);
+  SExprType(const Type& type = Type()) throw(IllegalArgumentException);
 
   /** Get the constituent types */
   std::vector<Type> getTypes() const;
@@ -548,7 +547,7 @@ class CVC4_PUBLIC ArrayType : public Type {
 public:
 
   /** Construct from the base type */
-  ArrayType(const Type& type = Type()) throw(AssertionException);
+  ArrayType(const Type& type = Type()) throw(IllegalArgumentException);
 
   /** Get the index type */
   Type getIndexType() const;
@@ -565,7 +564,7 @@ class CVC4_PUBLIC SortType : public Type {
 public:
 
   /** Construct from the base type */
-  SortType(const Type& type = Type()) throw(AssertionException);
+  SortType(const Type& type = Type()) throw(IllegalArgumentException);
 
   /** Get the name of the sort */
   std::string getName() const;
@@ -586,7 +585,7 @@ class CVC4_PUBLIC SortConstructorType : public Type {
 public:
 
   /** Construct from the base type */
-  SortConstructorType(const Type& type = Type()) throw(AssertionException);
+  SortConstructorType(const Type& type = Type()) throw(IllegalArgumentException);
 
   /** Get the name of the sort constructor */
   std::string getName() const;
@@ -607,7 +606,7 @@ class CVC4_PUBLIC PredicateSubtype : public Type {
 public:
 
   /** Construct from the base type */
-  PredicateSubtype(const Type& type = Type()) throw(AssertionException);
+  PredicateSubtype(const Type& type = Type()) throw(IllegalArgumentException);
 
   /** Get the LAMBDA defining this predicate subtype */
   Expr getPredicate() const;
@@ -625,7 +624,7 @@ class CVC4_PUBLIC SubrangeType : public Type {
 public:
 
   /** Construct from the base type */
-  SubrangeType(const Type& type = Type()) throw(AssertionException);
+  SubrangeType(const Type& type = Type()) throw(IllegalArgumentException);
 
   /** Get the bounds defining this integer subrange */
   SubrangeBounds getSubrangeBounds() const;
@@ -640,7 +639,7 @@ class CVC4_PUBLIC BitVectorType : public Type {
 public:
 
   /** Construct from the base type */
-  BitVectorType(const Type& type = Type()) throw(AssertionException);
+  BitVectorType(const Type& type = Type()) throw(IllegalArgumentException);
 
   /**
    * Returns the size of the bit-vector type.
@@ -659,7 +658,7 @@ class CVC4_PUBLIC DatatypeType : public Type {
 public:
 
   /** Construct from the base type */
-  DatatypeType(const Type& type = Type()) throw(AssertionException);
+  DatatypeType(const Type& type = Type()) throw(IllegalArgumentException);
 
   /** Get the underlying datatype */
   const Datatype& getDatatype() const;
@@ -705,7 +704,7 @@ class CVC4_PUBLIC ConstructorType : public Type {
 public:
 
   /** Construct from the base type */
-  ConstructorType(const Type& type = Type()) throw(AssertionException);
+  ConstructorType(const Type& type = Type()) throw(IllegalArgumentException);
 
   /** Get the range type */
   DatatypeType getRangeType() const;
@@ -727,7 +726,7 @@ class CVC4_PUBLIC SelectorType : public Type {
 public:
 
   /** Construct from the base type */
-  SelectorType(const Type& type = Type()) throw(AssertionException);
+  SelectorType(const Type& type = Type()) throw(IllegalArgumentException);
 
   /** Get the domain type for this selector (the datatype type) */
   DatatypeType getDomain() const;
@@ -745,7 +744,7 @@ class CVC4_PUBLIC TesterType : public Type {
 public:
 
   /** Construct from the base type */
-  TesterType(const Type& type = Type()) throw(AssertionException);
+  TesterType(const Type& type = Type()) throw(IllegalArgumentException);
 
   /** Get the type that this tester tests (the datatype type) */
   DatatypeType getDomain() const;