Eneabled writing/reading pAbc->nFrames into/from status files.

2 files changed, 16 insertions, 14 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index efdf3c94..32618e76 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -6780,7 +6780,7 @@ int Abc_CommandReach( Abc_Frame_t * pAbc, int argc, char ** argv )
     pAbc->nFrames = pPars->iFrame;
     Abc_FrameReplaceCex( pAbc, &pNtk->pSeqModel );
     if ( pLogFileName )
-        Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, "reach" );
+        Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, pAbc->nFrames, "reach" );
     return 0;
 
 usage:
@@ -16884,7 +16884,7 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv )
     pAbc->Status = Abc_NtkDarProve( pNtk, pSecPar );
     Abc_FrameReplaceCex( pAbc, &pNtk->pSeqModel );
     if ( pLogFileName )
-        Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, "dprove" );
+        Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, pAbc->nFrames, "dprove" );
 
     // read back the resulting unsolved reduced sequential miter
     if ( pSecPar->fReadUnsolved && pSecPar->nSMnumber >= 0 )
@@ -18132,7 +18132,7 @@ int Abc_CommandBmc( Abc_Frame_t * pAbc, int argc, char ** argv )
     pAbc->nFrames = iFrames;
     Abc_FrameReplaceCex( pAbc, &pNtk->pSeqModel );
     if ( pLogFileName )
-        Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, "bmc" );
+        Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, pAbc->nFrames, "bmc" );
     return 0;
 
 usage:
@@ -18316,7 +18316,7 @@ int Abc_CommandBmc2( Abc_Frame_t * pAbc, int argc, char ** argv )
     pAbc->nFrames = iFrames;
     Abc_FrameReplaceCex( pAbc, &pNtk->pSeqModel );
     if ( pLogFileName )
-        Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, "bmc2" );
+        Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, pAbc->nFrames, "bmc2" );
     return 0;
 
 usage:
@@ -18450,7 +18450,7 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv )
     pAbc->nFrames = pPars->iFrame;
     Abc_FrameReplaceCex( pAbc, &pNtk->pSeqModel );
     if ( pLogFileName )
-        Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, "bmc3" );
+        Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, pAbc->nFrames, "bmc3" );
     if ( pPars->fSolveAll && pPars->fDropSatOuts )
     {
         if ( pNtk->pSeqModelVec == NULL )
@@ -18662,7 +18662,7 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_FrameReplaceCex( pAbc, &pNtk->pSeqModel );
     }
     if ( pLogFileName )
-        Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, "int" );
+        Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, pAbc->nFrames, "int" );
     return 0;
 
 usage:
@@ -24182,7 +24182,7 @@ int Abc_CommandAbc9Sim( Abc_Frame_t * pAbc, int argc, char ** argv )
         pAbc->Status = -1;
     Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq );
 //    if ( pLogFileName )
-//        Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, "&sim" );
+//        Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, pAbc->nFrames, "&sim" );
     return 0;
 
 usage:
@@ -27594,7 +27594,7 @@ int Abc_CommandAbc9ReachM( Abc_Frame_t * pAbc, int argc, char ** argv )
     pAbc->nFrames = pPars->iFrame;
     Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq );
     if ( pLogFileName )
-        Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, "&reachm" );
+        Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, pAbc->nFrames, "&reachm" );
     return 0;
 
 usage:
@@ -27742,7 +27742,7 @@ int Abc_CommandAbc9ReachP( Abc_Frame_t * pAbc, int argc, char ** argv )
     pAbc->nFrames = pPars->iFrame;
     Abc_FrameReplaceCex( pAbc, &pMan->pSeqModel );
     if ( pLogFileName )
-        Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, "&reachp" );
+        Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, pAbc->nFrames, "&reachp" );
     Aig_ManStop( pMan );
     return 0;
 
@@ -27870,7 +27870,7 @@ int Abc_CommandAbc9ReachN( Abc_Frame_t * pAbc, int argc, char ** argv )
     pAbc->nFrames = pPars->iFrame;
     Abc_FrameReplaceCex( pAbc, &pMan->pSeqModel );
     if ( pLogFileName )
-        Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, "&reachn" );
+        Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, pAbc->nFrames, "&reachn" );
     Aig_ManStop( pMan );
     return 0;
 
diff --git a/src/base/abci/abcLog.c b/src/base/abci/abcLog.c
index acdfc79b..615584a1 100644
--- a/src/base/abci/abcLog.c
+++ b/src/base/abci/abcLog.c
@@ -64,7 +64,7 @@ ABC_NAMESPACE_IMPL_START
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkWriteLogFile( char * pFileName, Abc_Cex_t * pCex, int Status, char * pCommand )
+void Abc_NtkWriteLogFile( char * pFileName, Abc_Cex_t * pCex, int Status, int nFrames, char * pCommand )
 {
     FILE * pFile;
     int i;
@@ -85,7 +85,7 @@ void Abc_NtkWriteLogFile( char * pFileName, Abc_Cex_t * pCex, int Status, char *
         printf( "Abc_NtkWriteLogFile(): Cannot recognize solving status.\n" );
     fprintf( pFile, " " );
     // write <cyc>
-    fprintf( pFile, "%d", pCex ? pCex->iFrame + 1 : -1 );
+    fprintf( pFile, "%d", pCex ? pCex->iFrame + 1 : nFrames );
     fprintf( pFile, " " );
     // write <engine_name>
     fprintf( pFile, "%s", pCommand ? pCommand : "unknown" );
@@ -125,12 +125,12 @@ void Abc_NtkWriteLogFile( char * pFileName, Abc_Cex_t * pCex, int Status, char *
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkReadLogFile( char * pFileName, Abc_Cex_t ** ppCex )
+int Abc_NtkReadLogFile( char * pFileName, Abc_Cex_t ** ppCex, int * pnFrames )
 {
+    FILE * pFile;
     Abc_Cex_t * pCex;
     Vec_Int_t * vNums;
     char Buffer[1000], * pToken;
-    FILE * pFile;
     int c, nRegs = -1, nFrames = -1, iPo = -1, Status = -1;
     pFile = fopen( pFileName, "r" );
     if ( pFile == NULL )
@@ -210,6 +210,8 @@ int Abc_NtkReadLogFile( char * pFileName, Abc_Cex_t ** ppCex )
         else
             ABC_FREE( pCex );
     }
+    if ( pnFrames )
+        *pnFrames = nFrames;
     return Status;
 }