luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Fixed a corner case bug in dprove when a trivial CEX is not produced.

This commit is contained in:
Alan Mishchenko 2011-10-01 10:50:50 +07:00
parent dbe2b466d7
commit 7884dd01bc
1 changed files with 11 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

11
src/aig/fra/fraSec.c
View File

@ -620,6 +620,17 @@ ABC_PRT( "Time", clock() - clkTotal );
}
else if ( RetValue == 0 )
{
if ( pNew->pSeqModel == NULL )
{
int i;
// if the CEX is not derives, it is because tricial CEX should be assumed
pNew->pSeqModel = Abc_CexAlloc( Aig_ManRegNum(pNew), pNew->nTruePis, 1 );
// if the CEX does not work, we need to change PIs to 1 because
// the only way it can happen is when a PO is equal to a PI...
if ( Saig_ManFindFailedPoCex( pNew, pNew->pSeqModel ) == -1 )
for ( i = 0; i < pNew->nTruePis; i++ )
Aig_InfoSetBit( pNew->pSeqModel->pData, i );
}
if ( !pParSec->fSilent )
{
printf( "Networks are NOT EQUIVALENT. " );