Skip to content

A
abc
Commit 8cde0dd3 by Alan Mishchenko
Options

Bug fix in CBA.

parent 11dca3aa
Showing with 5 additions and 0 deletions
src/aig/saig/saigAbsCba.c
...@@ -621,6 +621,11 @@ Vec_Int_t * Saig_ManCbaPerform( Aig_Man_t * pAbs, int nInputs, Saig_ParBmc_t * p ...@@ -621,6 +621,11 @@ Vec_Int_t * Saig_ManCbaPerform( Aig_Man_t * pAbs, int nInputs, Saig_ParBmc_t * p
assert( pAbs->pSeqModel == NULL ); assert( pAbs->pSeqModel == NULL );
return Vec_IntAlloc( 0 ); 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 ) if ( pPars->fVerbose )
Abc_CexPrintStats( pAbs->pSeqModel ); Abc_CexPrintStats( pAbs->pSeqModel );
// CEX is detected - refine the flops // CEX is detected - refine the flops
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment