3 files changed, 9 insertions, 1 deletions
diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c
index 0a7cb1c7..2e3af2dd 100644
--- a/src/sat/bsat/satSolver.c
+++ b/src/sat/bsat/satSolver.c
@@ -1502,7 +1502,9 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit
     lbool   status        = l_Undef;
     lit*    i;
 
-//    printf( "Running SAT solver with parameters %d and %d and %d.\n", s->nLearntStart, s->nLearntDelta, s->nLearntRatio );
+    if ( s->fVerbose )
+        printf( "Running SAT solver with parameters %d and %d and %d.\n", s->nLearntStart, s->nLearntDelta, s->nLearntRatio );
+
     ////////////////////////////////////////////////
     if ( s->fSolved )
     {
diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c
index 0e456f46..58ea531c 100644
--- a/src/sat/bsat/satSolver2.c
+++ b/src/sat/bsat/satSolver2.c
@@ -1574,6 +1574,7 @@ void sat_solver2_rollback( sat_solver2* s )
     for ( i = 2*s->iVarPivot; i < 2*s->size; i++ )
         s->wlists[i].size = 0;
 
+
     // initialize other vars
     s->size = s->iVarPivot;
     if ( s->size == 0 )
diff --git a/src/sat/bsat/satSolver2.h b/src/sat/bsat/satSolver2.h
index bca9bc97..cba57638 100644
--- a/src/sat/bsat/satSolver2.h
+++ b/src/sat/bsat/satSolver2.h
@@ -212,6 +212,11 @@ static inline int sat_solver2_nclauses(sat_solver2* s)
     return (int)s->stats.clauses;
 }
 
+static inline int sat_solver2_nlearnts(sat_solver2* s)
+{
+    return (int)s->stats.learnts;
+}
+
 static inline int sat_solver2_nconflicts(sat_solver2* s)
 {
     return (int)s->stats.conflicts;