comment

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));

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;
 }