Format

4 files changed, 20 insertions, 16 deletions

diff --git a/src/proof/lfsc/lfsc_printer.cpp b/src/proof/lfsc/lfsc_printer.cpp
index 5667ee520..69cc79399 100644
--- a/src/proof/lfsc/lfsc_printer.cpp
+++ b/src/proof/lfsc/lfsc_printer.cpp
@@ -584,7 +584,7 @@ bool LfscPrinter::computeProofArgs(const ProofNode* pn,
       // should be robust to different orderings
       pf << h << h << h << cs[0] << cs[1];
     }
-      break;
+    break;
     // strings
     case PfRule::STRING_LENGTH_POS: pf << as[0]; break;
     case PfRule::STRING_LENGTH_NON_EMPTY: pf << h << cs[0]; break;
diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp
index 3566cb3b4..fe7071bcb 100644
--- a/src/smt/proof_post_processor.cpp
+++ b/src/smt/proof_post_processor.cpp
@@ -998,16 +998,19 @@ Node ProofPostprocessCallback::expandMacros(PfRule id,
       Node retCurr = args[0];
       std::vector<Node> transEq;
       // try to reconstruct the (extended) rewrite
-      // first, use the standard rewriter followed by the extended equality rewriter
-      for (size_t i=0; i<2; i++)
+      // first, use the standard rewriter followed by the extended equality
+      // rewriter
+      for (size_t i = 0; i < 2; i++)
       {
-        if (i==1 && retCurr.getKind()!=EQUAL)
+        if (i == 1 && retCurr.getKind() != EQUAL)
         {
           break;
         }
-        MethodId midi = i==0 ? MethodId::RW_REWRITE : MethodId::RW_REWRITE_EQ_EXT;
-        Node retDef = builtin::BuiltinProofRuleChecker::applyRewrite(retCurr, midi);
-        if (retDef!=retCurr)
+        MethodId midi =
+            i == 0 ? MethodId::RW_REWRITE : MethodId::RW_REWRITE_EQ_EXT;
+        Node retDef =
+            builtin::BuiltinProofRuleChecker::applyRewrite(retCurr, midi);
+        if (retDef != retCurr)
         {
           // will expand this as a default rewrite if needed
           Node eqd = retCurr.eqNode(retDef);
@@ -1016,15 +1019,16 @@ Node ProofPostprocessCallback::expandMacros(PfRule id,
           transEq.push_back(eqd);
         }
         retCurr = retDef;
-        if (retCurr==ret)
+        if (retCurr == ret)
         {
           // already successful
           break;
         }
       }
-      if (retCurr!=ret)
+      if (retCurr != ret)
       {
-        // try to prove the rewritten form is equal to the extended rewritten form
+        // try to prove the rewritten form is equal to the extended rewritten
+        // form
         Node eqp = retCurr.eqNode(ret);
         std::vector<Node> targs;
         targs.push_back(eqp);
@@ -1041,7 +1045,7 @@ Node ProofPostprocessCallback::expandMacros(PfRule id,
           return Node::null();
         }
       }
-      if (transEq.size()>1)
+      if (transEq.size() > 1)
       {
         // put together with transitivity
         cdp->addStep(eq, PfRule::TRANS, transEq, {});
diff --git a/src/theory/builtin/proof_checker.cpp b/src/theory/builtin/proof_checker.cpp
index 1be7b44c6..e0a56830a 100644
--- a/src/theory/builtin/proof_checker.cpp
+++ b/src/theory/builtin/proof_checker.cpp
@@ -21,10 +21,10 @@
 #include "rewriter/rewrite_proof_rule.h"
 #include "smt/term_formula_removal.h"
 #include "theory/evaluator.h"
+#include "theory/quantifiers/extended_rewrite.h"
 #include "theory/rewriter.h"
 #include "theory/substitutions.h"
 #include "theory/theory.h"
-#include "theory/quantifiers/extended_rewrite.h"
 
 using namespace cvc5::kind;
 
diff --git a/src/theory/builtin/proof_checker.h b/src/theory/builtin/proof_checker.h
index 0386978e6..86fbf1c58 100644
--- a/src/theory/builtin/proof_checker.h
+++ b/src/theory/builtin/proof_checker.h
@@ -100,10 +100,10 @@ class BuiltinProofRuleChecker : public ProofRuleChecker
    * @return The substituted, rewritten form of n.
    */
   static Node applySubstitutionRewrite(Node n,
-                                const std::vector<Node>& exp,
-                                MethodId ids = MethodId::SB_DEFAULT,
-                                MethodId ida = MethodId::SBA_SEQUENTIAL,
-                                MethodId idr = MethodId::RW_REWRITE);
+                                       const std::vector<Node>& exp,
+                                       MethodId ids = MethodId::SB_DEFAULT,
+                                       MethodId ida = MethodId::SBA_SEQUENTIAL,
+                                       MethodId idr = MethodId::RW_REWRITE);
 
   /** get a TheoryId from a node, return false if we fail */
   static bool getTheoryId(TNode n, TheoryId& tid);