1 files changed, 28 insertions, 23 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_- _ _ _ _ _ ";