Format

3 files changed, 9 insertions, 8 deletions

diff --git a/src/expr/proof_node_manager.h b/src/expr/proof_node_manager.h
index 6562d3e02..01ab6d915 100644
--- a/src/expr/proof_node_manager.h
+++ b/src/expr/proof_node_manager.h
@@ -80,17 +80,17 @@ class ProofNodeManager
                                     Node expected = Node::null());
   /**
    * Make the proof node corresponding to the assumption of fact.
-   * 
+   *
    * @param fact The fact to assume.
    * @return The assume proof of fact.
    */
   std::shared_ptr<ProofNode> mkAssume(Node fact);
-  /** 
+  /**
    * Make scope having body pf and arguments (assumptions-to-close) assump.
    * If ensureClosed is true, then this method throws an assertion failure if
    * the returned proof is not closed. This is the case if a free assumption
-   * of pf is missing from the vector assumps. 
-   * 
+   * of pf is missing from the vector assumps.
+   *
    * For conveinence, the proof pf may be modified to ensure that the overall
    * result is closed. For instance, given input:
    *   pf = TRANS( ASSUME( x=y ), ASSUME( y=z ) )
@@ -99,11 +99,11 @@ class ProofNodeManager
    *   pf = TRANS( SYMM( ASSUME( y=x ) ), ASSUME( y=z ) )
    * so that y=x matches the free assumption. The returned proof is:
    *   SCOPE(TRANS( SYMM( ASSUME( y=x ) ), ASSUME( y=z ) ) :args { y=x, y=z })
-   * 
+   *
    * Additionally, if both ensureClosed and doMinimize are true, assumps is
    * updated to contain exactly the free asumptions of pf. The minimized
    * vector is passed as arguments to the SCOPE.
-   * 
+   *
    * @param pf The body of the proof,
    * @param assumps The assumptions-to-close of the scope,
    * @param ensureClosed Whether to ensure that the proof is closed,
diff --git a/src/theory/booleans/proof_checker.cpp b/src/theory/booleans/proof_checker.cpp
index 37f8d209d..9e5758764 100644
--- a/src/theory/booleans/proof_checker.cpp
+++ b/src/theory/booleans/proof_checker.cpp
@@ -547,7 +547,8 @@ Node BoolProofRuleChecker::checkInternal(PfRule id,
     {
       return Node::null();
     }
-    std::vector<Node> disjuncts{args[0], args[0][1].notNode(), args[0][2].notNode()};
+    std::vector<Node> disjuncts{
+        args[0], args[0][1].notNode(), args[0][2].notNode()};
     return NodeManager::currentNM()->mkNode(kind::OR, disjuncts);
   }
   // no rule
diff --git a/src/theory/uf/proof_equality_engine.cpp b/src/theory/uf/proof_equality_engine.cpp
index f26012177..9dc674650 100644
--- a/src/theory/uf/proof_equality_engine.cpp
+++ b/src/theory/uf/proof_equality_engine.cpp
@@ -388,7 +388,7 @@ TrustNode ProofEqEngine::ensureProofForFact(Node conc,
     // words, the SCOPE could be closing (= x y) in a proof with free
     // assumption (= y x). We modify the proof leaves to account for this
     // below.
-    
+
     std::vector<Node> scopeAssumps;
     // we first ensure the assumptions are flattened
     for (const TNode& a : assumps)