Renamed reference counting APIs in GIA package.

23 files changed, 85 insertions, 93 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index fd47d2c7..b3efa455 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -109,7 +109,6 @@ struct Gia_Man_t_
     int            nHTable;       // hash table size 
     int            fAddStrash;    // performs additional structural hashing
     int *          pRefs;         // the reference count
-    int *          pNodeRefs;     // node references
     Vec_Int_t *    vLevels;       // levels of the nodes
     int            nLevels;       // the mamixum level
     int            nConstrs;      // the number of constraints
@@ -368,21 +367,14 @@ static inline void         Gia_ObjSetAndLevel( Gia_Man_t * p, Gia_Obj_t * pObj )
 static inline int          Gia_ObjNum( Gia_Man_t * p, Gia_Obj_t * pObj )       { return (int)(unsigned char)Vec_StrGetEntry(p->vTtNums, Gia_ObjId(p,pObj));                  }
 static inline void         Gia_ObjSetNum( Gia_Man_t * p, Gia_Obj_t * pObj, int n ) { assert( n >= 0 && n < 254 ); Vec_StrSetEntry(p->vTtNums, Gia_ObjId(p,pObj), (char)n);   }
 
-static inline int          Gia_ObjRefs( Gia_Man_t * p, Gia_Obj_t * pObj )      { assert( p->pRefs); return p->pRefs[Gia_ObjId(p, pObj)];    }
-static inline int          Gia_ObjRefsId( Gia_Man_t * p, int Id )              { assert( p->pRefs); return p->pRefs[Id];                    }
-static inline int          Gia_ObjRefInc( Gia_Man_t * p, Gia_Obj_t * pObj )    { assert( p->pRefs); return p->pRefs[Gia_ObjId(p, pObj)]++;  }
-static inline int          Gia_ObjRefDec( Gia_Man_t * p, Gia_Obj_t * pObj )    { assert( p->pRefs); return --p->pRefs[Gia_ObjId(p, pObj)];  }
-static inline void         Gia_ObjRefFanin0Inc(Gia_Man_t * p, Gia_Obj_t * pObj){ assert( p->pRefs); Gia_ObjRefInc(p, Gia_ObjFanin0(pObj));  }
-static inline void         Gia_ObjRefFanin1Inc(Gia_Man_t * p, Gia_Obj_t * pObj){ assert( p->pRefs); Gia_ObjRefInc(p, Gia_ObjFanin1(pObj));  }
-static inline void         Gia_ObjRefFanin0Dec(Gia_Man_t * p, Gia_Obj_t * pObj){ assert( p->pRefs); Gia_ObjRefDec(p, Gia_ObjFanin0(pObj));  }
-static inline void         Gia_ObjRefFanin1Dec(Gia_Man_t * p, Gia_Obj_t * pObj){ assert( p->pRefs); Gia_ObjRefDec(p, Gia_ObjFanin1(pObj));  }
-
-static inline int          Gia_ObjNodeRefs( Gia_Man_t * p, Gia_Obj_t * pObj )      { assert( p->pNodeRefs); return p->pNodeRefs[Gia_ObjId(p, pObj)];    }
-static inline int          Gia_ObjNodeRefsId( Gia_Man_t * p, int Id )              { assert( p->pNodeRefs); return p->pNodeRefs[Id];                    }
-static inline int          Gia_ObjNodeRefIncId( Gia_Man_t * p, int Id )            { assert( p->pNodeRefs); return p->pNodeRefs[Id]++;                  }
-static inline int          Gia_ObjNodeRefDecId( Gia_Man_t * p, int Id )            { assert( p->pNodeRefs); return --p->pNodeRefs[Id];                  }
-static inline int          Gia_ObjNodeRefInc( Gia_Man_t * p, Gia_Obj_t * pObj )    { assert( p->pNodeRefs); return p->pNodeRefs[Gia_ObjId(p, pObj)]++;  }
-static inline int          Gia_ObjNodeRefDec( Gia_Man_t * p, Gia_Obj_t * pObj )    { assert( p->pNodeRefs); return --p->pNodeRefs[Gia_ObjId(p, pObj)];  }
+static inline int          Gia_ObjRefNumId( Gia_Man_t * p, int Id )            { assert(p->pRefs); return p->pRefs[Id];                    }
+static inline int          Gia_ObjRefNum( Gia_Man_t * p, Gia_Obj_t * pObj )    { assert(p->pRefs); return p->pRefs[Gia_ObjId(p, pObj)];    }
+static inline int          Gia_ObjRefInc( Gia_Man_t * p, Gia_Obj_t * pObj )    { assert(p->pRefs); return p->pRefs[Gia_ObjId(p, pObj)]++;  }
+static inline int          Gia_ObjRefDec( Gia_Man_t * p, Gia_Obj_t * pObj )    { assert(p->pRefs); return --p->pRefs[Gia_ObjId(p, pObj)];  }
+static inline void         Gia_ObjRefFanin0Inc(Gia_Man_t * p, Gia_Obj_t * pObj){ assert(p->pRefs); Gia_ObjRefInc(p, Gia_ObjFanin0(pObj));  }
+static inline void         Gia_ObjRefFanin1Inc(Gia_Man_t * p, Gia_Obj_t * pObj){ assert(p->pRefs); Gia_ObjRefInc(p, Gia_ObjFanin1(pObj));  }
+static inline void         Gia_ObjRefFanin0Dec(Gia_Man_t * p, Gia_Obj_t * pObj){ assert(p->pRefs); Gia_ObjRefDec(p, Gia_ObjFanin0(pObj));  }
+static inline void         Gia_ObjRefFanin1Dec(Gia_Man_t * p, Gia_Obj_t * pObj){ assert(p->pRefs); Gia_ObjRefDec(p, Gia_ObjFanin1(pObj));  }
 
 static inline void         Gia_ObjSetTravIdCurrent( Gia_Man_t * p, Gia_Obj_t * pObj )         { assert( Gia_ObjId(p, pObj) < p->nTravIdsAlloc ); p->pTravIds[Gia_ObjId(p, pObj)] = p->nTravIds;                    }
 static inline void         Gia_ObjSetTravIdPrevious( Gia_Man_t * p, Gia_Obj_t * pObj )        { assert( Gia_ObjId(p, pObj) < p->nTravIdsAlloc ); p->pTravIds[Gia_ObjId(p, pObj)] = p->nTravIds - 1;                }
@@ -911,9 +903,9 @@ extern void                Gia_ManSetPhase( Gia_Man_t * p );
 extern void                Gia_ManSetPhase1( Gia_Man_t * p );
 extern void                Gia_ManCleanPhase( Gia_Man_t * p );
 extern int                 Gia_ManLevelNum( Gia_Man_t * p );
-extern void                Gia_ManSetRefs( Gia_Man_t * p );
-extern int *               Gia_ManCreateMuxRefs( Gia_Man_t * p );
+extern void                Gia_ManCreateValueRefs( Gia_Man_t * p );
 extern void                Gia_ManCreateRefs( Gia_Man_t * p );
+extern int *               Gia_ManCreateMuxRefs( Gia_Man_t * p );
 extern int                 Gia_ManCrossCut( Gia_Man_t * p );
 extern int                 Gia_ManIsNormalized( Gia_Man_t * p );
 extern Vec_Int_t *         Gia_ManCollectPoIds( Gia_Man_t * p );
diff --git a/src/aig/gia/giaCSat.c b/src/aig/gia/giaCSat.c
index b4bc5b3e..6d7df6b5 100644
--- a/src/aig/gia/giaCSat.c
+++ b/src/aig/gia/giaCSat.c
@@ -375,8 +375,8 @@ static inline int Cbs_VarFaninFanoutMax( Cbs_Man_t * p, Gia_Obj_t * pObj )
     int Count0, Count1;
     assert( !Gia_IsComplement(pObj) );
     assert( Gia_ObjIsAnd(pObj) );
-    Count0 = Gia_ObjRefs( p->pAig, Gia_ObjFanin0(pObj) );
-    Count1 = Gia_ObjRefs( p->pAig, Gia_ObjFanin1(pObj) );
+    Count0 = Gia_ObjRefNum( p->pAig, Gia_ObjFanin0(pObj) );
+    Count1 = Gia_ObjRefNum( p->pAig, Gia_ObjFanin1(pObj) );
     return Abc_MaxInt( Count0, Count1 );
 }
 
@@ -888,7 +888,7 @@ int Cbs_ManSolve_rec( Cbs_Man_t * p, int Level )
     else assert( 0 );
     assert( Cbs_VarIsJust( pVar ) );
     // chose decision variable using fanout count
-    if ( Gia_ObjRefs(p->pAig, Gia_ObjFanin0(pVar)) > Gia_ObjRefs(p->pAig, Gia_ObjFanin1(pVar)) )
+    if ( Gia_ObjRefNum(p->pAig, Gia_ObjFanin0(pVar)) > Gia_ObjRefNum(p->pAig, Gia_ObjFanin1(pVar)) )
         pDecVar = Gia_Not(Gia_ObjChild0(pVar));
     else
         pDecVar = Gia_Not(Gia_ObjChild1(pVar));
diff --git a/src/aig/gia/giaCSatOld.c b/src/aig/gia/giaCSatOld.c
index 1dd4a425..75b4c3e0 100644
--- a/src/aig/gia/giaCSatOld.c
+++ b/src/aig/gia/giaCSatOld.c
@@ -330,8 +330,8 @@ static inline int Cbs0_VarFaninFanoutMax( Cbs0_Man_t * p, Gia_Obj_t * pObj )
     int Count0, Count1;
     assert( !Gia_IsComplement(pObj) );
     assert( Gia_ObjIsAnd(pObj) );
-    Count0 = Gia_ObjRefs( p->pAig, Gia_ObjFanin0(pObj) );
-    Count1 = Gia_ObjRefs( p->pAig, Gia_ObjFanin1(pObj) );
+    Count0 = Gia_ObjRefNum( p->pAig, Gia_ObjFanin0(pObj) );
+    Count1 = Gia_ObjRefNum( p->pAig, Gia_ObjFanin1(pObj) );
     return Abc_MaxInt( Count0, Count1 );
 }
 
@@ -612,7 +612,7 @@ int Cbs0_ManSolve_rec( Cbs0_Man_t * p )
     else assert( 0 );
     assert( Cbs0_VarIsJust( pVar ) );
     // chose decision variable using fanout count
-    if ( Gia_ObjRefs(p->pAig, Gia_ObjFanin0(pVar)) > Gia_ObjRefs(p->pAig, Gia_ObjFanin1(pVar)) )
+    if ( Gia_ObjRefNum(p->pAig, Gia_ObjFanin0(pVar)) > Gia_ObjRefNum(p->pAig, Gia_ObjFanin1(pVar)) )
         pDecVar = Gia_Not(Gia_ObjChild0(pVar));
     else
         pDecVar = Gia_Not(Gia_ObjChild1(pVar));
diff --git a/src/aig/gia/giaCTas.c b/src/aig/gia/giaCTas.c
index 6dd0e0fa..79b42c66 100644
--- a/src/aig/gia/giaCTas.c
+++ b/src/aig/gia/giaCTas.c
@@ -441,8 +441,8 @@ static inline int Tas_VarFaninFanoutMax( Tas_Man_t * p, Gia_Obj_t * pObj )
     int Count0, Count1;
     assert( !Gia_IsComplement(pObj) );
     assert( Gia_ObjIsAnd(pObj) );
-    Count0 = Gia_ObjRefs( p->pAig, Gia_ObjFanin0(pObj) );
-    Count1 = Gia_ObjRefs( p->pAig, Gia_ObjFanin1(pObj) );
+    Count0 = Gia_ObjRefNum( p->pAig, Gia_ObjFanin0(pObj) );
+    Count1 = Gia_ObjRefNum( p->pAig, Gia_ObjFanin1(pObj) );
     return Abc_MaxInt( Count0, Count1 );
 }
 
@@ -1321,7 +1321,7 @@ int Tas_ManSolve_rec( Tas_Man_t * p, int Level )
     if ( pVar != NULL )
     {
         assert( Tas_VarIsJust( pVar ) );
-        if ( Gia_ObjRefs(p->pAig, Gia_ObjFanin0(pVar)) > Gia_ObjRefs(p->pAig, Gia_ObjFanin1(pVar)) )
+        if ( Gia_ObjRefNum(p->pAig, Gia_ObjFanin0(pVar)) > Gia_ObjRefNum(p->pAig, Gia_ObjFanin1(pVar)) )
             pDecVar = Gia_Not(Gia_ObjChild0(pVar));
         else
             pDecVar = Gia_Not(Gia_ObjChild1(pVar));
diff --git a/src/aig/gia/giaChoice.c b/src/aig/gia/giaChoice.c
index a1d9e325..f5619028 100644
--- a/src/aig/gia/giaChoice.c
+++ b/src/aig/gia/giaChoice.c
@@ -228,7 +228,7 @@ int Gia_ManHasChoices( Gia_Man_t * p )
     Gia_ManCreateRefs( p );
     Gia_ManForEachAnd( p, pObj, i )
     {
-        if ( Gia_ObjRefs(p, pObj) == 0 )
+        if ( Gia_ObjRefNum(p, pObj) == 0 )
         {
             if ( Gia_ObjReprObj( p, Gia_ObjId(p, pObj) ) == NULL )
                 nFailNoRepr++;
diff --git a/src/aig/gia/giaCof.c b/src/aig/gia/giaCof.c
index d41b6723..e9fd6c8b 100644
--- a/src/aig/gia/giaCof.c
+++ b/src/aig/gia/giaCof.c
@@ -143,7 +143,7 @@ Cof_Man_t * Cof_ManCreateLogicSimple( Gia_Man_t * pGia )
         pObj->Value = iHandle;
         pObjLog = Cof_ManObj( p, iHandle );
         pObjLog->nFanins  = 0;
-        pObjLog->nFanouts = Gia_ObjRefs( pGia, pObj );
+        pObjLog->nFanouts = Gia_ObjRefNum( pGia, pObj );
         pObjLog->Id       = i;
         pObjLog->Value    = 0;
         if ( Gia_ObjIsAnd(pObj) )
@@ -811,7 +811,7 @@ Vec_Int_t * Gia_ManCofVars( Gia_Man_t * p, int nFanLim )
     Gia_ManCreateRefs( p );
     vVars = Vec_IntAlloc( 100 );
     Gia_ManForEachObj( p, pObj, i )
-        if ( Gia_ObjIsCand(pObj) && Gia_ObjRefs(p, pObj) >= nFanLim )
+        if ( Gia_ObjIsCand(pObj) && Gia_ObjRefNum(p, pObj) >= nFanLim )
             Vec_IntPush( vVars, i );
     ABC_FREE( p->pRefs );
     return vVars;
@@ -877,7 +877,7 @@ Gia_Man_t * Gia_ManDupCofAllInt( Gia_Man_t * p, Vec_Int_t * vSigs, int fVerbose
         Vec_IntSort( vSigsNew, 0 );
         iVar = Vec_IntPop( vSigsNew );
 //        Gia_ManCreateRefs( pAig );
-//        printf( "ref count = %d\n", Gia_ObjRefs( pAig, Gia_ManObj(pAig, iVar) ) );
+//        printf( "ref count = %d\n", Gia_ObjRefNum( pAig, Gia_ManObj(pAig, iVar) ) );
 //        ABC_FREE( pAig->pRefs );
         pCof = Gia_ManDupCofInt( pAig, iVar );
         pNew = Gia_ManCleanup( pCof );
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index d598b511..e49ce616 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -1061,7 +1061,7 @@ Gia_Man_t * Gia_ManDupTrimmed( Gia_Man_t * p, int fTrimCis, int fTrimCos, int fD
     // check if there are PIs to be added
     Gia_ManCreateRefs( p );
     Gia_ManForEachPi( p, pObj, i )
-        if ( !fTrimCis || Gia_ObjRefs(p, pObj) )
+        if ( !fTrimCis || Gia_ObjRefNum(p, pObj) )
             break;
     if ( i == Gia_ManPiNum(p) ) // there is no PIs - add dummy PI
         Gia_ManAppendCi(pNew);
@@ -1069,7 +1069,7 @@ Gia_Man_t * Gia_ManDupTrimmed( Gia_Man_t * p, int fTrimCis, int fTrimCos, int fD
     Gia_ManFillValue( p );
     Gia_ManConst0(p)->Value = 0;
     Gia_ManForEachCi( p, pObj, i )
-        if ( !fTrimCis || Gia_ObjRefs(p, pObj) || Gia_ObjIsRo(p, pObj) )
+        if ( !fTrimCis || Gia_ObjRefNum(p, pObj) || Gia_ObjIsRo(p, pObj) )
             pObj->Value = Gia_ManAppendCi(pNew);
     Gia_ManForEachAnd( p, pObj, i )
         pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
@@ -1142,7 +1142,7 @@ Gia_Man_t * Gia_ManDupTrimmed2( Gia_Man_t * p )
         Gia_ObjRefFanin0Dec( p, pObj );
     // check if PIs are left
     Gia_ManForEachPi( p, pObj, i )
-        if ( Gia_ObjRefs(p, pObj) )
+        if ( Gia_ObjRefNum(p, pObj) )
             break;
     if ( i == Gia_ManPiNum(p) ) // there is no PIs - add dummy PI
         Gia_ManAppendCi(pNew);
@@ -1150,7 +1150,7 @@ Gia_Man_t * Gia_ManDupTrimmed2( Gia_Man_t * p )
     Gia_ManFillValue( p );
     Gia_ManConst0(p)->Value = 0;
     Gia_ManForEachCi( p, pObj, i )
-        if ( Gia_ObjRefs(p, pObj) || Gia_ObjIsRo(p, pObj) )
+        if ( Gia_ObjRefNum(p, pObj) || Gia_ObjIsRo(p, pObj) )
             pObj->Value = Gia_ManAppendCi(pNew);
     Gia_ManForEachAnd( p, pObj, i )
         pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
diff --git a/src/aig/gia/giaEmbed.c b/src/aig/gia/giaEmbed.c
index 17f80707..b6c4655e 100644
--- a/src/aig/gia/giaEmbed.c
+++ b/src/aig/gia/giaEmbed.c
@@ -190,7 +190,7 @@ Emb_Man_t * Emb_ManStartSimple( Gia_Man_t * pGia )
     pObjLog = Emb_ManObj( p, hHandle );
     pObjLog->hHandle  = hHandle;
     pObjLog->nFanins  = Gia_ManCoNum(pGia);  //0;
-    pObjLog->nFanouts = Gia_ObjRefs( pGia, Gia_ManConst0(pGia) );
+    pObjLog->nFanouts = Gia_ObjRefNum( pGia, Gia_ManConst0(pGia) );
     // count objects
     hHandle += Emb_ObjSize( pObjLog );
     nNodes = 1;
@@ -204,7 +204,7 @@ Emb_Man_t * Emb_ManStartSimple( Gia_Man_t * pGia )
         pObjLog = Emb_ManObj( p, hHandle );
         pObjLog->hHandle  = hHandle;
         pObjLog->nFanins  = Gia_ObjIsRo( pGia, pObj );
-        pObjLog->nFanouts = Gia_ObjRefs( pGia, pObj );
+        pObjLog->nFanouts = Gia_ObjRefNum( pGia, pObj );
         pObjLog->fCi = 1;
         // count objects
         hHandle += Emb_ObjSize( pObjLog );
@@ -213,13 +213,13 @@ Emb_Man_t * Emb_ManStartSimple( Gia_Man_t * pGia )
     // create internal nodes
     Gia_ManForEachAnd( pGia, pObj, i )
     {
-        assert( Gia_ObjRefs( pGia, pObj ) > 0 );
+        assert( Gia_ObjRefNum( pGia, pObj ) > 0 );
         // create node object
         pObj->Value = hHandle;
         pObjLog = Emb_ManObj( p, hHandle );
         pObjLog->hHandle  = hHandle;
         pObjLog->nFanins  = 2;
-        pObjLog->nFanouts = Gia_ObjRefs( pGia, pObj );
+        pObjLog->nFanouts = Gia_ObjRefNum( pGia, pObj );
         // add fanins
         pFanLog = Emb_ManObj( p, Gia_ObjValue(Gia_ObjFanin0(pObj)) ); 
         Emb_ObjAddFanin( pObjLog, pFanLog );
@@ -364,7 +364,7 @@ void Emb_ManCreateRefsSpecial( Gia_Man_t * p )
             Gia_ObjRefDec( p, Gia_Regular(pObjD0) );
     }
     Gia_ManForEachAnd( p, pObj, i )
-        assert( Gia_ObjRefs(p, pObj) > 0 );
+        assert( Gia_ObjRefNum(p, pObj) > 0 );
     Gia_ManCleanMark0( p );
 }
 
@@ -394,7 +394,7 @@ void Emb_ManTransformRefs( Gia_Man_t * p, int * pnObjs, int * pnFanios )
         pObj->fMark0 = 1;
     // mark those nodes that have ref count more than 1
     Gia_ManForEachAnd( p, pObj, i )
-        pObj->fMark0 = (Gia_ObjRefs(p, pObj) > 1);
+        pObj->fMark0 = (Gia_ObjRefNum(p, pObj) > 1);
     // mark the output drivers
     Gia_ManForEachCoDriver( p, pObj, i )
         pObj->fMark0 = 1;
@@ -516,7 +516,7 @@ Emb_Man_t * Emb_ManStart( Gia_Man_t * pGia )
     pObjLog = Emb_ManObj( p, hHandle );
     pObjLog->hHandle  = hHandle;
     pObjLog->nFanins  = Gia_ManCoNum(pGia);  //0;
-    pObjLog->nFanouts = Gia_ObjRefs( pGia, Gia_ManConst0(pGia) );
+    pObjLog->nFanouts = Gia_ObjRefNum( pGia, Gia_ManConst0(pGia) );
     // count objects
     hHandle += Emb_ObjSize( pObjLog );
     nNodes++;
@@ -530,7 +530,7 @@ Emb_Man_t * Emb_ManStart( Gia_Man_t * pGia )
         pObjLog = Emb_ManObj( p, hHandle );
         pObjLog->hHandle  = hHandle;
         pObjLog->nFanins  = Gia_ObjIsRo( pGia, pObj );
-        pObjLog->nFanouts = Gia_ObjRefs( pGia, pObj );
+        pObjLog->nFanouts = Gia_ObjRefNum( pGia, pObj );
         pObjLog->fCi = 1;
         // count objects
         hHandle += Emb_ObjSize( pObjLog );
@@ -543,17 +543,17 @@ Emb_Man_t * Emb_ManStart( Gia_Man_t * pGia )
     {
         if ( pObj->fMark0 == 0 )
         {
-            assert( Gia_ObjRefs( pGia, pObj ) == 0 );
+            assert( Gia_ObjRefNum( pGia, pObj ) == 0 );
             continue;
         }
-        assert( Gia_ObjRefs( pGia, pObj ) > 0 );
+        assert( Gia_ObjRefNum( pGia, pObj ) > 0 );
         Emb_ManCollectSuper( pGia, pObj, vSuper, vVisit );
         // create node object
         pObj->Value = hHandle;
         pObjLog = Emb_ManObj( p, hHandle );
         pObjLog->hHandle  = hHandle;
         pObjLog->nFanins  = Vec_IntSize( vSuper );
-        pObjLog->nFanouts = Gia_ObjRefs( pGia, pObj );
+        pObjLog->nFanouts = Gia_ObjRefNum( pGia, pObj );
         // add fanins
         Gia_ManForEachObjVec( vSuper, pGia, pFanin, k )
         {
diff --git a/src/aig/gia/giaEnable.c b/src/aig/gia/giaEnable.c
index f2fbd123..9cb0dce5 100644
--- a/src/aig/gia/giaEnable.c
+++ b/src/aig/gia/giaEnable.c
@@ -110,7 +110,7 @@ void Gia_ManPrintSignals( Gia_Man_t * p, int * pFreq, char * pStr )
         if ( pFreq[i] > 10 )
         {
             printf( "%3d :   Obj = %6d   Refs = %6d   Freq = %6d\n", 
-                ++Counter, i, Gia_ObjRefs(p, Gia_ManObj(p,i)), pFreq[i] );
+                ++Counter, i, Gia_ObjRefNum(p, Gia_ManObj(p,i)), pFreq[i] );
             Vec_IntPush( vObjs, i );
         }
     Vec_IntFree( vObjs );
diff --git a/src/aig/gia/giaForce.c b/src/aig/gia/giaForce.c
index a32e71b4..d37fa455 100644
--- a/src/aig/gia/giaForce.c
+++ b/src/aig/gia/giaForce.c
@@ -168,7 +168,7 @@ Frc_Man_t * Frc_ManStartSimple( Gia_Man_t * pGia )
     pObjLog = Frc_ManObj( p, hHandle );
     pObjLog->hHandle  = hHandle;
     pObjLog->nFanins  = 0;
-    pObjLog->nFanouts = Gia_ObjRefs( pGia, Gia_ManConst0(pGia) );
+    pObjLog->nFanouts = Gia_ObjRefNum( pGia, Gia_ManConst0(pGia) );
     // count objects
     hHandle += Frc_ObjSize( pObjLog );
     nNodes = 1;
@@ -182,7 +182,7 @@ Frc_Man_t * Frc_ManStartSimple( Gia_Man_t * pGia )
         pObjLog = Frc_ManObj( p, hHandle );
         pObjLog->hHandle  = hHandle;
         pObjLog->nFanins  = 0;
-        pObjLog->nFanouts = Gia_ObjRefs( pGia, pObj );
+        pObjLog->nFanouts = Gia_ObjRefNum( pGia, pObj );
         pObjLog->fCi = 0;
         // count objects
         hHandle += Frc_ObjSize( pObjLog );
@@ -191,13 +191,13 @@ Frc_Man_t * Frc_ManStartSimple( Gia_Man_t * pGia )
     // create internal nodes
     Gia_ManForEachAnd( pGia, pObj, i )
     {
-        assert( Gia_ObjRefs( pGia, pObj ) > 0 );
+        assert( Gia_ObjRefNum( pGia, pObj ) > 0 );
         // create node object
         pObj->Value = hHandle;
         pObjLog = Frc_ManObj( p, hHandle );
         pObjLog->hHandle  = hHandle;
         pObjLog->nFanins  = 2;
-        pObjLog->nFanouts = Gia_ObjRefs( pGia, pObj );
+        pObjLog->nFanouts = Gia_ObjRefNum( pGia, pObj );
         // add fanins
         pFanLog = Frc_ManObj( p, Gia_ObjValue(Gia_ObjFanin0(pObj)) ); 
         Frc_ObjAddFanin( pObjLog, pFanLog );
@@ -341,7 +341,7 @@ void Frc_ManCreateRefsSpecial( Gia_Man_t * p )
             Gia_ObjRefDec( p, Gia_Regular(pObjD0) );
     }
     Gia_ManForEachAnd( p, pObj, i )
-        assert( Gia_ObjRefs(p, pObj) > 0 );
+        assert( Gia_ObjRefNum(p, pObj) > 0 );
     Gia_ManCleanMark0( p );
 }
 
@@ -371,7 +371,7 @@ void Frc_ManTransformRefs( Gia_Man_t * p, int * pnObjs, int * pnFanios )
         pObj->fMark0 = 1;
     // mark those nodes that have ref count more than 1
     Gia_ManForEachAnd( p, pObj, i )
-        pObj->fMark0 = (Gia_ObjRefs(p, pObj) > 1);
+        pObj->fMark0 = (Gia_ObjRefNum(p, pObj) > 1);
     // mark the output drivers
     Gia_ManForEachCoDriver( p, pObj, i )
         pObj->fMark0 = 1;
@@ -451,7 +451,7 @@ Frc_Man_t * Frc_ManStart( Gia_Man_t * pGia )
     pObjLog = Frc_ManObj( p, hHandle );
     pObjLog->hHandle  = hHandle;
     pObjLog->nFanins  = 0;
-    pObjLog->nFanouts = Gia_ObjRefs( pGia, Gia_ManConst0(pGia) );
+    pObjLog->nFanouts = Gia_ObjRefNum( pGia, Gia_ManConst0(pGia) );
     // count objects
     hHandle += Frc_ObjSize( pObjLog );
     nNodes++;
@@ -465,7 +465,7 @@ Frc_Man_t * Frc_ManStart( Gia_Man_t * pGia )
         pObjLog = Frc_ManObj( p, hHandle );
         pObjLog->hHandle  = hHandle;
         pObjLog->nFanins  = 0;
-        pObjLog->nFanouts = Gia_ObjRefs( pGia, pObj );
+        pObjLog->nFanouts = Gia_ObjRefNum( pGia, pObj );
         pObjLog->fCi = 1;
         // count objects
         hHandle += Frc_ObjSize( pObjLog );
@@ -478,17 +478,17 @@ Frc_Man_t * Frc_ManStart( Gia_Man_t * pGia )
     {
         if ( pObj->fMark0 == 0 )
         {
-            assert( Gia_ObjRefs( pGia, pObj ) == 0 );
+            assert( Gia_ObjRefNum( pGia, pObj ) == 0 );
             continue;
         }
-        assert( Gia_ObjRefs( pGia, pObj ) > 0 );
+        assert( Gia_ObjRefNum( pGia, pObj ) > 0 );
         Frc_ManCollectSuper( pGia, pObj, vSuper, vVisit );
         // create node object
         pObj->Value = hHandle;
         pObjLog = Frc_ManObj( p, hHandle );
         pObjLog->hHandle  = hHandle;
         pObjLog->nFanins  = Vec_IntSize( vSuper );
-        pObjLog->nFanouts = Gia_ObjRefs( pGia, pObj );
+        pObjLog->nFanouts = Gia_ObjRefNum( pGia, pObj );
         // add fanins
         Gia_ManForEachObjVec( vSuper, pGia, pFanin, k )
         {
diff --git a/src/aig/gia/giaFront.c b/src/aig/gia/giaFront.c
index 08fd6081..322da785 100644
--- a/src/aig/gia/giaFront.c
+++ b/src/aig/gia/giaFront.c
@@ -112,7 +112,7 @@ Gia_Man_t * Gia_ManFront( Gia_Man_t * p )
     int nCrossCutMaxInit = Gia_ManCrossCut( p );
     int iFront = 0;//, clk = clock(); 
     // set references for all objects
-    Gia_ManSetRefs( p );
+    Gia_ManCreateValueRefs( p );
     // start the new manager
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
     pNew->pName = Abc_UtilStrsav( p->pName );
diff --git a/src/aig/gia/giaIf.c b/src/aig/gia/giaIf.c
index 3fc5c04e..13e4f429 100644
--- a/src/aig/gia/giaIf.c
+++ b/src/aig/gia/giaIf.c
@@ -153,7 +153,7 @@ If_Man_t * Gia_ManToIf( Gia_Man_t * p, If_Par_t * pPars, Vec_Ptr_t * vAigToIf )
         // set up the choice node
 /*
 //        if ( p->pReprs && p->pNexts && Gia_ObjIsHead( p, i ) )
-        if ( p->pNexts && Gia_ObjNext(p, i) && Gia_ObjRefsId(p, i) )
+        if ( p->pNexts && Gia_ObjNext(p, i) && Gia_ObjRefNumId(p, i) )
         {
             int iPrev, iFanin;
             pIfMan->nChoices++;
@@ -509,7 +509,7 @@ void Gia_ManPrintNpnClasses( Gia_Man_t * p )
         Gia_LutForEachFanin( p, i, iFan, k )
         {
             Counter  += (pLutClass[iFan] == 109);
-            Counter2 += (pLutClass[iFan] == 109) && (Gia_ObjRefsId(p, iFan) == 1);
+            Counter2 += (pLutClass[iFan] == 109) && (Gia_ObjRefNumId(p, iFan) == 1);
         }
         OtherClasses  += (Counter > 1);
         OtherClasses2 += (Counter2 > 1);
diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c
index e7b831bd..f78ea847 100644
--- a/src/aig/gia/giaMan.c
+++ b/src/aig/gia/giaMan.c
@@ -108,7 +108,7 @@ void Gia_ManStop( Gia_Man_t * p )
     ABC_FREE( p->pReprs );
     ABC_FREE( p->pNexts );
     ABC_FREE( p->pRefs );
-    ABC_FREE( p->pNodeRefs );
+//    ABC_FREE( p->pNodeRefs );
     ABC_FREE( p->pHTable );
     ABC_FREE( p->pObjs );
     ABC_FREE( p->pSpec );
diff --git a/src/aig/gia/giaSat.c b/src/aig/gia/giaSat.c
index 4f8a6acb..9bea8ef7 100644
--- a/src/aig/gia/giaSat.c
+++ b/src/aig/gia/giaSat.c
@@ -358,7 +358,7 @@ void Gia_ManSatExperiment( Gia_Man_t * p )
     int nWords = 0, nWords2 = 0;
     pMan = Gia_ManSatStart();
     // mark the nodes to become roots of leaf-DAGs
-    Gia_ManSetRefs( p );
+    Gia_ManCreateValueRefs( p );
     Gia_ManForEachObj( p, pObj, i )
     {
         pObj->fMark0 = 0;
diff --git a/src/aig/gia/giaSwitch.c b/src/aig/gia/giaSwitch.c
index 63c1ff9f..8bf027a4 100644
--- a/src/aig/gia/giaSwitch.c
+++ b/src/aig/gia/giaSwitch.c
@@ -720,7 +720,7 @@ float Gia_ManEvaluateSwitching( Gia_Man_t * p )
     ABC_FREE( p->pRefs );
     Gia_ManCreateRefs( p );
     Gia_ManForEachObj( p, pObj, i )
-        SwitchTotal += (float)Gia_ObjRefs(p, pObj) * p->pSwitching[i] / 255;
+        SwitchTotal += (float)Gia_ObjRefNum(p, pObj) * p->pSwitching[i] / 255;
     return SwitchTotal;
 }
 
@@ -777,9 +777,9 @@ float Gia_ManComputeSwitching( Gia_Man_t * p, int nFrames, int nPref, int fProbO
         pObjDfs = Gia_ObjFromLit( pDfs, pObj->Value );
         Switch = pSwitching[ Gia_ObjId(pDfs, pObjDfs) ];
         p->pSwitching[i] = (char)((Switch >= 1.0) ? 255 : (int)((0.002 + Switch) * 255)); // 0.00196 = (1/255)/2
-        SwitchTotal += (float)Gia_ObjRefs(p, pObj) * p->pSwitching[i] / 255;
-//        SwitchTotal2 += Gia_ObjRefs(p, pObj) * Switch;
-//        printf( "%d = %.2f\n", i, Gia_ObjRefs(p, pObj) * Switch );
+        SwitchTotal += (float)Gia_ObjRefNum(p, pObj) * p->pSwitching[i] / 255;
+//        SwitchTotal2 += Gia_ObjRefNum(p, pObj) * Switch;
+//        printf( "%d = %.2f\n", i, Gia_ObjRefNum(p, pObj) * Switch );
     }
 //    printf( "\nSwitch float = %f. Switch char = %f.\n", SwitchTotal2, SwitchTotal );
     Vec_IntFree( vSwitching );
diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c
index 2898488f..da713aa0 100644
--- a/src/aig/gia/giaUtil.c
+++ b/src/aig/gia/giaUtil.c
@@ -465,7 +465,7 @@ int Gia_ManLevelNum( Gia_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Gia_ManSetRefs( Gia_Man_t * p )  
+void Gia_ManCreateValueRefs( Gia_Man_t * p )  
 {
     Gia_Obj_t * pObj;
     int i;
@@ -554,7 +554,7 @@ int Gia_ManCrossCut( Gia_Man_t * p )
 {
     Gia_Obj_t * pObj;
     int i, nCutCur = 0, nCutMax = 0;
-    Gia_ManSetRefs( p );
+    Gia_ManCreateValueRefs( p );
     Gia_ManForEachObj( p, pObj, i )
     {
         if ( pObj->Value )
@@ -810,11 +810,11 @@ int Gia_NodeDeref_rec( Gia_Man_t * p, Gia_Obj_t * pNode )
         return 0;
     assert( Gia_ObjIsAnd(pNode) );
     pFanin = Gia_ObjFanin0(pNode);
-    assert( Gia_ObjRefs(p, pFanin) > 0 );
+    assert( Gia_ObjRefNum(p, pFanin) > 0 );
     if ( Gia_ObjRefDec(p, pFanin) == 0 )
         Counter += Gia_NodeDeref_rec( p, pFanin );
     pFanin = Gia_ObjFanin1(pNode);
-    assert( Gia_ObjRefs(p, pFanin) > 0 );
+    assert( Gia_ObjRefNum(p, pFanin) > 0 );
     if ( Gia_ObjRefDec(p, pFanin) == 0 )
         Counter += Gia_NodeDeref_rec( p, pFanin );
     return Counter + 1;
@@ -1027,7 +1027,7 @@ void Gia_ObjPrint( Gia_Man_t * p, Gia_Obj_t * pObj )
             Gia_ObjFaninId0p(p, pObj), (Gia_ObjFaninC0(pObj)? "\'" : " "), 
             Gia_ObjFaninId1p(p, pObj), (Gia_ObjFaninC1(pObj)? "\'" : " ") );
     if ( p->pRefs )
-        printf( " (refs = %3d)", Gia_ObjRefs(p, pObj) );
+        printf( " (refs = %3d)", Gia_ObjRefNum(p, pObj) );
     printf( "\n" );
 /*
     if ( p->pRefs )
diff --git a/src/base/cmd/cmdPlugin.c b/src/base/cmd/cmdPlugin.c
index 93eee5b8..b89238fc 100644
--- a/src/base/cmd/cmdPlugin.c
+++ b/src/base/cmd/cmdPlugin.c
@@ -301,7 +301,7 @@ Vec_Int_t * Abc_ManExpandCex( Gia_Man_t * pGia, Vec_Int_t * vCex )
     {
         Gia_ManForEachPi( pGia, pObj, i )
         {
-            if ( Gia_ObjRefs(pGia, pObj) == 0 )
+            if ( Gia_ObjRefNum(pGia, pObj) == 0 )
                 Vec_IntPush( vCexNew, 0 );
             else
             {
diff --git a/src/opt/nwk/nwkAig.c b/src/opt/nwk/nwkAig.c
index 5b0aaf20..b70c71fc 100644
--- a/src/opt/nwk/nwkAig.c
+++ b/src/opt/nwk/nwkAig.c
@@ -165,12 +165,12 @@ Nwk_Man_t * Nwk_ManCreateFromGia( Gia_Man_t * p, Vec_Int_t * vPPis, Vec_Int_t *
     ppCopies = ABC_ALLOC( Nwk_Obj_t *, Gia_ManObjNum(p) );
     // copy objects
     pObj = Gia_ManConst0(p);
-//    ppCopies[Gia_ObjId(p,pObj)] = Nwk_ManCreateNode( pNtk, 0, Gia_ObjRefs(p,pObj) );
-    ppCopies[Gia_ObjId(p,pObj)] = Nwk_ManCreateNode( pNtk, 0, Gia_ObjRefs(p,pObj) + (Vec_IntSize(vLeaves) > Vec_IntSize(vPPis) ? Vec_IntSize(vLeaves) - Vec_IntSize(vPPis) : 0) );
+//    ppCopies[Gia_ObjId(p,pObj)] = Nwk_ManCreateNode( pNtk, 0, Gia_ObjRefNum(p,pObj) );
+    ppCopies[Gia_ObjId(p,pObj)] = Nwk_ManCreateNode( pNtk, 0, Gia_ObjRefNum(p,pObj) + (Vec_IntSize(vLeaves) > Vec_IntSize(vPPis) ? Vec_IntSize(vLeaves) - Vec_IntSize(vPPis) : 0) );
     Vec_IntPush( vMaps, Gia_ObjId(p,pObj) );
     Gia_ManForEachObjVec( vLeaves, p, pObj, i )
     {
-        ppCopies[Gia_ObjId(p,pObj)] = Nwk_ManCreateCi( pNtk, Gia_ObjRefs(p,pObj) );
+        ppCopies[Gia_ObjId(p,pObj)] = Nwk_ManCreateCi( pNtk, Gia_ObjRefNum(p,pObj) );
         assert( Vec_IntSize(vMaps) == Nwk_ObjId(ppCopies[Gia_ObjId(p,pObj)]) );
         Vec_IntPush( vMaps, Gia_ObjId(p,pObj) );
     }
@@ -181,7 +181,7 @@ Nwk_Man_t * Nwk_ManCreateFromGia( Gia_Man_t * p, Vec_Int_t * vPPis, Vec_Int_t *
     }
     Gia_ManForEachObjVec( vNodes, p, pObj, i )
     {
-        ppCopies[Gia_ObjId(p,pObj)] = Nwk_ManCreateNode( pNtk, 2, Gia_ObjRefs(p,pObj) );
+        ppCopies[Gia_ObjId(p,pObj)] = Nwk_ManCreateNode( pNtk, 2, Gia_ObjRefNum(p,pObj) );
         Nwk_ObjAddFanin( ppCopies[Gia_ObjId(p,pObj)], ppCopies[Gia_ObjFaninId0p(p,pObj)] );
         Nwk_ObjAddFanin( ppCopies[Gia_ObjId(p,pObj)], ppCopies[Gia_ObjFaninId1p(p,pObj)] );
         assert( Vec_IntSize(vMaps) == Nwk_ObjId(ppCopies[Gia_ObjId(p,pObj)]) );
diff --git a/src/proof/abs/absRpm.c b/src/proof/abs/absRpm.c
index b0dc1665..3d5b2ac3 100644
--- a/src/proof/abs/absRpm.c
+++ b/src/proof/abs/absRpm.c
@@ -93,7 +93,7 @@ void Gia_ManComputeDoms( Gia_Man_t * p )
     {
         if ( i == 0 || Gia_ObjIsCi(pObj) )
             continue;
-        if ( pObj->fMark1 || (p->pRefs && Gia_ObjIsAnd(pObj) && Gia_ObjRefs(p, pObj) == 0) )
+        if ( pObj->fMark1 || (p->pRefs && Gia_ObjIsAnd(pObj) && Gia_ObjRefNum(p, pObj) == 0) )
             continue;
         if ( Gia_ObjIsCo(pObj) )
         {
@@ -173,7 +173,7 @@ Vec_Int_t * Gia_ManCollectDoms( Gia_Man_t * p )
     {
         if ( !pObj->fMark1 )
             continue;
-        if ( p->pRefs && Gia_ObjRefs(p, pObj) == 0 )
+        if ( p->pRefs && Gia_ObjRefNum(p, pObj) == 0 )
             continue;
         iDom = Gia_ObjDom(p, pObj);
         if ( iDom == -1 )
@@ -238,7 +238,7 @@ void Gia_ManCountFanoutlessFlops( Gia_Man_t * p )
     int Counter = 0;
     Gia_ManCreateRefs( p );
     Gia_ManForEachRo( p, pObj, i )
-        if ( Gia_ObjRefs(p, pObj) == 0 )
+        if ( Gia_ObjRefNum(p, pObj) == 0 )
             Counter++;
     printf( "Fanoutless flops = %d.\n", Counter );
     ABC_FREE( p->pRefs );
@@ -305,11 +305,11 @@ int Abs_GiaObjDeref_rec( Gia_Man_t * p, Gia_Obj_t * pNode )
         return 0;
     assert( Gia_ObjIsAnd(pNode) );
     pFanin = Gia_ObjFanin0(pNode);
-    assert( Gia_ObjRefs(p, pFanin) > 0 );
+    assert( Gia_ObjRefNum(p, pFanin) > 0 );
     if ( Gia_ObjRefDec(p, pFanin) == 0 )
         Counter += Abs_GiaObjDeref_rec( p, pFanin );
     pFanin = Gia_ObjFanin1(pNode);
-    assert( Gia_ObjRefs(p, pFanin) > 0 );
+    assert( Gia_ObjRefNum(p, pFanin) > 0 );
     if ( Gia_ObjRefDec(p, pFanin) == 0 )
         Counter += Abs_GiaObjDeref_rec( p, pFanin );
     return Counter + 1;
@@ -347,14 +347,14 @@ int Abs_GiaSortNodes( Gia_Man_t * p, Vec_Int_t * vSupp )
     int nSize = Vec_IntSize(vSupp);
     int i, RetValue;
     Gia_ManForEachObjVec( vSupp, p, pObj, i )
-        if ( i < nSize && Gia_ObjRefs(p, pObj) == 0 && !Gia_ObjIsRo(p, pObj) ) // add removable leaves
+        if ( i < nSize && Gia_ObjRefNum(p, pObj) == 0 && !Gia_ObjIsRo(p, pObj) ) // add removable leaves
         {
             assert( pObj->fMark1 );
             Vec_IntPush( vSupp, Gia_ObjId(p, pObj) );
         }
     RetValue = Vec_IntSize(vSupp) - nSize;
     Gia_ManForEachObjVec( vSupp, p, pObj, i )
-        if ( i < nSize && !(Gia_ObjRefs(p, pObj) == 0 && !Gia_ObjIsRo(p, pObj)) ) // add non-removable leaves
+        if ( i < nSize && !(Gia_ObjRefNum(p, pObj) == 0 && !Gia_ObjIsRo(p, pObj)) ) // add non-removable leaves
             Vec_IntPush( vSupp, Gia_ObjId(p, pObj) );
     assert( Vec_IntSize(vSupp) == 2 * nSize );
     memmove( Vec_IntArray(vSupp), Vec_IntArray(vSupp) + nSize, sizeof(int) * nSize );
@@ -413,7 +413,7 @@ void Abs_ManSupport2_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSupp )
     if ( Gia_ObjIsTravIdCurrent(p, pObj) )
         return;
     Gia_ObjSetTravIdCurrent(p, pObj);
-    if ( pObj->fMark1 || Gia_ObjIsRo(p, pObj) || Gia_ObjRefs(p, pObj) > 0 )
+    if ( pObj->fMark1 || Gia_ObjIsRo(p, pObj) || Gia_ObjRefNum(p, pObj) > 0 )
     {
         Vec_IntPush( vSupp, Gia_ObjId(p, pObj) );
         return;
@@ -464,7 +464,7 @@ int Abs_ManSupport3( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSupp )
             if ( !Gia_ObjIsAnd(pTemp) )
                 continue;
             assert( !pTemp->fMark1 );
-            assert( Gia_ObjRefs(p, pTemp) > 0 );
+            assert( Gia_ObjRefNum(p, pTemp) > 0 );
             pFan0 = Gia_ObjFanin0(pTemp);
             pFan1 = Gia_ObjFanin1(pTemp);
             if ( Gia_ObjIsTravIdCurrent(p, pFan0) && Gia_ObjIsTravIdCurrent(p, pFan1) )
@@ -630,7 +630,7 @@ void Abs_RpmPerformMark( Gia_Man_t * p, int nCutMax, int fVerbose, int fVeryVerb
         Gia_ManForEachObjVec( vDoms, p, pObj, i )
         {
             assert( !pObj->fMark1 );
-            assert( Gia_ObjRefs( p, pObj ) > 0 );
+            assert( Gia_ObjRefNum( p, pObj ) > 0 );
             // dereference root node
             nNodes = Abs_GiaObjDeref_rec( p, pObj );
 /*
diff --git a/src/proof/cec/cecClass.c b/src/proof/cec/cecClass.c
index 46e585a9..2d820c39 100644
--- a/src/proof/cec/cecClass.c
+++ b/src/proof/cec/cecClass.c
@@ -857,7 +857,7 @@ int Cec_ManSimClassesPrepare( Cec_ManSim_t * p, int LevelMax )
     p->pAig->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p->pAig) );
     p->pAig->pNexts = ABC_CALLOC( int, Gia_ManObjNum(p->pAig) );
     // create references
-    Gia_ManSetRefs( p->pAig );
+    Gia_ManCreateValueRefs( p->pAig );
     // set starting representative of internal nodes to be constant 0
     if ( p->pPars->fLatchCorr )
         Gia_ManForEachObj( p->pAig, pObj, i )
@@ -908,7 +908,7 @@ int Cec_ManSimClassesPrepare( Cec_ManSim_t * p, int LevelMax )
 int Cec_ManSimClassesRefine( Cec_ManSim_t * p )
 {
     int i;
-    Gia_ManSetRefs( p->pAig );
+    Gia_ManCreateValueRefs( p->pAig );
     p->nWords = p->pPars->nWords;
     for ( i = 0; i < p->pPars->nRounds; i++ )
     {
diff --git a/src/proof/cec/cecCorr.c b/src/proof/cec/cecCorr.c
index 300c10d5..f35cd952 100644
--- a/src/proof/cec/cecCorr.c
+++ b/src/proof/cec/cecCorr.c
@@ -548,7 +548,7 @@ int Cec_ManResimulateCounterExamples( Cec_ManSim_t * pSim, Vec_Int_t * vCexStore
     Vec_Ptr_t * vSimInfo; 
     int RetValue = 0, iStart = 0;
     vPairs = Gia_ManCorrCreateRemapping( pSim->pAig );
-    Gia_ManSetRefs( pSim->pAig );
+    Gia_ManCreateValueRefs( pSim->pAig );
 //    pSim->pPars->nWords  = 63;
     pSim->pPars->nFrames = nFrames;
     vSimInfo = Vec_PtrAllocSimInfo( Gia_ManRegNum(pSim->pAig) + Gia_ManPiNum(pSim->pAig) * nFrames, pSim->pPars->nWords );
@@ -584,7 +584,7 @@ int Cec_ManResimulateCounterExamplesComb( Cec_ManSim_t * pSim, Vec_Int_t * vCexS
 { 
     Vec_Ptr_t * vSimInfo; 
     int RetValue = 0, iStart = 0;
-    Gia_ManSetRefs( pSim->pAig );
+    Gia_ManCreateValueRefs( pSim->pAig );
     pSim->pPars->nFrames = 1;
     vSimInfo = Vec_PtrAllocSimInfo( Gia_ManCiNum(pSim->pAig), pSim->pPars->nWords );
     while ( iStart < Vec_IntSize(vCexStore) )
diff --git a/src/proof/cec/cecSeq.c b/src/proof/cec/cecSeq.c
index 3afbd1c8..da60de1d 100644
--- a/src/proof/cec/cecSeq.c
+++ b/src/proof/cec/cecSeq.c
@@ -191,7 +191,7 @@ int Cec_ManSeqResimulateInfo( Gia_Man_t * pAig, Vec_Ptr_t * vSimInfo, Abc_Cex_t
     pParsSim->nFrames = (Vec_PtrSize(vSimInfo) - Gia_ManRegNum(pAig)) / Gia_ManPiNum(pAig);
     pParsSim->nWords  = Vec_PtrReadWordsSimInfo( vSimInfo );
     pParsSim->fCheckMiter = fCheckMiter;
-    Gia_ManSetRefs( pAig );
+    Gia_ManCreateValueRefs( pAig );
     pSim = Cec_ManSimStart( pAig, pParsSim );
     if ( pBestState )
         pSim->pBestState = pBestState;
diff --git a/src/proof/cec/cecSweep.c b/src/proof/cec/cecSweep.c
index 16697776..9ba2e07e 100644
--- a/src/proof/cec/cecSweep.c
+++ b/src/proof/cec/cecSweep.c
@@ -197,7 +197,7 @@ p->timePat += clock() - clk;
 clk = clock();
     if ( vInfo != NULL )
     {
-        Gia_ManSetRefs( p->pAig );
+        Gia_ManCreateValueRefs( p->pAig );
         for ( i = 0; i < pPat->nSeries; i++ )
         {
             Cec_ManFraCreateInfo( pSim, pSim->vCiSimInfo, vInfo, i );