diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-12-04 18:35:44 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-12-04 18:35:44 -0800 |
| commit | 8c04d9501f414b6985f9125cac91e41455ff26f3 (patch) | |
| tree | 4acf6c54c7b4b24e304a7acdbfe731ecb948a9d7 /src/proof/ssw | |
| parent | fe694d38e34c047a9a34a515f82543f31f4c7c97 (diff) | |
| download | abc-8c04d9501f414b6985f9125cac91e41455ff26f3.tar.gz abc-8c04d9501f414b6985f9125cac91e41455ff26f3.tar.bz2 abc-8c04d9501f414b6985f9125cac91e41455ff26f3.zip | |
Making 'scorr -c' applicable to seq benchmarks without constraints.
Diffstat (limited to 'src/proof/ssw')
| -rw-r--r-- | src/proof/ssw/sswConstr.c | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/proof/ssw/sswConstr.c b/src/proof/ssw/sswConstr.c index 475ed70c..3dcf0a34 100644 --- a/src/proof/ssw/sswConstr.c +++ b/src/proof/ssw/sswConstr.c @@ -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 ); } } |