refactor(src/opensmt/smtsolvers/CoreSMTSolver.C): fixed style

dreal · May 6, 2015 · 344e64c · 344e64c
1 parent 876f92b
commit 344e64c
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 4 deletions.
diff --git a/src/opensmt/smtsolvers/CoreSMTSolver.C b/src/opensmt/smtsolvers/CoreSMTSolver.C
@@ -1750,7 +1750,7 @@ lbool CoreSMTSolver::search(int nof_conflicts, int nof_learnts)
             if ( res == -1 ) return l_False;
             assert( res == 1 );
 
-            if(config.nra_short_sat) {
+            if (config.nra_short_sat) {
             	// the problem is satisfiable as res = 1 at this point
             	return l_True;
             }
@@ -1964,13 +1964,13 @@ int CoreSMTSolver::restartNextLimit ( int nof_conflicts )
 }
 /*_________________________________________________________________________________________________
  |
- |  entailment : ()  ->  [lbool]
+ |  entailment : ()  ->  [bool]
  |
  |  Description:
  |   Checks if all clauses are satisfied.
  |
  |  Output:
- |    'l_True' if all clauses are satisfied. 'l_False'
+ |    'true' if all clauses are satisfied. 'false'
  |    if there exists unsatisfied clause.
  |________________________________________________________________________________________________@*/
 

diff --git a/src/opensmt/smtsolvers/CoreSMTSolver.h b/src/opensmt/smtsolvers/CoreSMTSolver.h
@@ -337,7 +337,7 @@ class CoreSMTSolver : public SMTSolver
         int    restartNextLimit       ( int );         // Next conflict limit for restart
         Var    generateMoreEij        ( );             // Generate more eij
         Var    generateNextEij        ( );             // Generate next eij
-        bool   entailment             ( );             // Check is a partial assignment entails a formula
+        bool   entailment             ( );             // Check if a partial assignment entails a formula
 
 #ifndef SMTCOMP
         void   dumpCNF                ( );             // Dumps CNF to cnf.smt2