Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. (#3366)

24 files changed, 456 insertions, 460 deletions

diff --git a/src/expr/array_store_all.cpp b/src/expr/array_store_all.cpp
index eff2c2151..f2d9a35a9 100644
--- a/src/expr/array_store_all.cpp
+++ b/src/expr/array_store_all.cpp
@@ -20,7 +20,7 @@
 
 #include <iostream>
 
-#include "base/cvc4_assert.h"
+#include "base/check.h"
 #include "expr/expr.h"
 #include "expr/type.h"
 
diff --git a/src/expr/attribute.cpp b/src/expr/attribute.cpp
index b9234883b..553c19f6e 100644
--- a/src/expr/attribute.cpp
+++ b/src/expr/attribute.cpp
@@ -79,7 +79,7 @@ void AttributeManager::deleteAttributes(const AttrIdVec& atids) {
 
     switch(tableId) {
     case AttrTableBool:
-      Unimplemented("delete attributes is unimplemented for bools");
+      Unimplemented() << "delete attributes is unimplemented for bools";
       break;
     case AttrTableUInt64:
       deleteAttributesFromTable(d_ints, ids);
@@ -103,7 +103,8 @@ void AttributeManager::deleteAttributes(const AttrIdVec& atids) {
     case AttrTableCDNode:
     case AttrTableCDString:
     case AttrTableCDPointer:
-      Unimplemented("CDAttributes cannot be deleted. Contact Tim/Morgan if this behavior is desired.");
+      Unimplemented() << "CDAttributes cannot be deleted. Contact Tim/Morgan "
+                         "if this behavior is desired.";
       break;
 
     case LastAttrTable:
diff --git a/src/expr/attribute_internals.h b/src/expr/attribute_internals.h
index e47dce434..bc34324b0 100644
--- a/src/expr/attribute_internals.h
+++ b/src/expr/attribute_internals.h
@@ -463,9 +463,8 @@ public:
    */
   static inline uint64_t registerAttribute() {
     const uint64_t id = attr::LastAttributeId<bool, context_dep>::getNextId();
-    AlwaysAssert( id <= 63,
-                  "Too many boolean node attributes registered "
-                  "during initialization !" );
+    AlwaysAssert(id <= 63) << "Too many boolean node attributes registered "
+                              "during initialization !";
     return id;
   }
 };/* class Attribute<..., bool, ...> */
diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp
index 4ec6ac36a..2356f74bc 100644
--- a/src/expr/datatype.cpp
+++ b/src/expr/datatype.cpp
@@ -19,7 +19,7 @@
 #include <string>
 #include <sstream>
 
-#include "base/cvc4_assert.h"
+#include "base/check.h"
 #include "expr/attribute.h"
 #include "expr/expr_manager.h"
 #include "expr/expr_manager_scope.h"
@@ -67,7 +67,7 @@ const Datatype& Datatype::datatypeOf(Expr item) {
   case kind::TESTER_TYPE:
     return DatatypeType(t[0].toType()).getDatatype();
   default:
-    Unhandled("arg must be a datatype constructor, selector, or tester");
+    Unhandled() << "arg must be a datatype constructor, selector, or tester";
   }
 }
 
@@ -242,7 +242,7 @@ void Datatype::setRecord() {
 Cardinality Datatype::getCardinality(Type t) const
 {
   PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
-  Assert( t.isDatatype() && ((DatatypeType)t).getDatatype()==*this );
+  Assert(t.isDatatype() && ((DatatypeType)t).getDatatype() == *this);
   std::vector< Type > processing;
   computeCardinality( t, processing );
   return d_card;
@@ -275,10 +275,10 @@ Cardinality Datatype::computeCardinality(Type t,
 bool Datatype::isRecursiveSingleton(Type t) const
 {
   PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
-  Assert( t.isDatatype() && ((DatatypeType)t).getDatatype()==*this );
+  Assert(t.isDatatype() && ((DatatypeType)t).getDatatype() == *this);
   if( d_card_rec_singleton.find( t )==d_card_rec_singleton.end() ){
     if( isCodatatype() ){
-      Assert( d_card_u_assume[t].empty() );
+      Assert(d_card_u_assume[t].empty());
       std::vector< Type > processing;
       if( computeCardinalityRecSingleton( t, processing, d_card_u_assume[t] ) ){
         d_card_rec_singleton[t] = 1;
@@ -307,8 +307,8 @@ bool Datatype::isRecursiveSingleton() const
 
 unsigned Datatype::getNumRecursiveSingletonArgTypes(Type t) const
 {
-  Assert( d_card_rec_singleton.find( t )!=d_card_rec_singleton.end() );
-  Assert( isRecursiveSingleton( t ) );
+  Assert(d_card_rec_singleton.find(t) != d_card_rec_singleton.end());
+  Assert(isRecursiveSingleton(t));
   return d_card_u_assume[t].size();
 }
 
@@ -320,8 +320,8 @@ unsigned Datatype::getNumRecursiveSingletonArgTypes() const
 
 Type Datatype::getRecursiveSingletonArgType(Type t, unsigned i) const
 {
-  Assert( d_card_rec_singleton.find( t )!=d_card_rec_singleton.end() );
-  Assert( isRecursiveSingleton( t ) );
+  Assert(d_card_rec_singleton.find(t) != d_card_rec_singleton.end());
+  Assert(isRecursiveSingleton(t));
   return d_card_u_assume[t][i];
 }
 
@@ -384,7 +384,7 @@ bool Datatype::computeCardinalityRecSingleton(Type t,
 bool Datatype::isFinite(Type t) const
 {
   PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
-  Assert( t.isDatatype() && ((DatatypeType)t).getDatatype()==*this );
+  Assert(t.isDatatype() && ((DatatypeType)t).getDatatype() == *this);
 
   // we're using some internals, so we have to set up this library context
   ExprManagerScope ems(d_self);
@@ -413,7 +413,7 @@ bool Datatype::isFinite() const
 bool Datatype::isInterpretedFinite(Type t) const
 {
   PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
-  Assert( t.isDatatype() && ((DatatypeType)t).getDatatype()==*this );
+  Assert(t.isDatatype() && ((DatatypeType)t).getDatatype() == *this);
   // we're using some internals, so we have to set up this library context
   ExprManagerScope ems(d_self);
   TypeNode self = TypeNode::fromType(d_self);
@@ -596,10 +596,10 @@ bool Datatype::operator==(const Datatype& other) const
     // testing equivalence of constructors and testers is harder b/c
     // this constructor might not be resolved yet; only compare them
     // if they are both resolved
-    Assert(isResolved() == !(*i).d_constructor.isNull() &&
-           isResolved() == !(*i).d_tester.isNull() &&
-           (*i).d_constructor.isNull() == (*j).d_constructor.isNull() &&
-           (*i).d_tester.isNull() == (*j).d_tester.isNull());
+    Assert(isResolved() == !(*i).d_constructor.isNull()
+           && isResolved() == !(*i).d_tester.isNull()
+           && (*i).d_constructor.isNull() == (*j).d_constructor.isNull()
+           && (*i).d_tester.isNull() == (*j).d_tester.isNull());
     if(!(*i).d_constructor.isNull() && (*i).d_constructor != (*j).d_constructor) {
       return false;
     }
@@ -613,8 +613,8 @@ bool Datatype::operator==(const Datatype& other) const
       }
       // testing equivalence of selectors is harder b/c args might not
       // be resolved yet
-      Assert(isResolved() == (*k).isResolved() &&
-             (*k).isResolved() == (*l).isResolved());
+      Assert(isResolved() == (*k).isResolved()
+             && (*k).isResolved() == (*l).isResolved());
       if((*k).isResolved()) {
         // both are resolved, so simply compare the selectors directly
         if((*k).d_selector != (*l).d_selector) {
@@ -1121,7 +1121,7 @@ Expr DatatypeConstructor::computeGroundTerm(Type t,
 
   Expr groundTerm = getConstructor().getExprManager()->mkExpr(kind::APPLY_CONSTRUCTOR, groundTerms);
   if( groundTerm.getType()!=t ){
-    Assert( Datatype::datatypeOf( d_constructor ).isParametric() );
+    Assert(Datatype::datatypeOf(d_constructor).isParametric());
     //type is ambiguous, must apply type ascription
     Debug("datatypes-gt") << "ambiguous type for " << groundTerm << ", ascribe to " << t << std::endl;
     groundTerms[0] = getConstructor().getExprManager()->mkExpr(kind::APPLY_TYPE_ASCRIPTION,
@@ -1140,8 +1140,8 @@ void DatatypeConstructor::computeSharedSelectors( Type domainType ) const {
     }else{
       ctype = TypeNode::fromType( d_constructor.getType() );
     }
-    Assert( ctype.isConstructor() );
-    Assert( ctype.getNumChildren()-1==getNumArgs() );
+    Assert(ctype.isConstructor());
+    Assert(ctype.getNumChildren() - 1 == getNumArgs());
     //compute the shared selectors
     const Datatype& dt = Datatype::datatypeOf(d_constructor);
     std::map< TypeNode, unsigned > counter;
@@ -1149,7 +1149,8 @@ void DatatypeConstructor::computeSharedSelectors( Type domainType ) const {
       TypeNode t = ctype[j];
       Expr ss = dt.getSharedSelector( domainType, t.toType(), counter[t] );
       d_shared_selectors[domainType].push_back( ss );
-      Assert( d_shared_selector_index[domainType].find( ss )==d_shared_selector_index[domainType].end() );
+      Assert(d_shared_selector_index[domainType].find(ss)
+             == d_shared_selector_index[domainType].end());
       d_shared_selector_index[domainType][ss] = j;
       counter[t]++;
     }
@@ -1226,7 +1227,7 @@ Expr DatatypeConstructor::getSelectorInternal( Type domainType, size_t index ) c
   PrettyCheckArgument(index < getNumArgs(), index, "index out of bounds");
   if( options::dtSharedSelectors() ){
     computeSharedSelectors( domainType );
-    Assert( d_shared_selectors[domainType].size()==getNumArgs() );
+    Assert(d_shared_selectors[domainType].size() == getNumArgs());
     return d_shared_selectors[domainType][index];
   }else{
     return d_args[index].getSelector();
@@ -1236,7 +1237,7 @@ Expr DatatypeConstructor::getSelectorInternal( Type domainType, size_t index ) c
 int DatatypeConstructor::getSelectorIndexInternal( Expr sel ) const {
   PrettyCheckArgument(isResolved(), this, "cannot get an internal selector index for an unresolved datatype constructor");
   if( options::dtSharedSelectors() ){
-    Assert( sel.getType().isSelector() );
+    Assert(sel.getType().isSelector());
     Type domainType = ((SelectorType)sel.getType()).getDomain();
     computeSharedSelectors( domainType );
     std::map< Expr, unsigned >::iterator its = d_shared_selector_index[domainType].find( sel );
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index bc3d450d0..09555da1b 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -578,7 +578,7 @@ FunctionType ExprManager::mkFunctionType(Type domain, Type range) {
 /** Make a function type with input types from argTypes. */
 FunctionType ExprManager::mkFunctionType(const std::vector<Type>& argTypes, Type range) {
   NodeManagerScope nms(d_nodeManager);
-  Assert( argTypes.size() >= 1 );
+  Assert(argTypes.size() >= 1);
   std::vector<TypeNode> argTypeNodes;
   for (unsigned i = 0, i_end = argTypes.size(); i < i_end; ++ i) {
     argTypeNodes.push_back(*argTypes[i].d_typeNode);
@@ -588,7 +588,7 @@ FunctionType ExprManager::mkFunctionType(const std::vector<Type>& argTypes, Type
 
 FunctionType ExprManager::mkFunctionType(const std::vector<Type>& sorts) {
   NodeManagerScope nms(d_nodeManager);
-  Assert( sorts.size() >= 2 );
+  Assert(sorts.size() >= 2);
   std::vector<TypeNode> sortNodes;
   for (unsigned i = 0, i_end = sorts.size(); i < i_end; ++ i) {
      sortNodes.push_back(*sorts[i].d_typeNode);
@@ -598,7 +598,7 @@ FunctionType ExprManager::mkFunctionType(const std::vector<Type>& sorts) {
 
 FunctionType ExprManager::mkPredicateType(const std::vector<Type>& sorts) {
   NodeManagerScope nms(d_nodeManager);
-  Assert( sorts.size() >= 1 );
+  Assert(sorts.size() >= 1);
   std::vector<TypeNode> sortNodes;
   for (unsigned i = 0, i_end = sorts.size(); i < i_end; ++ i) {
      sortNodes.push_back(*sorts[i].d_typeNode);
@@ -735,7 +735,7 @@ std::vector<DatatypeType> ExprManager::mkMutualDatatypeTypes(
     if( (*i).isSort() ) {
       name = SortType(*i).getName();
     } else {
-      Assert( (*i).isSortConstructor() );
+      Assert((*i).isSortConstructor());
       name = SortConstructorType(*i).getName();
     }
     std::map<std::string, DatatypeType>::const_iterator resolver =
@@ -753,7 +753,7 @@ std::vector<DatatypeType> ExprManager::mkMutualDatatypeTypes(
       placeholders.push_back(*i);
       replacements.push_back( (*resolver).second );
     } else {
-      Assert( (*i).isSortConstructor() );
+      Assert((*i).isSortConstructor());
       paramTypes.push_back( SortConstructorType(*i) );
       paramReplacements.push_back( (*resolver).second );
     }
@@ -794,31 +794,31 @@ void ExprManager::checkResolvedDatatype(DatatypeType dtt) const {
       ++i) {
     const DatatypeConstructor& c = *i;
     Type testerType CVC4_UNUSED = c.getTester().getType();
-    Assert(c.isResolved() &&
-           testerType.isTester() &&
-           TesterType(testerType).getDomain() == dtt &&
-           TesterType(testerType).getRangeType() == booleanType(),
-           "malformed tester in datatype post-resolution");
+    Assert(c.isResolved() && testerType.isTester()
+           && TesterType(testerType).getDomain() == dtt
+           && TesterType(testerType).getRangeType() == booleanType())
+        << "malformed tester in datatype post-resolution";
     Type ctorType CVC4_UNUSED = c.getConstructor().getType();
-    Assert(ctorType.isConstructor() &&
-           ConstructorType(ctorType).getArity() == c.getNumArgs() &&
-           ConstructorType(ctorType).getRangeType() == dtt,
-           "malformed constructor in datatype post-resolution");
+    Assert(ctorType.isConstructor()
+           && ConstructorType(ctorType).getArity() == c.getNumArgs()
+           && ConstructorType(ctorType).getRangeType() == dtt)
+        << "malformed constructor in datatype post-resolution";
     // for all selectors...
     for(DatatypeConstructor::const_iterator j = c.begin(), j_end = c.end();
         j != j_end;
         ++j) {
       const DatatypeConstructorArg& a = *j;
       Type selectorType = a.getType();
-      Assert(a.isResolved() &&
-             selectorType.isSelector() &&
-             SelectorType(selectorType).getDomain() == dtt,
-             "malformed selector in datatype post-resolution");
+      Assert(a.isResolved() && selectorType.isSelector()
+             && SelectorType(selectorType).getDomain() == dtt)
+          << "malformed selector in datatype post-resolution";
       // This next one's a "hard" check, performed in non-debug builds
       // as well; the other ones should all be guaranteed by the
       // CVC4::Datatype class, but this actually needs to be checked.
-      AlwaysAssert(!SelectorType(selectorType).getRangeType().d_typeNode->isFunctionLike(),
-                   "cannot put function-like things in datatypes");
+      AlwaysAssert(!SelectorType(selectorType)
+                        .getRangeType()
+                        .d_typeNode->isFunctionLike())
+          << "cannot put function-like things in datatypes";
     }
   }
 }
@@ -892,7 +892,9 @@ Type ExprManager::getType(Expr e, bool check)
 }
 
 Expr ExprManager::mkVar(const std::string& name, Type type, uint32_t flags) {
-  Assert(NodeManager::currentNM() == NULL, "ExprManager::mkVar() should only be called externally, not from within CVC4 code.  Please use mkSkolem().");
+  Assert(NodeManager::currentNM() == NULL)
+      << "ExprManager::mkVar() should only be called externally, not from "
+         "within CVC4 code.  Please use mkSkolem().";
   NodeManagerScope nms(d_nodeManager);
   Node* n = d_nodeManager->mkVarPtr(name, *type.d_typeNode, flags);
   Debug("nm") << "set " << name << " on " << *n << std::endl;
@@ -901,7 +903,9 @@ Expr ExprManager::mkVar(const std::string& name, Type type, uint32_t flags) {
 }
 
 Expr ExprManager::mkVar(Type type, uint32_t flags) {
-  Assert(NodeManager::currentNM() == NULL, "ExprManager::mkVar() should only be called externally, not from within CVC4 code.  Please use mkSkolem().");
+  Assert(NodeManager::currentNM() == NULL)
+      << "ExprManager::mkVar() should only be called externally, not from "
+         "within CVC4 code.  Please use mkSkolem().";
   NodeManagerScope nms(d_nodeManager);
   INC_STAT_VAR(type, false);
   return Expr(this, d_nodeManager->mkVarPtr(*type.d_typeNode, flags));
@@ -974,8 +978,8 @@ Expr ExprManager::mkAssociative(Kind kind,
 
   /* It would be really weird if this happened (it would require
    * min > 2, for one thing), but let's make sure. */
-  AlwaysAssert( newChildren.size() >= min,
-                "Too few new children in mkAssociative" );
+  AlwaysAssert(newChildren.size() >= min)
+      << "Too few new children in mkAssociative";
 
   // recurse
   return mkAssociative(kind, newChildren);
@@ -1085,8 +1089,8 @@ TypeNode exportTypeInternal(TypeNode n, NodeManager* from, NodeManager* to, Expr
 }/* CVC4::expr namespace */
 
 Type ExprManager::exportType(const Type& t, ExprManager* em, ExprManagerMapCollection& vmap) {
-  Assert(t.d_nodeManager != em->d_nodeManager,
-         "Can't export a Type to the same ExprManager");
+  Assert(t.d_nodeManager != em->d_nodeManager)
+      << "Can't export a Type to the same ExprManager";
   NodeManagerScope ems(t.d_nodeManager);
   return Type(em->d_nodeManager,
               new TypeNode(expr::exportTypeInternal(*t.d_typeNode, t.d_nodeManager, em->d_nodeManager, vmap)));
diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index 2338a7320..998f58d0c 100644
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -20,7 +20,7 @@
 #include <utility>
 #include <vector>
 
-#include "base/cvc4_assert.h"
+#include "base/check.h"
 #include "expr/expr_manager_scope.h"
 #include "expr/node.h"
 #include "expr/node_algorithm.h"
@@ -306,15 +306,15 @@ public:
 
 Expr Expr::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap,
                     uint32_t flags /* = 0 */) const {
-  Assert(d_exprManager != exprManager,
-         "No sense in cloning an Expr in the same ExprManager");
+  Assert(d_exprManager != exprManager)
+      << "No sense in cloning an Expr in the same ExprManager";
   ExprManagerScope ems(*this);
   return Expr(exprManager, new Node(expr::ExportPrivate(d_exprManager, exprManager, variableMap, flags).exportInternal(*d_node)));
 }
 
 Expr& Expr::operator=(const Expr& e) {
-  Assert(d_node != NULL, "Unexpected NULL expression pointer!");
-  Assert(e.d_node != NULL, "Unexpected NULL expression pointer!");
+  Assert(d_node != NULL) << "Unexpected NULL expression pointer!";
+  Assert(e.d_node != NULL) << "Unexpected NULL expression pointer!";
 
   if(this != &e) {
     if(d_exprManager == e.d_exprManager) {
@@ -342,8 +342,8 @@ bool Expr::operator==(const Expr& e) const {
     return false;
   }
   ExprManagerScope ems(*this);
-  Assert(d_node != NULL, "Unexpected NULL expression pointer!");
-  Assert(e.d_node != NULL, "Unexpected NULL expression pointer!");
+  Assert(d_node != NULL) << "Unexpected NULL expression pointer!";
+  Assert(e.d_node != NULL) << "Unexpected NULL expression pointer!";
   return *d_node == *e.d_node;
 }
 
@@ -352,8 +352,8 @@ bool Expr::operator!=(const Expr& e) const {
 }
 
 bool Expr::operator<(const Expr& e) const {
-  Assert(d_node != NULL, "Unexpected NULL expression pointer!");
-  Assert(e.d_node != NULL, "Unexpected NULL expression pointer!");
+  Assert(d_node != NULL) << "Unexpected NULL expression pointer!";
+  Assert(e.d_node != NULL) << "Unexpected NULL expression pointer!";
   if(isNull() && !e.isNull()) {
     return true;
   }
@@ -362,8 +362,8 @@ bool Expr::operator<(const Expr& e) const {
 }
 
 bool Expr::operator>(const Expr& e) const {
-  Assert(d_node != NULL, "Unexpected NULL expression pointer!");
-  Assert(e.d_node != NULL, "Unexpected NULL expression pointer!");
+  Assert(d_node != NULL) << "Unexpected NULL expression pointer!";
+  Assert(e.d_node != NULL) << "Unexpected NULL expression pointer!";
   if(isNull() && !e.isNull()) {
     return true;
   }
@@ -374,38 +374,38 @@ bool Expr::operator>(const Expr& e) const {
 uint64_t Expr::getId() const
 {
   ExprManagerScope ems(*this);
-  Assert(d_node != NULL, "Unexpected NULL expression pointer!");
+  Assert(d_node != NULL) << "Unexpected NULL expression pointer!";
   return d_node->getId();
 }
 
 Kind Expr::getKind() const {
   ExprManagerScope ems(*this);
-  Assert(d_node != NULL, "Unexpected NULL expression pointer!");
+  Assert(d_node != NULL) << "Unexpected NULL expression pointer!";
   return d_node->getKind();
 }
 
 size_t Expr::getNumChildren() const {
   ExprManagerScope ems(*this);
-  Assert(d_node != NULL, "Unexpected NULL expression pointer!");
+  Assert(d_node != NULL) << "Unexpected NULL expression pointer!";
   return d_node->getNumChildren();
 }
 
 Expr Expr::operator[](unsigned i) const {
   ExprManagerScope ems(*this);
-  Assert(d_node != NULL, "Unexpected NULL expression pointer!");
-  Assert(i >= 0 && i < d_node->getNumChildren(), "Child index out of bounds");
+  Assert(d_node != NULL) << "Unexpected NULL expression pointer!";
+  Assert(i >= 0 && i < d_node->getNumChildren()) << "Child index out of bounds";
   return Expr(d_exprManager, new Node((*d_node)[i]));
 }
 
 bool Expr::hasOperator() const {
   ExprManagerScope ems(*this);
-  Assert(d_node != NULL, "Unexpected NULL expression pointer!");
+  Assert(d_node != NULL) << "Unexpected NULL expression pointer!";
   return d_node->hasOperator();
 }
 
 Expr Expr::getOperator() const {
   ExprManagerScope ems(*this);
-  Assert(d_node != NULL, "Unexpected NULL expression pointer!");
+  Assert(d_node != NULL) << "Unexpected NULL expression pointer!";
   PrettyCheckArgument(d_node->hasOperator(), *this,
                       "Expr::getOperator() called on an Expr with no operator");
   return Expr(d_exprManager, new Node(d_node->getOperator()));
@@ -414,14 +414,14 @@ Expr Expr::getOperator() const {
 bool Expr::isParameterized() const
 {
   ExprManagerScope ems(*this);
-  Assert(d_node != NULL, "Unexpected NULL expression pointer!");
+  Assert(d_node != NULL) << "Unexpected NULL expression pointer!";
   return d_node->getMetaKind() == kind::metakind::PARAMETERIZED;
 }
 
 Type Expr::getType(bool check) const
 {
   ExprManagerScope ems(*this);
-  Assert(d_node != NULL, "Unexpected NULL expression pointer!");
+  Assert(d_node != NULL) << "Unexpected NULL expression pointer!";
   PrettyCheckArgument(!d_node->isNull(), this,
                       "Can't get type of null expression!");
   return d_exprManager->getType(*this, check);
@@ -553,32 +553,32 @@ Expr::const_iterator Expr::end() const {
 
 std::string Expr::toString() const {
   ExprManagerScope ems(*this);
-  Assert(d_node != NULL, "Unexpected NULL expression pointer!");
+  Assert(d_node != NULL) << "Unexpected NULL expression pointer!";
   return d_node->toString();
 }
 
 bool Expr::isNull() const {
   ExprManagerScope ems(*this);
-  Assert(d_node != NULL, "Unexpected NULL expression pointer!");
+  Assert(d_node != NULL) << "Unexpected NULL expression pointer!";
   return d_node->isNull();
 }
 
 bool Expr::isVariable() const {
   ExprManagerScope ems(*this);
-  Assert(d_node != NULL, "Unexpected NULL expression pointer!");
+  Assert(d_node != NULL) << "Unexpected NULL expression pointer!";
   return d_node->getMetaKind() == kind::metakind::VARIABLE;
 }
 
 bool Expr::isConst() const {
   ExprManagerScope ems(*this);
-  Assert(d_node != NULL, "Unexpected NULL expression pointer!");
+  Assert(d_node != NULL) << "Unexpected NULL expression pointer!";
   return d_node->isConst();
 }
 
 bool Expr::hasFreeVariable() const
 {
   ExprManagerScope ems(*this);
-  Assert(d_node != NULL, "Unexpected NULL expression pointer!");
+  Assert(d_node != NULL) << "Unexpected NULL expression pointer!";
   return expr::hasFreeVar(*d_node);
 }
 
@@ -591,30 +591,30 @@ void Expr::toStream(std::ostream& out, int depth, bool types, size_t dag,
 Node Expr::getNode() const { return *d_node; }
 TNode Expr::getTNode() const { return *d_node; }
 Expr Expr::notExpr() const {
-  Assert(d_exprManager != NULL,
-         "Don't have an expression manager for this expression!");
+  Assert(d_exprManager != NULL)
+      << "Don't have an expression manager for this expression!";
   return d_exprManager->mkExpr(NOT, *this);
 }
 
 Expr Expr::andExpr(const Expr& e) const {
-  Assert(d_exprManager != NULL,
-         "Don't have an expression manager for this expression!");
+  Assert(d_exprManager != NULL)
+      << "Don't have an expression manager for this expression!";
   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!");
+  Assert(d_exprManager != NULL)
+      << "Don't have an expression manager for this expression!";
   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!");
+  Assert(d_exprManager != NULL)
+      << "Don't have an expression manager for this expression!";
   PrettyCheckArgument(d_exprManager == e.d_exprManager, e,
                       "Different expression managers!");
   return d_exprManager->mkExpr(XOR, *this, e);
@@ -622,16 +622,16 @@ Expr Expr::xorExpr(const Expr& e) const {
 
 Expr Expr::eqExpr(const Expr& e) const
 {
-  Assert(d_exprManager != NULL,
-         "Don't have an expression manager for this expression!");
+  Assert(d_exprManager != NULL)
+      << "Don't have an expression manager for this expression!";
   PrettyCheckArgument(d_exprManager == e.d_exprManager, e,
                       "Different expression managers!");
   return d_exprManager->mkExpr(EQUAL, *this, e);
 }
 
 Expr Expr::impExpr(const Expr& e) const {
-  Assert(d_exprManager != NULL,
-         "Don't have an expression manager for this expression!");
+  Assert(d_exprManager != NULL)
+      << "Don't have an expression manager for this expression!";
   PrettyCheckArgument(d_exprManager == e.d_exprManager, e,
                       "Different expression managers!");
   return d_exprManager->mkExpr(IMPLIES, *this, e);
@@ -639,8 +639,8 @@ Expr Expr::impExpr(const Expr& e) const {
 
 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!");
+  Assert(d_exprManager != NULL)
+      << "Don't have an expression manager for this expression!";
   PrettyCheckArgument(d_exprManager == then_e.d_exprManager, then_e,
                       "Different expression managers!");
   PrettyCheckArgument(d_exprManager == else_e.d_exprManager, else_e,
@@ -684,7 +684,7 @@ static Node exportConstant(TNode n, NodeManager* to, ExprManagerMapCollection& v
   switch(n.getKind()) {
 ${exportConstant_cases}
 
-  default: Unhandled(n.getKind());
+default: Unhandled() << n.getKind();
   }
 
 }/* exportConstant() */
diff --git a/src/expr/kind_map.h b/src/expr/kind_map.h
index a5ae73802..3b49ad51a 100644
--- a/src/expr/kind_map.h
+++ b/src/expr/kind_map.h
@@ -23,7 +23,7 @@
 #include <stdint.h>
 #include <iterator>
 
-#include "base/cvc4_assert.h"
+#include "base/check.h"
 #include "expr/kind.h"
 
 namespace CVC4 {
diff --git a/src/expr/matcher.h b/src/expr/matcher.h
index 95ece7d23..9a2dad7d0 100644
--- a/src/expr/matcher.h
+++ b/src/expr/matcher.h
@@ -24,7 +24,6 @@
 #include <vector>
 #include <map>
 
-#include "base/cvc4_assert.h"
 #include "expr/node.h"
 #include "expr/type_node.h"
 
diff --git a/src/expr/metakind_template.cpp b/src/expr/metakind_template.cpp
index 5116392cb..83c7e6e2c 100644
--- a/src/expr/metakind_template.cpp
+++ b/src/expr/metakind_template.cpp
@@ -52,13 +52,14 @@ ${metakind_constantMaps}
 namespace kind {
 namespace metakind {
 
-size_t NodeValueCompare::constHash(const ::CVC4::expr::NodeValue* nv) {
+size_t NodeValueCompare::constHash(const ::CVC4::expr::NodeValue* nv)
+{
   Assert(nv->getMetaKind() == kind::metakind::CONSTANT);
 
-  switch(nv->d_kind) {
+  switch (nv->d_kind)
+  {
 ${metakind_constHashes}
-  default:
-    Unhandled(::CVC4::expr::NodeValue::dKindToKind(nv->d_kind));
+    default: Unhandled() << ::CVC4::expr::NodeValue::dKindToKind(nv->d_kind);
   }
 }
 
@@ -69,11 +70,12 @@ bool NodeValueCompare::compare(const ::CVC4::expr::NodeValue* nv1,
     return false;
   }
 
-  if(nv1->getMetaKind() == kind::metakind::CONSTANT) {
-    switch(nv1->d_kind) {
+  if (nv1->getMetaKind() == kind::metakind::CONSTANT)
+  {
+    switch (nv1->d_kind)
+    {
 ${metakind_compares}
-    default:
-      Unhandled(::CVC4::expr::NodeValue::dKindToKind(nv1->d_kind));
+      default: Unhandled() << ::CVC4::expr::NodeValue::dKindToKind(nv1->d_kind);
     }
   }
 
@@ -105,10 +107,10 @@ void NodeValueConstPrinter::toStream(std::ostream& out,
                                             const ::CVC4::expr::NodeValue* nv) {
   Assert(nv->getMetaKind() == kind::metakind::CONSTANT);
 
-  switch(nv->d_kind) {
+  switch (nv->d_kind)
+  {
 ${metakind_constPrinters}
-  default:
-    Unhandled(::CVC4::expr::NodeValue::dKindToKind(nv->d_kind));
+    default: Unhandled() << ::CVC4::expr::NodeValue::dKindToKind(nv->d_kind);
   }
 }
 
@@ -135,10 +137,10 @@ void NodeValueConstPrinter::toStream(std::ostream& out, TNode n) {
 void deleteNodeValueConstant(::CVC4::expr::NodeValue* nv) {
   Assert(nv->getMetaKind() == kind::metakind::CONSTANT);
 
-  switch(nv->d_kind) {
+  switch (nv->d_kind)
+  {
 ${metakind_constDeleters}
-  default:
-    Unhandled(::CVC4::expr::NodeValue::dKindToKind(nv->d_kind));
+    default: Unhandled() << ::CVC4::expr::NodeValue::dKindToKind(nv->d_kind);
   }
 }
 
diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h
index 1615d461b..c4d35b7dc 100644
--- a/src/expr/metakind_template.h
+++ b/src/expr/metakind_template.h
@@ -21,7 +21,7 @@
 
 #include <iosfwd>
 
-#include "base/cvc4_assert.h"
+#include "base/check.h"
 #include "expr/kind.h"
 
 namespace CVC4 {
diff --git a/src/expr/mkkind b/src/expr/mkkind
index a8a74b5a6..8e45b94ba 100755
--- a/src/expr/mkkind
+++ b/src/expr/mkkind
@@ -274,7 +274,7 @@ function register_sort {
     fi
   else
     type_constant_groundterms="${type_constant_groundterms}#line $lineno \"$kf\"
-  case $id: Unhandled(tc);
+  case $id: Unhandled() << tc;
 "
   fi
 }
@@ -323,7 +323,7 @@ function register_wellfoundedness {
 "
   else
     type_groundterms="${type_groundterms}#line $lineno \"$kf\"
-  case $id: Unhandled(typeNode);
+  case $id: Unhandled() << typeNode;
 "
   fi
   if [ -n "$header" ]; then
diff --git a/src/expr/node.h b/src/expr/node.h
index e0231bef6..cd3c99a78 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -33,15 +33,15 @@
 #include <utility>
 #include <vector>
 
+#include "base/check.h"
 #include "base/configuration.h"
-#include "base/cvc4_assert.h"
 #include "base/exception.h"
 #include "base/output.h"
-#include "expr/type.h"
-#include "expr/kind.h"
-#include "expr/metakind.h"
 #include "expr/expr.h"
 #include "expr/expr_iomanip.h"
+#include "expr/kind.h"
+#include "expr/metakind.h"
+#include "expr/type.h"
 #include "options/language.h"
 #include "options/set_language.h"
 #include "util/hash.h"
@@ -226,7 +226,7 @@ class NodeTemplate {
   inline void assertTNodeNotExpired() const
   {
     if(!ref_count) {
-      Assert( d_nv->d_rc > 0, "TNode pointing to an expired NodeValue" );
+      Assert(d_nv->d_rc > 0) << "TNode pointing to an expired NodeValue";
     }
   }
 
@@ -1022,9 +1022,9 @@ template <bool ref_count>
 template <class AttrKind>
 inline typename AttrKind::value_type NodeTemplate<ref_count>::
 getAttribute(const AttrKind&) const {
-  Assert( NodeManager::currentNM() != NULL,
-          "There is no current CVC4::NodeManager associated to this thread.\n"
-          "Perhaps a public-facing function is missing a NodeManagerScope ?" );
+  Assert(NodeManager::currentNM() != NULL)
+      << "There is no current CVC4::NodeManager associated to this thread.\n"
+         "Perhaps a public-facing function is missing a NodeManagerScope ?";
 
   assertTNodeNotExpired();
 
@@ -1035,9 +1035,9 @@ template <bool ref_count>
 template <class AttrKind>
 inline bool NodeTemplate<ref_count>::
 hasAttribute(const AttrKind&) const {
-  Assert( NodeManager::currentNM() != NULL,
-          "There is no current CVC4::NodeManager associated to this thread.\n"
-          "Perhaps a public-facing function is missing a NodeManagerScope ?" );
+  Assert(NodeManager::currentNM() != NULL)
+      << "There is no current CVC4::NodeManager associated to this thread.\n"
+         "Perhaps a public-facing function is missing a NodeManagerScope ?";
 
   assertTNodeNotExpired();
 
@@ -1048,9 +1048,9 @@ template <bool ref_count>
 template <class AttrKind>
 inline bool NodeTemplate<ref_count>::getAttribute(const AttrKind&,
                                                   typename AttrKind::value_type& ret) const {
-  Assert( NodeManager::currentNM() != NULL,
-          "There is no current CVC4::NodeManager associated to this thread.\n"
-          "Perhaps a public-facing function is missing a NodeManagerScope ?" );
+  Assert(NodeManager::currentNM() != NULL)
+      << "There is no current CVC4::NodeManager associated to this thread.\n"
+         "Perhaps a public-facing function is missing a NodeManagerScope ?";
 
   assertTNodeNotExpired();
 
@@ -1061,9 +1061,9 @@ template <bool ref_count>
 template <class AttrKind>
 inline void NodeTemplate<ref_count>::
 setAttribute(const AttrKind&, const typename AttrKind::value_type& value) {
-  Assert( NodeManager::currentNM() != NULL,
-          "There is no current CVC4::NodeManager associated to this thread.\n"
-          "Perhaps a public-facing function is missing a NodeManagerScope ?" );
+  Assert(NodeManager::currentNM() != NULL)
+      << "There is no current CVC4::NodeManager associated to this thread.\n"
+         "Perhaps a public-facing function is missing a NodeManagerScope ?";
 
   assertTNodeNotExpired();
 
@@ -1080,12 +1080,12 @@ NodeTemplate<ref_count> NodeTemplate<ref_count>::s_null(&expr::NodeValue::null()
 template <bool ref_count>
 NodeTemplate<ref_count>::NodeTemplate(const expr::NodeValue* ev) :
   d_nv(const_cast<expr::NodeValue*> (ev)) {
-  Assert(d_nv != NULL, "Expecting a non-NULL expression value!");
+  Assert(d_nv != NULL) << "Expecting a non-NULL expression value!";
   if(ref_count) {
     d_nv->inc();
   } else {
-    Assert(d_nv->d_rc > 0 || d_nv == &expr::NodeValue::null(),
-           "TNode constructed from NodeValue with rc == 0");
+    Assert(d_nv->d_rc > 0 || d_nv == &expr::NodeValue::null())
+        << "TNode constructed from NodeValue with rc == 0";
   }
 }
 
@@ -1095,37 +1095,37 @@ NodeTemplate<ref_count>::NodeTemplate(const expr::NodeValue* ev) :
 
 template <bool ref_count>
 NodeTemplate<ref_count>::NodeTemplate(const NodeTemplate<!ref_count>& e) {
-  Assert(e.d_nv != NULL, "Expecting a non-NULL expression value!");
+  Assert(e.d_nv != NULL) << "Expecting a non-NULL expression value!";
   d_nv = e.d_nv;
   if(ref_count) {
-    Assert(d_nv->d_rc > 0, "Node constructed from TNode with rc == 0");
+    Assert(d_nv->d_rc > 0) << "Node constructed from TNode with rc == 0";
     d_nv->inc();
   } else {
     // shouldn't ever fail
-    Assert(d_nv->d_rc > 0, "TNode constructed from Node with rc == 0");
+    Assert(d_nv->d_rc > 0) << "TNode constructed from Node with rc == 0";
   }
 }
 
 template <bool ref_count>
 NodeTemplate<ref_count>::NodeTemplate(const NodeTemplate& e) {
-  Assert(e.d_nv != NULL, "Expecting a non-NULL expression value!");
+  Assert(e.d_nv != NULL) << "Expecting a non-NULL expression value!";
   d_nv = e.d_nv;
   if(ref_count) {
     // shouldn't ever fail
-    Assert(d_nv->d_rc > 0, "Node constructed from Node with rc == 0");
+    Assert(d_nv->d_rc > 0) << "Node constructed from Node with rc == 0";
     d_nv->inc();
   } else {
-    Assert(d_nv->d_rc > 0, "TNode constructed from TNode with rc == 0");
+    Assert(d_nv->d_rc > 0) << "TNode constructed from TNode with rc == 0";
   }
 }
 
 template <bool ref_count>
 NodeTemplate<ref_count>::NodeTemplate(const Expr& e) {
-  Assert(e.d_node != NULL, "Expecting a non-NULL expression value!");
-  Assert(e.d_node->d_nv != NULL, "Expecting a non-NULL expression value!");
+  Assert(e.d_node != NULL) << "Expecting a non-NULL expression value!";
+  Assert(e.d_node->d_nv != NULL) << "Expecting a non-NULL expression value!";
   d_nv = e.d_node->d_nv;
   // shouldn't ever fail
-  Assert(d_nv->d_rc > 0, "Node constructed from Expr with rc == 0");
+  Assert(d_nv->d_rc > 0) << "Node constructed from Expr with rc == 0";
   if(ref_count) {
     d_nv->inc();
   }
@@ -1133,10 +1133,10 @@ NodeTemplate<ref_count>::NodeTemplate(const Expr& e) {
 
 template <bool ref_count>
 NodeTemplate<ref_count>::~NodeTemplate() {
-  Assert(d_nv != NULL, "Expecting a non-NULL expression value!");
+  Assert(d_nv != NULL) << "Expecting a non-NULL expression value!";
   if(ref_count) {
     // shouldn't ever fail
-    Assert(d_nv->d_rc > 0, "Node reference count would be negative");
+    Assert(d_nv->d_rc > 0) << "Node reference count would be negative";
     d_nv->dec();
   }
 }
@@ -1147,29 +1147,28 @@ void NodeTemplate<ref_count>::assignNodeValue(expr::NodeValue* ev) {
   if(ref_count) {
     d_nv->inc();
   } else {
-    Assert(d_nv->d_rc > 0, "TNode assigned to NodeValue with rc == 0");
+    Assert(d_nv->d_rc > 0) << "TNode assigned to NodeValue with rc == 0";
   }
 }
 
 template <bool ref_count>
 NodeTemplate<ref_count>& NodeTemplate<ref_count>::
 operator=(const NodeTemplate& e) {
-  Assert(d_nv != NULL, "Expecting a non-NULL expression value!");
-  Assert(e.d_nv != NULL, "Expecting a non-NULL expression value on RHS!");
+  Assert(d_nv != NULL) << "Expecting a non-NULL expression value!";
+  Assert(e.d_nv != NULL) << "Expecting a non-NULL expression value on RHS!";
   if(__builtin_expect( ( d_nv != e.d_nv ), true )) {
     if(ref_count) {
       // shouldn't ever fail
-      Assert(d_nv->d_rc > 0,
-             "Node reference count would be negative");
+      Assert(d_nv->d_rc > 0) << "Node reference count would be negative";
       d_nv->dec();
     }
     d_nv = e.d_nv;
     if(ref_count) {
       // shouldn't ever fail
-      Assert(d_nv->d_rc > 0, "Node assigned from Node with rc == 0");
+      Assert(d_nv->d_rc > 0) << "Node assigned from Node with rc == 0";
       d_nv->inc();
     } else {
-      Assert(d_nv->d_rc > 0, "TNode assigned from TNode with rc == 0");
+      Assert(d_nv->d_rc > 0) << "TNode assigned from TNode with rc == 0";
     }
   }
   return *this;
@@ -1178,21 +1177,21 @@ operator=(const NodeTemplate& e) {
 template <bool ref_count>
 NodeTemplate<ref_count>& NodeTemplate<ref_count>::
 operator=(const NodeTemplate<!ref_count>& e) {
-  Assert(d_nv != NULL, "Expecting a non-NULL expression value!");
-  Assert(e.d_nv != NULL, "Expecting a non-NULL expression value on RHS!");
+  Assert(d_nv != NULL) << "Expecting a non-NULL expression value!";
+  Assert(e.d_nv != NULL) << "Expecting a non-NULL expression value on RHS!";
   if(__builtin_expect( ( d_nv != e.d_nv ), true )) {
     if(ref_count) {
       // shouldn't ever fail
-      Assert(d_nv->d_rc > 0, "Node reference count would be negative");
+      Assert(d_nv->d_rc > 0) << "Node reference count would be negative";
       d_nv->dec();
     }
     d_nv = e.d_nv;
     if(ref_count) {
-      Assert(d_nv->d_rc > 0, "Node assigned from TNode with rc == 0");
+      Assert(d_nv->d_rc > 0) << "Node assigned from TNode with rc == 0";
       d_nv->inc();
     } else {
       // shouldn't ever happen
-      Assert(d_nv->d_rc > 0, "TNode assigned from Node with rc == 0");
+      Assert(d_nv->d_rc > 0) << "TNode assigned from Node with rc == 0";
     }
   }
   return *this;
@@ -1273,9 +1272,9 @@ NodeTemplate<ref_count>::printAst(std::ostream& out, int indent) const {
  */
 template <bool ref_count>
 NodeTemplate<true> NodeTemplate<ref_count>::getOperator() const {
-  Assert( NodeManager::currentNM() != NULL,
-          "There is no current CVC4::NodeManager associated to this thread.\n"
-          "Perhaps a public-facing function is missing a NodeManagerScope ?" );
+  Assert(NodeManager::currentNM() != NULL)
+      << "There is no current CVC4::NodeManager associated to this thread.\n"
+         "Perhaps a public-facing function is missing a NodeManagerScope ?";
 
   assertTNodeNotExpired();
 
@@ -1301,8 +1300,7 @@ NodeTemplate<true> NodeTemplate<ref_count>::getOperator() const {
   case kind::metakind::NULLARY_OPERATOR:
     IllegalArgument(*this, "getOperator() called on Node with NULLARY_OPERATOR-kinded kind");
 
-  default:
-    Unhandled(mk);
+  default: Unhandled() << mk;
   }
 }
 
@@ -1319,9 +1317,9 @@ inline bool NodeTemplate<ref_count>::hasOperator() const {
 template <bool ref_count>
 TypeNode NodeTemplate<ref_count>::getType(bool check) const
 {
-  Assert( NodeManager::currentNM() != NULL,
-          "There is no current CVC4::NodeManager associated to this thread.\n"
-          "Perhaps a public-facing function is missing a NodeManagerScope ?" );
+  Assert(NodeManager::currentNM() != NULL)
+      << "There is no current CVC4::NodeManager associated to this thread.\n"
+         "Perhaps a public-facing function is missing a NodeManagerScope ?";
 
   assertTNodeNotExpired();
 
@@ -1409,8 +1407,9 @@ NodeTemplate<ref_count>::substitute(Iterator1 nodesBegin,
   }
 
   // otherwise compute
-  Assert( std::distance(nodesBegin, nodesEnd) == std::distance(replacementsBegin, replacementsEnd),
-          "Substitution iterator ranges must be equal size" );
+  Assert(std::distance(nodesBegin, nodesEnd)
+         == std::distance(replacementsBegin, replacementsEnd))
+      << "Substitution iterator ranges must be equal size";
   Iterator1 j = find(nodesBegin, nodesEnd, TNode(*this));
   if(j != nodesEnd) {
     Iterator2 b = replacementsBegin;
diff --git a/src/expr/node_algorithm.cpp b/src/expr/node_algorithm.cpp
index 59e3d3b03..eda4dadd2 100644
--- a/src/expr/node_algorithm.cpp
+++ b/src/expr/node_algorithm.cpp
@@ -436,8 +436,8 @@ Node substituteCaptureAvoiding(TNode n,
   std::vector<TNode> visit;
   TNode curr;
   visit.push_back(n);
-  Assert(src.size() == dest.size(),
-         "Substitution domain and range must be equal size");
+  Assert(src.size() == dest.size())
+      << "Substitution domain and range must be equal size";
   do
   {
     curr = visit.back();
diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h
index b5e99c6fd..b6594a933 100644
--- a/src/expr/node_builder.h
+++ b/src/expr/node_builder.h
@@ -170,13 +170,12 @@ namespace CVC4 {
   class NodeManager;
 }/* CVC4 namespace */
 
-#include "base/cvc4_assert.h"
+#include "base/check.h"
 #include "base/output.h"
 #include "expr/kind.h"
 #include "expr/metakind.h"
 #include "expr/node_value.h"
 
-
 namespace CVC4 {
 
 // Sometimes it's useful for debugging to output a NodeBuilder that
@@ -231,10 +230,9 @@ class NodeBuilder {
    * Set this NodeBuilder to the `used' state.
    */
   inline void setUsed() {
-    Assert(!isUsed(), "Internal error: bad `used' state in NodeBuilder!");
-    Assert(d_inlineNv.d_nchildren == 0 &&
-           d_nvMaxChildren == nchild_thresh,
-           "Internal error: bad `inline' state in NodeBuilder!");
+    Assert(!isUsed()) << "Internal error: bad `used' state in NodeBuilder!";
+    Assert(d_inlineNv.d_nchildren == 0 && d_nvMaxChildren == nchild_thresh)
+        << "Internal error: bad `inline' state in NodeBuilder!";
     d_nv = NULL;
   }
 
@@ -243,10 +241,9 @@ class NodeBuilder {
    * from clear().
    */
   inline void setUnused() {
-    Assert(isUsed(), "Internal error: bad `used' state in NodeBuilder!");
-    Assert(d_inlineNv.d_nchildren == 0 &&
-           d_nvMaxChildren == nchild_thresh,
-           "Internal error: bad `inline' state in NodeBuilder!");
+    Assert(isUsed()) << "Internal error: bad `used' state in NodeBuilder!";
+    Assert(d_inlineNv.d_nchildren == 0 && d_nvMaxChildren == nchild_thresh)
+        << "Internal error: bad `inline' state in NodeBuilder!";
     d_nv = &d_inlineNv;
   }
 
@@ -381,9 +378,8 @@ public:
     d_nv(&d_inlineNv),
     d_nm(NodeManager::currentNM()),
     d_nvMaxChildren(nchild_thresh) {
-
-    Assert(k != kind::NULL_EXPR && k != kind::UNDEFINED_KIND,
-           "illegal Node-building kind");
+    Assert(k != kind::NULL_EXPR && k != kind::UNDEFINED_KIND)
+        << "illegal Node-building kind";
 
     d_inlineNv.d_id = 1; // have a kind already
     d_inlineNv.d_rc = 0;
@@ -406,9 +402,8 @@ public:
     d_nv(&d_inlineNv),
     d_nm(nm),
     d_nvMaxChildren(nchild_thresh) {
-
-    Assert(k != kind::NULL_EXPR && k != kind::UNDEFINED_KIND,
-           "illegal Node-building kind");
+    Assert(k != kind::NULL_EXPR && k != kind::UNDEFINED_KIND)
+        << "illegal Node-building kind";
 
     d_inlineNv.d_id = 1; // have a kind already
     d_inlineNv.d_rc = 0;
@@ -461,48 +456,48 @@ public:
 
   /** Get the begin-const-iterator of this Node-under-construction. */
   inline const_iterator begin() const {
-    Assert(!isUsed(), "NodeBuilder is one-shot only; "
-           "attempt to access it after conversion");
-    Assert(getKind() != kind::UNDEFINED_KIND,
-           "Iterators over NodeBuilder<> are undefined "
-           "until a Kind is set");
+    Assert(!isUsed()) << "NodeBuilder is one-shot only; "
+                         "attempt to access it after conversion";
+    Assert(getKind() != kind::UNDEFINED_KIND)
+        << "Iterators over NodeBuilder<> are undefined "
+           "until a Kind is set";
     return d_nv->begin< NodeTemplate<true> >();
   }
 
   /** Get the end-const-iterator of this Node-under-construction. */
   inline const_iterator end() const {
-    Assert(!isUsed(), "NodeBuilder is one-shot only; "
-           "attempt to access it after conversion");
-    Assert(getKind() != kind::UNDEFINED_KIND,
-           "Iterators over NodeBuilder<> are undefined "
-           "until a Kind is set");
+    Assert(!isUsed()) << "NodeBuilder is one-shot only; "
+                         "attempt to access it after conversion";
+    Assert(getKind() != kind::UNDEFINED_KIND)
+        << "Iterators over NodeBuilder<> are undefined "
+           "until a Kind is set";
     return d_nv->end< NodeTemplate<true> >();
   }
 
   /** Get the kind of this Node-under-construction. */
   inline Kind getKind() const {
-    Assert(!isUsed(), "NodeBuilder is one-shot only; "
-           "attempt to access it after conversion");
+    Assert(!isUsed()) << "NodeBuilder is one-shot only; "
+                         "attempt to access it after conversion";
     return d_nv->getKind();
   }
 
   /** Get the kind of this Node-under-construction. */
   inline kind::MetaKind getMetaKind() const {
-    Assert(!isUsed(), "NodeBuilder is one-shot only; "
-           "attempt to access it after conversion");
-    Assert(getKind() != kind::UNDEFINED_KIND,
-           "The metakind of a NodeBuilder<> is undefined "
-           "until a Kind is set");
+    Assert(!isUsed()) << "NodeBuilder is one-shot only; "
+                         "attempt to access it after conversion";
+    Assert(getKind() != kind::UNDEFINED_KIND)
+        << "The metakind of a NodeBuilder<> is undefined "
+           "until a Kind is set";
     return d_nv->getMetaKind();
   }
 
   /** Get the current number of children of this Node-under-construction. */
   inline unsigned getNumChildren() const {
-    Assert(!isUsed(), "NodeBuilder is one-shot only; "
-           "attempt to access it after conversion");
-    Assert(getKind() != kind::UNDEFINED_KIND,
-           "The number of children of a NodeBuilder<> is undefined "
-           "until a Kind is set");
+    Assert(!isUsed()) << "NodeBuilder is one-shot only; "
+                         "attempt to access it after conversion";
+    Assert(getKind() != kind::UNDEFINED_KIND)
+        << "The number of children of a NodeBuilder<> is undefined "
+           "until a Kind is set";
     return d_nv->getNumChildren();
   }
 
@@ -512,15 +507,15 @@ public:
    * that is of PARAMETERIZED metakind.
    */
   inline Node getOperator() const {
-    Assert(!isUsed(), "NodeBuilder is one-shot only; "
-           "attempt to access it after conversion");
-    Assert(getKind() != kind::UNDEFINED_KIND,
-           "NodeBuilder<> operator access is not permitted "
-           "until a Kind is set");
-    Assert(getMetaKind() == kind::metakind::PARAMETERIZED,
-           "NodeBuilder<> operator access is only permitted "
-           "on parameterized kinds, not `%s'",
-           kind::kindToString(getKind()).c_str());
+    Assert(!isUsed()) << "NodeBuilder is one-shot only; "
+                         "attempt to access it after conversion";
+    Assert(getKind() != kind::UNDEFINED_KIND)
+        << "NodeBuilder<> operator access is not permitted "
+           "until a Kind is set";
+    Assert(getMetaKind() == kind::metakind::PARAMETERIZED)
+        << "NodeBuilder<> operator access is only permitted "
+           "on parameterized kinds, not `"
+        << getKind() << "'";
     return Node(d_nv->getOperator());
   }
 
@@ -529,13 +524,13 @@ public:
    * if this NodeBuilder is unused and has a defined kind.
    */
   inline Node getChild(int i) const {
-    Assert(!isUsed(), "NodeBuilder is one-shot only; "
-           "attempt to access it after conversion");
-    Assert(getKind() != kind::UNDEFINED_KIND,
-           "NodeBuilder<> child access is not permitted "
-           "until a Kind is set");
-    Assert(i >= 0 && unsigned(i) < d_nv->getNumChildren(),
-           "index out of range for NodeBuilder::getChild()");
+    Assert(!isUsed()) << "NodeBuilder is one-shot only; "
+                         "attempt to access it after conversion";
+    Assert(getKind() != kind::UNDEFINED_KIND)
+        << "NodeBuilder<> child access is not permitted "
+           "until a Kind is set";
+    Assert(i >= 0 && unsigned(i) < d_nv->getNumChildren())
+        << "index out of range for NodeBuilder::getChild()";
     return Node(d_nv->getChild(i));
   }
 
@@ -562,12 +557,12 @@ public:
 
   /** Set the Kind of this Node-under-construction. */
   inline NodeBuilder<nchild_thresh>& operator<<(const Kind& k) {
-    Assert(!isUsed(), "NodeBuilder is one-shot only; "
-           "attempt to access it after conversion");
-    Assert(getKind() == kind::UNDEFINED_KIND || d_nv->d_id == 0,
-           "can't redefine the Kind of a NodeBuilder");
-    Assert(d_nv->d_id == 0,
-           "internal inconsistency with NodeBuilder: d_id != 0");
+    Assert(!isUsed()) << "NodeBuilder is one-shot only; "
+                         "attempt to access it after conversion";
+    Assert(getKind() == kind::UNDEFINED_KIND || d_nv->d_id == 0)
+        << "can't redefine the Kind of a NodeBuilder";
+    Assert(d_nv->d_id == 0)
+        << "internal inconsistency with NodeBuilder: d_id != 0";
     AssertArgument(k != kind::UNDEFINED_KIND &&
                    k != kind::NULL_EXPR &&
                    k < kind::LAST_KIND,
@@ -592,8 +587,8 @@ public:
    * append the given Node as a child.  Otherwise, simply append.
    */
   NodeBuilder<nchild_thresh>& operator<<(TNode n) {
-    Assert(!isUsed(), "NodeBuilder is one-shot only; "
-           "attempt to access it after conversion");
+    Assert(!isUsed()) << "NodeBuilder is one-shot only; "
+                         "attempt to access it after conversion";
     // This test means: we didn't have a Kind at the beginning (on
     // NodeBuilder construction or at the last clear()), but we do
     // now.  That means we appended a Kind with operator<<(Kind),
@@ -611,8 +606,8 @@ public:
    * append the given Node as a child.  Otherwise, simply append.
    */
   NodeBuilder<nchild_thresh>& operator<<(TypeNode n) {
-    Assert(!isUsed(), "NodeBuilder is one-shot only; "
-           "attempt to access it after conversion");
+    Assert(!isUsed()) << "NodeBuilder is one-shot only; "
+                         "attempt to access it after conversion";
     // This test means: we didn't have a Kind at the beginning (on
     // NodeBuilder construction or at the last clear()), but we do
     // now.  That means we appended a Kind with operator<<(Kind),
@@ -628,8 +623,8 @@ public:
   /** Append a sequence of children to this TypeNode-under-construction. */
   inline NodeBuilder<nchild_thresh>&
   append(const std::vector<TypeNode>& children) {
-    Assert(!isUsed(), "NodeBuilder is one-shot only; "
-           "attempt to access it after conversion");
+    Assert(!isUsed()) << "NodeBuilder is one-shot only; "
+                         "attempt to access it after conversion";
     return append(children.begin(), children.end());
   }
 
@@ -637,16 +632,16 @@ public:
   template <bool ref_count>
   inline NodeBuilder<nchild_thresh>&
   append(const std::vector<NodeTemplate<ref_count> >& children) {
-    Assert(!isUsed(), "NodeBuilder is one-shot only; "
-           "attempt to access it after conversion");
+    Assert(!isUsed()) << "NodeBuilder is one-shot only; "
+                         "attempt to access it after conversion";
     return append(children.begin(), children.end());
   }
 
   /** Append a sequence of children to this Node-under-construction. */
   template <class Iterator>
   NodeBuilder<nchild_thresh>& append(const Iterator& begin, const Iterator& end) {
-    Assert(!isUsed(), "NodeBuilder is one-shot only; "
-           "attempt to access it after conversion");
+    Assert(!isUsed()) << "NodeBuilder is one-shot only; "
+                         "attempt to access it after conversion";
     for(Iterator i = begin; i != end; ++i) {
       append(*i);
     }
@@ -655,9 +650,9 @@ public:
 
   /** Append a child to this Node-under-construction. */
   NodeBuilder<nchild_thresh>& append(TNode n) {
-    Assert(!isUsed(), "NodeBuilder is one-shot only; "
-           "attempt to access it after conversion");
-    Assert(!n.isNull(), "Cannot use NULL Node as a child of a Node");
+    Assert(!isUsed()) << "NodeBuilder is one-shot only; "
+                         "attempt to access it after conversion";
+    Assert(!n.isNull()) << "Cannot use NULL Node as a child of a Node";
     if(n.getKind() == kind::BUILTIN) {
       return *this << NodeManager::operatorToKind(n);
     }
@@ -671,9 +666,9 @@ public:
 
   /** Append a child to this Node-under-construction. */
   NodeBuilder<nchild_thresh>& append(const TypeNode& typeNode) {
-    Assert(!isUsed(), "NodeBuilder is one-shot only; "
-           "attempt to access it after conversion");
-    Assert(!typeNode.isNull(), "Cannot use NULL Node as a child of a Node");
+    Assert(!isUsed()) << "NodeBuilder is one-shot only; "
+                         "attempt to access it after conversion";
+    Assert(!typeNode.isNull()) << "Cannot use NULL Node as a child of a Node";
     allocateNvIfNecessaryForAppend();
     expr::NodeValue* nv = typeNode.d_nv;
     nv->inc();
@@ -751,7 +746,7 @@ namespace CVC4 {
 
 template <unsigned nchild_thresh>
 void NodeBuilder<nchild_thresh>::clear(Kind k) {
-  Assert(k != kind::NULL_EXPR, "illegal Node-building clear kind");
+  Assert(k != kind::NULL_EXPR) << "illegal Node-building clear kind";
 
   if(__builtin_expect( ( nvIsAllocated() ), false )) {
     dealloc();
@@ -774,13 +769,11 @@ void NodeBuilder<nchild_thresh>::clear(Kind k) {
 
 template <unsigned nchild_thresh>
 void NodeBuilder<nchild_thresh>::realloc(size_t toSize) {
-  AlwaysAssert(toSize > d_nvMaxChildren,
-               "attempt to realloc() a NodeBuilder to a smaller/equal size!");
-  Assert(toSize < (static_cast<size_t>(1) << expr::NodeValue::NBITS_NCHILDREN),
-         "attempt to realloc() a NodeBuilder to size %lu (beyond hard limit of "
-         "%u)",
-         toSize,
-         expr::NodeValue::MAX_CHILDREN);
+  AlwaysAssert(toSize > d_nvMaxChildren)
+      << "attempt to realloc() a NodeBuilder to a smaller/equal size!";
+  Assert(toSize < (static_cast<size_t>(1) << expr::NodeValue::NBITS_NCHILDREN))
+      << "attempt to realloc() a NodeBuilder to size " << toSize
+      << " (beyond hard limit of " << expr::NodeValue::MAX_CHILDREN << ")";
 
   if(__builtin_expect( ( nvIsAllocated() ), false )) {
     // Ensure d_nv is not modified on allocation failure
@@ -793,7 +786,7 @@ void NodeBuilder<nchild_thresh>::realloc(size_t toSize) {
       throw std::bad_alloc();
     }
     d_nvMaxChildren = toSize;
-    Assert(d_nvMaxChildren == toSize);//overflow check
+    Assert(d_nvMaxChildren == toSize);  // overflow check
     // Here, the copy (between two heap-allocated buffers) has already
     // been done for us by the std::realloc().
     d_nv = newBlock;
@@ -806,7 +799,7 @@ void NodeBuilder<nchild_thresh>::realloc(size_t toSize) {
       throw std::bad_alloc();
     }
     d_nvMaxChildren = toSize;
-    Assert(d_nvMaxChildren == toSize);//overflow check
+    Assert(d_nvMaxChildren == toSize);  // overflow check
 
     d_nv = newBlock;
     d_nv->d_id = d_inlineNv.d_id;
@@ -825,9 +818,9 @@ void NodeBuilder<nchild_thresh>::realloc(size_t toSize) {
 
 template <unsigned nchild_thresh>
 void NodeBuilder<nchild_thresh>::dealloc() {
-  Assert( nvIsAllocated(),
-          "Internal error: NodeBuilder: dealloc() called without a "
-          "private NodeBuilder-allocated buffer" );
+  Assert(nvIsAllocated())
+      << "Internal error: NodeBuilder: dealloc() called without a "
+         "private NodeBuilder-allocated buffer";
 
   for(expr::NodeValue::nv_iterator i = d_nv->nv_begin();
       i != d_nv->nv_end();
@@ -842,9 +835,9 @@ void NodeBuilder<nchild_thresh>::dealloc() {
 
 template <unsigned nchild_thresh>
 void NodeBuilder<nchild_thresh>::decrRefCounts() {
-  Assert( !nvIsAllocated(),
-          "Internal error: NodeBuilder: decrRefCounts() called with a "
-          "private NodeBuilder-allocated buffer" );
+  Assert(!nvIsAllocated())
+      << "Internal error: NodeBuilder: decrRefCounts() called with a "
+         "private NodeBuilder-allocated buffer";
 
   for(expr::NodeValue::nv_iterator i = d_inlineNv.nv_begin();
       i != d_inlineNv.nv_end();
@@ -918,10 +911,10 @@ NodeBuilder<nchild_thresh>::operator TypeNode() const {
 
 template <unsigned nchild_thresh>
 expr::NodeValue* NodeBuilder<nchild_thresh>::constructNV() {
-  Assert(!isUsed(), "NodeBuilder is one-shot only; "
-         "attempt to access it after conversion");
-  Assert(getKind() != kind::UNDEFINED_KIND,
-         "Can't make an expression of an undefined kind!");
+  Assert(!isUsed()) << "NodeBuilder is one-shot only; "
+                       "attempt to access it after conversion";
+  Assert(getKind() != kind::UNDEFINED_KIND)
+      << "Can't make an expression of an undefined kind!";
 
   // NOTE: The comments in this function refer to the cases in the
   // file comments at the top of this file.
@@ -933,12 +926,12 @@ expr::NodeValue* NodeBuilder<nchild_thresh>::constructNV() {
      * and we don't keep VARIABLE-kinded Nodes in the NodeManager
      * pool. */
 
-    Assert( ! nvIsAllocated(),
-            "internal NodeBuilder error: "
-            "VARIABLE-kinded NodeBuilder is heap-allocated !?" );
-    Assert( d_inlineNv.d_nchildren == 0,
-            "improperly-formed VARIABLE-kinded NodeBuilder: "
-            "no children permitted" );
+    Assert(!nvIsAllocated())
+        << "internal NodeBuilder error: "
+           "VARIABLE-kinded NodeBuilder is heap-allocated !?";
+    Assert(d_inlineNv.d_nchildren == 0)
+        << "improperly-formed VARIABLE-kinded NodeBuilder: "
+           "no children permitted";
 
     // we have to copy the inline NodeValue out
     expr::NodeValue* nv = (expr::NodeValue*)
@@ -963,20 +956,20 @@ expr::NodeValue* NodeBuilder<nchild_thresh>::constructNV() {
   }
 
   // check that there are the right # of children for this kind
-  Assert(getMetaKind() != kind::metakind::CONSTANT,
-         "Cannot make Nodes with NodeBuilder that have CONSTANT-kinded kinds");
-  Assert(getNumChildren() >= kind::metakind::getLowerBoundForKind(getKind()),
-         "Nodes with kind %s must have at least %u children (the one under "
-         "construction has %u)",
-         kind::kindToString(getKind()).c_str(),
-         kind::metakind::getLowerBoundForKind(getKind()),
-         getNumChildren());
-  Assert(getNumChildren() <= kind::metakind::getUpperBoundForKind(getKind()),
-         "Nodes with kind %s must have at most %u children (the one under "
-         "construction has %u)",
-         kind::kindToString(getKind()).c_str(),
-         kind::metakind::getUpperBoundForKind(getKind()),
-         getNumChildren());
+  Assert(getMetaKind() != kind::metakind::CONSTANT)
+      << "Cannot make Nodes with NodeBuilder that have CONSTANT-kinded kinds";
+  Assert(getNumChildren() >= kind::metakind::getLowerBoundForKind(getKind()))
+      << "Nodes with kind " << getKind() << " must have at least "
+      << kind::metakind::getLowerBoundForKind(getKind())
+      << " children (the one under "
+         "construction has "
+      << getNumChildren() << ")";
+  Assert(getNumChildren() <= kind::metakind::getUpperBoundForKind(getKind()))
+      << "Nodes with kind " << getKind() << " must have at most "
+      << kind::metakind::getUpperBoundForKind(getKind())
+      << " children (the one under "
+         "construction has "
+      << getNumChildren() << ")";
 
   // Implementation differs depending on whether the NodeValue was
   // malloc'ed or not and whether or not it's in the already-been-seen
@@ -1098,10 +1091,10 @@ expr::NodeValue* NodeBuilder<nchild_thresh>::constructNV() {
 // CONST VERSION OF NODE EXTRACTOR
 template <unsigned nchild_thresh>
 expr::NodeValue* NodeBuilder<nchild_thresh>::constructNV() const {
-  Assert(!isUsed(), "NodeBuilder is one-shot only; "
-         "attempt to access it after conversion");
-  Assert(getKind() != kind::UNDEFINED_KIND,
-         "Can't make an expression of an undefined kind!");
+  Assert(!isUsed()) << "NodeBuilder is one-shot only; "
+                       "attempt to access it after conversion";
+  Assert(getKind() != kind::UNDEFINED_KIND)
+      << "Can't make an expression of an undefined kind!";
 
   // NOTE: The comments in this function refer to the cases in the
   // file comments at the top of this file.
@@ -1113,12 +1106,12 @@ expr::NodeValue* NodeBuilder<nchild_thresh>::constructNV() const {
      * and we don't keep VARIABLE-kinded Nodes in the NodeManager
      * pool. */
 
-    Assert( ! nvIsAllocated(),
-            "internal NodeBuilder error: "
-            "VARIABLE-kinded NodeBuilder is heap-allocated !?" );
-    Assert( d_inlineNv.d_nchildren == 0,
-            "improperly-formed VARIABLE-kinded NodeBuilder: "
-            "no children permitted" );
+    Assert(!nvIsAllocated())
+        << "internal NodeBuilder error: "
+           "VARIABLE-kinded NodeBuilder is heap-allocated !?";
+    Assert(d_inlineNv.d_nchildren == 0)
+        << "improperly-formed VARIABLE-kinded NodeBuilder: "
+           "no children permitted";
 
     // we have to copy the inline NodeValue out
     expr::NodeValue* nv = (expr::NodeValue*)
@@ -1138,29 +1131,27 @@ expr::NodeValue* NodeBuilder<nchild_thresh>::constructNV() const {
   }
 
   // check that there are the right # of children for this kind
-  Assert(getMetaKind() != kind::metakind::CONSTANT,
-         "Cannot make Nodes with NodeBuilder that have CONSTANT-kinded kinds");
-  Assert(getNumChildren() >= kind::metakind::getLowerBoundForKind(getKind()),
-         "Nodes with kind %s must have at least %u children (the one under "
-         "construction has %u)",
-         kind::kindToString(getKind()).c_str(),
-         kind::metakind::getLowerBoundForKind(getKind()),
-         getNumChildren());
-  Assert(getNumChildren() <= kind::metakind::getUpperBoundForKind(getKind()),
-         "Nodes with kind %s must have at most %u children (the one under "
-         "construction has %u)",
-         kind::kindToString(getKind()).c_str(),
-         kind::metakind::getUpperBoundForKind(getKind()),
-         getNumChildren());
+  Assert(getMetaKind() != kind::metakind::CONSTANT)
+      << "Cannot make Nodes with NodeBuilder that have CONSTANT-kinded kinds";
+  Assert(getNumChildren() >= kind::metakind::getLowerBoundForKind(getKind()))
+      << "Nodes with kind " << getKind() << " must have at least "
+      << kind::metakind::getLowerBoundForKind(getKind())
+      << " children (the one under "
+         "construction has "
+      << getNumChildren() << ")";
+  Assert(getNumChildren() <= kind::metakind::getUpperBoundForKind(getKind()))
+      << "Nodes with kind " << getKind() << " must have at most "
+      << kind::metakind::getUpperBoundForKind(getKind())
+      << " children (the one under "
+         "construction has "
+      << getNumChildren() << ")";
 
 #if 0
   // if the kind is PARAMETERIZED, check that the operator is correctly-kinded
   Assert(kind::metaKindOf(getKind()) != kind::metakind::PARAMETERIZED ||
-         NodeManager::operatorToKind(getOperator()) == getKind(),
-         "Attempted to construct a parameterized kind `%s' with "
-         "incorrectly-kinded operator `%s'",
-         kind::kindToString(getKind()).c_str(),
-         kind::kindToString(getOperator().getKind()).c_str());
+         NodeManager::operatorToKind(getOperator()) == getKind()) << 
+         "Attempted to construct a parameterized kind `"<< getKind() <<"' with "
+         "incorrectly-kinded operator `"<< getOperator().getKind() <<"'";
 #endif /* 0 */
 
   // Implementation differs depending on whether the NodeValue was
@@ -1298,10 +1289,12 @@ void NodeBuilder<nchild_thresh>::internalCopy(const NodeBuilder<N>& nb) {
 
   Assert(nb.d_nvMaxChildren <= d_nvMaxChildren);
   Assert(nb.d_nv->nv_end() >= nb.d_nv->nv_begin());
-  Assert((size_t)(nb.d_nv->nv_end() - nb.d_nv->nv_begin()) <= d_nvMaxChildren, "realloced:%s, d_nvMax:%u, size:%u, nc:%u", realloced ? "true" : "false", d_nvMaxChildren, nb.d_nv->nv_end() - nb.d_nv->nv_begin(), nb.d_nv->getNumChildren());
-  std::copy(nb.d_nv->nv_begin(),
-            nb.d_nv->nv_end(),
-            d_nv->nv_begin());
+  Assert((size_t)(nb.d_nv->nv_end() - nb.d_nv->nv_begin()) <= d_nvMaxChildren)
+      << "realloced:" << (realloced ? "true" : "false")
+      << ", d_nvMax:" << d_nvMaxChildren
+      << ", size:" << nb.d_nv->nv_end() - nb.d_nv->nv_begin()
+      << ", nc:" << nb.d_nv->getNumChildren();
+  std::copy(nb.d_nv->nv_begin(), nb.d_nv->nv_end(), d_nv->nv_begin());
 
   d_nv->d_nchildren = nb.d_nv->d_nchildren;
 
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 66d597a36..d66225961 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -21,7 +21,7 @@
 #include <stack>
 #include <utility>
 
-#include "base/cvc4_assert.h"
+#include "base/check.h"
 #include "base/listener.h"
 #include "expr/attribute.h"
 #include "expr/node_manager_attributes.h"
@@ -29,8 +29,8 @@
 #include "expr/type_checker.h"
 #include "options/options.h"
 #include "options/smt_options.h"
-#include "util/statistics_registry.h"
 #include "util/resource_manager.h"
+#include "util/statistics_registry.h"
 
 using namespace std;
 using namespace CVC4::expr;
@@ -195,7 +195,7 @@ NodeManager::~NodeManager() {
   }
   d_ownedDatatypes.clear();
 
-  Assert(!d_attrManager->inGarbageCollection() );
+  Assert(!d_attrManager->inGarbageCollection());
 
   std::vector<NodeValue*> order = TopologicalSort(d_maxedOut);
   d_maxedOut.clear();
@@ -253,7 +253,7 @@ unsigned NodeManager::registerDatatype(Datatype* dt) {
 }
 
 const Datatype & NodeManager::getDatatypeForIndex( unsigned index ) const{
-  Assert( index<d_ownedDatatypes.size() );
+  Assert(index < d_ownedDatatypes.size());
   return *d_ownedDatatypes[index];
 }
 
@@ -264,7 +264,8 @@ void NodeManager::reclaimZombies() {
   Debug("gc") << "reclaiming " << d_zombies.size() << " zombie(s)!\n";
 
   // during reclamation, reclaimZombies() is never supposed to be called
-  Assert(! d_inReclaimZombies, "NodeManager::reclaimZombies() not re-entrant!");
+  Assert(!d_inReclaimZombies)
+      << "NodeManager::reclaimZombies() not re-entrant!";
 
   // whether exit is normal or exceptional, the Reclaim dtor is called
   // and ensures that d_inReclaimZombies is set back to false.
@@ -446,7 +447,7 @@ TypeNode NodeManager::getType(TNode n, bool check)
       }
 
       if( readyToCompute ) {
-        Assert( check || m.getMetaKind()!=kind::metakind::NULLARY_OPERATOR );
+        Assert(check || m.getMetaKind() != kind::metakind::NULLARY_OPERATOR);
         /* All the children have types, time to compute */
         typeNode = TypeChecker::computeType(this, m, check);
         worklist.pop();
@@ -454,18 +455,18 @@ TypeNode NodeManager::getType(TNode n, bool check)
     } // end while
 
     /* Last type computed in loop should be the type of n */
-    Assert( typeNode == getAttribute(n, TypeAttr()) );
+    Assert(typeNode == getAttribute(n, TypeAttr()));
   } else if( !hasType || needsCheck ) {
     /* We can compute the type top-down, without worrying about
        deep recursion. */
-    Assert( check || n.getMetaKind()!=kind::metakind::NULLARY_OPERATOR );
+    Assert(check || n.getMetaKind() != kind::metakind::NULLARY_OPERATOR);
     typeNode = TypeChecker::computeType(this, n, check);
   }
 
   /* The type should be have been computed and stored. */
-  Assert( hasAttribute(n, TypeAttr()) );
+  Assert(hasAttribute(n, TypeAttr()));
   /* The check should have happened, if we asked for it. */
-  Assert( !check || getAttribute(n, TypeCheckedAttr()) );
+  Assert(!check || getAttribute(n, TypeCheckedAttr()));
 
   Debug("getType") << "type of " << &n << " " <<  n << " is " << typeNode << endl;
   return typeNode;
@@ -628,16 +629,17 @@ TypeNode NodeManager::mkSort(const std::string& name, uint32_t flags) {
 TypeNode NodeManager::mkSort(TypeNode constructor,
                                     const std::vector<TypeNode>& children,
                                     uint32_t flags) {
-  Assert(constructor.getKind() == kind::SORT_TYPE &&
-         constructor.getNumChildren() == 0,
-         "expected a sort constructor");
-  Assert(children.size() > 0, "expected non-zero # of children");
-  Assert( hasAttribute(constructor.d_nv, expr::SortArityAttr()) &&
-          hasAttribute(constructor.d_nv, expr::VarNameAttr()),
-          "expected a sort constructor" );
+  Assert(constructor.getKind() == kind::SORT_TYPE
+         && constructor.getNumChildren() == 0)
+      << "expected a sort constructor";
+  Assert(children.size() > 0) << "expected non-zero # of children";
+  Assert(hasAttribute(constructor.d_nv, expr::SortArityAttr())
+         && hasAttribute(constructor.d_nv, expr::VarNameAttr()))
+      << "expected a sort constructor";
   std::string name = getAttribute(constructor.d_nv, expr::VarNameAttr());
-  Assert(getAttribute(constructor.d_nv, expr::SortArityAttr()) == children.size(),
-         "arity mismatch in application of sort constructor");
+  Assert(getAttribute(constructor.d_nv, expr::SortArityAttr())
+         == children.size())
+      << "arity mismatch in application of sort constructor";
   NodeBuilder<> nb(this, kind::SORT_TYPE);
   Node sortTag = Node(constructor.d_nv->d_children[0]);
   nb << sortTag;
@@ -706,7 +708,7 @@ Node* NodeManager::mkBoundVarPtr(const std::string& name,
 }
 
 Node NodeManager::getBoundVarListForFunctionType( TypeNode tn ) {
-  Assert( tn.isFunction() );
+  Assert(tn.isFunction());
   Node bvl = tn.getAttribute(LambdaBoundVarListAttr());
   if( bvl.isNull() ){
     std::vector< Node > vars;
@@ -777,7 +779,7 @@ Node NodeManager::mkNullaryOperator(const TypeNode& type, Kind k) {
     setAttribute(n, TypeAttr(), type);
     //setAttribute(n, TypeCheckedAttr(), true);
     d_unique_vars[k][type] = n;
-    Assert( n.getMetaKind() == kind::metakind::NULLARY_OPERATOR );
+    Assert(n.getMetaKind() == kind::metakind::NULLARY_OPERATOR);
     return n;
   }else{
     return it->second;
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 510e6d585..a3fd50d8c 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -32,6 +32,7 @@
 #include <string>
 #include <unordered_set>
 
+#include "base/check.h"
 #include "expr/kind.h"
 #include "expr/metakind.h"
 #include "expr/node_value.h"
@@ -411,14 +412,16 @@ public:
 
   /** Subscribe to NodeManager events */
   void subscribeEvents(NodeManagerListener* listener) {
-    Assert(std::find(d_listeners.begin(), d_listeners.end(), listener) == d_listeners.end(), "listener already subscribed");
+    Assert(std::find(d_listeners.begin(), d_listeners.end(), listener)
+           == d_listeners.end())
+        << "listener already subscribed";
     d_listeners.push_back(listener);
   }
 
   /** Unsubscribe from NodeManager events */
   void unsubscribeEvents(NodeManagerListener* listener) {
     std::vector<NodeManagerListener*>::iterator elt = std::find(d_listeners.begin(), d_listeners.end(), listener);
-    Assert(elt != d_listeners.end(), "listener not subscribed");
+    Assert(elt != d_listeners.end()) << "listener not subscribed";
     d_listeners.erase(elt);
   }
   
@@ -1177,14 +1180,14 @@ inline expr::NodeValue* NodeManager::poolLookup(expr::NodeValue* nv) const {
 }
 
 inline void NodeManager::poolInsert(expr::NodeValue* nv) {
-  Assert(d_nodeValuePool.find(nv) == d_nodeValuePool.end(),
-         "NodeValue already in the pool!");
+  Assert(d_nodeValuePool.find(nv) == d_nodeValuePool.end())
+      << "NodeValue already in the pool!";
   d_nodeValuePool.insert(nv);// FIXME multithreading
 }
 
 inline void NodeManager::poolRemove(expr::NodeValue* nv) {
-  Assert(d_nodeValuePool.find(nv) != d_nodeValuePool.end(),
-         "NodeValue is not in the pool!");
+  Assert(d_nodeValuePool.find(nv) != d_nodeValuePool.end())
+      << "NodeValue is not in the pool!";
 
   d_nodeValuePool.erase(nv);// FIXME multithreading
 }
@@ -1240,8 +1243,7 @@ inline bool NodeManager::hasOperator(Kind k) {
   case kind::metakind::CONSTANT:
     return false;
 
-  default:
-    Unhandled(mk);
+  default: Unhandled() << mk;
   }
 }
 
diff --git a/src/expr/node_self_iterator.h b/src/expr/node_self_iterator.h
index 7e0478acc..79df7691c 100644
--- a/src/expr/node_self_iterator.h
+++ b/src/expr/node_self_iterator.h
@@ -21,7 +21,7 @@
 
 #include <iterator>
 
-#include "base/cvc4_assert.h"
+#include "base/check.h"
 #include "expr/node.h"
 
 namespace CVC4 {
@@ -53,12 +53,12 @@ public:
 };/* class NodeSelfIterator */
 
 inline NodeSelfIterator NodeSelfIterator::self(TNode n) {
-  Assert(!n.isNull(), "Self-iteration over null nodes not permitted.");
+  Assert(!n.isNull()) << "Self-iteration over null nodes not permitted.";
   return NodeSelfIterator(n);
 }
 
 inline NodeSelfIterator NodeSelfIterator::selfEnd(TNode n) {
-  Assert(!n.isNull(), "Self-iteration over null nodes not permitted.");
+  Assert(!n.isNull()) << "Self-iteration over null nodes not permitted.";
   return NodeSelfIterator(n.end());
 }
 
@@ -70,13 +70,13 @@ inline NodeSelfIterator::NodeSelfIterator() :
 inline NodeSelfIterator::NodeSelfIterator(Node node) :
   d_node(node),
   d_child() {
-  Assert(!node.isNull(), "Self-iteration over null nodes not permitted.");
+  Assert(!node.isNull()) << "Self-iteration over null nodes not permitted.";
 }
 
 inline NodeSelfIterator::NodeSelfIterator(TNode node) :
   d_node(node),
   d_child() {
-  Assert(!node.isNull(), "Self-iteration over null nodes not permitted.");
+  Assert(!node.isNull()) << "Self-iteration over null nodes not permitted.";
 }
 
 inline NodeSelfIterator::NodeSelfIterator(const NodeSelfIterator& i) :
diff --git a/src/expr/node_value.h b/src/expr/node_value.h
index 9d1a4f98e..2c52c46be 100644
--- a/src/expr/node_value.h
+++ b/src/expr/node_value.h
@@ -421,18 +421,18 @@ inline void NodeValue::decrRefCounts() {
 }
 
 inline void NodeValue::inc() {
-  Assert(!isBeingDeleted(),
-         "NodeValue is currently being deleted "
-         "and increment is being called on it. Don't Do That!");
+  Assert(!isBeingDeleted())
+      << "NodeValue is currently being deleted "
+         "and increment is being called on it. Don't Do That!";
   // FIXME multithreading
   if (__builtin_expect((d_rc < MAX_RC - 1), true)) {
     ++d_rc;
   } else if (__builtin_expect((d_rc == MAX_RC - 1), false)) {
     ++d_rc;
-    Assert(NodeManager::currentNM() != NULL,
-           "No current NodeManager on incrementing of NodeValue: "
+    Assert(NodeManager::currentNM() != NULL)
+        << "No current NodeManager on incrementing of NodeValue: "
            "maybe a public CVC4 interface function is missing a "
-           "NodeManagerScope ?");
+           "NodeManagerScope ?";
     NodeManager::currentNM()->markRefCountMaxedOut(this);
   }
 }
@@ -442,10 +442,10 @@ inline void NodeValue::dec() {
   if(__builtin_expect( ( d_rc < MAX_RC ), true )) {
     --d_rc;
     if(__builtin_expect( ( d_rc == 0 ), false )) {
-      Assert(NodeManager::currentNM() != NULL,
-             "No current NodeManager on destruction of NodeValue: "
+      Assert(NodeManager::currentNM() != NULL)
+          << "No current NodeManager on destruction of NodeValue: "
              "maybe a public CVC4 interface function is missing a "
-             "NodeManagerScope ?");
+             "NodeManagerScope ?";
       NodeManager::currentNM()->markForDeletion(this);
     }
   }
diff --git a/src/expr/record.cpp b/src/expr/record.cpp
index 0303ff705..074205d04 100644
--- a/src/expr/record.cpp
+++ b/src/expr/record.cpp
@@ -16,7 +16,7 @@
 
 #include "expr/record.h"
 
-#include "base/cvc4_assert.h"
+#include "base/check.h"
 #include "base/output.h"
 #include "expr/expr.h"
 #include "expr/type.h"
diff --git a/src/expr/type_checker_template.cpp b/src/expr/type_checker_template.cpp
index 9ca5f00cc..375fbd515 100644
--- a/src/expr/type_checker_template.cpp
+++ b/src/expr/type_checker_template.cpp
@@ -48,7 +48,7 @@ ${typerules}
 
   default:
     Debug("getType") << "FAILURE" << std::endl;
-    Unhandled(n.getKind());
+    Unhandled() << n.getKind();
   }
 
   nodeManager->setAttribute(n, TypeAttr(), typeNode);
@@ -61,14 +61,16 @@ ${typerules}
 
 bool TypeChecker::computeIsConst(NodeManager* nodeManager, TNode n)
 {
-  Assert(n.getMetaKind() == kind::metakind::OPERATOR || n.getMetaKind() == kind::metakind::PARAMETERIZED || n.getMetaKind() == kind::metakind::NULLARY_OPERATOR);
+  Assert(n.getMetaKind() == kind::metakind::OPERATOR
+         || n.getMetaKind() == kind::metakind::PARAMETERIZED
+         || n.getMetaKind() == kind::metakind::NULLARY_OPERATOR);
 
   switch(n.getKind()) {
 ${construles}
 
-#line 70 "${template}"
+#line 72 "${template}"
 
-  default:;
+    default:;
   }
 
   return false;
@@ -77,14 +79,16 @@ ${construles}
 
 bool TypeChecker::neverIsConst(NodeManager* nodeManager, TNode n)
 {
-  Assert(n.getMetaKind() == kind::metakind::OPERATOR || n.getMetaKind() == kind::metakind::PARAMETERIZED || n.getMetaKind() == kind::metakind::NULLARY_OPERATOR);
+  Assert(n.getMetaKind() == kind::metakind::OPERATOR
+         || n.getMetaKind() == kind::metakind::PARAMETERIZED
+         || n.getMetaKind() == kind::metakind::NULLARY_OPERATOR);
 
   switch(n.getKind()) {
 ${neverconstrules}
 
-#line 86 "${template}"
+#line 90 "${template}"
 
-  default:;
+    default:;
   }
 
   return true;
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index 9db29f115..b3c8592ed 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -377,14 +377,14 @@ bool TypeNode::isRecord() const {
 size_t TypeNode::getTupleLength() const {
   Assert(isTuple());
   const Datatype& dt = getDatatype();
-  Assert(dt.getNumConstructors()==1);
+  Assert(dt.getNumConstructors() == 1);
   return dt[0].getNumArgs();
 }
 
 vector<TypeNode> TypeNode::getTupleTypes() const {
   Assert(isTuple());
   const Datatype& dt = getDatatype();
-  Assert(dt.getNumConstructors()==1);
+  Assert(dt.getNumConstructors() == 1);
   vector<TypeNode> types;
   for(unsigned i = 0; i < dt[0].getNumArgs(); ++i) {
     types.push_back(TypeNode::fromType(dt[0][i].getRangeType()));
@@ -444,9 +444,9 @@ TypeNode TypeNode::mostCommonTypeNode(TypeNode t0, TypeNode t1){
 }
 
 TypeNode TypeNode::commonTypeNode(TypeNode t0, TypeNode t1, bool isLeast) {
-  Assert( NodeManager::currentNM() != NULL,
-          "There is no current CVC4::NodeManager associated to this thread.\n"
-          "Perhaps a public-facing function is missing a NodeManagerScope ?" );
+  Assert(NodeManager::currentNM() != NULL)
+      << "There is no current CVC4::NodeManager associated to this thread.\n"
+         "Perhaps a public-facing function is missing a NodeManagerScope ?";
 
   Assert(!t0.isNull());
   Assert(!t1.isNull());
@@ -506,15 +506,17 @@ TypeNode TypeNode::commonTypeNode(TypeNode t0, TypeNode t1, bool isLeast) {
     }
   }
   case kind::SEXPR_TYPE:
-    Unimplemented("haven't implemented leastCommonType for symbolic expressions yet");
+    Unimplemented()
+        << "haven't implemented leastCommonType for symbolic expressions yet";
   default:
-    Unimplemented("don't have a commonType for types `%s' and `%s'", t0.toString().c_str(), t1.toString().c_str());
+    Unimplemented() << "don't have a commonType for types `" << t0 << "' and `"
+                    << t1 << "'";
   }
 }
 
 Node TypeNode::getEnsureTypeCondition( Node n, TypeNode tn ) {
   TypeNode ntn = n.getType();
-  Assert( ntn.isComparableTo( tn ) );
+  Assert(ntn.isComparableTo(tn));
   if( !ntn.isSubtypeOf( tn ) ){
     if( tn.isInteger() ){
       if( tn.isSubtypeOf( ntn ) ){
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index c5e1f400c..1fcd64fc7 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -29,7 +29,7 @@
 #include <unordered_map>
 #include <vector>
 
-#include "base/cvc4_assert.h"
+#include "base/check.h"
 #include "expr/kind.h"
 #include "expr/metakind.h"
 #include "util/cardinality.h"
@@ -752,8 +752,8 @@ TypeNode TypeNode::substitute(Iterator1 typesBegin,
   }
 
   // otherwise compute
-  Assert( typesEnd - typesBegin == replacementsEnd - replacementsBegin,
-          "Substitution iterator ranges must be equal size" );
+  Assert(typesEnd - typesBegin == replacementsEnd - replacementsBegin)
+      << "Substitution iterator ranges must be equal size";
   Iterator1 j = find(typesBegin, typesEnd, *this);
   if(j != typesEnd) {
     TypeNode tn = *(replacementsBegin + (j - typesBegin));
@@ -792,18 +792,18 @@ inline const T& TypeNode::getConst() const {
 
 inline TypeNode::TypeNode(const expr::NodeValue* ev) :
   d_nv(const_cast<expr::NodeValue*> (ev)) {
-  Assert(d_nv != NULL, "Expecting a non-NULL expression value!");
+  Assert(d_nv != NULL) << "Expecting a non-NULL expression value!";
   d_nv->inc();
 }
 
 inline TypeNode::TypeNode(const TypeNode& typeNode) {
-  Assert(typeNode.d_nv != NULL, "Expecting a non-NULL expression value!");
+  Assert(typeNode.d_nv != NULL) << "Expecting a non-NULL expression value!";
   d_nv = typeNode.d_nv;
   d_nv->inc();
 }
 
 inline TypeNode::~TypeNode() {
-  Assert(d_nv != NULL, "Expecting a non-NULL expression value!");
+  Assert(d_nv != NULL) << "Expecting a non-NULL expression value!";
   d_nv->dec();
 }
 
@@ -813,9 +813,9 @@ inline void TypeNode::assignNodeValue(expr::NodeValue* ev) {
 }
 
 inline TypeNode& TypeNode::operator=(const TypeNode& typeNode) {
-  Assert(d_nv != NULL, "Expecting a non-NULL expression value!");
-  Assert(typeNode.d_nv != NULL,
-         "Expecting a non-NULL expression value on RHS!");
+  Assert(d_nv != NULL) << "Expecting a non-NULL expression value!";
+  Assert(typeNode.d_nv != NULL)
+      << "Expecting a non-NULL expression value on RHS!";
   if(__builtin_expect( ( d_nv != typeNode.d_nv ), true )) {
     d_nv->dec();
     d_nv = typeNode.d_nv;
@@ -827,35 +827,35 @@ inline TypeNode& TypeNode::operator=(const TypeNode& typeNode) {
 template <class AttrKind>
 inline typename AttrKind::value_type TypeNode::
 getAttribute(const AttrKind&) const {
-  Assert( NodeManager::currentNM() != NULL,
-          "There is no current CVC4::NodeManager associated to this thread.\n"
-          "Perhaps a public-facing function is missing a NodeManagerScope ?" );
+  Assert(NodeManager::currentNM() != NULL)
+      << "There is no current CVC4::NodeManager associated to this thread.\n"
+         "Perhaps a public-facing function is missing a NodeManagerScope ?";
   return NodeManager::currentNM()->getAttribute(d_nv, AttrKind());
 }
 
 template <class AttrKind>
 inline bool TypeNode::
 hasAttribute(const AttrKind&) const {
-  Assert( NodeManager::currentNM() != NULL,
-          "There is no current CVC4::NodeManager associated to this thread.\n"
-          "Perhaps a public-facing function is missing a NodeManagerScope ?" );
+  Assert(NodeManager::currentNM() != NULL)
+      << "There is no current CVC4::NodeManager associated to this thread.\n"
+         "Perhaps a public-facing function is missing a NodeManagerScope ?";
   return NodeManager::currentNM()->hasAttribute(d_nv, AttrKind());
 }
 
 template <class AttrKind>
 inline bool TypeNode::getAttribute(const AttrKind&, typename AttrKind::value_type& ret) const {
-  Assert( NodeManager::currentNM() != NULL,
-          "There is no current CVC4::NodeManager associated to this thread.\n"
-          "Perhaps a public-facing function is missing a NodeManagerScope ?" );
+  Assert(NodeManager::currentNM() != NULL)
+      << "There is no current CVC4::NodeManager associated to this thread.\n"
+         "Perhaps a public-facing function is missing a NodeManagerScope ?";
   return NodeManager::currentNM()->getAttribute(d_nv, AttrKind(), ret);
 }
 
 template <class AttrKind>
 inline void TypeNode::
 setAttribute(const AttrKind&, const typename AttrKind::value_type& value) {
-  Assert( NodeManager::currentNM() != NULL,
-          "There is no current CVC4::NodeManager associated to this thread.\n"
-          "Perhaps a public-facing function is missing a NodeManagerScope ?" );
+  Assert(NodeManager::currentNM() != NULL)
+      << "There is no current CVC4::NodeManager associated to this thread.\n"
+         "Perhaps a public-facing function is missing a NodeManagerScope ?";
   NodeManager::currentNM()->setAttribute(d_nv, AttrKind(), value);
 }
 
@@ -1022,7 +1022,7 @@ inline const Datatype& TypeNode::getDatatype() const {
     DatatypeIndexConstant dic = getConst<DatatypeIndexConstant>();
     return NodeManager::currentNM()->getDatatypeForIndex( dic.getIndex() );
   }else{
-    Assert( getKind() == kind::PARAMETRIC_DATATYPE );
+    Assert(getKind() == kind::PARAMETRIC_DATATYPE);
     return (*this)[0].getDatatype();
   }
 }
@@ -1035,8 +1035,8 @@ inline unsigned TypeNode::getFloatingPointExponentSize() const {
 
 /** Get the significand size of this floating-point type */
 inline unsigned TypeNode::getFloatingPointSignificandSize() const {
- Assert(isFloatingPoint());
- return getConst<FloatingPointSize>().significand();
+  Assert(isFloatingPoint());
+  return getConst<FloatingPointSize>().significand();
 }
 
 /** Get the size of this bit-vector type */
diff --git a/src/expr/type_properties_template.h b/src/expr/type_properties_template.h
index 88447a125..6f1297f16 100644
--- a/src/expr/type_properties_template.h
+++ b/src/expr/type_properties_template.h
@@ -23,15 +23,15 @@
 
 #include <sstream>
 
-#include "base/cvc4_assert.h"
-#include "options/language.h"
-#include "expr/type_node.h"
-#include "expr/kind.h"
+#include "base/check.h"
 #include "expr/expr.h"
+#include "expr/kind.h"
+#include "expr/type_node.h"
+#include "options/language.h"
 
 ${type_properties_includes}
 
-#line 35 "${template}"
+#line 36 "${template}"
 
 namespace CVC4 {
 namespace kind {
@@ -42,17 +42,15 @@ namespace kind {
  * "kinds" files, so includes contributions from each theory regarding
  * that theory's types.
  */
-inline Cardinality getCardinality(TypeConstant tc) {
-  switch(tc) {
+inline Cardinality getCardinality(TypeConstant tc)
+{
+  switch (tc)
+  {
 ${type_constant_cardinalities}
-#line 49 "${template}"
-  default: {
-    std::stringstream ss;
-    ss << "No cardinality known for type constant " << tc;
-    InternalError(ss.str());
-  }
+#line 51 "${template}"
+    default: InternalError() << "No cardinality known for type constant " << tc;
   }
-}/* getCardinality(TypeConstant) */
+} /* getCardinality(TypeConstant) */
 
 /**
  * Return the cardinality of the type represented by the TypeNode
@@ -66,26 +64,21 @@ inline Cardinality getCardinality(TypeNode typeNode) {
   case TYPE_CONSTANT:
     return getCardinality(typeNode.getConst<TypeConstant>());
 ${type_cardinalities}
-#line 70 "${template}"
-  default: {
-    std::stringstream ss;
-    ss << "A theory kinds file did not provide a cardinality "
-       << "or cardinality computer for type:\n" << typeNode
-       << "\nof kind " << k;
-    InternalError(ss.str());
-  }
+#line 68 "${template}"
+  default:
+    InternalError() << "A theory kinds file did not provide a cardinality "
+                    << "or cardinality computer for type:\n"
+                    << typeNode << "\nof kind " << k;
   }
 }/* getCardinality(TypeNode) */
 
 inline bool isWellFounded(TypeConstant tc) {
   switch(tc) {
 ${type_constant_wellfoundednesses}
-#line 84 "${template}"
-  default: {
-    std::stringstream ss;
-    ss << "No well-foundedness status known for type constant: " << tc;
-    InternalError(ss.str());
-  }
+#line 79 "${template}"
+default:
+  InternalError() << "No well-foundedness status known for type constant: "
+                  << tc;
   }
 }/* isWellFounded(TypeConstant) */
 
@@ -95,45 +88,40 @@ inline bool isWellFounded(TypeNode typeNode) {
   case TYPE_CONSTANT:
     return isWellFounded(typeNode.getConst<TypeConstant>());
 ${type_wellfoundednesses}
-#line 99 "${template}"
-  default: {
-    std::stringstream ss;
-    ss << "A theory kinds file did not provide a well-foundedness "
-       << "or well-foundedness computer for type:\n" << typeNode
-       << "\nof kind " << k;
-    InternalError(ss.str());
-  }
+#line 92 "${template}"
+  default:
+    InternalError() << "A theory kinds file did not provide a well-foundedness "
+                    << "or well-foundedness computer for type:\n"
+                    << typeNode << "\nof kind " << k;
   }
 }/* isWellFounded(TypeNode) */
 
-inline Node mkGroundTerm(TypeConstant tc) {
-  switch(tc) {
+inline Node mkGroundTerm(TypeConstant tc)
+{
+  switch (tc)
+  {
 ${type_constant_groundterms}
-#line 113 "${template}"
-  default: {
-    std::stringstream ss;
-    ss << "No ground term known for type constant: " << tc;
-    InternalError(ss.str());
+#line 105 "${template}"
+    default:
+      InternalError() << "No ground term known for type constant: " << tc;
   }
-  }
-}/* mkGroundTerm(TypeConstant) */
+} /* mkGroundTerm(TypeConstant) */
 
-inline Node mkGroundTerm(TypeNode typeNode) {
+inline Node mkGroundTerm(TypeNode typeNode)
+{
   AssertArgument(!typeNode.isNull(), typeNode);
-  switch(Kind k = typeNode.getKind()) {
-  case TYPE_CONSTANT:
-    return mkGroundTerm(typeNode.getConst<TypeConstant>());
+  switch (Kind k = typeNode.getKind())
+  {
+    case TYPE_CONSTANT:
+      return mkGroundTerm(typeNode.getConst<TypeConstant>());
 ${type_groundterms}
-#line 128 "${template}"
-  default: {
-    std::stringstream ss;
-    ss << "A theory kinds file did not provide a ground term "
-       << "or ground term computer for type:\n" << typeNode
-       << "\nof kind " << k;
-    InternalError(ss.str());
-  }
+#line 119 "${template}"
+    default:
+      InternalError() << "A theory kinds file did not provide a ground term "
+                      << "or ground term computer for type:\n"
+                      << typeNode << "\nof kind " << k;
   }
-}/* mkGroundTerm(TypeNode) */
+} /* mkGroundTerm(TypeNode) */
 
 }/* CVC4::kind namespace */
 }/* CVC4 namespace */
diff --git a/src/expr/uninterpreted_constant.cpp b/src/expr/uninterpreted_constant.cpp
index 64180c377..574580259 100644
--- a/src/expr/uninterpreted_constant.cpp
+++ b/src/expr/uninterpreted_constant.cpp
@@ -21,7 +21,7 @@
 #include <sstream>
 #include <string>
 
-#include "base/cvc4_assert.h"
+#include "base/check.h"
 
 using namespace std;