diff options
Diffstat (limited to 'src/aig/saig/saigAbsCba.c')
| -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 |