Commit 7e501b9b by Alan Mishchenko

Bug fix in equivalence class handling.

parent 41a2b2a0
...@@ -769,6 +769,8 @@ Vec_Int_t * Gia_ManMapEquivAfterScorr( Gia_Man_t * p, Vec_Int_t * vMap ) ...@@ -769,6 +769,8 @@ Vec_Int_t * Gia_ManMapEquivAfterScorr( Gia_Man_t * p, Vec_Int_t * vMap )
{ {
if ( iObjLit == -1 ) if ( iObjLit == -1 )
continue; continue;
if ( Gia_ObjHasRepr(p, Abc_Lit2Var(iObjLit)) && !Gia_ObjProved(p, Abc_Lit2Var(iObjLit)) )
continue;
iReprGia = Gia_ObjReprSelf( p, Abc_Lit2Var(iObjLit) ); iReprGia = Gia_ObjReprSelf( p, Abc_Lit2Var(iObjLit) );
iReprMini = Vec_IntEntry( vGia2Mini, iReprGia ); iReprMini = Vec_IntEntry( vGia2Mini, iReprGia );
if ( iReprMini == -1 ) if ( iReprMini == -1 )
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment