Variable timeframe abstraction.

6 files changed, 199 insertions, 306 deletions

diff --git a/src/aig/gia/giaAbsVta.c b/src/aig/gia/giaAbsVta.c
index 4af2b7e7..cd8e14b9 100644
--- a/src/aig/gia/giaAbsVta.c
+++ b/src/aig/gia/giaAbsVta.c
@@ -66,7 +66,12 @@ struct Vta_Man_t_
     Vec_Int_t *   vCla2Var;     // map clauses into variables
     Vec_Ptr_t *   vCores;       // unsat core for each frame
     sat_solver2 * pSat;         // incremental SAT solver
-    int           iPivot;
+    Vec_Int_t *   vAddedNew;    // the IDs of variables added to the solver
+    // statistics 
+    int           timeSat;
+    int           timeUnsat;
+    int           timeCex;
+    int           timeOther;
 };
 
 
@@ -351,7 +356,7 @@ int Vec_IntDoubleWidth( Vec_Int_t * p, int nWords )
 ***********************************************************************/
 static inline int Vga_ManHash( int iObj, int iFrame, int nBins )
 {
-    return ((iObj + iFrame)*(iObj + iFrame + 1)) % nBins;
+    return ((unsigned)((iObj + iFrame)*(iObj + iFrame + 1))) % nBins;
 }
 static inline int * Vga_ManLookup( Vta_Man_t * p, int iObj, int iFrame )
 {
@@ -605,6 +610,8 @@ void Vta_ManSatVerify( Vta_Man_t * p )
         }
         else if ( Gia_ObjIsRo(p->pGia, pObj) )
         {
+            int VarA = Vta_ObjId(p,pThis);
+            int VarB = !pThis0 ? 0 : Vta_ObjId(p,pThis0);
             pObj = Gia_ObjRoToRi( p->pGia, pObj );
             if ( pThis->iFrame == 0 )
                 assert( pThis->Value == VTA_VAR0 );
@@ -637,7 +644,7 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
     Gia_Obj_t * pObj;
     int i, Counter;
 
-    Vta_ManSatVerify( p );
+//    Vta_ManSatVerify( p );
 
     // collect nodes in a topological order
     vOrder = Vta_ManCollectNodes( p, f );
@@ -647,7 +654,7 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
         pThis->Value = sat_solver2_var_value(p->pSat, Vta_ObjId(p, pThis)) ? VTA_VAR1 : VTA_VAR0;
         pThis->fVisit = 0;
     }
-
+/*
     // verify
     Vta_ManForEachObjObjVec( vOrder, p, pThis, pObj, i )
     {
@@ -674,7 +681,7 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
             else assert( 0 );
         }
     }
-
+*/
     // compute distance in reverse order
     pThis = Vta_ManObj( p, Vec_IntEntryLast(vOrder) );
     pThis->Prio  = 1;
@@ -787,7 +794,6 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
     pTop = Vta_ManObj( p, Vec_IntEntryLast(vOrder) );
     pTop->fVisit = 1;
     vTermsToAdd = Vec_IntAlloc( 100 );
-    printf( "\n\n" );
     Vta_ManForEachObjObjVecReverse( vOrder, p, pThis, pObj, i )
     {
         if ( !pThis->fVisit )
@@ -816,8 +822,6 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
                 assert( pThis1->Prio <= pThis->Prio );
                 pThis0->fVisit = 1;
                 pThis1->fVisit = 1;
-
-//                printf( "And1 %d requires %d %d\n", Vta_ObjId(p,pThis), Vta_ObjId(p,pThis0), Vta_ObjId(p,pThis1) );
             }
             else if ( pThis->Value == VTA_VAR0 )
             {
@@ -825,36 +829,30 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
                 {
                     if ( pThis0->fVisit )
                     {
-//                printf( "And0 %d requires %d\n", Vta_ObjId(p,pThis), Vta_ObjId(p,pThis0) );
                     }
                     else if ( pThis1->fVisit )
                     {
-//                printf( "And0 %d requires %d\n", Vta_ObjId(p,pThis), Vta_ObjId(p,pThis1) );
                     }
                     else if ( pThis0->Prio <= pThis1->Prio ) // choice!!!
                     {
                         pThis0->fVisit = 1;
                         assert( pThis0->Prio == pThis->Prio );
-//                printf( "And0 %d requires %d\n", Vta_ObjId(p,pThis), Vta_ObjId(p,pThis0) );
                     }
                     else
                     {
                         pThis1->fVisit = 1;
                         assert( pThis1->Prio == pThis->Prio );
-//                printf( "And0 %d requires %d\n", Vta_ObjId(p,pThis), Vta_ObjId(p,pThis1) );
                     }
                 }
                 else if ( Vta_ValIs0(pThis0, Gia_ObjFaninC0(pObj)) )
                 {
                     pThis0->fVisit = 1;
                     assert( pThis0->Prio == pThis->Prio );
-//                printf( "And0 %d requires %d\n", Vta_ObjId(p,pThis), Vta_ObjId(p,pThis0) );
                 }
                 else if ( Vta_ValIs0(pThis1, Gia_ObjFaninC1(pObj)) )
                 {
                     pThis1->fVisit = 1;
                     assert( pThis1->Prio == pThis->Prio );
-//                printf( "And0 %d requires %d\n", Vta_ObjId(p,pThis), Vta_ObjId(p,pThis1) );
                 }
                 else assert( 0 );
             }
@@ -869,14 +867,13 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
                 assert( pThis0 );
                 pThis0->fVisit = 1;
                 assert( pThis0->Prio == pThis->Prio );
-//                printf( "Reg %d requires %d\n", Vta_ObjId(p,pThis), Vta_ObjId(p,pThis0) );
             }
         }
         else if ( !Gia_ObjIsConst0(pObj) )
             assert( 0 );
     }
-//printf( "\n" );
 
+/*
     // verify
     Vta_ManForEachObjVec( vOrder, p, pThis, i )
         pThis->Value = VTA_VARX;
@@ -941,32 +938,18 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
         printf( "Vta_ManRefineAbstraction(): Terminary simulation verification failed!\n" );
 //    else
 //        printf( "Verification OK.\n" );
+*/
 
     // produce true counter-example
     if ( pTop->Prio == 0 )
         pCex = Vga_ManDeriveCex( p );
-/*
-    {
-        pCex = Abc_CexAlloc( Gia_ManRegNum(p->pGia), Gia_ManPiNum(p->pGia), p->pPars->iFrame+1 );
-        pCex->iPo = 0;
-        pCex->iFrame = p->pPars->iFrame;
-        Vta_ManForEachObjObjVec( vTermsToAdd, p, pThis, pObj, i )
-        {
-            assert( pThis->Value == VTA_VAR0 || pThis->Value == VTA_VAR1 );
-            assert( Gia_ObjIsConst0(pObj) || Gia_ObjIsCi(pObj) );
-            if ( Gia_ObjIsRo(p->pGia, pObj) )
-                assert( pThis->iFrame == 0 && pThis->Value == VTA_VAR0 );
-            else if ( Gia_ObjIsPi(p->pGia, pObj) && pThis->Value == VTA_VAR1 )
-                Abc_InfoSetBit( pCex->pData, pCex->nRegs + pThis->iFrame * pCex->nPis + Gia_ObjCioId(pObj) );
-        }
-    }
-*/
-    // perform refinement
     else
     {
+        int nObjOld = p->nObjs;
         Vta_ManForEachObjObjVec( vTermsToAdd, p, pThis, pObj, i )
             if ( !Gia_ObjIsPi(p->pGia, pObj) )
                 Vga_ManAddClausesOne( p, pThis->iObj, pThis->iFrame );
+        sat_solver2_simplify( p->pSat );
     }
     Vec_IntFree( vTermsToAdd );
     return pCex;
@@ -993,7 +976,7 @@ Vta_Man_t * Vga_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars )
     p->nObjsAlloc  = (1 << 20);
     p->pObjs       = ABC_CALLOC( Vta_Obj_t, p->nObjsAlloc );
     p->nObjs       = 1;
-    p->nBins       = Abc_PrimeCudd( p->nObjsAlloc/2 );
+    p->nBins       = Abc_PrimeCudd( 2*p->nObjsAlloc );
     p->pBins       = ABC_CALLOC( int, p->nBins );
     p->vOrder      = Vec_IntAlloc( 1013 );
     // abstraction
@@ -1023,10 +1006,10 @@ Vta_Man_t * Vga_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars )
         }
     }
     // other data
-    p->vCla2Var    = Vec_IntAlloc( 1000 );
+    p->vCla2Var    = Vec_IntAlloc( 1000 );  Vec_IntPush( p->vCla2Var, -1 );
     p->vCores      = Vec_PtrAlloc( 100 );
     p->pSat        = sat_solver2_new();
-    p->iPivot      = Gia_ObjFaninId0p(p->pGia, Gia_ManPo(p->pGia, 0));
+    p->vAddedNew   = Vec_IntAlloc( 1000 );
     return p;
 }
 
@@ -1043,7 +1026,7 @@ Vta_Man_t * Vga_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars )
 ***********************************************************************/
 void Vga_ManStop( Vta_Man_t * p )
 {
-    if ( p->pPars->fVerbose )
+//    if ( p->pPars->fVerbose )
         printf( "SAT solver:  Variables = %d. Clauses = %d. Conflicts = %d.\n", 
             sat_solver2_nvars(p->pSat), sat_solver2_nclauses(p->pSat), sat_solver2_nconflicts(p->pSat) );
 
@@ -1053,6 +1036,7 @@ void Vga_ManStop( Vta_Man_t * p )
     Vec_IntFreeP( &p->vSeens );
     Vec_IntFreeP( &p->vOrder );
     Vec_IntFreeP( &p->vCla2Var );
+    Vec_IntFreeP( &p->vAddedNew );
     sat_solver2_delete( p->pSat );
     ABC_FREE( p->pBins );
     ABC_FREE( p->pObjs );
@@ -1144,7 +1128,7 @@ Vec_Int_t * Vta_ManUnsatCore( int iLit, Vec_Int_t * vCla2Var, sat_solver2 * pSat
   SeeAlso     []
 
 ***********************************************************************/
-void Vta_ManAbsPrintFrame( Vta_Man_t * p, Vec_Int_t * vCore, int nFrames, int fVerbose )
+void Vta_ManAbsPrintFrame( Vta_Man_t * p, Vec_Int_t * vCore, int nFrames, int nCexes, int fVerbose )
 {
     unsigned * pInfo;
     int * pCountAll, * pCountUni;
@@ -1176,6 +1160,7 @@ void Vta_ManAbsPrintFrame( Vta_Man_t * p, Vec_Int_t * vCore, int nFrames, int fV
     {
     //    printf( "%5d%5d", pCountAll[0], pCountUni[0] ); 
         printf( "%6d", p->nSeenGla ); 
+        printf( "%5d", nCexes ); 
         printf( "%6d", pCountAll[0] ); 
         for ( k = 0; k < nFrames; k++ )
     //        printf( "%5d%5d  ", pCountAll[k+1], pCountUni[k+1] ); 
@@ -1203,38 +1188,25 @@ void Vga_ManAddClausesOne( Vta_Man_t * p, int iObj, int iFrame )
     Vta_Obj_t * pThis0, * pThis1;
     Gia_Obj_t * pObj = Gia_ManObj( p->pGia, iObj );
     Vta_Obj_t * pThis = Vga_ManFindOrAdd( p, iObj, iFrame );
-    int iMainVar = Vta_ObjId(p, pThis);
+    int iThis0, iMainVar = Vta_ObjId(p, pThis);
     assert( pThis->iObj == iObj && pThis->iFrame == iFrame );
-
-    if ( iObj == 317 && iFrame == 0 )
-    {
-        int s = 0;
-    }
     if ( pThis->fAdded )
-    {
-//        if ( p->iPivot == iObj )
-//            printf( "Pivot in frame %d is already added\n", iFrame );
         return;
-    }
-//    if ( p->iPivot == iObj )
-//        printf( "Adding pivot in frame %d\n", iFrame );
-//    printf( "(%d,%d) ", iObj, iFrame );
-
     pThis->fAdded = 1;
+    Vec_IntPush( p->vAddedNew, iMainVar );
     if ( Gia_ObjIsAnd(pObj) )
     {
         pThis0 = Vga_ManFindOrAdd( p, Gia_ObjFaninId0p(p->pGia, pObj), iFrame );
+        iThis0 = Vta_ObjId(p, pThis0);
         pThis1 = Vga_ManFindOrAdd( p, Gia_ObjFaninId1p(p->pGia, pObj), iFrame );
-        sat_solver2_add_and( p->pSat, iMainVar, Vta_ObjId(p, pThis0), Vta_ObjId(p, pThis1), 
+        sat_solver2_add_and( p->pSat, iMainVar, iThis0, Vta_ObjId(p, pThis1), 
             Gia_ObjFaninC0(pObj), Gia_ObjFaninC1(pObj), 0 );
         Vec_IntPush( p->vCla2Var, iMainVar );
         Vec_IntPush( p->vCla2Var, iMainVar );
         Vec_IntPush( p->vCla2Var, iMainVar );
-//printf( "Adding node %d (var %d)\n", iObj, iMainVar );
     }
     else if ( Gia_ObjIsRo(p->pGia, pObj) )
     {
-//printf( "Adding flop %d (var %d)\n", iObj, iMainVar );
         if ( iFrame == 0 )
         {
             if ( p->pPars->fUseTermVars )
@@ -1253,7 +1225,7 @@ void Vga_ManAddClausesOne( Vta_Man_t * p, int iObj, int iFrame )
         else
         {
             pObj = Gia_ObjRoToRi( p->pGia, pObj );
-            pThis0 = Vga_ManFindOrAdd( p, Gia_ObjFaninId0p(p->pGia, pObj), pThis->iFrame-1 );
+            pThis0 = Vga_ManFindOrAdd( p, Gia_ObjFaninId0p(p->pGia, pObj), iFrame-1 );
             sat_solver2_add_buffer( p->pSat, iMainVar, Vta_ObjId(p, pThis0), Gia_ObjFaninC0(pObj), 0 );  
             Vec_IntPush( p->vCla2Var, iMainVar );
             Vec_IntPush( p->vCla2Var, iMainVar );
@@ -1261,7 +1233,6 @@ void Vga_ManAddClausesOne( Vta_Man_t * p, int iObj, int iFrame )
     }
     else if ( Gia_ObjIsConst0(pObj) )
     {
-//printf( "Adding const %d (var %d)\n", iObj, iMainVar );
         sat_solver2_add_const( p->pSat, iMainVar, 1, 0 );
         Vec_IntPush( p->vCla2Var, iMainVar );
     }
@@ -1286,7 +1257,7 @@ void Vga_ManLoadSlice( Vta_Man_t * p, Vec_Int_t * vOne, int Lift )
     Vec_IntForEachEntry( vOne, Entry, i )
         Vga_ManAddClausesOne( p, Entry & p->nObjMask, (Entry >> p->nObjBits) + Lift );
     sat_solver2_simplify( p->pSat );
-    printf( "\n\n" );
+//    printf( "\n\n" );
 }
 
 /**Function*************************************************************
@@ -1346,10 +1317,18 @@ void Vga_ManRollBack( Vta_Man_t * p, int nObjOld )
 {
     Vta_Obj_t * pThis  = p->pObjs + nObjOld;
     Vta_Obj_t * pLimit = p->pObjs + p->nObjs;
+    int i, Entry;
     for ( ; pThis < pLimit; pThis++ )
         Vga_ManDelete( p, pThis->iObj, pThis->iFrame );
     memset( p->pObjs + nObjOld, 0, sizeof(Vta_Obj_t) * (p->nObjs - nObjOld) );
     p->nObjs = nObjOld;
+    Vec_IntForEachEntry( p->vAddedNew, Entry, i )
+        if ( Entry < p->nObjs )
+        {
+            pThis = Vta_ManObj(p, Entry);
+            assert( pThis->fAdded == 1 );
+            pThis->fAdded = 0;
+        }
 }
 
 /**Function*************************************************************
@@ -1369,7 +1348,7 @@ int Gia_VtaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
     Vec_Int_t * vCore;
     Abc_Cex_t * pCex = NULL;
     int i, f, nConfls, Status, RetValue = -1;
-    int clk = clock();
+    int clk = clock(), clk2;
     // preconditions
     assert( Gia_ManPoNum(pAig) == 1 );
     assert( pPars->nFramesMax == 0 || pPars->nFramesStart <= pPars->nFramesMax );
@@ -1377,7 +1356,7 @@ int Gia_VtaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
     p = Vga_ManStart( pAig, pPars );
     // perform initial abstraction
     if ( p->pPars->fVerbose )
-        printf( "Frame  Confl  One   All  F0  F1  F2  F3 ...\n" );
+        printf( "Frame Confl  One  Cex   All  F0  F1  F2  F3 ...\n" );
     for ( f = 0; !p->pPars->nFramesMax || f < p->pPars->nFramesMax; f++ )
     {
         if ( p->pPars->fVerbose )
@@ -1387,62 +1366,60 @@ int Gia_VtaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
         if ( f == p->nWords * 32 )
             p->nWords = Vec_IntDoubleWidth( p->vSeens, p->nWords );
         // check this timeframe
+        i = 0;
         if ( f < p->pPars->nFramesStart )
             Vga_ManLoadSlice( p, (Vec_Int_t *)Vec_PtrEntry(p->vFrames, f), 0 );
         else
-//        for ( f = 0; f < p->pPars->nFramesStart; f++ )
-//            Vga_ManLoadSlice( p, (Vec_Int_t *)Vec_PtrEntry(p->vFrames, f), 0 );
         {
             // create bookmark to be used for rollback
-            int nObjOld;
-            int nClaOld;
-//start:            
-            nObjOld = p->nObjs;
-            nClaOld = Vec_IntSize(p->vCla2Var);
+            int nObjOld = p->nObjs;
             sat_solver2_bookmark( p->pSat );
+            Vec_IntClear( p->vAddedNew );
             // load the time frame
             for ( i = 1; i <= Abc_MinInt(p->pPars->nFramesOver, p->pPars->nFramesStart); i++ )
-            {
                 Vga_ManLoadSlice( p, (Vec_Int_t *)Vec_PtrEntry(p->vCores, f-i), i );
-//Vga_ManPrintCore( p, (Vec_Int_t *)Vec_PtrEntry(p->vCores, f-i), i );
-            }
             // iterate as long as there are counter-examples
-            for ( i = 1; ; i++ )
+            for ( i = 0; ; i++ )
             {
+                clk2 = clock();
                 vCore = Vta_ManUnsatCore( Vga_ManGetOutLit(p, f), p->vCla2Var, p->pSat, pPars->nConfLimit, pPars->fVerbose, &Status, &nConfls );
                 assert( (vCore != NULL) == (Status == 1) );
                 if ( Status == -1 ) // resource limit is reached
                     goto finish;
                 if ( vCore != NULL )
+                {
+                    p->timeUnsat += clock() - clk2;
                     break;
-                printf( "Frame %d  iter %d...\n", f, i );
+                }
+                p->timeSat += clock() - clk2;
                 assert( Status == 0 );
+                // perform the refinement
+                clk2 = clock();
                 pCex = Vta_ManRefineAbstraction( p, f );
+                p->timeCex += clock() - clk2;
                 if ( pCex != NULL )
                     goto finish;
             }
             assert( Status == 1 );
-/*
             // valid core is obtained
             Vta_ManUnsatCoreRemap( p, vCore );
-printf( "Double checked core...\n" );
-Vga_ManPrintCore( p, vCore, 0 );
-//            Vec_IntSort( vCore, 0 );
+            Vec_IntSort( vCore, 1 );
             // update the SAT solver
             sat_solver2_rollback( p->pSat );
             // update storage
             Vga_ManRollBack( p, nObjOld );
-            Vec_IntShrink( p->vCla2Var, nClaOld );
+            Vec_IntShrink( p->vCla2Var, (int)p->pSat->stats.clauses+1 );
             // load this timeframe
+            nObjOld = p->nObjs;
             Vga_ManLoadSlice( p, vCore, 0 );
-*/
             Vec_IntFree( vCore );
-//            goto start;
         }
         // run SAT solver
+        clk2 = clock();
         vCore = Vta_ManUnsatCore( Vga_ManGetOutLit(p, f), p->vCla2Var, p->pSat, pPars->nConfLimit, p->pPars->fVerbose, &Status, &nConfls );
+        p->timeUnsat += clock() - clk2;
         if ( p->pPars->fVerbose )
-            printf( "%6d", nConfls );
+            printf( "%5d", nConfls );
         assert( (vCore != NULL) == (Status == 1) );
         if ( Status == -1 ) // resource limit is reached
             goto finish;
@@ -1454,20 +1431,11 @@ Vga_ManPrintCore( p, vCore, 0 );
         }
         // add the core
         Vta_ManUnsatCoreRemap( p, vCore );
-
-        if ( f >= p->pPars->nFramesStart )
-        {
-//            printf( "Core to record:\n" );
-//            Vga_ManPrintCore( p, vCore, 0 );
-        }
-
         // add in direct topological order
-//        Vec_IntSort( vCore, 1 );
+        Vec_IntSort( vCore, 1 );
         Vec_PtrPush( p->vCores, vCore );
         // print the result
-        Vta_ManAbsPrintFrame( p, vCore, f+1, p->pPars->fVerbose );
-//        if ( f == p->pPars->nFramesStart-1 )
-//           break;
+        Vta_ManAbsPrintFrame( p, vCore, f+1, i, p->pPars->fVerbose );
     }
 finish:
     // analize the results
@@ -1481,7 +1449,7 @@ finish:
         if ( Status == -1 )
             printf( "SAT solver ran out of resources at %d conflicts in frame %d.  ", pPars->nConfLimit, f );
         else
-            printf( "SAT solver completed %d frames and produced an abstraction.  ", f+1 );
+            printf( "SAT solver completed %d frames and produced an abstraction.  ", f );
     }
     else
     {
@@ -1492,6 +1460,14 @@ finish:
         printf( "Counter-example detected in frame %d.  ", f );
     }
     Abc_PrintTime( 1, "Time", clock() - clk );
+
+    p->timeOther = (clock() - clk) - p->timeUnsat - p->timeSat - p->timeCex;
+    ABC_PRTP( "Solver UNSAT", p->timeUnsat,  clock() - clk );
+    ABC_PRTP( "Solver SAT  ", p->timeSat,    clock() - clk );
+    ABC_PRTP( "Refinement  ", p->timeCex,    clock() - clk );
+    ABC_PRTP( "Other       ", p->timeOther,  clock() - clk );
+    ABC_PRTP( "TOTAL       ", clock() - clk, clock() - clk );
+
     Vga_ManStop( p );
     return RetValue;
 }
diff --git a/src/aig/saig/saigGlaPba2.c b/src/aig/saig/saigGlaPba2.c
index 8bc2b982..55aa0a3d 100644
--- a/src/aig/saig/saigGlaPba2.c
+++ b/src/aig/saig/saigGlaPba2.c
@@ -308,7 +308,7 @@ int Aig_Gla3CreateSatSolver( Aig_Gla3Man_t * p )
     Vec_IntPush( p->vCla2Fra, 0 );
     assert( Vec_IntSize(p->vCla2Fra) == Vec_IntSize(p->vCla2Obj) );
     assert( nVars == Vec_IntSize(p->vVar2Inf) );
-    assert( Vec_IntSize(p->vCla2Obj) == (int)p->pSat->stats.clauses );
+    assert( Vec_IntSize(p->vCla2Obj) == (int)p->pSat->stats.clauses+1 );
     if ( p->fVerbose )
         printf( "The resulting SAT problem contains %d variables and %d clauses.\n", 
             p->pSat->size, p->pSat->stats.clauses );
@@ -337,8 +337,8 @@ Aig_Gla3Man_t * Aig_Gla3ManStart( Aig_Man_t * pAig, int nStart, int nFramesMax,
     p->vObj2Vec   = Vec_IntStart( Aig_ManObjNumMax(pAig) );
     p->vVec2Var   = Vec_IntAlloc( 1 << 20 );
     p->vVar2Inf   = Vec_IntAlloc( 1 << 20 );
-    p->vCla2Obj   = Vec_IntAlloc( 1 << 20 );
-    p->vCla2Fra   = Vec_IntAlloc( 1 << 20 );
+    p->vCla2Obj   = Vec_IntAlloc( 1 << 20 ); Vec_IntPush( p->vCla2Obj, -1 );
+    p->vCla2Fra   = Vec_IntAlloc( 1 << 20 ); Vec_IntPush( p->vCla2Fra, -1 );
 
     // skip first vector ID
     p->nStart     = nStart;
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index cee1b439..bffff493 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -26234,7 +26234,7 @@ int Abc_CommandAbc9GlaCba( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( 1, "The number of frames should be a positive integer.\n" );
         return 0;
     }
-    if ( pPars->nStart > 0 && pPars->nStart >= pPars->nFramesMax )
+    if ( pPars->nStart > 0 && pPars->nFramesMax > 0 && pPars->nStart >= pPars->nFramesMax )
     {
         Abc_Print( 1, "The starting frame is larger than the max number of frames.\n" );
         return 0;
diff --git a/src/sat/bsat/satProof.c b/src/sat/bsat/satProof.c
index 111b3ece..b8420014 100644
--- a/src/sat/bsat/satProof.c
+++ b/src/sat/bsat/satProof.c
@@ -447,9 +447,13 @@ void Sat_ProofCheck( sat_solver2 * s )
     Vec_Int_t * vUsed, * vTemp;
     satset * pSet, * pSet0, * pSet1;
     int i, k, hRoot, Handle, Counter = 0, clk = clock(); 
-    if ( s->hLearntLast < 0 )
+//    if ( s->hLearntLast < 0 )
+//        return;
+//    hRoot = veci_begin(&s->claProofs)[satset_read(&s->learnts, s->hLearntLast>>1)->Id];
+    hRoot = s->hProofLast;
+    if ( hRoot == -1 )
         return;
-    hRoot = veci_begin(&s->claProofs)[satset_read(&s->learnts, s->hLearntLast>>1)->Id];
+
     // collect visited clauses
     vUsed = Proof_CollectUsedIter( vProof, NULL, hRoot );
     Proof_CleanCollected( vProof, vUsed );
@@ -490,7 +494,7 @@ void Sat_ProofCheck( sat_solver2 * s )
 
   Synopsis    [Collects nodes belonging to the UNSAT core.]
 
-  Description [The resulting array contains 0-based IDs of root clauses.]
+  Description [The resulting array contains 1-based IDs of root clauses.]
                
   SideEffects []
 
@@ -518,7 +522,8 @@ Vec_Int_t * Sat_ProofCollectCore( Vec_Int_t * vClauses, Vec_Int_t * vProof, Vec_
     {
         pNode->mark = 0;
         if ( fUseIds )
-            Vec_IntWriteEntry( vCore, i, pNode->Id - 1 );
+//            Vec_IntWriteEntry( vCore, i, pNode->Id - 1 );
+            Vec_IntWriteEntry( vCore, i, pNode->Id );
     }
     return vCore;
 }
@@ -592,9 +597,12 @@ void * Sat_ProofInterpolant( sat_solver2 * s, void * pGloVars )
     Aig_Man_t * pAig;
     Aig_Obj_t * pObj;
     int i, k, iVar, Lit, Entry, hRoot;
-    if ( s->hLearntLast < 0 )
+//    if ( s->hLearntLast < 0 )
+//        return NULL;
+//    hRoot = veci_begin(&s->claProofs)[satset_read(&s->learnts, s->hLearntLast>>1)->Id];
+    hRoot = s->hProofLast;
+    if ( hRoot == -1 )
         return NULL;
-    hRoot = veci_begin(&s->claProofs)[satset_read(&s->learnts, s->hLearntLast>>1)->Id];
 
     Sat_ProofInterpolantCheckVars( s, vGlobVars );
 
@@ -693,9 +701,12 @@ word * Sat_ProofInterpolantTruth( sat_solver2 * s, void * pGloVars )
     word * pRes = ABC_ALLOC( word, nWords );
     int i, k, iVar, Lit, Entry, hRoot;
     assert( nVars > 0 && nVars <= 16 );
-    if ( s->hLearntLast < 0 )
+//    if ( s->hLearntLast < 0 )
+//        return NULL;
+//    hRoot = veci_begin(&s->claProofs)[satset_read(&s->learnts, s->hLearntLast>>1)->Id];
+    hRoot = s->hProofLast;
+    if ( hRoot == -1 )
         return NULL;
-    hRoot = veci_begin(&s->claProofs)[satset_read(&s->learnts, s->hLearntLast>>1)->Id];
 
     Sat_ProofInterpolantCheckVars( s, vGlobVars );
 
@@ -794,9 +805,13 @@ void * Sat_ProofCore( sat_solver2 * s )
     Vec_Int_t * vProof    = (Vec_Int_t *)&s->proofs;
     Vec_Int_t * vCore, * vUsed;
     int hRoot;
-    if ( s->hLearntLast < 0 )
+//    if ( s->hLearntLast < 0 )
+//        return NULL;
+//    hRoot = veci_begin(&s->claProofs)[satset_read(&s->learnts, s->hLearntLast>>1)->Id];
+    hRoot = s->hProofLast;
+    if ( hRoot == -1 )
         return NULL;
-    hRoot = veci_begin(&s->claProofs)[satset_read(&s->learnts, s->hLearntLast>>1)->Id];
+
     // collect visited clauses
     vUsed = Proof_CollectUsedIter( vProof, NULL, hRoot );
     // collect core clauses 
diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c
index 37ae7354..25ba35c3 100644
--- a/src/sat/bsat/satSolver2.c
+++ b/src/sat/bsat/satSolver2.c
@@ -28,7 +28,6 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 
 ABC_NAMESPACE_IMPL_START
 
-#define SAT_USE_ANALYZE_FINAL
 #define SAT_USE_PROOF_LOGGING
 
 //=================================================================================================
@@ -150,7 +149,9 @@ static inline int     clause_is_used(sat_solver2* s, cla h)      { return (h & 1
 static inline int     var_reason    (sat_solver2* s, int v)            { return s->reasons[v];           } 
 static inline int     lit_reason    (sat_solver2* s, int l)            { return s->reasons[lit_var(l)];  } 
 static inline satset* var_unit_clause(sat_solver2* s, int v)           { return clause_read(s, s->units[v]);                                          } 
-static inline void    var_set_unit_clause(sat_solver2* s, int v, cla i){ assert(v >= 0 && v < s->size && !s->units[v]); s->units[v] = i; s->nUnits++; } 
+static inline void    var_set_unit_clause(sat_solver2* s, int v, cla i){ 
+    assert(v >= 0 && v < s->size && !s->units[v]); s->units[v] = i; s->nUnits++; 
+} 
 //static inline void    var_set_unit_clause(sat_solver2* s, int v, cla i){ assert(v >= 0 && v < s->size); s->units[v] = i; s->nUnits++; } 
 
 // these two only work after creating a clause before the solver is called
@@ -501,13 +502,8 @@ static void solver2_canceluntil(sat_solver2* s, int level) {
     int      bound;
     int      lastLev;
     int      c, x;
-
-    if ( level == 0 )
-    {
-        int ss = 0;
-    }
    
-    if (solver2_dlevel(s) <= level)
+    if (solver2_dlevel(s) < level)
         return;
 
     trail   = s->trail;
@@ -532,7 +528,7 @@ static void solver2_canceluntil(sat_solver2* s, int level) {
 }
 
 
-static void solver2_record(sat_solver2* s, veci* cls, int proof_id, int fSkipUnit)
+static void solver2_record(sat_solver2* s, veci* cls, int proof_id)
 {
     lit* begin = veci_begin(cls);
     lit* end   = begin + veci_size(cls);
@@ -540,7 +536,7 @@ static void solver2_record(sat_solver2* s, veci* cls, int proof_id, int fSkipUni
     assert(veci_size(cls) > 0);
     if ( veci_size(cls) == 1 )
     {
-        if ( s->fProofLogging && !fSkipUnit)
+        if ( s->fProofLogging )
             var_set_unit_clause(s, lit_var(begin[0]), Cid);
         Cid = 0;
     }
@@ -610,14 +606,12 @@ void Solver::analyzeFinal(satset* confl, bool skip_first)
 }
 */
 
-#ifdef SAT_USE_ANALYZE_FINAL
-
 static int solver2_analyze_final(sat_solver2* s, satset* conf, int skip_first)
 {
     int i, j, x;//, start;
     veci_resize(&s->conf_final,0);
     if ( s->root_level == 0 )
-        return -1;
+        return s->hProofLast;
     proof_chain_start( s, conf );
     assert( veci_size(&s->tagged) == 0 );
     satset_foreach_var( conf, x, i, skip_first ){
@@ -650,9 +644,6 @@ static int solver2_analyze_final(sat_solver2* s, satset* conf, int skip_first)
     return proof_chain_stop( s );
 }
 
-#endif
-
-
 static int solver2_lit_removable_rec(sat_solver2* s, int v)
 {
     // tag[0]: True if original conflict clause literal.
@@ -916,8 +907,6 @@ satset* solver2_propagate(sat_solver2* s)
         end   = begin + veci_size(ws);
 
         s->stats.propagations++;
-        s->simpdb_props--;
-
         for (i = j = begin; i < end; ){
             c = clause_read(s,*i);
             lits = c->pEnts;
@@ -968,7 +957,8 @@ satset* solver2_propagate(sat_solver2* s)
                         proof_chain_start( s, clause_read(s,Cid) );
                         proof_chain_resolve( s, NULL, Var );
                         proof_id = proof_chain_stop( s );
-                        clause_create_new( s, &Lit, &Lit, 1, proof_id );
+                        s->hProofLast = proof_id;
+//                        clause_create_new( s, &Lit, &Lit, 1, proof_id );
                     }
                 }
 
@@ -990,71 +980,10 @@ WatchFound: i++;
     return confl;
 }
 
-
-/*
-static void clause_remove(sat_solver2* s, satset* c)
-{
-    assert(lit_neg(c->pEnts[0]) < s->size*2);
-    assert(lit_neg(c->pEnts[1]) < s->size*2);
-
-    veci_remove(solver2_wlist(s,lit_neg(c->pEnts[0])),clause_handle(s,c));
-    veci_remove(solver2_wlist(s,lit_neg(c->pEnts[1])),clause_handle(s,c));
-
-    if (c->learnt){
-        s->stats.learnts--;
-        s->stats.learnts_literals -= c->nEnts;
-    }else{
-        s->stats.clauses--;
-        s->stats.clauses_literals -= c->nEnts;
-    }
-}
-*/
-
-static lbool clause_simplify(sat_solver2* s, satset* c)
-{
-    int i, x;
-    assert(solver2_dlevel(s) == 0);
-    satset_foreach_var( c, x, i, 0 )
-        if (var_value(s, x) == lit_sign(c->pEnts[i]))
-            return l_True;
-    return l_False;
-}
-
 int sat_solver2_simplify(sat_solver2* s)
 {
-    int TailOld = s->qtail;
-//    int type;
-    int Counter = 0;
     assert(solver2_dlevel(s) == 0);
-    // reset the head
-    s->qhead = 0;
-    if (solver2_propagate(s) != 0)
-        return false;
-//    printf( "Tail moved from %d to %d.\n", TailOld, s->qtail );
-
-    if (s->qhead == s->simpdb_assigns || s->simpdb_props > 0)
-        return true;
-/*
-    for (type = 0; type < 2; type++){
-        veci* cs  = type ? &s->learnts : &s->clauses;
-        int*  cls = (int*)veci_begin(cs);
-        int i, j;
-        for (j = i = 0; i < veci_size(cs); i++){
-            satset* c = clause_read(s,cls[i]);
-            if (lit_reason(s,c->pEnts[0]) != cls[i] &&
-                clause_simplify(s,c) == l_True)
-                clause_remove(s,c), Counter++;
-            else
-                cls[j++] = cls[i];
-        }
-        veci_resize(cs,j);
-    }
-*/
-//printf( "Simplification removed %d clauses (out of %d)...\n", Counter, s->stats.clauses );
-    s->simpdb_assigns = s->qhead;
-    // (shouldn't depend on 'stats' really, but it will do for now)
-    s->simpdb_props   = (int)(s->stats.clauses_literals + s->stats.learnts_literals);
-    return true;
+    return (solver2_propagate(s) == NULL);
 }
 
 /*
@@ -1123,11 +1052,10 @@ static lbool solver2_search(sat_solver2* s, ABC_INT64_T nof_conflicts)
 #endif
             s->stats.conflicts++; conflictC++;
             if (solver2_dlevel(s) <= s->root_level){
-#ifdef SAT_USE_ANALYZE_FINAL
                 proof_id = solver2_analyze_final(s, confl, 0);
                 assert( proof_id > 0 );
-                solver2_record(s,&s->conf_final, proof_id, 0);
-#endif
+//                solver2_record(s,&s->conf_final, proof_id);
+                s->hProofLast = proof_id;
                 veci_delete(&learnt_clause);
                 return l_False;
             }
@@ -1137,13 +1065,11 @@ static lbool solver2_search(sat_solver2* s, ABC_INT64_T nof_conflicts)
             blevel = veci_size(&learnt_clause) > 1 ? var_level(s, lit_var(veci_begin(&learnt_clause)[1])) : s->root_level;
             blevel = s->root_level > blevel ? s->root_level : blevel;
             solver2_canceluntil(s,blevel);
-            solver2_record(s,&learnt_clause, proof_id, 0);
-#ifdef SAT_USE_ANALYZE_FINAL
+            solver2_record(s,&learnt_clause, proof_id);
             // if (learnt_clause.size() == 1) level[var(learnt_clause[0])] = 0;    
             // (this is ugly (but needed for 'analyzeFinal()') -- in future versions, we will backtrack past the 'root_level' and redo the assumptions)
             if ( learnt_clause.size == 1 ) 
                 var_set_level( s, lit_var(learnt_clause.ptr[0]), 0 );
-#endif
             act_var_decay(s);
             act_clause_decay(s);
 
@@ -1169,9 +1095,9 @@ static lbool solver2_search(sat_solver2* s, ABC_INT64_T nof_conflicts)
                 return l_Undef; 
             }
 
-            if (solver2_dlevel(s) == 0 && !s->fSkipSimplify)
+//            if (solver2_dlevel(s) == 0 && !s->fSkipSimplify)
                 // Simplify the set of problem clauses:
-                sat_solver2_simplify(s);
+//                sat_solver2_simplify(s);
 
             // New variable decision:
             s->stats.decisions++;
@@ -1267,9 +1193,12 @@ sat_solver2* sat_solver2_new(void)
         veci_push(&s->proofs, -1);
     }
     // initialize clause pointers
-    s->hClausePivot   =  1;
-    s->hLearntPivot   =  1;
     s->hLearntLast    = -1; // the last learnt clause 
+    s->hProofLast     = -1; // the last proof ID
+    s->hClausePivot   =  1; // the pivot among clauses
+    s->hLearntPivot   =  1; // the pivot moang learned clauses
+    s->iVarPivot      =  0; // the pivot among the variables
+    s->iSimpPivot     =  0; // marker of unit-clauses
     return s;
 }
 
@@ -1381,17 +1310,13 @@ void sat_solver2_delete(sat_solver2* s)
 }
 
 
-int sat_solver2_addclause__(sat_solver2* s, lit* begin, lit* end)
+int sat_solver2_addclause(sat_solver2* s, lit* begin, lit* end)
 {
-    lit *i,*j;
-    int maxvar;
-    lit last;
-
-    if (begin == end) 
-    {
-        assert( 0 );
-        return false;
-    }
+    cla Cid;
+    lit *i,*j,*iFree = NULL;
+    int maxvar, count, temp;
+    assert( solver2_dlevel(s) == 0 );
+    assert( begin < end );
 
     // copy clause into storage
     veci_resize( &s->temp_clause, 0 );
@@ -1400,7 +1325,6 @@ int sat_solver2_addclause__(sat_solver2* s, lit* begin, lit* end)
     begin = veci_begin( &s->temp_clause );
     end = begin + veci_size( &s->temp_clause );
 
-    //printlits(begin,end); printf("\n");
     // insertion sort
     maxvar = lit_var(*begin);
     for (i = begin + 1; i < end; i++){
@@ -1412,67 +1336,58 @@ int sat_solver2_addclause__(sat_solver2* s, lit* begin, lit* end)
     }
     sat_solver2_setnvars(s,maxvar+1);
 
-    // delete duplicates
-    last = lit_Undef;
-    for (i = j = begin; i < end; i++){
-        //printf("lit: "L_LIT", value = %d\n", L_lit(*i), (lit_sign(*i) ? -var_value(s, lit_var(*i)) : var_value(s, lit_var(*i))));
-        if (*i == lit_neg(last) || var_value(s, lit_var(*i)) == lit_sign(*i))
-            return true;   // tautology
-        else if (*i != last && var_value(s, lit_var(*i)) == varX)
-            last = *j++ = *i;
-    }
-    //printf("final: "); printlits(begin,j); printf("\n");
-    if (j == begin)          // empty clause
+    // coount the number of 0-literals
+    count = 0;
+    for ( i = begin; i < end; i++ )
     {
-        assert( 0 );
-        return false;
+        // make sure all literals are unique
+        assert( i == begin || lit_var(*(i-1)) != lit_var(*i) );
+        // consider the value of this literal
+        if ( var_value(s, lit_var(*i)) == lit_sign(*i) ) // this clause is always true
+            return clause_create_new( s, begin, end, 0, 0 ); // add it anyway, to preserve proper clause count       
+        if ( var_value(s, lit_var(*i)) == varX ) // unassigned literal
+            iFree = i;
+        else
+            count++; // literal is 0
     }
+    assert( count < end-begin ); // the clause cannot be UNSAT
 
-    if (j - begin == 1) // unit clause
-        return solver2_enqueue(s,*begin,0);
-
-    // create new clause
-    return clause_create_new(s,begin,j,0,0);
-}
-
-int sat_solver2_addclause(sat_solver2* s, lit* begin, lit* end)
-{
-    cla Cid;
-    lit *i,*j;
-    int maxvar;
-    assert( begin < end );
-
-    // copy clause into storage
-    veci_resize( &s->temp_clause, 0 );
-    for ( i = begin; i < end; i++ )
-        veci_push( &s->temp_clause, *i );
-    begin = veci_begin( &s->temp_clause );
-    end = begin + veci_size( &s->temp_clause );
-
-    // insertion sort
-    maxvar = lit_var(*begin);
-    for (i = begin + 1; i < end; i++){
-        lit l = *i;
-        maxvar = lit_var(l) > maxvar ? lit_var(l) : maxvar;
-        for (j = i; j > begin && *(j-1) > l; j--)
-            *j = *(j-1);
-        *j = l;
-    }
-    sat_solver2_setnvars(s,maxvar+1);
+    // swap variables to make sure the clause is watched using unassigned variable
+    temp   = *iFree;
+    *iFree = *begin;
+    *begin = temp;
 
     // create a new clause
     Cid = clause_create_new( s, begin, end, 0, 0 );
+
     // handle unit clause
-    if ( begin + 1 == end )
+    if ( count+1 == end-begin )
     {
-//        printf( "Adding unit clause %d\n", begin[0] );
-//        solver2_canceluntil(s, 0);
         if ( s->fProofLogging )
-            var_set_unit_clause( s, lit_var(begin[0]), Cid );
-        if ( !solver2_enqueue(s,begin[0],0) )
-            assert( 0 );
+        {
+            if ( count == 0 ) // original learned clause
+            {
+                var_set_unit_clause( s, lit_var(begin[0]), Cid );
+                if ( !solver2_enqueue(s,begin[0],0) )
+                    assert( 0 );
+            }
+            else
+            {
+                // Log production of top-level unit clause:
+                int x, k, proof_id, CidNew;
+                satset* c = clause_read(s, Cid);
+                proof_chain_start( s, c );
+                satset_foreach_var( c, x, k, 1 )
+                    proof_chain_resolve( s, NULL, x );
+                proof_id = proof_chain_stop( s );
+                // generate a new clause
+                CidNew = clause_create_new( s, begin, begin+1, 1, proof_id );
+                var_set_unit_clause( s, lit_var(begin[0]), CidNew );
+                if ( !solver2_enqueue(s,begin[0],Cid) )
+                    assert( 0 );
+            }
+        }
     }
-//satset_print( clause_read(s, Cid) );
     return Cid;
 }
 
@@ -1571,6 +1486,7 @@ void solver2_reducedb(sat_solver2* s)
 void sat_solver2_rollback( sat_solver2* s )
 {
     int i, k, j;
+    assert( s->qhead == s->qtail );
     assert( s->hClausePivot >= 1 && s->hClausePivot <= veci_size(&s->clauses) );
     assert( s->hLearntPivot >= 1 && s->hLearntPivot <= veci_size(&s->learnts) );
     assert( s->iVarPivot >= 0 && s->iVarPivot <= s->size );
@@ -1596,34 +1512,37 @@ void sat_solver2_rollback( sat_solver2* s )
             veci_resize(&s->wlists[i],j);
         }
         // compact units
-        if ( s->fProofLogging )
-        for ( i = 0; i < s->size; i++ )
-            if ( s->units[i] && !clause_is_used(s, s->units[i]) )
-                s->units[i] = 0;
+        if ( s->fProofLogging ) {
+            for ( i = 0; i < s->size; i++ )
+                if ( s->units[i] && !clause_is_used(s, s->units[i]) )
+                {
+                    var_set_value(s, i, varX);
+                    s->reasons[i] = 0;
+                    s->units[i] = 0;
+                }
+        }
     }
     // reset implication queue
-    assert( (&s->trail_lim)->ptr[0] == s->simpdb_assigns );
-    assert( s->simpdb_assigns >= s->iSimpPivot );
+    assert( (&s->trail_lim)->ptr[0] >= s->iSimpPivot );
     (&s->trail_lim)->ptr[0] = s->iSimpPivot;
-    s->simpdb_assigns = s->iSimpPivot;
     solver2_canceluntil( s, 0 );
     // reset problem clauses
     if ( s->hClausePivot < veci_size(&s->clauses) )
     {
         satset* first = satset_read(&s->clauses, s->hClausePivot);
-        s->stats.clauses = first->Id;
+        s->stats.clauses = first->Id-1;
         veci_resize(&s->clauses, s->hClausePivot);
     }
     // resetn learned clauses
     if ( s->hLearntPivot < veci_size(&s->learnts) )
     {
         satset* first = satset_read(&s->learnts, s->hLearntPivot);
-        veci_resize(&s->claActs,   first->Id+1);
+        veci_resize(&s->claActs,   first->Id);
         if ( s->fProofLogging ) {
-            veci_resize(&s->claProofs, first->Id+1);
+            veci_resize(&s->claProofs, first->Id);
             Sat_ProofReduce( s );
         }
-        s->stats.learnts = first->Id;
+        s->stats.learnts = first->Id-1;
         veci_resize(&s->learnts, s->hLearntPivot);
     }
     // reset watcher lists
@@ -1647,8 +1566,6 @@ void sat_solver2_rollback( sat_solver2* s )
         s->cla_inc                = (1 << 11);
 #endif
         s->root_level             = 0;
-        s->simpdb_assigns         = 0;
-        s->simpdb_props           = 0;
         s->random_seed            = 91648253;
         s->progress_estimate      = 0;
         s->verbosity              = 0;
@@ -1664,9 +1581,12 @@ void sat_solver2_rollback( sat_solver2* s )
         s->stats.learnts_literals = 0;
         s->stats.tot_literals     = 0;
         // initialize clause pointers
-        s->hClausePivot   =  1;
-        s->hLearntPivot   =  1;
         s->hLearntLast    = -1; // the last learnt clause 
+        s->hProofLast     = -1; // the last proof ID
+        s->hClausePivot   =  1; // the pivot among clauses
+        s->hLearntPivot   =  1; // the pivot moang learned clauses
+        s->iVarPivot      =  0; // the pivot among the variables
+        s->iSimpPivot     =  0; // marker of unit-clauses
     }
 }
 
@@ -1717,10 +1637,10 @@ void sat_solver2_verify( sat_solver2* s )
             Counter++;
         }
     }
-    if ( Counter == 0 )
-        printf( "Verification passed.\n" );
-    else
+    if ( Counter != 0 )
         printf( "Verification failed!\n" );
+//    else
+//        printf( "Verification passed.\n" );
 }
 
 
@@ -1734,6 +1654,7 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim
     lit * i;
 
     s->hLearntLast = -1;
+    s->hProofLast = -1;
 
     // set the external limits
 //    s->nCalls++;
@@ -1750,27 +1671,6 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim
     if ( nInsLimitGlobal && (s->nInsLimit == 0 || s->nInsLimit > nInsLimitGlobal) )
         s->nInsLimit = nInsLimitGlobal;
 
-#ifndef SAT_USE_ANALYZE_FINAL
-
-    //printf("solve: "); printlits(begin, end); printf("\n");
-    for (i = begin; i < end; i++){
-        switch (var_value(s, *i)) {
-        case var1: // l_True: 
-            break;
-        case varX: // l_Undef
-            solver2_assume(s, *i);
-            if (solver2_propagate(s) == NULL)
-                break;
-            // fallthrough
-        case var0: // l_False 
-            solver2_canceluntil(s, 0);
-            return l_False;
-        }
-    }
-    s->root_level = solver2_dlevel(s);
-
-#endif
-
 /*
     // Perform assumptions:
     root_level = assumps.size();
@@ -1803,7 +1703,6 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim
     assert(root_level == decisionLevel());
 */
 
-#ifdef SAT_USE_ANALYZE_FINAL
     // Perform assumptions:
     s->root_level = end - begin;
     for ( i = begin; i < end; i++ )
@@ -1822,6 +1721,7 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim
             }
             else
             {
+                assert( 0 );
                 proof_id = -1; // the only case when ProofId is not assigned (conflicting assumptions)
                 veci_resize(&s->conf_final,0);
                 veci_push(&s->conf_final, lit_neg(p));
@@ -1829,7 +1729,8 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim
                 if (var_level(s, lit_var(p)) > 0) 
                     veci_push(&s->conf_final, p);
             }
-            solver2_record(s, &s->conf_final, proof_id, 1);
+//            solver2_record(s, &s->conf_final, proof_id, 1);
+            s->hProofLast = proof_id;
             solver2_canceluntil(s, 0);
             return l_False; 
         }
@@ -1839,14 +1740,14 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim
             if (confl != NULL){
                 proof_id = solver2_analyze_final(s, confl, 0);
                 assert(s->conf_final.size > 0);
+//                solver2_record(s,&s->conf_final, proof_id, 1);
+                s->hProofLast = proof_id;
                 solver2_canceluntil(s, 0);
-                solver2_record(s,&s->conf_final, proof_id, 1);
                 return l_False; 
             }
         }
     }
     assert(s->root_level == solver2_dlevel(s));
-#endif
 
     if (s->verbosity >= 1){
         printf("==================================[MINISAT]===================================\n");
@@ -1891,6 +1792,7 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim
         printf("==============================================================================\n");
 
     solver2_canceluntil(s,0);
+    assert( s->qhead == s->qtail );
 //    if ( status == l_True )
 //        sat_solver2_verify( s );
     return status;
diff --git a/src/sat/bsat/satSolver2.h b/src/sat/bsat/satSolver2.h
index 2c5f8bf4..63fc9755 100644
--- a/src/sat/bsat/satSolver2.h
+++ b/src/sat/bsat/satSolver2.h
@@ -85,8 +85,6 @@ struct sat_solver2_t
     int             qtail;          // Tail index of queue.
 
     int             root_level;     // Level of first proper decision.
-    int             simpdb_assigns; // Number of top-level assignments at last 'simplifyDB()'.
-    int             simpdb_props;   // Number of propagations before next 'simplifyDB()'.
     double          random_seed;
     double          progress_estimate;
     int             verbosity;      // Verbosity level. 0=silent, 1=some progress report, 2=everything    // activities
@@ -111,9 +109,10 @@ struct sat_solver2_t
     veci            clauses;        // clause memory
     veci            learnts;        // learnt memory
     veci*           wlists;         // watcher lists (for each literal)
+    int             hLearntLast;    // in proof-logging mode, the ID of the final conflict clause (conf_final)
+    int             hProofLast;     // in proof-logging mode, the ID of the final conflict clause (conf_final)
     int             hClausePivot;   // the pivot among problem clause
     int             hLearntPivot;   // the pivot among learned clause
-    int             hLearntLast;    // in proof-logging mode, the ID of the final conflict clause (conf_final)
     int             iVarPivot;      // the pivot among the variables
     int             iSimpPivot;     // marker of unit-clauses
 
@@ -247,10 +246,11 @@ static inline int sat_solver2_set_random(sat_solver2* s, int fNotUseRandom)
 
 static inline void sat_solver2_bookmark(sat_solver2* s)
 {
+    assert( s->qhead == s->qtail );
     s->hLearntPivot = veci_size(&s->learnts);
     s->hClausePivot = veci_size(&s->clauses);
     s->iVarPivot    = s->size;
-    s->iSimpPivot   = s->simpdb_assigns;
+    s->iSimpPivot   = s->qhead;
 }
 
 static inline int sat_solver2_add_const( sat_solver2 * pSat, int iVar, int fCompl, int fMark )