From 2906ef01a19fbd8ec3d583daa24f3210460da0f3 Mon Sep 17 00:00:00 2001
From: Giles <--global>
Date: Mon, 2 Jun 2014 09:05:59 +0100
Subject: [PATCH] comment

---
 SAT/MinimizingSolver.cpp | 2 +-
 Saturation/SSplitter.cpp | 4 +++-
 2 files changed, 4 insertions(+), 2 deletions(-)

diff --git a/SAT/MinimizingSolver.cpp b/SAT/MinimizingSolver.cpp
index 7e0abbb799..ffc994a862 100644
--- a/SAT/MinimizingSolver.cpp
+++ b/SAT/MinimizingSolver.cpp
@@ -48,7 +48,7 @@ void MinimizingSolver::addClauses(SATClauseIterator cit, bool onlyPropagate)
   newClauses.loadFromIterator(cit);
 
   //we need to filter out the empty clause -- it won't have any influence on our algorithm
-  //(as it will make the problem unsat and we process only satisfiale assignment), but it'd
+  //(as it will make the problem unsat and we process only satisfiale assignment), but it
   //is a corner case that needs to be handled
   _unprocessed.loadFromIterator(
       getFilteredIterator(SATClauseStack::BottomFirstIterator(newClauses), isNonEmptyClause));
diff --git a/Saturation/SSplitter.cpp b/Saturation/SSplitter.cpp
index 9f4ae3ae52..1455664c41 100644
--- a/Saturation/SSplitter.cpp
+++ b/Saturation/SSplitter.cpp
@@ -457,7 +457,7 @@ bool SSplitter::shouldAddClauseForNonSplittable(Clause* cl, unsigned& compName,
   }
 
   if(_congruenceClosure && cl->length()==1 && (*cl)[0]->ground() && cl->splits()->isEmpty()) {
-    //we add ground clauses if we use congruence closure...
+    //we add ground unit clauses if we use congruence closure...
     compName = getComponentName(cl->length(), cl->literals(), cl, compCl);
     RSTAT_CTR_INC("ssat_ground_clauses_for_congruence");
     return true;
@@ -490,6 +490,8 @@ bool SSplitter::shouldAddClauseForNonSplittable(Clause* cl, unsigned& compName,
   }
   ASS_NEQ(cl,compCl);
 
+  // We only reach here if cl already exists as a component
+
   return true;
 }