Setting the number of completed time frames.

2 files changed, 13 insertions, 3 deletions

diff --git a/src/aig/gia/giaAbs.c b/src/aig/gia/giaAbs.c
index 16fe9c35..0a8652ad 100644
--- a/src/aig/gia/giaAbs.c
+++ b/src/aig/gia/giaAbs.c
@@ -291,6 +291,8 @@ int Gia_ManCbaPerform( Gia_Man_t * pGia, void * pPars )
     // update flop classes
     Gia_ManFlopsAddToClasses( pGia->vFlopClasses, vAbsFfsToAdd );
     Vec_IntFree( vAbsFfsToAdd );
+    if ( p->fVerbose )
+        Gia_ManPrintStats( pGia, 0 );
     return -1;
 }
 
@@ -362,6 +364,8 @@ int Gia_ManPbaPerform( Gia_Man_t * pGia, int nStart, int nFrames, int nConfLimit
         RetValue = -1;
     }
     Aig_ManStop( pAig );
+    if ( fVerbose )
+        Gia_ManPrintStats( pGia, 0 );
     return RetValue;
 }
 
@@ -379,7 +383,7 @@ int Gia_ManPbaPerform( Gia_Man_t * pGia, int nStart, int nFrames, int nConfLimit
 ***********************************************************************/
 int Gia_ManGlaCbaPerform( Gia_Man_t * pGia, void * pPars, int fNaiveCnf )
 {
-    extern Vec_Int_t * Aig_Gla1ManPerform( Aig_Man_t * pAig, Vec_Int_t * vGateClassesOld, int nStart, int nFramesMax, int nConfLimit, int TimeLimit, int fNaiveCnf, int fVerbose );
+    extern Vec_Int_t * Aig_Gla1ManPerform( Aig_Man_t * pAig, Vec_Int_t * vGateClassesOld, int nStart, int nFramesMax, int nConfLimit, int TimeLimit, int fNaiveCnf, int fVerbose, int * piFrame );
     Saig_ParBmc_t * p = (Saig_ParBmc_t *)pPars;
     Vec_Int_t * vGateClasses, * vGateClassesOld = NULL;
     Aig_Man_t * pAig;
@@ -395,14 +399,17 @@ int Gia_ManGlaCbaPerform( Gia_Man_t * pGia, void * pPars, int fNaiveCnf )
     }
 
     // perform abstraction
+    p->iFrame = -1;
     pAig = Gia_ManToAigSimple( pGia );
     assert( vGateClassesOld == NULL || Vec_IntSize(vGateClassesOld) == Aig_ManObjNumMax(pAig) );
-    vGateClasses = Aig_Gla1ManPerform( pAig, vGateClassesOld, p->nStart, p->nFramesMax, p->nConfLimit, p->nTimeOut, fNaiveCnf, p->fVerbose );
+    vGateClasses = Aig_Gla1ManPerform( pAig, vGateClassesOld, p->nStart, p->nFramesMax, p->nConfLimit, p->nTimeOut, fNaiveCnf, p->fVerbose, &p->iFrame );
     Aig_ManStop( pAig );
 
     // update the map
     Vec_IntFreeP( &vGateClassesOld );
     pGia->vGateClasses = vGateClasses;
+    if ( p->fVerbose )
+        Gia_ManPrintStats( pGia, 0 );
     return 1;
 }
 
@@ -476,6 +483,8 @@ int Gia_ManGlaPbaPerform( Gia_Man_t * pGia, void * pPars )
         Vec_IntFreeP( &pGia->vGateClasses );
         pGia->vGateClasses = vGateClasses;
     }
+    if ( p->fVerbose )
+        Gia_ManPrintStats( pGia, 0 );
     return 1;
 }
 
diff --git a/src/aig/saig/saigGlaCba.c b/src/aig/saig/saigGlaCba.c
index 9140c7bf..eae9a3c2 100644
--- a/src/aig/saig/saigGlaCba.c
+++ b/src/aig/saig/saigGlaCba.c
@@ -676,7 +676,7 @@ void Aig_Gla1ExtendIncluded( Aig_Gla1Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Int_t * Aig_Gla1ManPerform( Aig_Man_t * pAig, Vec_Int_t * vGateClassesOld, int nStart, int nFramesMax, int nConfLimit, int TimeLimit, int fNaiveCnf, int fVerbose )
+Vec_Int_t * Aig_Gla1ManPerform( Aig_Man_t * pAig, Vec_Int_t * vGateClassesOld, int nStart, int nFramesMax, int nConfLimit, int TimeLimit, int fNaiveCnf, int fVerbose, int * piFrame )
 {
     Vec_Int_t * vResult = NULL;
     Aig_Gla1Man_t * p;
@@ -812,6 +812,7 @@ Vec_Int_t * Aig_Gla1ManPerform( Aig_Man_t * pAig, Vec_Int_t * vGateClassesOld, i
         printf( "The problem is SAT in frame %d. The CEX is currently not produced.\n", f );
     else
         printf( "Ran out of conflict limit (%d) at frame %d.\n", nConfLimit, f );
+    *piFrame = i;
     // print stats
     if ( fVerbose )
     {