diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2011-08-31 11:37:59 +0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2011-08-31 11:37:59 +0700 |
| commit | 8cde0dd33c00fb9525e835551f87a1525ad70f3b (patch) | |
| tree | a4c86f3141df680b311c998ea26000c0329d5606 | |
| parent | 11dca3aab04295f5d74f8efe02758a12b04c4e7f (diff) | |
| download | abc-8cde0dd33c00fb9525e835551f87a1525ad70f3b.tar.gz abc-8cde0dd33c00fb9525e835551f87a1525ad70f3b.tar.bz2 abc-8cde0dd33c00fb9525e835551f87a1525ad70f3b.zip | |
Bug fix in CBA.
| -rw-r--r-- | src/aig/saig/saigAbsCba.c | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/aig/saig/saigAbsCba.c b/src/aig/saig/saigAbsCba.c index f79cbf09..4d9cef57 100644 --- a/src/aig/saig/saigAbsCba.c +++ b/src/aig/saig/saigAbsCba.c @@ -621,6 +621,11 @@ Vec_Int_t * Saig_ManCbaPerform( Aig_Man_t * pAbs, int nInputs, Saig_ParBmc_t * p assert( pAbs->pSeqModel == NULL ); return Vec_IntAlloc( 0 ); } + if ( pAbs->pSeqModel == NULL ) + { + printf( "BMC did not detect a CEX with the given depth.\n" ); + return Vec_IntAlloc( 0 ); + } if ( pPars->fVerbose ) Abc_CexPrintStats( pAbs->pSeqModel ); // CEX is detected - refine the flops |