Format

4 files changed, 13 insertions, 6 deletions

diff --git a/src/theory/strings/infer_proof_cons.cpp b/src/theory/strings/infer_proof_cons.cpp
index 3eaf2c17d..b10bc47be 100644
--- a/src/theory/strings/infer_proof_cons.cpp
+++ b/src/theory/strings/infer_proof_cons.cpp
@@ -42,7 +42,7 @@ void InferProofCons::notifyFact(const InferInfo& ii)
 {
   Trace("strings-ipc-debug")
       << "InferProofCons::notifyFact: " << ii << std::endl;
-  if (d_lazyFactMap.find(ii.d_conc)!=d_lazyFactMap.end())
+  if (d_lazyFactMap.find(ii.d_conc) != d_lazyFactMap.end())
   {
     Trace("strings-ipc-debug") << "...duplicate!" << std::endl;
     return;
diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index 56f081151..67213fb9b 100644
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -460,7 +460,7 @@ void EqualityEngine::assertPredicate(TNode t, bool polarity, TNode reason, unsig
   Debug("equality") << d_name << "::eq::addPredicate(" << t << "," << (polarity ? "true" : "false") << ")" << std::endl;
   Assert(t.getKind() != kind::EQUAL) << "Use assertEquality instead";
   TNode b = polarity ? d_true : d_false;
-  if (hasTerm(t) && areEqual(t,b))
+  if (hasTerm(t) && areEqual(t, b))
   {
     return false;
   }
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index 5d6801c7b..7f86da54f 100644
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -811,7 +811,10 @@ public:
    * @param reason the reason to keep for building explanations
    * @return true if a new fact was asserted, false if this call was a no-op.
    */
-  bool assertPredicate(TNode p, bool polarity, TNode reason, unsigned pid = MERGED_THROUGH_EQUALITY);
+  bool assertPredicate(TNode p,
+                       bool polarity,
+                       TNode reason,
+                       unsigned pid = MERGED_THROUGH_EQUALITY);
 
   /**
    * Adds an equality eq with the given polarity to the database.
@@ -822,7 +825,10 @@ public:
    * @param reason the reason to keep for building explanations
    * @return true if a new fact was asserted, false if this call was a no-op.
    */
-  bool assertEquality(TNode eq, bool polarity, TNode reason, unsigned pid = MERGED_THROUGH_EQUALITY);
+  bool assertEquality(TNode eq,
+                      bool polarity,
+                      TNode reason,
+                      unsigned pid = MERGED_THROUGH_EQUALITY);
 
   /**
    * Returns the current representative of the term t.
diff --git a/src/theory/uf/proof_equality_engine.cpp b/src/theory/uf/proof_equality_engine.cpp
index 6838c9568..d600a546b 100644
--- a/src/theory/uf/proof_equality_engine.cpp
+++ b/src/theory/uf/proof_equality_engine.cpp
@@ -460,8 +460,9 @@ TrustNode ProofEqEngine::ensureProofForFact(Node conc,
       {
         ss << "- assumption: " << aprint << std::endl;
       }
-      AlwaysAssert(false) << "Generated a proof that is not closed by the scope: " << ss.str()
-                          << std::endl;
+      AlwaysAssert(false)
+          << "Generated a proof that is not closed by the scope: " << ss.str()
+          << std::endl;
     }
     if (acu.size() < ac.size())
     {