From aa9c87cf8d9d3e729ef5ab263c34d531a8f73d07 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 25 Jan 2013 05:59:56 +0700 Subject: Extending verification status file format to allow for SAT status without CEX. --- src/base/abci/abcLog.c | 19 +++++++++++++++---- 1 file changed, 15 insertions(+), 4 deletions(-) (limited to 'src') diff --git a/src/base/abci/abcLog.c b/src/base/abci/abcLog.c index 32635a91..b583aa02 100644 --- a/src/base/abci/abcLog.c +++ b/src/base/abci/abcLog.c @@ -156,10 +156,16 @@ int Abc_NtkReadLogFile( char * pFileName, Abc_Cex_t ** ppCex, int * pnFrames ) nFrames = atoi( pToken ); pToken = strtok( NULL, " \t\n" ); pToken = strtok( NULL, " \t\n" ); - iPo = atoi( pToken ); - pToken = strtok( NULL, " \t\n" ); - if ( pToken ) - nFrames2 = atoi( pToken ); + if ( pToken != NULL ) + { + iPo = atoi( pToken ); + pToken = strtok( NULL, " \t\n" ); + if ( pToken ) + nFrames2 = atoi( pToken ); + } + else + printf( "Warning! The current status is SAT but the current CEX is not given.\n" ); + } else if ( !strncmp( Buffer, "snl_UNK", strlen("snl_UNK") ) ) { @@ -193,16 +199,19 @@ int Abc_NtkReadLogFile( char * pFileName, Abc_Cex_t ** ppCex, int * pnFrames ) if ( nRegs < 0 ) { printf( "Cannot read register number.\n" ); + Vec_IntFree( vNums ); return -1; } if ( Vec_IntSize(vNums)-nRegs == 0 ) { printf( "Cannot read counter example.\n" ); + Vec_IntFree( vNums ); return -1; } if ( (Vec_IntSize(vNums)-nRegs) % (iFrameCex + 1) != 0 ) { printf( "Incorrect number of bits.\n" ); + Vec_IntFree( vNums ); return -1; } pCex = Abc_CexAlloc( nRegs, (Vec_IntSize(vNums)-nRegs)/(iFrameCex + 1), iFrameCex + 1 ); @@ -218,6 +227,8 @@ int Abc_NtkReadLogFile( char * pFileName, Abc_Cex_t ** ppCex, int * pnFrames ) else ABC_FREE( pCex ); } + else + Vec_IntFree( vNums ); if ( pnFrames ) *pnFrames = nFrames; return Status; -- cgit v1.2.3