diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2011-07-30 20:19:28 +0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2011-07-30 20:19:28 +0700 |
| commit | 43d8b8bece095d86cb927bf1d5ccac9aa1fab4e2 (patch) | |
| tree | dfad6e5d82a5866529e93a18b171a3a96de6f0e8 /src/base | |
| parent | b8de7a28e08a68860a9b88ee47a27841f83b5083 (diff) | |
| download | abc-43d8b8bece095d86cb927bf1d5ccac9aa1fab4e2.tar.gz abc-43d8b8bece095d86cb927bf1d5ccac9aa1fab4e2.tar.bz2 abc-43d8b8bece095d86cb927bf1d5ccac9aa1fab4e2.zip | |
Changes to enable smarter simulation.
Diffstat (limited to 'src/base')
| -rw-r--r-- | src/base/abci/abc.c | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 980ba7ed..3e2f720e 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -25438,6 +25438,11 @@ int Abc_CommandAbc9Equiv3( Abc_Frame_t * pAbc, int argc, char ** argv ) } if ( fUseCex ) { + if ( pAbc->pCex == NULL ) + { + Abc_Print( 0, "Abc_CommandAbc9Equiv3(): Counter-example is not available.\n" ); + return 0; + } if ( pAbc->pCex->nPis != Gia_ManPiNum(pAbc->pGia) ) { Abc_Print( -1, "Abc_CommandAbc9Equiv3(): The number of PIs differs in cex (%d) and in AIG (%d).\n", @@ -25450,7 +25455,8 @@ int Abc_CommandAbc9Equiv3( Abc_Frame_t * pAbc, int argc, char ** argv ) // else // pAbc->Status = Ssw_RarSignalFilterGia2( pAbc->pGia, nFrames, nWords, nBinSize, nRounds, TimeOut, fUseCex? pAbc->pCex: NULL, fLatchOnly, fVerbose ); // pAbc->nFrames = pAbc->pGia->pCexSeq->iFrame; - Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq ); + if ( pAbc->pGia->pCexSeq ) + Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq ); return 0; usage: |