Bug fix in equivalence class handling (another try).

berkeley-abc · May 14, 2023 · 96e1de4 · 96e1de4
1 parent bb43789
commit 96e1de4
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 2 deletions.
diff --git 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
@@ -1862,6 +1862,9 @@ int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** p
             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 )