3 files changed, 32 insertions, 13 deletions
diff --git a/src/sat/bsat/satInterA.c b/src/sat/bsat/satInterA.c
index 5837e68f..82f4e034 100644
--- a/src/sat/bsat/satInterA.c
+++ b/src/sat/bsat/satInterA.c
@@ -809,8 +809,12 @@ int Inta_ManProcessRoots( Inta_Man_t * p )
         if ( !Inta_ManEnqueue( p, pClause->pLits[0], pClause ) )
         {
             // detected root level conflict
-            printf( "Error in Inta_ManProcessRoots(): Detected a root-level conflict too early!\n" );
-            assert( 0 );
+//            printf( "Error in Inta_ManProcessRoots(): Detected a root-level conflict too early!\n" );
+//            assert( 0 );
+            // detected root level conflict
+            Inta_ManProofTraceOne( p, pClause, p->pCnf->pEmpty );
+            if ( p->fVerbose )
+                printf( "Found root level conflict!\n" );
             return 0;
         }
     }
diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c
index 0179796c..12529ca7 100644
--- a/src/sat/bsat/satSolver.c
+++ b/src/sat/bsat/satSolver.c
@@ -1061,7 +1061,8 @@ bool sat_solver_addclause(sat_solver* s, lit* begin, lit* end)
     begin = veci_begin( &s->temp_clause );
     end = begin + veci_size( &s->temp_clause );
 
-    if (begin == end) return false;
+    if (begin == end) 
+        return false;
 
     //printlits(begin,end); printf("\n");
     // insertion sort
@@ -1076,6 +1077,16 @@ bool sat_solver_addclause(sat_solver* s, lit* begin, lit* end)
     sat_solver_setnvars(s,maxvar+1);
 //    sat_solver_setnvars(s, lit_var(*(end-1))+1 );
 
+    ///////////////////////////////////
+    // add clause to internal storage
+    if ( s->pStore )
+    {
+        extern int Sto_ManAddClause( void * p, lit * pBeg, lit * pEnd );
+        int RetValue = Sto_ManAddClause( s->pStore, begin, end );
+        assert( RetValue );
+    }
+    ///////////////////////////////////
+
     //printlits(begin,end); printf("\n");
     values = s->assigns;
 
@@ -1095,16 +1106,6 @@ bool sat_solver_addclause(sat_solver* s, lit* begin, lit* end)
     if (j == begin)          // empty clause
         return false;
 
-    ///////////////////////////////////
-    // add clause to internal storage
-    if ( s->pStore )
-    {
-        extern int Sto_ManAddClause( void * p, lit * pBeg, lit * pEnd );
-        int RetValue = Sto_ManAddClause( s->pStore, begin, j );
-        assert( RetValue );
-    }
-    ///////////////////////////////////
-
     if (j - begin == 1) // unit clause
         return enqueue(s,*begin,(clause*)0);
 
@@ -1164,6 +1165,19 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, sint64 nConfLimit, sin
     lbool*  values        = s->assigns;
     lit*    i;
 
+    ////////////////////////////////////////////////
+    if ( s->fSolved )
+    {
+        if ( s->pStore )
+        {
+            extern int Sto_ManAddClause( void * p, lit * pBeg, lit * pEnd );
+            int RetValue = Sto_ManAddClause( s->pStore, NULL, NULL );
+            assert( RetValue );
+        }
+        return l_False;
+    }
+    ////////////////////////////////////////////////
+
     // set the external limits
     s->nCalls++;
     s->nRestarts  = 0;
diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h
index 9ffc2b75..86e7a966 100644
--- a/src/sat/bsat/satSolver.h
+++ b/src/sat/bsat/satSolver.h
@@ -182,6 +182,7 @@ struct sat_solver_t
 
     // clause store
     void *   pStore;
+    int      fSolved;
 
     // trace recording
     FILE *   pFile;