Format

5 files changed, 25 insertions, 11 deletions

diff --git a/src/proof/lean/lean_post_processor.cpp b/src/proof/lean/lean_post_processor.cpp
index 960bd17f7..092a69a15 100644
--- a/src/proof/lean/lean_post_processor.cpp
+++ b/src/proof/lean/lean_post_processor.cpp
@@ -104,7 +104,9 @@ bool LeanProofPostprocessCallback::update(Node res,
                   *cdp);
       break;
     }
-    default: { return false;
+    default:
+    {
+      return false;
     }
   };
   return true;
diff --git a/src/proof/verit/verit_post_processor.cpp b/src/proof/verit/verit_post_processor.cpp
index 2bfb9fef2..bedb1ab8d 100644
--- a/src/proof/verit/verit_post_processor.cpp
+++ b/src/proof/verit/verit_post_processor.cpp
@@ -445,11 +445,17 @@ bool VeritProofPostprocessCallback::update(Node res,
               vrule = VeritRule::EQUIV_SIMPLIFY;
               break;
             }
-            case kind::LT: { [[fallthrough]];
+            case kind::LT:
+            {
+              [[fallthrough]];
             }
-            case kind::GT: { [[fallthrough]];
+            case kind::GT:
+            {
+              [[fallthrough]];
             }
-            case kind::GEQ: { [[fallthrough]];
+            case kind::GEQ:
+            {
+              [[fallthrough]];
             }
             case kind::LEQ:
             {
@@ -477,7 +483,8 @@ bool VeritProofPostprocessCallback::update(Node res,
           vrule = VeritRule::QUANTIFIER_SIMPLIFY;
           break;
         }
-        default: {
+        default:
+        {
         };
       }
       return addVeritStep(
@@ -991,7 +998,7 @@ bool VeritProofPostprocessCallback::update(Node res,
       return addVeritStep(vp2, VeritRule::NOT_NOT, {}, {}, *cdp)
              && addVeritStep(vp1, VeritRule::NOT_NOT, {}, {}, *cdp)
              && addVeritStepFromOr(
-                    res, VeritRule::RESOLUTION, {vp1, vp2}, {}, *cdp);
+                 res, VeritRule::RESOLUTION, {vp1, vp2}, {}, *cdp);
     }
     // ======== Equality resolution
     // Children: (P1:F1, P2:(= F1 F2))
@@ -1836,7 +1843,7 @@ bool VeritProofPostprocessCallback::update(Node res,
              && addVeritStep(vp3, VeritRule::RESOLUTION, {vp1, vp2}, {}, *cdp)
              && addVeritStep(vp4, VeritRule::REORDER, {vp3}, {}, *cdp)
              && addVeritStepFromOr(
-                    res, VeritRule::DUPLICATED_LITERALS, {vp4}, {}, *cdp);
+                 res, VeritRule::DUPLICATED_LITERALS, {vp4}, {}, *cdp);
     }
     // ======== CNF ITE Neg version 1
     // Children: ()
@@ -1918,7 +1925,7 @@ bool VeritProofPostprocessCallback::update(Node res,
              && addVeritStep(vp3, VeritRule::RESOLUTION, {vp1, vp2}, {}, *cdp)
              && addVeritStep(vp4, VeritRule::REORDER, {vp3}, {}, *cdp)
              && addVeritStepFromOr(
-                    res, VeritRule::DUPLICATED_LITERALS, {vp4}, {}, *cdp);
+                 res, VeritRule::DUPLICATED_LITERALS, {vp4}, {}, *cdp);
     }
 
     //================================================= Equality rules
diff --git a/src/smt/proof_final_callback.cpp b/src/smt/proof_final_callback.cpp
index 9f561e8a1..4c73d00aa 100644
--- a/src/smt/proof_final_callback.cpp
+++ b/src/smt/proof_final_callback.cpp
@@ -31,7 +31,7 @@ namespace smt {
 
 ProofFinalCallback::ProofFinalCallback(ProofNodeManager* pnm)
     : d_ruleCount(smtStatisticsRegistry().registerHistogram<PfRule>(
-          "finalProof::ruleCount")),
+        "finalProof::ruleCount")),
       d_instRuleIds(
           smtStatisticsRegistry().registerHistogram<theory::InferenceId>(
               "finalProof::instRuleId")),
diff --git a/src/theory/quantifiers/query_cache.cpp b/src/theory/quantifiers/query_cache.cpp
index cfd4c313e..f73c20ab2 100644
--- a/src/theory/quantifiers/query_cache.cpp
+++ b/src/theory/quantifiers/query_cache.cpp
@@ -77,7 +77,8 @@ bool QueryCache::addTerm(Node sol)
     {
       sol = convertToSkolem(sol);
       std::vector<Node> modelVals;
-      Result r = checkWithSubsolver(sol, d_skolems, modelVals, d_subOptions, d_env.getLogicInfo());
+      Result r = checkWithSubsolver(
+          sol, d_skolems, modelVals, d_subOptions, d_env.getLogicInfo());
       if (r.asSatisfiabilityResult().isSat() != Result::UNSAT)
       {
         // check the sample point
diff --git a/src/theory/strings/infer_proof_cons.cpp b/src/theory/strings/infer_proof_cons.cpp
index 0da360a0c..8812c971a 100644
--- a/src/theory/strings/infer_proof_cons.cpp
+++ b/src/theory/strings/infer_proof_cons.cpp
@@ -787,7 +787,11 @@ void InferProofCons::convert(InferenceId infer,
       Trace("strings-ipc-prefix")
           << "- Possible conflicting equality : " << curr << std::endl;
       std::vector<Node> emp;
-      Node concE = psb.applyPredElim(curr, emp, MethodId::SB_DEFAULT, MethodId::SBA_SEQUENTIAL, MethodId::RW_REWRITE_EQ_EXT);
+      Node concE = psb.applyPredElim(curr,
+                                     emp,
+                                     MethodId::SB_DEFAULT,
+                                     MethodId::SBA_SEQUENTIAL,
+                                     MethodId::RW_REWRITE_EQ_EXT);
       Trace("strings-ipc-prefix")
           << "- After pred elim: " << concE << std::endl;
       if (concE == conc)