Renamed Aig_ManForEachPi/Po to be ...Ci/Co and Aig_ObjCreatePi/Po to be ...Ci/Co.

50 files changed, 263 insertions, 263 deletions

diff --git a/src/proof/bbr/bbrNtbdd.c b/src/proof/bbr/bbrNtbdd.c
index 09456df0..49c2873b 100644
--- a/src/proof/bbr/bbrNtbdd.c
+++ b/src/proof/bbr/bbrNtbdd.c
@@ -136,7 +136,7 @@ int Aig_ManSizeOfGlobalBdds( Aig_Man_t * p )
     int RetValue, i;
     // complement the global functions
     vFuncsGlob = Vec_PtrAlloc( Aig_ManPoNum(p) );
-    Aig_ManForEachPo( p, pObj, i )
+    Aig_ManForEachCo( p, pObj, i )
         Vec_PtrPush( vFuncsGlob, Aig_ObjGlobalBdd(pObj) );
     RetValue = Cudd_SharingSize( (DdNode **)Vec_PtrArray(vFuncsGlob), Vec_PtrSize(vFuncsGlob) );
     Vec_PtrFree( vFuncsGlob );
@@ -171,7 +171,7 @@ DdManager * Aig_ManComputeGlobalBdds( Aig_Man_t * p, int nBddSizeMax, int fDropI
     // assign the constant node BDD
     Aig_ObjSetGlobalBdd( Aig_ManConst1(p), dd->one );   Cudd_Ref( dd->one );
     // set the elementary variables
-    Aig_ManForEachPi( p, pObj, i )
+    Aig_ManForEachCi( p, pObj, i )
     {
         Aig_ObjSetGlobalBdd( pObj, dd->vars[i] );  Cudd_Ref( dd->vars[i] );
     }
@@ -180,7 +180,7 @@ DdManager * Aig_ManComputeGlobalBdds( Aig_Man_t * p, int nBddSizeMax, int fDropI
     Counter = 0;
     // construct the BDDs
 //    pProgress = Extra_ProgressBarStart( stdout, Aig_ManNodeNum(p) );
-    Aig_ManForEachPo( p, pObj, i )
+    Aig_ManForEachCo( p, pObj, i )
     {
         bFunc = Bbr_NodeGlobalBdds_rec( dd, Aig_ObjFanin0(pObj), nBddSizeMax, fDropInternal, pProgress, &Counter, fVerbose );
         if ( bFunc == NULL )
diff --git a/src/proof/dch/dchAig.c b/src/proof/dch/dchAig.c
index 91a00c63..59828443 100644
--- a/src/proof/dch/dchAig.c
+++ b/src/proof/dch/dchAig.c
@@ -83,21 +83,21 @@ Aig_Man_t * Dch_DeriveTotalAig( Vec_Ptr_t * vAigs )
     Vec_PtrForEachEntry( Aig_Man_t *, vAigs, pAig2, k )
         Aig_ManConst1(pAig2)->pData = Aig_ManConst1(pAigTotal);
     // map primary inputs
-    Aig_ManForEachPi( pAig, pObj, i )
+    Aig_ManForEachCi( pAig, pObj, i )
     {
-        pObjPi = Aig_ObjCreatePi( pAigTotal );
+        pObjPi = Aig_ObjCreateCi( pAigTotal );
         Vec_PtrForEachEntry( Aig_Man_t *, vAigs, pAig2, k )
             Aig_ManPi( pAig2, i )->pData = pObjPi;
     }
     // construct the AIG in the order of POs
-    Aig_ManForEachPo( pAig, pObj, i )
+    Aig_ManForEachCo( pAig, pObj, i )
     {
         Vec_PtrForEachEntry( Aig_Man_t *, vAigs, pAig2, k )
         {
             pObjPo = Aig_ManPo( pAig2, i );
             Dch_DeriveTotalAig_rec( pAigTotal, Aig_ObjFanin0(pObjPo) );
         }
-        Aig_ObjCreatePo( pAigTotal, Aig_ObjChild0Copy(pObj) );
+        Aig_ObjCreateCo( pAigTotal, Aig_ObjChild0Copy(pObj) );
     }
 /*
     // mark the cone of the first AIG
diff --git a/src/proof/dch/dchChoice.c b/src/proof/dch/dchChoice.c
index 1772f8aa..1de11509 100644
--- a/src/proof/dch/dchChoice.c
+++ b/src/proof/dch/dchChoice.c
@@ -255,14 +255,14 @@ Aig_Man_t * Dch_DeriveChoiceAig_old( Aig_Man_t * pAig )
     // map constants and PIs
     Aig_ManCleanData( pAig );
     Aig_ManConst1(pAig)->pData = Aig_ManConst1(pChoices);
-    Aig_ManForEachPi( pAig, pObj, i )
-        pObj->pData = Aig_ObjCreatePi( pChoices );
+    Aig_ManForEachCi( pAig, pObj, i )
+        pObj->pData = Aig_ObjCreateCi( pChoices );
     // construct choices for the internal nodes
     assert( pAig->pReprs != NULL );
     Aig_ManForEachNode( pAig, pObj, i )
         Dch_DeriveChoiceAigNode( pChoices, pAig, pObj );
-    Aig_ManForEachPo( pAig, pObj, i )
-        Aig_ObjCreatePo( pChoices, Aig_ObjChild0CopyRepr(pChoices, pObj) );
+    Aig_ManForEachCo( pAig, pObj, i )
+        Aig_ObjCreateCo( pChoices, Aig_ObjChild0CopyRepr(pChoices, pObj) );
     Dch_DeriveChoiceCountEquivs( pChoices );
     // there is no need for cleanup
     ABC_FREE( pChoices->pReprs );
@@ -384,7 +384,7 @@ int Aig_ManCheckAcyclic( Aig_Man_t * p, int fVerbose )
     // pNode->TravId <  pNet->nTravIds - 1  means "pNode is not visited"
     // traverse the network to detect cycles
     fAcyclic = 1;
-    Aig_ManForEachPo( p, pNode, i )
+    Aig_ManForEachCo( p, pNode, i )
     {
         pNode = Aig_ObjFanin0(pNode);
         if ( Aig_ObjIsTravIdPrevious(p, pNode) )
@@ -454,14 +454,14 @@ Aig_Man_t * Dch_DeriveChoiceAigInt( Aig_Man_t * pAig )
     // map constants and PIs
     Aig_ManCleanData( pAig );
     Aig_ManConst1(pAig)->pData = Aig_ManConst1(pChoices);
-    Aig_ManForEachPi( pAig, pObj, i )
-        pObj->pData = Aig_ObjCreatePi( pChoices );
+    Aig_ManForEachCi( pAig, pObj, i )
+        pObj->pData = Aig_ObjCreateCi( pChoices );
     // construct choices for the internal nodes
     assert( pAig->pReprs != NULL );
     Aig_ManForEachNode( pAig, pObj, i )
         Dch_DeriveChoiceAigNode( pChoices, pAig, pObj );
-    Aig_ManForEachPo( pAig, pObj, i )
-        Aig_ObjCreatePo( pChoices, Aig_ObjChild0CopyRepr(pChoices, pObj) );
+    Aig_ManForEachCo( pAig, pObj, i )
+        Aig_ObjCreateCo( pChoices, Aig_ObjChild0CopyRepr(pChoices, pObj) );
     Dch_DeriveChoiceCountEquivs( pChoices );
     Aig_ManSetRegNum( pChoices, Aig_ManRegNum(pAig) );
     return pChoices;
diff --git a/src/proof/dch/dchSim.c b/src/proof/dch/dchSim.c
index b2d24761..3e7c575b 100644
--- a/src/proof/dch/dchSim.c
+++ b/src/proof/dch/dchSim.c
@@ -211,7 +211,7 @@ void Dch_PerformRandomSimulation( Aig_Man_t * pAig, Vec_Ptr_t * vSims )
     memset( pSim, 0xff, sizeof(unsigned) * nWords );
 
     // assign primary input random sim info
-    Aig_ManForEachPi( pAig, pObj, i )
+    Aig_ManForEachCi( pAig, pObj, i )
     {
         pSim = Dch_ObjSim( vSims, pObj );
         for ( k = 0; k < nWords; k++ )
diff --git a/src/proof/dch/dchSweep.c b/src/proof/dch/dchSweep.c
index a1c4f79b..dafab06e 100644
--- a/src/proof/dch/dchSweep.c
+++ b/src/proof/dch/dchSweep.c
@@ -112,8 +112,8 @@ void Dch_ManSweep( Dch_Man_t * p )
     p->pAigFraig = Aig_ManStart( Aig_ManObjNumMax(p->pAigTotal) );
     Aig_ManCleanData( p->pAigTotal );
     Aig_ManConst1(p->pAigTotal)->pData = Aig_ManConst1(p->pAigFraig);
-    Aig_ManForEachPi( p->pAigTotal, pObj, i )
-        pObj->pData = Aig_ObjCreatePi( p->pAigFraig );
+    Aig_ManForEachCi( p->pAigTotal, pObj, i )
+        pObj->pData = Aig_ObjCreateCi( p->pAigFraig );
     // sweep internal nodes
     pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pAigTotal) );
     Aig_ManForEachNode( p->pAigTotal, pObj, i )
diff --git a/src/proof/fra/fraBmc.c b/src/proof/fra/fraBmc.c
index 7b4db3de..b0dd3c86 100644
--- a/src/proof/fra/fraBmc.c
+++ b/src/proof/fra/fraBmc.c
@@ -250,7 +250,7 @@ Aig_Man_t * Fra_BmcFrames( Fra_Bmc_t * p, int fKeepPos )
         Bmc_ObjSetFrames( Aig_ManConst1(p->pAig), f, Aig_ManConst1(pAigFrames) );
     for ( f = 0; f < p->nFramesAll; f++ )
         Aig_ManForEachPiSeq( p->pAig, pObj, i )
-            Bmc_ObjSetFrames( pObj, f, Aig_ObjCreatePi(pAigFrames) );
+            Bmc_ObjSetFrames( pObj, f, Aig_ObjCreateCi(pAigFrames) );
     // set initial state for the latches
     Aig_ManForEachLoSeq( p->pAig, pObj, i )
         Bmc_ObjSetFrames( pObj, 0, Aig_ManConst0(pAigFrames) );
@@ -283,7 +283,7 @@ Aig_Man_t * Fra_BmcFrames( Fra_Bmc_t * p, int fKeepPos )
     {
         for ( f = 0; f < p->nFramesAll; f++ )
             Aig_ManForEachPoSeq( p->pAig, pObj, i )
-                Aig_ObjCreatePo( pAigFrames, Bmc_ObjChild0Frames(pObj,f) );
+                Aig_ObjCreateCo( pAigFrames, Bmc_ObjChild0Frames(pObj,f) );
         Aig_ManCleanup( pAigFrames );
     }
     else
@@ -291,7 +291,7 @@ Aig_Man_t * Fra_BmcFrames( Fra_Bmc_t * p, int fKeepPos )
         // add POs to all the dangling nodes
         Aig_ManForEachObj( pAigFrames, pObjNew, i )
             if ( Aig_ObjIsNode(pObjNew) && pObjNew->nRefs == 0 )
-                Aig_ObjCreatePo( pAigFrames, pObjNew );
+                Aig_ObjCreateCo( pAigFrames, pObjNew );
     }
     // return the new manager
     return pAigFrames;
diff --git a/src/proof/fra/fraClass.c b/src/proof/fra/fraClass.c
index 67351f6d..f7850241 100644
--- a/src/proof/fra/fraClass.c
+++ b/src/proof/fra/fraClass.c
@@ -779,7 +779,7 @@ static inline void Fra_ClassesDeriveNode( Aig_Man_t * pManFraig, Aig_Obj_t * pOb
     pMiter = Aig_Exor( pManFraig, Aig_Regular(pObjNew), Aig_Regular(pObjReprNew) );
     pMiter = Aig_NotCond( pMiter, Aig_Regular(pMiter)->fPhase ^ Aig_IsComplement(pMiter) );
     pMiter = Aig_Not( pMiter );
-    Aig_ObjCreatePo( pManFraig, pMiter );
+    Aig_ObjCreateCo( pManFraig, pMiter );
 }
 
 /**Function*************************************************************
@@ -811,14 +811,14 @@ Aig_Man_t * Fra_ClassesDeriveAig( Fra_Cla_t * p, int nFramesK )
     Fra_ObjSetEqu( ppEquivs, Aig_ManConst1(p->pAig), Aig_ManConst1(pManFraig) );
     // create latches for the first frame
     Aig_ManForEachLoSeq( p->pAig, pObj, i )
-        Fra_ObjSetEqu( ppEquivs, pObj, Aig_ObjCreatePi(pManFraig) );
+        Fra_ObjSetEqu( ppEquivs, pObj, Aig_ObjCreateCi(pManFraig) );
     // add timeframes
     pLatches = ABC_ALLOC( Aig_Obj_t *, Aig_ManRegNum(p->pAig) );
     for ( f = 0; f < nFramesAll; f++ )
     {
         // create PIs for this frame
         Aig_ManForEachPiSeq( p->pAig, pObj, i )
-            Fra_ObjSetEqu( ppEquivs, pObj, Aig_ObjCreatePi(pManFraig) );
+            Fra_ObjSetEqu( ppEquivs, pObj, Aig_ObjCreateCi(pManFraig) );
         // set the constraints on the latch outputs
         Aig_ManForEachLoSeq( p->pAig, pObj, i )
             Fra_ClassesDeriveNode( pManFraig, pObj, ppEquivs );
diff --git a/src/proof/fra/fraClau.c b/src/proof/fra/fraClau.c
index 48640d1d..28e9e9b9 100644
--- a/src/proof/fra/fraClau.c
+++ b/src/proof/fra/fraClau.c
@@ -109,7 +109,7 @@ Vec_Int_t * Fra_ClauSaveOutputVars( Aig_Man_t * pMan, Cnf_Dat_t * pCnf )
     Aig_Obj_t * pObj;
     int i;
     vVars = Vec_IntAlloc( Aig_ManPoNum(pMan) );
-    Aig_ManForEachPo( pMan, pObj, i )
+    Aig_ManForEachCo( pMan, pObj, i )
         Vec_IntPush( vVars, pCnf->pVarNums[pObj->Id] );
     return vVars;
 }
@@ -131,7 +131,7 @@ Vec_Int_t * Fra_ClauSaveInputVars( Aig_Man_t * pMan, Cnf_Dat_t * pCnf, int nStar
     Aig_Obj_t * pObj;
     int i;
     vVars = Vec_IntAlloc( Aig_ManPiNum(pMan) - nStarting );
-    Aig_ManForEachPi( pMan, pObj, i )
+    Aig_ManForEachCi( pMan, pObj, i )
     {
         if ( i < nStarting )
             continue;
diff --git a/src/proof/fra/fraClaus.c b/src/proof/fra/fraClaus.c
index e71219b5..f27c63ce 100644
--- a/src/proof/fra/fraClaus.c
+++ b/src/proof/fra/fraClaus.c
@@ -1565,7 +1565,7 @@ void Fra_ClausWriteIndClauses( Clu_Man_t * p )
             pLiteral = Fra_ClausGetLiteral( p, pVar2Id, pStart[k] );
             pClause = Aig_Or( pNew, pClause, pLiteral );
         }
-        Aig_ObjCreatePo( pNew, pClause );
+        Aig_ObjCreateCo( pNew, pClause );
         Beg = End;
     }
     ABC_FREE( pVar2Id );
diff --git a/src/proof/fra/fraCore.c b/src/proof/fra/fraCore.c
index d3b60ab7..1969b36d 100644
--- a/src/proof/fra/fraCore.c
+++ b/src/proof/fra/fraCore.c
@@ -193,12 +193,12 @@ void Fra_FraigVerifyCounterEx( Fra_Man_t * p, Vec_Int_t * vCex )
         assert( !pObj->fMarkB );
     // simulate the cex through the AIG
     Aig_ManConst1(p->pManAig)->fMarkB = 1;
-    Aig_ManForEachPi( p->pManAig, pObj, i )
+    Aig_ManForEachCi( p->pManAig, pObj, i )
         pObj->fMarkB = Vec_IntEntry(vCex, i);
     Aig_ManForEachNode( p->pManAig, pObj, i )
         pObj->fMarkB = (Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj)) & 
                        (Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj));
-    Aig_ManForEachPo( p->pManAig, pObj, i )
+    Aig_ManForEachCo( p->pManAig, pObj, i )
         pObj->fMarkB = Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj);
     // check if the classes hold
     Vec_PtrForEachEntry( Aig_Obj_t *, p->pCla->vClasses1, pObj, i )
diff --git a/src/proof/fra/fraHot.c b/src/proof/fra/fraHot.c
index 29c9c33d..03dd468a 100644
--- a/src/proof/fra/fraHot.c
+++ b/src/proof/fra/fraHot.c
@@ -402,9 +402,9 @@ Aig_Man_t * Fra_OneHotCreateExdc( Fra_Man_t * p, Vec_Int_t * vOneHots )
     int i, Out1, Out2, nTruePis;
     pNew = Aig_ManStart( Vec_IntSize(vOneHots)/2 );
 //    for ( i = 0; i < Aig_ManRegNum(p->pManAig); i++ )
-//        Aig_ObjCreatePi(pNew);
-    Aig_ManForEachPi( p->pManAig, pObj, i )
-        Aig_ObjCreatePi(pNew);
+//        Aig_ObjCreateCi(pNew);
+    Aig_ManForEachCi( p->pManAig, pObj, i )
+        Aig_ObjCreateCi(pNew);
     nTruePis = Aig_ManPiNum(p->pManAig) - Aig_ManRegNum(p->pManAig);
     for ( i = 0; i < Vec_IntSize(vOneHots); i += 2 )
     {
@@ -417,7 +417,7 @@ Aig_Man_t * Fra_OneHotCreateExdc( Fra_Man_t * p, Vec_Int_t * vOneHots )
         pObj1 = Aig_NotCond( pObj1, Fra_LitSign(Out1) );
         pObj2 = Aig_NotCond( pObj2, Fra_LitSign(Out2) );
         pObj  = Aig_Or( pNew, pObj1, pObj2 );
-        Aig_ObjCreatePo( pNew, pObj );
+        Aig_ObjCreateCo( pNew, pObj );
     }
     Aig_ManCleanup(pNew);
 //    printf( "Created AIG with %d nodes and %d outputs.\n", Aig_ManNodeNum(pNew), Aig_ManPoNum(pNew) );
diff --git a/src/proof/fra/fraImp.c b/src/proof/fra/fraImp.c
index 9877ceaa..de24f179 100644
--- a/src/proof/fra/fraImp.c
+++ b/src/proof/fra/fraImp.c
@@ -717,7 +717,7 @@ void Fra_ImpRecordInManager( Fra_Man_t * p, Aig_Man_t * pNew )
         pMiter = Aig_Or( pNew, 
             Aig_NotCond((Aig_Obj_t *)pLeft->pData, !pLeft->fPhase), 
             Aig_NotCond((Aig_Obj_t *)pRight->pData, pRight->fPhase) ); 
-        Aig_ObjCreatePo( pNew, pMiter );
+        Aig_ObjCreateCo( pNew, pMiter );
     }
     pNew->nAsserts = Aig_ManPoNum(pNew) - nPosOld;
 }
diff --git a/src/proof/fra/fraInd.c b/src/proof/fra/fraInd.c
index 1224bab3..b8a1e6bf 100644
--- a/src/proof/fra/fraInd.c
+++ b/src/proof/fra/fraInd.c
@@ -112,7 +112,7 @@ static inline void Fra_FramesConstrainNode( Aig_Man_t * pManFraig, Aig_Obj_t * p
     pMiter = Aig_Exor( pManFraig, pObjNew, pObjReprNew );
     pMiter = Aig_NotCond( pMiter, !Aig_ObjPhaseReal(pMiter) );
     assert( Aig_ObjPhaseReal(pMiter) == 1 );
-    Aig_ObjCreatePo( pManFraig, pMiter );
+    Aig_ObjCreateCo( pManFraig, pMiter );
 }
 
 /**Function*************************************************************
@@ -145,10 +145,10 @@ Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p )
         Fra_ObjSetFraig( Aig_ManConst1(p->pManAig), f, Aig_ManConst1(pManFraig) );
     for ( f = 0; f < p->nFramesAll; f++ )
         Aig_ManForEachPiSeq( p->pManAig, pObj, i )
-            Fra_ObjSetFraig( pObj, f, Aig_ObjCreatePi(pManFraig) );
+            Fra_ObjSetFraig( pObj, f, Aig_ObjCreateCi(pManFraig) );
     // create latches for the first frame
     Aig_ManForEachLoSeq( p->pManAig, pObj, i )
-        Fra_ObjSetFraig( pObj, 0, Aig_ObjCreatePi(pManFraig) );
+        Fra_ObjSetFraig( pObj, 0, Aig_ObjCreateCi(pManFraig) );
 
     // add timeframes
 //    pManFraig->fAddStrash = 1;
@@ -173,7 +173,7 @@ Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p )
     pManFraig->nAsserts = Aig_ManPoNum(pManFraig);
     // add the POs for the latch outputs of the last frame
     Aig_ManForEachLoSeq( p->pManAig, pObj, i )
-        Aig_ObjCreatePo( pManFraig, Fra_ObjFraig(pObj,p->nFramesAll-1) );
+        Aig_ObjCreateCo( pManFraig, Fra_ObjFraig(pObj,p->nFramesAll-1) );
 
     // remove dangling nodes
     Aig_ManCleanup( pManFraig );
diff --git a/src/proof/fra/fraLcr.c b/src/proof/fra/fraLcr.c
index 238e3096..d24b37f6 100644
--- a/src/proof/fra/fraLcr.c
+++ b/src/proof/fra/fraLcr.c
@@ -134,7 +134,7 @@ void Lcr_ManFree( Fra_Lcr_t * p )
     int i;
     if ( p->fVerbose )
         Lcr_ManPrint( p );
-    Aig_ManForEachPi( p->pAig, pObj, i )
+    Aig_ManForEachCi( p->pAig, pObj, i )
         pObj->pNext = NULL;
     Vec_PtrFree( p->vFraigs );
     if ( p->pCla  )     Fra_ClassesStop( p->pCla );
@@ -162,7 +162,7 @@ Fra_Man_t * Fra_LcrAigPrepare( Aig_Man_t * pAig )
     int i;
     p = ABC_ALLOC( Fra_Man_t, 1 );
     memset( p, 0, sizeof(Fra_Man_t) );
-//    Aig_ManForEachPi( pAig, pObj, i )
+//    Aig_ManForEachCi( pAig, pObj, i )
     Aig_ManForEachObj( pAig, pObj, i )
         pObj->pData = p;
     return p;
@@ -183,7 +183,7 @@ void Fra_LcrAigPrepareTwo( Aig_Man_t * pAig, Fra_Man_t * p )
 {
     Aig_Obj_t * pObj;
     int i;
-    Aig_ManForEachPi( pAig, pObj, i )
+    Aig_ManForEachCi( pAig, pObj, i )
         pObj->pData = p;
 }
 
@@ -300,7 +300,7 @@ Aig_Man_t * Fra_LcrDeriveAigForPartitioning( Fra_Lcr_t * pLcr )
     Aig_Obj_t * pObj, * pObjPo, * pObjNew, ** ppClass, * pMiter;
     int i, c, Offset;
     // remember the numbers of the inputs of the original AIG
-    Aig_ManForEachPi( pLcr->pAig, pObj, i )
+    Aig_ManForEachCi( pLcr->pAig, pObj, i )
     {
         pObj->pData = pLcr;
         pObj->pNext = (Aig_Obj_t *)(long)i;
@@ -321,7 +321,7 @@ Aig_Man_t * Fra_LcrDeriveAigForPartitioning( Fra_Lcr_t * pLcr )
             pObjNew = Fra_LcrManDup_rec( pNew, pLcr->pAig, Aig_ObjFanin0(pObjPo) );
             pMiter  = Aig_Exor( pNew, pMiter, pObjNew );
         }
-        Aig_ObjCreatePo( pNew, pMiter );
+        Aig_ObjCreateCo( pNew, pMiter );
     }
     // go over the constant candidates
     Vec_PtrForEachEntry( Aig_Obj_t *, pLcr->pCla->vClasses1, pObj, i )
@@ -329,7 +329,7 @@ Aig_Man_t * Fra_LcrDeriveAigForPartitioning( Fra_Lcr_t * pLcr )
         assert( Aig_ObjIsPi(pObj) );
         pObjPo = Aig_ManPo( pLcr->pAig, Offset+(long)pObj->pNext );
         pMiter = Fra_LcrManDup_rec( pNew, pLcr->pAig, Aig_ObjFanin0(pObjPo) );
-        Aig_ObjCreatePo( pNew, pMiter );
+        Aig_ObjCreateCo( pNew, pMiter );
     }
     return pNew;
 }
@@ -403,7 +403,7 @@ Aig_Obj_t * Fra_LcrCreatePart_rec( Fra_Cla_t * pCla, Aig_Man_t * pNew, Aig_Man_t
 //        Aig_Obj_t * pRepr = Fra_ClassObjRepr(pObj);
         Aig_Obj_t * pRepr = pCla->pMemRepr[pObj->Id];
         if ( pRepr == NULL )
-            pObj->pData = Aig_ObjCreatePi( pNew );
+            pObj->pData = Aig_ObjCreateCi( pNew );
         else
         {
             pObj->pData = Fra_LcrCreatePart_rec( pCla, pNew, p, pRepr );
@@ -447,7 +447,7 @@ Aig_Man_t * Fra_LcrCreatePart( Fra_Lcr_t * p, Vec_Int_t * vPart )
         }
         else
             pObjNew = Aig_ManConst1( pNew );
-        Aig_ObjCreatePo( pNew, pObjNew ); 
+        Aig_ObjCreateCo( pNew, pObjNew ); 
     }
     return pNew;
 }
diff --git a/src/proof/fra/fraMan.c b/src/proof/fra/fraMan.c
index 90e8b762..67832f83 100644
--- a/src/proof/fra/fraMan.c
+++ b/src/proof/fra/fraMan.c
@@ -187,8 +187,8 @@ Aig_Man_t * Fra_ManPrepareComb( Fra_Man_t * p )
     pManFraig->nAsserts = p->pManAig->nAsserts;
     // set the pointers to the available fraig nodes
     Fra_ObjSetFraig( Aig_ManConst1(p->pManAig), 0, Aig_ManConst1(pManFraig) );
-    Aig_ManForEachPi( p->pManAig, pObj, i )
-        Fra_ObjSetFraig( pObj, 0, Aig_ObjCreatePi(pManFraig) );
+    Aig_ManForEachCi( p->pManAig, pObj, i )
+        Fra_ObjSetFraig( pObj, 0, Aig_ObjCreateCi(pManFraig) );
     // set the pointers to the manager
     Aig_ManForEachObj( pManFraig, pObj, i )
         pObj->pData = p;
@@ -219,8 +219,8 @@ void Fra_ManFinalizeComb( Fra_Man_t * p )
     Aig_Obj_t * pObj;
     int i;
     // add the POs
-    Aig_ManForEachPo( p->pManAig, pObj, i )
-        Aig_ObjCreatePo( p->pManFraig, Fra_ObjChild0Fra(pObj,0) );
+    Aig_ManForEachCo( p->pManAig, pObj, i )
+        Aig_ObjCreateCo( p->pManFraig, Fra_ObjChild0Fra(pObj,0) );
     // postprocess
     Aig_ManCleanMarkB( p->pManFraig );
 }
diff --git a/src/proof/fra/fraPart.c b/src/proof/fra/fraPart.c
index e9739f97..6594ac0b 100644
--- a/src/proof/fra/fraPart.c
+++ b/src/proof/fra/fraPart.c
@@ -64,7 +64,7 @@ clk = clock();
     vSupps = (Vec_Vec_t *)Aig_ManSupports( p );
 ABC_PRT( "Supports", clock() - clk );
     // remove last entry
-    Aig_ManForEachPo( p, pObj, i )
+    Aig_ManForEachCo( p, pObj, i )
     {
         vSup = Vec_VecEntryInt( vSupps, i );
         Vec_IntPop( vSup );
@@ -75,7 +75,7 @@ ABC_PRT( "Supports", clock() - clk );
     // create reverse supports
 clk = clock();
     vSuppsIn = Vec_VecStart( Aig_ManPiNum(p) );
-    Aig_ManForEachPo( p, pObj, i )
+    Aig_ManForEachCo( p, pObj, i )
     {
         vSup = Vec_VecEntryInt( vSupps, i );
         Vec_IntForEachEntry( vSup, Entry, k )
@@ -90,7 +90,7 @@ clk = clock();
     vOverNew  = Vec_IntAlloc( Aig_ManPoNum(p) );
     vQuantNew = Vec_IntAlloc( Aig_ManPoNum(p) );
 //    pProgress = Bar_ProgressStart( stdout, Aig_ManPoNum(p) );
-    Aig_ManForEachPo( p, pObj, i )
+    Aig_ManForEachCo( p, pObj, i )
     {
 //        Bar_ProgressUpdate( pProgress, i, NULL );
         // get old supports
@@ -101,7 +101,7 @@ clk = clock();
         CountOver = CountQuant = 0;
         vSupNew = Vec_IntDup( vSup );
         // go through the nodes where the first var appears
-        Aig_ManForEachPo( p, pObj, k )
+        Aig_ManForEachCo( p, pObj, k )
 //        iVar = Vec_IntEntry( vSup, 0 );
 //        vSupIn = Vec_VecEntry( vSuppsIn, iVar );
 //        Vec_IntForEachEntry( vSupIn, Entry, k )
@@ -198,7 +198,7 @@ clk = clock();
     vSupps = (Vec_Vec_t *)Aig_ManSupports( p );
 ABC_PRT( "Supports", clock() - clk );
     // remove last entry
-    Aig_ManForEachPo( p, pObj, i )
+    Aig_ManForEachCo( p, pObj, i )
     {
         vSup = Vec_VecEntryInt( vSupps, i );
         Vec_IntPop( vSup );
@@ -209,7 +209,7 @@ ABC_PRT( "Supports", clock() - clk );
     // create reverse supports
 clk = clock();
     vSuppsIn = Vec_VecStart( Aig_ManPiNum(p) );
-    Aig_ManForEachPo( p, pObj, i )
+    Aig_ManForEachCo( p, pObj, i )
     {
         if ( i == p->nAsserts )
             break;
@@ -222,7 +222,7 @@ ABC_PRT( "Inverse ", clock() - clk );
     // create affective supports
 clk = clock();
     pSupp = ABC_ALLOC( char, Aig_ManPiNum(p) );
-    Aig_ManForEachPo( p, pObj, i )
+    Aig_ManForEachCo( p, pObj, i )
     {
         if ( i % 50 != 0 )
             continue;
diff --git a/src/proof/fra/fraSim.c b/src/proof/fra/fraSim.c
index eb42c665..e54846bc 100644
--- a/src/proof/fra/fraSim.c
+++ b/src/proof/fra/fraSim.c
@@ -243,7 +243,7 @@ void Fra_SmlSavePattern( Fra_Man_t * p )
     Aig_Obj_t * pObj;
     int i;
     memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
-    Aig_ManForEachPi( p->pManFraig, pObj, i )
+    Aig_ManForEachCi( p->pManFraig, pObj, i )
 //        if ( p->pSat->model.ptr[Fra_ObjSatNum(pObj)] == l_True )
         if ( sat_solver_var_value(p->pSat, Fra_ObjSatNum(pObj)) )
             Abc_InfoSetBit( p->pPatWords, i );
@@ -259,7 +259,7 @@ void Fra_SmlSavePattern( Fra_Man_t * p )
 
 /*
     printf( "Pattern: " );
-    Aig_ManForEachPi( p->pManFraig, pObj, i )
+    Aig_ManForEachCi( p->pManFraig, pObj, i )
         printf( "%d", Abc_InfoHasBit( p->pPatWords, i ) );
     printf( "\n" );
 */
@@ -299,7 +299,7 @@ void Fra_SmlCheckOutputSavePattern( Fra_Man_t * p, Aig_Obj_t * pObjPo )
     BestPat = i * 32 + k;
     // fill in the counter-example data
     pModel = ABC_ALLOC( int, Aig_ManPiNum(p->pManFraig)+1 );
-    Aig_ManForEachPi( p->pManAig, pObjPi, i )
+    Aig_ManForEachCi( p->pManAig, pObjPi, i )
     {
         pModel[i] = Abc_InfoHasBit(Fra_ObjSim(p->pSml, pObjPi->Id), BestPat);
 //        printf( "%d", pModel[i] );
@@ -330,7 +330,7 @@ int Fra_SmlCheckOutput( Fra_Man_t * p )
     // make sure the reference simulation pattern does not detect the bug
     pObj = Aig_ManPo( p->pManAig, 0 );
     assert( Aig_ObjFanin0(pObj)->fPhase == (unsigned)Aig_ObjFaninC0(pObj) ); 
-    Aig_ManForEachPo( p->pManAig, pObj, i )
+    Aig_ManForEachCo( p->pManAig, pObj, i )
     {
         if ( !Fra_SmlNodeIsConst( Aig_ObjFanin0(pObj) ) )
         {
@@ -414,7 +414,7 @@ void Fra_SmlInitialize( Fra_Sml_t * p, int fInit )
     }
     else
     {
-        Aig_ManForEachPi( p->pAig, pObj, i )
+        Aig_ManForEachCi( p->pAig, pObj, i )
             Fra_SmlAssignRandom( p, pObj );
     }
 }
@@ -438,7 +438,7 @@ void Fra_SmlAssignDist1( Fra_Sml_t * p, unsigned * pPat )
     if ( p->nFrames == 1 )
     {
         // copy the PI info 
-        Aig_ManForEachPi( p->pAig, pObj, i )
+        Aig_ManForEachCi( p->pAig, pObj, i )
             Fra_SmlAssignConst( p, pObj, Abc_InfoHasBit(pPat, i), 0 );
         // flip one bit
         Limit = Abc_MinInt( Aig_ManPiNum(p->pAig), p->nWordsTotal * 32 - 1 );
@@ -980,7 +980,7 @@ Abc_Cex_t * Fra_SmlCopyCounterExample( Aig_Man_t * pAig, Aig_Man_t * pFrames, in
     // find the PO that failed
     iPo = -1;
     iFrame = -1;
-    Aig_ManForEachPo( pFrames, pObj, i )
+    Aig_ManForEachCo( pFrames, pObj, i )
         if ( pObj->Id == pModel[Aig_ManPiNum(pFrames)] )
         {
             iPo = i % nTruePos;
diff --git a/src/proof/int/intCheck.c b/src/proof/int/intCheck.c
index 6b36fe30..57d6e7d0 100644
--- a/src/proof/int/intCheck.c
+++ b/src/proof/int/intCheck.c
@@ -67,13 +67,13 @@ Aig_Man_t * Inter_ManUnrollFrames( Aig_Man_t * pAig, int nFrames )
     Aig_ManConst1(pAig)->pData = Aig_ManConst1( pFrames );
     // create variables for register outputs
     Saig_ManForEachLo( pAig, pObj, i )
-        pObj->pData = Aig_ObjCreatePi( pFrames );
+        pObj->pData = Aig_ObjCreateCi( pFrames );
     // add timeframes
     for ( f = 0; f < nFrames; f++ )
     {
         // create PI nodes for this frame
         Saig_ManForEachPi( pAig, pObj, i )
-            pObj->pData = Aig_ObjCreatePi( pFrames );
+            pObj->pData = Aig_ObjCreateCi( pFrames );
         // add internal nodes of this frame
         Aig_ManForEachNode( pAig, pObj, i )
             pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
@@ -84,7 +84,7 @@ Aig_Man_t * Inter_ManUnrollFrames( Aig_Man_t * pAig, int nFrames )
         Saig_ManForEachLiLo(  pAig, pObjLi, pObjLo, i )
         {
             pObjLo->pData = pObjLi->pData;
-            Aig_ObjCreatePo( pFrames, (Aig_Obj_t *)pObjLo->pData );
+            Aig_ObjCreateCo( pFrames, (Aig_Obj_t *)pObjLo->pData );
         }
     }
     Aig_ManCleanup( pFrames );
@@ -240,7 +240,7 @@ int Inter_CheckPerform( Inter_Check_t * p, Cnf_Dat_t * pCnfInt, int nTimeNewOut
             assert( RetValue );
         }
         // add equality clauses for the flop variables
-        Aig_ManForEachPi( pCnfInt->pMan, pObj, i )
+        Aig_ManForEachCi( pCnfInt->pMan, pObj, i )
         {
             pObj2 = f ? Aig_ManPo(p->pFrames, i + (f-1) * nRegs) : Aig_ManPi(p->pFrames, i);
             Inter_CheckAddEqual( p, pCnfInt->pVarNums[pObj->Id], p->pCnf->pVarNums[pObj2->Id] );
diff --git a/src/proof/int/intContain.c b/src/proof/int/intContain.c
index 58b408d7..213c557c 100644
--- a/src/proof/int/intContain.c
+++ b/src/proof/int/intContain.c
@@ -121,7 +121,7 @@ Aig_Man_t * Inter_ManFramesLatches( Aig_Man_t * pAig, int nFrames, Vec_Ptr_t **
     *pvMapReg = Vec_PtrAlloc( (nFrames+1) * Saig_ManRegNum(pAig) );
     Saig_ManForEachLo( pAig, pObj, i )
     {
-        pObj->pData = Aig_ObjCreatePi( pFrames );
+        pObj->pData = Aig_ObjCreateCi( pFrames );
         Vec_PtrPush( *pvMapReg, pObj->pData );
     }
     // add timeframes
@@ -129,7 +129,7 @@ Aig_Man_t * Inter_ManFramesLatches( Aig_Man_t * pAig, int nFrames, Vec_Ptr_t **
     {
         // create PI nodes for this frame
         Saig_ManForEachPi( pAig, pObj, i )
-            pObj->pData = Aig_ObjCreatePi( pFrames );
+            pObj->pData = Aig_ObjCreateCi( pFrames );
         // add internal nodes of this frame
         Aig_ManForEachNode( pAig, pObj, i )
             pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
@@ -165,14 +165,14 @@ void Inter_ManAppendCone( Aig_Man_t * pOld, Aig_Man_t * pNew, Aig_Obj_t ** ppNew
     // create the PIs
     Aig_ManCleanData( pOld );
     Aig_ManConst1(pOld)->pData = Aig_ManConst1(pNew);
-    Aig_ManForEachPi( pOld, pObj, i )
+    Aig_ManForEachCi( pOld, pObj, i )
         pObj->pData = ppNewPis[i];
     // duplicate internal nodes
     Aig_ManForEachNode( pOld, pObj, i )
         pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
     // add one PO to new
     pObj = Aig_ManPo( pOld, 0 );
-    Aig_ObjCreatePo( pNew, Aig_NotCond( Aig_ObjChild0Copy(pObj), fCompl ) );
+    Aig_ObjCreateCo( pNew, Aig_NotCond( Aig_ObjChild0Copy(pObj), fCompl ) );
 }
 
 
@@ -287,7 +287,7 @@ int Inter_ManCheckUniqueness( Aig_Man_t * p, sat_solver * pSat, Cnf_Dat_t * pCnf
 
     // get the counter-example
     vPis = Vec_IntAlloc( 100 );
-    Aig_ManForEachPi( pCnf->pMan, pObj, k )
+    Aig_ManForEachCi( pCnf->pMan, pObj, k )
         Vec_IntPush( vPis, pCnf->pVarNums[Aig_ObjId(pObj)] );
     assert( Vec_IntSize(vPis) == Aig_ManRegNum(p) + nFrames * Saig_ManPiNum(p) );
     pCounterEx = Sat_SolverGetModel( pSat, vPis->pArray, vPis->nSize );
diff --git a/src/proof/int/intCtrex.c b/src/proof/int/intCtrex.c
index 9ba8c9df..22e689f4 100644
--- a/src/proof/int/intCtrex.c
+++ b/src/proof/int/intCtrex.c
@@ -61,7 +61,7 @@ Aig_Man_t * Inter_ManFramesBmc( Aig_Man_t * pAig, int nFrames )
     {
         // create PI nodes for this frame
         Saig_ManForEachPi( pAig, pObj, i )
-            pObj->pData = Aig_ObjCreatePi( pFrames );
+            pObj->pData = Aig_ObjCreateCi( pFrames );
         // add internal nodes of this frame
         Aig_ManForEachNode( pAig, pObj, i )
             pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
@@ -76,7 +76,7 @@ Aig_Man_t * Inter_ManFramesBmc( Aig_Man_t * pAig, int nFrames )
     }
     // create POs for the output of the last frame
     pObj = Aig_ManPo( pAig, 0 );
-    Aig_ObjCreatePo( pFrames, Aig_ObjChild0Copy(pObj) );
+    Aig_ObjCreateCo( pFrames, Aig_ObjChild0Copy(pObj) );
     Aig_ManCleanup( pFrames );
     return pFrames;
 }
diff --git a/src/proof/int/intDup.c b/src/proof/int/intDup.c
index 551473ef..adc692cb 100644
--- a/src/proof/int/intDup.c
+++ b/src/proof/int/intDup.c
@@ -52,9 +52,9 @@ Aig_Man_t * Inter_ManStartInitState( int nRegs )
     ppInputs = ABC_ALLOC( Aig_Obj_t *, nRegs );
     p = Aig_ManStart( nRegs );
     for ( i = 0; i < nRegs; i++ )
-        ppInputs[i] = Aig_Not( Aig_ObjCreatePi(p) );
+        ppInputs[i] = Aig_Not( Aig_ObjCreateCi(p) );
     pRes = Aig_Multi( p, ppInputs, nRegs, AIG_OBJ_AND );
-    Aig_ObjCreatePo( p, pRes );
+    Aig_ObjCreateCo( p, pRes );
     ABC_FREE( ppInputs );
     return p;
 }
@@ -83,8 +83,8 @@ Aig_Man_t * Inter_ManStartDuplicated( Aig_Man_t * p )
     // create the PIs
     Aig_ManCleanData( p );
     Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
-    Aig_ManForEachPi( p, pObj, i )
-        pObj->pData = Aig_ObjCreatePi( pNew );
+    Aig_ManForEachCi( p, pObj, i )
+        pObj->pData = Aig_ObjCreateCi( pNew );
     // set registers
     pNew->nTruePis = p->nTruePis;
     pNew->nTruePos = Saig_ManConstrNum(p);
@@ -98,12 +98,12 @@ Aig_Man_t * Inter_ManStartDuplicated( Aig_Man_t * p )
     {
         if ( i < Saig_ManPoNum(p)-Saig_ManConstrNum(p) )
             continue;
-        Aig_ObjCreatePo( pNew, Aig_Not( Aig_ObjChild0Copy(pObj) ) );
+        Aig_ObjCreateCo( pNew, Aig_Not( Aig_ObjChild0Copy(pObj) ) );
     }
 
     // create register inputs with MUXes
     Saig_ManForEachLi( p, pObj, i )
-        Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
+        Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
     Aig_ManCleanup( pNew );
     return pNew;
 }
@@ -133,11 +133,11 @@ Aig_Man_t * Inter_ManStartOneOutput( Aig_Man_t * p, int fAddFirstPo )
     // create the PIs
     Aig_ManCleanData( p );
     Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
-    Aig_ManForEachPi( p, pObj, i )
+    Aig_ManForEachCi( p, pObj, i )
     {
         if ( i == Saig_ManPiNum(p) )
-            pCtrl = Aig_ObjCreatePi( pNew );
-        pObj->pData = Aig_ObjCreatePi( pNew );
+            pCtrl = Aig_ObjCreateCi( pNew );
+        pObj->pData = Aig_ObjCreateCi( pNew );
     }
     // set registers
     pNew->nRegs    = fAddFirstPo? 0 : p->nRegs;
@@ -152,14 +152,14 @@ Aig_Man_t * Inter_ManStartOneOutput( Aig_Man_t * p, int fAddFirstPo )
     {
         if ( i < Saig_ManPoNum(p)-Saig_ManConstrNum(p) )
             continue;
-        Aig_ObjCreatePo( pNew, Aig_Not( Aig_ObjChild0Copy(pObj) ) );
+        Aig_ObjCreateCo( pNew, Aig_Not( Aig_ObjChild0Copy(pObj) ) );
     }
 
     // add the PO
     if ( fAddFirstPo )
     {
         pObj = Aig_ManPo( p, 0 );
-        Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
+        Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
     }
     else
     {
@@ -168,7 +168,7 @@ Aig_Man_t * Inter_ManStartOneOutput( Aig_Man_t * p, int fAddFirstPo )
         {
             pObj = Aig_Mux( pNew, pCtrl, (Aig_Obj_t *)pObjLo->pData, Aig_ObjChild0Copy(pObjLi) );
     //        pObj = Aig_Mux( pNew, pCtrl, Aig_ManConst0(pNew), Aig_ObjChild0Copy(pObjLi) );
-            Aig_ObjCreatePo( pNew, pObj );
+            Aig_ObjCreateCo( pNew, pObj );
         }
     }
     Aig_ManCleanup( pNew );
diff --git a/src/proof/int/intFrames.c b/src/proof/int/intFrames.c
index 0fbab6cb..8e74d99a 100644
--- a/src/proof/int/intFrames.c
+++ b/src/proof/int/intFrames.c
@@ -63,14 +63,14 @@ Aig_Man_t * Inter_ManFramesInter( Aig_Man_t * pAig, int nFrames, int fAddRegOuts
     else
     {
         Saig_ManForEachLo( pAig, pObj, i )
-            pObj->pData = Aig_ObjCreatePi( pFrames );
+            pObj->pData = Aig_ObjCreateCi( pFrames );
     }
     // add timeframes
     for ( f = 0; f < nFrames; f++ )
     {
         // create PI nodes for this frame
         Saig_ManForEachPi( pAig, pObj, i )
-            pObj->pData = Aig_ObjCreatePi( pFrames );
+            pObj->pData = Aig_ObjCreateCi( pFrames );
         // add internal nodes of this frame
         Aig_ManForEachNode( pAig, pObj, i )
             pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
@@ -79,7 +79,7 @@ Aig_Man_t * Inter_ManFramesInter( Aig_Man_t * pAig, int nFrames, int fAddRegOuts
         {
             if ( i < Saig_ManPoNum(pAig)-Saig_ManConstrNum(pAig) )
                 continue;
-            Aig_ObjCreatePo( pFrames, Aig_Not( Aig_ObjChild0Copy(pObj) ) );
+            Aig_ObjCreateCo( pFrames, Aig_Not( Aig_ObjChild0Copy(pObj) ) );
         }
         if ( f == nFrames - 1 )
             break;
@@ -94,13 +94,13 @@ Aig_Man_t * Inter_ManFramesInter( Aig_Man_t * pAig, int nFrames, int fAddRegOuts
     if ( fAddRegOuts )
     {
         Saig_ManForEachLi( pAig, pObj, i )
-            Aig_ObjCreatePo( pFrames, Aig_ObjChild0Copy(pObj) );
+            Aig_ObjCreateCo( pFrames, Aig_ObjChild0Copy(pObj) );
     }
     // create the only PO of the manager
     else
     {
         pObj = Aig_ManPo( pAig, 0 );
-        Aig_ObjCreatePo( pFrames, Aig_ObjChild0Copy(pObj) );
+        Aig_ObjCreateCo( pFrames, Aig_ObjChild0Copy(pObj) );
     }
     Aig_ManCleanup( pFrames );
     return pFrames;
diff --git a/src/proof/int/intM114.c b/src/proof/int/intM114.c
index 139c9bbd..c37cb2c6 100644
--- a/src/proof/int/intM114.c
+++ b/src/proof/int/intM114.c
@@ -113,7 +113,7 @@ sat_solver * Inter_ManDeriveSatSolver(
     }
     else
     {
-        Aig_ManForEachPi( pInter, pObj, i )
+        Aig_ManForEachCi( pInter, pObj, i )
         {
             pObj2 = Saig_ManLo( pAig, i );
 
@@ -137,7 +137,7 @@ sat_solver * Inter_ManDeriveSatSolver(
     Vec_IntClear( vVarsAB );
     if ( fUseBackward )
     {
-        Aig_ManForEachPo( pFrames, pObj, i )
+        Aig_ManForEachCo( pFrames, pObj, i )
         {
             assert( pCnfFrames->pVarNums[pObj->Id] >= 0 );
             Vec_IntPush( vVarsAB, pCnfFrames->pVarNums[pObj->Id] );
@@ -155,7 +155,7 @@ sat_solver * Inter_ManDeriveSatSolver(
     }
     else
     {
-        Aig_ManForEachPi( pFrames, pObj, i )
+        Aig_ManForEachCi( pFrames, pObj, i )
         {
             if ( i == Aig_ManRegNum(pAig) )
                 break;
diff --git a/src/proof/int/intM114p.c b/src/proof/int/intM114p.c
index 7c011426..6164a389 100644
--- a/src/proof/int/intM114p.c
+++ b/src/proof/int/intM114p.c
@@ -87,7 +87,7 @@ M114p_Solver_t Inter_ManDeriveSatSolverM114p(
             assert( 0 );
     }
     // connector clauses
-    Aig_ManForEachPi( pInter, pObj, i )
+    Aig_ManForEachCi( pInter, pObj, i )
     {
         pObj2 = Saig_ManLo( pAig, i );
         Lits[0] = toLitCond( pCnfInter->pVarNums[pObj->Id], 0 );
@@ -109,7 +109,7 @@ M114p_Solver_t Inter_ManDeriveSatSolverM114p(
             assert( 0 );
     }
     // connector clauses
-    Aig_ManForEachPi( pFrames, pObj, i )
+    Aig_ManForEachCi( pFrames, pObj, i )
     { 
         if ( i == Aig_ManRegNum(pAig) )
             break;
@@ -296,7 +296,7 @@ Aig_Man_t * Inter_ManInterpolateM114pPudlak( M114p_Solver_t s, Vec_Int_t * vMapR
     Vec_IntFree( vLiterals );
     Vec_IntFree( vClauses );
     Vec_IntFree( vResolvent );
-    Aig_ObjCreatePo( p, pInter );
+    Aig_ObjCreateCo( p, pInter );
     Aig_ManCleanup( p );
     return p;
 }
@@ -372,7 +372,7 @@ Aig_Man_t * Inter_ManpInterpolateM114( M114p_Solver_t s, Vec_Int_t * vMapRoots,
 
     assert( Vec_PtrSize(vInters) == M114p_SolverProofClauseNum(s) );
     Vec_PtrFree( vInters );
-    Aig_ObjCreatePo( p, pInter );
+    Aig_ObjCreateCo( p, pInter );
     Aig_ManCleanup( p );
     assert( Aig_ManCheck(p) );
     return p;
diff --git a/src/proof/live/liveness.c b/src/proof/live/liveness.c
index a86a8cd1..d961e509 100644
--- a/src/proof/live/liveness.c
+++ b/src/proof/live/liveness.c
@@ -119,7 +119,7 @@ char * retrieveTruePiName( Abc_Ntk_t *pNtkOld, Aig_Man_t *pAigOld, Aig_Man_t *pA
     int index;
 
     assert( Saig_ObjIsPi( pAigNew, pObjPivot ) );
-    Aig_ManForEachPi( pAigNew, pObj, index )
+    Aig_ManForEachCi( pAigNew, pObj, index )
         if( pObj == pObjPivot )
             break;
     assert( index < Aig_ManPiNum( pAigNew ) - Aig_ManRegNum( pAigNew ) );
@@ -287,7 +287,7 @@ Aig_Man_t * LivenessToSafetyTransformation( int mode, Abc_Ntk_t * pNtk, Aig_Man_
     Saig_ManForEachPi( p, pObj, i )
     {
         piCopied++;
-        pObj->pData = Aig_ObjCreatePi(pNew);
+        pObj->pData = Aig_ObjCreateCi(pNew);
         Vec_PtrPush( vecPis, pObj->pData );
         nodeName = Abc_UtilStrsav(Abc_ObjName( Abc_NtkPi( pNtk, i ) ));
         Vec_PtrPush( vecPiNames, nodeName );
@@ -298,7 +298,7 @@ Aig_Man_t * LivenessToSafetyTransformation( int mode, Abc_Ntk_t * pNtk, Aig_Man_
     //****************************************************************
     if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
     {
-        pObjSavePi = Aig_ObjCreatePi( pNew );
+        pObjSavePi = Aig_ObjCreateCi( pNew );
         nodeName = "SAVE_BIERE",
         Vec_PtrPush( vecPiNames, nodeName );
     }
@@ -309,7 +309,7 @@ Aig_Man_t * LivenessToSafetyTransformation( int mode, Abc_Ntk_t * pNtk, Aig_Man_
     Saig_ManForEachLo( p, pObj, i )
     {
         loCopied++;
-        pObj->pData = Aig_ObjCreatePi(pNew);
+        pObj->pData = Aig_ObjCreateCi(pNew);
         Vec_PtrPush( vecLos, pObj->pData );
         nodeName = Abc_UtilStrsav(Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i ) ));
         Vec_PtrPush( vecLoNames, nodeName );
@@ -321,7 +321,7 @@ Aig_Man_t * LivenessToSafetyTransformation( int mode, Abc_Ntk_t * pNtk, Aig_Man_
     if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
     {
         loCreated++;
-        pObjSavedLo = Aig_ObjCreatePi( pNew );
+        pObjSavedLo = Aig_ObjCreateCi( pNew );
         Vec_PtrPush( vecLos, pObjSavedLo );
         nodeName = "SAVED_LO";
         Vec_PtrPush( vecLoNames, nodeName );
@@ -360,7 +360,7 @@ Aig_Man_t * LivenessToSafetyTransformation( int mode, Abc_Ntk_t * pNtk, Aig_Man_
                 pArgument = Aig_NotCond( (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) );
                 pObjAndAcc = Aig_And( pNew, pArgument, pObjAndAcc );
             }
-            pObjOriginalSafetyPropertyOutput = Aig_ObjCreatePo( pNew, Aig_Not(pObjAndAcc) );
+            pObjOriginalSafetyPropertyOutput = Aig_ObjCreateCo( pNew, Aig_Not(pObjAndAcc) );
         }
         else if( Vec_PtrSize( vAssertSafety ) != 0 && Vec_PtrSize( vAssumeSafety ) != 0 )
         {
@@ -379,12 +379,12 @@ Aig_Man_t * LivenessToSafetyTransformation( int mode, Abc_Ntk_t * pNtk, Aig_Man_
                 pObjAndAcc = Aig_And( pNew, pArgument, pObjAndAcc );
             }
             collectiveAssumeSafety = pObjAndAcc;
-            pObjOriginalSafetyPropertyOutput = Aig_ObjCreatePo( pNew, Aig_And( pNew, Aig_Not(collectiveAssertSafety), collectiveAssumeSafety ) );
+            pObjOriginalSafetyPropertyOutput = Aig_ObjCreateCo( pNew, Aig_And( pNew, Aig_Not(collectiveAssertSafety), collectiveAssumeSafety ) );
         }
         else
         {
             printf("WARNING!! No safety property is found, a new (negated) constant 1 output is created\n");
-            pObjOriginalSafetyPropertyOutput = Aig_ObjCreatePo( pNew, Aig_Not( Aig_ManConst1(pNew) ) );
+            pObjOriginalSafetyPropertyOutput = Aig_ObjCreateCo( pNew, Aig_Not( Aig_ManConst1(pNew) ) );
         }
     }
 
@@ -394,7 +394,7 @@ Aig_Man_t * LivenessToSafetyTransformation( int mode, Abc_Ntk_t * pNtk, Aig_Man_
     //********************************************************************
     if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
     {
-        pObjSafetyPropertyOutput = Aig_ObjCreatePo( pNew, (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData );
+        pObjSafetyPropertyOutput = Aig_ObjCreateCo( pNew, (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData );
     }
 
     // create register inputs for the original registers
@@ -403,7 +403,7 @@ Aig_Man_t * LivenessToSafetyTransformation( int mode, Abc_Ntk_t * pNtk, Aig_Man_
     Saig_ManForEachLo( p, pObj, i )
     {
         pMatch = Saig_ObjLoToLi( p, pObj );
-        Aig_ObjCreatePo( pNew, Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pMatch)->pData, Aig_ObjFaninC0( pMatch ) ) );
+        Aig_ObjCreateCo( pNew, Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pMatch)->pData, Aig_ObjFaninC0( pMatch ) ) );
         nRegCount++;
         liCopied++;
     }
@@ -412,7 +412,7 @@ Aig_Man_t * LivenessToSafetyTransformation( int mode, Abc_Ntk_t * pNtk, Aig_Man_
     if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
     {
         #ifndef DUPLICATE_CKT_DEBUG
-            pObjSavedLi = Aig_ObjCreatePo( pNew, pObjSaveOrSaved );
+            pObjSavedLi = Aig_ObjCreateCo( pNew, pObjSaveOrSaved );
             nRegCount++;
             liCreated++;
 
@@ -423,7 +423,7 @@ Aig_Man_t * LivenessToSafetyTransformation( int mode, Abc_Ntk_t * pNtk, Aig_Man_
     // create the family of shadow registers, then create the cascade of Xnor and And gates for the comparator 
             Saig_ManForEachLo( p, pObj, i )
             {
-                pObjShadowLo = Aig_ObjCreatePi( pNew );
+                pObjShadowLo = Aig_ObjCreateCi( pNew );
 
                 #ifdef PROPAGATE_NAMES
                     Vec_PtrPush( vecLos, pObjShadowLo );
@@ -434,7 +434,7 @@ Aig_Man_t * LivenessToSafetyTransformation( int mode, Abc_Ntk_t * pNtk, Aig_Man_
                 #endif
 
                 pObjShadowLiDriver = Aig_Mux( pNew, pObjSaveAndNotSaved, (Aig_Obj_t *)pObj->pData, pObjShadowLo );
-                pObjShadowLi = Aig_ObjCreatePo( pNew, pObjShadowLiDriver );
+                pObjShadowLi = Aig_ObjCreateCo( pNew, pObjShadowLiDriver );
                 nRegCount++;
                 loCreated++; liCreated++;
         
@@ -459,7 +459,7 @@ Aig_Man_t * LivenessToSafetyTransformation( int mode, Abc_Ntk_t * pNtk, Aig_Man_
                 {
                     liveLatch++;
                     pDriverImage = Aig_NotCond((Aig_Obj_t *)Aig_Regular(Aig_ObjChild0( pObj ))->pData, Aig_ObjFaninC0(pObj));
-                    pObjShadowLo = Aig_ObjCreatePi( pNew );
+                    pObjShadowLo = Aig_ObjCreateCi( pNew );
 
                     #ifdef PROPAGATE_NAMES
                         Vec_PtrPush( vecLos, pObjShadowLo );
@@ -469,7 +469,7 @@ Aig_Man_t * LivenessToSafetyTransformation( int mode, Abc_Ntk_t * pNtk, Aig_Man_
                     #endif
 
                     pObjShadowLiDriver = Aig_Or( pNew, pObjShadowLo, Aig_And( pNew, pDriverImage, pObjSaveOrSaved ) );
-                    pObjShadowLi = Aig_ObjCreatePo( pNew, pObjShadowLiDriver );
+                    pObjShadowLi = Aig_ObjCreateCo( pNew, pObjShadowLiDriver );
                     nRegCount++;
                     loCreated++; liCreated++;
             
@@ -488,7 +488,7 @@ Aig_Man_t * LivenessToSafetyTransformation( int mode, Abc_Ntk_t * pNtk, Aig_Man_
                 {
                     fairLatch++;
                     pDriverImage = Aig_NotCond((Aig_Obj_t *)Aig_Regular(Aig_ObjChild0( pObj ))->pData, Aig_ObjFaninC0(pObj));
-                    pObjShadowLo = Aig_ObjCreatePi( pNew );
+                    pObjShadowLo = Aig_ObjCreateCi( pNew );
 
                     #ifdef PROPAGATE_NAMES
                         Vec_PtrPush( vecLos, pObjShadowLo );
@@ -498,7 +498,7 @@ Aig_Man_t * LivenessToSafetyTransformation( int mode, Abc_Ntk_t * pNtk, Aig_Man_
                     #endif
 
                     pObjShadowLiDriver = Aig_Or( pNew, pObjShadowLo, Aig_And( pNew, pDriverImage, pObjSaveOrSaved ) );
-                    pObjShadowLi = Aig_ObjCreatePo( pNew, pObjShadowLiDriver );
+                    pObjShadowLi = Aig_ObjCreateCo( pNew, pObjShadowLiDriver );
                     nRegCount++;
                     loCreated++; liCreated++;
             
@@ -584,7 +584,7 @@ Aig_Man_t * LivenessToSafetyTransformationAbs( int mode, Abc_Ntk_t * pNtk, Aig_M
     Saig_ManForEachPi( p, pObj, i )
     {
         piCopied++;
-        pObj->pData = Aig_ObjCreatePi(pNew);
+        pObj->pData = Aig_ObjCreateCi(pNew);
         Vec_PtrPush( vecPis, pObj->pData );
         nodeName = Abc_UtilStrsav(Abc_ObjName( Abc_NtkPi( pNtk, i ) ));
         Vec_PtrPush( vecPiNames, nodeName );
@@ -595,7 +595,7 @@ Aig_Man_t * LivenessToSafetyTransformationAbs( int mode, Abc_Ntk_t * pNtk, Aig_M
     //****************************************************************
     if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
     {
-        pObjSavePi = Aig_ObjCreatePi( pNew );
+        pObjSavePi = Aig_ObjCreateCi( pNew );
         nodeName = "SAVE_BIERE",
         Vec_PtrPush( vecPiNames, nodeName );
     }
@@ -606,7 +606,7 @@ Aig_Man_t * LivenessToSafetyTransformationAbs( int mode, Abc_Ntk_t * pNtk, Aig_M
     Saig_ManForEachLo( p, pObj, i )
     {
         loCopied++;
-        pObj->pData = Aig_ObjCreatePi(pNew);
+        pObj->pData = Aig_ObjCreateCi(pNew);
         Vec_PtrPush( vecLos, pObj->pData );
         nodeName = Abc_UtilStrsav(Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i ) ));
         Vec_PtrPush( vecLoNames, nodeName );
@@ -618,7 +618,7 @@ Aig_Man_t * LivenessToSafetyTransformationAbs( int mode, Abc_Ntk_t * pNtk, Aig_M
     if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
     {
         loCreated++;
-        pObjSavedLo = Aig_ObjCreatePi( pNew );
+        pObjSavedLo = Aig_ObjCreateCi( pNew );
         Vec_PtrPush( vecLos, pObjSavedLo );
         nodeName = "SAVED_LO";
         Vec_PtrPush( vecLoNames, nodeName );
@@ -657,7 +657,7 @@ Aig_Man_t * LivenessToSafetyTransformationAbs( int mode, Abc_Ntk_t * pNtk, Aig_M
                 pArgument = Aig_NotCond( (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) );
                 pObjAndAcc = Aig_And( pNew, pArgument, pObjAndAcc );
             }
-            Aig_ObjCreatePo( pNew, Aig_Not(pObjAndAcc) );
+            Aig_ObjCreateCo( pNew, Aig_Not(pObjAndAcc) );
         }
         else if( Vec_PtrSize( vAssertSafety ) != 0 && Vec_PtrSize( vAssumeSafety ) != 0 )
         {
@@ -676,12 +676,12 @@ Aig_Man_t * LivenessToSafetyTransformationAbs( int mode, Abc_Ntk_t * pNtk, Aig_M
                 pObjAndAcc = Aig_And( pNew, pArgument, pObjAndAcc );
             }
             collectiveAssumeSafety = pObjAndAcc;
-            Aig_ObjCreatePo( pNew, Aig_And( pNew, Aig_Not(collectiveAssertSafety), collectiveAssumeSafety ) );
+            Aig_ObjCreateCo( pNew, Aig_And( pNew, Aig_Not(collectiveAssertSafety), collectiveAssumeSafety ) );
         }
         else
         {
             printf("WARNING!! No safety property is found, a new (negated) constant 1 output is created\n");
-            Aig_ObjCreatePo( pNew, Aig_Not( Aig_ManConst1(pNew) ) );
+            Aig_ObjCreateCo( pNew, Aig_Not( Aig_ManConst1(pNew) ) );
         }
     }
 
@@ -691,7 +691,7 @@ Aig_Man_t * LivenessToSafetyTransformationAbs( int mode, Abc_Ntk_t * pNtk, Aig_M
     //********************************************************************
     if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
     {
-        pObjSafetyPropertyOutput = Aig_ObjCreatePo( pNew, (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData );
+        pObjSafetyPropertyOutput = Aig_ObjCreateCo( pNew, (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData );
     }
 
     // create register inputs for the original registers
@@ -700,7 +700,7 @@ Aig_Man_t * LivenessToSafetyTransformationAbs( int mode, Abc_Ntk_t * pNtk, Aig_M
     Saig_ManForEachLo( p, pObj, i )
     {
         pMatch = Saig_ObjLoToLi( p, pObj );
-        Aig_ObjCreatePo( pNew, Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pMatch)->pData, Aig_ObjFaninC0( pMatch ) ) );
+        Aig_ObjCreateCo( pNew, Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pMatch)->pData, Aig_ObjFaninC0( pMatch ) ) );
         nRegCount++;
         liCopied++;
     }
@@ -709,7 +709,7 @@ Aig_Man_t * LivenessToSafetyTransformationAbs( int mode, Abc_Ntk_t * pNtk, Aig_M
     if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
     {
         #ifndef DUPLICATE_CKT_DEBUG
-            pObjSavedLi = Aig_ObjCreatePo( pNew, pObjSaveOrSaved );
+            pObjSavedLi = Aig_ObjCreateCo( pNew, pObjSaveOrSaved );
             nRegCount++;
             liCreated++;
 
@@ -725,7 +725,7 @@ Aig_Man_t * LivenessToSafetyTransformationAbs( int mode, Abc_Ntk_t * pNtk, Aig_M
             }
             Vec_IntForEachEntry( vFlops, iEntry, i )
             {
-                pObjShadowLo = Aig_ObjCreatePi( pNew );
+                pObjShadowLo = Aig_ObjCreateCi( pNew );
                 pObj = Aig_ManLo( p, iEntry );
 
                 #ifdef PROPAGATE_NAMES
@@ -737,7 +737,7 @@ Aig_Man_t * LivenessToSafetyTransformationAbs( int mode, Abc_Ntk_t * pNtk, Aig_M
                 #endif
 
                 pObjShadowLiDriver = Aig_Mux( pNew, pObjSaveAndNotSaved, (Aig_Obj_t *)pObj->pData, pObjShadowLo );
-                pObjShadowLi = Aig_ObjCreatePo( pNew, pObjShadowLiDriver );
+                pObjShadowLi = Aig_ObjCreateCo( pNew, pObjShadowLiDriver );
                 nRegCount++;
                 loCreated++; liCreated++;
         
@@ -762,7 +762,7 @@ Aig_Man_t * LivenessToSafetyTransformationAbs( int mode, Abc_Ntk_t * pNtk, Aig_M
                 {
                     liveLatch++;
                     pDriverImage = Aig_NotCond((Aig_Obj_t *)Aig_Regular(Aig_ObjChild0( pObj ))->pData, Aig_ObjFaninC0(pObj));
-                    pObjShadowLo = Aig_ObjCreatePi( pNew );
+                    pObjShadowLo = Aig_ObjCreateCi( pNew );
 
                     #ifdef PROPAGATE_NAMES
                         Vec_PtrPush( vecLos, pObjShadowLo );
@@ -772,7 +772,7 @@ Aig_Man_t * LivenessToSafetyTransformationAbs( int mode, Abc_Ntk_t * pNtk, Aig_M
                     #endif
 
                     pObjShadowLiDriver = Aig_Or( pNew, pObjShadowLo, Aig_And( pNew, pDriverImage, pObjSaveOrSaved ) );
-                    pObjShadowLi = Aig_ObjCreatePo( pNew, pObjShadowLiDriver );
+                    pObjShadowLi = Aig_ObjCreateCo( pNew, pObjShadowLiDriver );
                     nRegCount++;
                     loCreated++; liCreated++;
             
@@ -791,7 +791,7 @@ Aig_Man_t * LivenessToSafetyTransformationAbs( int mode, Abc_Ntk_t * pNtk, Aig_M
                 {
                     fairLatch++;
                     pDriverImage = Aig_NotCond((Aig_Obj_t *)Aig_Regular(Aig_ObjChild0( pObj ))->pData, Aig_ObjFaninC0(pObj));
-                    pObjShadowLo = Aig_ObjCreatePi( pNew );
+                    pObjShadowLo = Aig_ObjCreateCi( pNew );
 
                     #ifdef PROPAGATE_NAMES
                         Vec_PtrPush( vecLos, pObjShadowLo );
@@ -801,7 +801,7 @@ Aig_Man_t * LivenessToSafetyTransformationAbs( int mode, Abc_Ntk_t * pNtk, Aig_M
                     #endif
 
                     pObjShadowLiDriver = Aig_Or( pNew, pObjShadowLo, Aig_And( pNew, pDriverImage, pObjSaveOrSaved ) );
-                    pObjShadowLi = Aig_ObjCreatePo( pNew, pObjShadowLiDriver );
+                    pObjShadowLi = Aig_ObjCreateCo( pNew, pObjShadowLiDriver );
                     nRegCount++;
                     loCreated++; liCreated++;
             
@@ -892,7 +892,7 @@ Aig_Man_t * LivenessToSafetyTransformationOneStepLoop( int mode, Abc_Ntk_t * pNt
     Saig_ManForEachPi( p, pObj, i )
     {
         piCopied++;
-        pObj->pData = Aig_ObjCreatePi(pNew);
+        pObj->pData = Aig_ObjCreateCi(pNew);
         Vec_PtrPush( vecPis, pObj->pData );
         nodeName = Abc_UtilStrsav(Abc_ObjName( Abc_NtkPi( pNtk, i ) ));
         Vec_PtrPush( vecPiNames, nodeName );
@@ -903,7 +903,7 @@ Aig_Man_t * LivenessToSafetyTransformationOneStepLoop( int mode, Abc_Ntk_t * pNt
     //****************************************************************
     if( mode == FULL_BIERE_ONE_LOOP_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_ONE_LOOP_MODE )
     {
-        pObjSavePi = Aig_ObjCreatePi( pNew );
+        pObjSavePi = Aig_ObjCreateCi( pNew );
         nodeName = "SAVE_BIERE",
         Vec_PtrPush( vecPiNames, nodeName );
     }
@@ -914,7 +914,7 @@ Aig_Man_t * LivenessToSafetyTransformationOneStepLoop( int mode, Abc_Ntk_t * pNt
     Saig_ManForEachLo( p, pObj, i )
     {
         loCopied++;
-        pObj->pData = Aig_ObjCreatePi(pNew);
+        pObj->pData = Aig_ObjCreateCi(pNew);
         Vec_PtrPush( vecLos, pObj->pData );
         nodeName = Abc_UtilStrsav(Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i ) ));
         Vec_PtrPush( vecLoNames, nodeName );
@@ -926,7 +926,7 @@ Aig_Man_t * LivenessToSafetyTransformationOneStepLoop( int mode, Abc_Ntk_t * pNt
 
 #if 0
     loCreated++;
-    pObjSavedLo = Aig_ObjCreatePi( pNew );
+    pObjSavedLo = Aig_ObjCreateCi( pNew );
     Vec_PtrPush( vecLos, pObjSavedLo );
     nodeName = "SAVED_LO";
     Vec_PtrPush( vecLoNames, nodeName );
@@ -954,7 +954,7 @@ Aig_Man_t * LivenessToSafetyTransformationOneStepLoop( int mode, Abc_Ntk_t * pNt
     //********************************************************************
     Vec_PtrForEachEntry( Aig_Obj_t *, vAssertSafety, pObj, i )
     {
-        pObj->pData = Aig_ObjCreatePo( pNew, Aig_NotCond(Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) ) );
+        pObj->pData = Aig_ObjCreateCo( pNew, Aig_NotCond(Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) ) );
     }
 #endif
 
@@ -965,7 +965,7 @@ Aig_Man_t * LivenessToSafetyTransformationOneStepLoop( int mode, Abc_Ntk_t * pNt
             pObjAndAcc = NULL;
             Vec_PtrForEachEntry( Aig_Obj_t *, vAssertSafety, pObj, i )
             {
-                //pObj->pData = Aig_ObjCreatePo( pNew, Aig_NotCond(Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) ) );
+                //pObj->pData = Aig_ObjCreateCo( pNew, Aig_NotCond(Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) ) );
                 pArgument = Aig_NotCond( (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) );
                 if( pObjAndAcc == NULL )
                     pObjAndAcc = pArgument;
@@ -975,14 +975,14 @@ Aig_Man_t * LivenessToSafetyTransformationOneStepLoop( int mode, Abc_Ntk_t * pNt
                     pObjAndAcc = Aig_And( pNew, pArgument, pObjAndAccDummy );
                 }
             }
-            Aig_ObjCreatePo( pNew, Aig_Not(pObjAndAcc) );
+            Aig_ObjCreateCo( pNew, Aig_Not(pObjAndAcc) );
         }
         else if( Vec_PtrSize( vAssertSafety ) != 0 && Vec_PtrSize( vAssumeSafety ) != 0 )
         {
             pObjAndAcc = NULL;
             Vec_PtrForEachEntry( Aig_Obj_t *, vAssertSafety, pObj, i )
             {
-                //pObj->pData = Aig_ObjCreatePo( pNew, Aig_NotCond(Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) ) );
+                //pObj->pData = Aig_ObjCreateCo( pNew, Aig_NotCond(Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) ) );
                 pArgument = Aig_NotCond( (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) );
                 if( pObjAndAcc == NULL )
                     pObjAndAcc = pArgument;
@@ -996,7 +996,7 @@ Aig_Man_t * LivenessToSafetyTransformationOneStepLoop( int mode, Abc_Ntk_t * pNt
             pObjAndAcc = NULL;
             Vec_PtrForEachEntry( Aig_Obj_t *, vAssumeSafety, pObj, i )
             {
-                //pObj->pData = Aig_ObjCreatePo( pNew, Aig_NotCond(Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) ) );
+                //pObj->pData = Aig_ObjCreateCo( pNew, Aig_NotCond(Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) ) );
                 pArgument = Aig_NotCond( (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) );
                 if( pObjAndAcc == NULL )
                     pObjAndAcc = pArgument;
@@ -1007,7 +1007,7 @@ Aig_Man_t * LivenessToSafetyTransformationOneStepLoop( int mode, Abc_Ntk_t * pNt
                 }
             }
             collectiveAssumeSafety = pObjAndAcc;
-            Aig_ObjCreatePo( pNew, Aig_And( pNew, Aig_Not(collectiveAssertSafety), collectiveAssumeSafety ) );
+            Aig_ObjCreateCo( pNew, Aig_And( pNew, Aig_Not(collectiveAssertSafety), collectiveAssumeSafety ) );
         }
         else
             printf("No safety property is specified, hence no safety gate is created\n");
@@ -1021,7 +1021,7 @@ Aig_Man_t * LivenessToSafetyTransformationOneStepLoop( int mode, Abc_Ntk_t * pNt
 
     if( mode == FULL_BIERE_ONE_LOOP_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_ONE_LOOP_MODE )
     {
-        pObjSafetyPropertyOutput = Aig_ObjCreatePo( pNew, (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData );
+        pObjSafetyPropertyOutput = Aig_ObjCreateCo( pNew, (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData );
     }
 
     // create register inputs for the original registers
@@ -1030,15 +1030,15 @@ Aig_Man_t * LivenessToSafetyTransformationOneStepLoop( int mode, Abc_Ntk_t * pNt
     Saig_ManForEachLo( p, pObj, i )
     {
         pMatch = Saig_ObjLoToLi( p, pObj );
-        //Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pMatch) );
-        Aig_ObjCreatePo( pNew, Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pMatch)->pData, Aig_ObjFaninC0( pMatch ) ) );
+        //Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pMatch) );
+        Aig_ObjCreateCo( pNew, Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pMatch)->pData, Aig_ObjFaninC0( pMatch ) ) );
         nRegCount++;
         liCopied++;
     }
 
 #if 0
     // create register input corresponding to the register "saved"
-    pObjSavedLi = Aig_ObjCreatePo( pNew, pObjSaveOrSaved );
+    pObjSavedLi = Aig_ObjCreateCo( pNew, pObjSaveOrSaved );
     nRegCount++;
     liCreated++;7
 #endif
@@ -1919,7 +1919,7 @@ Aig_Man_t * LivenessToSafetyTransformationWithLTL( int mode, Abc_Ntk_t * pNtk, A
         Saig_ManForEachPi( p, pObj, i )
         {
             piCopied++;
-            pObj->pData = Aig_ObjCreatePi(pNew);
+            pObj->pData = Aig_ObjCreateCi(pNew);
             Vec_PtrPush( vecPis, pObj->pData );
             nodeName = Abc_UtilStrsav(Abc_ObjName( Abc_NtkPi( pNtk, i ) ));
             Vec_PtrPush( vecPiNames, nodeName );
@@ -1930,7 +1930,7 @@ Aig_Man_t * LivenessToSafetyTransformationWithLTL( int mode, Abc_Ntk_t * pNtk, A
         //****************************************************************
         if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
         {
-            pObjSavePi = Aig_ObjCreatePi( pNew );
+            pObjSavePi = Aig_ObjCreateCi( pNew );
             nodeName = "SAVE_BIERE",
             Vec_PtrPush( vecPiNames, nodeName );
         }
@@ -1941,7 +1941,7 @@ Aig_Man_t * LivenessToSafetyTransformationWithLTL( int mode, Abc_Ntk_t * pNtk, A
         Saig_ManForEachLo( p, pObj, i )
         {
             loCopied++;
-            pObj->pData = Aig_ObjCreatePi(pNew);
+            pObj->pData = Aig_ObjCreateCi(pNew);
             Vec_PtrPush( vecLos, pObj->pData );
             nodeName = Abc_UtilStrsav(Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i ) ));
             Vec_PtrPush( vecLoNames, nodeName );
@@ -1953,7 +1953,7 @@ Aig_Man_t * LivenessToSafetyTransformationWithLTL( int mode, Abc_Ntk_t * pNtk, A
         if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
         {
             loCreated++;
-            pObjSavedLo = Aig_ObjCreatePi( pNew );
+            pObjSavedLo = Aig_ObjCreateCi( pNew );
             Vec_PtrPush( vecLos, pObjSavedLo );
             nodeName = "SAVED_LO";
             Vec_PtrPush( vecLoNames, nodeName );
@@ -1995,7 +1995,7 @@ Aig_Man_t * LivenessToSafetyTransformationWithLTL( int mode, Abc_Ntk_t * pNtk, A
                 }
                 pNegatedSafetyConjunction = Aig_Not(pObjAndAcc);
                 if( mode == FULL_BIERE_MODE || mode == IGNORE_LIVENESS_KEEP_SAFETY_MODE )
-                    pObjOriginalSafetyPropertyOutput = Aig_ObjCreatePo( pNew, Aig_Not(pObjAndAcc) );
+                    pObjOriginalSafetyPropertyOutput = Aig_ObjCreateCo( pNew, Aig_Not(pObjAndAcc) );
             }
             else if( Vec_PtrSize( vAssertSafety ) != 0 && Vec_PtrSize( vAssumeSafety ) != 0 )
             {
@@ -2016,14 +2016,14 @@ Aig_Man_t * LivenessToSafetyTransformationWithLTL( int mode, Abc_Ntk_t * pNtk, A
                 collectiveAssumeSafety = pObjAndAcc;
                 pNegatedSafetyConjunction =  Aig_And( pNew, Aig_Not(collectiveAssertSafety), collectiveAssumeSafety );
                 if( mode == FULL_BIERE_MODE || mode == IGNORE_LIVENESS_KEEP_SAFETY_MODE )
-                    pObjOriginalSafetyPropertyOutput = Aig_ObjCreatePo( pNew, Aig_And( pNew, Aig_Not(collectiveAssertSafety), collectiveAssumeSafety ) );
+                    pObjOriginalSafetyPropertyOutput = Aig_ObjCreateCo( pNew, Aig_And( pNew, Aig_Not(collectiveAssertSafety), collectiveAssumeSafety ) );
             }
             else
             {
                 printf("WARNING!! No safety property is found, a new (negated) constant 1 output is created\n");
                 pNegatedSafetyConjunction = Aig_Not( Aig_ManConst1(pNew) );
                 if( mode == FULL_BIERE_MODE || mode == IGNORE_LIVENESS_KEEP_SAFETY_MODE )
-                    pObjOriginalSafetyPropertyOutput = Aig_ObjCreatePo( pNew, Aig_Not( Aig_ManConst1(pNew) ) );
+                    pObjOriginalSafetyPropertyOutput = Aig_ObjCreateCo( pNew, Aig_Not( Aig_ManConst1(pNew) ) );
             }
         }
         assert( pNegatedSafetyConjunction != NULL );
@@ -2042,7 +2042,7 @@ Aig_Man_t * LivenessToSafetyTransformationWithLTL( int mode, Abc_Ntk_t * pNtk, A
             }
             for( i=0; i<Vec_PtrSize( vTopASTNodeArray ); i++ )
             {
-                pObjSafetyPropertyOutput = Aig_ObjCreatePo( pNew, (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData );
+                pObjSafetyPropertyOutput = Aig_ObjCreateCo( pNew, (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData );
                 Vec_PtrPush( vPoForLtlProps, pObjSafetyPropertyOutput );
             }
         }
@@ -2058,7 +2058,7 @@ Aig_Man_t * LivenessToSafetyTransformationWithLTL( int mode, Abc_Ntk_t * pNtk, A
         Saig_ManForEachLo( p, pObj, i )
         {
             pMatch = Saig_ObjLoToLi( p, pObj );
-            Aig_ObjCreatePo( pNew, Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pMatch)->pData, Aig_ObjFaninC0( pMatch ) ) );
+            Aig_ObjCreateCo( pNew, Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pMatch)->pData, Aig_ObjFaninC0( pMatch ) ) );
             nRegCount++;
             liCopied++;
         }
@@ -2069,7 +2069,7 @@ Aig_Man_t * LivenessToSafetyTransformationWithLTL( int mode, Abc_Ntk_t * pNtk, A
         if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
         {
             #ifndef DUPLICATE_CKT_DEBUG
-                pObjSavedLi = Aig_ObjCreatePo( pNew, pObjSaveOrSaved );
+                pObjSavedLi = Aig_ObjCreateCo( pNew, pObjSaveOrSaved );
                 nRegCount++;
                 liCreated++;
 
@@ -2087,7 +2087,7 @@ Aig_Man_t * LivenessToSafetyTransformationWithLTL( int mode, Abc_Ntk_t * pNtk, A
                 //    if( strcmp(  Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i ) ), "top|route0_queue1_num[0]" ) == 0 
                 //            || strcmp(  Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i ) ), "top|route0_queue1_num[1]" ) == 0 || strcmp(  Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i ) ), "top|route0_queue1_num[2]" ) == 0 )
                     {        
-                        pObjShadowLo = Aig_ObjCreatePi( pNew );
+                        pObjShadowLo = Aig_ObjCreateCi( pNew );
 
                     #ifdef PROPAGATE_NAMES
                         Vec_PtrPush( vecLos, pObjShadowLo );
@@ -2098,7 +2098,7 @@ Aig_Man_t * LivenessToSafetyTransformationWithLTL( int mode, Abc_Ntk_t * pNtk, A
                     #endif
 
                         pObjShadowLiDriver = Aig_Mux( pNew, pObjSaveAndNotSaved, (Aig_Obj_t *)pObj->pData, pObjShadowLo );
-                        pObjShadowLi = Aig_ObjCreatePo( pNew, pObjShadowLiDriver );
+                        pObjShadowLi = Aig_ObjCreateCo( pNew, pObjShadowLiDriver );
                         nRegCount++;
                         loCreated++; liCreated++;
             
@@ -2175,9 +2175,9 @@ Aig_Man_t * LivenessToSafetyTransformationWithLTL( int mode, Abc_Ntk_t * pNtk, A
                                             liveLatch++;
 
                                             pDriverImage = pObj;
-                                            pObjShadowLo = Aig_ObjCreatePi( pNew );
+                                            pObjShadowLo = Aig_ObjCreateCi( pNew );
                                             pObjShadowLiDriver = Aig_Or( pNew, pObjShadowLo, Aig_And( pNew, pDriverImage, pObjSaveOrSaved ) );
-                                            pObjShadowLi = Aig_ObjCreatePo( pNew, pObjShadowLiDriver );
+                                            pObjShadowLi = Aig_ObjCreateCo( pNew, pObjShadowLiDriver );
 
                                             nRegCount++;
                                             loCreated++; liCreated++;
diff --git a/src/proof/live/liveness_sim.c b/src/proof/live/liveness_sim.c
index c631e187..552c5204 100644
--- a/src/proof/live/liveness_sim.c
+++ b/src/proof/live/liveness_sim.c
@@ -82,7 +82,7 @@ static char * retrieveTruePiName( Abc_Ntk_t *pNtkOld, Aig_Man_t *pAigOld, Aig_Ma
     int index;
 
     assert( Saig_ObjIsPi( pAigNew, pObjPivot ) );
-    Aig_ManForEachPi( pAigNew, pObj, index )
+    Aig_ManForEachCi( pAigNew, pObj, index )
         if( pObj == pObjPivot )
             break;
     assert( index < Aig_ManPiNum( pAigNew ) - Aig_ManRegNum( pAigNew ) );
@@ -243,7 +243,7 @@ static Aig_Man_t * LivenessToSafetyTransformationSim( Abc_Ntk_t * pNtk, Aig_Man_
     Saig_ManForEachPi( p, pObj, i )
     {
         piCopied++;
-        pObj->pData = Aig_ObjCreatePi(pNew);
+        pObj->pData = Aig_ObjCreateCi(pNew);
         Vec_PtrPush( vecPis, pObj->pData );
         nodeName = Abc_UtilStrsav(Abc_ObjName( Abc_NtkPi( pNtk, i ) ));
         Vec_PtrPush( vecPiNames, nodeName );
@@ -253,7 +253,7 @@ static Aig_Man_t * LivenessToSafetyTransformationSim( Abc_Ntk_t * pNtk, Aig_Man_
     // Step 4: create the special Pi corresponding to SAVE
     //****************************************************************
 #ifndef DUPLICATE_CKT_DEBUG
-    pObjSavePi = Aig_ObjCreatePi( pNew );
+    pObjSavePi = Aig_ObjCreateCi( pNew );
     nodeName = Abc_UtilStrsav("SAVE_BIERE"),
     Vec_PtrPush( vecPiNames, nodeName );
 #endif
@@ -264,7 +264,7 @@ static Aig_Man_t * LivenessToSafetyTransformationSim( Abc_Ntk_t * pNtk, Aig_Man_
     Saig_ManForEachLo( p, pObj, i )
     {
         loCopied++;
-        pObj->pData = Aig_ObjCreatePi(pNew);
+        pObj->pData = Aig_ObjCreateCi(pNew);
         Vec_PtrPush( vecLos, pObj->pData );
         nodeName = Abc_UtilStrsav(Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i ) ));
         Vec_PtrPush( vecLoNames, nodeName );
@@ -275,7 +275,7 @@ static Aig_Man_t * LivenessToSafetyTransformationSim( Abc_Ntk_t * pNtk, Aig_Man_
     //****************************************************************
 #ifndef DUPLICATE_CKT_DEBUG
     loCreated++;
-    pObjSavedLo = Aig_ObjCreatePi( pNew );
+    pObjSavedLo = Aig_ObjCreateCi( pNew );
     Vec_PtrPush( vecLos, pObjSavedLo );
     nodeName = Abc_UtilStrsav("SAVED_LO");
     Vec_PtrPush( vecLoNames, nodeName );
@@ -303,7 +303,7 @@ static Aig_Man_t * LivenessToSafetyTransformationSim( Abc_Ntk_t * pNtk, Aig_Man_
     // of the whole circuit, discuss with Sat/Alan for an alternative implementation
     //********************************************************************
 #ifndef DUPLICATE_CKT_DEBUG
-    pObjSafetyPropertyOutput = Aig_ObjCreatePo( pNew, (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData );
+    pObjSafetyPropertyOutput = Aig_ObjCreateCo( pNew, (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData );
 #endif
 
     //********************************************************************
@@ -313,7 +313,7 @@ static Aig_Man_t * LivenessToSafetyTransformationSim( Abc_Ntk_t * pNtk, Aig_Man_
 #ifdef DUPLICATE_CKT_DEBUG
     Saig_ManForEachPo( p, pObj, i )
     {
-        Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
+        Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
     }
 #endif
 
@@ -323,15 +323,15 @@ static Aig_Man_t * LivenessToSafetyTransformationSim( Abc_Ntk_t * pNtk, Aig_Man_
     Saig_ManForEachLo( p, pObj, i )
     {
         pMatch = Saig_ObjLoToLi( p, pObj );
-        //Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pMatch) );
-        Aig_ObjCreatePo( pNew, Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pMatch)->pData, Aig_ObjFaninC0( pMatch ) ) );
+        //Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pMatch) );
+        Aig_ObjCreateCo( pNew, Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pMatch)->pData, Aig_ObjFaninC0( pMatch ) ) );
         nRegCount++;
         liCopied++;
     }
 
     // create register input corresponding to the register "saved"
 #ifndef DUPLICATE_CKT_DEBUG
-    pObjSavedLi = Aig_ObjCreatePo( pNew, pObjSaveOrSaved );
+    pObjSavedLi = Aig_ObjCreateCo( pNew, pObjSaveOrSaved );
     nRegCount++;
     liCreated++;
 
@@ -340,7 +340,7 @@ static Aig_Man_t * LivenessToSafetyTransformationSim( Abc_Ntk_t * pNtk, Aig_Man_
     // create the family of shadow registers, then create the cascade of Xnor and And gates for the comparator 
     Saig_ManForEachLo( p, pObj, i )
     {
-        pObjShadowLo = Aig_ObjCreatePi( pNew );
+        pObjShadowLo = Aig_ObjCreateCi( pNew );
 
 #ifdef PROPAGATE_NAMES
         Vec_PtrPush( vecLos, pObjShadowLo );
@@ -350,7 +350,7 @@ static Aig_Man_t * LivenessToSafetyTransformationSim( Abc_Ntk_t * pNtk, Aig_Man_
 #endif
 
         pObjShadowLiDriver = Aig_Mux( pNew, pObjSavePi, (Aig_Obj_t *)pObj->pData, pObjShadowLo );
-        pObjShadowLi = Aig_ObjCreatePo( pNew, pObjShadowLiDriver );
+        pObjShadowLi = Aig_ObjCreateCo( pNew, pObjShadowLiDriver );
         nRegCount++;
         loCreated++; liCreated++;
         
@@ -380,7 +380,7 @@ static Aig_Man_t * LivenessToSafetyTransformationSim( Abc_Ntk_t * pNtk, Aig_Man_
             //Aig_ObjPrint( pNew, pObj );
             liveLatch++;
             pDriverImage = Aig_NotCond((Aig_Obj_t *)Aig_Regular(Aig_ObjChild0( pObj ))->pData, Aig_ObjFaninC0(pObj));
-            pObjShadowLo = Aig_ObjCreatePi( pNew );
+            pObjShadowLo = Aig_ObjCreateCi( pNew );
 
 #ifdef PROPAGATE_NAMES
         Vec_PtrPush( vecLos, pObjShadowLo );
@@ -391,7 +391,7 @@ static Aig_Man_t * LivenessToSafetyTransformationSim( Abc_Ntk_t * pNtk, Aig_Man_
 
             pObjShadowLiDriver = Aig_Or( pNew, Aig_Mux(pNew, pObjSavePi, Aig_Not(Aig_ManConst1(pNew)), pObjShadowLo), 
                                                 Aig_And( pNew, pDriverImage, pObjSaveOrSaved ) );
-            pObjShadowLi = Aig_ObjCreatePo( pNew, pObjShadowLiDriver );
+            pObjShadowLi = Aig_ObjCreateCo( pNew, pObjShadowLiDriver );
             nRegCount++;
             loCreated++; liCreated++;
             
@@ -421,7 +421,7 @@ static Aig_Man_t * LivenessToSafetyTransformationSim( Abc_Ntk_t * pNtk, Aig_Man_
             fairLatch++;
             //assert( Aig_ObjIsNode( Aig_ObjChild0( pObj ) ) );
             pDriverImage = Aig_NotCond((Aig_Obj_t *)Aig_Regular(Aig_ObjChild0( pObj ))->pData, Aig_ObjFaninC0(pObj));
-            pObjShadowLo = Aig_ObjCreatePi( pNew );
+            pObjShadowLo = Aig_ObjCreateCi( pNew );
 
 #ifdef PROPAGATE_NAMES
         Vec_PtrPush( vecLos, pObjShadowLo );
@@ -432,7 +432,7 @@ static Aig_Man_t * LivenessToSafetyTransformationSim( Abc_Ntk_t * pNtk, Aig_Man_
 
             pObjShadowLiDriver = Aig_Or( pNew, Aig_Mux(pNew, pObjSavePi, Aig_Not(Aig_ManConst1(pNew)), pObjShadowLo), 
                                     Aig_And( pNew, pDriverImage, pObjSaveOrSaved ) );
-            pObjShadowLi = Aig_ObjCreatePo( pNew, pObjShadowLiDriver );
+            pObjShadowLi = Aig_ObjCreateCo( pNew, pObjShadowLiDriver );
             nRegCount++;
             loCreated++; liCreated++;
             
@@ -520,7 +520,7 @@ static Aig_Man_t * LivenessToSafetyTransformationOneStepLoopSim( Abc_Ntk_t * pNt
     Saig_ManForEachPi( p, pObj, i )
     {
         piCopied++;
-        pObj->pData = Aig_ObjCreatePi(pNew);
+        pObj->pData = Aig_ObjCreateCi(pNew);
         Vec_PtrPush( vecPis, pObj->pData );
         nodeName = Abc_UtilStrsav(Abc_ObjName( Abc_NtkPi( pNtk, i ) ));
         Vec_PtrPush( vecPiNames, nodeName );
@@ -529,7 +529,7 @@ static Aig_Man_t * LivenessToSafetyTransformationOneStepLoopSim( Abc_Ntk_t * pNt
     //****************************************************************
     // Step 4: create the special Pi corresponding to SAVE
     //****************************************************************
-    pObjSavePi = Aig_ObjCreatePi( pNew );
+    pObjSavePi = Aig_ObjCreateCi( pNew );
     nodeName = "SAVE_BIERE",
     Vec_PtrPush( vecPiNames, nodeName );
         
@@ -539,7 +539,7 @@ static Aig_Man_t * LivenessToSafetyTransformationOneStepLoopSim( Abc_Ntk_t * pNt
     Saig_ManForEachLo( p, pObj, i )
     {
         loCopied++;
-        pObj->pData = Aig_ObjCreatePi(pNew);
+        pObj->pData = Aig_ObjCreateCi(pNew);
         Vec_PtrPush( vecLos, pObj->pData );
         nodeName = Abc_UtilStrsav(Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i ) ));
         Vec_PtrPush( vecLoNames, nodeName );
@@ -551,7 +551,7 @@ static Aig_Man_t * LivenessToSafetyTransformationOneStepLoopSim( Abc_Ntk_t * pNt
 
 #if 0
     loCreated++;
-    pObjSavedLo = Aig_ObjCreatePi( pNew );
+    pObjSavedLo = Aig_ObjCreateCi( pNew );
     Vec_PtrPush( vecLos, pObjSavedLo );
     nodeName = "SAVED_LO";
     Vec_PtrPush( vecLoNames, nodeName );
@@ -579,7 +579,7 @@ static Aig_Man_t * LivenessToSafetyTransformationOneStepLoopSim( Abc_Ntk_t * pNt
     // of the whole circuit, discuss with Sat/Alan for an alternative implementation
     //********************************************************************
 
-    pObjSafetyPropertyOutput = Aig_ObjCreatePo( pNew, (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData );
+    pObjSafetyPropertyOutput = Aig_ObjCreateCo( pNew, (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData );
 
     // create register inputs for the original registers
     nRegCount = 0;
@@ -587,15 +587,15 @@ static Aig_Man_t * LivenessToSafetyTransformationOneStepLoopSim( Abc_Ntk_t * pNt
     Saig_ManForEachLo( p, pObj, i )
     {
         pMatch = Saig_ObjLoToLi( p, pObj );
-        //Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pMatch) );
-        Aig_ObjCreatePo( pNew, Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pMatch)->pData, Aig_ObjFaninC0( pMatch ) ) );
+        //Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pMatch) );
+        Aig_ObjCreateCo( pNew, Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pMatch)->pData, Aig_ObjFaninC0( pMatch ) ) );
         nRegCount++;
         liCopied++;
     }
 
 #if 0
     // create register input corresponding to the register "saved"
-    pObjSavedLi = Aig_ObjCreatePo( pNew, pObjSaveOrSaved );
+    pObjSavedLi = Aig_ObjCreateCo( pNew, pObjSaveOrSaved );
     nRegCount++;
     liCreated++;
 #endif
diff --git a/src/proof/llb/llb1Constr.c b/src/proof/llb/llb1Constr.c
index 67fb30ba..4ce911db 100644
--- a/src/proof/llb/llb1Constr.c
+++ b/src/proof/llb/llb1Constr.c
@@ -236,7 +236,7 @@ DdManager * Llb_ManConstructGlobalBdds( Aig_Man_t * p )
     Cudd_AutodynEnable( dd,  CUDD_REORDER_SYMM_SIFT );
     pObj = Aig_ManConst1(p);
     pObj->pData = Cudd_ReadOne(dd);  Cudd_Ref( (DdNode *)pObj->pData );
-    Aig_ManForEachPi( p, pObj, i )
+    Aig_ManForEachCi( p, pObj, i )
     {
         pObj->pData = Cudd_bddIthVar(dd, i);  Cudd_Ref( (DdNode *)pObj->pData );
     }
@@ -246,7 +246,7 @@ DdManager * Llb_ManConstructGlobalBdds( Aig_Man_t * p )
         bBdd1 = Cudd_NotCond( (DdNode *)Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj) );
         pObj->pData = Cudd_bddAnd( dd, bBdd0, bBdd1 );   Cudd_Ref( (DdNode *)pObj->pData );
     }
-    Aig_ManForEachPo( p, pObj, i )
+    Aig_ManForEachCo( p, pObj, i )
     {
         pObj->pData = Cudd_NotCond( (DdNode *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );  Cudd_Ref( (DdNode *)pObj->pData );
     }
diff --git a/src/proof/llb/llb1Hint.c b/src/proof/llb/llb1Hint.c
index f68030ff..6e705a38 100644
--- a/src/proof/llb/llb1Hint.c
+++ b/src/proof/llb/llb1Hint.c
@@ -46,7 +46,7 @@ int Llb_ManMaxFanoutCi( Aig_Man_t * pAig )
 {
     Aig_Obj_t * pObj; 
     int i, WeightMax = -ABC_INFINITY, iInput = -1;
-    Aig_ManForEachPi( pAig, pObj, i )
+    Aig_ManForEachCi( pAig, pObj, i )
         if ( WeightMax < Aig_ObjRefs(pObj) )
         {
             WeightMax = Aig_ObjRefs(pObj);
diff --git a/src/proof/llb/llb1Pivot.c b/src/proof/llb/llb1Pivot.c
index 688060bc..7a5bb66f 100644
--- a/src/proof/llb/llb1Pivot.c
+++ b/src/proof/llb/llb1Pivot.c
@@ -154,7 +154,7 @@ void Llb_ManLabelLiCones( Aig_Man_t * p )
     int i;
     // mark const and PIs
     Aig_ManConst1(p)->fMarkB = 1;
-    Aig_ManForEachPi( p, pObj, i )
+    Aig_ManForEachCi( p, pObj, i )
         pObj->fMarkB = 1;
     // mark cones
     Saig_ManForEachLi( p, pObj, i )
@@ -223,7 +223,7 @@ Vec_Int_t * Llb_ManMarkPivotNodes( Aig_Man_t * p, int fUseInternal )
     Aig_Obj_t * pObj;
     int i;
     // mark inputs/outputs
-    Aig_ManForEachPi( p, pObj, i )
+    Aig_ManForEachCi( p, pObj, i )
         pObj->fMarkA = 1;
     Saig_ManForEachLi( p, pObj, i )
         pObj->fMarkA = 1;
@@ -235,7 +235,7 @@ Vec_Int_t * Llb_ManMarkPivotNodes( Aig_Man_t * p, int fUseInternal )
     // assign variable numbers
     Aig_ManConst1(p)->fMarkA = 0;
     vVar2Obj = Vec_IntAlloc( 100 );
-    Aig_ManForEachPi( p, pObj, i )
+    Aig_ManForEachCi( p, pObj, i )
         Vec_IntPush( vVar2Obj, Aig_ObjId(pObj) );
     Aig_ManForEachNode( p, pObj, i )
         if ( pObj->fMarkA )
diff --git a/src/proof/llb/llb1Reach.c b/src/proof/llb/llb1Reach.c
index 722a8342..d8c667ae 100644
--- a/src/proof/llb/llb1Reach.c
+++ b/src/proof/llb/llb1Reach.c
@@ -430,7 +430,7 @@ DdNode * Llb_ManCreateConstraints( Llb_Man_t * p, Vec_Int_t * vHints, int fUseNs
     // transfer them to the global AIG
     Aig_ManCleanData( p->pAigGlo );
     Aig_ManConst1( p->pAigGlo )->pData = Cudd_ReadOne( p->dd );
-    Aig_ManForEachPi( p->pAigGlo, pObj, i )
+    Aig_ManForEachCi( p->pAigGlo, pObj, i )
         pObj->pData = Aig_ManPi(p->pAig, i)->pData;
     // derive consraints
     bConstr = Cudd_ReadOne( p->dd );   Cudd_Ref( bConstr );
diff --git a/src/proof/llb/llb2Flow.c b/src/proof/llb/llb2Flow.c
index 544d7c04..295f0bfe 100644
--- a/src/proof/llb/llb2Flow.c
+++ b/src/proof/llb/llb2Flow.c
@@ -960,7 +960,7 @@ void Llb_ManFlowPrepareCut( Aig_Man_t * p, Vec_Ptr_t * vLower, Vec_Ptr_t * vUppe
     }
     // clean PIs and const
     Aig_ManConst1(p)->fMarkB = 0;
-    Aig_ManForEachPi( p, pObj, i )
+    Aig_ManForEachCi( p, pObj, i )
         pObj->fMarkB = 0;
     // clean upper cut
 //printf( "Upper: ");
@@ -1077,7 +1077,7 @@ Vec_Ptr_t * Llb_ManComputeCutLo( Aig_Man_t * p )
     Aig_Obj_t * pObj;
     int i;
     vMinCut = Vec_PtrAlloc( 100 );
-    Aig_ManForEachPi( p, pObj, i )
+    Aig_ManForEachCi( p, pObj, i )
         Vec_PtrPush( vMinCut, pObj );
     return vMinCut;
 }
diff --git a/src/proof/llb/llb3Nonlin.c b/src/proof/llb/llb3Nonlin.c
index d28edecc..678a6fff 100644
--- a/src/proof/llb/llb3Nonlin.c
+++ b/src/proof/llb/llb3Nonlin.c
@@ -712,7 +712,7 @@ Llb_Mnn_t * Llb_MnnStart( Aig_Man_t * pInit, Aig_Man_t * pAig, Gia_ParLlb_t *  p
     p->vRings = Vec_PtrAlloc( 100 );
     // create leaves
     p->vLeaves = Vec_PtrAlloc( Aig_ManPiNum(pAig) );
-    Aig_ManForEachPi( pAig, pObj, i )
+    Aig_ManForEachCi( pAig, pObj, i )
         Vec_PtrPush( p->vLeaves, pObj );
     // create roots
     p->vRoots = Vec_PtrAlloc( Aig_ManPoNum(pAig) );
@@ -723,7 +723,7 @@ Llb_Mnn_t * Llb_MnnStart( Aig_Man_t * pInit, Aig_Man_t * pAig, Gia_ParLlb_t *  p
     p->pOrderL2= ABC_CALLOC( int, Aig_ManObjNumMax(pAig) );
     p->pOrderG = ABC_CALLOC( int, Aig_ManObjNumMax(pAig) );
     p->pVars2Q = ABC_CALLOC( int, Aig_ManObjNumMax(pAig) );
-    Aig_ManForEachPi( pAig, pObj, i )
+    Aig_ManForEachCi( pAig, pObj, i )
         p->pVars2Q[Aig_ObjId(pObj)] = 1;
     for ( i = 0; i < Aig_ManObjNumMax(pAig); i++ )
         p->pOrderL[i] = p->pOrderL2[i] = p->pOrderG[i] = i;
diff --git a/src/proof/llb/llb4Cex.c b/src/proof/llb/llb4Cex.c
index 3a1c96e5..69ba6ab1 100644
--- a/src/proof/llb/llb4Cex.c
+++ b/src/proof/llb/llb4Cex.c
@@ -230,7 +230,7 @@ Vec_Ptr_t * Llb4_Nonlin4VerifyCex( Aig_Man_t * pAig, Abc_Cex_t * p )
         Aig_ManForEachNode( pAig, pObj, k )
             pObj->fMarkB = (Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj)) & 
                            (Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj));
-        Aig_ManForEachPo( pAig, pObj, k )
+        Aig_ManForEachCo( pAig, pObj, k )
             pObj->fMarkB = Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj);
         if ( i == p->iFrame )
             break;
diff --git a/src/proof/llb/llb4Cluster.c b/src/proof/llb/llb4Cluster.c
index 8d29eed4..c151a618 100644
--- a/src/proof/llb/llb4Cluster.c
+++ b/src/proof/llb/llb4Cluster.c
@@ -94,20 +94,20 @@ Vec_Int_t * Llb_Nonlin4FindOrder( Aig_Man_t * pAig, int * pCounter )
     Aig_ManForEachNode( pAig, pObj, i )
         if ( Aig_ObjLevel(pObj) > 3 )
             pObj->fMarkA = 1;
-    Aig_ManForEachPo( pAig, pObj, i )
+    Aig_ManForEachCo( pAig, pObj, i )
         Aig_ObjFanin0(pObj)->fMarkA = 0;
 
     // collect nodes in the order
     vOrder = Vec_IntStartFull( Aig_ManObjNumMax(pAig) );
     Aig_ManIncrementTravId( pAig );
     Aig_ObjSetTravIdCurrent( pAig, Aig_ManConst1(pAig) );
-//    Aig_ManForEachPo( pAig, pObj, i )
+//    Aig_ManForEachCo( pAig, pObj, i )
     Saig_ManForEachLi( pAig, pObj, i )
     {
         Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), Counter++ );
         Llb_Nonlin4FindOrder_rec( pAig, Aig_ObjFanin0(pObj), vOrder, &Counter );
     }
-    Aig_ManForEachPi( pAig, pObj, i )
+    Aig_ManForEachCi( pAig, pObj, i )
         if ( Llb_ObjBddVar(vOrder, pObj) < 0 )
             Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), Counter++ );
     Aig_ManCleanMarkA( pAig );
@@ -232,7 +232,7 @@ Vec_Int_t * Llb_Nonlin4FindVars2Q( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t *
     Vec_IntFill( vVars2Q, Cudd_ReadSize(dd), 1 );
     Saig_ManForEachLo( pAig, pObj, i )
         Vec_IntWriteEntry( vVars2Q, Llb_ObjBddVar(vOrder, pObj), 0 );
-//    Aig_ManForEachPo( pAig, pObj, i )
+//    Aig_ManForEachCo( pAig, pObj, i )
     Saig_ManForEachLi( pAig, pObj, i )
         Vec_IntWriteEntry( vVars2Q, Llb_ObjBddVar(vOrder, pObj), 0 );
     return vVars2Q;
diff --git a/src/proof/llb/llb4Nonlin.c b/src/proof/llb/llb4Nonlin.c
index 6442d62e..31f94acf 100644
--- a/src/proof/llb/llb4Nonlin.c
+++ b/src/proof/llb/llb4Nonlin.c
@@ -81,7 +81,7 @@ DdNode * Llb_Nonlin4ComputeBad( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * vO
     Aig_ManCleanData( pAig );
     // assign elementary variables
     Aig_ManConst1(pAig)->pData = Cudd_ReadOne(dd); 
-    Aig_ManForEachPi( pAig, pObj, i )
+    Aig_ManForEachCi( pAig, pObj, i )
         pObj->pData = Cudd_bddIthVar( dd, Llb_ObjBddVar(vOrder, pObj) );
     // compute internal nodes
     vNodes = Aig_ManDfsNodes( pAig, (Aig_Obj_t **)Vec_PtrArray(pAig->vPos), Saig_ManPoNum(pAig) );
@@ -171,7 +171,7 @@ Vec_Ptr_t * Llb_Nonlin4DerivePartitions( DdManager * dd, Aig_Man_t * pAig, Vec_I
     Aig_ManCleanData( pAig );
     // assign elementary variables
     Aig_ManConst1(pAig)->pData = Cudd_ReadOne(dd); 
-    Aig_ManForEachPi( pAig, pObj, i )
+    Aig_ManForEachCi( pAig, pObj, i )
         pObj->pData = Cudd_bddIthVar( dd, Llb_ObjBddVar(vOrder, pObj) );
     Aig_ManForEachNode( pAig, pObj, i )
         if ( Llb_ObjBddVar(vOrder, pObj) >= 0 )
@@ -248,7 +248,7 @@ Vec_Int_t * Llb_Nonlin4CreateOrderSimple( Aig_Man_t * pAig )
     Aig_Obj_t * pObj;
     int i, Counter = 0;
     vOrder = Vec_IntStartFull( Aig_ManObjNumMax(pAig) );
-    Aig_ManForEachPi( pAig, pObj, i )
+    Aig_ManForEachCi( pAig, pObj, i )
         Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), Counter++ );
     Saig_ManForEachLi( pAig, pObj, i )
         Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), Counter++ );
@@ -364,7 +364,7 @@ printf( "Techmapping added %d pivots.\n", Vec_IntSize(vNodes) );
         Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), Counter++ );
         Llb_Nonlin4CreateOrder_rec( pAig, Aig_ObjFanin0(pObj), vOrder, &Counter );
     }
-    Aig_ManForEachPi( pAig, pObj, i )
+    Aig_ManForEachCi( pAig, pObj, i )
         if ( Llb_ObjBddVar(vOrder, pObj) < 0 )
         {
 //            if ( Saig_ObjIsLo(pAig, pObj) )
diff --git a/src/proof/llb/llb4Sweep.c b/src/proof/llb/llb4Sweep.c
index d13c366f..292fb176 100644
--- a/src/proof/llb/llb4Sweep.c
+++ b/src/proof/llb/llb4Sweep.c
@@ -92,12 +92,12 @@ Vec_Int_t * Llb_Nonlin4SweepOrder( Aig_Man_t * pAig, int * pCounter, int fSaveAl
     vOrder = Vec_IntStartFull( Aig_ManObjNumMax(pAig) );
     Aig_ManIncrementTravId( pAig );
     Aig_ObjSetTravIdCurrent( pAig, Aig_ManConst1(pAig) );
-    Aig_ManForEachPo( pAig, pObj, i )
+    Aig_ManForEachCo( pAig, pObj, i )
     {
         Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), Counter++ );
         Llb_Nonlin4SweepOrder_rec( pAig, Aig_ObjFanin0(pObj), vOrder, &Counter, fSaveAll );
     }
-    Aig_ManForEachPi( pAig, pObj, i )
+    Aig_ManForEachCi( pAig, pObj, i )
         if ( Llb_ObjBddVar(vOrder, pObj) < 0 )
             Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), Counter++ );
 //    assert( Counter == Aig_ManObjNum(pAig) - 1 ); // no dangling nodes
@@ -127,7 +127,7 @@ int Llb4_Nonlin4SweepCutpoints( Aig_Man_t * pAig, Vec_Int_t * vOrder, int nBddLi
     dd = Cudd_Init( Aig_ManObjNumMax(pAig), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
     // assign elementary variables
     Aig_ManCleanData( pAig );
-    Aig_ManForEachPi( pAig, pObj, i )
+    Aig_ManForEachCi( pAig, pObj, i )
         pObj->pData = Cudd_bddIthVar( dd, Llb_ObjBddVar(vOrder, pObj) );
     // sweep internal nodes
     Aig_ManForEachNode( pAig, pObj, i )
diff --git a/src/proof/pdr/pdrClass.c b/src/proof/pdr/pdrClass.c
index 4b28c196..cbe5e1c2 100644
--- a/src/proof/pdr/pdrClass.c
+++ b/src/proof/pdr/pdrClass.c
@@ -55,8 +55,8 @@ Aig_Man_t * Pdr_ManRehashWithMap( Aig_Man_t * pAig, Vec_Int_t * vMap )
     // create CI mapping
     Aig_ManCleanData( pAig );
     Aig_ManConst1(pAig)->pData = Aig_ManConst1(pFrames);
-    Aig_ManForEachPi( pAig, pObj, i )
-        pObj->pData = Aig_ObjCreatePi(pFrames);
+    Aig_ManForEachCi( pAig, pObj, i )
+        pObj->pData = Aig_ObjCreateCi(pFrames);
     Saig_ManForEachLo( pAig, pObj, i )
     {
         iReg = Vec_IntEntry(vMap, i);
@@ -69,8 +69,8 @@ Aig_Man_t * Pdr_ManRehashWithMap( Aig_Man_t * pAig, Vec_Int_t * vMap )
     Aig_ManForEachNode( pAig, pObj, i )
         pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
     // add output nodes
-    Aig_ManForEachPo( pAig, pObj, i )
-        pObj->pData = Aig_ObjCreatePo( pFrames, Aig_ObjChild0Copy(pObj) );
+    Aig_ManForEachCo( pAig, pObj, i )
+        pObj->pData = Aig_ObjCreateCo( pFrames, Aig_ObjChild0Copy(pObj) );
     // finish off
     Aig_ManCleanup( pFrames );
     Aig_ManSetRegNum( pFrames, Aig_ManRegNum(pAig) );
diff --git a/src/proof/ssw/sswAig.c b/src/proof/ssw/sswAig.c
index 8ab99f83..5cdced62 100644
--- a/src/proof/ssw/sswAig.c
+++ b/src/proof/ssw/sswAig.c
@@ -120,13 +120,13 @@ static inline void Ssw_FramesConstrainNode( Ssw_Man_t * p, Aig_Man_t * pFrames,
     // add the constraint
     if ( fTwoPos )
     {
-        Aig_ObjCreatePo( pFrames, pObjNew2 );
-        Aig_ObjCreatePo( pFrames, pObjNew );
+        Aig_ObjCreateCo( pFrames, pObjNew2 );
+        Aig_ObjCreateCo( pFrames, pObjNew );
     }
     else
     {
         pMiter = Aig_Exor( pFrames, pObjNew, pObjNew2 );
-        Aig_ObjCreatePo( pFrames, Aig_NotCond(pMiter, Aig_ObjPhaseReal(pMiter)) );
+        Aig_ObjCreateCo( pFrames, Aig_NotCond(pMiter, Aig_ObjPhaseReal(pMiter)) );
     }
 }
 
@@ -155,7 +155,7 @@ Aig_Man_t * Ssw_FramesWithClasses( Ssw_Man_t * p )
     pFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * p->nFrames );
     // create latches for the first frame
     Saig_ManForEachLo( p->pAig, pObj, i )
-        Ssw_ObjSetFrame( p, pObj, 0, Aig_ObjCreatePi(pFrames) );
+        Ssw_ObjSetFrame( p, pObj, 0, Aig_ObjCreateCi(pFrames) );
     // add timeframes
     iLits = 0;
     for ( f = 0; f < p->pPars->nFramesK; f++ )
@@ -164,7 +164,7 @@ Aig_Man_t * Ssw_FramesWithClasses( Ssw_Man_t * p )
         Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(pFrames) );
         Saig_ManForEachPi( p->pAig, pObj, i )
         {
-            pObjNew = Aig_ObjCreatePi(pFrames);
+            pObjNew = Aig_ObjCreateCi(pFrames);
             pObjNew->fPhase = (p->vInits != NULL) && Vec_IntEntry(p->vInits, iLits++);
             Ssw_ObjSetFrame( p, pObj, f, pObjNew );
         }
@@ -179,7 +179,7 @@ Aig_Man_t * Ssw_FramesWithClasses( Ssw_Man_t * p )
             Ssw_FramesConstrainNode( p, pFrames, p->pAig, pObj, f, 1 );
         }
         // transfer to the primary outputs
-        Aig_ManForEachPo( p->pAig, pObj, i )
+        Aig_ManForEachCo( p->pAig, pObj, i )
             Ssw_ObjSetFrame( p, pObj, f, Ssw_ObjChild0Fra(p, pObj,f) );
         // transfer latch input to the latch outputs 
         Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
@@ -188,7 +188,7 @@ Aig_Man_t * Ssw_FramesWithClasses( Ssw_Man_t * p )
     assert( p->vInits == NULL || Vec_IntSize(p->vInits) == iLits + Saig_ManPiNum(p->pAig) );
     // add the POs for the latch outputs of the last frame
     Saig_ManForEachLo( p->pAig, pObj, i )
-        Aig_ObjCreatePo( pFrames, Ssw_ObjFrame( p, pObj, p->pPars->nFramesK ) );
+        Aig_ObjCreateCo( pFrames, Ssw_ObjFrame( p, pObj, p->pPars->nFramesK ) );
 
     // remove dangling nodes
     Aig_ManCleanup( pFrames );
@@ -225,10 +225,10 @@ Aig_Man_t * Ssw_SpeculativeReduction( Ssw_Man_t * p )
     // map constants and PIs
     Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), 0, Aig_ManConst1(pFrames) );
     Saig_ManForEachPi( p->pAig, pObj, i )
-        Ssw_ObjSetFrame( p, pObj, 0, Aig_ObjCreatePi(pFrames) );
+        Ssw_ObjSetFrame( p, pObj, 0, Aig_ObjCreateCi(pFrames) );
     // create latches for the first frame
     Saig_ManForEachLo( p->pAig, pObj, i )
-        Ssw_ObjSetFrame( p, pObj, 0, Aig_ObjCreatePi(pFrames) );
+        Ssw_ObjSetFrame( p, pObj, 0, Aig_ObjCreateCi(pFrames) );
     // set the constraints on the latch outputs
     Saig_ManForEachLo( p->pAig, pObj, i )
         Ssw_FramesConstrainNode( p, pFrames, p->pAig, pObj, 0, 0 );
@@ -241,7 +241,7 @@ Aig_Man_t * Ssw_SpeculativeReduction( Ssw_Man_t * p )
     }
     // add the POs for the latch outputs of the last frame
     Saig_ManForEachLi( p->pAig, pObj, i )
-        Aig_ObjCreatePo( pFrames, Ssw_ObjChild0Fra(p, pObj,0) );
+        Aig_ObjCreateCo( pFrames, Ssw_ObjChild0Fra(p, pObj,0) );
     // remove dangling nodes
     Aig_ManCleanup( pFrames );
     Aig_ManSetRegNum( pFrames, Aig_ManRegNum(p->pAig) );
diff --git a/src/proof/ssw/sswBmc.c b/src/proof/ssw/sswBmc.c
index 8cb14f4a..0eabaa92 100644
--- a/src/proof/ssw/sswBmc.c
+++ b/src/proof/ssw/sswBmc.c
@@ -50,7 +50,7 @@ Aig_Obj_t * Ssw_BmcUnroll_rec( Ssw_Frm_t * pFrm, Aig_Obj_t * pObj, int f )
     if ( Aig_ObjIsConst1(pObj) )
         pRes = Aig_ManConst1( pFrm->pFrames );
     else if ( Saig_ObjIsPi(pFrm->pAig, pObj) )
-        pRes = Aig_ObjCreatePi( pFrm->pFrames );
+        pRes = Aig_ObjCreateCi( pFrm->pFrames );
     else if ( Aig_ObjIsPo(pObj) )
     {
         Ssw_BmcUnroll_rec( pFrm, Aig_ObjFanin0(pObj), f );
diff --git a/src/proof/ssw/sswConstr.c b/src/proof/ssw/sswConstr.c
index 239e35b9..6d8a152d 100644
--- a/src/proof/ssw/sswConstr.c
+++ b/src/proof/ssw/sswConstr.c
@@ -63,19 +63,19 @@ Aig_Man_t * Ssw_FramesWithConstraints( Aig_Man_t * p, int nFrames )
         // map constants and PIs
         Aig_ObjSetCopy( Aig_ManConst1(p), Aig_ManConst1(pFrames) );
         Saig_ManForEachPi( p, pObj, i )
-            Aig_ObjSetCopy( pObj, Aig_ObjCreatePi(pFrames) );
+            Aig_ObjSetCopy( pObj, Aig_ObjCreateCi(pFrames) );
         // add internal nodes of this frame
         Aig_ManForEachNode( p, pObj, i )
             Aig_ObjSetCopy( pObj, Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ) );
         // transfer to the primary output
-        Aig_ManForEachPo( p, pObj, i )
+        Aig_ManForEachCo( p, pObj, i )
             Aig_ObjSetCopy( pObj, Aig_ObjChild0Copy(pObj) );
         // create constraint outputs
         Saig_ManForEachPo( p, pObj, i )
         {
             if ( i < Saig_ManPoNum(p) - Saig_ManConstrNum(p) )
                 continue;
-            Aig_ObjCreatePo( pFrames, Aig_Not( Aig_ObjCopy(pObj) ) );
+            Aig_ObjCreateCo( pFrames, Aig_Not( Aig_ObjCopy(pObj) ) );
         }
         // transfer latch inputs to the latch outputs 
         Saig_ManForEachLiLo( p, pObjLi, pObjLo, i )
@@ -125,10 +125,10 @@ int Ssw_ManSetConstrPhases( Aig_Man_t * p, int nFrames, Vec_Int_t ** pvInits )
     if ( RetValue == l_True && pvInits )
     {
         *pvInits = Vec_IntAlloc( 1000 );
-        Aig_ManForEachPi( pFrames, pObj, i )
+        Aig_ManForEachCi( pFrames, pObj, i )
             Vec_IntPush( *pvInits, sat_solver_var_value(pSat, pCnf->pVarNums[Aig_ObjId(pObj)]) );
 
-//        Aig_ManForEachPi( pFrames, pObj, i )
+//        Aig_ManForEachCi( pFrames, pObj, i )
 //            printf( "%d", Vec_IntEntry(*pvInits, i) );
 //        printf( "\n" );
     }
@@ -268,7 +268,7 @@ void Ssw_ManRefineByConstrSim( Ssw_Man_t * p )
             pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) )
                          & ( Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj) );
         // assign the COs
-        Aig_ManForEachPo( p->pAig, pObj, i )
+        Aig_ManForEachCo( p->pAig, pObj, i )
             pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) );
         // check the outputs
         Saig_ManForEachPo( p->pAig, pObj, i )
@@ -424,7 +424,7 @@ clk = clock();
         Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) );
         Saig_ManForEachPi( p->pAig, pObj, i )
         {
-            pObjNew = Aig_ObjCreatePi(p->pFrames);
+            pObjNew = Aig_ObjCreateCi(p->pFrames);
             pObjNew->fPhase = Vec_IntEntry( p->vInits, iLits++ );
             Ssw_ObjSetFrame( p, pObj, f, pObjNew );
         }
@@ -464,7 +464,7 @@ clk = clock();
         if ( f == p->pPars->nFramesK - 1 )
             break;
         // transfer latch input to the latch outputs 
-        Aig_ManForEachPo( p->pAig, pObj, i )
+        Aig_ManForEachCo( p->pAig, pObj, i )
             Ssw_ObjSetFrame( p, pObj, f, Ssw_ObjChild0Fra(p, pObj, f) );
         // build logic cones for register outputs
         Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
@@ -514,7 +514,7 @@ clk = clock();
         Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) );
         Saig_ManForEachPi( p->pAig, pObj, i )
         {
-            pObjNew = Aig_ObjCreatePi(p->pFrames);
+            pObjNew = Aig_ObjCreateCi(p->pFrames);
             pObjNew->fPhase = Vec_IntEntry( p->vInits, iLits++ );
             Ssw_ObjSetFrame( p, pObj, f, pObjNew );
         }
@@ -544,7 +544,7 @@ clk = clock();
         if ( f == p->pPars->nFramesK - 1 )
             break;
         // transfer latch input to the latch outputs 
-        Aig_ManForEachPo( p->pAig, pObj, i )
+        Aig_ManForEachCo( p->pAig, pObj, i )
             Ssw_ObjSetFrame( p, pObj, f, Ssw_ObjChild0Fra(p, pObj, f) );
         // build logic cones for register outputs
         Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
@@ -648,7 +648,7 @@ clk = clock();
     Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) );
     Saig_ManForEachPi( p->pAig, pObj, i )
     {
-        pObjNew = Aig_ObjCreatePi(p->pFrames);
+        pObjNew = Aig_ObjCreateCi(p->pFrames);
         pObjNew->fPhase = (p->vInits != NULL) && Vec_IntEntry(p->vInits, iLits++);
         Ssw_ObjSetFrame( p, pObj, f, pObjNew );
     }
diff --git a/src/proof/ssw/sswDyn.c b/src/proof/ssw/sswDyn.c
index d9a16e22..0f6002fa 100644
--- a/src/proof/ssw/sswDyn.c
+++ b/src/proof/ssw/sswDyn.c
@@ -215,7 +215,7 @@ void Ssw_ManSweepTransferDyn( Ssw_Man_t * p )
     int i, f, nFrames;
 
     // transfer simulation information
-    Aig_ManForEachPi( p->pAig, pObj, i )
+    Aig_ManForEachCi( p->pAig, pObj, i )
     {
         pObjFraig = Ssw_ObjFrame( p, pObj, 0 );
         if ( pObjFraig == Aig_ManConst0(p->pFrames) )
@@ -385,7 +385,7 @@ clk = clock();
     f = p->pPars->nFramesK;
     Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) );
     Saig_ManForEachPi( p->pAig, pObj, i )
-        Ssw_ObjSetFrame( p, pObj, f, Aig_ObjCreatePi(p->pFrames) );
+        Ssw_ObjSetFrame( p, pObj, f, Aig_ObjCreateCi(p->pFrames) );
     Aig_ManSetPioNumbers( p->pFrames );
     // label nodes corresponding to primary inputs
     Ssw_ManLabelPiNodes( p );
diff --git a/src/proof/ssw/sswFilter.c b/src/proof/ssw/sswFilter.c
index 4f6fb26e..536316ff 100644
--- a/src/proof/ssw/sswFilter.c
+++ b/src/proof/ssw/sswFilter.c
@@ -65,7 +65,7 @@ void Ssw_ManRefineByFilterSim( Ssw_Man_t * p, int nFrames )
             pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) )
                          & ( Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj) );
         // assign the COs
-        Aig_ManForEachPo( p->pAig, pObj, i )
+        Aig_ManForEachCo( p->pAig, pObj, i )
             pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) );
         // transfer
         if ( f == 0 )
@@ -115,7 +115,7 @@ void Ssw_ManRollForward( Ssw_Man_t * p, int nFrames )
             pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) )
                          & ( Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj) );
         // assign the COs
-        Aig_ManForEachPo( p->pAig, pObj, i )
+        Aig_ManForEachCo( p->pAig, pObj, i )
             pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) );
     }
     // record the new pattern
@@ -157,7 +157,7 @@ void Ssw_ManFindStartingState( Ssw_Man_t * p, Abc_Cex_t * pCex )
             pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) )
                          & ( Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj) );
         // assign the COs
-        Aig_ManForEachPo( p->pAig, pObj, i )
+        Aig_ManForEachCo( p->pAig, pObj, i )
             pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) );
     }
     assert( iBit == pCex->nBits );
@@ -317,7 +317,7 @@ int Ssw_ManSweepBmcFilter( Ssw_Man_t * p, int TimeLimit )
         Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) );
         Saig_ManForEachPi( p->pAig, pObj, i )
         {
-            pObjNew = Aig_ObjCreatePi(p->pFrames);
+            pObjNew = Aig_ObjCreateCi(p->pFrames);
             Ssw_ObjSetFrame( p, pObj, f, pObjNew );
         }
         // sweep internal nodes
@@ -351,7 +351,7 @@ int Ssw_ManSweepBmcFilter( Ssw_Man_t * p, int TimeLimit )
         if ( TimeLimit && ((float)TimeLimit <= (float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)) )
             break;
         // transfer latch input to the latch outputs 
-        Aig_ManForEachPo( p->pAig, pObj, i )
+        Aig_ManForEachCo( p->pAig, pObj, i )
             Ssw_ObjSetFrame( p, pObj, f, Ssw_ObjChild0Fra(p, pObj, f) );
         // build logic cones for register outputs
         Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
diff --git a/src/proof/ssw/sswIslands.c b/src/proof/ssw/sswIslands.c
index ca95cf23..3173ec6f 100644
--- a/src/proof/ssw/sswIslands.c
+++ b/src/proof/ssw/sswIslands.c
@@ -90,7 +90,7 @@ void Ssw_MatchingStart( Aig_Man_t * p0, Aig_Man_t * p1, Vec_Int_t * vPairs )
         assert( pObj1->pData == pObj0 );
     }
     // make sure the POs are not matched
-    Aig_ManForEachPo( p0, pObj0, i )
+    Aig_ManForEachCo( p0, pObj0, i )
     {
         pObj1 = Aig_ManPo( p1, i );
         assert( pObj0->pData == NULL );
@@ -295,7 +295,7 @@ void Ssw_MatchingComplete( Aig_Man_t * p0, Aig_Man_t * p1 )
     {
         if ( pObj0->pData != NULL )
             continue;
-        pObj1 = Aig_ObjCreatePi( p1 );
+        pObj1 = Aig_ObjCreateCi( p1 );
         pObj0->pData = pObj1;
         pObj1->pData = pObj0;
         Vec_PtrPush( vNewLis, pObj0Li );
@@ -311,7 +311,7 @@ void Ssw_MatchingComplete( Aig_Man_t * p0, Aig_Man_t * p1 )
     }
     // create register outputs in p0 that are absent in p1
     Vec_PtrForEachEntry( Aig_Obj_t *, vNewLis, pObj0Li, i )
-        Aig_ObjCreatePo( p1, Aig_ObjChild0Copy(pObj0Li) );
+        Aig_ObjCreateCo( p1, Aig_ObjChild0Copy(pObj0Li) );
     // increment the number of registers
     Aig_ManSetRegNum( p1, Aig_ManRegNum(p1) + Vec_PtrSize(vNewLis) );
     Vec_PtrFree( vNewLis );
diff --git a/src/proof/ssw/sswLcorr.c b/src/proof/ssw/sswLcorr.c
index ce9c2563..c41a74ef 100644
--- a/src/proof/ssw/sswLcorr.c
+++ b/src/proof/ssw/sswLcorr.c
@@ -49,7 +49,7 @@ void Ssw_ManSweepTransfer( Ssw_Man_t * p )
     unsigned * pInfo;
     int i;
     // transfer simulation information
-    Aig_ManForEachPi( p->pAig, pObj, i )
+    Aig_ManForEachCi( p->pAig, pObj, i )
     {
         pObjFraig = Ssw_ObjFrame( p, pObj, 0 );
         if ( pObjFraig == Aig_ManConst0(p->pFrames) )
@@ -245,7 +245,7 @@ int Ssw_ManSweepLatch( Ssw_Man_t * p )
     // map constants and PIs
     Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), 0, Aig_ManConst1(p->pFrames) );
     Saig_ManForEachPi( p->pAig, pObj, i )
-        Ssw_ObjSetFrame( p, pObj, 0, Aig_ObjCreatePi(p->pFrames) );
+        Ssw_ObjSetFrame( p, pObj, 0, Aig_ObjCreateCi(p->pFrames) );
 
     // implement equivalence classes
     Saig_ManForEachLo( p->pAig, pObj, i )
@@ -253,7 +253,7 @@ int Ssw_ManSweepLatch( Ssw_Man_t * p )
         pRepr = Aig_ObjRepr( p->pAig, pObj );
         if ( pRepr == NULL )
         {
-            pTemp = Aig_ObjCreatePi(p->pFrames);
+            pTemp = Aig_ObjCreateCi(p->pFrames);
             pTemp->pData = pObj;
         }
         else
diff --git a/src/proof/ssw/sswRarity.c b/src/proof/ssw/sswRarity.c
index 25a80be7..6e36ae12 100644
--- a/src/proof/ssw/sswRarity.c
+++ b/src/proof/ssw/sswRarity.c
@@ -587,7 +587,7 @@ void Ssw_RarManSimulate( Ssw_RarMan_t * p, Vec_Int_t * vInit, int fUpdate, int f
     Aig_ManIncrementTravId( p->pAig );
     // check comb inputs
     if ( fUpdate )
-    Aig_ManForEachPi( p->pAig, pObj, i )
+    Aig_ManForEachCi( p->pAig, pObj, i )
     {
         pRepr = Aig_ObjRepr(p->pAig, pObj);
         if ( pRepr == NULL || Aig_ObjIsTravIdCurrent( p->pAig, pRepr ) )
@@ -631,7 +631,7 @@ void Ssw_RarManSimulate( Ssw_RarMan_t * p, Vec_Int_t * vInit, int fUpdate, int f
         }
     }
     // transfer to POs
-    Aig_ManForEachPo( p->pAig, pObj, i )
+    Aig_ManForEachCo( p->pAig, pObj, i )
     {
         pSim  = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
         pSim0 = Ssw_RarObjSim( p, Aig_ObjFaninId0(pObj) );
@@ -826,7 +826,7 @@ static Vec_Int_t * Ssw_RarFindStartingState( Aig_Man_t * pAig, Abc_Cex_t * pCex
             pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) )
                          & ( Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj) );
         // assign the COs
-        Aig_ManForEachPo( pAig, pObj, i )
+        Aig_ManForEachCo( pAig, pObj, i )
             pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) );
     }
     assert( iBit == pCex->nBits );
diff --git a/src/proof/ssw/sswRarity2.c b/src/proof/ssw/sswRarity2.c
index ac22b0d5..dce7ac3e 100644
--- a/src/proof/ssw/sswRarity2.c
+++ b/src/proof/ssw/sswRarity2.c
@@ -277,7 +277,7 @@ static Vec_Int_t * Ssw_RarFindStartingState( Aig_Man_t * pAig, Abc_Cex_t * pCex
             pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) )
                          & ( Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj) );
         // assign the COs
-        Aig_ManForEachPo( pAig, pObj, i )
+        Aig_ManForEachCo( pAig, pObj, i )
             pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) );
     }
     assert( iBit == pCex->nBits );
diff --git a/src/proof/ssw/sswSemi.c b/src/proof/ssw/sswSemi.c
index ec50ab50..a04f6f54 100644
--- a/src/proof/ssw/sswSemi.c
+++ b/src/proof/ssw/sswSemi.c
@@ -198,7 +198,7 @@ clk = clock();
         // map constants and PIs
         Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) );
         Saig_ManForEachPi( p->pAig, pObj, i )
-            Ssw_ObjSetFrame( p, pObj, f, Aig_ObjCreatePi(p->pFrames) );
+            Ssw_ObjSetFrame( p, pObj, f, Aig_ObjCreateCi(p->pFrames) );
         // sweep internal nodes
         Aig_ManForEachNode( p->pAig, pObj, i )
         {
diff --git a/src/proof/ssw/sswSim.c b/src/proof/ssw/sswSim.c
index 9ce89a71..946224cd 100644
--- a/src/proof/ssw/sswSim.c
+++ b/src/proof/ssw/sswSim.c
@@ -458,7 +458,7 @@ int * Ssw_SmlCheckOutputSavePattern( Ssw_Sml_t * p, Aig_Obj_t * pObjPo )
     BestPat = i * 32 + k;
     // fill in the counter-example data
     pModel = ABC_ALLOC( int, Aig_ManPiNum(p->pAig)+1 );
-    Aig_ManForEachPi( p->pAig, pObjPi, i )
+    Aig_ManForEachCi( p->pAig, pObjPi, i )
     {
         pModel[i] = Abc_InfoHasBit(Ssw_ObjSim(p, pObjPi->Id), BestPat);
 //        printf( "%d", pModel[i] );
@@ -486,7 +486,7 @@ int * Ssw_SmlCheckOutput( Ssw_Sml_t * p )
     // make sure the reference simulation pattern does not detect the bug
     pObj = Aig_ManPo( p->pAig, 0 );
     assert( Aig_ObjFanin0(pObj)->fPhase == (unsigned)Aig_ObjFaninC0(pObj) ); 
-    Aig_ManForEachPo( p->pAig, pObj, i )
+    Aig_ManForEachCo( p->pAig, pObj, i )
     {
         if ( !Ssw_SmlObjIsConstWord( p, Aig_ObjFanin0(pObj) ) )
         {
@@ -628,7 +628,7 @@ void Ssw_SmlAssignDist1( Ssw_Sml_t * p, unsigned * pPat )
     if ( p->nFrames == 1 )
     {
         // copy the PI info 
-        Aig_ManForEachPi( p->pAig, pObj, i )
+        Aig_ManForEachCi( p->pAig, pObj, i )
             Ssw_SmlObjAssignConst( p, pObj, Abc_InfoHasBit(pPat, i), 0 );
         // flip one bit
         Limit = Abc_MinInt( Aig_ManPiNum(p->pAig), p->nWordsTotal * 32 - 1 );
@@ -678,7 +678,7 @@ void Ssw_SmlAssignDist1Plus( Ssw_Sml_t * p, unsigned * pPat )
     assert( p->nFrames > 0 );
 
     // copy the pattern into the primary inputs
-    Aig_ManForEachPi( p->pAig, pObj, i )
+    Aig_ManForEachCi( p->pAig, pObj, i )
         Ssw_SmlObjAssignConst( p, pObj, Abc_InfoHasBit(pPat, i), 0 );
 
     // set distance one PIs for the first frame
@@ -909,7 +909,7 @@ void Ssw_SmlInitialize( Ssw_Sml_t * p, int fInit )
     }
     else
     {
-        Aig_ManForEachPi( p->pAig, pObj, i )
+        Aig_ManForEachCi( p->pAig, pObj, i )
             Ssw_SmlAssignRandom( p, pObj );
     }
 }
diff --git a/src/proof/ssw/sswSimSat.c b/src/proof/ssw/sswSimSat.c
index 4c094a2d..098b1e0f 100644
--- a/src/proof/ssw/sswSimSat.c
+++ b/src/proof/ssw/sswSimSat.c
@@ -48,7 +48,7 @@ void Ssw_ManResimulateBit( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pRepr )
     int i, RetValue1, RetValue2, clk = clock();
     // set the PI simulation information
     Aig_ManConst1(p->pAig)->fMarkB = 1;
-    Aig_ManForEachPi( p->pAig, pObj, i )
+    Aig_ManForEachCi( p->pAig, pObj, i )
         pObj->fMarkB = Abc_InfoHasBit( p->pPatWords, i );
     // simulate internal nodes
     Aig_ManForEachNode( p->pAig, pObj, i )
diff --git a/src/proof/ssw/sswSweep.c b/src/proof/ssw/sswSweep.c
index e2a4f65d..a3a8d1c8 100644
--- a/src/proof/ssw/sswSweep.c
+++ b/src/proof/ssw/sswSweep.c
@@ -117,7 +117,7 @@ void Ssw_SmlSavePatternAigPhase( Ssw_Man_t * p, int f )
     Aig_Obj_t * pObj;
     int i;
     memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
-    Aig_ManForEachPi( p->pAig, pObj, i )
+    Aig_ManForEachCi( p->pAig, pObj, i )
         if ( Aig_ObjPhaseReal( Ssw_ObjFrame(p, pObj, f) ) )
             Abc_InfoSetBit( p->pPatWords, i );
 }
@@ -138,7 +138,7 @@ void Ssw_SmlSavePatternAig( Ssw_Man_t * p, int f )
     Aig_Obj_t * pObj;
     int i;
     memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
-    Aig_ManForEachPi( p->pAig, pObj, i )
+    Aig_ManForEachCi( p->pAig, pObj, i )
         if ( Ssw_ManGetSatVarValue( p, pObj, f ) )
             Abc_InfoSetBit( p->pPatWords, i );
 }
@@ -284,7 +284,7 @@ clk = clock();
         // map constants and PIs
         Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) );
         Saig_ManForEachPi( p->pAig, pObj, i )
-            Ssw_ObjSetFrame( p, pObj, f, Aig_ObjCreatePi(p->pFrames) );
+            Ssw_ObjSetFrame( p, pObj, f, Aig_ObjCreateCi(p->pFrames) );
         // sweep internal nodes
         Aig_ManForEachNode( p->pAig, pObj, i )
         {
@@ -298,7 +298,7 @@ clk = clock();
         if ( f == p->pPars->nFramesK - 1 )
             break;
         // transfer latch input to the latch outputs 
-        Aig_ManForEachPo( p->pAig, pObj, i )
+        Aig_ManForEachCo( p->pAig, pObj, i )
             Ssw_ObjSetFrame( p, pObj, f, Ssw_ObjChild0Fra(p, pObj, f) );
         // build logic cones for register outputs
         Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
@@ -393,7 +393,7 @@ clk = clock();
     f = p->pPars->nFramesK;
     Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) );
     Saig_ManForEachPi( p->pAig, pObj, i )
-        Ssw_ObjSetFrame( p, pObj, f, Aig_ObjCreatePi(p->pFrames) );
+        Ssw_ObjSetFrame( p, pObj, f, Aig_ObjCreateCi(p->pFrames) );
 p->timeReduce += clock() - clk;
 
     // sweep internal nodes