Format

ajreynol · Dec 17, 2024 · 3226cb0 · 3226cb0
1 parent 2e46dea
commit 3226cb0
Show file tree

Hide file tree

Showing 3 changed files with 7 additions and 7 deletions.
diff --git a/src/expr/node_algorithm.cpp b/src/expr/node_algorithm.cpp
@@ -805,7 +805,7 @@ void getMatchConditions(Node n1, Node n2, std::vector<Node>& eqs)
         for (size_t i = 0, n = curr.first.getNumChildren(); i < n; ++i)
         {
           // if there is a type mismatch, we can't unify
-          if (curr.first[i].getType()!=curr.second[i].getType())
+          if (curr.first[i].getType() != curr.second[i].getType())
           {
             stack.resize(prevSize);
             rec = false;

diff --git a/src/rewriter/basic_rewrite_rcons.cpp b/src/rewriter/basic_rewrite_rcons.cpp
@@ -1168,11 +1168,11 @@ bool BasicRewriteRCons::ensureProofMacroQuantRewriteBody(CDProof* cdp,
   // term context.
   WithinKindTermContext wktc(Kind::INST_PATTERN_LIST);
   TConvProofGenerator tcpg(d_env,
-            nullptr,
-            TConvPolicy::FIXPOINT,
-            TConvCachePolicy::NEVER,
-            "EnsureProofMacroQuantRewrite",
-            &wktc);
+                           nullptr,
+                           TConvPolicy::FIXPOINT,
+                           TConvCachePolicy::NEVER,
+                           "EnsureProofMacroQuantRewrite",
+                           &wktc);
   theory::quantifiers::QuantifiersRewriter qrew(
       nodeManager(), d_env.getRewriter(), options());
   Node qr = qrew.computeRewriteBody(eq[0], &tcpg);

diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -280,7 +280,7 @@ Node QuantifiersRewriter::rewriteViaRule(ProofRewriteRule id, const Node& n)
         while (varIndex < nvars && fvs.find(n[0][varIndex]) != fvs.end())
         {
           // cannot have shadowing
-          if (varsUsed.find(n[0][varIndex])!=varsUsed.end())
+          if (varsUsed.find(n[0][varIndex]) != varsUsed.end())
           {
             return Node::null();
           }