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

Timeout crash fix in 'reachy'.

This commit is contained in:
Alan Mishchenko 2012-02-13 21:10:15 -08:00
parent 59ea100dbf
commit e0650dce0a
1 changed files with 16 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

21
src/proof/llb/llb4Nonlin.c
View File

@ -127,13 +127,24 @@ DdNode * Llb_Nonlin4ComputeBad( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * vO
bCube = Cudd_ReadOne(dd); Cudd_Ref( bCube );
Saig_ManForEachPi( pAig, pObj, i )
{
bCube = Cudd_bddAnd( dd, bTemp = bCube, (DdNode *)pObj->pData ); Cudd_Ref( bCube );
bCube = Cudd_bddAnd( dd, bTemp = bCube, (DdNode *)pObj->pData );
if ( bCube == NULL )
{
Cudd_RecursiveDeref( dd, bTemp );
Cudd_RecursiveDeref( dd, bResult );
bResult = NULL;
break;
}
Cudd_Ref( bCube );
Cudd_RecursiveDeref( dd, bTemp );
}
bResult = Cudd_bddExistAbstract( dd, bTemp = bResult, bCube ); Cudd_Ref( bResult );
Cudd_RecursiveDeref( dd, bTemp );
Cudd_RecursiveDeref( dd, bCube );
Cudd_Deref( bResult );
if ( bResult != NULL )
{
bResult = Cudd_bddExistAbstract( dd, bTemp = bResult, bCube ); Cudd_Ref( bResult );
Cudd_RecursiveDeref( dd, bTemp );
Cudd_RecursiveDeref( dd, bCube );
Cudd_Deref( bResult );
}
}
//if ( bResult )
//printf( "Bad state = %d.\n", Cudd_DagSize(bResult) );