Bug fix in GLA PBA.

2 files changed, 19 insertions, 5 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 5ec8de3f..a79e12dd 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -350,6 +350,8 @@ static inline int          Gia_ObjFaninLit1p( Gia_Man_t * p, Gia_Obj_t * pObj) {
 static inline void         Gia_ObjFlipFaninC0( Gia_Obj_t * pObj )              { assert( Gia_ObjIsCo(pObj) ); pObj->fCompl0 ^= 1;          }
 static inline int          Gia_ObjWhatFanin( Gia_Obj_t * pObj, Gia_Obj_t * pFanin )  { return Gia_ObjFanin0(pObj) == pFanin ? 0 : (Gia_ObjFanin1(pObj) == pFanin ? 1 : -1); }
 
+static inline Gia_Obj_t *  Gia_ObjCopy( Gia_Man_t * p, Gia_Obj_t * pObj )      { return Gia_ManObj( p, Gia_Lit2Var(pObj->Value) );                              }
+
 static inline int          Gia_ObjFanin0Copy( Gia_Obj_t * pObj )               { return Gia_LitNotCond( Gia_ObjFanin0(pObj)->Value, Gia_ObjFaninC0(pObj) );     }
 static inline int          Gia_ObjFanin1Copy( Gia_Obj_t * pObj )               { return Gia_LitNotCond( Gia_ObjFanin1(pObj)->Value, Gia_ObjFaninC1(pObj) );     }
 
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index 1faa13cd..f1508375 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -1619,7 +1619,7 @@ Gia_Man_t * Gia_ManDupAbsGates( Gia_Man_t * p, Vec_Int_t * vGateClasses )
 { 
     Vec_Int_t * vAssigned, * vPis, * vPPis, * vFlops, * vNodes;
     Gia_Man_t * pNew, * pTemp;
-    Gia_Obj_t * pObj;
+    Gia_Obj_t * pObj, * pCopy;
     int i, nFlops = 0;
     assert( Gia_ManPoNum(p) == 1 );
     assert( Vec_IntSize(vGateClasses) == Gia_ManObjNum(p) );
@@ -1672,11 +1672,23 @@ Gia_Man_t * Gia_ManDupAbsGates( Gia_Man_t * p, Vec_Int_t * vGateClasses )
         Gia_ObjRoToRi(p, pObj)->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(Gia_ObjRoToRi(p, pObj)) );
     Gia_ManSetRegNum( pNew, Vec_IntSize(vFlops) );
     // clean up
-//    pNew = Gia_ManSeqCleanup( pTemp = pNew );
-    pNew = Gia_ManCleanup( pTemp = pNew );
+    pNew = Gia_ManSeqCleanup( pTemp = pNew );
+    // transfer copy values: (p -> pTemp -> pNew) => (p -> pNew)
     if ( Gia_ManObjNum(pTemp) != Gia_ManObjNum(pNew) )
-        printf( "Gia_ManDupAbsGates() Internal error: object mismatch.\n" );
-    assert( Gia_ManObjNum(pTemp) == Gia_ManObjNum(pNew) );
+    {
+//        printf( "Gia_ManDupAbsGates() Internal error: object mismatch.\n" );
+        Gia_ManForEachObj( p, pObj, i )
+        {
+            if ( !~pObj->Value )
+                continue;
+            assert( !Gia_LitIsCompl(pObj->Value) );
+            pCopy = Gia_ObjCopy( pTemp, pObj );
+            if ( !~pCopy->Value )
+                continue;
+            assert( !Gia_LitIsCompl(pCopy->Value) );
+            pObj->Value = pCopy->Value;
+        }
+    }
     Gia_ManStop( pTemp );
 
     Vec_IntFree( vPis );