diff options
| author | Miodrag Milanovic <mmicko@gmail.com> | 2022-05-06 15:41:34 +0200 |
|---|---|---|
| committer | Miodrag Milanovic <mmicko@gmail.com> | 2022-05-06 15:41:34 +0200 |
| commit | 6234e18df79ebd2484eb7d088dffaad61cbfe8ef (patch) | |
| tree | 122060dfa6044ef552cf5c98c9a2e3cc5f89dbd9 /src | |
| parent | c84323b5a5c6df273404b5d5ace70ae61a06bdb0 (diff) | |
| download | abc-6234e18df79ebd2484eb7d088dffaad61cbfe8ef.tar.gz abc-6234e18df79ebd2484eb7d088dffaad61cbfe8ef.tar.bz2 abc-6234e18df79ebd2484eb7d088dffaad61cbfe8ef.zip | |
Give more reasonable error on read_cex and handle status
Diffstat (limited to 'src')
| -rw-r--r-- | src/base/io/io.c | 11 |
1 files changed, 7 insertions, 4 deletions
diff --git a/src/base/io/io.c b/src/base/io/io.c index 27742664..7ad057df 100644 --- a/src/base/io/io.c +++ b/src/base/io/io.c @@ -686,7 +686,7 @@ int Abc_NtkReadCexFile( char * pFileName, Abc_Ntk_t * pNtk, Abc_Cex_t ** ppCex, FILE * pFile; Abc_Cex_t * pCex; Vec_Int_t * vNums; - int c, nRegs = -1, nFrames = -1, Status = 0; + int c, nRegs = -1, nFrames = -1; pFile = fopen( pFileName, "r" ); if ( pFile == NULL ) { @@ -804,7 +804,10 @@ int Abc_NtkReadCexFile( char * pFileName, Abc_Ntk_t * pNtk, Abc_Cex_t ** ppCex, Abc_NtkForEachPo(pNtk, pObj, i ) nPoNtk++; if ( nRegs < 0 ) { - printf( "ERROR: Cannot read register number.\n" ); + if (status == 1) + printf( "ERROR: Cannot read register number.\n" ); + else + printf( "Counter-example is not available.\n" ); Vec_IntFree( vNums ); return -1; } @@ -866,7 +869,7 @@ int Abc_NtkReadCexFile( char * pFileName, Abc_Ntk_t * pNtk, Abc_Cex_t ** ppCex, if ( pnFrames ) *pnFrames = nFrames; - return Status; + return status; } /**Function************************************************************* @@ -927,7 +930,7 @@ int IoCommandReadCex( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_FrameClearVerifStatus( pAbc ); pAbc->Status = Abc_NtkReadCexFile( pFileName, pNtk, &pAbc->pCex, &pAbc->nFrames, &fOldFormat ); - if ( fCheck ) { + if ( fCheck && pAbc->Status==1) { extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters ); Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 1 ); Bmc_CexCareVerify( pAig, pAbc->pCex, pAbc->pCex, false ); |