diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2020-11-15 00:12:03 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2020-11-15 00:12:03 -0800 |
| commit | 36e8567e778cdc4f0b2e3009b20083703e2b4f87 (patch) | |
| tree | 1844cb4176be2fafc28639597fe5ebcedbc53d2f | |
| parent | 4c78f37a5a78ee39957bcb5c793a7203509e642e (diff) | |
| download | abc-36e8567e778cdc4f0b2e3009b20083703e2b4f87.tar.gz abc-36e8567e778cdc4f0b2e3009b20083703e2b4f87.tar.bz2 abc-36e8567e778cdc4f0b2e3009b20083703e2b4f87.zip | |
Sweeping up to a given level (bug fix).
| -rw-r--r-- | src/proof/cec/cecSatG2.c | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/proof/cec/cecSatG2.c b/src/proof/cec/cecSatG2.c index b9ea682d..ffb000ed 100644 --- a/src/proof/cec/cecSatG2.c +++ b/src/proof/cec/cecSatG2.c @@ -656,7 +656,7 @@ void Cec4_RefineInit( Gia_Man_t * p, Cec4_Man_t * pMan ) Gia_ManForEachObj( p, pObj, i ) { p->pReprs[i].iRepr = GIA_VOID; - if ( !Gia_ObjIsCo(pObj) ) + if ( !Gia_ObjIsCo(pObj) && (!pMan->pPars->nLevelMax || Gia_ObjLevel(p, pObj) <= pMan->pPars->nLevelMax) ) Vec_IntPush( pMan->vRefNodes, i ); } pMan->vRefBins = Vec_IntAlloc( Gia_ManObjNum(p)/2 ); @@ -1466,7 +1466,7 @@ Gia_Obj_t * Cec4_ManFindRepr( Gia_Man_t * p, Cec4_Man_t * pMan, int iObj ) { if ( iObj == iMem ) break; - if ( Gia_ObjProved(p, iMem) ) + if ( Gia_ObjProved(p, iMem) || Gia_ObjFailed(p, iMem) ) continue; Cec4_ManSimulate_rec( p, pMan, iMem ); if ( Cec4_ObjSimEqual(p, iObj, iMem) ) |