Variable timeframe abstraction.

2 files changed, 71 insertions, 95 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;