Version abc70202

2 files changed, 25 insertions, 21 deletions

diff --git a/src/sat/bsat/satInter.c b/src/sat/bsat/satInter.c
index 32a011b9..b52cd6c7 100644
--- a/src/sat/bsat/satInter.c
+++ b/src/sat/bsat/satInter.c
@@ -771,7 +771,8 @@ int Int_ManProofRecordOne( Int_Man_t * p, Sto_Cls_t * pClause )
     {
         // construct the proof
         Int_ManProofTraceOne( p, pConflict, p->pCnf->pEmpty );
-        printf( "Found last conflict after adding unit clause number %d!\n", pClause->Id );
+        if ( p->fVerbose )
+            printf( "Found last conflict after adding unit clause number %d!\n", pClause->Id );
         return 0;
     }
 
@@ -827,7 +828,7 @@ int Int_ManProcessRoots( Int_Man_t * p )
         if ( !Int_ManEnqueue( p, pClause->pLits[0], pClause ) )
         {
             // detected root level conflict
-            printf( "Int_ManProcessRoots(): Detected a root-level conflict\n" );
+            printf( "Error in Int_ManProcessRoots(): Detected a root-level conflict too early!\n" );
             assert( 0 );
             return 0;
         }
@@ -838,8 +839,9 @@ int Int_ManProcessRoots( Int_Man_t * p )
     if ( pClause )
     {
         // detected root level conflict
-        printf( "Int_ManProcessRoots(): Detected a root-level conflict\n" );
-//        assert( 0 );
+        Int_ManProofTraceOne( p, pClause, p->pCnf->pEmpty );
+        if ( p->fVerbose )
+            printf( "Found root level conflict!\n" );
         return 0;
     }
 
@@ -925,17 +927,12 @@ int Int_ManInterpolate( Int_Man_t * p, Sto_Man_t * pCnf, int fVerbose, unsigned
     // check that the CNF makes sense
     assert( pCnf->nVars > 0 && pCnf->nClauses > 0 );
     p->pCnf = pCnf;
+    p->fVerbose = fVerbose;
+    *ppResult = NULL;
 
     // adjust the manager
     Int_ManResize( p );
 
-    // propagate root level assignments
-    if ( !Int_ManProcessRoots( p ) )
-    {
-        *ppResult = NULL;
-        return p->nVarsAB;
-    }
-
     // prepare the interpolant computation
     Int_ManPrepareInter( p );
 
@@ -951,15 +948,19 @@ int Int_ManInterpolate( Int_Man_t * p, Sto_Man_t * pCnf, int fVerbose, unsigned
     Sto_ManForEachClauseRoot( p->pCnf, pClause )
         Int_ManProofWriteOne( p, pClause );
 
-    // consider each learned clause
-    Sto_ManForEachClause( p->pCnf, pClause )
+    // propagate root level assignments
+    if ( Int_ManProcessRoots( p ) )
     {
-        if ( pClause->fRoot )
-            continue;
-        if ( !Int_ManProofRecordOne( p, pClause ) )
+        // if there is no conflict, consider learned clauses
+        Sto_ManForEachClause( p->pCnf, pClause )
         {
-            RetValue = 0;
-            break;
+            if ( pClause->fRoot )
+                continue;
+            if ( !Int_ManProofRecordOne( p, pClause ) )
+            {
+                RetValue = 0;
+                break;
+            }
         }
     }
 
@@ -970,12 +971,15 @@ int Int_ManInterpolate( Int_Man_t * p, Sto_Man_t * pCnf, int fVerbose, unsigned
         p->pFile = NULL;    
     }
 
+    if ( fVerbose )
+    {
     printf( "Vars = %d. Roots = %d. Learned = %d. Resol steps = %d.  Ave = %.2f.  Mem = %.2f Mb\n", 
         p->pCnf->nVars, p->pCnf->nRoots, p->pCnf->nClauses-p->pCnf->nRoots, p->Counter,  
         1.0*(p->Counter-p->pCnf->nRoots)/(p->pCnf->nClauses-p->pCnf->nRoots), 
         1.0*Sto_ManMemoryReport(p->pCnf)/(1<<20) );
-
 p->timeTotal += clock() - clkTotal;
+    }
+
     *ppResult = Int_ManTruthRead( p, p->pCnf->pTail );
     return p->nVarsAB;
 }
diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c
index 1756b5df..c4847be4 100644
--- a/src/sat/bsat/satSolver.c
+++ b/src/sat/bsat/satSolver.c
@@ -1264,7 +1264,7 @@ void sat_solver_store_alloc( sat_solver * s )
 void sat_solver_store_write( sat_solver * s, char * pFileName )
 {
     extern void Sto_ManDumpClauses( void * p, char * pFileName );
-    Sto_ManDumpClauses( s->pStore, pFileName );
+    if ( s->pStore ) Sto_ManDumpClauses( s->pStore, pFileName );
 }
 
 void sat_solver_store_free( sat_solver * s )
@@ -1273,7 +1273,7 @@ void sat_solver_store_free( sat_solver * s )
     if ( s->pStore ) Sto_ManFree( s->pStore );
     s->pStore = NULL;
 }
-
+ 
 void sat_solver_store_mark_roots( sat_solver * s )
 {
     extern void Sto_ManMarkRoots( void * p );