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

Making 'scorr -c' applicable to seq benchmarks without constraints.

This commit is contained in:
Alan Mishchenko 2012-12-04 18:35:44 -08:00
parent fe694d38e3
commit 8c04d9501f
1 changed files with 4 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
src/proof/ssw/sswConstr.c
View File

@ -49,7 +49,7 @@ Aig_Man_t * Ssw_FramesWithConstraints( Aig_Man_t * p, int nFrames )
Aig_Man_t * pFrames;
Aig_Obj_t * pObj, * pObjLi, * pObjLo;
int i, f;
assert( Saig_ManConstrNum(p) > 0 );
// assert( Saig_ManConstrNum(p) > 0 );
assert( Aig_ManRegNum(p) > 0 );
assert( Aig_ManRegNum(p) < Aig_ManCiNum(p) );
// start the fraig package
@ -106,7 +106,7 @@ int Ssw_ManSetConstrPhases( Aig_Man_t * p, int nFrames, Vec_Int_t ** pvInits )
int i, RetValue;
if ( pvInits )
*pvInits = NULL;
assert( p->nConstrs > 0 );
// assert( p->nConstrs > 0 );
// derive the timeframes
pFrames = Ssw_FramesWithConstraints( p, nFrames );
// create CNF
@ -275,12 +275,12 @@ void Ssw_ManRefineByConstrSim( Ssw_Man_t * p )
{
if ( i < Saig_ManPoNum(p->pAig) - Saig_ManConstrNum(p->pAig) )
{
if ( pObj->fMarkB )
if ( pObj->fMarkB && Saig_ManConstrNum(p->pAig) )
Abc_Print( 1, "output %d failed in frame %d.\n", i, f );
}
else
{
if ( pObj->fMarkB )
if ( pObj->fMarkB && Saig_ManConstrNum(p->pAig) )
Abc_Print( 1, "constraint %d failed in frame %d.\n", i, f );
}
}