From 96e1de436e3a87e7286e30b2b9f7840182f12715 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 14 May 2023 12:43:07 -0700 Subject: [PATCH] Bug fix in equivalence class handling (another try). --- src/aig/gia/giaMini.c | 4 ++-- src/proof/cec/cecSatG2.c | 3 +++ 2 files changed, 5 insertions(+), 2 deletions(-) diff --git a/src/aig/gia/giaMini.c b/src/aig/gia/giaMini.c index 904bbe9ad..6ba85706d 100644 --- a/src/aig/gia/giaMini.c +++ b/src/aig/gia/giaMini.c @@ -769,8 +769,8 @@ Vec_Int_t * Gia_ManMapEquivAfterScorr( Gia_Man_t * p, Vec_Int_t * vMap ) { if ( iObjLit == -1 ) continue; - if ( Gia_ObjHasRepr(p, Abc_Lit2Var(iObjLit)) && !Gia_ObjProved(p, Abc_Lit2Var(iObjLit)) ) - continue; +// if ( Gia_ObjHasRepr(p, Abc_Lit2Var(iObjLit)) && !Gia_ObjProved(p, Abc_Lit2Var(iObjLit)) ) +// continue; iReprGia = Gia_ObjReprSelf( p, Abc_Lit2Var(iObjLit) ); iReprMini = Vec_IntEntry( vGia2Mini, iReprGia ); if ( iReprMini == -1 ) diff --git a/src/proof/cec/cecSatG2.c b/src/proof/cec/cecSatG2.c index ef93548bd..2ee8e3f86 100644 --- a/src/proof/cec/cecSatG2.c +++ b/src/proof/cec/cecSatG2.c @@ -1862,6 +1862,9 @@ finalize: pMan->nSatUndec, pMan->nSimulates, pMan->nRecycles, 100.0*pMan->nGates[1]/Abc_MaxInt(1, pMan->nGates[0]+pMan->nGates[1]) ); Cec4_ManDestroy( pMan ); + Gia_ManForEachAnd( p, pObj, i ) + if ( Gia_ObjHasRepr(p, i) && !Gia_ObjProved(p, i) ) + Gia_ObjSetRepr(p, i, GIA_VOID); //Gia_ManStaticFanoutStop( p ); //Gia_ManEquivPrintClasses( p, 1, 0 ); if ( ppNew && *ppNew == NULL )