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

18 files changed, 213 insertions, 174 deletions

diff --git a/src/proof/arith_proof.cpp b/src/proof/arith_proof.cpp
index 8b55c29db..77f4b1630 100644
--- a/src/proof/arith_proof.cpp
+++ b/src/proof/arith_proof.cpp
@@ -236,7 +236,8 @@ Node ProofArith::toStreamRecLFSC(std::ostream& out,
       out << ss.str();
       out << ") (pred_eq_f _ " << ProofManager::getLitName(n2[0]) << ")) t_t_neq_f))" << std::endl;
     } else {
-      Assert((n1[0] == n2[0][0] && n1[1] == n2[0][1]) || (n1[1] == n2[0][0] && n1[0] == n2[0][1]));
+      Assert((n1[0] == n2[0][0] && n1[1] == n2[0][1])
+             || (n1[1] == n2[0][0] && n1[0] == n2[0][1]));
       if(n1[1] == n2[0][0]) {
         out << "(symm _ _ _ " << ss.str() << ")";
       } else {
@@ -256,12 +257,17 @@ Node ProofArith::toStreamRecLFSC(std::ostream& out,
          pf2->d_id == theory::eq::MERGED_THROUGH_CONGRUENCE;
          pf2 = pf2->d_children[0].get()) {
       Assert(!pf2->d_node.isNull());
-      Assert(pf2->d_node.getKind() == kind::PARTIAL_APPLY_UF || pf2->d_node.getKind() == kind::BUILTIN || pf2->d_node.getKind() == kind::APPLY_UF || pf2->d_node.getKind() == kind::SELECT || pf2->d_node.getKind() == kind::STORE);
+      Assert(pf2->d_node.getKind() == kind::PARTIAL_APPLY_UF
+             || pf2->d_node.getKind() == kind::BUILTIN
+             || pf2->d_node.getKind() == kind::APPLY_UF
+             || pf2->d_node.getKind() == kind::SELECT
+             || pf2->d_node.getKind() == kind::STORE);
       Assert(pf2->d_children.size() == 2);
       out << "(cong _ _ _ _ _ _ ";
       stk.push(pf2);
     }
-    Assert(stk.top()->d_children[0]->d_id != theory::eq::MERGED_THROUGH_CONGRUENCE);
+    Assert(stk.top()->d_children[0]->d_id
+           != theory::eq::MERGED_THROUGH_CONGRUENCE);
     NodeBuilder<> b1(kind::PARTIAL_APPLY_UF), b2(kind::PARTIAL_APPLY_UF);
     const theory::eq::EqProof* pf2 = stk.top();
     stk.pop();
@@ -322,7 +328,12 @@ Node ProofArith::toStreamRecLFSC(std::ostream& out,
       b2 << n2[1-side];
       out << ss.str();
     } else {
-      Assert(pf2->d_node[b1.getNumChildren() - (pf2->d_node.getMetaKind() == kind::metakind::PARAMETERIZED ? 0 : 1)] == n2[1-side]);
+      Assert(pf2->d_node[b1.getNumChildren()
+                         - (pf2->d_node.getMetaKind()
+                                    == kind::metakind::PARAMETERIZED
+                                ? 0
+                                : 1)]
+             == n2[1 - side]);
       b1 << n2[1-side];
       b2 << n2[side];
       out << "(symm _ _ _ " << ss.str() << ")";
@@ -349,7 +360,7 @@ Node ProofArith::toStreamRecLFSC(std::ostream& out,
         b2 << n2[1-side];
         out << ss.str();
       } else {
-        Assert(pf2->d_node[b1.getNumChildren()] == n2[1-side]);
+        Assert(pf2->d_node[b1.getNumChildren()] == n2[1 - side]);
         b1 << n2[1-side];
         b2 << n2[side];
         out << "(symm _ _ _ " << ss.str() << ")";
@@ -677,7 +688,7 @@ void LFSCArithProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLetM
 
   // !d_realMode <--> term.getType().isInteger()
 
-  Assert (theory::Theory::theoryOf(term) == theory::THEORY_ARITH);
+  Assert(theory::Theory::theoryOf(term) == theory::THEORY_ARITH);
   switch (term.getKind())
   {
     case kind::CONST_RATIONAL:
@@ -899,9 +910,8 @@ void LFSCArithProof::printLinearPolynomialNormalizer(std::ostream& o,
     }
     default:
 #ifdef CVC4_ASSERTIONS
-      std::ostringstream msg;
-      msg << "Invalid operation " << n.getKind() << " in linear polynomial";
-      Unreachable(msg.str().c_str());
+      Unreachable() << "Invalid operation " << n.getKind()
+                    << " in linear polynomial";
 #endif  // CVC4_ASSERTIONS
       break;
   }
@@ -914,13 +924,11 @@ void LFSCArithProof::printLinearMonomialNormalizer(std::ostream& o,
   {
     case kind::MULT: {
 #ifdef CVC4_ASSERTIONS
-      std::ostringstream s;
-      s << "node " << n << " is not a linear monomial";
-      s << " " << n[0].getKind() << " " << n[1].getKind();
       Assert((n[0].getKind() == kind::CONST_RATIONAL
               && (n[1].getKind() == kind::VARIABLE
-                  || n[1].getKind() == kind::SKOLEM)),
-             s.str().c_str());
+                  || n[1].getKind() == kind::SKOLEM)))
+          << "node " << n << " is not a linear monomial"
+          << " " << n[0].getKind() << " " << n[1].getKind();
 #endif  // CVC4_ASSERTIONS
 
       o << "\n        (pn_mul_c_L _ _ _ ";
@@ -946,9 +954,8 @@ void LFSCArithProof::printLinearMonomialNormalizer(std::ostream& o,
     }
     default:
 #ifdef CVC4_ASSERTIONS
-      std::ostringstream msg;
-      msg << "Invalid operation " << n.getKind() << " in linear monomial";
-      Unreachable(msg.str().c_str());
+      Unreachable() << "Invalid operation " << n.getKind()
+                    << " in linear monomial";
 #endif  // CVC4_ASSERTIONS
       break;
   }
@@ -963,18 +970,16 @@ void LFSCArithProof::printConstRational(std::ostream& o, const Node& n)
 
 void LFSCArithProof::printVariableNormalizer(std::ostream& o, const Node& n)
 {
-  std::ostringstream msg;
-  msg << "Invalid variable kind " << n.getKind() << " in linear monomial";
-  Assert(n.getKind() == kind::VARIABLE || n.getKind() == kind::SKOLEM,
-         msg.str().c_str());
+  Assert(n.getKind() == kind::VARIABLE || n.getKind() == kind::SKOLEM)
+      << "Invalid variable kind " << n.getKind() << " in linear monomial";
   o << "(pn_var " << n << ")";
 }
 
 void LFSCArithProof::printLinearPolynomialPredicateNormalizer(std::ostream& o,
                                                               const Node& n)
 {
-  Assert(n.getKind() == kind::GEQ,
-         "can only print normalization witnesses for (>=) nodes");
+  Assert(n.getKind() == kind::GEQ)
+      << "can only print normalization witnesses for (>=) nodes";
   Assert(n[1].getKind() == kind::CONST_RATIONAL);
   o << "(poly_formula_norm_>= _ _ _ ";
   o << "\n    (pn_- _ _ _ _ _ ";
diff --git a/src/proof/array_proof.cpp b/src/proof/array_proof.cpp
index 131fcd3b6..ec2f85829 100644
--- a/src/proof/array_proof.cpp
+++ b/src/proof/array_proof.cpp
@@ -152,7 +152,8 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
         out << ss.str();
         out << ") (pred_eq_f _ " << ProofManager::getLitName(n2[0]) << ")) t_t_neq_f))" << std::endl;
       } else {
-        Assert((n1[0] == n2[0][0] && n1[1] == n2[0][1]) || (n1[1] == n2[0][0] && n1[0] == n2[0][1]));
+        Assert((n1[0] == n2[0][0] && n1[1] == n2[0][1])
+               || (n1[1] == n2[0][0] && n1[0] == n2[0][1]));
         if(n1[1] == n2[0][0]) {
           out << "(symm _ _ _ " << ss.str() << ")";
         } else {
@@ -166,7 +167,8 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
     } else {
       Node n2 = pf.d_node;
       Assert(n2.getKind() == kind::EQUAL);
-      Assert((n1[0] == n2[0] && n1[1] == n2[1]) || (n1[1] == n2[0] && n1[0] == n2[1]));
+      Assert((n1[0] == n2[0] && n1[1] == n2[1])
+             || (n1[1] == n2[0] && n1[0] == n2[1]));
 
       out << ss.str();
       out << " ";
@@ -323,10 +325,15 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
       b2 << n2[1-side];
       out << ss.str();
     } else {
-      Assert(pf2->d_node[b1.getNumChildren() +
-                         (n1[side].getKind() == kind::PARTIAL_SELECT_0 ? 1 : 0) +
-                         (n1[side].getKind() == kind::PARTIAL_SELECT_1 ? 1 : 0) -
-                         (pf2->d_node.getMetaKind() == kind::metakind::PARAMETERIZED ? 0 : 1)] == n2[1-side]);
+      Assert(
+          pf2->d_node[b1.getNumChildren()
+                      + (n1[side].getKind() == kind::PARTIAL_SELECT_0 ? 1 : 0)
+                      + (n1[side].getKind() == kind::PARTIAL_SELECT_1 ? 1 : 0)
+                      - (pf2->d_node.getMetaKind()
+                                 == kind::metakind::PARAMETERIZED
+                             ? 0
+                             : 1)]
+          == n2[1 - side]);
       b1 << n2[1-side];
       b2 << n2[side];
       out << "(symm _ _ _ " << ss.str() << ")";
@@ -359,7 +366,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
         b2 << n2[1-side];
         out << ss.str();
       } else {
-        Assert(pf2->d_node[b1.getNumChildren()] == n2[1-side]);
+        Assert(pf2->d_node[b1.getNumChildren()] == n2[1 - side]);
         b1 << n2[1-side];
         b2 << n2[side];
         out << "(symm _ _ _ " << ss.str() << ")";
@@ -383,7 +390,8 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
     Debug("mgd") << "n1.getNumChildren() + 1 = "
                  << n1.getNumChildren() + 1 << std::endl;
 
-    Assert(!((n1.getKind() == kind::PARTIAL_SELECT_0 && n1.getNumChildren() == 2)));
+    Assert(!(
+        (n1.getKind() == kind::PARTIAL_SELECT_0 && n1.getNumChildren() == 2)));
     if (n1.getKind() == kind::PARTIAL_SELECT_1 && n1.getNumChildren() == 2) {
       Debug("mgd") << "Finished a SELECT. Updating.." << std::endl;
       b1.clear(kind::SELECT);
@@ -410,7 +418,8 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
     Debug("mgd") << "n2.getNumChildren() + 1 = "
                  << n2.getNumChildren() + 1 << std::endl;
 
-    Assert(!((n2.getKind() == kind::PARTIAL_SELECT_0 && n2.getNumChildren() == 2)));
+    Assert(!(
+        (n2.getKind() == kind::PARTIAL_SELECT_0 && n2.getNumChildren() == 2)));
     if (n2.getKind() == kind::PARTIAL_SELECT_1 && n2.getNumChildren() == 2) {
       Debug("mgd") << "Finished a SELECT. Updating.." << std::endl;
       b2.clear(kind::SELECT);
@@ -1115,7 +1124,7 @@ std::string ArrayProof::skolemToLiteral(Expr skolem) {
 }
 
 void LFSCArrayProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map) {
-  Assert (theory::Theory::theoryOf(term) == theory::THEORY_ARRAYS);
+  Assert(theory::Theory::theoryOf(term) == theory::THEORY_ARRAYS);
 
   if (theory::Theory::theoryOf(term) != theory::THEORY_ARRAYS) {
     // We can get here, for instance, if there's a (select ite ...), e.g. a non-array term
@@ -1129,7 +1138,10 @@ void LFSCArrayProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLetM
     return;
   }
 
-  Assert ((term.getKind() == kind::SELECT) || (term.getKind() == kind::PARTIAL_SELECT_0) || (term.getKind() == kind::PARTIAL_SELECT_1) || (term.getKind() == kind::STORE));
+  Assert((term.getKind() == kind::SELECT)
+         || (term.getKind() == kind::PARTIAL_SELECT_0)
+         || (term.getKind() == kind::PARTIAL_SELECT_1)
+         || (term.getKind() == kind::STORE));
 
   switch (term.getKind()) {
   case kind::SELECT: {
@@ -1196,7 +1208,7 @@ void LFSCArrayProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLetM
 
 void LFSCArrayProof::printOwnedSort(Type type, std::ostream& os) {
   Debug("pf::array") << std::endl << "(pf::array) LFSCArrayProof::printOwnedSort: type is: " << type << std::endl;
-  Assert (type.isArray() || type.isSort());
+  Assert(type.isArray() || type.isSort());
   if (type.isArray()){
     ArrayType array_type(type);
 
diff --git a/src/proof/bitvector_proof.cpp b/src/proof/bitvector_proof.cpp
index 18e46a292..98f57e25f 100644
--- a/src/proof/bitvector_proof.cpp
+++ b/src/proof/bitvector_proof.cpp
@@ -224,16 +224,16 @@ void BitVectorProof::printOwnedTerm(Expr term,
 void BitVectorProof::printEmptyClauseProof(std::ostream& os,
                                            std::ostream& paren)
 {
-  Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER,
-         "the BV theory should only be proving bottom directly in the eager "
-         "bitblasting mode");
+  Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER)
+      << "the BV theory should only be proving bottom directly in the eager "
+         "bitblasting mode";
 }
 
 void BitVectorProof::printBitOf(Expr term,
                                 std::ostream& os,
                                 const ProofLetMap& map)
 {
-  Assert (term.getKind() == kind::BITVECTOR_BITOF);
+  Assert(term.getKind() == kind::BITVECTOR_BITOF);
   unsigned bit = term.getOperator().getConst<BitVectorBitOf>().bitIndex;
   Expr var = term[0];
 
@@ -247,7 +247,7 @@ void BitVectorProof::printBitOf(Expr term,
 
 void BitVectorProof::printConstant(Expr term, std::ostream& os)
 {
-  Assert (term.isConst());
+  Assert(term.isConst());
   os << "(a_bv " << utils::getSize(term) << " ";
 
   if (d_useConstantLetification) {
@@ -336,7 +336,7 @@ void BitVectorProof::printOperatorParametric(Expr term,
     os << high <<" " << low << " " << utils::getSize(term[0]);
   }
   os <<" ";
-  Assert (term.getNumChildren() == 1);
+  Assert(term.getNumChildren() == 1);
   d_proofEngine->printBoundTerm(term[0], os, map);
   os <<")";
 }
@@ -346,7 +346,7 @@ void BitVectorProof::printOwnedSort(Type type, std::ostream& os)
   Debug("pf::bv") << std::endl
                   << "(pf::bv) BitVectorProof::printOwnedSort( " << type << " )"
                   << std::endl;
-  Assert (type.isBitVector());
+  Assert(type.isBitVector());
   unsigned width = utils::getSize(type);
   os << "(BitVec " << width << ")";
 }
@@ -433,7 +433,7 @@ void BitVectorProof::printTermBitblasting(Expr term, std::ostream& os)
 {
   // TODO: once we have the operator elimination rules remove those that we
   // eliminated
-  Assert (term.getType().isBitVector());
+  Assert(term.getType().isBitVector());
   Kind kind = term.getKind();
 
   if (theory::Theory::isLeafOf(term, theory::THEORY_BV) && !term.isConst())
@@ -568,7 +568,7 @@ void BitVectorProof::printTermBitblasting(Expr term, std::ostream& os)
     return;
   }
 
-  default: Unreachable("BitVectorProof Unknown operator");
+  default: Unreachable() << "BitVectorProof Unknown operator";
   }
 }
 
@@ -601,7 +601,7 @@ void BitVectorProof::printAtomBitblasting(Expr atom,
 
     return;
   }
-  default: Unreachable("BitVectorProof Unknown atom kind");
+  default: Unreachable() << "BitVectorProof Unknown atom kind";
   }
 }
 
@@ -739,9 +739,9 @@ bool BitVectorProof::hasAlias(Expr expr)
 void BitVectorProof::printConstantDisequalityProof(
     std::ostream& os, Expr c1, Expr c2, const ProofLetMap& globalLetMap)
 {
-  Assert (c1.isConst());
-  Assert (c2.isConst());
-  Assert (utils::getSize(c1) == utils::getSize(c2));
+  Assert(c1.isConst());
+  Assert(c2.isConst());
+  Assert(utils::getSize(c1) == utils::getSize(c2));
 
   os << "(bv_disequal_constants " << utils::getSize(c1) << " ";
 
diff --git a/src/proof/clausal_bitvector_proof.cpp b/src/proof/clausal_bitvector_proof.cpp
index 4e700a832..bb9213b4b 100644
--- a/src/proof/clausal_bitvector_proof.cpp
+++ b/src/proof/clausal_bitvector_proof.cpp
@@ -175,13 +175,13 @@ void ClausalBitVectorProof::optimizeDratProof()
                                                    optFormulaFilename,
                                                    optDratFilename,
                                                    drat2er::options::QUIET);
-      AlwaysAssert(
-          dratTrimExitCode == 0, "drat-trim exited with %d", dratTrimExitCode);
+      AlwaysAssert(dratTrimExitCode == 0)
+          << "drat-trim exited with " << dratTrimExitCode;
     }
 #else
-    Unimplemented(
-        "Proof production when using CryptoMiniSat requires drat2er.\n"
-        "Run contrib/get-drat2er, reconfigure with --drat2er, and rebuild");
+    Unimplemented()
+        << "Proof production when using CryptoMiniSat requires drat2er.\n"
+        << "Run contrib/get-drat2er, reconfigure with --drat2er, and rebuild";
 #endif
 
     {
@@ -314,9 +314,9 @@ void LfscClausalBitVectorProof::printTheoryLemmaProof(std::vector<Expr>& lemma,
                                                       std::ostream& paren,
                                                       const ProofLetMap& map)
 {
-  Unreachable(
-      "Clausal bit-vector proofs should only be used in combination with eager "
-      "bitblasting, which **does not use theory lemmas**");
+  Unreachable() << "Clausal bit-vector proofs should only be used in "
+                   "combination with eager "
+                   "bitblasting, which **does not use theory lemmas**";
 }
 
 void LfscClausalBitVectorProof::printBBDeclarationAndCnf(std::ostream& os,
@@ -339,9 +339,9 @@ void LfscClausalBitVectorProof::printBBDeclarationAndCnf(std::ostream& os,
 void LfscDratBitVectorProof::printEmptyClauseProof(std::ostream& os,
                                                    std::ostream& paren)
 {
-  Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER,
-         "the BV theory should only be proving bottom directly in the eager "
-         "bitblasting mode");
+  Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER)
+      << "the BV theory should only be proving bottom directly in the eager "
+         "bitblasting mode";
 
   os << "\n;; Proof of input to SAT solver\n";
   os << "(@ proofOfSatInput ";
@@ -366,9 +366,9 @@ void LfscDratBitVectorProof::printEmptyClauseProof(std::ostream& os,
 void LfscLratBitVectorProof::printEmptyClauseProof(std::ostream& os,
                                                    std::ostream& paren)
 {
-  Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER,
-         "the BV theory should only be proving bottom directly in the eager "
-         "bitblasting mode");
+  Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER)
+      << "the BV theory should only be proving bottom directly in the eager "
+         "bitblasting mode";
 
   os << "\n;; Proof of input to SAT solver\n";
   os << "(@ proofOfCMap ";
@@ -396,9 +396,9 @@ void LfscLratBitVectorProof::printEmptyClauseProof(std::ostream& os,
 void LfscErBitVectorProof::printEmptyClauseProof(std::ostream& os,
                                                  std::ostream& paren)
 {
-  Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER,
-         "the BV theory should only be proving bottom directly in the eager "
-         "bitblasting mode");
+  Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER)
+      << "the BV theory should only be proving bottom directly in the eager "
+         "bitblasting mode";
 
   d_dratTranslationStatistics.d_totalTime.start();
   er::ErProof pf =
diff --git a/src/proof/cnf_proof.cpp b/src/proof/cnf_proof.cpp
index 9c263e08f..c8284762c 100644
--- a/src/proof/cnf_proof.cpp
+++ b/src/proof/cnf_proof.cpp
@@ -57,7 +57,7 @@ bool CnfProof::isDefinition(Node node) {
 }
 
 ProofRule CnfProof::getProofRule(Node node) {
-  Assert (isAssertion(node));
+  Assert(isAssertion(node));
   NodeToProofRule::iterator it = d_assertionToProofRule.find(node);
   return (*it).second;
 }
@@ -69,27 +69,26 @@ ProofRule CnfProof::getProofRule(ClauseId clause) {
 
 Node CnfProof::getAssertionForClause(ClauseId clause) {
   ClauseIdToNode::const_iterator it = d_clauseToAssertion.find(clause);
-  Assert (it != d_clauseToAssertion.end());
+  Assert(it != d_clauseToAssertion.end());
   return (*it).second;
 }
 
 Node CnfProof::getDefinitionForClause(ClauseId clause) {
   ClauseIdToNode::const_iterator it = d_clauseToDefinition.find(clause);
-  Assert (it != d_clauseToDefinition.end());
+  Assert(it != d_clauseToDefinition.end());
   return (*it).second;
 }
 
 void CnfProof::registerConvertedClause(ClauseId clause, bool explanation) {
-  Assert (clause != ClauseIdUndef &&
-          clause != ClauseIdError &&
-          clause != ClauseIdEmpty);
+  Assert(clause != ClauseIdUndef && clause != ClauseIdError
+         && clause != ClauseIdEmpty);
 
   // Explanations do not need a CNF conversion proof since they are in CNF
   // (they will only need a theory proof as they are theory valid)
   if (explanation) {
     Debug("proof:cnf") << "CnfProof::registerConvertedClause "
                        << clause << " explanation? " << explanation << std::endl;
-    Assert (d_explanations.find(clause) == d_explanations.end());
+    Assert(d_explanations.find(clause) == d_explanations.end());
     d_explanations.insert(clause);
     return;
   }
@@ -180,7 +179,7 @@ void CnfProof::setCnfDependence(Node from, Node to) {
                      << "from " << from  << std::endl
                      << "     to " << to << std::endl;
 
-  Assert (from != to);
+  Assert(from != to);
   d_cnfDeps.insert(std::make_pair(from, to));
 }
 
@@ -196,7 +195,7 @@ void CnfProof::pushCurrentAssertion(Node assertion) {
 }
 
 void CnfProof::popCurrentAssertion() {
-  Assert (d_currentAssertionStack.size());
+  Assert(d_currentAssertionStack.size());
 
   Debug("proof:cnf") << "CnfProof::popCurrentAssertion "
                      << d_currentAssertionStack.back() << std::endl;
@@ -209,7 +208,7 @@ void CnfProof::popCurrentAssertion() {
 }
 
 Node CnfProof::getCurrentAssertion() {
-  Assert (d_currentAssertionStack.size());
+  Assert(d_currentAssertionStack.size());
   return d_currentAssertionStack.back();
 }
 
@@ -227,7 +226,7 @@ void CnfProof::pushCurrentDefinition(Node definition) {
 }
 
 void CnfProof::popCurrentDefinition() {
-  Assert (d_currentDefinitionStack.size());
+  Assert(d_currentDefinitionStack.size());
 
   Debug("proof:cnf") << "CnfProof::popCurrentDefinition "
                      << d_currentDefinitionStack.back() << std::endl;
@@ -236,7 +235,7 @@ void CnfProof::popCurrentDefinition() {
 }
 
 Node CnfProof::getCurrentDefinition() {
-  Assert (d_currentDefinitionStack.size());
+  Assert(d_currentDefinitionStack.size());
   return d_currentDefinitionStack.back();
 }
 
@@ -295,7 +294,7 @@ void CnfProof::collectAtomsAndRewritesForLemmas(const IdToSatClause& lemmaClause
       Node node = getAtom(lit.getSatVariable());
       Expr atom = node.toExpr();
       if (atom.isConst()) {
-        Assert (atom == utils::mkTrue());
+        Assert(atom == utils::mkTrue());
         continue;
       }
       clause_expr_nodes.insert(lit.isNegated() ? node.notNode() : node);
@@ -462,7 +461,7 @@ void LFSCCnfProof::printCnfProofForClause(ClauseId id,
 
   // return;
 
-  Assert( clause->size()>0 );
+  Assert(clause->size() > 0);
 
   // If the clause contains x v ~x, it's easy!
   //
@@ -639,10 +638,10 @@ void LFSCCnfProof::printCnfProofForClause(ClauseId id,
 
     Node iatom;
     if (is_in_clause) {
-      Assert( assertion.getNumChildren()==2 );
+      Assert(assertion.getNumChildren() == 2);
       iatom = assertion[ base_index==0 ? 1 : 0];
     } else {
-      Assert( assertion.getNumChildren()==1 );
+      Assert(assertion.getNumChildren() == 1);
       iatom = assertion[0];
     }
 
@@ -753,7 +752,7 @@ void LFSCCnfProof::printCnfProofForClause(ClauseId id,
         Trace("cnf-pf-debug") << "CALLING getlitname" << std::endl;
         os_base_n << ProofManager::getLitName(lit1, d_name) << " ";
       }
-      Assert( elimNum!=0 );
+      Assert(elimNum != 0);
       os_base_n << "(" << ( k==kind::EQUAL ? "iff" : "xor" ) << "_elim_" << elimNum << " _ _ ";
       if( !base_pol ){
         os_base_n << "(not_" << ( base_assertion.getKind()==kind::EQUAL ? "iff" : "xor" ) << "_elim _ _ " << os_base.str() << ")";
diff --git a/src/proof/dimacs.cpp b/src/proof/dimacs.cpp
index cced98660..fd5b79383 100644
--- a/src/proof/dimacs.cpp
+++ b/src/proof/dimacs.cpp
@@ -16,7 +16,7 @@
 
 #include "proof/dimacs.h"
 
-#include "base/cvc4_assert.h"
+#include "base/check.h"
 
 #include <iostream>
 
diff --git a/src/proof/drat/drat_proof.cpp b/src/proof/drat/drat_proof.cpp
index 5a01ffdfd..162efc3e5 100644
--- a/src/proof/drat/drat_proof.cpp
+++ b/src/proof/drat/drat_proof.cpp
@@ -158,7 +158,9 @@ void DratInstruction::outputAsText(std::ostream& os) const
       os << '0' << std::endl;
       break;
     }
-    default: { Unreachable("Unknown DRAT instruction kind");
+    default:
+    {
+      Unreachable() << "Unknown DRAT instruction kind";
     }
   }
 }
@@ -267,7 +269,9 @@ void DratProof::outputAsLfsc(std::ostream& os, uint8_t indentation) const
         os << "DRATProofd ";
         break;
       }
-      default: { Unreachable("Unrecognized DRAT instruction kind");
+      default:
+      {
+        Unreachable() << "Unrecognized DRAT instruction kind";
       }
     }
     for (const SatLiteral& l : i.d_clause)
diff --git a/src/proof/er/er_proof.cpp b/src/proof/er/er_proof.cpp
index 9f22e236b..19c838e2d 100644
--- a/src/proof/er/er_proof.cpp
+++ b/src/proof/er/er_proof.cpp
@@ -29,7 +29,7 @@
 #include <iterator>
 #include <unordered_set>
 
-#include "base/cvc4_assert.h"
+#include "base/check.h"
 #include "base/map_util.h"
 #include "proof/dimacs.h"
 #include "proof/lfsc_proof_printer.h"
@@ -114,9 +114,9 @@ ErProof ErProof::fromBinaryDratProof(
                                                drat2er::options::QUIET,
                                                false);
 #else
-    Unimplemented(
-        "ER proof production requires drat2er.\n"
-        "Run contrib/get-drat2er, reconfigure with --drat2er, and rebuild");
+    Unimplemented()
+        << "ER proof production requires drat2er.\n"
+        << "Run contrib/get-drat2er, reconfigure with --drat2er, and rebuild";
 #endif
   }
 
@@ -184,8 +184,8 @@ ErProof::ErProof(const std::unordered_map<ClauseId, prop::SatClause>& clauses,
     size_t nLinesForThisDef = 2 + otherLiterals.size();
     // Look at the negation of the second literal in the second clause to get
     // the old literal
-    AlwaysAssert(d_tracecheck.d_lines.size() > i + 1,
-                 "Malformed definition in TRACECHECK proof from drat2er");
+    AlwaysAssert(d_tracecheck.d_lines.size() > i + 1)
+        << "Malformed definition in TRACECHECK proof from drat2er";
     d_definitions.emplace_back(newVar,
                                ~d_tracecheck.d_lines[i + 1].d_clause[1],
                                std::move(otherLiterals));
@@ -299,8 +299,8 @@ void ErProof::outputAsLfsc(std::ostream& os) const
   }
 
   // Write proof of bottom
-  Assert(d_tracecheck.d_lines.back().d_clause.size() == 0,
-         "The TRACECHECK proof from drat2er did not prove bottom.");
+  Assert(d_tracecheck.d_lines.back().d_clause.size() == 0)
+      << "The TRACECHECK proof from drat2er did not prove bottom.";
   os << "\n      er.c" << d_tracecheck.d_lines.back().d_idx
      << " ; (holds cln)\n";
 
diff --git a/src/proof/lemma_proof.cpp b/src/proof/lemma_proof.cpp
index 6bb2c2854..f4249f3d5 100644
--- a/src/proof/lemma_proof.cpp
+++ b/src/proof/lemma_proof.cpp
@@ -147,7 +147,8 @@ bool LemmaProofRecipe::wasRewritten(Node assertion) const {
 }
 
 Node LemmaProofRecipe::getExplanation(Node assertion) const {
-  Assert(d_assertionToExplanation.find(assertion) != d_assertionToExplanation.end());
+  Assert(d_assertionToExplanation.find(assertion)
+         != d_assertionToExplanation.end());
   return d_assertionToExplanation.find(assertion)->second;
 }
 
diff --git a/src/proof/lrat/lrat_proof.cpp b/src/proof/lrat/lrat_proof.cpp
index 1685ad1c3..4a19f07be 100644
--- a/src/proof/lrat/lrat_proof.cpp
+++ b/src/proof/lrat/lrat_proof.cpp
@@ -24,7 +24,7 @@
 #include <sstream>
 #include <unordered_map>
 
-#include "base/cvc4_assert.h"
+#include "base/check.h"
 #include "base/output.h"
 #include "proof/dimacs.h"
 #include "proof/lfsc_proof_printer.h"
@@ -151,9 +151,9 @@ LratProof LratProof::fromDratProof(
     drat2er::drat_trim::CheckAndConvertToLRAT(
         formulaFilename, dratFilename, lratFilename, drat2er::options::QUIET);
 #else
-    Unimplemented(
-        "LRAT proof production requires drat2er.\n"
-        "Run contrib/get-drat2er, reconfigure with --drat2er, and rebuild");
+    Unimplemented()
+        << "LRAT proof production requires drat2er.\n"
+        << "Run contrib/get-drat2er, reconfigure with --drat2er, and rebuild";
 #endif
   }
 
@@ -221,7 +221,8 @@ LratProof::LratProof(std::istream& textualProof)
       SatLiteral lit;
       firstS >> lit;
       Trace("pf::lrat") << "First lit: " << lit << std::endl;
-      Assert(!firstS.fail(), "Couldn't parse first literal from addition line");
+      Assert(!firstS.fail())
+          << "Couldn't parse first literal from addition line";
 
       SatClause clause;
       for (; lit != 0; textualProof >> lit)
diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
index f68d5937c..fa4c1ecb5 100644
--- a/src/proof/proof_manager.cpp
+++ b/src/proof/proof_manager.cpp
@@ -17,7 +17,7 @@
 
 #include "proof/proof_manager.h"
 
-#include "base/cvc4_assert.h"
+#include "base/check.h"
 #include "context/context.h"
 #include "options/bv_options.h"
 #include "options/proof_options.h"
@@ -97,52 +97,52 @@ const Proof& ProofManager::getProof(SmtEngine* smt)
 }
 
 CoreSatProof* ProofManager::getSatProof() {
-  Assert (currentPM()->d_satProof);
+  Assert(currentPM()->d_satProof);
   return currentPM()->d_satProof;
 }
 
 CnfProof* ProofManager::getCnfProof() {
-  Assert (currentPM()->d_cnfProof);
+  Assert(currentPM()->d_cnfProof);
   return currentPM()->d_cnfProof;
 }
 
 TheoryProofEngine* ProofManager::getTheoryProofEngine() {
-  Assert (currentPM()->d_theoryProof != NULL);
+  Assert(currentPM()->d_theoryProof != NULL);
   return currentPM()->d_theoryProof;
 }
 
 UFProof* ProofManager::getUfProof() {
-  Assert (options::proof());
+  Assert(options::proof());
   TheoryProof* pf = getTheoryProofEngine()->getTheoryProof(theory::THEORY_UF);
   return (UFProof*)pf;
 }
 
 proof::ResolutionBitVectorProof* ProofManager::getBitVectorProof()
 {
-  Assert (options::proof());
+  Assert(options::proof());
   TheoryProof* pf = getTheoryProofEngine()->getTheoryProof(theory::THEORY_BV);
   return static_cast<proof::ResolutionBitVectorProof*>(pf);
 }
 
 ArrayProof* ProofManager::getArrayProof() {
-  Assert (options::proof());
+  Assert(options::proof());
   TheoryProof* pf = getTheoryProofEngine()->getTheoryProof(theory::THEORY_ARRAYS);
   return (ArrayProof*)pf;
 }
 
 ArithProof* ProofManager::getArithProof() {
-  Assert (options::proof());
+  Assert(options::proof());
   TheoryProof* pf = getTheoryProofEngine()->getTheoryProof(theory::THEORY_ARITH);
   return (ArithProof*)pf;
 }
 
 SkolemizationManager* ProofManager::getSkolemizationManager() {
-  Assert (options::proof() || options::unsatCores());
+  Assert(options::proof() || options::unsatCores());
   return &(currentPM()->d_skolemizationManager);
 }
 
 void ProofManager::initSatProof(Minisat::Solver* solver) {
-  Assert (currentPM()->d_satProof == NULL);
+  Assert(currentPM()->d_satProof == NULL);
   Assert(currentPM()->d_format == LFSC);
   currentPM()->d_satProof = new CoreSatProof(solver, d_context, "");
 }
@@ -151,8 +151,8 @@ void ProofManager::initCnfProof(prop::CnfStream* cnfStream,
                                 context::Context* ctx) {
   ProofManager* pm = currentPM();
   Assert(pm->d_satProof != NULL);
-  Assert (pm->d_cnfProof == NULL);
-  Assert (pm->d_format == LFSC);
+  Assert(pm->d_cnfProof == NULL);
+  Assert(pm->d_format == LFSC);
   CnfProof* cnf = new LFSCCnfProof(cnfStream, ctx, "");
   pm->d_cnfProof = cnf;
 
@@ -175,8 +175,8 @@ void ProofManager::initCnfProof(prop::CnfStream* cnfStream,
 }
 
 void ProofManager::initTheoryProofEngine() {
-  Assert (currentPM()->d_theoryProof == NULL);
-  Assert (currentPM()->d_format == LFSC);
+  Assert(currentPM()->d_theoryProof == NULL);
+  Assert(currentPM()->d_format == LFSC);
   currentPM()->d_theoryProof = new LFSCTheoryProofEngine();
 }
 
@@ -250,7 +250,7 @@ bool ProofManager::hasLitName(TNode lit) {
 }
 
 std::string ProofManager::sanitize(TNode node) {
-  Assert (node.isVar() || node.isConst());
+  Assert(node.isVar() || node.isConst());
 
   std::string name = node.toString();
   if (node.isVar()) {
@@ -282,7 +282,9 @@ void ProofManager::traceDeps(TNode n, ExprSet* coreAssertions) {
         Debug("cores") << " -- Could not track cause assertion. Failing silently." << std::endl;
         return;
       }
-      InternalError("Cannot trace dependence information back to input assertion:\n`%s'", n.toString().c_str());
+      InternalError()
+          << "Cannot trace dependence information back to input assertion:\n`"
+          << n << "'";
     }
     Assert(d_deps.find(n) != d_deps.end());
     std::vector<Node> deps = (*d_deps.find(n)).second;
@@ -312,7 +314,9 @@ void ProofManager::traceDeps(TNode n, CDExprSet* coreAssertions) {
         Debug("cores") << " -- Could not track cause assertion. Failing silently." << std::endl;
         return;
       }
-      InternalError("Cannot trace dependence information back to input assertion:\n`%s'", n.toString().c_str());
+      InternalError()
+          << "Cannot trace dependence information back to input assertion:\n`"
+          << n << "'";
     }
     Assert(d_deps.find(n) != d_deps.end());
     std::vector<Node> deps = (*d_deps.find(n)).second;
@@ -327,7 +331,7 @@ void ProofManager::traceDeps(TNode n, CDExprSet* coreAssertions) {
 }
 
 void ProofManager::traceUnsatCore() {
-  Assert (options::unsatCores());
+  Assert(options::unsatCores());
   d_satProof->refreshProof();
   IdToSatClause used_lemmas;
   IdToSatClause used_inputs;
@@ -375,8 +379,9 @@ void ProofManager::constructSatProof() {
 }
 
 void ProofManager::getLemmasInUnsatCore(theory::TheoryId theory, std::vector<Node> &lemmas) {
-  Assert(PROOF_ON(), "Cannot compute unsat core when proofs are off");
-  Assert(unsatCoreAvailable(), "Cannot get unsat core at this time. Mabye the input is SAT?" );
+  Assert(PROOF_ON()) << "Cannot compute unsat core when proofs are off";
+  Assert(unsatCoreAvailable())
+      << "Cannot get unsat core at this time. Mabye the input is SAT?";
 
   constructSatProof();
 
@@ -425,8 +430,9 @@ std::set<Node> ProofManager::satClauseToNodeSet(prop::SatClause* clause) {
 }
 
 Node ProofManager::getWeakestImplicantInUnsatCore(Node lemma) {
-  Assert(PROOF_ON(), "Cannot compute unsat core when proofs are off");
-  Assert(unsatCoreAvailable(), "Cannot get unsat core at this time. Mabye the input is SAT?" );
+  Assert(PROOF_ON()) << "Cannot compute unsat core when proofs are off";
+  Assert(unsatCoreAvailable())
+      << "Cannot get unsat core at this time. Mabye the input is SAT?";
 
   // If we're doing aggressive minimization, work on all lemmas, not just conjunctions.
   if (!options::aggressiveCoreMin() && (lemma.getKind() != kind::AND))
@@ -531,7 +537,7 @@ void ProofManager::addDependence(TNode n, TNode dep) {
 }
 
 void ProofManager::addUnsatCore(Expr formula) {
-  Assert (d_inputCoreFormulas.find(formula) != d_inputCoreFormulas.end());
+  Assert(d_inputCoreFormulas.find(formula) != d_inputCoreFormulas.end());
   d_outputCoreFormulas.insert(formula);
 }
 
@@ -912,7 +918,8 @@ void LFSCProof::checkUnrewrittenAssertion(const NodeSet& rewrites) const
   for (rewrite = rewrites.begin(); rewrite != rewrites.end(); ++rewrite) {
     Debug("pf::pm") << "LFSCProof::checkUnrewrittenAssertion: handling " << *rewrite << std::endl;
     if (ProofManager::currentPM()->have_input_assertion((*rewrite).toExpr())) {
-      Assert(ProofManager::currentPM()->have_input_assertion((*rewrite).toExpr()));
+      Assert(
+          ProofManager::currentPM()->have_input_assertion((*rewrite).toExpr()));
       Debug("pf::pm") << "LFSCProof::checkUnrewrittenAssertion: this assertion was NOT rewritten!" << std::endl
                       << "\tAdding filter: "
                       << ProofManager::getPreprocessedAssertionName(*rewrite, "")
@@ -947,7 +954,8 @@ Node ProofManager::mkOp(TNode n) {
 
   Node& op = d_ops[n];
   if(op.isNull()) {
-    Assert((n.getConst<Kind>() == kind::SELECT) || (n.getConst<Kind>() == kind::STORE));
+    Assert((n.getConst<Kind>() == kind::SELECT)
+           || (n.getConst<Kind>() == kind::STORE));
 
     Debug("mgd-pm-mkop") << "making an op for " << n << "\n";
 
@@ -1036,12 +1044,12 @@ std::ostream& operator<<(std::ostream& out, CVC4::ProofRule k) {
 }
 
 void ProofManager::registerRewrite(unsigned ruleId, Node original, Node result){
-  Assert (currentPM()->d_theoryProof != NULL);
+  Assert(currentPM()->d_theoryProof != NULL);
   currentPM()->d_rewriteLog.push_back(RewriteLogEntry(ruleId, original, result));
 }
 
 void ProofManager::clearRewriteLog() {
-  Assert (currentPM()->d_theoryProof != NULL);
+  Assert(currentPM()->d_theoryProof != NULL);
   currentPM()->d_rewriteLog.clear();
 }
 
diff --git a/src/proof/proof_output_channel.cpp b/src/proof/proof_output_channel.cpp
index 449e12225..aa2175e66 100644
--- a/src/proof/proof_output_channel.cpp
+++ b/src/proof/proof_output_channel.cpp
@@ -17,7 +17,7 @@
 
 #include "proof/proof_output_channel.h"
 
-#include "base/cvc4_assert.h"
+#include "base/check.h"
 #include "theory/term_registration_visitor.h"
 #include "theory/valuation.h"
 
@@ -55,8 +55,8 @@ theory::LemmaStatus ProofOutputChannel::lemma(TNode n, ProofRule rule, bool,
   // following assertion cannot be enabled due to
   // "test/regress/regress0/arrays/swap_t1_np_nf_ai_00005_007.cvc.smt".
   // Assert(
-  //     d_lemma.isNull(),
-  //     "Multiple calls to ProofOutputChannel::lemma() are not supported.");
+  //     d_lemma.isNull()) <<
+  //     "Multiple calls to ProofOutputChannel::lemma() are not supported.";
   d_lemma = n;
   return theory::LemmaStatus(TNode::null(), 0);
 }
diff --git a/src/proof/proof_utils.h b/src/proof/proof_utils.h
index cb509063d..66e20069d 100644
--- a/src/proof/proof_utils.h
+++ b/src/proof/proof_utils.h
@@ -107,7 +107,7 @@ inline unsigned getSize(Type type) {
 
 
 inline unsigned getSize(Expr node) {
-  Assert (node.getType().isBitVector());
+  Assert(node.getType().isBitVector());
   return getSize(node.getType());
 }
 
@@ -147,7 +147,7 @@ inline Expr mkConst(const BitVector& value) {
 inline Expr mkOr(const std::vector<Expr>& nodes) {
   std::set<Expr> all;
   all.insert(nodes.begin(), nodes.end());
-  Assert(all.size() != 0 );
+  Assert(all.size() != 0);
 
   if (all.size() == 1) {
     // All the same, or just one
@@ -220,8 +220,7 @@ inline Expr mkSortedExpr(Kind kind, const std::vector<Expr>& children) {
 }/* mkSortedNode() */
 
 inline const bool getBit(Expr expr, unsigned i) {
-  Assert (i < utils::getSize(expr) &&
-          expr.isConst());
+  Assert(i < utils::getSize(expr) && expr.isConst());
   Integer bit = expr.getConst<BitVector>().extract(i, i).getValue();
   return (bit == 1u);
 }
diff --git a/src/proof/resolution_bitvector_proof.cpp b/src/proof/resolution_bitvector_proof.cpp
index 505500d5e..f4ced1748 100644
--- a/src/proof/resolution_bitvector_proof.cpp
+++ b/src/proof/resolution_bitvector_proof.cpp
@@ -513,9 +513,9 @@ void LfscResolutionBitVectorProof::printBBDeclarationAndCnf(std::ostream& os,
 void LfscResolutionBitVectorProof::printEmptyClauseProof(std::ostream& os,
                                                          std::ostream& paren)
 {
-  Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER,
-         "the BV theory should only be proving bottom directly in the eager "
-         "bitblasting mode");
+  Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER)
+      << "the BV theory should only be proving bottom directly in the eager "
+         "bitblasting mode";
   proof::LFSCProofPrinter::printResolutionEmptyClause(
       d_resolutionProof.get(), os, paren);
 }
diff --git a/src/proof/skolemization_manager.cpp b/src/proof/skolemization_manager.cpp
index b0397d08c..44ca08fa6 100644
--- a/src/proof/skolemization_manager.cpp
+++ b/src/proof/skolemization_manager.cpp
@@ -37,13 +37,14 @@ bool SkolemizationManager::hasSkolem(Node disequality) {
 
 Node SkolemizationManager::getSkolem(Node disequality) {
   Debug("pf::pm") << "SkolemizationManager: getSkolem( ";
-  Assert (d_disequalityToSkolem.find(disequality) != d_disequalityToSkolem.end());
+  Assert(d_disequalityToSkolem.find(disequality)
+         != d_disequalityToSkolem.end());
   Debug("pf::pm") << disequality << " ) = " << d_disequalityToSkolem[disequality] << std::endl;
   return d_disequalityToSkolem[disequality];
 }
 
 Node SkolemizationManager::getDisequality(Node skolem) {
-  Assert (d_skolemToDisequality.find(skolem) != d_skolemToDisequality.end());
+  Assert(d_skolemToDisequality.find(skolem) != d_skolemToDisequality.end());
   return d_skolemToDisequality[skolem];
 }
 
diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp
index c66aa59e4..1f3e6abf1 100644
--- a/src/proof/theory_proof.cpp
+++ b/src/proof/theory_proof.cpp
@@ -16,7 +16,7 @@
  **/
 #include "proof/theory_proof.h"
 
-#include "base/cvc4_assert.h"
+#include "base/check.h"
 #include "context/context.h"
 #include "options/bv_options.h"
 #include "options/proof_options.h"
@@ -103,7 +103,9 @@ void TheoryProofEngine::registerTheory(theory::Theory* th) {
               bvp = new proof::LfscErBitVectorProof(thBv, this);
               break;
             }
-            default: { Unreachable("Invalid BvProofFormat");
+            default:
+            {
+              Unreachable() << "Invalid BvProofFormat";
             }
           };
           d_theoryProofTable[id] = bvp;
@@ -154,9 +156,9 @@ TheoryProof* TheoryProofEngine::getTheoryProof(theory::TheoryId id) {
   }
 
   if (d_theoryProofTable.find(id) == d_theoryProofTable.end()) {
-    std::stringstream ss;
-    ss << "Error! Proofs not yet supported for the following theory: " << id << std::endl;
-    InternalError(ss.str().c_str());
+    InternalError()
+        << "Error! Proofs not yet supported for the following theory: " << id
+        << std::endl;
   }
 
   return d_theoryProofTable[id];
@@ -221,7 +223,7 @@ theory::TheoryId TheoryProofEngine::getTheoryForLemma(const prop::SatClause* cla
     Node node = pm->getCnfProof()->getAtom(lit.getSatVariable());
     Expr atom = node.toExpr();
     if (atom.isConst()) {
-      Assert (atom == utils::mkTrue());
+      Assert(atom == utils::mkTrue());
       continue;
     }
 
@@ -229,7 +231,7 @@ theory::TheoryId TheoryProofEngine::getTheoryForLemma(const prop::SatClause* cla
   }
 
   // Ensure that the lemma is in the database.
-  Assert (pm->getCnfProof()->haveProofRecipe(nodes));
+  Assert(pm->getCnfProof()->haveProofRecipe(nodes));
   return pm->getCnfProof()->getProofRecipe(nodes).getTheory();
 }
 
@@ -257,7 +259,7 @@ void LFSCTheoryProofEngine::printLetTerm(Expr term, std::ostream& os) {
     Expr current_expr = let_order[i].expr;
     unsigned let_id = let_order[i].id;
     ProofLetMap::const_iterator it = map.find(current_expr);
-    Assert (it != map.end());
+    Assert(it != map.end());
     unsigned let_count = it->second.count;
     Assert(let_count);
     // skip terms that only appear once
@@ -387,8 +389,8 @@ void LFSCTheoryProofEngine::printLemmaRewrites(NodePairSet& rewrites,
 
     Node n1 = it->first;
     Node n2 = it->second;
-    Assert(n1.toExpr() == utils::mkFalse() ||
-           theory::Theory::theoryOf(n1) == theory::Theory::theoryOf(n2));
+    Assert(n1.toExpr() == utils::mkFalse()
+           || theory::Theory::theoryOf(n1) == theory::Theory::theoryOf(n2));
 
     std::ostringstream rewriteRule;
     rewriteRule << ".lrr" << d_assertionToRewrite.size();
@@ -462,7 +464,7 @@ void LFSCTheoryProofEngine::dumpTheoryLemmas(const IdToSatClause& lemmas) {
       prop::SatLiteral lit = (*clause)[i];
       Node node = pm->getCnfProof()->getAtom(lit.getSatVariable());
       if (node.isConst()) {
-        Assert (node.toExpr() == utils::mkTrue());
+        Assert(node.toExpr() == utils::mkTrue());
         continue;
       }
       nodes.insert(lit.isNegated() ? node.notNode() : node);
@@ -493,8 +495,8 @@ void LFSCTheoryProofEngine::finalizeBvConflicts(const IdToSatClause& lemmas, std
 
       // The literals (true) and (not false) are omitted from conflicts
       if (atom.isConst()) {
-        Assert (atom == utils::mkTrue() ||
-                (atom == utils::mkFalse() && lit.isNegated()));
+        Assert(atom == utils::mkTrue()
+               || (atom == utils::mkFalse() && lit.isNegated()));
         continue;
       }
 
@@ -584,7 +586,7 @@ void LFSCTheoryProofEngine::printTheoryLemmas(const IdToSatClause& lemmas,
   ProofManager::getBitVectorProof()->printBBDeclarationAndCnf(os, paren, map);
 
   if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
-    Assert (lemmas.size() == 1);
+    Assert(lemmas.size() == 1);
     // nothing more to do (no combination with eager so far)
     return;
   }
@@ -606,7 +608,7 @@ void LFSCTheoryProofEngine::printTheoryLemmas(const IdToSatClause& lemmas,
       Node node = pm->getCnfProof()->getAtom(lit.getSatVariable());
       Expr atom = node.toExpr();
       if (atom.isConst()) {
-        Assert (atom == utils::mkTrue());
+        Assert(atom == utils::mkTrue());
         continue;
       }
       Expr expr_lit = lit.isNegated() ? atom.notExpr(): atom;
@@ -922,7 +924,7 @@ void LFSCTheoryProofEngine::printCoreTerm(Expr term, std::ostream& os, const Pro
 
   case kind::DISTINCT:
     // Distinct nodes can have any number of chidlren.
-    Assert (term.getNumChildren() >= 2);
+    Assert(term.getNumChildren() >= 2);
 
     if (term.getNumChildren() == 2) {
       os << "(not (= ";
@@ -999,8 +1001,7 @@ void LFSCTheoryProofEngine::printCoreTerm(Expr term, std::ostream& os, const Pro
     return;
   }
 
-  default:
-    Unhandled(k);
+  default: Unhandled() << k;
   }
 
 }
@@ -1010,7 +1011,7 @@ void TheoryProof::printTheoryLemmaProof(std::vector<Expr>& lemma,
                                         std::ostream& paren,
                                         const ProofLetMap& map) {
   // Default method for replaying proofs: assert (negated) literals back to a fresh copy of the theory
-  Assert(d_theory!=NULL);
+  Assert(d_theory != NULL);
 
   context::UserContext fakeContext;
   ProofOutputChannel oc;
@@ -1032,7 +1033,8 @@ void TheoryProof::printTheoryLemmaProof(std::vector<Expr>& lemma,
     os << " (clausify_false trust)";
     return;
   } else {
-    InternalError(std::string("can't generate theory-proof for ") + ProofManager::currentPM()->getLogic());
+    InternalError() << "can't generate theory-proof for "
+                    << ProofManager::currentPM()->getLogic();
   }
 
   Debug("pf::tp") << "TheoryProof::printTheoryLemmaProof - calling th->ProduceProofs()" << std::endl;
@@ -1122,7 +1124,7 @@ BooleanProof::BooleanProof(TheoryProofEngine* proofEngine)
 {}
 
 void BooleanProof::registerTerm(Expr term) {
-  Assert (term.getType().isBoolean());
+  Assert(term.getType().isBoolean());
 
   if (term.isVariable() && d_declarations.find(term) == d_declarations.end()) {
     d_declarations.insert(term);
@@ -1149,7 +1151,7 @@ void LFSCBooleanProof::printConstantDisequalityProof(std::ostream& os, Expr c1,
 }
 
 void LFSCBooleanProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map) {
-  Assert (term.getType().isBoolean());
+  Assert(term.getType().isBoolean());
   if (term.isVariable()) {
     os << ProofManager::sanitize(term);
     return;
@@ -1224,14 +1226,13 @@ void LFSCBooleanProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLe
     os << (term.getConst<bool>() ? "true" : "false");
     return;
 
-  default:
-    Unhandled(k);
+  default: Unhandled() << k;
   }
 
 }
 
 void LFSCBooleanProof::printOwnedSort(Type type, std::ostream& os) {
-  Assert (type.isBoolean());
+  Assert(type.isBoolean());
   os << "Bool";
 }
 
@@ -1262,7 +1263,7 @@ void LFSCBooleanProof::printTheoryLemmaProof(std::vector<Expr>& lemma,
                                              std::ostream& os,
                                              std::ostream& paren,
                                              const ProofLetMap& map) {
-  Unreachable("No boolean lemmas yet!");
+  Unreachable() << "No boolean lemmas yet!";
 }
 
 bool LFSCBooleanProof::printsAsBool(const Node &n)
diff --git a/src/proof/uf_proof.cpp b/src/proof/uf_proof.cpp
index 10823693d..b88f7dc33 100644
--- a/src/proof/uf_proof.cpp
+++ b/src/proof/uf_proof.cpp
@@ -119,7 +119,8 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out,
       } else if (n2[0].getKind() == kind::BOOLEAN_TERM_VARIABLE) {
         out << ss.str() << " " << ProofManager::getLitName(n2[0]) << "))";
       } else {
-        Assert((n1[0] == n2[0][0] && n1[1] == n2[0][1]) || (n1[1] == n2[0][0] && n1[0] == n2[0][1]));
+        Assert((n1[0] == n2[0][0] && n1[1] == n2[0][1])
+               || (n1[1] == n2[0][0] && n1[0] == n2[0][1]));
         if(n1[1] == n2[0][0]) {
           out << "(symm _ _ _ " << ss.str() << ")";
         } else {
@@ -130,7 +131,8 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out,
     } else {
       Node n2 = pf.d_node;
       Assert(n2.getKind() == kind::EQUAL);
-      Assert((n1[0] == n2[0] && n1[1] == n2[1]) || (n1[1] == n2[0] && n1[0] == n2[1]));
+      Assert((n1[0] == n2[0] && n1[1] == n2[1])
+             || (n1[1] == n2[0] && n1[0] == n2[1]));
 
       out << ss.str();
       out << " ";
@@ -160,7 +162,8 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out,
       out << "(cong _ _ _ _ _ _ ";
       stk.push(pf2);
     }
-    Assert(stk.top()->d_children[0]->d_id != theory::eq::MERGED_THROUGH_CONGRUENCE);
+    Assert(stk.top()->d_children[0]->d_id
+           != theory::eq::MERGED_THROUGH_CONGRUENCE);
     NodeBuilder<> b1(kind::PARTIAL_APPLY_UF), b2(kind::PARTIAL_APPLY_UF);
     const theory::eq::EqProof* pf2 = stk.top();
     stk.pop();
@@ -231,7 +234,12 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out,
       b2 << n2[1-side];
       out << ss.str();
     } else {
-      Assert(pf2->d_node[b1.getNumChildren() - (pf2->d_node.getMetaKind() == kind::metakind::PARAMETERIZED ? 0 : 1)] == n2[1-side]);
+      Assert(pf2->d_node[b1.getNumChildren()
+                         - (pf2->d_node.getMetaKind()
+                                    == kind::metakind::PARAMETERIZED
+                                ? 0
+                                : 1)]
+             == n2[1 - side]);
       b1 << n2[1-side];
       b2 << n2[side];
       out << "(symm _ _ _ " << ss.str() << ")";
@@ -258,7 +266,7 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out,
         b2 << n2[1-side];
         out << ss.str();
       } else {
-        Assert(pf2->d_node[b1.getNumChildren()] == n2[1-side]);
+        Assert(pf2->d_node[b1.getNumChildren()] == n2[1 - side]);
         b1 << n2[1-side];
         b2 << n2[side];
         out << "(symm _ _ _ " << ss.str() << ")";
@@ -618,7 +626,7 @@ void UFProof::registerTerm(Expr term) {
 void LFSCUFProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map) {
   Debug("pf::uf") << std::endl << "(pf::uf) LFSCUfProof::printOwnedTerm: term = " << term << std::endl;
 
-  Assert (theory::Theory::theoryOf(term) == theory::THEORY_UF);
+  Assert(theory::Theory::theoryOf(term) == theory::THEORY_UF);
 
   if (term.getKind() == kind::VARIABLE ||
       term.getKind() == kind::SKOLEM ||
@@ -627,7 +635,7 @@ void LFSCUFProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap&
     return;
   }
 
-  Assert (term.getKind() == kind::APPLY_UF);
+  Assert(term.getKind() == kind::APPLY_UF);
 
   if(term.getType().isBoolean()) {
     os << "(p_app ";
@@ -653,7 +661,7 @@ void LFSCUFProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap&
 void LFSCUFProof::printOwnedSort(Type type, std::ostream& os) {
   Debug("pf::uf") << std::endl << "(pf::uf) LFSCArrayProof::printOwnedSort: type is: " << type << std::endl;
 
-  Assert (type.isSort());
+  Assert(type.isSort());
   os << type;
 }
 
@@ -705,7 +713,7 @@ void LFSCUFProof::printTermDeclarations(std::ostream& os, std::ostream& paren) {
       }
       os << fparen.str() << "))\n";
     } else {
-      Assert (term.isVariable());
+      Assert(term.isVariable());
       os << type << ")\n";
     }
     paren << ")";
diff --git a/src/proof/unsat_core.cpp b/src/proof/unsat_core.cpp
index 4212331af..0776197cb 100644
--- a/src/proof/unsat_core.cpp
+++ b/src/proof/unsat_core.cpp
@@ -16,7 +16,7 @@
 
 #include "proof/unsat_core.h"
 
-#include "base/cvc4_assert.h"
+#include "base/check.h"
 #include "expr/expr_iomanip.h"
 #include "options/base_options.h"
 #include "printer/printer.h"