Fixing the problem with writing/reading bug-free depth in status files.

src/base/abci/abcLog.c

@@ -84,13 +84,16 @@ void Abc_NtkWriteLogFile( char * pFileName, Abc_Cex_t * pCex, int Status, int nF
     else 
         printf( "Abc_NtkWriteLogFile(): Cannot recognize solving status.\n" );
     fprintf( pFile, " " );
-    // write <cyc>
-    fprintf( pFile, "%d", pCex ? pCex->iFrame : nFrames );
+    // write <bug_free_depth>
+    fprintf( pFile, "%d", nFrames );
     fprintf( pFile, " " );
     // write <engine_name>
     fprintf( pFile, "%s", pCommand ? pCommand : "unknown" );
     if ( Status == 0 )
         fprintf( pFile, " %d", pCex->iPo );
+    // write <cyc>
+    if ( pCex && pCex->iFrame != nFrames )
+        fprintf( pFile, " %d", pCex->iFrame );
     fprintf( pFile, "\n" );
     // write <INIT_STATE>
     if ( pCex == NULL )
@@ -131,7 +134,7 @@ int Abc_NtkReadLogFile( char * pFileName, Abc_Cex_t ** ppCex, int * pnFrames )
     Abc_Cex_t * pCex;
     Vec_Int_t * vNums;
     char Buffer[1000], * pToken;
-    int c, nRegs = -1, nFrames = -1, iPo = -1, Status = -1;
+    int c, nRegs = -1, nFrames = -1, iPo = -1, Status = -1, nFrames2 = -1;
     pFile = fopen( pFileName, "r" );
     if ( pFile == NULL )
     {
@@ -153,6 +156,9 @@ int Abc_NtkReadLogFile( char * pFileName, Abc_Cex_t ** ppCex, int * pnFrames )
         pToken  = strtok( NULL, " \t\n" );
         pToken  = strtok( NULL, " \t\n" );
         iPo     = atoi( pToken ); 
+        pToken  = strtok( NULL, " \t\n" );
+        if ( pToken )
+            nFrames2 = atoi( pToken ); 
     }
     else if ( !strncmp( Buffer, "snl_UNK", strlen("snl_UNK") ) )
     {
@@ -182,6 +188,7 @@ int Abc_NtkReadLogFile( char * pFileName, Abc_Cex_t ** ppCex, int * pnFrames )
     fclose( pFile );
     if ( Vec_IntSize(vNums) )
     {
+        int iFrameCex = (nFrames2 == -1) ? nFrames : nFrames2;
         if ( nRegs == 0 )
         {
             printf( "Cannot read register number.\n" );
@@ -192,14 +199,14 @@ int Abc_NtkReadLogFile( char * pFileName, Abc_Cex_t ** ppCex, int * pnFrames )
             printf( "Cannot read counter example.\n" );
             return -1;
         }
-        if ( (Vec_IntSize(vNums)-nRegs) % nFrames != 0 )
+        if ( (Vec_IntSize(vNums)-nRegs) % (iFrameCex + 1) != 0 )
         {
             printf( "Incorrect number of bits.\n" );
             return -1;
         }
-        pCex = Abc_CexAlloc( nRegs, (Vec_IntSize(vNums)-nRegs)/nFrames, nFrames );
+        pCex = Abc_CexAlloc( nRegs, (Vec_IntSize(vNums)-nRegs)/(iFrameCex + 1), iFrameCex + 1 );
         pCex->iPo    = iPo;
-        pCex->iFrame = nFrames - 1;
+        pCex->iFrame = iFrameCex;
         assert( Vec_IntSize(vNums) == pCex->nBits );
         for ( c = 0; c < pCex->nBits; c++ )
             if ( Vec_IntEntry(vNums, c) )