Reducing memory usage in proof-based abstraction.

7 files changed, 524 insertions, 85 deletions

diff --git a/src/aig/gia/giaAbsGla.c b/src/aig/gia/giaAbsGla.c
index 7654e44f..b8c13e38 100644
--- a/src/aig/gia/giaAbsGla.c
+++ b/src/aig/gia/giaAbsGla.c
@@ -74,6 +74,9 @@ struct Gla_Man_t_
     unsigned *     pObj2Obj;        // mapping of GIA obj into GLA obj
     int            nObjs;           // the number of objects
     int            nAbsOld;         // previous abstraction
+    int            nAbsNew;         // previous abstraction
+    int            nLrnOld;         // the number of bytes
+    int            nLrnNew;         // the number of bytes
     // other data
     int            nCexes;          // the number of counter-examples
     int            nObjAdded;       // total number of objects added
@@ -84,6 +87,8 @@ struct Gla_Man_t_
     Vec_Int_t *    vAddedNew;       // temporary array
     Vec_Int_t *    vObjCounts;      // object counters
     Vec_Int_t *    vCoreCounts;     // counts how many times each object appears in the core
+    Vec_Int_t *    vProofIds;       // counts how many times each object appears in the core
+    int            nProofIds;       // proof ID counter
     // refinement
     Vec_Int_t *    pvRefis;         // vectors of each object
     // refinement manager
@@ -1056,6 +1061,7 @@ Gla_Man_t * Gla_ManStart( Gia_Man_t * pGia0, Gia_ParVta_t * pPars )
     assert( pGia0->vGateClasses != 0 );
     p->pGia->vGateClasses = Vec_IntStart( Gia_ManObjNum(p->pGia) );
     p->vCoreCounts = Vec_IntStart( Gia_ManObjNum(p->pGia) );
+    p->vProofIds = Vec_IntAlloc(0);
     // update p->pCnf->vMapping, p->pCnf->pObj2Count, p->pCnf->pObj2Clause 
     // (here are not updating p->pCnf->pVarNums because it is not needed)
     vMappingNew = Vec_IntStart( Gia_ManObjNum(p->pGia) );
@@ -1318,6 +1324,7 @@ void Gla_ManStop( Gla_Man_t * p )
     Vec_IntFreeP( &p->vObjCounts );
     Vec_IntFreeP( &p->vAddedNew );
     Vec_IntFreeP( &p->vCoreCounts );
+    Vec_IntFreeP( &p->vProofIds );
     Vec_IntFreeP( &p->vTemp );
     Vec_IntFreeP( &p->vAbs );
     ABC_FREE( p->pvRefis );
@@ -1567,15 +1574,29 @@ void Gia_GlaAddToCounters( Gla_Man_t * p, Vec_Int_t * vCore )
 void Gia_GlaAddToAbs( Gla_Man_t * p, Vec_Int_t * vAbsAdd, int fCheck )
 {
     Gla_Obj_t * pGla;
-    int i;
+    int i, Counter = 0;
     Gla_ManForEachObjAbsVec( vAbsAdd, p, pGla, i )
     {
-        assert( !fCheck || pGla->fAbs == 0 );
+        if ( fCheck )
+        {
+            assert( pGla->fAbs == 0 );
+            if ( p->pSat->pPrf2 )
+                Vec_IntWriteEntry( p->vProofIds, Gla_ObjId(p, pGla), p->nProofIds++ );
+        }
         if ( pGla->fAbs )
             continue;
+
+        if ( !fCheck )
+        {
+            Counter++;
+//            printf( "%d ", Gla_ObjId(p, pGla) );
+        }
+
         pGla->fAbs = 1;
         Vec_IntPush( p->vAbs, Gla_ObjId(p, pGla) );
     }
+//    if ( Counter )
+//    printf( "  Total = %d\n", Counter );
 }
 void Gia_GlaAddTimeFrame( Gla_Man_t * p, int f )
 {
@@ -1635,7 +1656,7 @@ int Gla_ManGetOutLit( Gla_Man_t * p, int f )
 }
 Vec_Int_t * Gla_ManUnsatCore( Gla_Man_t * p, int f, sat_solver2 * pSat, int nConfMax, int fVerbose, int * piRetValue, int * pnConfls )
 {
-    Vec_Int_t * vCore;
+    Vec_Int_t * vCore = NULL;
     int nConfPrev = pSat->stats.conflicts;
     int RetValue, iLit = Gla_ManGetOutLit( p, f );
     clock_t clk = clock();
@@ -1675,6 +1696,8 @@ Vec_Int_t * Gla_ManUnsatCore( Gla_Man_t * p, int f, sat_solver2 * pSat, int nCon
     // derive the UNSAT core
     clk = clock();
     vCore = (Vec_Int_t *)Sat_ProofCore( pSat );
+    if ( vCore )
+        Vec_IntSort( vCore, 1 );
     if ( fVerbose )
     {
 //        Abc_Print( 1, "Core is %8d vars    (out of %8d).   ", Vec_IntSize(vCore), sat_solver2_nvars(pSat) );
@@ -1717,6 +1740,9 @@ void Gla_ManAbsPrintFrame( Gla_Man_t * p, int nCoreSize, int nFrames, int nConfl
 //    Abc_Print( 1, " %6d", nCoreSize > 0 ? nCoreSize : 0 ); 
     Abc_Print( 1, "%9.2f sec", 1.0*Time/CLOCKS_PER_SEC );
     Abc_Print( 1, "%5.1f GB", (sat_solver2_memory_proof(p->pSat) + sat_solver2_memory(p->pSat, 0)) / (1<<30) );
+//    Abc_PrintInt( p->nAbsNew );
+//    Abc_PrintInt( p->nLrnNew );
+//    Abc_Print( 1, "%4.1f MB", 4.0 * p->nLrnNew * Abc_BitWordNum(p->nAbsNew) / (1<<20) );
     Abc_Print( 1, "%s", nCoreSize > 0 ? "\n" : "\r" );
     fflush( stdout );
 }
@@ -1740,13 +1766,13 @@ void Gla_ManReportMemory( Gla_Man_t * p )
     memOth += Vec_IntCap(p->vTemp) * sizeof(int);
     memOth += Vec_IntCap(p->vAbs) * sizeof(int);
     memTot = memAig + memSat + memPro + memMap + memRef + memOth;
-    ABC_PRMP( "Memory: AIG   ", memAig, memTot );
-    ABC_PRMP( "Memory: SAT   ", memSat, memTot );
-    ABC_PRMP( "Memory: Proof ", memPro, memTot );
-    ABC_PRMP( "Memory: Map   ", memMap, memTot );
-    ABC_PRMP( "Memory: Refine", memRef, memTot );
-    ABC_PRMP( "Memory: Other ", memOth, memTot );
-    ABC_PRMP( "Memory: TOTAL ", memTot, memTot );
+    ABC_PRMP( "Memory: AIG      ", memAig, memTot );
+    ABC_PRMP( "Memory: SAT      ", memSat, memTot );
+    ABC_PRMP( "Memory: Proof    ", memPro, memTot );
+    ABC_PRMP( "Memory: Map      ", memMap, memTot );
+    ABC_PRMP( "Memory: Refine   ", memRef, memTot );
+    ABC_PRMP( "Memory: Other    ", memOth, memTot );
+    ABC_PRMP( "Memory: TOTAL    ", memTot, memTot );
 }
 
 
@@ -1830,7 +1856,7 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta )
 {
     extern int Gia_VtaPerformInt( Gia_Man_t * pAig, Gia_ParVta_t * pPars );
     Gla_Man_t * p;
-    Vec_Int_t * vCore, * vPPis;
+    Vec_Int_t * vPPis, * vCore;//, * vCore2 = NULL;
     Abc_Cex_t * pCex = NULL;
     int f, i, iPrev, nConfls, Status, nVarsOld, nCoreSize, fOneIsSent = 0, RetValue = -1;
     clock_t clk2, clk = clock();
@@ -1913,24 +1939,31 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta )
         Vec_IntClear( p->vAddedNew );
         p->nAbsOld = Vec_IntSize( p->vAbs );
         nVarsOld = p->nSatVars;
+        p->nLrnOld = sat_solver2_nlearnts( p->pSat );
 
         // iterate as long as there are counter-examples
+        p->nAbsNew = 0;
+        p->nLrnNew = 0;
         for ( i = 0; ; i++ )
         { 
             clk2 = clock();
             vCore = Gla_ManUnsatCore( p, f, p->pSat, pPars->nConfLimit, pPars->fVerbose, &Status, &nConfls );
-            assert( (vCore != NULL) == (Status == 1) );
+//            assert( (vCore != NULL) == (Status == 1) );
             if ( Status == -1 || (p->pSat->nRuntimeLimit && clock() > p->pSat->nRuntimeLimit) ) // resource limit is reached
             {
+                if ( p->pSat->pPrf2 )
+                    Prf_ManStopP( &p->pSat->pPrf2 );
                 if ( Gia_ManRegNum(p->pGia) > 1 ) // for comb cases, return the abstration
                     Gla_ManRollBack( p );
                 goto finish;
             }
-            if ( vCore != NULL )
+            if ( Status == 1 )
             {
+                if ( p->pSat->pPrf2 )
+                    Prf_ManStopP( &p->pSat->pPrf2 );
                 p->timeUnsat += clock() - clk2;
                 break;
-            }
+            } 
             p->timeSat += clock() - clk2;
             assert( Status == 0 );
             p->nCexes++;
@@ -1954,17 +1987,37 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta )
                 vPPis = Gla_ManRefinement( p );
                 if ( vPPis == NULL )
                 {
+                    if ( p->pSat->pPrf2 )
+                        Prf_ManStopP( &p->pSat->pPrf2 );
                     pCex = p->pGia->pCexSeq; p->pGia->pCexSeq = NULL;
                     break;
                 }
             } 
+            assert( pCex == NULL );
+
+            // start proof logging
+            if ( i == 0 )
+            {
+                assert( p->pSat->pPrf2 == NULL );
+                p->pSat->pPrf2 = Prf_ManAlloc();
+                if ( p->pSat->pPrf2 )
+                {
+                    p->nProofIds = 0;
+                    Vec_IntFill( p->vProofIds, Gia_ManObjNum(p->pGia), -1 );
+                    Prf_ManRestart( p->pSat->pPrf2, p->vProofIds, sat_solver2_nlearnts(p->pSat), Vec_IntSize(vPPis) );
+                }
+            }
+            else
+            {
+                // resize the proof logger
+                if ( p->pSat->pPrf2 )
+                    Prf_ManGrow( p->pSat->pPrf2, Vec_IntSize(p->vAbs) - p->nAbsOld + Vec_IntSize(vPPis) );
+            }
+
             Gia_GlaAddToAbs( p, vPPis, 1 );
             Gia_GlaAddOneSlice( p, f, vPPis );
             Vec_IntFree( vPPis );
 
-            p->timeCex += clock() - clk2;
-            if ( pCex != NULL )
-                goto finish;
             // print the result (do not count it towards change)
             if ( p->pPars->fVerbose )
             Gla_ManAbsPrintFrame( p, -1, f+1, sat_solver2_nconflicts(p->pSat)-nConflsBeg, i, clock() - clk );
@@ -1972,24 +2025,30 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta )
         if ( pCex != NULL )
             break;
         assert( Status == 1 );
+
         // valid core is obtained
-        nCoreSize = Vec_IntSize( vCore );
-        Gia_GlaAddToCounters( p, vCore );
+        nCoreSize = 1;
+        if ( vCore )
+        {
+            nCoreSize += Vec_IntSize( vCore );
+            Gia_GlaAddToCounters( p, vCore );
+        }
         if ( i == 0 )
         {
             p->pPars->nFramesNoChange++;
-            Vec_IntFree( vCore );
+            Vec_IntFreeP( &vCore );
         }
         else
         {
             p->pPars->nFramesNoChange = 0;
+            p->nAbsNew = Vec_IntSize( p->vAbs ) - p->nAbsOld;
+            p->nLrnNew = Abc_AbsInt( sat_solver2_nlearnts( p->pSat ) - p->nLrnOld );
             // update the SAT solver
             sat_solver2_rollback( p->pSat );
             // update storage
             Gla_ManRollBack( p );
             p->nSatVars = nVarsOld;
             // load this timeframe
-            Vec_IntSort( vCore, 1 );
             Gia_GlaAddToAbs( p, vCore, 0 );
             Gia_GlaAddOneSlice( p, f, vCore );
             Vec_IntFree( vCore );
@@ -1997,7 +2056,7 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta )
             clk2 = clock();
             vCore = Gla_ManUnsatCore( p, f, p->pSat, pPars->nConfLimit, p->pPars->fVerbose, &Status, &nConfls );
             p->timeUnsat += clock() - clk2;
-            assert( (vCore != NULL) == (Status == 1) );
+//            assert( (vCore != NULL) == (Status == 1) );
             Vec_IntFreeP( &vCore );
             if ( Status == -1 ) // resource limit is reached
                 break;
@@ -2046,10 +2105,10 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta )
     }
 finish:
     // analize the results
-    if ( p->pPars->fVerbose )
-        printf( "\n" );
     if ( pCex == NULL )
     {
+        if ( p->pPars->fVerbose && Status == -1 )
+            printf( "\n" );
         if ( pAig->vGateClasses != NULL )
             Abc_Print( 1, "Replacing the old abstraction by a new one.\n" );
         Vec_IntFreeP( &pAig->vGateClasses );
diff --git a/src/aig/gia/giaAbsGla2.c b/src/aig/gia/giaAbsGla2.c
index 7edacf3c..cf2dfb95 100644
--- a/src/aig/gia/giaAbsGla2.c
+++ b/src/aig/gia/giaAbsGla2.c
@@ -41,21 +41,22 @@ struct Ga2_Man_t_
     Gia_Man_t *    pGia;         // working AIG manager
     Gia_ParVta_t * pPars;        // parameters
     // markings 
-    int            nMarked;      // total number of marked nodes and flops
     Vec_Ptr_t *    vCnfs;        // for each object: CNF0, CNF1
     // abstraction
-    Vec_Int_t *    vIds;         // abstraction ID for each object
+    Vec_Int_t *    vIds;         // abstraction ID for each GIA object
     Vec_Int_t *    vAbs;         // array of abstracted objects
-    Vec_Int_t *    vValues;      // array of objects with SAT numbers assigned
+    Vec_Int_t *    vValues;      // array of objects with abstraction ID assigned
+    Vec_Int_t *    vProofIds;    // proof IDs for these objects (1-to-1 with vValues)
+    int            nProofIds;    // the counter of proof IDs
     int            LimAbs;       // limit value for starting abstraction objects
     int            LimPpi;       // limit value for starting PPI objects
+    int            nMarked;      // total number of marked nodes and flops
     // refinement
     Rnm_Man_t *    pRnm;         // refinement manager
     // SAT solver and variables
     Vec_Ptr_t *    vId2Lit;      // mapping, for each timeframe, of object ID into SAT literal
     sat_solver2 *  pSat;         // incremental SAT solver
     int            nSatVars;     // the number of SAT variables
-    int            nProofIds;    // the counter of proof IDs
     // temporaries
     Vec_Int_t *    vLits;
     Vec_Int_t *    vIsopMem;
@@ -356,7 +357,9 @@ Ga2_Man_t * Ga2_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars )
     p->vIds      = Vec_IntStart( Gia_ManObjNum(pGia) );
     p->vAbs      = Vec_IntAlloc( 1000 );
     p->vValues   = Vec_IntAlloc( 1000 );
+    p->vProofIds = Vec_IntAlloc( 1000 );
     Vec_IntPush( p->vValues, -1 );
+    Vec_IntPush( p->vProofIds, -1 );
     // refinement
     p->pRnm      = Rnm_ManStart( pGia );
     // SAT solver and variables
@@ -380,17 +383,18 @@ void Ga2_ManReportMemory( Ga2_Man_t * p )
     memOth += Vec_IntMemory( p->vIds );
     memOth += Vec_IntMemory( p->vAbs );
     memOth += Vec_IntMemory( p->vValues );
+    memOth += Vec_IntMemory( p->vProofIds );
     memOth += Vec_IntMemory( p->vLits );
     memOth += Vec_IntMemory( p->vIsopMem );
     memOth += 336450 + (sizeof(char) + sizeof(char*)) * 65536;
     memTot = memAig + memSat + memPro + memMap + memRef + memOth;
-    ABC_PRMP( "Memory: AIG   ", memAig, memTot );
-    ABC_PRMP( "Memory: SAT   ", memSat, memTot );
-    ABC_PRMP( "Memory: Proof ", memPro, memTot );
-    ABC_PRMP( "Memory: Map   ", memMap, memTot );
-    ABC_PRMP( "Memory: Refine", memRef, memTot );
-    ABC_PRMP( "Memory: Other ", memOth, memTot );
-    ABC_PRMP( "Memory: TOTAL ", memTot, memTot );
+    ABC_PRMP( "Memory: AIG      ", memAig, memTot );
+    ABC_PRMP( "Memory: SAT      ", memSat, memTot );
+    ABC_PRMP( "Memory: Proof    ", memPro, memTot );
+    ABC_PRMP( "Memory: Map      ", memMap, memTot );
+    ABC_PRMP( "Memory: Refine   ", memRef, memTot );
+    ABC_PRMP( "Memory: Other    ", memOth, memTot );
+    ABC_PRMP( "Memory: TOTAL    ", memTot, memTot );
 }
 void Ga2_ManStop( Ga2_Man_t * p )
 {
@@ -404,6 +408,7 @@ void Ga2_ManStop( Ga2_Man_t * p )
     Vec_VecFree( (Vec_Vec_t *)p->vId2Lit );
     Vec_IntFree( p->vIds );
     Vec_IntFree( p->vAbs );
+    Vec_IntFree( p->vProofIds );
     Vec_IntFree( p->vValues );
     Vec_IntFree( p->vLits );
     Vec_IntFree( p->vIsopMem );
@@ -610,17 +615,19 @@ static inline void Ga2_ManCnfAddStatic( Ga2_Man_t * p, Vec_Int_t * vCnf0, Vec_In
   SeeAlso     []
 
 ***********************************************************************/
-void Ga2_ManSetupNode( Ga2_Man_t * p, Gia_Obj_t * pObj, int fAbs )
+void Ga2_ManSetupNode( Ga2_Man_t * p, Gia_Obj_t * pObj, int fAbs, int ProofId )
 {
     unsigned uTruth;
     int nLeaves;
     assert( pObj->fPhase );
     assert( Vec_PtrSize(p->vCnfs) == 2 * Vec_IntSize(p->vValues) );
+    assert( Vec_IntSize(p->vProofIds) == Vec_IntSize(p->vValues) );
     // assign abstraction ID to the node
     if ( Ga2_ObjId(p,pObj) == 0 )
     {
         Ga2_ObjSetId( p, pObj, Vec_IntSize(p->vValues) );
         Vec_IntPush( p->vValues, Gia_ObjId(p->pGia, pObj) );
+        Vec_IntPush( p->vProofIds, ProofId );
         Vec_PtrPush( p->vCnfs, NULL );
         Vec_PtrPush( p->vCnfs, NULL );
     }
@@ -629,14 +636,14 @@ void Ga2_ManSetupNode( Ga2_Man_t * p, Gia_Obj_t * pObj, int fAbs )
         return;
     // compute parameters
     nLeaves = Ga2_ObjLeaveNum(p->pGia, pObj);
-    uTruth = Ga2_ObjTruth( p->pGia, pObj );
     // create CNF for pos/neg phases
+    uTruth = Ga2_ObjTruth( p->pGia, pObj );
     Vec_PtrWriteEntry( p->vCnfs, 2 * Ga2_ObjId(p,pObj),     Ga2_ManCnfCompute(uTruth, nLeaves, p->vIsopMem) );    
     uTruth = (~uTruth) & Abc_InfoMask( (1 << nLeaves) );
     Vec_PtrWriteEntry( p->vCnfs, 2 * Ga2_ObjId(p,pObj) + 1, Ga2_ManCnfCompute(uTruth, nLeaves, p->vIsopMem) );
 }
 
-void Ga2_ManAddToAbs( Ga2_Man_t * p, Vec_Int_t * vToAdd )
+void Ga2_ManAddToAbs( Ga2_Man_t * p, Vec_Int_t * vToAdd, int ProofId )
 {
     Vec_Int_t * vLeaves, * vMap;
     Gia_Obj_t * pObj, * pFanin;
@@ -644,15 +651,16 @@ void Ga2_ManAddToAbs( Ga2_Man_t * p, Vec_Int_t * vToAdd )
     // add abstraction objects
     Gia_ManForEachObjVec( vToAdd, p->pGia, pObj, i )
     {
-        Ga2_ManSetupNode( p, pObj, 1 );
+        Ga2_ManSetupNode( p, pObj, 1, ProofId );
         Vec_IntPush( p->vAbs, Gia_ObjId(p->pGia, pObj) );
+        Vec_IntPush( p->vProofIds, ProofId );
     }
     // add PPI objects
     Gia_ManForEachObjVec( vToAdd, p->pGia, pObj, i )
     {
         vLeaves = Ga2_ObjLeaves( p->pGia, pObj );
         Gia_ManForEachObjVec( vLeaves, p->pGia, pFanin, k )
-            Ga2_ManSetupNode( p, pObj, 0 );
+            Ga2_ManSetupNode( p, pObj, 0, -1 );
     }
     // clean mapping in the timeframes
     Vec_PtrForEachEntry( Vec_Int_t *, p->vId2Lit, vMap, i )
@@ -666,8 +674,12 @@ void Ga2_ManAddToAbs( Ga2_Man_t * p, Vec_Int_t * vToAdd )
         Vec_IntClear( p->vLits );
         Gia_ManForEachObjVec( vLeaves, p->pGia, pFanin, k )
             Vec_IntPush( p->vLits, Ga2_ObjFindOrAddLit( p, pFanin, f ) );
-        Ga2_ManCnfAddStatic( p, Ga2_ObjCnf0(p, pObj), Ga2_ObjCnf1(p, pObj), Vec_IntArray(p->vLits), iLitOut, p->nProofIds + i );
+        Ga2_ManCnfAddStatic( p, Ga2_ObjCnf0(p, pObj), Ga2_ObjCnf1(p, pObj), Vec_IntArray(p->vLits), iLitOut, Vec_IntEntry(p->vProofIds, Ga2_ObjId(p, pObj)) );
     }
+    // verify -- if ProofId == -1, all proof IDs should be the same
+    if ( ProofId == -1 )
+        Vec_IntForEachEntry( p->vProofIds, k, i )
+            assert( k == -1 );
 }
 
 void Ga2_ManAddAbsClauses( Ga2_Man_t * p, int f )
@@ -679,11 +691,11 @@ void Ga2_ManAddAbsClauses( Ga2_Man_t * p, int f )
     {
         if ( i < p->LimAbs )
             continue;
-        iLitOut =  Ga2_ObjFindOrAddLit( p, pObj, f );
         vLeaves = Ga2_ObjLeaves( p->pGia, pObj );
         Vec_IntClear( p->vLits );
         Gia_ManForEachObjVec( vLeaves, p->pGia, pFanin, k )
             Vec_IntPush( p->vLits, Ga2_ObjFindOrAddLit( p, pFanin, f ) );
+        iLitOut =  Ga2_ObjFindOrAddLit( p, pObj, f );
         Ga2_ManCnfAddStatic( p, Ga2_ObjCnf0(p, pObj), Ga2_ObjCnf1(p, pObj), Vec_IntArray(p->vLits), iLitOut, i - p->LimAbs );
     }
 }
@@ -717,6 +729,7 @@ void Ga2_ManShrinkAbs( Ga2_Man_t * p, int nAbs, int nValues )
         Ga2_ObjSetId( p, pObj, 0 );
     }
     Vec_IntShrink( p->vValues, nValues );
+    Vec_IntShrink( p->vProofIds, nValues );
     Vec_PtrShrink( p->vCnfs, 2 * nValues );
     // clean mapping into timeframes
     Vec_PtrForEachEntry( Vec_Int_t *, p->vId2Lit, vMap, i )
@@ -775,6 +788,7 @@ void Ga2_ManRestart( Ga2_Man_t * p )
     Vec_Int_t * vToAdd;
     assert( p->pGia != NULL && p->pGia->vGateClasses != NULL );
     assert( Gia_ManPi(p->pGia, 0)->fPhase ); // marks are set
+    p->nProofIds = 0;
     // clear mappings from objects
     Ga2_ManShrinkAbs( p, 0, 1 );
     // clear SAT variable numbers (begin with 1)
@@ -783,11 +797,10 @@ void Ga2_ManRestart( Ga2_Man_t * p )
     p->nSatVars  = 1;
     // start abstraction
     vToAdd = Ga2_ManAbsDerive( p->pGia );
-    Ga2_ManAddToAbs( p, vToAdd );
+    Ga2_ManAddToAbs( p, vToAdd, -1 );
     Vec_IntFree( vToAdd );
     p->LimAbs = Vec_IntSize(p->vAbs) + 1;
     p->LimPpi = Vec_IntSize(p->vValues);
-    p->nProofIds = 0;
     // set runtime limit
     if ( p->pPars->nTimeOut )
         sat_solver2_set_runtime_limit( p->pSat, p->pPars->nTimeOut * CLOCKS_PER_SEC + p->timeStart );
@@ -1069,7 +1082,7 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
         for ( f = 0; !pPars->nFramesMax || f < pPars->nFramesMax; f++ )
         {
             p->pPars->iFrame = f;
-            // add abstraction clauses
+            // add static clauses to this timeframe
             Ga2_ManAddAbsClauses( p, f );
             // get the output literal
             Lit = Ga2_ManUnroll_rec( p, Gia_ManPo(pAig,0), f );
@@ -1087,7 +1100,7 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
                     p->timeCex += clock() - clk;
                     if ( vPPis == NULL )
                         goto finish;
-                    Ga2_ManAddToAbs( p, vPPis );
+                    Ga2_ManAddToAbs( p, vPPis, p->nProofIds++ );
                     Vec_IntFree( vPPis );
                     // verify
                     if ( Vec_IntCheckUnique(p->vAbs) )
@@ -1103,8 +1116,9 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
                 // derive UNSAT core
                 vCore = (Vec_Int_t *)Sat_ProofCore( p->pSat );
                 Ga2_ManShrinkAbs( p, nAbs, nValues );
-                Ga2_ManAddToAbs( p, vCore );
+                Ga2_ManAddToAbs( p, vCore, -1 );
                 Vec_IntFree( vCore );
+                p->nProofIds = 0;
                 // remember current limits
                 nAbs    = Vec_IntSize(p->vAbs);
                 nValues = Vec_IntSize(p->vValues);
diff --git a/src/aig/gia/giaAbsVta.c b/src/aig/gia/giaAbsVta.c
index 69f40af5..31158e9d 100644
--- a/src/aig/gia/giaAbsVta.c
+++ b/src/aig/gia/giaAbsVta.c
@@ -1035,6 +1035,7 @@ Vta_Man_t * Vga_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars )
     // other data
     p->vCores      = Vec_PtrAlloc( 100 );
     p->pSat        = sat_solver2_new();
+    p->pSat->pPrf1 = Vec_SetAlloc( 20 );
 //    p->pSat->fVerbose = p->pPars->fVerbose;
 //    sat_solver2_set_learntmax( p->pSat, pPars->nLearnedMax );
     p->pSat->nLearntStart = p->pPars->nLearnedStart;
@@ -1499,12 +1500,12 @@ void Gia_VtaPrintMemory( Vta_Man_t * p )
     memOth += Vec_VecMemoryInt( (Vec_Vec_t *)p->vCores );
     memOth += Vec_IntCap(p->vAddedNew) * sizeof(int);
     memTot = memAig + memSat + memPro + memMap + memOth;
-    ABC_PRMP( "Memory: AIG  ", memAig, memTot );
-    ABC_PRMP( "Memory: SAT  ", memSat, memTot );
-    ABC_PRMP( "Memory: Proof", memPro, memTot );
-    ABC_PRMP( "Memory: Map  ", memMap, memTot );
-    ABC_PRMP( "Memory: Other", memOth, memTot );
-    ABC_PRMP( "Memory: TOTAL", memTot, memTot );
+    ABC_PRMP( "Memory: AIG     ", memAig, memTot );
+    ABC_PRMP( "Memory: SAT     ", memSat, memTot );
+    ABC_PRMP( "Memory: Proof   ", memPro, memTot );
+    ABC_PRMP( "Memory: Map     ", memMap, memTot );
+    ABC_PRMP( "Memory: Other   ", memOth, memTot );
+    ABC_PRMP( "Memory: TOTAL   ", memTot, memTot );
 }
 
 
@@ -1694,10 +1695,10 @@ int Gia_VtaPerformInt( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
     }
 finish:
     // analize the results
-    if ( p->pPars->fVerbose )
-        printf( "\n" );
     if ( pCex == NULL )
     {
+        if ( p->pPars->fVerbose && Status == -1 )
+            printf( "\n" );
         if ( Vec_PtrSize(p->vCores) == 0 )
             Abc_Print( 1, "Abstraction is not produced because first frame is not solved.  " );
         else
diff --git a/src/misc/vec/vecSet.h b/src/misc/vec/vecSet.h
index c96636f8..40318b48 100644
--- a/src/misc/vec/vecSet.h
+++ b/src/misc/vec/vecSet.h
@@ -168,12 +168,14 @@ static inline void Vec_SetRestart( Vec_Set_t * p )
 static inline void Vec_SetFree_( Vec_Set_t * p )
 {
     int i;
+    if ( p == NULL ) return;
     for ( i = 0; i < p->nPagesAlloc; i++ )
         ABC_FREE( p->pPages[i] );
     ABC_FREE( p->pPages );
 }
 static inline void Vec_SetFree( Vec_Set_t * p )
 {
+    if ( p == NULL ) return;
     Vec_SetFree_( p );
     ABC_FREE( p );
 }
diff --git a/src/sat/bsat/satProof2.h b/src/sat/bsat/satProof2.h
new file mode 100644
index 00000000..82ed9264
--- /dev/null
+++ b/src/sat/bsat/satProof2.h
@@ -0,0 +1,326 @@
+/**CFile****************************************************************
+
+  FileName    [satProof2.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [SAT solver.]
+
+  Synopsis    [Proof logging.]
+
+  Author      [Alan Mishchenko <alanmi@eecs.berkeley.edu>]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - January 1, 2004.]
+
+  Revision    [$Id: satProof2.h,v 1.0 2004/01/01 1:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef ABC__sat__bsat__satProof2_h
+#define ABC__sat__bsat__satProof2_h
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+#include "misc/vec/vec.h"
+
+ABC_NAMESPACE_HEADER_START
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                    STRUCTURE DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Prf_Man_t_ Prf_Man_t;
+struct Prf_Man_t_ 
+{
+    int             iFirst;    // first learned clause with proof
+    int             iFirst2;   // first learned clause with proof
+    int             nWords;    // the number of proof words
+    word *          pInfo;     // pointer to the current proof
+    Vec_Wrd_t *     vInfo;     // proof information
+    Vec_Int_t *     vSaved;    // IDs of saved clauses
+    Vec_Int_t *     vId2Pr;    // mapping proof IDs of problem clauses into bitshifts (user's array)
+};
+
+////////////////////////////////////////////////////////////////////////
+///                       GLOBAL VARIABLES                           ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                       MACRO DEFINITIONS                          ///
+////////////////////////////////////////////////////////////////////////
+
+static inline int    Prf_BitWordNum( int nWidth )                { return (nWidth >> 6) + ((nWidth & 63) > 0);                           }
+static inline int    Prf_ManSize( Prf_Man_t * p )                { return Vec_WrdSize( p->vInfo ) / p->nWords;                           }
+static inline void   Prf_ManClearNewInfo( Prf_Man_t * p )        { int w; for ( w = 0; w < p->nWords; w++ ) Vec_WrdPush( p->vInfo, 0 );  }
+static inline word * Prf_ManClauseInfo( Prf_Man_t * p, int Id )  { return Vec_WrdEntryP( p->vInfo, Id * p->nWords );                     }
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DECLARATIONS                        ///
+////////////////////////////////////////////////////////////////////////
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Prf_Man_t * Prf_ManAlloc()
+{
+    Prf_Man_t * p;
+    p = ABC_CALLOC( Prf_Man_t, 1 );
+    p->iFirst  = -1;
+    p->iFirst2 = -1;
+    p->vInfo   = Vec_WrdAlloc( 1000 );
+    p->vSaved  = Vec_IntAlloc( 1000 );
+    return p;
+}
+static inline void Prf_ManStop( Prf_Man_t * p )
+{
+    if ( p == NULL )
+        return;
+    Vec_IntFree( p->vSaved );
+    Vec_WrdFree( p->vInfo );
+    ABC_FREE( p );
+}
+static inline void Prf_ManStopP( Prf_Man_t ** p )
+{
+    Prf_ManStop( *p );
+    *p = NULL;
+}
+static inline double Prf_ManMemory( Prf_Man_t * p )
+{
+    return Vec_WrdMemory(p->vInfo) + Vec_IntMemory(p->vSaved) + sizeof(Prf_Man_t);
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Prf_ManRestart( Prf_Man_t * p, Vec_Int_t * vId2Pr, int iFirst, int nWidth )
+{
+    assert( p->iFirst == -1 );
+    p->iFirst = iFirst;
+    p->nWords = Prf_BitWordNum( nWidth );
+    p->vId2Pr = vId2Pr;
+    p->pInfo  = NULL;
+    Vec_WrdClear( p->vInfo );
+}
+static inline void Prf_ManGrow( Prf_Man_t * p, int nWidth )
+{
+    Vec_Wrd_t * vInfoNew;
+    int i, w, nSize, nWordsNew;
+    assert( p->iFirst >= 0 );
+    assert( p->pInfo == NULL );
+    if ( nWidth < 64 * p->nWords )
+        return;
+    // get word count after resizing
+    nWordsNew = Abc_MaxInt( Prf_BitWordNum(nWidth), 2 * p->nWords );
+    // remap the entries
+    nSize = Prf_ManSize( p );
+    vInfoNew = Vec_WrdAlloc( (nSize + 1000) * nWordsNew );
+    for ( i = 0; i < nSize; i++ )
+    {
+        p->pInfo = Prf_ManClauseInfo( p, i );
+        for ( w = 0; w < p->nWords; w++ )
+            Vec_WrdPush( vInfoNew, p->pInfo[w] );
+        for ( ; w < nWordsNew; w++ )
+            Vec_WrdPush( vInfoNew, 0 );
+    }
+    Vec_WrdFree( p->vInfo );
+    p->vInfo = vInfoNew;
+    p->nWords = nWordsNew;
+    p->pInfo = NULL;
+
+}
+static inline void Prf_ManShrink( Prf_Man_t * p, int iClause )
+{
+    assert( p->iFirst >= 0 );
+    assert( iClause - p->iFirst >= 0 );
+    assert( iClause - p->iFirst < Prf_ManSize(p) ); 
+    Vec_WrdShrink( p->vInfo, (iClause - p->iFirst) * p->nWords );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Prf_ManAddSaved( Prf_Man_t * p, int i, int iNew )
+{
+    assert( p->iFirst >= 0 );
+    if ( i < p->iFirst )
+        return;
+    if ( Vec_IntSize(p->vSaved) == 0 )
+    {
+        assert( p->iFirst2 == -1 );
+        p->iFirst2 = iNew;
+    }
+    Vec_IntPush( p->vSaved, i );
+}
+static inline void Prf_ManCompact( Prf_Man_t * p, int iNew )
+{
+    int i, w, k = 0, Entry, nSize;
+    assert( p->iFirst >= 0 );
+    assert( p->pInfo == NULL );
+    nSize = Prf_ManSize( p );
+    Vec_IntForEachEntry( p->vSaved, Entry, i )
+    {
+        assert( Entry - p->iFirst >= 0 && Entry - p->iFirst < nSize );
+        p->pInfo = Prf_ManClauseInfo( p, Entry - p->iFirst );
+        for ( w = 0; w < p->nWords; w++ )
+            Vec_WrdWriteEntry( p->vInfo, k++, p->pInfo[w] );
+    }
+    Vec_WrdShrink( p->vInfo, k );
+    Vec_IntClear( p->vSaved );
+    p->pInfo = NULL;
+    // update first
+    if ( p->iFirst2 == -1 )
+        p->iFirst = iNew;
+    else
+        p->iFirst = p->iFirst2;
+    p->iFirst2 = -1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Prf_ManChainResolve( Prf_Man_t * p, clause * c )
+{
+    assert( p->iFirst >= 0 );
+    assert( p->pInfo != NULL );
+    // add to proof info
+    if ( c->lrn ) // learned clause
+    {
+        if ( clause_id(c) >= p->iFirst )
+        {
+            word * pProofStart;
+            int w;
+            assert( clause_id(c) - p->iFirst >= 0 );
+            assert( clause_id(c) - p->iFirst < Prf_ManSize(p) ); 
+            pProofStart = Prf_ManClauseInfo( p, clause_id(c) - p->iFirst );
+            for ( w = 0; w < p->nWords; w++ )
+                p->pInfo[w] |= pProofStart[w];
+        }
+    }
+    else // problem clause
+    {  
+        if ( clause_id(c) ) // has proof ID
+        {
+            int Entry;
+            if ( p->vId2Pr == NULL )
+                Entry = clause_id(c);
+            else
+                Entry = Vec_IntEntry( p->vId2Pr, clause_id(c) );
+            if ( Entry >= 0 )
+            {
+                assert( Entry < 64 * p->nWords );
+                Abc_InfoSetBit( (unsigned *)p->pInfo, Entry );
+            }
+        }
+    }
+}
+static inline void Prf_ManChainStart( Prf_Man_t * p, clause * c )
+{
+    assert( p->iFirst >= 0 );
+    // prepare info for new clause
+    Prf_ManClearNewInfo( p );
+    // get pointer to the proof
+    assert( p->pInfo == NULL );
+    p->pInfo = Prf_ManClauseInfo( p, Prf_ManSize(p)-1 );
+    // add to proof info
+    Prf_ManChainResolve( p, c );
+}
+static inline int Prf_ManChainStop( Prf_Man_t * p )
+{
+    assert( p->pInfo != NULL );
+    p->pInfo = NULL;
+    return 0;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Vec_Int_t * Prf_ManUnsatCore( Prf_Man_t * p )
+{
+    Vec_Int_t * vCore;
+    int i, Entry;
+    assert( p->iFirst >= 0 );
+    assert( p->pInfo == NULL );
+    vCore = Vec_IntAlloc( 64 * p->nWords );
+    p->pInfo = Prf_ManClauseInfo( p, Prf_ManSize(p)-1 );
+    if ( p->vId2Pr == NULL )
+    {
+        for ( i = 0; i < 64 * p->nWords; i++ )
+            if ( Abc_InfoHasBit( (unsigned *)p->pInfo, i ) )
+                Vec_IntPush( vCore, i );
+    }
+    else
+    {
+        Vec_IntForEachEntry( p->vId2Pr, Entry, i )
+        {
+            if ( Entry < 0 )
+                continue;
+            assert( Entry < 64 * p->nWords );
+            if ( Abc_InfoHasBit( (unsigned *)p->pInfo, Entry ) )
+                Vec_IntPush( vCore, i );
+        }
+    }
+    p->pInfo = NULL;
+    Vec_IntSort( vCore, 1 );
+    return vCore;
+}
+
+
+
+ABC_NAMESPACE_HEADER_END
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c
index b84f5a5f..6662eca5 100644
--- a/src/sat/bsat/satSolver2.c
+++ b/src/sat/bsat/satSolver2.c
@@ -161,7 +161,11 @@ static inline veci*   solver2_wlist(sat_solver2* s, lit l) { return &s->wlists[l
 
 static inline void proof_chain_start( sat_solver2* s, clause* c )
 {
-    if ( s->fProofLogging )
+    if ( !s->fProofLogging )
+        return;
+    if ( s->pPrf2 )
+        Prf_ManChainStart( s->pPrf2, c );
+    if ( s->pPrf1 )
     {
         int ProofId = clause2_proofid(s, c, 0);
         assert( (ProofId >> 2) > 0 );
@@ -174,7 +178,14 @@ static inline void proof_chain_start( sat_solver2* s, clause* c )
 
 static inline void proof_chain_resolve( sat_solver2* s, clause* cls, int Var )
 {
-    if ( s->fProofLogging )
+    if ( !s->fProofLogging )
+        return;
+    if ( s->pPrf2 )
+    {
+        clause* c = cls ? cls : var_unit_clause( s, Var );
+        Prf_ManChainResolve( s->pPrf2, c );
+    }
+    if ( s->pPrf1 )
     {
         clause* c = cls ? cls : var_unit_clause( s, Var );
         int ProofId = clause2_proofid(s, c, var_is_partA(s,Var));
@@ -185,11 +196,15 @@ static inline void proof_chain_resolve( sat_solver2* s, clause* cls, int Var )
 
 static inline int proof_chain_stop( sat_solver2* s )
 {
-    if ( s->fProofLogging )
+    if ( !s->fProofLogging )
+        return 0;
+    if ( s->pPrf2 )
+        Prf_ManChainStop( s->pPrf2 );
+    if ( s->pPrf1 )
     {
         extern void Proof_ClauseSetEnts( Vec_Set_t* p, int h, int nEnts );
-        int h = Vec_SetAppend( &s->Proofs, veci_begin(&s->temp_proof), veci_size(&s->temp_proof) );
-        Proof_ClauseSetEnts( &s->Proofs, h, veci_size(&s->temp_proof) - 2 );
+        int h = Vec_SetAppend( s->pPrf1, veci_begin(&s->temp_proof), veci_size(&s->temp_proof) );
+        Proof_ClauseSetEnts( s->pPrf1, h, veci_size(&s->temp_proof) - 2 );
         return h;
     }
     return 0;
@@ -371,7 +386,7 @@ static inline int sat_clause_compute_lbd( sat_solver2* s, clause* c )
     return lbd;
 }
 
-static int clause2_create_new(sat_solver2* s, lit* begin, lit* end, int learnt, int proof_id)
+static int clause2_create_new(sat_solver2* s, lit* begin, lit* end, int learnt, int proof_id )
 {
     clause* c;
     int h, size = end - begin;
@@ -385,11 +400,11 @@ static int clause2_create_new(sat_solver2* s, lit* begin, lit* end, int learnt,
     c = clause2_read( s, h );
     if (learnt)
     {
-        if ( s->fProofLogging )
+        if ( s->pPrf1 )
             assert( proof_id );
         c->lbd = sat_clause_compute_lbd( s, c );
         assert( clause_id(c) == veci_size(&s->act_clas) );
-        if ( proof_id )
+        if ( s->pPrf1 )
             veci_push(&s->claProofs, proof_id);
 //        veci_push(&s->act_clas, (1<<10));
         veci_push(&s->act_clas, 0);
@@ -674,7 +689,8 @@ static int solver2_lit_removable(sat_solver2* s, int x)
     while (veci_size(&s->stack))
     {
         x = veci_pop(&s->stack);
-        if ( s->fProofLogging ){
+        if ( s->fProofLogging )
+        {
             if ( x & 1 ){
                 if ( var_tag(s,x >> 1) & 1 )
                     veci_push(&s->min_lit_order, x >> 1 );
@@ -910,7 +926,8 @@ clause* solver2_propagate(sat_solver2* s)
 
                 // Did not find watch -- clause is unit under assignment:
                 Lit = lits[0];
-                if (s->fProofLogging && solver2_dlevel(s) == 0){
+                if ( s->fProofLogging && solver2_dlevel(s) == 0 )
+                {
                     int k, x, proof_id, Cid, Var = lit_var(Lit);
                     int fLitIsFalse = (var_value(s, Var) == !lit_sign(Lit));
                     // Log production of top-level unit clause:
@@ -990,7 +1007,8 @@ static lbool solver2_search(sat_solver2* s, ABC_INT64_T nof_conflicts)
             s->stats.conflicts++; conflictC++;
             if (solver2_dlevel(s) <= s->root_level){
                 proof_id = solver2_analyze_final(s, confl, 0);
-                assert( proof_id > 0 );
+                if ( s->pPrf1 )
+                    assert( proof_id > 0 );
                 s->hProofLast = proof_id;
                 veci_delete(&learnt_clause);
                 return l_False;
@@ -1112,12 +1130,11 @@ sat_solver2* sat_solver2_new(void)
     veci_new(&s->min_lit_order);
     veci_new(&s->min_step_order);
 //    veci_new(&s->learnt_live);
-
     Sat_MemAlloc_( &s->Mem, 14 );
     veci_new(&s->act_clas);  
+    // proof-logging
     veci_new(&s->claProofs);
-    if ( s->fProofLogging )
-        Vec_SetAlloc_( &s->Proofs, 20 );
+//    s->pPrf1 = Vec_SetAlloc( 20 );
 
     // initialize clause pointers
     s->hLearntLast            = -1; // the last learnt clause 
@@ -1218,7 +1235,8 @@ void sat_solver2_delete(sat_solver2* s)
 //    veci_delete(&s->lrns);
     Sat_MemFree_( &s->Mem );
 //    veci_delete(&s->proofs);
-    Vec_SetFree_( &s->Proofs );
+    Vec_SetFree( s->pPrf1 );
+    Prf_ManStop( s->pPrf2 );
 
     // delete arrays
     if (s->vi != 0){
@@ -1424,7 +1442,7 @@ void sat_solver2_reducedb(sat_solver2* s)
 
     // mark learned clauses to remove
     Counter = j = 0;
-    pClaProofs = s->fProofLogging ? veci_begin(&s->claProofs) : NULL;
+    pClaProofs = veci_size(&s->claProofs) ? veci_begin(&s->claProofs) : NULL;
     Sat_MemForEachLearned( pMem, c, i, k )
     {
         assert( c->mark == 0 );
@@ -1432,7 +1450,9 @@ void sat_solver2_reducedb(sat_solver2* s)
         {
             pSortValues[j] = pSortValues[clause_id(c)];
             if ( pClaProofs ) 
-            pClaProofs[j] = pClaProofs[clause_id(c)];
+                pClaProofs[j] = pClaProofs[clause_id(c)];
+            if ( s->pPrf2 )
+                Prf_ManAddSaved( s->pPrf2, clause_id(c), j );
             j++;
         }
         else // delete
@@ -1443,13 +1463,15 @@ void sat_solver2_reducedb(sat_solver2* s)
         }
     }
     ABC_FREE( pSortValues );
+    if ( s->pPrf2 )
+        Prf_ManCompact( s->pPrf2, j );
 //    if ( j == nLearnedOld )
 //        return;
 
     assert( s->stats.learnts == (unsigned)j );
     assert( Counter == nLearnedOld );
     veci_resize(&s->act_clas,j);
-    if ( s->fProofLogging )
+    if ( veci_size(&s->claProofs) )
         veci_resize(&s->claProofs,j);
 
     // update ID of each clause to be its new handle
@@ -1508,8 +1530,8 @@ void sat_solver2_reducedb(sat_solver2* s)
     assert( Counter == (int)s->stats.learnts );
 
     // compact proof (compacts 'proofs' and update 'claProofs')
-    if ( s->fProofLogging )
-        s->hProofPivot = Sat_ProofReduce( &s->Proofs, &s->claProofs, s->hProofPivot );
+    if ( s->pPrf1 )
+        s->hProofPivot = Sat_ProofReduce( s->pPrf1, &s->claProofs, s->hProofPivot );
 
 
     // report the results
@@ -1531,7 +1553,7 @@ void sat_solver2_rollback( sat_solver2* s )
     Count++;
     assert( s->iVarPivot >= 0 && s->iVarPivot <= s->size );
     assert( s->iTrailPivot >= 0 && s->iTrailPivot <= s->qtail );
-    assert( s->hProofPivot >= 1 && s->hProofPivot <= Vec_SetHandCurrent(&s->Proofs) );
+    assert( s->pPrf1 == NULL || (s->hProofPivot >= 1 && s->hProofPivot <= Vec_SetHandCurrent(s->pPrf1)) );
     // reset implication queue
     solver2_canceluntil_rollback( s, s->iTrailPivot );
     // update order 
@@ -1568,14 +1590,17 @@ void sat_solver2_rollback( sat_solver2* s )
 
     // resize learned arrays
     veci_resize(&s->act_clas,  s->stats.learnts);
-    if ( s->fProofLogging ) 
+    if ( s->pPrf1 ) 
     {
         veci_resize(&s->claProofs, s->stats.learnts);
 //        Vec_SetShrink(&s->Proofs, s->hProofPivot); 
         // some weird bug here, which shows only on 64-bits!
         // temporarily, perform more general proof reduction
-        Sat_ProofReduce( &s->Proofs, &s->claProofs, s->hProofPivot );
+        Sat_ProofReduce( s->pPrf1, &s->claProofs, s->hProofPivot );
     }
+    assert( s->pPrf2 == NULL );
+//    if ( s->pPrf2 )
+//        Prf_ManShrink( s->pPrf2, s->stats.learnts );
 
     // initialize other vars
     s->size = s->iVarPivot;
@@ -1641,8 +1666,6 @@ double sat_solver2_memory( sat_solver2* s, int fAll )
 #else
     Mem += s->cap * sizeof(unsigned); // ABC_FREE(s->activity );
 #endif
-//    if ( s->factors )
-//    Mem += s->cap * sizeof(double);   // ABC_FREE(s->factors  );
     Mem += s->cap * sizeof(lit);      // ABC_FREE(s->trail    );
     Mem += s->cap * sizeof(int);      // ABC_FREE(s->orderpos );
     Mem += s->cap * sizeof(int);      // ABC_FREE(s->reasons  );
@@ -1659,12 +1682,15 @@ double sat_solver2_memory( sat_solver2* s, int fAll )
     Mem += s->min_step_order.cap * sizeof(int);
     Mem += s->temp_proof.cap * sizeof(int);
     Mem += Sat_MemMemoryAll( &s->Mem );
-//    Mem += Vec_ReportMemory( &s->Proofs );
+//    Mem += Vec_ReportMemory( s->pPrf1 );
     return Mem;
 }
 double sat_solver2_memory_proof( sat_solver2* s )
 {
-    return Vec_ReportMemory( &s->Proofs );
+    double Mem = s->dPrfMemory;
+    if ( s->pPrf1 )
+        Mem += Vec_ReportMemory( s->pPrf1 );
+    return Mem;
 }
 
 
@@ -1911,7 +1937,14 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim
 void * Sat_ProofCore( sat_solver2 * s )
 {
     extern void * Proof_DeriveCore( Vec_Set_t * vProof, int hRoot );
-    return Proof_DeriveCore( &s->Proofs, s->hProofLast );
+    if ( s->pPrf1 )
+        return Proof_DeriveCore( s->pPrf1, s->hProofLast );
+    if ( s->pPrf2 )
+    {
+        s->dPrfMemory = Abc_MaxDouble( s->dPrfMemory, Prf_ManMemory(s->pPrf2) );
+        return Prf_ManUnsatCore( s->pPrf2 );
+    }
+    return NULL;
 }
 
 ABC_NAMESPACE_IMPL_END
diff --git a/src/sat/bsat/satSolver2.h b/src/sat/bsat/satSolver2.h
index 81ecea76..1682ab6e 100644
--- a/src/sat/bsat/satSolver2.h
+++ b/src/sat/bsat/satSolver2.h
@@ -31,6 +31,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "satVec.h"
 #include "satClause.h"
 #include "misc/vec/vecSet.h"
+#include "satProof2.h"
 
 ABC_NAMESPACE_HEADER_START
 
@@ -147,10 +148,12 @@ struct sat_solver2_t
     veci            learnt_live;    // remaining clauses after reduce DB
 
     // proof logging
-    Vec_Set_t       Proofs;         // sequence of proof records
+    Vec_Set_t *     pPrf1;          // sequence of proof records
     veci            temp_proof;     // temporary place to store proofs
     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)
+    Prf_Man_t *     pPrf2;          // another proof manager
+    double          dPrfMemory;     // memory used by the proof-logger
 
     // statistics
     stats_t         stats;
@@ -234,7 +237,8 @@ static inline void sat_solver2_bookmark(sat_solver2* s)
     assert( s->qhead == s->qtail );
     s->iVarPivot    = s->size;
     s->iTrailPivot  = s->qhead;
-    s->hProofPivot  = Vec_SetHandCurrent(&s->Proofs);
+    if ( s->pPrf1 )
+        s->hProofPivot  = Vec_SetHandCurrent(s->pPrf1);
     Sat_MemBookMark( &s->Mem );
 }