5 files changed, 16 insertions, 12 deletions
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 0b7c569b7..b11ee77a7 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -434,7 +434,7 @@ void CvcPrinter::toStream(
       }
       break;
     case kind::APPLY_TESTER: {
-      Assert( !n.getType().isTuple() && !n.getType().isRecord() );
+      Assert(!n.getType().isTuple() && !n.getType().isRecord());
       op << "is_";
       unsigned cindex = Datatype::indexOf(n.getOperator().toExpr());
       const Datatype& dt = Datatype::datatypeOf(n.getOperator().toExpr());
diff --git a/src/printer/dagification_visitor.cpp b/src/printer/dagification_visitor.cpp
index 67c5aa7e5..5463b1c22 100644
--- a/src/printer/dagification_visitor.cpp
+++ b/src/printer/dagification_visitor.cpp
@@ -132,7 +132,7 @@ void DagificationVisitor::visit(TNode current, TNode parent) {
 }
 
 void DagificationVisitor::start(TNode node) {
-  AlwaysAssert(!d_done, "DagificationVisitor cannot be re-used");
+  AlwaysAssert(!d_done) << "DagificationVisitor cannot be re-used";
   d_top = node;
 }
 
@@ -175,18 +175,22 @@ void DagificationVisitor::done(TNode node) {
 
     // apply previous substitutions to the rhs, enabling cascading LETs
     Node n = d_substitutions->apply(*i);
-    Assert(! d_substitutions->hasSubstitution(n));
+    Assert(!d_substitutions->hasSubstitution(n));
     d_substitutions->addSubstitution(n, letvar);
   }
 }
 
 const theory::SubstitutionMap& DagificationVisitor::getLets() {
-  AlwaysAssert(d_done, "DagificationVisitor must be used as a visitor before getting the dagified version out!");
+  AlwaysAssert(d_done)
+      << "DagificationVisitor must be used as a visitor before "
+         "getting the dagified version out!";
   return *d_substitutions;
 }
 
 Node DagificationVisitor::getDagifiedBody() {
-  AlwaysAssert(d_done, "DagificationVisitor must be used as a visitor before getting the dagified version out!");
+  AlwaysAssert(d_done)
+      << "DagificationVisitor must be used as a visitor before "
+         "getting the dagified version out!";
 
 #ifdef CVC4_TRACING
 #  ifdef CVC4_DEBUG
diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp
index cacdd6694..28471de72 100644
--- a/src/printer/printer.cpp
+++ b/src/printer/printer.cpp
@@ -77,8 +77,7 @@ unique_ptr<Printer> Printer::makePrinter(OutputLanguage lang)
     return unique_ptr<Printer>(
         new printer::cvc::CvcPrinter(/* cvc3-mode = */ true));
 
-  default:
-    Unhandled(lang);
+  default: Unhandled() << lang;
   }
 }
 
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 013288880..0d3bab3d0 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -195,7 +195,8 @@ void Smt2Printer::toStream(std::ostream& out,
       case roundTowardNegative : out << "roundTowardNegative"; break;
       case roundTowardZero : out << "roundTowardZero"; break;
       default :
-        Unreachable("Invalid value of rounding mode constant (%d)",n.getConst<RoundingMode>());
+        Unreachable() << "Invalid value of rounding mode constant ("
+                      << n.getConst<RoundingMode>() << ")";
       }
       break;
     case kind::CONST_BOOLEAN:
@@ -982,7 +983,7 @@ void Smt2Printer::toStream(std::ostream& out,
       force_child_type[1] = NodeManager::currentNM()->mkSetType( elemType );
     }else{
       // APPLY_UF, APPLY_CONSTRUCTOR, etc.
-      Assert( n.hasOperator() );
+      Assert(n.hasOperator());
       TypeNode opt = n.getOperator().getType();
       if (n.getKind() == kind::APPLY_CONSTRUCTOR)
       {
@@ -996,7 +997,7 @@ void Smt2Printer::toStream(std::ostream& out,
           opt = TypeNode::fromType(dt[ci].getSpecializedConstructorType(tn));
         }
       }
-      Assert( opt.getNumChildren() == n.getNumChildren() + 1 );
+      Assert(opt.getNumChildren() == n.getNumChildren() + 1);
       for(size_t i = 0; i < n.getNumChildren(); ++i ) {
         force_child_type[i] = opt[i];
       }
@@ -1350,7 +1351,7 @@ void Smt2Printer::toStream(std::ostream& out, const UnsatCore& core) const
 {
   out << "(" << std::endl;
   SmtEngine * smt = core.getSmtEngine();
-  Assert( smt!=NULL );
+  Assert(smt != NULL);
   for(UnsatCore::const_iterator i = core.begin(); i != core.end(); ++i) {
     std::string name;
     if (smt->getExpressionName(*i,name)) {
diff --git a/src/printer/tptp/tptp_printer.cpp b/src/printer/tptp/tptp_printer.cpp
index 3ed642805..72fdfe41d 100644
--- a/src/printer/tptp/tptp_printer.cpp
+++ b/src/printer/tptp/tptp_printer.cpp
@@ -73,7 +73,7 @@ void TptpPrinter::toStream(std::ostream& out, const UnsatCore& core) const
 {
   out << "% SZS output start UnsatCore " << std::endl;
   SmtEngine * smt = core.getSmtEngine();
-  Assert( smt!=NULL );
+  Assert(smt != NULL);
   for(UnsatCore::const_iterator i = core.begin(); i != core.end(); ++i) {
     std::string name;
     if (smt->getExpressionName(*i, name)) {