From 36e8567e778cdc4f0b2e3009b20083703e2b4f87 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 15 Nov 2020 00:12:03 -0800 Subject: Sweeping up to a given level (bug fix). --- src/proof/cec/cecSatG2.c | 4 ++-- 1 file 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) ) -- cgit v1.2.3