Renamed Aig_ObjIsPi/Po to be ...Ci/Co and Aig_Man(Pi/Po)Num to be ...(Ci/Co)...

72 files changed, 409 insertions, 409 deletions

diff --git a/src/proof/bbr/bbrNtbdd.c b/src/proof/bbr/bbrNtbdd.c
index 49c2873b..f61c3d73 100644
--- a/src/proof/bbr/bbrNtbdd.c
+++ b/src/proof/bbr/bbrNtbdd.c
@@ -135,7 +135,7 @@ int Aig_ManSizeOfGlobalBdds( Aig_Man_t * p )
     Aig_Obj_t * pObj;
     int RetValue, i;
     // complement the global functions
-    vFuncsGlob = Vec_PtrAlloc( Aig_ManPoNum(p) );
+    vFuncsGlob = Vec_PtrAlloc( Aig_ManCoNum(p) );
     Aig_ManForEachCo( p, pObj, i )
         Vec_PtrPush( vFuncsGlob, Aig_ObjGlobalBdd(pObj) );
     RetValue = Cudd_SharingSize( (DdNode **)Vec_PtrArray(vFuncsGlob), Vec_PtrSize(vFuncsGlob) );
@@ -162,7 +162,7 @@ DdManager * Aig_ManComputeGlobalBdds( Aig_Man_t * p, int nBddSizeMax, int fDropI
     DdNode * bFunc;
     int i, Counter;
     // start the manager
-    dd = Cudd_Init( Aig_ManPiNum(p), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
+    dd = Cudd_Init( Aig_ManCiNum(p), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
     // set reordering
     if ( fReorder )
         Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT );
diff --git a/src/proof/bbr/bbrReach.c b/src/proof/bbr/bbrReach.c
index 1b5c3984..eda4d7cf 100644
--- a/src/proof/bbr/bbrReach.c
+++ b/src/proof/bbr/bbrReach.c
@@ -548,7 +548,7 @@ int Aig_ManVerifyUsingBdds( Aig_Man_t * pInit, Saig_ParBbr_t * pPars )
         return Aig_ManVerifyUsingBdds_int( pInit, pPars );
     // create new AIG
     p = Aig_ManDupTrim( pInit );
-    assert( Aig_ManPiNum(p) < Aig_ManPiNum(pInit) );
+    assert( Aig_ManCiNum(p) < Aig_ManCiNum(pInit) );
     assert( Aig_ManRegNum(p) == Aig_ManRegNum(pInit) );
     RetValue = Aig_ManVerifyUsingBdds_int( p, pPars );
     if ( RetValue != 0 )
diff --git a/src/proof/cec/cecCec.c b/src/proof/cec/cecCec.c
index 22474042..aa36a28e 100644
--- a/src/proof/cec/cecCec.c
+++ b/src/proof/cec/cecCec.c
@@ -97,7 +97,7 @@ Abc_PrintTime( 1, "Time", clock() - clkTotal );
                 Abc_Print( 1, "Counter-example verification has failed.\n" );
             else 
             {
-//                Aig_Obj_t * pObj = Aig_ManPo(pMiterCec, iOut);
+//                Aig_Obj_t * pObj = Aig_ManCo(pMiterCec, iOut);
 //                Aig_Obj_t * pFan = Aig_ObjFanin0(pObj);
                 Abc_Print( 1, "Primary output %d has failed", iOut );
                 if ( nOuts-1 >= 0 )
diff --git a/src/proof/dch/dchAig.c b/src/proof/dch/dchAig.c
index 59828443..1b6f1539 100644
--- a/src/proof/dch/dchAig.c
+++ b/src/proof/dch/dchAig.c
@@ -73,8 +73,8 @@ Aig_Man_t * Dch_DeriveTotalAig( Vec_Ptr_t * vAigs )
     pAig = (Aig_Man_t *)Vec_PtrEntry( vAigs, 0 );
     Vec_PtrForEachEntry( Aig_Man_t *, vAigs, pAig2, i )
     {
-        assert( Aig_ManPiNum(pAig) == Aig_ManPiNum(pAig2) );
-        assert( Aig_ManPoNum(pAig) == Aig_ManPoNum(pAig2) );
+        assert( Aig_ManCiNum(pAig) == Aig_ManCiNum(pAig2) );
+        assert( Aig_ManCoNum(pAig) == Aig_ManCoNum(pAig2) );
         nNodes += Aig_ManNodeNum(pAig2);
         Aig_ManCleanData( pAig2 );
     }
@@ -87,14 +87,14 @@ Aig_Man_t * Dch_DeriveTotalAig( Vec_Ptr_t * vAigs )
     {
         pObjPi = Aig_ObjCreateCi( pAigTotal );
         Vec_PtrForEachEntry( Aig_Man_t *, vAigs, pAig2, k )
-            Aig_ManPi( pAig2, i )->pData = pObjPi;
+            Aig_ManCi( pAig2, i )->pData = pObjPi;
     }
     // construct the AIG in the order of POs
     Aig_ManForEachCo( pAig, pObj, i )
     {
         Vec_PtrForEachEntry( Aig_Man_t *, vAigs, pAig2, k )
         {
-            pObjPo = Aig_ManPo( pAig2, i );
+            pObjPo = Aig_ManCo( pAig2, i );
             Dch_DeriveTotalAig_rec( pAigTotal, Aig_ObjFanin0(pObjPo) );
         }
         Aig_ObjCreateCo( pAigTotal, Aig_ObjChild0Copy(pObj) );
diff --git a/src/proof/dch/dchChoice.c b/src/proof/dch/dchChoice.c
index 1de11509..7a763d84 100644
--- a/src/proof/dch/dchChoice.c
+++ b/src/proof/dch/dchChoice.c
@@ -117,7 +117,7 @@ int Dch_ObjCheckTfi_rec( Aig_Man_t * p, Aig_Obj_t * pObj )
     // check the trivial cases
     if ( pObj == NULL )
         return 0;
-    if ( Aig_ObjIsPi(pObj) )
+    if ( Aig_ObjIsCi(pObj) )
         return 0;
     if ( pObj->fMarkA )
         return 1;
@@ -289,7 +289,7 @@ int Aig_ManCheckAcyclic_rec( Aig_Man_t * p, Aig_Obj_t * pNode, int fVerbose )
 {
     Aig_Obj_t * pFanin;
     int fAcyclic;
-    if ( Aig_ObjIsPi(pNode) || Aig_ObjIsConst1(pNode) )
+    if ( Aig_ObjIsCi(pNode) || Aig_ObjIsConst1(pNode) )
         return 1;
     assert( Aig_ObjIsNode(pNode) );
     // make sure the node is not visited
diff --git a/src/proof/dch/dchClass.c b/src/proof/dch/dchClass.c
index 24476309..1f974236 100644
--- a/src/proof/dch/dchClass.c
+++ b/src/proof/dch/dchClass.c
@@ -350,12 +350,12 @@ void Dch_ClassesPrepare( Dch_Cla_t * p, int fLatchCorr, int nMaxLevs )
     {
         if ( fLatchCorr )
         {
-            if ( !Aig_ObjIsPi(pObj) )
+            if ( !Aig_ObjIsCi(pObj) )
                 continue;
         }
         else
         {
-            if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
+            if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsCi(pObj) )
                 continue;
             // skip the node with more that the given number of levels
             if ( nMaxLevs && (int)pObj->Level >= nMaxLevs )
@@ -400,7 +400,7 @@ void Dch_ClassesPrepare( Dch_Cla_t * p, int fLatchCorr, int nMaxLevs )
     nEntries2 = 0;
     Aig_ManForEachObj( p->pAig, pObj, i )
     {
-        if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
+        if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsCi(pObj) )
             continue;
         nNodes = p->pClassSizes[pObj->Id];
         // skip the nodes that are not representatives of non-trivial classes
diff --git a/src/proof/dch/dchCnf.c b/src/proof/dch/dchCnf.c
index 4175a123..b65b096c 100644
--- a/src/proof/dch/dchCnf.c
+++ b/src/proof/dch/dchCnf.c
@@ -217,7 +217,7 @@ void Dch_AddClausesSuper( Dch_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vSuper )
 void Dch_CollectSuper_rec( Aig_Obj_t * pObj, Vec_Ptr_t * vSuper, int fFirst, int fUseMuxes )
 {
     // if the new node is complemented or a PI, another gate begins
-    if ( Aig_IsComplement(pObj) || Aig_ObjIsPi(pObj) || 
+    if ( Aig_IsComplement(pObj) || Aig_ObjIsCi(pObj) || 
          (!fFirst && Aig_ObjRefs(pObj) > 1) || 
          (fUseMuxes && Aig_ObjIsMuxType(pObj)) )
     {
@@ -243,7 +243,7 @@ void Dch_CollectSuper_rec( Aig_Obj_t * pObj, Vec_Ptr_t * vSuper, int fFirst, int
 void Dch_CollectSuper( Aig_Obj_t * pObj, int fUseMuxes, Vec_Ptr_t * vSuper )
 {
     assert( !Aig_IsComplement(pObj) );
-    assert( !Aig_ObjIsPi(pObj) );
+    assert( !Aig_ObjIsCi(pObj) );
     Vec_PtrClear( vSuper );
     Dch_CollectSuper_rec( pObj, vSuper, 1, fUseMuxes );
 }
diff --git a/src/proof/dch/dchSimSat.c b/src/proof/dch/dchSimSat.c
index 808e754a..6f69b47e 100644
--- a/src/proof/dch/dchSimSat.c
+++ b/src/proof/dch/dchSimSat.c
@@ -113,7 +113,7 @@ void Dch_ManResimulateSolved_rec( Dch_Man_t * p, Aig_Obj_t * pObj )
     if ( Aig_ObjIsTravIdCurrent(p->pAigTotal, pObj) )
         return;
     Aig_ObjSetTravIdCurrent(p->pAigTotal, pObj);
-    if ( Aig_ObjIsPi(pObj) )
+    if ( Aig_ObjIsCi(pObj) )
     {
         Aig_Obj_t * pObjFraig;
         int nVarNum;
@@ -151,7 +151,7 @@ void Dch_ManResimulateOther_rec( Dch_Man_t * p, Aig_Obj_t * pObj )
     if ( Aig_ObjIsTravIdCurrent(p->pAigTotal, pObj) )
         return;
     Aig_ObjSetTravIdCurrent(p->pAigTotal, pObj);
-    if ( Aig_ObjIsPi(pObj) )
+    if ( Aig_ObjIsCi(pObj) )
     {
         // set random value
         pObj->fMarkB = Aig_ManRandom(0) & 1;
diff --git a/src/proof/fra/fraBmc.c b/src/proof/fra/fraBmc.c
index b0dd3c86..2ddecf48 100644
--- a/src/proof/fra/fraBmc.c
+++ b/src/proof/fra/fraBmc.c
@@ -395,10 +395,10 @@ void Fra_BmcPerformSimple( Aig_Man_t * pAig, int nFrames, int nBTLimit, int fRew
     if ( fVerbose )
     {
         printf( "AIG:  PI/PO/Reg = %d/%d/%d.  Node = %6d. Lev = %5d.\n", 
-            Aig_ManPiNum(pAig)-Aig_ManRegNum(pAig), Aig_ManPoNum(pAig)-Aig_ManRegNum(pAig), Aig_ManRegNum(pAig),
+            Aig_ManCiNum(pAig)-Aig_ManRegNum(pAig), Aig_ManCoNum(pAig)-Aig_ManRegNum(pAig), Aig_ManRegNum(pAig),
             Aig_ManNodeNum(pAig), Aig_ManLevelNum(pAig) );
         printf( "Time-frames (%d):  PI/PO = %d/%d.  Node = %6d. Lev = %5d.  ", 
-            nFrames, Aig_ManPiNum(pBmc->pAigFrames), Aig_ManPoNum(pBmc->pAigFrames), 
+            nFrames, Aig_ManCiNum(pBmc->pAigFrames), Aig_ManCoNum(pBmc->pAigFrames), 
             Aig_ManNodeNum(pBmc->pAigFrames), Aig_ManLevelNum(pBmc->pAigFrames) );
         ABC_PRT( "Time", clock() - clk );
     }
@@ -417,7 +417,7 @@ void Fra_BmcPerformSimple( Aig_Man_t * pAig, int nFrames, int nBTLimit, int fRew
     clk = clock();
     iOutput = Fra_FraigMiterAssertedOutput( pBmc->pAigFrames );
     if ( iOutput >= 0 )
-        pAig->pSeqModel = Abc_CexMakeTriv( Aig_ManRegNum(pAig), Aig_ManPiNum(pAig)-Aig_ManRegNum(pAig), Aig_ManPoNum(pAig)-Aig_ManRegNum(pAig), iOutput );
+        pAig->pSeqModel = Abc_CexMakeTriv( Aig_ManRegNum(pAig), Aig_ManCiNum(pAig)-Aig_ManRegNum(pAig), Aig_ManCoNum(pAig)-Aig_ManRegNum(pAig), iOutput );
     else
     {
         pBmc->pAigFraig = Fra_FraigEquivence( pBmc->pAigFrames, nBTLimit, 1 );
@@ -428,7 +428,7 @@ void Fra_BmcPerformSimple( Aig_Man_t * pAig, int nFrames, int nBTLimit, int fRew
             ABC_FREE( pBmc->pAigFraig->pData );
         }
         else if ( iOutput >= 0 )
-            pAig->pSeqModel = Abc_CexMakeTriv( Aig_ManRegNum(pAig), Aig_ManPiNum(pAig)-Aig_ManRegNum(pAig), Aig_ManPoNum(pAig)-Aig_ManRegNum(pAig), iOutput );
+            pAig->pSeqModel = Abc_CexMakeTriv( Aig_ManRegNum(pAig), Aig_ManCiNum(pAig)-Aig_ManRegNum(pAig), Aig_ManCoNum(pAig)-Aig_ManRegNum(pAig), iOutput );
     }
     if ( fVerbose )
     {
diff --git a/src/proof/fra/fraCec.c b/src/proof/fra/fraCec.c
index ac11b0bb..0acca245 100644
--- a/src/proof/fra/fraCec.c
+++ b/src/proof/fra/fraCec.c
@@ -60,8 +60,8 @@ int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimi
         pMan->pData = NULL;
 
         // derive CNF
-        pCnf = Cnf_Derive( pMan, Aig_ManPoNum(pMan) );
-    //    pCnf = Cnf_DeriveSimple( pMan, Aig_ManPoNum(pMan) );
+        pCnf = Cnf_Derive( pMan, Aig_ManCoNum(pMan) );
+    //    pCnf = Cnf_DeriveSimple( pMan, Aig_ManCoNum(pMan) );
 
         if ( fFlipBits ) 
             Cnf_DataTranformPolarity( pCnf, 0 );
@@ -166,8 +166,8 @@ int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimi
         pMan->pData = NULL;
 
         // derive CNF
-        pCnf = Cnf_Derive( pMan, Aig_ManPoNum(pMan) );
-    //    pCnf = Cnf_DeriveSimple( pMan, Aig_ManPoNum(pMan) );
+        pCnf = Cnf_Derive( pMan, Aig_ManCoNum(pMan) );
+    //    pCnf = Cnf_DeriveSimple( pMan, Aig_ManCoNum(pMan) );
 
         if ( fFlipBits ) 
             Cnf_DataTranformPolarity( pCnf, 0 );
@@ -293,8 +293,8 @@ int Fra_FraigCec( Aig_Man_t ** ppAig, int nConfLimit, int fVerbose )
 //    assert( RetValue == -1 );
     if ( RetValue == 0 )
     {
-        pAig->pData = ABC_ALLOC( int, Aig_ManPiNum(pAig) );
-        memset( pAig->pData, 0, sizeof(int) * Aig_ManPiNum(pAig) );
+        pAig->pData = ABC_ALLOC( int, Aig_ManCiNum(pAig) );
+        memset( pAig->pData, 0, sizeof(int) * Aig_ManCiNum(pAig) );
         return RetValue;
     }
 
@@ -406,7 +406,7 @@ int Fra_FraigCecPartitioned( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nConfLimi
         if ( fVerbose )
         {
             printf( "Verifying part %4d  (out of %4d)  PI = %5d. PO = %5d. And = %6d. Lev = %4d.\r", 
-                i+1, Vec_PtrSize(vParts), Aig_ManPiNum(pAig), Aig_ManPoNum(pAig), 
+                i+1, Vec_PtrSize(vParts), Aig_ManCiNum(pAig), Aig_ManCoNum(pAig), 
                 Aig_ManNodeNum(pAig), Aig_ManLevelNum(pAig) );
             fflush( stdout );
         }
@@ -459,18 +459,18 @@ int Fra_FraigCecTop( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nConfLimit, int n
     //Abc_NtkDarCec( pNtk1, pNtk2, fPartition, fVerbose );
     int RetValue, clkTotal = clock();
 
-    if ( Aig_ManPiNum(pMan1) != Aig_ManPiNum(pMan1) )
+    if ( Aig_ManCiNum(pMan1) != Aig_ManCiNum(pMan1) )
     {
         printf( "Abc_CommandAbc8Cec(): Miters have different number of PIs.\n" );
         return 0;
     }
-    if ( Aig_ManPoNum(pMan1) != Aig_ManPoNum(pMan1) )
+    if ( Aig_ManCoNum(pMan1) != Aig_ManCoNum(pMan1) )
     {
         printf( "Abc_CommandAbc8Cec(): Miters have different number of POs.\n" );
         return 0;
     }
-    assert( Aig_ManPiNum(pMan1) == Aig_ManPiNum(pMan1) );
-    assert( Aig_ManPoNum(pMan1) == Aig_ManPoNum(pMan1) );
+    assert( Aig_ManCiNum(pMan1) == Aig_ManCiNum(pMan1) );
+    assert( Aig_ManCoNum(pMan1) == Aig_ManCoNum(pMan1) );
 
     // make sure that the first miter has more nodes
     if ( Aig_ManNodeNum(pMan1) < Aig_ManNodeNum(pMan2) )
@@ -484,7 +484,7 @@ int Fra_FraigCecTop( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nConfLimit, int n
     if ( nPartSize )
         RetValue = Fra_FraigCecPartitioned( pMan1, pMan2, nConfLimit, nPartSize, fSmart, fVerbose );
     else // no partitioning
-        RetValue = Fra_FraigCecPartitioned( pMan1, pMan2, nConfLimit, Aig_ManPoNum(pMan1), 0, fVerbose );
+        RetValue = Fra_FraigCecPartitioned( pMan1, pMan2, nConfLimit, Aig_ManCoNum(pMan1), 0, fVerbose );
 
     // report the miter
     if ( RetValue == 1 )
diff --git a/src/proof/fra/fraClass.c b/src/proof/fra/fraClass.c
index f7850241..cef2f673 100644
--- a/src/proof/fra/fraClass.c
+++ b/src/proof/fra/fraClass.c
@@ -291,12 +291,12 @@ void Fra_ClassesPrepare( Fra_Cla_t * p, int fLatchCorr, int nMaxLevs )
     {
         if ( fLatchCorr )
         {
-            if ( !Aig_ObjIsPi(pObj) )
+            if ( !Aig_ObjIsCi(pObj) )
                 continue;
         }
         else
         {
-            if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
+            if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsCi(pObj) )
                 continue;
             // skip the node with more that the given number of levels
             if ( nMaxLevs && (int)pObj->Level > nMaxLevs )
@@ -349,7 +349,7 @@ void Fra_ClassesPrepare( Fra_Cla_t * p, int fLatchCorr, int nMaxLevs )
     nEntries = 0;
     Aig_ManForEachObj( p->pAig, pObj, i )
     {
-        if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
+        if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsCi(pObj) )
             continue;
         // skip the nodes that are not representatives of non-trivial classes
         if ( pObj->fMarkA == 0 )
@@ -800,7 +800,7 @@ Aig_Man_t * Fra_ClassesDeriveAig( Fra_Cla_t * p, int nFramesK )
     Aig_Obj_t ** pLatches, ** ppEquivs;
     int i, k, f, nFramesAll = nFramesK + 1;
     assert( Aig_ManRegNum(p->pAig) > 0 );
-    assert( Aig_ManRegNum(p->pAig) < Aig_ManPiNum(p->pAig) );
+    assert( Aig_ManRegNum(p->pAig) < Aig_ManCiNum(p->pAig) );
     assert( nFramesK > 0 );
     // start the fraig package
     pManFraig = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * nFramesAll );
@@ -832,7 +832,7 @@ Aig_Man_t * Fra_ClassesDeriveAig( Fra_Cla_t * p, int nFramesK )
         if ( f == nFramesAll - 1 )
             break;
         if ( f == nFramesAll - 2 )
-            pManFraig->nAsserts = Aig_ManPoNum(pManFraig);
+            pManFraig->nAsserts = Aig_ManCoNum(pManFraig);
         // save the latch input values
         k = 0;
         Aig_ManForEachLiSeq( p->pAig, pObj, i )
@@ -845,9 +845,9 @@ Aig_Man_t * Fra_ClassesDeriveAig( Fra_Cla_t * p, int nFramesK )
     ABC_FREE( pLatches );
     ABC_FREE( ppEquivs );
     // mark the asserts
-    assert( Aig_ManPoNum(pManFraig) % nFramesAll == 0 );
+    assert( Aig_ManCoNum(pManFraig) % nFramesAll == 0 );
 printf( "Assert miters = %6d. Output miters = %6d.\n", 
-       pManFraig->nAsserts, Aig_ManPoNum(pManFraig) - pManFraig->nAsserts );
+       pManFraig->nAsserts, Aig_ManCoNum(pManFraig) - pManFraig->nAsserts );
     // remove dangling nodes
     Aig_ManCleanup( pManFraig );
     return pManFraig;
diff --git a/src/proof/fra/fraClau.c b/src/proof/fra/fraClau.c
index 28e9e9b9..6c692afa 100644
--- a/src/proof/fra/fraClau.c
+++ b/src/proof/fra/fraClau.c
@@ -108,7 +108,7 @@ Vec_Int_t * Fra_ClauSaveOutputVars( Aig_Man_t * pMan, Cnf_Dat_t * pCnf )
     Vec_Int_t * vVars;
     Aig_Obj_t * pObj;
     int i;
-    vVars = Vec_IntAlloc( Aig_ManPoNum(pMan) );
+    vVars = Vec_IntAlloc( Aig_ManCoNum(pMan) );
     Aig_ManForEachCo( pMan, pObj, i )
         Vec_IntPush( vVars, pCnf->pVarNums[pObj->Id] );
     return vVars;
@@ -130,7 +130,7 @@ Vec_Int_t * Fra_ClauSaveInputVars( Aig_Man_t * pMan, Cnf_Dat_t * pCnf, int nStar
     Vec_Int_t * vVars;
     Aig_Obj_t * pObj;
     int i;
-    vVars = Vec_IntAlloc( Aig_ManPiNum(pMan) - nStarting );
+    vVars = Vec_IntAlloc( Aig_ManCiNum(pMan) - nStarting );
     Aig_ManForEachCi( pMan, pObj, i )
     {
         if ( i < nStarting )
@@ -217,7 +217,7 @@ Cla_Man_t * Fra_ClauStart( Aig_Man_t * pMan )
     Aig_Man_t * pFramesMain;
     Aig_Man_t * pFramesTest;
     Aig_Man_t * pFramesBmc;
-    assert( Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan) == 1 );
+    assert( Aig_ManCoNum(pMan) - Aig_ManRegNum(pMan) == 1 );
 
     // start the manager
     p = ABC_ALLOC( Cla_Man_t, 1 );
@@ -232,8 +232,8 @@ Cla_Man_t * Fra_ClauStart( Aig_Man_t * pMan )
     // derive two timeframes to be checked
     pFramesMain = Aig_ManFrames( pMan, 2, 0, 1, 0, 0, NULL ); // nFrames, fInit, fOuts, fRegs
 //Aig_ManShow( pFramesMain, 0, NULL );
-    assert( Aig_ManPoNum(pFramesMain) == 2 );
-    Aig_ObjChild0Flip( Aig_ManPo(pFramesMain, 0) ); // complement the first output
+    assert( Aig_ManCoNum(pFramesMain) == 2 );
+    Aig_ObjChild0Flip( Aig_ManCo(pFramesMain, 0) ); // complement the first output
     pCnfMain = Cnf_DeriveSimple( pFramesMain, 0 );
 //Cnf_DataWriteIntoFile( pCnfMain, "temp.cnf", 1 );
     p->pSatMain = (sat_solver *)Cnf_DataWriteIntoSolver( pCnfMain, 1, 0 );
@@ -249,7 +249,7 @@ Cla_Man_t * Fra_ClauStart( Aig_Man_t * pMan )
 
     // derive one timeframe to be checked
     pFramesTest = Aig_ManFrames( pMan, 1, 0, 0, 1, 0, NULL );
-    assert( Aig_ManPoNum(pFramesTest) == Aig_ManRegNum(pMan) );
+    assert( Aig_ManCoNum(pFramesTest) == Aig_ManRegNum(pMan) );
     pCnfTest = Cnf_DeriveSimple( pFramesTest, Aig_ManRegNum(pMan) );
     p->pSatTest = (sat_solver *)Cnf_DataWriteIntoSolver( pCnfTest, 1, 0 );
     p->nSatVarsTestBeg = p->nSatVarsTestCur = sat_solver_nvars( p->pSatTest );
@@ -257,12 +257,12 @@ Cla_Man_t * Fra_ClauStart( Aig_Man_t * pMan )
     // derive one timeframe to be checked for BMC
     pFramesBmc = Aig_ManFrames( pMan, 1, 1, 0, 1, 0, NULL );
 //Aig_ManShow( pFramesBmc, 0, NULL );
-    assert( Aig_ManPoNum(pFramesBmc) == Aig_ManRegNum(pMan) );
+    assert( Aig_ManCoNum(pFramesBmc) == Aig_ManRegNum(pMan) );
     pCnfBmc = Cnf_DeriveSimple( pFramesBmc, Aig_ManRegNum(pMan) );
     p->pSatBmc = (sat_solver *)Cnf_DataWriteIntoSolver( pCnfBmc, 1, 0 );
 
     // create variable sets
-    p->vSatVarsMainCs = Fra_ClauSaveInputVars( pFramesMain, pCnfMain, 2 * (Aig_ManPiNum(pMan)-Aig_ManRegNum(pMan)) );
+    p->vSatVarsMainCs = Fra_ClauSaveInputVars( pFramesMain, pCnfMain, 2 * (Aig_ManCiNum(pMan)-Aig_ManRegNum(pMan)) );
     p->vSatVarsTestCs = Fra_ClauSaveLatchVars( pFramesTest, pCnfTest, 1 );
     p->vSatVarsTestNs = Fra_ClauSaveLatchVars( pFramesTest, pCnfTest, 0 );
     p->vSatVarsBmcNs  = Fra_ClauSaveOutputVars( pFramesBmc, pCnfBmc );
@@ -638,7 +638,7 @@ int Fra_Clau( Aig_Man_t * pMan, int nIters, int fVerbose, int fVeryVerbose )
 {
     Cla_Man_t * p;
     int Iter, RetValue, fFailed, i;
-    assert( Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan) == 1 );
+    assert( Aig_ManCoNum(pMan) - Aig_ManRegNum(pMan) == 1 );
     // create the manager
     p = Fra_ClauStart( pMan );
     if ( p == NULL )
diff --git a/src/proof/fra/fraClaus.c b/src/proof/fra/fraClaus.c
index f27c63ce..571cc510 100644
--- a/src/proof/fra/fraClaus.c
+++ b/src/proof/fra/fraClaus.c
@@ -97,7 +97,7 @@ int Fra_ClausRunBmc( Clu_Man_t * p )
     int Lits[2], nLitsTot, RetValue, i;
     // set the output literals
     nLitsTot = 2 * p->pCnf->nVars;
-    pObj = Aig_ManPo(p->pAig, 0);
+    pObj = Aig_ManCo(p->pAig, 0);
     for ( i = 0; i < p->nPref + p->nFrames; i++ )
     {
         Lits[0] = i * nLitsTot + toLitCond( p->pCnf->pVarNums[pObj->Id], 0 ); 
@@ -126,7 +126,7 @@ int Fra_ClausRunSat( Clu_Man_t * p )
     int i, RetValue;
     pLits = ABC_ALLOC( int, p->nFrames + 1 );
     // set the output literals
-    pObj = Aig_ManPo(p->pAig, 0);
+    pObj = Aig_ManCo(p->pAig, 0);
     for ( i = 0; i <= p->nFrames; i++ )
         pLits[i] = i * 2 * p->pCnf->nVars + toLitCond( p->pCnf->pVarNums[pObj->Id], i != p->nFrames ); 
     // try to solve the problem
@@ -154,7 +154,7 @@ int Fra_ClausRunSat0( Clu_Man_t * p )
 {
     Aig_Obj_t * pObj;
     int Lits[2], RetValue;
-    pObj = Aig_ManPo(p->pAig, 0);
+    pObj = Aig_ManCo(p->pAig, 0);
     Lits[0] = toLitCond( p->pCnf->pVarNums[pObj->Id], 0 ); 
     RetValue = sat_solver_solve( p->pSatMain, Lits, Lits + 1, (ABC_INT64_T)p->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
     if ( RetValue == l_False )
@@ -523,7 +523,7 @@ int Fra_ClausCollectLatchClauses( Clu_Man_t * p, Fra_Sml_t * pSeq )
     {
         Aig_Obj_t * pObj;
         int Lits[1];
-        pObj = Aig_ManPo( p->pAig, 0 );
+        pObj = Aig_ManCo( p->pAig, 0 );
         Lits[0] = toLitCond( p->pCnf->pVarNums[pObj->Id], 1 ); 
         Vec_IntPush( p->vLits, Lits[0] );
         Vec_IntPush( p->vClauses, Vec_IntSize(p->vLits) );
@@ -1242,7 +1242,7 @@ int Fra_ClausInductiveClauses( Clu_Man_t * p )
         Aig_Obj_t * pObj;
         int Lits[2];
         // set the output literals
-        pObj = Aig_ManPo(p->pAig, 0);
+        pObj = Aig_ManCo(p->pAig, 0);
         Lits[0] = i * nLitsTot + toLitCond( p->pCnf->pVarNums[pObj->Id], 1 ); 
         // add the clause
         RetValue = sat_solver_addclause( p->pSatMain, Lits, Lits + 1 );
@@ -1637,9 +1637,9 @@ void Fra_ClausEstimateCoverage( Clu_Man_t * p )
             pVar2Id[ p->pCnf->pVarNums[i] ] = i;
         }
     // get storage for one assignment and all assignments
-    assert( Aig_ManPoNum(p->pAig) > 2 );
-    pResultOne = Fra_ObjSim( pComb, Aig_ManPo(p->pAig, 0)->Id );
-    pResultTot = Fra_ObjSim( pComb, Aig_ManPo(p->pAig, 1)->Id );
+    assert( Aig_ManCoNum(p->pAig) > 2 );
+    pResultOne = Fra_ObjSim( pComb, Aig_ManCo(p->pAig, 0)->Id );
+    pResultTot = Fra_ObjSim( pComb, Aig_ManCo(p->pAig, 1)->Id );
     // start the OR of don't-cares
     for ( w = 0; w < nCombSimWords; w++ )
         pResultTot[w] = 0;
@@ -1693,13 +1693,13 @@ if ( p->fVerbose )
 //ABC_PRT( "Sim-seq", clock() - clk );
 }
 
-    assert( !p->fTarget || Aig_ManPoNum(pAig) - Aig_ManRegNum(pAig) == 1 );
+    assert( !p->fTarget || Aig_ManCoNum(pAig) - Aig_ManRegNum(pAig) == 1 );
 
 clk = clock();
     // derive CNF
 //    if ( p->fTarget )
 //        p->pAig->nRegs++;
-    p->pCnf = Cnf_DeriveSimple( p->pAig, Aig_ManPoNum(p->pAig) );
+    p->pCnf = Cnf_DeriveSimple( p->pAig, Aig_ManCoNum(p->pAig) );
 //    if ( p->fTarget )
 //        p->pAig->nRegs--;
 if ( fVerbose )
@@ -1846,8 +1846,8 @@ clk = clock();
         assert( p->nBatches == 1 );
         pTable = fopen( "stats.txt", "a+" );
         fprintf( pTable, "%s ",  pAig->pName );
-        fprintf( pTable, "%d ",  Aig_ManPiNum(pAig)-Aig_ManRegNum(pAig) );
-        fprintf( pTable, "%d ",  Aig_ManPoNum(pAig)-Aig_ManRegNum(pAig) );
+        fprintf( pTable, "%d ",  Aig_ManCiNum(pAig)-Aig_ManRegNum(pAig) );
+        fprintf( pTable, "%d ",  Aig_ManCoNum(pAig)-Aig_ManRegNum(pAig) );
         fprintf( pTable, "%d ",  Aig_ManRegNum(pAig) );
         fprintf( pTable, "%d ",  Aig_ManNodeNum(pAig) );
         fprintf( pTable, "%d ",  p->nCuts );
diff --git a/src/proof/fra/fraCnf.c b/src/proof/fra/fraCnf.c
index 5021e750..7024c0f4 100644
--- a/src/proof/fra/fraCnf.c
+++ b/src/proof/fra/fraCnf.c
@@ -167,7 +167,7 @@ void Fra_AddClausesSuper( Fra_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vSuper )
 void Fra_CollectSuper_rec( Aig_Obj_t * pObj, Vec_Ptr_t * vSuper, int fFirst, int fUseMuxes )
 {
     // if the new node is complemented or a PI, another gate begins
-    if ( Aig_IsComplement(pObj) || Aig_ObjIsPi(pObj) || (!fFirst && Aig_ObjRefs(pObj) > 1) || 
+    if ( Aig_IsComplement(pObj) || Aig_ObjIsCi(pObj) || (!fFirst && Aig_ObjRefs(pObj) > 1) || 
          (fUseMuxes && Aig_ObjIsMuxType(pObj)) )
     {
         Vec_PtrPushUnique( vSuper, pObj );
@@ -193,7 +193,7 @@ Vec_Ptr_t * Fra_CollectSuper( Aig_Obj_t * pObj, int fUseMuxes )
 {
     Vec_Ptr_t * vSuper;
     assert( !Aig_IsComplement(pObj) );
-    assert( !Aig_ObjIsPi(pObj) );
+    assert( !Aig_ObjIsCi(pObj) );
     vSuper = Vec_PtrAlloc( 4 );
     Fra_CollectSuper_rec( pObj, vSuper, 1, fUseMuxes );
     return vSuper;
diff --git a/src/proof/fra/fraCore.c b/src/proof/fra/fraCore.c
index 1969b36d..2148b467 100644
--- a/src/proof/fra/fraCore.c
+++ b/src/proof/fra/fraCore.c
@@ -81,7 +81,7 @@ int Fra_FraigMiterStatus( Aig_Man_t * p )
             continue;
         }
         // check if the output is a primary input
-        if ( Aig_ObjIsPi(Aig_Regular(pChild)) && Aig_ObjPioNum(Aig_Regular(pChild)) < p->nTruePis )
+        if ( Aig_ObjIsCi(Aig_Regular(pChild)) && Aig_ObjPioNum(Aig_Regular(pChild)) < p->nTruePis )
         {
             CountNonConst0++;
             continue;
@@ -97,7 +97,7 @@ int Fra_FraigMiterStatus( Aig_Man_t * p )
 /*
     if ( p->pParams->fVerbose )
     {
-        printf( "Miter has %d outputs. ", Aig_ManPoNum(p->pManAig) );
+        printf( "Miter has %d outputs. ", Aig_ManCoNum(p->pManAig) );
         printf( "Const0 = %d.  ", CountConst0 );
         printf( "NonConst0 = %d.  ", CountNonConst0 );
         printf( "Undecided = %d.  ", CountUndecided );
@@ -187,7 +187,7 @@ void Fra_FraigVerifyCounterEx( Fra_Man_t * p, Vec_Int_t * vCex )
 {
     Aig_Obj_t * pObj, ** ppClass;
     int i, c;
-    assert( Aig_ManPiNum(p->pManAig) == Vec_IntSize(vCex) );
+    assert( Aig_ManCiNum(p->pManAig) == Vec_IntSize(vCex) );
     // make sure the input pattern is not used
     Aig_ManForEachObj( p->pManAig, pObj, i )
         assert( !pObj->fMarkB );
diff --git a/src/proof/fra/fraHot.c b/src/proof/fra/fraHot.c
index 03dd468a..338b5717 100644
--- a/src/proof/fra/fraHot.c
+++ b/src/proof/fra/fraHot.c
@@ -137,7 +137,7 @@ Vec_Int_t * Fra_OneHotCompute( Fra_Man_t * p, Fra_Sml_t * pSim )
     Vec_Int_t * vOneHots;
     Aig_Obj_t * pObj1, * pObj2;
     int i, k;
-    int nTruePis = Aig_ManPiNum(pSim->pAig) - Aig_ManRegNum(pSim->pAig);
+    int nTruePis = Aig_ManCiNum(pSim->pAig) - Aig_ManRegNum(pSim->pAig);
     assert( pSim->pAig == p->pManAig );
     vOneHots = Vec_IntAlloc( 100 );
     Aig_ManForEachLoSeq( pSim->pAig, pObj1, i )
@@ -146,8 +146,8 @@ Vec_Int_t * Fra_OneHotCompute( Fra_Man_t * p, Fra_Sml_t * pSim )
             continue;
         assert( i-nTruePis >= 0 );
 //        Aig_ManForEachLoSeq( pSim->pAig, pObj2, k )
-//        Vec_PtrForEachEntryStart( Aig_Obj_t *, pSim->pAig->vPis, pObj2, k, Aig_ManPiNum(p)-Aig_ManRegNum(p) )
-        Vec_PtrForEachEntryStart( Aig_Obj_t *, pSim->pAig->vPis, pObj2, k, i+1 )
+//        Vec_PtrForEachEntryStart( Aig_Obj_t *, pSim->pAig->vPis, pObj2, k, Aig_ManCiNum(p)-Aig_ManRegNum(p) )
+        Vec_PtrForEachEntryStart( Aig_Obj_t *, pSim->pAig->vCis, pObj2, k, i+1 )
         {
             if ( fSkipConstEqu && Fra_OneHotNodeIsConst(pSim, pObj2) )
                 continue;
@@ -192,7 +192,7 @@ void Fra_OneHotAssume( Fra_Man_t * p, Vec_Int_t * vOneHots )
 {
     Aig_Obj_t * pObj1, * pObj2;
     int i, Out1, Out2, pLits[2];
-    int nPiNum = Aig_ManPiNum(p->pManFraig) - Aig_ManRegNum(p->pManFraig);
+    int nPiNum = Aig_ManCiNum(p->pManFraig) - Aig_ManRegNum(p->pManFraig);
     assert( p->pPars->nFramesK == 1 ); // add to only one frame
     for ( i = 0; i < Vec_IntSize(vOneHots); i += 2 )
     {
@@ -200,8 +200,8 @@ void Fra_OneHotAssume( Fra_Man_t * p, Vec_Int_t * vOneHots )
         Out2 = Vec_IntEntry( vOneHots, i+1 );
         if ( Out1 == 0 && Out2 == 0 )
             continue;
-        pObj1 = Aig_ManPi( p->pManFraig, nPiNum + Fra_LitReg(Out1) );
-        pObj2 = Aig_ManPi( p->pManFraig, nPiNum + Fra_LitReg(Out2) );
+        pObj1 = Aig_ManCi( p->pManFraig, nPiNum + Fra_LitReg(Out1) );
+        pObj2 = Aig_ManCi( p->pManFraig, nPiNum + Fra_LitReg(Out2) );
         pLits[0] = toLitCond( Fra_ObjSatNum(pObj1), Fra_LitSign(Out1) );
         pLits[1] = toLitCond( Fra_ObjSatNum(pObj2), Fra_LitSign(Out2) );
         // add constraint to solver
@@ -230,15 +230,15 @@ void Fra_OneHotCheck( Fra_Man_t * p, Vec_Int_t * vOneHots )
 {
     Aig_Obj_t * pObj1, * pObj2;
     int RetValue, i, Out1, Out2;
-    int nTruePos = Aig_ManPoNum(p->pManFraig) - Aig_ManRegNum(p->pManFraig);
+    int nTruePos = Aig_ManCoNum(p->pManFraig) - Aig_ManRegNum(p->pManFraig);
     for ( i = 0; i < Vec_IntSize(vOneHots); i += 2 )
     {
         Out1 = Vec_IntEntry( vOneHots, i );
         Out2 = Vec_IntEntry( vOneHots, i+1 );
         if ( Out1 == 0 && Out2 == 0 )
             continue;
-        pObj1 = Aig_ManPo( p->pManFraig, nTruePos + Fra_LitReg(Out1) );
-        pObj2 = Aig_ManPo( p->pManFraig, nTruePos + Fra_LitReg(Out2) );
+        pObj1 = Aig_ManCo( p->pManFraig, nTruePos + Fra_LitReg(Out1) );
+        pObj2 = Aig_ManCo( p->pManFraig, nTruePos + Fra_LitReg(Out2) );
         RetValue = Fra_NodesAreClause( p, pObj1, pObj2, Fra_LitSign(Out1), Fra_LitSign(Out2) );
         if ( RetValue != 1 )
         {
@@ -267,7 +267,7 @@ int Fra_OneHotRefineUsingCex( Fra_Man_t * p, Vec_Int_t * vOneHots )
 {
     Aig_Obj_t * pObj1, * pObj2;
     int i, Out1, Out2, RetValue = 0;
-    int nPiNum = Aig_ManPiNum(p->pManAig) - Aig_ManRegNum(p->pManAig);
+    int nPiNum = Aig_ManCiNum(p->pManAig) - Aig_ManRegNum(p->pManAig);
     assert( p->pSml->pAig == p->pManAig );
     for ( i = 0; i < Vec_IntSize(vOneHots); i += 2 )
     {
@@ -276,8 +276,8 @@ int Fra_OneHotRefineUsingCex( Fra_Man_t * p, Vec_Int_t * vOneHots )
         if ( Out1 == 0 && Out2 == 0 )
             continue;
         // get the corresponding nodes
-        pObj1 = Aig_ManPi( p->pManAig, nPiNum + Fra_LitReg(Out1) );
-        pObj2 = Aig_ManPi( p->pManAig, nPiNum + Fra_LitReg(Out2) );
+        pObj1 = Aig_ManCi( p->pManAig, nPiNum + Fra_LitReg(Out1) );
+        pObj2 = Aig_ManCi( p->pManAig, nPiNum + Fra_LitReg(Out2) );
         // check if implication holds using this simulation info
         if ( !Fra_OneHotNodesAreClause( p->pSml, pObj1, pObj2, Fra_LitSign(Out1), Fra_LitSign(Out2) ) )
         {
@@ -405,22 +405,22 @@ Aig_Man_t * Fra_OneHotCreateExdc( Fra_Man_t * p, Vec_Int_t * vOneHots )
 //        Aig_ObjCreateCi(pNew);
     Aig_ManForEachCi( p->pManAig, pObj, i )
         Aig_ObjCreateCi(pNew);
-    nTruePis = Aig_ManPiNum(p->pManAig) - Aig_ManRegNum(p->pManAig);
+    nTruePis = Aig_ManCiNum(p->pManAig) - Aig_ManRegNum(p->pManAig);
     for ( i = 0; i < Vec_IntSize(vOneHots); i += 2 )
     {
         Out1 = Vec_IntEntry( vOneHots, i );
         Out2 = Vec_IntEntry( vOneHots, i+1 );
         if ( Out1 == 0 && Out2 == 0 )
             continue;
-        pObj1 = Aig_ManPi( pNew, nTruePis + Fra_LitReg(Out1) );
-        pObj2 = Aig_ManPi( pNew, nTruePis + Fra_LitReg(Out2) );
+        pObj1 = Aig_ManCi( pNew, nTruePis + Fra_LitReg(Out1) );
+        pObj2 = Aig_ManCi( pNew, nTruePis + Fra_LitReg(Out2) );
         pObj1 = Aig_NotCond( pObj1, Fra_LitSign(Out1) );
         pObj2 = Aig_NotCond( pObj2, Fra_LitSign(Out2) );
         pObj  = Aig_Or( pNew, pObj1, pObj2 );
         Aig_ObjCreateCo( pNew, pObj );
     }
     Aig_ManCleanup(pNew);
-//    printf( "Created AIG with %d nodes and %d outputs.\n", Aig_ManNodeNum(pNew), Aig_ManPoNum(pNew) );
+//    printf( "Created AIG with %d nodes and %d outputs.\n", Aig_ManNodeNum(pNew), Aig_ManCoNum(pNew) );
     return pNew;
 }
 
@@ -450,8 +450,8 @@ void Fra_OneHotAddKnownConstraint( Fra_Man_t * p, Vec_Ptr_t * vOnehots )
         Vec_IntForEachEntry( vGroup, Out1, i )
         Vec_IntForEachEntryStart( vGroup, Out2, j, i+1 )
         {
-            pObj1 = Aig_ManPi( p->pManFraig, Out1 );
-            pObj2 = Aig_ManPi( p->pManFraig, Out2 );
+            pObj1 = Aig_ManCi( p->pManFraig, Out1 );
+            pObj2 = Aig_ManCi( p->pManFraig, Out2 );
             pLits[0] = toLitCond( Fra_ObjSatNum(pObj1), 1 );
             pLits[1] = toLitCond( Fra_ObjSatNum(pObj2), 1 );
             // add constraint to solver
diff --git a/src/proof/fra/fraImp.c b/src/proof/fra/fraImp.c
index de24f179..f65aca5c 100644
--- a/src/proof/fra/fraImp.c
+++ b/src/proof/fra/fraImp.c
@@ -170,12 +170,12 @@ Vec_Ptr_t * Fra_SmlSortUsingOnes( Fra_Sml_t * p, int fLatchCorr )
         // skip non-PI and non-internal nodes
         if ( fLatchCorr )
         {
-            if ( !Aig_ObjIsPi(pObj) )
+            if ( !Aig_ObjIsCi(pObj) )
                 continue;
         }
         else
         {
-            if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
+            if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsCi(pObj) )
                 continue;
         }
         // skip nodes participating in the classes
@@ -203,12 +203,12 @@ Vec_Ptr_t * Fra_SmlSortUsingOnes( Fra_Sml_t * p, int fLatchCorr )
         // skip non-PI and non-internal nodes
         if ( fLatchCorr )
         {
-            if ( !Aig_ObjIsPi(pObj) )
+            if ( !Aig_ObjIsCi(pObj) )
                 continue;
         }
         else
         {
-            if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
+            if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsCi(pObj) )
                 continue;
         }
         // skip nodes participating in the classes
@@ -708,7 +708,7 @@ void Fra_ImpRecordInManager( Fra_Man_t * p, Aig_Man_t * pNew )
     if ( p->pCla->vImps == NULL || Vec_IntSize(p->pCla->vImps) == 0 )
         return;
     // go through the implication
-    nPosOld = Aig_ManPoNum(pNew);
+    nPosOld = Aig_ManCoNum(pNew);
     Vec_IntForEachEntry( p->pCla->vImps, Imp, i )
     {
         pLeft = Aig_ManObj( p->pManAig, Fra_ImpLeft(Imp) );
@@ -719,7 +719,7 @@ void Fra_ImpRecordInManager( Fra_Man_t * p, Aig_Man_t * pNew )
             Aig_NotCond((Aig_Obj_t *)pRight->pData, pRight->fPhase) ); 
         Aig_ObjCreateCo( pNew, pMiter );
     }
-    pNew->nAsserts = Aig_ManPoNum(pNew) - nPosOld;
+    pNew->nAsserts = Aig_ManCoNum(pNew) - nPosOld;
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/proof/fra/fraInd.c b/src/proof/fra/fraInd.c
index b8a1e6bf..29a76eea 100644
--- a/src/proof/fra/fraInd.c
+++ b/src/proof/fra/fraInd.c
@@ -61,16 +61,16 @@ void Fra_FraigInductionRewrite( Fra_Man_t * p )
     // transfer PI/register pointers
     assert( p->pManFraig->nRegs == pTemp->nRegs );
     assert( p->pManFraig->nAsserts == pTemp->nAsserts );
-    nTruePis = Aig_ManPiNum(p->pManAig) - Aig_ManRegNum(p->pManAig);
+    nTruePis = Aig_ManCiNum(p->pManAig) - Aig_ManRegNum(p->pManAig);
     memset( p->pMemFraig, 0, sizeof(Aig_Obj_t *) * p->nSizeAlloc * p->nFramesAll );
     Fra_ObjSetFraig( Aig_ManConst1(p->pManAig), p->pPars->nFramesK, Aig_ManConst1(pTemp) );
     Aig_ManForEachPiSeq( p->pManAig, pObj, i )
-        Fra_ObjSetFraig( pObj, p->pPars->nFramesK, Aig_ManPi(pTemp,nTruePis*p->pPars->nFramesK+i) );
+        Fra_ObjSetFraig( pObj, p->pPars->nFramesK, Aig_ManCi(pTemp,nTruePis*p->pPars->nFramesK+i) );
     k = 0;
-    assert( Aig_ManRegNum(p->pManAig) == Aig_ManPoNum(pTemp) - pTemp->nAsserts );
+    assert( Aig_ManRegNum(p->pManAig) == Aig_ManCoNum(pTemp) - pTemp->nAsserts );
     Aig_ManForEachLoSeq( p->pManAig, pObj, i )
     {
-        pObjPo = Aig_ManPo(pTemp, pTemp->nAsserts + k++);
+        pObjPo = Aig_ManCo(pTemp, pTemp->nAsserts + k++);
         Fra_ObjSetFraig( pObj, p->pPars->nFramesK, Aig_ObjChild0(pObjPo) );
     }
     // exchange
@@ -133,7 +133,7 @@ Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p )
     int i, k, f;
     assert( p->pManFraig == NULL );
     assert( Aig_ManRegNum(p->pManAig) > 0 );
-    assert( Aig_ManRegNum(p->pManAig) < Aig_ManPiNum(p->pManAig) );
+    assert( Aig_ManRegNum(p->pManAig) < Aig_ManCiNum(p->pManAig) );
 
     // start the fraig package
     pManFraig = Aig_ManStart( Aig_ManObjNumMax(p->pManAig) * p->nFramesAll );
@@ -170,7 +170,7 @@ Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p )
     }
 //    pManFraig->fAddStrash = 0;
     // mark the asserts
-    pManFraig->nAsserts = Aig_ManPoNum(pManFraig);
+    pManFraig->nAsserts = Aig_ManCoNum(pManFraig);
     // add the POs for the latch outputs of the last frame
     Aig_ManForEachLoSeq( p->pManAig, pObj, i )
         Aig_ObjCreateCo( pManFraig, Fra_ObjFraig(pObj,p->nFramesAll-1) );
@@ -291,7 +291,7 @@ Aig_Man_t * Fra_FraigInductionPart( Aig_Man_t * pAig, Fra_Ssw_t * pPars )
             pTemp = Aig_ManRegCreatePart( pAig, vPart, &nCountPis, &nCountRegs, NULL );
             Ioa_WriteAiger( pTemp, Buffer, 0, 0 );
             printf( "part%03d.aig : Reg = %4d. PI = %4d. (True = %4d. Regs = %4d.) And = %5d.\n", 
-                i, Vec_IntSize(vPart), Aig_ManPiNum(pTemp)-Vec_IntSize(vPart), nCountPis, nCountRegs, Aig_ManNodeNum(pTemp) );
+                i, Vec_IntSize(vPart), Aig_ManCiNum(pTemp)-Vec_IntSize(vPart), nCountPis, nCountRegs, Aig_ManNodeNum(pTemp) );
             Aig_ManStop( pTemp );
         }
     }
@@ -309,7 +309,7 @@ Aig_Man_t * Fra_FraigInductionPart( Aig_Man_t * pAig, Fra_Ssw_t * pPars )
         nClasses = Aig_TransferMappedClasses( pAig, pTemp, pMapBack );
         if ( fVerbose )
             printf( "%3d : Reg = %4d. PI = %4d. (True = %4d. Regs = %4d.) And = %5d. It = %3d. Cl = %5d.\n", 
-                i, Vec_IntSize(vPart), Aig_ManPiNum(pTemp)-Vec_IntSize(vPart), nCountPis, nCountRegs, Aig_ManNodeNum(pTemp), pPars->nIters, nClasses );
+                i, Vec_IntSize(vPart), Aig_ManCiNum(pTemp)-Vec_IntSize(vPart), nCountPis, nCountRegs, Aig_ManNodeNum(pTemp), pPars->nIters, nClasses );
         Aig_ManStop( pNew );
         Aig_ManStop( pTemp );
         ABC_FREE( pMapBack );
@@ -637,8 +637,8 @@ p->timeTotal = clock() - clk;
 finish:
     Fra_ManStop( p );
     // check the output
-//    if ( Aig_ManPoNum(pManAigNew) - Aig_ManRegNum(pManAigNew) == 1 )
-//        if ( Aig_ObjChild0( Aig_ManPo(pManAigNew,0) ) == Aig_ManConst0(pManAigNew) )
+//    if ( Aig_ManCoNum(pManAigNew) - Aig_ManRegNum(pManAigNew) == 1 )
+//        if ( Aig_ObjChild0( Aig_ManCo(pManAigNew,0) ) == Aig_ManConst0(pManAigNew) )
 //            printf( "Proved output constant 0.\n" );
     pParams->nIters = nIter;
     return pManAigNew;
diff --git a/src/proof/fra/fraIndVer.c b/src/proof/fra/fraIndVer.c
index 64437607..7c5e9e70 100644
--- a/src/proof/fra/fraIndVer.c
+++ b/src/proof/fra/fraIndVer.c
@@ -59,14 +59,14 @@ int Fra_InvariantVerify( Aig_Man_t * pAig, int nFrames, Vec_Int_t * vClauses, Ve
     }
 
     // derive CNF
-    pCnf = Cnf_DeriveSimple( pAig, Aig_ManPoNum(pAig) );
+    pCnf = Cnf_DeriveSimple( pAig, Aig_ManCoNum(pAig) );
 /*
     // add the property
     {
         Aig_Obj_t * pObj;
         int Lits[1];
 
-        pObj = Aig_ManPo( pAig, 0 );
+        pObj = Aig_ManCo( pAig, 0 );
         Lits[0] = toLitCond( pCnf->pVarNums[pObj->Id], 1 ); 
 
         Vec_IntPush( vLits, Lits[0] );
diff --git a/src/proof/fra/fraLcr.c b/src/proof/fra/fraLcr.c
index d24b37f6..8ea6d297 100644
--- a/src/proof/fra/fraLcr.c
+++ b/src/proof/fra/fraLcr.c
@@ -83,10 +83,10 @@ Fra_Lcr_t * Lcr_ManAlloc( Aig_Man_t * pAig )
     p = ABC_ALLOC( Fra_Lcr_t, 1 );
     memset( p, 0, sizeof(Fra_Lcr_t) );
     p->pAig = pAig;
-    p->pInToOutPart = ABC_ALLOC( int, Aig_ManPiNum(pAig) );
-    memset( p->pInToOutPart, 0, sizeof(int) * Aig_ManPiNum(pAig) );
-    p->pInToOutNum = ABC_ALLOC( int, Aig_ManPiNum(pAig) );
-    memset( p->pInToOutNum, 0, sizeof(int) * Aig_ManPiNum(pAig) );
+    p->pInToOutPart = ABC_ALLOC( int, Aig_ManCiNum(pAig) );
+    memset( p->pInToOutPart, 0, sizeof(int) * Aig_ManCiNum(pAig) );
+    p->pInToOutNum = ABC_ALLOC( int, Aig_ManCiNum(pAig) );
+    memset( p->pInToOutNum, 0, sizeof(int) * Aig_ManCiNum(pAig) );
     p->vFraigs = Vec_PtrAlloc( 1000 );
     return p;
 }
@@ -205,8 +205,8 @@ int Fra_LcrNodesAreEqual( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )
     Aig_Man_t * pFraig;
     Aig_Obj_t * pOut0, * pOut1;
     int nPart0, nPart1;
-    assert( Aig_ObjIsPi(pObj0) );
-    assert( Aig_ObjIsPi(pObj1) );
+    assert( Aig_ObjIsCi(pObj0) );
+    assert( Aig_ObjIsCi(pObj1) );
     // find the partition to which these nodes belong
     nPart0 = pLcr->pInToOutPart[(long)pObj0->pNext];
     nPart1 = pLcr->pInToOutPart[(long)pObj1->pNext];
@@ -220,8 +220,8 @@ int Fra_LcrNodesAreEqual( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )
     assert( nPart0 == nPart1 );
     pFraig = (Aig_Man_t *)Vec_PtrEntry( pLcr->vFraigs, nPart0 );
     // get the fraig outputs
-    pOut0 = Aig_ManPo( pFraig, pLcr->pInToOutNum[(long)pObj0->pNext] );
-    pOut1 = Aig_ManPo( pFraig, pLcr->pInToOutNum[(long)pObj1->pNext] );
+    pOut0 = Aig_ManCo( pFraig, pLcr->pInToOutNum[(long)pObj0->pNext] );
+    pOut1 = Aig_ManCo( pFraig, pLcr->pInToOutNum[(long)pObj1->pNext] );
     return Aig_ObjFanin0(pOut0) == Aig_ObjFanin0(pOut1);
 }
 
@@ -243,12 +243,12 @@ int Fra_LcrNodeIsConst( Aig_Obj_t * pObj )
     Aig_Man_t * pFraig;
     Aig_Obj_t * pOut;
     int nPart;
-    assert( Aig_ObjIsPi(pObj) );
+    assert( Aig_ObjIsCi(pObj) );
     // find the partition to which these nodes belong
     nPart = pLcr->pInToOutPart[(long)pObj->pNext];
     pFraig = (Aig_Man_t *)Vec_PtrEntry( pLcr->vFraigs, nPart );
     // get the fraig outputs
-    pOut = Aig_ManPo( pFraig, pLcr->pInToOutNum[(long)pObj->pNext] );
+    pOut = Aig_ManCo( pFraig, pLcr->pInToOutNum[(long)pObj->pNext] );
     return Aig_ObjFanin0(pOut) == Aig_ManConst1(pFraig);
 }
 
@@ -306,7 +306,7 @@ Aig_Man_t * Fra_LcrDeriveAigForPartitioning( Fra_Lcr_t * pLcr )
         pObj->pNext = (Aig_Obj_t *)(long)i;
     }
     // compute the LO/LI offset
-    Offset = Aig_ManPoNum(pLcr->pAig) - Aig_ManPiNum(pLcr->pAig);
+    Offset = Aig_ManCoNum(pLcr->pAig) - Aig_ManCiNum(pLcr->pAig);
     // create the PIs
     Aig_ManCleanData( pLcr->pAig );
     pNew = Aig_ManStartFrom( pLcr->pAig );
@@ -316,8 +316,8 @@ Aig_Man_t * Fra_LcrDeriveAigForPartitioning( Fra_Lcr_t * pLcr )
         pMiter = Aig_ManConst0(pNew);
         for ( c = 0; ppClass[c]; c++ )
         {
-            assert( Aig_ObjIsPi(ppClass[c]) );
-            pObjPo  = Aig_ManPo( pLcr->pAig, Offset+(long)ppClass[c]->pNext );
+            assert( Aig_ObjIsCi(ppClass[c]) );
+            pObjPo  = Aig_ManCo( pLcr->pAig, Offset+(long)ppClass[c]->pNext );
             pObjNew = Fra_LcrManDup_rec( pNew, pLcr->pAig, Aig_ObjFanin0(pObjPo) );
             pMiter  = Aig_Exor( pNew, pMiter, pObjNew );
         }
@@ -326,8 +326,8 @@ Aig_Man_t * Fra_LcrDeriveAigForPartitioning( Fra_Lcr_t * pLcr )
     // go over the constant candidates
     Vec_PtrForEachEntry( Aig_Obj_t *, pLcr->pCla->vClasses1, pObj, i )
     {
-        assert( Aig_ObjIsPi(pObj) );
-        pObjPo = Aig_ManPo( pLcr->pAig, Offset+(long)pObj->pNext );
+        assert( Aig_ObjIsCi(pObj) );
+        pObjPo = Aig_ManCo( pLcr->pAig, Offset+(long)pObj->pNext );
         pMiter = Fra_LcrManDup_rec( pNew, pLcr->pAig, Aig_ObjFanin0(pObjPo) );
         Aig_ObjCreateCo( pNew, pMiter );
     }
@@ -351,7 +351,7 @@ void Fra_LcrRemapPartitions( Vec_Ptr_t * vParts, Fra_Cla_t * pCla, int * pInToOu
     Aig_Obj_t ** ppClass, * pObjPi;
     int Out, Offset, i, k, c;
     // compute the LO/LI offset
-    Offset = Aig_ManPoNum(pCla->pAig) - Aig_ManPiNum(pCla->pAig);
+    Offset = Aig_ManCoNum(pCla->pAig) - Aig_ManCiNum(pCla->pAig);
     Vec_PtrForEachEntry( Vec_Int_t *, vParts, vOne, i )
     {
         vOneNew = Vec_IntAlloc( Vec_IntSize(vOne) );
@@ -398,7 +398,7 @@ Aig_Obj_t * Fra_LcrCreatePart_rec( Fra_Cla_t * pCla, Aig_Man_t * pNew, Aig_Man_t
     if ( Aig_ObjIsTravIdCurrent(p, pObj) )
         return (Aig_Obj_t *)pObj->pData;
     Aig_ObjSetTravIdCurrent(p, pObj);
-    if ( Aig_ObjIsPi(pObj) )
+    if ( Aig_ObjIsCi(pObj) )
     {
 //        Aig_Obj_t * pRepr = Fra_ClassObjRepr(pObj);
         Aig_Obj_t * pRepr = pCla->pMemRepr[pObj->Id];
@@ -439,7 +439,7 @@ Aig_Man_t * Fra_LcrCreatePart( Fra_Lcr_t * p, Vec_Int_t * vPart )
     Aig_ManConst1(p->pAig)->pData = Aig_ManConst1(pNew);
     Vec_IntForEachEntry( vPart, Out, i )
     {
-        pObj = Aig_ManPo( p->pAig, Out );
+        pObj = Aig_ManCo( p->pAig, Out );
         if ( pObj->fMarkA )
         {
             pObjNew = Fra_LcrCreatePart_rec( p->pCla, pNew, p->pAig, Aig_ObjFanin0(pObj) );
@@ -468,18 +468,18 @@ void Fra_ClassNodesMark( Fra_Lcr_t * p )
     Aig_Obj_t * pObj, ** ppClass;
     int i, c, Offset;
     // compute the LO/LI offset
-    Offset = Aig_ManPoNum(p->pCla->pAig) - Aig_ManPiNum(p->pCla->pAig);
+    Offset = Aig_ManCoNum(p->pCla->pAig) - Aig_ManCiNum(p->pCla->pAig);
     // mark the nodes remaining in the classes
     Vec_PtrForEachEntry( Aig_Obj_t *, p->pCla->vClasses1, pObj, i )
     {
-        pObj = Aig_ManPo( p->pCla->pAig, Offset+(long)pObj->pNext );
+        pObj = Aig_ManCo( p->pCla->pAig, Offset+(long)pObj->pNext );
         pObj->fMarkA = 1;
     }
     Vec_PtrForEachEntry( Aig_Obj_t **, p->pCla->vClasses, ppClass, i )
     {
         for ( c = 0; ppClass[c]; c++ )
         {
-            pObj = Aig_ManPo( p->pCla->pAig, Offset+(long)ppClass[c]->pNext );
+            pObj = Aig_ManCo( p->pCla->pAig, Offset+(long)ppClass[c]->pNext );
             pObj->fMarkA = 1;
         }
     }
@@ -501,18 +501,18 @@ void Fra_ClassNodesUnmark( Fra_Lcr_t * p )
     Aig_Obj_t * pObj, ** ppClass;
     int i, c, Offset;
     // compute the LO/LI offset
-    Offset = Aig_ManPoNum(p->pCla->pAig) - Aig_ManPiNum(p->pCla->pAig);
+    Offset = Aig_ManCoNum(p->pCla->pAig) - Aig_ManCiNum(p->pCla->pAig);
     // mark the nodes remaining in the classes
     Vec_PtrForEachEntry( Aig_Obj_t *, p->pCla->vClasses1, pObj, i )
     {
-        pObj = Aig_ManPo( p->pCla->pAig, Offset+(long)pObj->pNext );
+        pObj = Aig_ManCo( p->pCla->pAig, Offset+(long)pObj->pNext );
         pObj->fMarkA = 0;
     }
     Vec_PtrForEachEntry( Aig_Obj_t **, p->pCla->vClasses, ppClass, i )
     {
         for ( c = 0; ppClass[c]; c++ )
         {
-            pObj = Aig_ManPo( p->pCla->pAig, Offset+(long)ppClass[c]->pNext );
+            pObj = Aig_ManCo( p->pCla->pAig, Offset+(long)ppClass[c]->pNext );
             pObj->fMarkA = 0;
         }
     }
diff --git a/src/proof/fra/fraMan.c b/src/proof/fra/fraMan.c
index 67832f83..5ffbc778 100644
--- a/src/proof/fra/fraMan.c
+++ b/src/proof/fra/fraMan.c
@@ -114,7 +114,7 @@ Fra_Man_t * Fra_ManStart( Aig_Man_t * pManAig, Fra_Par_t * pPars )
     p->nSizeAlloc = Aig_ManObjNumMax( pManAig );
     p->nFramesAll = pPars->nFramesK + 1;
     // allocate storage for sim pattern
-    p->nPatWords  = Abc_BitWordNum( (Aig_ManPiNum(pManAig) - Aig_ManRegNum(pManAig)) * p->nFramesAll + Aig_ManRegNum(pManAig) );
+    p->nPatWords  = Abc_BitWordNum( (Aig_ManCiNum(pManAig) - Aig_ManRegNum(pManAig)) * p->nFramesAll + Aig_ManRegNum(pManAig) );
     p->pPatWords  = ABC_ALLOC( unsigned, p->nPatWords ); 
     p->vPiVars    = Vec_PtrAlloc( 100 );
     // equivalence classes
diff --git a/src/proof/fra/fraPart.c b/src/proof/fra/fraPart.c
index 6594ac0b..e3bb2850 100644
--- a/src/proof/fra/fraPart.c
+++ b/src/proof/fra/fraPart.c
@@ -74,7 +74,7 @@ ABC_PRT( "Supports", clock() - clk );
 
     // create reverse supports
 clk = clock();
-    vSuppsIn = Vec_VecStart( Aig_ManPiNum(p) );
+    vSuppsIn = Vec_VecStart( Aig_ManCiNum(p) );
     Aig_ManForEachCo( p, pObj, i )
     {
         vSup = Vec_VecEntryInt( vSupps, i );
@@ -86,10 +86,10 @@ ABC_PRT( "Inverse ", clock() - clk );
 clk = clock();
     // compute extended supports
     Largest = 0;
-    vSuppsNew = Vec_PtrAlloc( Aig_ManPoNum(p) );
-    vOverNew  = Vec_IntAlloc( Aig_ManPoNum(p) );
-    vQuantNew = Vec_IntAlloc( Aig_ManPoNum(p) );
-//    pProgress = Bar_ProgressStart( stdout, Aig_ManPoNum(p) );
+    vSuppsNew = Vec_PtrAlloc( Aig_ManCoNum(p) );
+    vOverNew  = Vec_IntAlloc( Aig_ManCoNum(p) );
+    vQuantNew = Vec_IntAlloc( Aig_ManCoNum(p) );
+//    pProgress = Bar_ProgressStart( stdout, Aig_ManCoNum(p) );
     Aig_ManForEachCo( p, pObj, i )
     {
 //        Bar_ProgressUpdate( pProgress, i, NULL );
@@ -160,9 +160,9 @@ ABC_PRT( "Scanning", clock() - clk );
 
     // print cumulative statistics
     printf( "PIs = %6d. POs = %6d. Lim = %3d.   AveS = %3d. SN = %3d. R = %4.2f Max = %5d.\n",
-        Aig_ManPiNum(p), Aig_ManPoNum(p), nComLim,
-        nTotalSupp/Aig_ManPoNum(p), nTotalSupp2/Aig_ManPoNum(p),
-        Ratio/Aig_ManPoNum(p), Largest );
+        Aig_ManCiNum(p), Aig_ManCoNum(p), nComLim,
+        nTotalSupp/Aig_ManCoNum(p), nTotalSupp2/Aig_ManCoNum(p),
+        Ratio/Aig_ManCoNum(p), Largest );
 
     Vec_VecFree( vSupps );
     Vec_VecFree( vSuppsIn );
@@ -208,7 +208,7 @@ ABC_PRT( "Supports", clock() - clk );
 
     // create reverse supports
 clk = clock();
-    vSuppsIn = Vec_VecStart( Aig_ManPiNum(p) );
+    vSuppsIn = Vec_VecStart( Aig_ManCiNum(p) );
     Aig_ManForEachCo( p, pObj, i )
     {
         if ( i == p->nAsserts )
@@ -221,13 +221,13 @@ ABC_PRT( "Inverse ", clock() - clk );
 
     // create affective supports
 clk = clock();
-    pSupp = ABC_ALLOC( char, Aig_ManPiNum(p) );
+    pSupp = ABC_ALLOC( char, Aig_ManCiNum(p) );
     Aig_ManForEachCo( p, pObj, i )
     {
         if ( i % 50 != 0 )
             continue;
         vSup = Vec_VecEntryInt( vSupps, i );
-        memset( pSupp, 0, sizeof(char) * Aig_ManPiNum(p) );
+        memset( pSupp, 0, sizeof(char) * Aig_ManCiNum(p) );
         // go through each input of this output
         Vec_IntForEachEntry( vSup, Entry, k )
         {
@@ -246,7 +246,7 @@ clk = clock();
         }
         // count the entries
         Counter = 0;
-        for ( m = 0; m < Aig_ManPiNum(p); m++ )
+        for ( m = 0; m < Aig_ManCiNum(p); m++ )
             Counter += pSupp[m];
         printf( "%d(%d) ", Vec_IntSize(vSup), Counter );
     }
diff --git a/src/proof/fra/fraSat.c b/src/proof/fra/fraSat.c
index 38702d5e..2702113c 100644
--- a/src/proof/fra/fraSat.c
+++ b/src/proof/fra/fraSat.c
@@ -507,7 +507,7 @@ int Fra_SetActivityFactors_rec( Fra_Man_t * p, Aig_Obj_t * pObj, int LevelMin, i
         return 0;
     Aig_ObjSetTravIdCurrent(p->pManFraig, pObj);
     // add the PI to the list
-    if ( pObj->Level <= (unsigned)LevelMin || Aig_ObjIsPi(pObj) )
+    if ( pObj->Level <= (unsigned)LevelMin || Aig_ObjIsCi(pObj) )
         return 0;
     // set the factor of this variable
     // (LevelMax-LevelMin) / (pObj->Level-LevelMin) = p->pPars->dActConeBumpMax / ThisBump
diff --git a/src/proof/fra/fraSec.c b/src/proof/fra/fraSec.c
index 8067b8c2..cde56809 100644
--- a/src/proof/fra/fraSec.c
+++ b/src/proof/fra/fraSec.c
@@ -142,8 +142,8 @@ clk = clock();
     if ( pParSec->fPhaseAbstract )
     {
         extern Aig_Man_t * Saig_ManPhaseAbstractAuto( Aig_Man_t * p, int fVerbose );
-        pNew->nTruePis = Aig_ManPiNum(pNew) - Aig_ManRegNum(pNew); 
-        pNew->nTruePos = Aig_ManPoNum(pNew) - Aig_ManRegNum(pNew); 
+        pNew->nTruePis = Aig_ManCiNum(pNew) - Aig_ManRegNum(pNew); 
+        pNew->nTruePos = Aig_ManCoNum(pNew) - Aig_ManRegNum(pNew); 
         pNew = Saig_ManPhaseAbstractAuto( pTemp = pNew, 0 );
         Aig_ManStop( pTemp );
         if ( pParSec->fVerbose )
@@ -301,8 +301,8 @@ ABC_PRT( "Time", clock() - clk );
     {
 //    extern Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int nMaxIters, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose );
 clk = clock();
-    pNew->nTruePis = Aig_ManPiNum(pNew) - Aig_ManRegNum(pNew); 
-    pNew->nTruePos = Aig_ManPoNum(pNew) - Aig_ManRegNum(pNew); 
+    pNew->nTruePis = Aig_ManCiNum(pNew) - Aig_ManRegNum(pNew); 
+    pNew->nTruePos = Aig_ManCoNum(pNew) - Aig_ManRegNum(pNew); 
 //        pNew = Rtm_ManRetime( pTemp = pNew, 1, 1000, 0 );
     pNew = Saig_ManRetimeMinArea( pTemp = pNew, 1000, 0, 0, 1, 0 );
     Aig_ManStop( pTemp );
@@ -391,8 +391,8 @@ ABC_PRT( "Time", clock() - clk );
         {
 //        extern Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int nMaxIters, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose );
 clk = clock();
-        pNew->nTruePis = Aig_ManPiNum(pNew) - Aig_ManRegNum(pNew); 
-        pNew->nTruePos = Aig_ManPoNum(pNew) - Aig_ManRegNum(pNew); 
+        pNew->nTruePis = Aig_ManCiNum(pNew) - Aig_ManRegNum(pNew); 
+        pNew->nTruePos = Aig_ManCoNum(pNew) - Aig_ManRegNum(pNew); 
 //        pNew = Rtm_ManRetime( pTemp = pNew, 1, 1000, 0 );
         pNew = Saig_ManRetimeMinArea( pTemp = pNew, 1000, 0, 0, 1, 0 );
         Aig_ManStop( pTemp );
@@ -580,8 +580,8 @@ ABC_PRT( "Time", clock() - clk );
         pPars->fReorderImage = 1;
         pPars->fVerbose      = 0;
         pPars->fSilent       = pParSec->fSilent;
-        pNew->nTruePis = Aig_ManPiNum(pNew) - Aig_ManRegNum(pNew); 
-        pNew->nTruePos = Aig_ManPoNum(pNew) - Aig_ManRegNum(pNew); 
+        pNew->nTruePis = Aig_ManCiNum(pNew) - Aig_ManRegNum(pNew); 
+        pNew->nTruePos = Aig_ManCoNum(pNew) - Aig_ManRegNum(pNew); 
         RetValue = Aig_ManVerifyUsingBdds( pNew, pPars );
     }
 
diff --git a/src/proof/fra/fraSim.c b/src/proof/fra/fraSim.c
index e54846bc..66579be3 100644
--- a/src/proof/fra/fraSim.c
+++ b/src/proof/fra/fraSim.c
@@ -221,7 +221,7 @@ void Fra_SmlSavePattern1( Fra_Man_t * p, int fInit )
     if ( !fInit )
         return;
     // clear the state bits to correspond to all-0 initial state
-    nTruePis = Aig_ManPiNum(p->pManAig) - Aig_ManRegNum(p->pManAig);
+    nTruePis = Aig_ManCiNum(p->pManAig) - Aig_ManRegNum(p->pManAig);
     k = 0;
     Aig_ManForEachLoSeq( p->pManAig, pObj, i )
         Abc_InfoXorBit( p->pPatWords, nTruePis * p->nFramesAll + k++ );
@@ -251,9 +251,9 @@ void Fra_SmlSavePattern( Fra_Man_t * p )
     if ( p->vCex )
     {
         Vec_IntClear( p->vCex );
-        for ( i = 0; i < Aig_ManPiNum(p->pManAig) - Aig_ManRegNum(p->pManAig); i++ )
+        for ( i = 0; i < Aig_ManCiNum(p->pManAig) - Aig_ManRegNum(p->pManAig); i++ )
             Vec_IntPush( p->vCex, Abc_InfoHasBit( p->pPatWords, i ) );
-        for ( i = Aig_ManPiNum(p->pManFraig) - Aig_ManRegNum(p->pManFraig); i < Aig_ManPiNum(p->pManFraig); i++ )
+        for ( i = Aig_ManCiNum(p->pManFraig) - Aig_ManRegNum(p->pManFraig); i < Aig_ManCiNum(p->pManFraig); i++ )
             Vec_IntPush( p->vCex, Abc_InfoHasBit( p->pPatWords, i ) );
     }
 
@@ -298,13 +298,13 @@ void Fra_SmlCheckOutputSavePattern( Fra_Man_t * p, Aig_Obj_t * pObjPo )
     // determine the best pattern
     BestPat = i * 32 + k;
     // fill in the counter-example data
-    pModel = ABC_ALLOC( int, Aig_ManPiNum(p->pManFraig)+1 );
+    pModel = ABC_ALLOC( int, Aig_ManCiNum(p->pManFraig)+1 );
     Aig_ManForEachCi( p->pManAig, pObjPi, i )
     {
         pModel[i] = Abc_InfoHasBit(Fra_ObjSim(p->pSml, pObjPi->Id), BestPat);
 //        printf( "%d", pModel[i] );
     }
-    pModel[Aig_ManPiNum(p->pManAig)] = pObjPo->Id;
+    pModel[Aig_ManCiNum(p->pManAig)] = pObjPo->Id;
 //    printf( "\n" );
     // set the model
     assert( p->pManFraig->pData == NULL );
@@ -328,7 +328,7 @@ int Fra_SmlCheckOutput( Fra_Man_t * p )
     Aig_Obj_t * pObj;
     int i;
     // make sure the reference simulation pattern does not detect the bug
-    pObj = Aig_ManPo( p->pManAig, 0 );
+    pObj = Aig_ManCo( p->pManAig, 0 );
     assert( Aig_ObjFanin0(pObj)->fPhase == (unsigned)Aig_ObjFaninC0(pObj) ); 
     Aig_ManForEachCo( p->pManAig, pObj, i )
     {
@@ -359,7 +359,7 @@ void Fra_SmlAssignRandom( Fra_Sml_t * p, Aig_Obj_t * pObj )
 {
     unsigned * pSims;
     int i;
-    assert( Aig_ObjIsPi(pObj) );
+    assert( Aig_ObjIsCi(pObj) );
     pSims = Fra_ObjSim( p, pObj->Id );
     for ( i = 0; i < p->nWordsTotal; i++ )
         pSims[i] = Fra_ObjRandomSim();
@@ -380,7 +380,7 @@ void Fra_SmlAssignConst( Fra_Sml_t * p, Aig_Obj_t * pObj, int fConst1, int iFram
 {
     unsigned * pSims;
     int i;
-    assert( Aig_ObjIsPi(pObj) );
+    assert( Aig_ObjIsCi(pObj) );
     pSims = Fra_ObjSim( p, pObj->Id ) + p->nWordsFrame * iFrame;
     for ( i = 0; i < p->nWordsFrame; i++ )
         pSims[i] = fConst1? ~(unsigned)0 : 0;
@@ -404,7 +404,7 @@ void Fra_SmlInitialize( Fra_Sml_t * p, int fInit )
     if ( fInit )
     {
         assert( Aig_ManRegNum(p->pAig) > 0 );
-        assert( Aig_ManRegNum(p->pAig) < Aig_ManPiNum(p->pAig) );
+        assert( Aig_ManRegNum(p->pAig) < Aig_ManCiNum(p->pAig) );
         // assign random info for primary inputs
         Aig_ManForEachPiSeq( p->pAig, pObj, i )
             Fra_SmlAssignRandom( p, pObj );
@@ -441,16 +441,16 @@ void Fra_SmlAssignDist1( Fra_Sml_t * p, unsigned * pPat )
         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 );
+        Limit = Abc_MinInt( Aig_ManCiNum(p->pAig), p->nWordsTotal * 32 - 1 );
         for ( i = 0; i < Limit; i++ )
-            Abc_InfoXorBit( Fra_ObjSim( p, Aig_ManPi(p->pAig,i)->Id ), i+1 );
+            Abc_InfoXorBit( Fra_ObjSim( p, Aig_ManCi(p->pAig,i)->Id ), i+1 );
     }
     else
     {
         int fUseDist1 = 0;
 
         // copy the PI info for each frame
-        nTruePis = Aig_ManPiNum(p->pAig) - Aig_ManRegNum(p->pAig);
+        nTruePis = Aig_ManCiNum(p->pAig) - Aig_ManRegNum(p->pAig);
         for ( f = 0; f < p->nFrames; f++ )
             Aig_ManForEachPiSeq( p->pAig, pObj, i )
                 Fra_SmlAssignConst( p, pObj, Abc_InfoHasBit(pPat, nTruePis * f + i), f );
@@ -458,14 +458,14 @@ void Fra_SmlAssignDist1( Fra_Sml_t * p, unsigned * pPat )
         k = 0;
         Aig_ManForEachLoSeq( p->pAig, pObj, i )
             Fra_SmlAssignConst( p, pObj, Abc_InfoHasBit(pPat, nTruePis * p->nFrames + k++), 0 );
-//        assert( p->pManFraig == NULL || nTruePis * p->nFrames + k == Aig_ManPiNum(p->pManFraig) );
+//        assert( p->pManFraig == NULL || nTruePis * p->nFrames + k == Aig_ManCiNum(p->pManFraig) );
 
         // flip one bit of the last frame
         if ( fUseDist1 ) //&& p->nFrames == 2 )
         {
             Limit = Abc_MinInt( nTruePis, p->nWordsFrame * 32 - 1 );
             for ( i = 0; i < Limit; i++ )
-                Abc_InfoXorBit( Fra_ObjSim( p, Aig_ManPi(p->pAig, i)->Id ) + p->nWordsFrame*(p->nFrames-1), i+1 );
+                Abc_InfoXorBit( Fra_ObjSim( p, Aig_ManCi(p->pAig, i)->Id ) + p->nWordsFrame*(p->nFrames-1), i+1 );
         }
     }
 }
@@ -581,7 +581,7 @@ void Fra_SmlNodeCopyFanin( Fra_Sml_t * p, Aig_Obj_t * pObj, int iFrame )
     unsigned * pSims, * pSims0;
     int fCompl, fCompl0, i;
     assert( !Aig_IsComplement(pObj) );
-    assert( Aig_ObjIsPo(pObj) );
+    assert( Aig_ObjIsCo(pObj) );
     assert( iFrame == 0 || p->nWordsFrame < p->nWordsTotal );
     // get hold of the simulation information
     pSims  = Fra_ObjSim(p, pObj->Id) + p->nWordsFrame * iFrame;
@@ -615,8 +615,8 @@ void Fra_SmlNodeTransferNext( Fra_Sml_t * p, Aig_Obj_t * pOut, Aig_Obj_t * pIn,
     int i;
     assert( !Aig_IsComplement(pOut) );
     assert( !Aig_IsComplement(pIn) );
-    assert( Aig_ObjIsPo(pOut) );
-    assert( Aig_ObjIsPi(pIn) );
+    assert( Aig_ObjIsCo(pOut) );
+    assert( Aig_ObjIsCi(pIn) );
     assert( iFrame == 0 || p->nWordsFrame < p->nWordsTotal );
     // get hold of the simulation information
     pSims0 = Fra_ObjSim(p, pOut->Id) + p->nWordsFrame * iFrame;
@@ -918,12 +918,12 @@ Abc_Cex_t * Fra_SmlGetCounterExample( Fra_Sml_t * p )
             }
         break;
     }
-    assert( iPo < Aig_ManPoNum(p->pAig)-Aig_ManRegNum(p->pAig) );
+    assert( iPo < Aig_ManCoNum(p->pAig)-Aig_ManRegNum(p->pAig) );
     assert( iFrame < p->nFrames );
     assert( iBit < 32 * p->nWordsFrame );
 
     // allocate the counter example
-    pCex = Abc_CexAlloc( Aig_ManRegNum(p->pAig), Aig_ManPiNum(p->pAig) - Aig_ManRegNum(p->pAig), iFrame + 1 );
+    pCex = Abc_CexAlloc( Aig_ManRegNum(p->pAig), Aig_ManCiNum(p->pAig) - Aig_ManRegNum(p->pAig), iFrame + 1 );
     pCex->iPo    = iPo;
     pCex->iFrame = iFrame;
 
@@ -972,16 +972,16 @@ Abc_Cex_t * Fra_SmlCopyCounterExample( Aig_Man_t * pAig, Aig_Man_t * pFrames, in
     // get the number of frames
     assert( Aig_ManRegNum(pAig) > 0 );
     assert( Aig_ManRegNum(pFrames) == 0 );
-    nTruePis = Aig_ManPiNum(pAig)-Aig_ManRegNum(pAig);
-    nTruePos = Aig_ManPoNum(pAig)-Aig_ManRegNum(pAig);
-    nFrames = Aig_ManPiNum(pFrames) / nTruePis;
-    assert( nTruePis * nFrames == Aig_ManPiNum(pFrames) );
-    assert( nTruePos * nFrames == Aig_ManPoNum(pFrames) );
+    nTruePis = Aig_ManCiNum(pAig)-Aig_ManRegNum(pAig);
+    nTruePos = Aig_ManCoNum(pAig)-Aig_ManRegNum(pAig);
+    nFrames = Aig_ManCiNum(pFrames) / nTruePis;
+    assert( nTruePis * nFrames == Aig_ManCiNum(pFrames) );
+    assert( nTruePos * nFrames == Aig_ManCoNum(pFrames) );
     // find the PO that failed
     iPo = -1;
     iFrame = -1;
     Aig_ManForEachCo( pFrames, pObj, i )
-        if ( pObj->Id == pModel[Aig_ManPiNum(pFrames)] )
+        if ( pObj->Id == pModel[Aig_ManCiNum(pFrames)] )
         {
             iPo = i % nTruePos;
             iFrame = i / nTruePos;
@@ -994,7 +994,7 @@ Abc_Cex_t * Fra_SmlCopyCounterExample( Aig_Man_t * pAig, Aig_Man_t * pFrames, in
     pCex->iFrame = iFrame;
 
     // copy the bit data
-    for ( i = 0; i < Aig_ManPiNum(pFrames); i++ )
+    for ( i = 0; i < Aig_ManCiNum(pFrames); i++ )
     {
         if ( pModel[i] )
             Abc_InfoSetBit( pCex->pData, pCex->nRegs + i );
diff --git a/src/proof/int/intCheck.c b/src/proof/int/intCheck.c
index 57d6e7d0..2b14d8ae 100644
--- a/src/proof/int/intCheck.c
+++ b/src/proof/int/intCheck.c
@@ -112,10 +112,10 @@ Inter_Check_t * Inter_CheckStart( Aig_Man_t * pTrans, int nFramesK )
     p->vAssLits = Vec_IntAlloc( 100 );
     // generate the timeframes 
     p->pFrames = Inter_ManUnrollFrames( pTrans, nFramesK );
-    assert( Aig_ManPiNum(p->pFrames) == nFramesK * Saig_ManPiNum(pTrans) + Saig_ManRegNum(pTrans) );
-    assert( Aig_ManPoNum(p->pFrames) == nFramesK * Saig_ManRegNum(pTrans) );
+    assert( Aig_ManCiNum(p->pFrames) == nFramesK * Saig_ManPiNum(pTrans) + Saig_ManRegNum(pTrans) );
+    assert( Aig_ManCoNum(p->pFrames) == nFramesK * Saig_ManRegNum(pTrans) );
     // convert to CNF
-    p->pCnf = Cnf_Derive( p->pFrames, Aig_ManPoNum(p->pFrames) ); 
+    p->pCnf = Cnf_Derive( p->pFrames, Aig_ManCoNum(p->pFrames) ); 
     p->pSat = (sat_solver *)Cnf_DataWriteIntoSolver( p->pCnf, 1, 0 );
     // assign parameters
     p->nFramesK = nFramesK;
@@ -221,9 +221,9 @@ int Inter_CheckPerform( Inter_Check_t * p, Cnf_Dat_t * pCnfInt, int nTimeNewOut
 {
     Aig_Obj_t * pObj, * pObj2;
     int i, f, VarA, VarB, RetValue, Entry, status;
-    int nRegs = Aig_ManPiNum(pCnfInt->pMan);
-    assert( Aig_ManPoNum(p->pCnf->pMan) == p->nFramesK * nRegs );
-    assert( Aig_ManPoNum(pCnfInt->pMan) == 1 );
+    int nRegs = Aig_ManCiNum(pCnfInt->pMan);
+    assert( Aig_ManCoNum(p->pCnf->pMan) == p->nFramesK * nRegs );
+    assert( Aig_ManCoNum(pCnfInt->pMan) == 1 );
 
     // set runtime limit
     if ( nTimeNewOut )
@@ -242,7 +242,7 @@ int Inter_CheckPerform( Inter_Check_t * p, Cnf_Dat_t * pCnfInt, int nTimeNewOut
         // add equality clauses for the flop variables
         Aig_ManForEachCi( pCnfInt->pMan, pObj, i )
         {
-            pObj2 = f ? Aig_ManPo(p->pFrames, i + (f-1) * nRegs) : Aig_ManPi(p->pFrames, i);
+            pObj2 = f ? Aig_ManCo(p->pFrames, i + (f-1) * nRegs) : Aig_ManCi(p->pFrames, i);
             Inter_CheckAddEqual( p, pCnfInt->pVarNums[pObj->Id], p->pCnf->pVarNums[pObj2->Id] );
         }
         // add final clauses
@@ -251,14 +251,14 @@ int Inter_CheckPerform( Inter_Check_t * p, Cnf_Dat_t * pCnfInt, int nTimeNewOut
             if ( f == Vec_IntSize(p->vOrLits) ) // find time here
             {
                 // add literal to this frame
-                VarB = pCnfInt->pVarNums[ Aig_ManPo(pCnfInt->pMan, 0)->Id ];
+                VarB = pCnfInt->pVarNums[ Aig_ManCo(pCnfInt->pMan, 0)->Id ];
                 Vec_IntPush( p->vOrLits, VarB );
             }
             else
             {
                 // add OR gate for this frame
                 VarA = Vec_IntEntry( p->vOrLits, f );
-                VarB = pCnfInt->pVarNums[ Aig_ManPo(pCnfInt->pMan, 0)->Id ];
+                VarB = pCnfInt->pVarNums[ Aig_ManCo(pCnfInt->pMan, 0)->Id ];
                 Inter_CheckAddOrGate( p, VarA, VarB, p->nVars + pCnfInt->nVars );
                 Vec_IntWriteEntry( p->vOrLits, f, p->nVars + pCnfInt->nVars ); // using var ID!
             }
@@ -266,7 +266,7 @@ int Inter_CheckPerform( Inter_Check_t * p, Cnf_Dat_t * pCnfInt, int nTimeNewOut
         else
         {
             // add AND gate for this frame
-            VarB = pCnfInt->pVarNums[ Aig_ManPo(pCnfInt->pMan, 0)->Id ];
+            VarB = pCnfInt->pVarNums[ Aig_ManCo(pCnfInt->pMan, 0)->Id ];
             Vec_IntPush( p->vAndLits, VarB );
         }
         // update variable IDs
diff --git a/src/proof/int/intContain.c b/src/proof/int/intContain.c
index 213c557c..a031c7a4 100644
--- a/src/proof/int/intContain.c
+++ b/src/proof/int/intContain.c
@@ -161,7 +161,7 @@ void Inter_ManAppendCone( Aig_Man_t * pOld, Aig_Man_t * pNew, Aig_Obj_t ** ppNew
 {
     Aig_Obj_t * pObj;
     int i;
-    assert( Aig_ManPoNum(pOld) == 1 );
+    assert( Aig_ManCoNum(pOld) == 1 );
     // create the PIs
     Aig_ManCleanData( pOld );
     Aig_ManConst1(pOld)->pData = Aig_ManConst1(pNew);
@@ -171,7 +171,7 @@ void Inter_ManAppendCone( Aig_Man_t * pOld, Aig_Man_t * pNew, Aig_Obj_t ** ppNew
     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 );
+    pObj = Aig_ManCo( pOld, 0 );
     Aig_ObjCreateCo( pNew, Aig_NotCond( Aig_ObjChild0Copy(pObj), fCompl ) );
 }
 
@@ -283,7 +283,7 @@ int Inter_ManCheckUniqueness( Aig_Man_t * p, sat_solver * pSat, Cnf_Dat_t * pCnf
         return 1;
 //    assert( Saig_ManPoNum(p) == 1 );
     assert( Aig_ManRegNum(p) > 0 );
-    assert( Aig_ManRegNum(p) < Aig_ManPiNum(p) );
+    assert( Aig_ManRegNum(p) < Aig_ManCiNum(p) );
 
     // get the counter-example
     vPis = Vec_IntAlloc( 100 );
@@ -303,12 +303,12 @@ int Inter_ManCheckUniqueness( Aig_Man_t * p, sat_solver * pSat, Cnf_Dat_t * pCnf
     for ( i = 0; i < nFrames; i++ )
         Aig_ManForEachPiSeq( p, pObj, k )
             Fra_SmlAssignConst( pSml, pObj, pCounterEx[iBit++], i );
-    assert( iBit == Aig_ManPiNum(pCnf->pMan) );
+    assert( iBit == Aig_ManCiNum(pCnf->pMan) );
     // run simulation
     Fra_SmlSimulateOne( pSml );
 
     // check if the given output has failed
-//    RetValue = !Fra_SmlNodeIsZero( pSml, Aig_ManPo(pAig, 0) );
+//    RetValue = !Fra_SmlNodeIsZero( pSml, Aig_ManCo(pAig, 0) );
 //    assert( RetValue );
 
     // check values at the internal nodes
diff --git a/src/proof/int/intCore.c b/src/proof/int/intCore.c
index 10a8fc74..8bef9c59 100644
--- a/src/proof/int/intCore.c
+++ b/src/proof/int/intCore.c
@@ -139,7 +139,7 @@ clk2 = clock();
             p->pInter = Inter_ManStartOneOutput( pAig, 1 );
         else
             p->pInter = Inter_ManStartInitState( Aig_ManRegNum(pAig) );
-        assert( Aig_ManPoNum(p->pInter) == 1 );
+        assert( Aig_ManCoNum(p->pInter) == 1 );
 clk = clock();
         p->pCnfInter = Cnf_Derive( p->pInter, 0 );  
 p->timeCnf += clock() - clk;    
@@ -157,7 +157,7 @@ p->timeRwr += clock() - clk;
         // can also do SAT sweeping on the timeframes...
 clk = clock();
         if ( pPars->fUseBackward )
-            p->pCnfFrames = Cnf_Derive( p->pFrames, Aig_ManPoNum(p->pFrames) );  
+            p->pCnfFrames = Cnf_Derive( p->pFrames, Aig_ManCoNum(p->pFrames) );  
         else
 //            p->pCnfFrames = Cnf_Derive( p->pFrames, 0 );  
             p->pCnfFrames = Cnf_DeriveSimple( p->pFrames, 0 );  
@@ -285,7 +285,7 @@ clk = clock();
 p->timeRwr += clock() - clk;
 
             // check if interpolant is trivial
-            if ( p->pInterNew == NULL || Aig_ObjChild0(Aig_ManPo(p->pInterNew,0)) == Aig_ManConst0(p->pInterNew) )
+            if ( p->pInterNew == NULL || Aig_ObjChild0(Aig_ManCo(p->pInterNew,0)) == Aig_ManConst0(p->pInterNew) )
             { 
 //                printf( "interpolant is constant 0\n" );
                 if ( pPars->fVerbose )
@@ -300,7 +300,7 @@ p->timeRwr += clock() - clk;
 clk = clock();
             if ( pPars->fCheckKstep ) // k-step unique-state induction
             {
-                if ( Aig_ManPiNum(p->pInterNew) == Aig_ManPiNum(p->pInter) )
+                if ( Aig_ManCiNum(p->pInterNew) == Aig_ManCiNum(p->pInter) )
                 {
                     if ( pPars->fTransLoop || pPars->fUseBackward || pPars->nFramesK > 1 )
                     {
@@ -326,7 +326,7 @@ timeTemp = clock() - clk2;
             }
             else // combinational containment
             {
-                if ( Aig_ManPiNum(p->pInterNew) == Aig_ManPiNum(p->pInter) )
+                if ( Aig_ManCiNum(p->pInterNew) == Aig_ManCiNum(p->pInter) )
                     Status = Inter_ManCheckContainment( p->pInterNew, p->pInter );
                 else
                     Status = 0;
diff --git a/src/proof/int/intCtrex.c b/src/proof/int/intCtrex.c
index 22e689f4..04aaa271 100644
--- a/src/proof/int/intCtrex.c
+++ b/src/proof/int/intCtrex.c
@@ -75,7 +75,7 @@ Aig_Man_t * Inter_ManFramesBmc( Aig_Man_t * pAig, int nFrames )
             pObjLo->pData = pObjLi->pData;
     }
     // create POs for the output of the last frame
-    pObj = Aig_ManPo( pAig, 0 );
+    pObj = Aig_ManCo( pAig, 0 );
     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 adc692cb..d7bc73d6 100644
--- a/src/proof/int/intDup.c
+++ b/src/proof/int/intDup.c
@@ -141,7 +141,7 @@ Aig_Man_t * Inter_ManStartOneOutput( Aig_Man_t * p, int fAddFirstPo )
     }
     // set registers
     pNew->nRegs    = fAddFirstPo? 0 : p->nRegs;
-    pNew->nTruePis = fAddFirstPo? Aig_ManPiNum(p) + 1 : p->nTruePis + 1;
+    pNew->nTruePis = fAddFirstPo? Aig_ManCiNum(p) + 1 : p->nTruePis + 1;
     pNew->nTruePos = fAddFirstPo + Saig_ManConstrNum(p);
     // duplicate internal nodes
     Aig_ManForEachNode( p, pObj, i )
@@ -158,7 +158,7 @@ Aig_Man_t * Inter_ManStartOneOutput( Aig_Man_t * p, int fAddFirstPo )
     // add the PO
     if ( fAddFirstPo )
     {
-        pObj = Aig_ManPo( p, 0 );
+        pObj = Aig_ManCo( p, 0 );
         Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
     }
     else
diff --git a/src/proof/int/intFrames.c b/src/proof/int/intFrames.c
index 8e74d99a..7c5231b7 100644
--- a/src/proof/int/intFrames.c
+++ b/src/proof/int/intFrames.c
@@ -99,7 +99,7 @@ Aig_Man_t * Inter_ManFramesInter( Aig_Man_t * pAig, int nFrames, int fAddRegOuts
     // create the only PO of the manager
     else
     {
-        pObj = Aig_ManPo( pAig, 0 );
+        pObj = Aig_ManCo( pAig, 0 );
         Aig_ObjCreateCo( pFrames, Aig_ObjChild0Copy(pObj) );
     }
     Aig_ManCleanup( pFrames );
diff --git a/src/proof/int/intInter.c b/src/proof/int/intInter.c
index ef32294b..ffc462d3 100644
--- a/src/proof/int/intInter.c
+++ b/src/proof/int/intInter.c
@@ -45,10 +45,10 @@ ABC_NAMESPACE_IMPL_START
 Aig_Man_t * Inter_ManDupExpand( Aig_Man_t * pInter, Aig_Man_t * pOther )
 {
     Aig_Man_t * pInterC;
-    assert( Aig_ManPiNum(pInter) <= Aig_ManPiNum(pOther) );
+    assert( Aig_ManCiNum(pInter) <= Aig_ManCiNum(pOther) );
     pInterC = Aig_ManDupSimple( pInter );
-    Aig_IthVar( pInterC, Aig_ManPiNum(pOther)-1 );
-    assert( Aig_ManPiNum(pInterC) == Aig_ManPiNum(pOther) );
+    Aig_IthVar( pInterC, Aig_ManCiNum(pOther)-1 );
+    assert( Aig_ManCiNum(pInterC) == Aig_ManCiNum(pOther) );
     return pInterC;
 }
 
diff --git a/src/proof/int/intM114.c b/src/proof/int/intM114.c
index c37cb2c6..ed3ef80e 100644
--- a/src/proof/int/intM114.c
+++ b/src/proof/int/intM114.c
@@ -61,10 +61,10 @@ sat_solver * Inter_ManDeriveSatSolver(
     assert( Aig_ManRegNum(pInter) == 0 );
     assert( Aig_ManRegNum(pAig) > 0 );
     assert( Aig_ManRegNum(pFrames) == 0 );
-    assert( Aig_ManPoNum(pInter) == 1 );
-    assert( Aig_ManPoNum(pFrames) == fUseBackward? Saig_ManRegNum(pAig) : 1 );
-    assert( fUseBackward || Aig_ManPiNum(pInter) == Aig_ManRegNum(pAig) );
-//    assert( (Aig_ManPiNum(pFrames) - Aig_ManRegNum(pAig)) % Saig_ManPiNum(pAig) == 0 );
+    assert( Aig_ManCoNum(pInter) == 1 );
+    assert( Aig_ManCoNum(pFrames) == fUseBackward? Saig_ManRegNum(pAig) : 1 );
+    assert( fUseBackward || Aig_ManCiNum(pInter) == Aig_ManRegNum(pAig) );
+//    assert( (Aig_ManCiNum(pFrames) - Aig_ManRegNum(pAig)) % Saig_ManPiNum(pAig) == 0 );
 
     // prepare CNFs
     Cnf_DataLift( pCnfAig,   pCnfFrames->nVars );
@@ -93,12 +93,12 @@ sat_solver * Inter_ManDeriveSatSolver(
     {
         Saig_ManForEachLi( pAig, pObj2, i )
         {
-            if ( Saig_ManRegNum(pAig) == Aig_ManPiNum(pInter) )
-                pObj = Aig_ManPi( pInter, i );
+            if ( Saig_ManRegNum(pAig) == Aig_ManCiNum(pInter) )
+                pObj = Aig_ManCi( pInter, i );
             else
             {
-                assert( Aig_ManPiNum(pAig) == Aig_ManPiNum(pInter) );
-                pObj = Aig_ManPi( pInter, Aig_ManPiNum(pAig)-Saig_ManRegNum(pAig) + i );
+                assert( Aig_ManCiNum(pAig) == Aig_ManCiNum(pInter) );
+                pObj = Aig_ManCi( pInter, Aig_ManCiNum(pAig)-Saig_ManRegNum(pAig) + i );
             }
 
             Lits[0] = toLitCond( pCnfInter->pVarNums[pObj->Id], 0 );
diff --git a/src/proof/int/intM114p.c b/src/proof/int/intM114p.c
index 6164a389..f143dc39 100644
--- a/src/proof/int/intM114p.c
+++ b/src/proof/int/intM114p.c
@@ -59,10 +59,10 @@ M114p_Solver_t Inter_ManDeriveSatSolverM114p(
     assert( Aig_ManRegNum(pInter) == 0 );
     assert( Aig_ManRegNum(pAig) > 0 );
     assert( Aig_ManRegNum(pFrames) == 0 );
-    assert( Aig_ManPoNum(pInter) == 1 );
-    assert( Aig_ManPoNum(pFrames) == 1 );
-    assert( Aig_ManPiNum(pInter) == Aig_ManRegNum(pAig) );
-//    assert( (Aig_ManPiNum(pFrames) - Aig_ManRegNum(pAig)) % Saig_ManPiNum(pAig) == 0 );
+    assert( Aig_ManCoNum(pInter) == 1 );
+    assert( Aig_ManCoNum(pFrames) == 1 );
+    assert( Aig_ManCiNum(pInter) == Aig_ManRegNum(pAig) );
+//    assert( (Aig_ManCiNum(pFrames) - Aig_ManRegNum(pAig)) % Saig_ManPiNum(pAig) == 0 );
 
     // prepare CNFs
     Cnf_DataLift( pCnfAig,   pCnfFrames->nVars );
diff --git a/src/proof/live/liveness.c b/src/proof/live/liveness.c
index d961e509..e457b3f8 100644
--- a/src/proof/live/liveness.c
+++ b/src/proof/live/liveness.c
@@ -122,12 +122,12 @@ char * retrieveTruePiName( Abc_Ntk_t *pNtkOld, Aig_Man_t *pAigOld, Aig_Man_t *pA
     Aig_ManForEachCi( pAigNew, pObj, index )
         if( pObj == pObjPivot )
             break;
-    assert( index < Aig_ManPiNum( pAigNew ) - Aig_ManRegNum( pAigNew ) );
+    assert( index < Aig_ManCiNum( pAigNew ) - Aig_ManRegNum( pAigNew ) );
     if( index == Saig_ManPiNum( pAigNew ) - 1 )
         return "SAVE_BIERE";
     else
     {
-        pObjOld = Aig_ManPi( pAigOld, index );
+        pObjOld = Aig_ManCi( pAigOld, index );
         pNode = Abc_NtkPi( pNtkOld, index );
         assert( pObjOld->pData == pObjPivot );
         return Abc_ObjName( pNode );
@@ -148,7 +148,7 @@ char * retrieveLOName( Abc_Ntk_t *pNtkOld, Aig_Man_t *pAigOld, Aig_Man_t *pAigNe
     if( index < originalLatchNum )
     {
         oldIndex = Saig_ManPiNum( pAigOld ) + index;
-        pObjOld = Aig_ManPi( pAigOld, oldIndex );
+        pObjOld = Aig_ManCi( pAigOld, oldIndex );
         pNode = Abc_NtkCi( pNtkOld, oldIndex );
         assert( pObjOld->pData == pObjPivot );
         return Abc_ObjName( pNode );
@@ -158,7 +158,7 @@ char * retrieveLOName( Abc_Ntk_t *pNtkOld, Aig_Man_t *pAigOld, Aig_Man_t *pAigNe
     else if( index > originalLatchNum && index < 2 * originalLatchNum + 1 )
     {
         oldIndex = Saig_ManPiNum( pAigOld ) + index - originalLatchNum - 1;
-        pObjOld = Aig_ManPi( pAigOld, oldIndex );
+        pObjOld = Aig_ManCi( pAigOld, oldIndex );
         pNode = Abc_NtkCi( pNtkOld, oldIndex );
         sprintf( dummyStr, "%s__%s", Abc_ObjName( pNode ), "SHADOW");
         return dummyStr;
@@ -219,26 +219,26 @@ Vec_Ptr_t *vecPis, *vecPiNames;
 Vec_Ptr_t *vecLos, *vecLoNames;
 
 
-int Aig_ManPiCleanupBiere( Aig_Man_t * p )
+int Aig_ManCiCleanupBiere( Aig_Man_t * p )
 {
-    int nPisOld = Aig_ManPiNum(p);
+    int nPisOld = Aig_ManCiNum(p);
     
-    p->nObjs[AIG_OBJ_PI] = Vec_PtrSize( p->vPis );
+    p->nObjs[AIG_OBJ_CI] = Vec_PtrSize( p->vCis );
     if ( Aig_ManRegNum(p) )
-        p->nTruePis = Aig_ManPiNum(p) - Aig_ManRegNum(p);
+        p->nTruePis = Aig_ManCiNum(p) - Aig_ManRegNum(p);
     
-    return nPisOld - Aig_ManPiNum(p);
+    return nPisOld - Aig_ManCiNum(p);
 }
 
 
-int Aig_ManPoCleanupBiere( Aig_Man_t * p )
+int Aig_ManCoCleanupBiere( Aig_Man_t * p )
 {
-    int nPosOld = Aig_ManPoNum(p);
+    int nPosOld = Aig_ManCoNum(p);
 
-    p->nObjs[AIG_OBJ_PO] = Vec_PtrSize( p->vPos );
+    p->nObjs[AIG_OBJ_CO] = Vec_PtrSize( p->vCos );
     if ( Aig_ManRegNum(p) )
-        p->nTruePos = Aig_ManPoNum(p) - Aig_ManRegNum(p);
-    return nPosOld - Aig_ManPoNum(p);
+        p->nTruePos = Aig_ManCoNum(p) - Aig_ManRegNum(p);
+    return nPosOld - Aig_ManCoNum(p);
 }
 
 Aig_Man_t * LivenessToSafetyTransformation( int mode, Abc_Ntk_t * pNtk, Aig_Man_t * p, 
@@ -518,8 +518,8 @@ Aig_Man_t * LivenessToSafetyTransformation( int mode, Abc_Ntk_t * pNtk, Aig_Man_
 
     Aig_ManSetRegNum( pNew, nRegCount );
 
-    Aig_ManPiCleanupBiere( pNew );
-    Aig_ManPoCleanupBiere( pNew );
+    Aig_ManCiCleanupBiere( pNew );
+    Aig_ManCoCleanupBiere( pNew );
     
     Aig_ManCleanup( pNew );
     
@@ -527,7 +527,7 @@ Aig_Man_t * LivenessToSafetyTransformation( int mode, Abc_Ntk_t * pNtk, Aig_Man_
     
     if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
     {
-            assert((Aig_Obj_t *)Vec_PtrEntry(pNew->vPos, Saig_ManPoNum(pNew)+Aig_ObjPioNum(pObjSavedLo)-Saig_ManPiNum(p)-1) == pObjSavedLi);
+            assert((Aig_Obj_t *)Vec_PtrEntry(pNew->vCos, Saig_ManPoNum(pNew)+Aig_ObjPioNum(pObjSavedLo)-Saig_ManPiNum(p)-1) == pObjSavedLi);
             assert( Saig_ManPiNum( p ) + 1 == Saig_ManPiNum( pNew ) );
             assert( Saig_ManRegNum( pNew ) == Saig_ManRegNum( p ) * 2 + 1 + liveLatch + fairLatch );
     }
@@ -821,8 +821,8 @@ Aig_Man_t * LivenessToSafetyTransformationAbs( int mode, Abc_Ntk_t * pNtk, Aig_M
 
     Aig_ManSetRegNum( pNew, nRegCount );
 
-    Aig_ManPiCleanupBiere( pNew );
-    Aig_ManPoCleanupBiere( pNew );
+    Aig_ManCiCleanupBiere( pNew );
+    Aig_ManCoCleanupBiere( pNew );
     
     Aig_ManCleanup( pNew );
     
@@ -830,7 +830,7 @@ Aig_Man_t * LivenessToSafetyTransformationAbs( int mode, Abc_Ntk_t * pNtk, Aig_M
     
     if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
     {
-            assert((Aig_Obj_t *)Vec_PtrEntry(pNew->vPos, Saig_ManPoNum(pNew)+Aig_ObjPioNum(pObjSavedLo)-Saig_ManPiNum(p)-1) == pObjSavedLi);
+            assert((Aig_Obj_t *)Vec_PtrEntry(pNew->vCos, Saig_ManPoNum(pNew)+Aig_ObjPioNum(pObjSavedLo)-Saig_ManPiNum(p)-1) == pObjSavedLi);
             assert( Saig_ManPiNum( p ) + 1 == Saig_ManPiNum( pNew ) );
             assert( Saig_ManRegNum( pNew ) == Saig_ManRegNum( p ) + Vec_IntSize( vFlops ) + 1 + liveLatch + fairLatch );
     }
@@ -1128,8 +1128,8 @@ Aig_Man_t * LivenessToSafetyTransformationOneStepLoop( int mode, Abc_Ntk_t * pNt
 
     //printf("\nSaig_ManPiNum = %d, Reg Num = %d, before everything, before Pi cleanup\n", Vec_PtrSize( pNew->vPis ), pNew->nRegs );
 
-    Aig_ManPiCleanupBiere( pNew );
-    Aig_ManPoCleanupBiere( pNew );
+    Aig_ManCiCleanupBiere( pNew );
+    Aig_ManCoCleanupBiere( pNew );
 
     Aig_ManCleanup( pNew );
     
@@ -1151,7 +1151,7 @@ Vec_Ptr_t * populateLivenessVector( Abc_Ntk_t *pNtk, Aig_Man_t *pAig )
         //if( strstr( Abc_ObjName( pNode ), "assert_fair") != NULL )
         if( nodeName_starts_with( pNode, "assert_fair" ) )
         {
-            Vec_PtrPush( vLive, Aig_ManPo( pAig, i ) );
+            Vec_PtrPush( vLive, Aig_ManCo( pAig, i ) );
             liveCounter++;
         }
     printf("Number of liveness property found = %d\n", liveCounter);
@@ -1169,7 +1169,7 @@ Vec_Ptr_t * populateFairnessVector( Abc_Ntk_t *pNtk, Aig_Man_t *pAig )
         //if( strstr( Abc_ObjName( pNode ), "assume_fair") != NULL )
         if( nodeName_starts_with( pNode, "assume_fair" ) )
         {
-            Vec_PtrPush( vFair, Aig_ManPo( pAig, i ) );
+            Vec_PtrPush( vFair, Aig_ManCo( pAig, i ) );
             fairCounter++;
         }
     printf("Number of fairness property found = %d\n", fairCounter);
@@ -1187,7 +1187,7 @@ Vec_Ptr_t * populateSafetyAssertionVector( Abc_Ntk_t *pNtk, Aig_Man_t *pAig )
         //if( strstr( Abc_ObjName( pNode ), "Assert") != NULL )
         if( nodeName_starts_with( pNode, "assert_safety" ) || nodeName_starts_with( pNode, "Assert" ))
         {
-            Vec_PtrPush( vAssertSafety, Aig_ManPo( pAig, i ) );
+            Vec_PtrPush( vAssertSafety, Aig_ManCo( pAig, i ) );
             assertSafetyCounter++;
         }
     printf("Number of safety property found = %d\n", assertSafetyCounter);
@@ -1205,7 +1205,7 @@ Vec_Ptr_t * populateSafetyAssumptionVector( Abc_Ntk_t *pNtk, Aig_Man_t *pAig )
         //if( strstr( Abc_ObjName( pNode ), "Assert") != NULL )
         if( nodeName_starts_with( pNode, "assume_safety" ) || nodeName_starts_with( pNode, "Assume" ))
         {
-            Vec_PtrPush( vAssumeSafety, Aig_ManPo( pAig, i ) );
+            Vec_PtrPush( vAssumeSafety, Aig_ManCo( pAig, i ) );
             assumeSafetyCounter++;
         }
     printf("Number of assume_safety property found = %d\n", assumeSafetyCounter);
@@ -2247,8 +2247,8 @@ Aig_Man_t * LivenessToSafetyTransformationWithLTL( int mode, Abc_Ntk_t * pNtk, A
 
     Aig_ManSetRegNum( pNew, nRegCount );
 
-    Aig_ManPiCleanupBiere( pNew );
-    Aig_ManPoCleanupBiere( pNew );
+    Aig_ManCiCleanupBiere( pNew );
+    Aig_ManCoCleanupBiere( pNew );
     
     Aig_ManCleanup( pNew );
     
@@ -2256,7 +2256,7 @@ Aig_Man_t * LivenessToSafetyTransformationWithLTL( int mode, Abc_Ntk_t * pNtk, A
     
     if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
     {
-            assert((Aig_Obj_t *)Vec_PtrEntry(pNew->vPos, Saig_ManPoNum(pNew)+Aig_ObjPioNum(pObjSavedLo)-Saig_ManPiNum(p)-1) == pObjSavedLi);
+            assert((Aig_Obj_t *)Vec_PtrEntry(pNew->vCos, Saig_ManPoNum(pNew)+Aig_ObjPioNum(pObjSavedLo)-Saig_ManPiNum(p)-1) == pObjSavedLi);
             assert( Saig_ManPiNum( p ) + 1 == Saig_ManPiNum( pNew ) );
             //assert( Saig_ManRegNum( pNew ) == Saig_ManRegNum( p ) * 2 + 1 + liveLatch + fairLatch );
     }
diff --git a/src/proof/live/liveness_sim.c b/src/proof/live/liveness_sim.c
index 552c5204..b99df807 100644
--- a/src/proof/live/liveness_sim.c
+++ b/src/proof/live/liveness_sim.c
@@ -85,12 +85,12 @@ static char * retrieveTruePiName( Abc_Ntk_t *pNtkOld, Aig_Man_t *pAigOld, Aig_Ma
     Aig_ManForEachCi( pAigNew, pObj, index )
         if( pObj == pObjPivot )
             break;
-    assert( index < Aig_ManPiNum( pAigNew ) - Aig_ManRegNum( pAigNew ) );
+    assert( index < Aig_ManCiNum( pAigNew ) - Aig_ManRegNum( pAigNew ) );
     if( index == Saig_ManPiNum( pAigNew ) - 1 )
         return "SAVE_BIERE";
     else
     {
-        pObjOld = Aig_ManPi( pAigOld, index );
+        pObjOld = Aig_ManCi( pAigOld, index );
         pNode = Abc_NtkPi( pNtkOld, index );
         assert( pObjOld->pData == pObjPivot );
         return Abc_ObjName( pNode );
@@ -111,7 +111,7 @@ static char * retrieveLOName( Abc_Ntk_t *pNtkOld, Aig_Man_t *pAigOld, Aig_Man_t
     if( index < originalLatchNum )
     {
         oldIndex = Saig_ManPiNum( pAigOld ) + index;
-        pObjOld = Aig_ManPi( pAigOld, oldIndex );
+        pObjOld = Aig_ManCi( pAigOld, oldIndex );
         pNode = Abc_NtkCi( pNtkOld, oldIndex );
         assert( pObjOld->pData == pObjPivot );
         return Abc_ObjName( pNode );
@@ -121,7 +121,7 @@ static char * retrieveLOName( Abc_Ntk_t *pNtkOld, Aig_Man_t *pAigOld, Aig_Man_t
     else if( index > originalLatchNum && index < 2 * originalLatchNum + 1 )
     {
         oldIndex = Saig_ManPiNum( pAigOld ) + index - originalLatchNum - 1;
-        pObjOld = Aig_ManPi( pAigOld, oldIndex );
+        pObjOld = Aig_ManCi( pAigOld, oldIndex );
         pNode = Abc_NtkCi( pNtkOld, oldIndex );
         sprintf( dummyStr, "%s__%s", Abc_ObjName( pNode ), "SHADOW");
         return dummyStr;
@@ -172,26 +172,26 @@ extern Vec_Ptr_t *vecPis, *vecPiNames;
 extern Vec_Ptr_t *vecLos, *vecLoNames;
 
 
-static int Aig_ManPiCleanupBiere( Aig_Man_t * p )
+static int Aig_ManCiCleanupBiere( Aig_Man_t * p )
 {
-    int nPisOld = Aig_ManPiNum(p);
+    int nPisOld = Aig_ManCiNum(p);
     
-    p->nObjs[AIG_OBJ_PI] = Vec_PtrSize( p->vPis );
+    p->nObjs[AIG_OBJ_CI] = Vec_PtrSize( p->vCis );
     if ( Aig_ManRegNum(p) )
-        p->nTruePis = Aig_ManPiNum(p) - Aig_ManRegNum(p);
+        p->nTruePis = Aig_ManCiNum(p) - Aig_ManRegNum(p);
     
-    return nPisOld - Aig_ManPiNum(p);
+    return nPisOld - Aig_ManCiNum(p);
 }
 
 
-static int Aig_ManPoCleanupBiere( Aig_Man_t * p )
+static int Aig_ManCoCleanupBiere( Aig_Man_t * p )
 {
-    int nPosOld = Aig_ManPoNum(p);
+    int nPosOld = Aig_ManCoNum(p);
 
-    p->nObjs[AIG_OBJ_PO] = Vec_PtrSize( p->vPos );
+    p->nObjs[AIG_OBJ_CO] = Vec_PtrSize( p->vCos );
     if ( Aig_ManRegNum(p) )
-        p->nTruePos = Aig_ManPoNum(p) - Aig_ManRegNum(p);
-    return nPosOld - Aig_ManPoNum(p);
+        p->nTruePos = Aig_ManCoNum(p) - Aig_ManRegNum(p);
+    return nPosOld - Aig_ManCoNum(p);
 }
 
 static Aig_Man_t * LivenessToSafetyTransformationSim( Abc_Ntk_t * pNtk, Aig_Man_t * p, Vec_Ptr_t *vLive, Vec_Ptr_t *vFair )
@@ -459,14 +459,14 @@ static Aig_Man_t * LivenessToSafetyTransformationSim( Abc_Ntk_t * pNtk, Aig_Man_
 
     Aig_ManSetRegNum( pNew, nRegCount );
 
-    Aig_ManPiCleanupBiere( pNew );
-    Aig_ManPoCleanupBiere( pNew );
+    Aig_ManCiCleanupBiere( pNew );
+    Aig_ManCoCleanupBiere( pNew );
     
     Aig_ManCleanup( pNew );
     assert( Aig_ManCheck( pNew ) );
     
 #ifndef DUPLICATE_CKT_DEBUG
-    assert((Aig_Obj_t *)Vec_PtrEntry(pNew->vPos, Saig_ManPoNum(pNew)+Aig_ObjPioNum(pObjSavedLo)-Saig_ManPiNum(p)-1) == pObjSavedLi);
+    assert((Aig_Obj_t *)Vec_PtrEntry(pNew->vCos, Saig_ManPoNum(pNew)+Aig_ObjPioNum(pObjSavedLo)-Saig_ManPiNum(p)-1) == pObjSavedLi);
     assert( Saig_ManPoNum( pNew ) == 1 );
     assert( Saig_ManPiNum( p ) + 1 == Saig_ManPiNum( pNew ) );
     assert( Saig_ManRegNum( pNew ) == Saig_ManRegNum( p ) * 2 + 1 + liveLatch + fairLatch );
@@ -680,10 +680,10 @@ static Aig_Man_t * LivenessToSafetyTransformationOneStepLoopSim( Abc_Ntk_t * pNt
 
     Aig_ManSetRegNum( pNew, nRegCount );
 
-    printf("\nSaig_ManPiNum = %d, Reg Num = %d, before everything, before Pi cleanup\n", Vec_PtrSize( pNew->vPis ), pNew->nRegs );
+    printf("\nSaig_ManPiNum = %d, Reg Num = %d, before everything, before Pi cleanup\n", Vec_PtrSize( pNew->vCis ), pNew->nRegs );
 
-    Aig_ManPiCleanupBiere( pNew );
-    Aig_ManPoCleanupBiere( pNew );
+    Aig_ManCiCleanupBiere( pNew );
+    Aig_ManCoCleanupBiere( pNew );
 
     Aig_ManCleanup( pNew );
     
@@ -704,7 +704,7 @@ static Vec_Ptr_t * populateLivenessVector( Abc_Ntk_t *pNtk, Aig_Man_t *pAig )
     Abc_NtkForEachPo( pNtk, pNode, i )
         if( strstr( Abc_ObjName( pNode ), "assert_fair") != NULL )
         {
-            Vec_PtrPush( vLive, Aig_ManPo( pAig, i ) );
+            Vec_PtrPush( vLive, Aig_ManCo( pAig, i ) );
             liveCounter++;
         }
     printf("\nNumber of liveness property found = %d\n", liveCounter);
@@ -721,7 +721,7 @@ static Vec_Ptr_t * populateFairnessVector( Abc_Ntk_t *pNtk, Aig_Man_t *pAig )
     Abc_NtkForEachPo( pNtk, pNode, i )
         if( strstr( Abc_ObjName( pNode ), "assume_fair") != NULL )
         {
-            Vec_PtrPush( vFair, Aig_ManPo( pAig, i ) );
+            Vec_PtrPush( vFair, Aig_ManCo( pAig, i ) );
             fairCounter++;
         }
     printf("\nNumber of fairness property found = %d\n", fairCounter);
diff --git a/src/proof/live/ltl_parser.c b/src/proof/live/ltl_parser.c
index 5572611f..de567576 100644
--- a/src/proof/live/ltl_parser.c
+++ b/src/proof/live/ltl_parser.c
@@ -762,8 +762,8 @@ void populateBoolWithAigNodePtr( Abc_Ntk_t *pNtk, Aig_Man_t *pAigOld, Aig_Man_t
             Abc_NtkForEachPo( pNtk, pNode, i )
                 if( strcmp( Abc_ObjName( pNode ), targetName ) == 0 )
                 {
-                    pObj = Aig_ManPo( pAigOld, i );
-                    assert( Aig_ObjIsPo( pObj ));
+                    pObj = Aig_ManCo( pAigOld, i );
+                    assert( Aig_ObjIsCo( pObj ));
                     pDriverImage = Aig_NotCond((Aig_Obj_t *)Aig_Regular(Aig_ObjChild0( pObj ))->pData, Aig_ObjFaninC0(pObj));
                     topASTNode->pObj = pDriverImage;
                     return;
diff --git a/src/proof/llb/llb1Constr.c b/src/proof/llb/llb1Constr.c
index 4ce911db..1ef4ce14 100644
--- a/src/proof/llb/llb1Constr.c
+++ b/src/proof/llb/llb1Constr.c
@@ -150,7 +150,7 @@ void Llb_ManComputeIndCase( Aig_Man_t * p, DdManager * dd, Vec_Int_t * vNodes )
     Vec_PtrWriteEntry( vBdds, Aig_ObjId(Aig_ManConst1(p)), bFunc );
     Saig_ManForEachPi( p, pObj, i )
     {
-        bFunc = Cudd_bddIthVar( dd, Aig_ManPiNum(p) + i );  Cudd_Ref( bFunc );
+        bFunc = Cudd_bddIthVar( dd, Aig_ManCiNum(p) + i );  Cudd_Ref( bFunc );
         Vec_PtrWriteEntry( vBdds, Aig_ObjId(pObj), bFunc );
     }
     Saig_ManForEachLi( p, pObj, i )
@@ -201,11 +201,11 @@ Vec_Int_t * Llb_ManComputeBaseCase( Aig_Man_t * p, DdManager * dd )
     Vec_Int_t * vNodes;
     Aig_Obj_t * pObj, * pRoot;
     int i;
-    pRoot = Aig_ManPo( p, 0 );
+    pRoot = Aig_ManCo( p, 0 );
     vNodes = Vec_IntStartFull( Aig_ManObjNumMax(p) );
     Aig_ManForEachObj( p, pObj, i )
     {
-        if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
+        if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsCi(pObj) )
             continue;
         if ( Cudd_bddLeq( dd, (DdNode *)pObj->pData, Cudd_Not(pRoot->pData) ) )
             Vec_IntWriteEntry( vNodes, i, 1 );
@@ -232,7 +232,7 @@ DdManager * Llb_ManConstructGlobalBdds( Aig_Man_t * p )
     DdNode * bBdd0, * bBdd1;
     Aig_Obj_t * pObj;
     int i;
-    dd = Cudd_Init( Aig_ManPiNum(p), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
+    dd = Cudd_Init( Aig_ManCiNum(p), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
     Cudd_AutodynEnable( dd,  CUDD_REORDER_SYMM_SIFT );
     pObj = Aig_ManConst1(p);
     pObj->pData = Cudd_ReadOne(dd);  Cudd_Ref( (DdNode *)pObj->pData );
diff --git a/src/proof/llb/llb1Core.c b/src/proof/llb/llb1Core.c
index ee697748..56e0cc6b 100644
--- a/src/proof/llb/llb1Core.c
+++ b/src/proof/llb/llb1Core.c
@@ -89,7 +89,7 @@ void Llb_ManPrintAig( Llb_Man_t * p )
     Abc_Print( 1, "pi =%3d  ",    Saig_ManPiNum(p->pAig) );
     Abc_Print( 1, "po =%3d  ",    Saig_ManPoNum(p->pAig) );
     Abc_Print( 1, "ff =%3d  ",    Saig_ManRegNum(p->pAig) );
-    Abc_Print( 1, "int =%5d  ",   Vec_IntSize(p->vVar2Obj)-Aig_ManPiNum(p->pAig)-Saig_ManRegNum(p->pAig) );
+    Abc_Print( 1, "int =%5d  ",   Vec_IntSize(p->vVar2Obj)-Aig_ManCiNum(p->pAig)-Saig_ManRegNum(p->pAig) );
     Abc_Print( 1, "var =%5d  ",   Vec_IntSize(p->vVar2Obj) );
     Abc_Print( 1, "part =%5d  ",  Vec_PtrSize(p->vGroups)-2 );
     Abc_Print( 1, "and =%5d  ",   Aig_ManNodeNum(p->pAig) );
diff --git a/src/proof/llb/llb1Group.c b/src/proof/llb/llb1Group.c
index c61f3a30..1099b2cd 100644
--- a/src/proof/llb/llb1Group.c
+++ b/src/proof/llb/llb1Group.c
@@ -95,7 +95,7 @@ void Llb_ManGroupCollect_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Ptr_t * vN
     Aig_ObjSetTravIdCurrent(pAig, pObj);
     if ( Aig_ObjIsConst1(pObj) )
         return;
-    if ( Aig_ObjIsPo(pObj) )
+    if ( Aig_ObjIsCo(pObj) )
     {
         Llb_ManGroupCollect_rec( pAig, Aig_ObjFanin0(pObj), vNodes );
         return;
@@ -180,7 +180,7 @@ Llb_Grp_t * Llb_ManGroupCreate( Llb_Man_t * pMan, Aig_Obj_t * pObj )
     p = Llb_ManGroupAlloc( pMan );
     Vec_PtrPush( p->vOuts, pObj );
     Aig_ManIncrementTravId( pMan->pAig );
-    if ( Aig_ObjIsPo(pObj) )
+    if ( Aig_ObjIsCo(pObj) )
         Llb_ManGroupCreate_rec( pMan->pAig, Aig_ObjFanin0(pObj), p->vIns );
     else
     {
diff --git a/src/proof/llb/llb1Hint.c b/src/proof/llb/llb1Hint.c
index 6e705a38..51d3a9fc 100644
--- a/src/proof/llb/llb1Hint.c
+++ b/src/proof/llb/llb1Hint.c
@@ -103,7 +103,7 @@ Vec_Int_t * Llb_ManCollectHighFanoutObjects( Aig_Man_t * pAig, int nCandMax, int
     vFanouts = Vec_IntAlloc( 100 );
     Aig_ManForEachObj( pAig, pObj, i )
     {
-//        if ( !Aig_ObjIsPi(pObj) && (fCisOnly || !Aig_ObjIsNode(pObj)) )
+//        if ( !Aig_ObjIsCi(pObj) && (fCisOnly || !Aig_ObjIsNode(pObj)) )
         if ( !Saig_ObjIsLo(pAig,pObj) && (fCisOnly || !Aig_ObjIsNode(pObj)) )
             continue;
         Vec_IntPush( vFanouts, Aig_ObjRefs(pObj) );
@@ -117,7 +117,7 @@ Vec_Int_t * Llb_ManCollectHighFanoutObjects( Aig_Man_t * pAig, int nCandMax, int
     vResult = Vec_IntAlloc( 100 );
     Aig_ManForEachObj( pAig, pObj, i )
     {
-//        if ( !Aig_ObjIsPi(pObj) && (fCisOnly || !Aig_ObjIsNode(pObj)) )
+//        if ( !Aig_ObjIsCi(pObj) && (fCisOnly || !Aig_ObjIsNode(pObj)) )
         if ( !Saig_ObjIsLo(pAig,pObj) && (fCisOnly || !Aig_ObjIsNode(pObj)) )
             continue;
         if ( Aig_ObjRefs(pObj) < PivotValue )
diff --git a/src/proof/llb/llb1Reach.c b/src/proof/llb/llb1Reach.c
index d8c667ae..60124378 100644
--- a/src/proof/llb/llb1Reach.c
+++ b/src/proof/llb/llb1Reach.c
@@ -69,7 +69,7 @@ DdNode * Llb_ManConstructOutBdd( Aig_Man_t * pAig, Aig_Obj_t * pNode, DdManager
         Cudd_RecursiveDeref( dd, (DdNode *)pObj->pData );
     }
     Vec_PtrFree( vNodes );
-    if ( Aig_ObjIsPo(pNode) )
+    if ( Aig_ObjIsCo(pNode) )
         bFunc = Cudd_NotCond( bFunc, Aig_ObjFaninC0(pNode) );
     Cudd_Deref( bFunc );
     dd->TimeStop = TimeStop;
@@ -113,7 +113,7 @@ DdNode * Llb_ManConstructGroupBdd( Llb_Man_t * p, Llb_Grp_t * pGroup )
     bRes = Cudd_ReadOne( p->dd );   Cudd_Ref( bRes );
     Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vOuts, pObj, i )
     {
-        if ( Aig_ObjIsPo(pObj) )
+        if ( Aig_ObjIsCo(pObj) )
             bBdd0 = Cudd_NotCond( Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
         else
             bBdd0 = (DdNode *)pObj->pData;
@@ -413,7 +413,7 @@ DdNode * Llb_ManCreateConstraints( Llb_Man_t * p, Vec_Int_t * vHints, int fUseNs
     if ( vHints == NULL )
         return Cudd_ReadOne( p->dd );
     TimeStop = p->dd->TimeStop; p->dd->TimeStop = 0;
-    assert( Aig_ManPiNum(p->pAig) == Aig_ManPiNum(p->pAigGlo) );
+    assert( Aig_ManCiNum(p->pAig) == Aig_ManCiNum(p->pAigGlo) );
     // assign const and PI nodes to the original AIG
     Aig_ManCleanData( p->pAig );
     Aig_ManConst1( p->pAig )->pData = Cudd_ReadOne( p->dd );
@@ -431,7 +431,7 @@ DdNode * Llb_ManCreateConstraints( Llb_Man_t * p, Vec_Int_t * vHints, int fUseNs
     Aig_ManCleanData( p->pAigGlo );
     Aig_ManConst1( p->pAigGlo )->pData = Cudd_ReadOne( p->dd );
     Aig_ManForEachCi( p->pAigGlo, pObj, i )
-        pObj->pData = Aig_ManPi(p->pAig, i)->pData;
+        pObj->pData = Aig_ManCi(p->pAig, i)->pData;
     // derive consraints
     bConstr = Cudd_ReadOne( p->dd );   Cudd_Ref( bConstr );
     Vec_IntForEachEntry( vHints, Entry, i )
@@ -595,7 +595,7 @@ int Llb_ManReachability( Llb_Man_t * p, Vec_Int_t * vHints, DdManager ** pddGlo
     assert( p->ddG == NULL );
     assert( p->ddR == NULL );
     p->dd  = Cudd_Init( Vec_IntSize(p->vVar2Obj), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
-    p->ddR = Cudd_Init( Aig_ManPiNum(p->pAig),    0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
+    p->ddR = Cudd_Init( Aig_ManCiNum(p->pAig),    0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
     if ( pddGlo && *pddGlo )
         p->ddG = *pddGlo, *pddGlo = NULL; 
     else
diff --git a/src/proof/llb/llb2Bad.c b/src/proof/llb/llb2Bad.c
index 9aecb9ff..f4359493 100644
--- a/src/proof/llb/llb2Bad.c
+++ b/src/proof/llb/llb2Bad.c
@@ -48,7 +48,7 @@ DdNode * Llb_BddComputeBad( Aig_Man_t * pInit, DdManager * dd, int TimeOut )
     DdNode * bBdd0, * bBdd1, * bTemp, * bResult;
     Aig_Obj_t * pObj;
     int i, k;
-    assert( Cudd_ReadSize(dd) == Aig_ManPiNum(pInit) );
+    assert( Cudd_ReadSize(dd) == Aig_ManCiNum(pInit) );
     // initialize elementary variables
     Aig_ManConst1(pInit)->pData = Cudd_ReadOne( dd );
     Saig_ManForEachLo( pInit, pObj, i )
@@ -56,7 +56,7 @@ DdNode * Llb_BddComputeBad( Aig_Man_t * pInit, DdManager * dd, int TimeOut )
     Saig_ManForEachPi( pInit, pObj, i )
         pObj->pData = Cudd_bddIthVar( dd, Aig_ManRegNum(pInit) + i );
     // compute internal nodes
-    vNodes = Aig_ManDfsNodes( pInit, (Aig_Obj_t **)Vec_PtrArray(pInit->vPos), Saig_ManPoNum(pInit) );
+    vNodes = Aig_ManDfsNodes( pInit, (Aig_Obj_t **)Vec_PtrArray(pInit->vCos), Saig_ManPoNum(pInit) );
     Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
     {
         if ( !Aig_ObjIsNode(pObj) )
@@ -111,7 +111,7 @@ DdNode * Llb_BddQuantifyPis( Aig_Man_t * pInit, DdManager * dd, DdNode * bFunc )
     DdNode * bVar, * bCube, * bTemp;
     Aig_Obj_t * pObj;
     int i, TimeStop;
-    assert( Cudd_ReadSize(dd) == Aig_ManPiNum(pInit) );
+    assert( Cudd_ReadSize(dd) == Aig_ManCiNum(pInit) );
     TimeStop = dd->TimeStop; dd->TimeStop = 0;
     // create PI cube
     bCube = Cudd_ReadOne( dd );  Cudd_Ref( bCube );
diff --git a/src/proof/llb/llb2Core.c b/src/proof/llb/llb2Core.c
index 626acbd2..3b98c32a 100644
--- a/src/proof/llb/llb2Core.c
+++ b/src/proof/llb/llb2Core.c
@@ -622,7 +622,7 @@ Llb_Img_t * Llb_CoreStart( Aig_Man_t * pInit, Aig_Man_t * pAig, Gia_ParLlb_t *
     p->pPars = pPars;
     p->dd    = Cudd_Init( Aig_ManObjNumMax(pAig), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
     p->ddG   = Cudd_Init( Aig_ManRegNum(pAig),    0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
-    p->ddR   = Cudd_Init( Aig_ManPiNum(pAig),     0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
+    p->ddR   = Cudd_Init( Aig_ManCiNum(pAig),     0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
     Cudd_AutodynEnable( p->dd,  CUDD_REORDER_SYMM_SIFT );
     Cudd_AutodynEnable( p->ddG, CUDD_REORDER_SYMM_SIFT );
     Cudd_AutodynEnable( p->ddR, CUDD_REORDER_SYMM_SIFT );
diff --git a/src/proof/llb/llb2Flow.c b/src/proof/llb/llb2Flow.c
index 295f0bfe..a1db70d3 100644
--- a/src/proof/llb/llb2Flow.c
+++ b/src/proof/llb/llb2Flow.c
@@ -194,7 +194,7 @@ Vec_Ptr_t * Llb_ManCutMap( Aig_Man_t * p, Vec_Ptr_t * vResult, Vec_Ptr_t * vSupp
     if ( fShowMatrix )
     Aig_ManForEachObj( p, pObj, i )
     {
-        if ( !Aig_ObjIsPi(pObj) && !Aig_ObjIsNode(pObj) )
+        if ( !Aig_ObjIsCi(pObj) && !Aig_ObjIsNode(pObj) )
             continue;
         Vec_PtrForEachEntry( Vec_Int_t *, vMaps, vMap, k )
             if ( Vec_IntEntry(vMap, i) )
@@ -276,7 +276,7 @@ int Llb_ManCutLiNum( Aig_Man_t * p, Vec_Ptr_t * vMinCut )
     int i, k, iFanout = -1, Counter = 0;
     Vec_PtrForEachEntry( Aig_Obj_t *, vMinCut, pObj, i )
     {
-        if ( Aig_ObjIsPi(pObj) )
+        if ( Aig_ObjIsCi(pObj) )
             continue;
         Aig_ObjForEachFanout( p, pObj, pFanout, iFanout, k )
         {
@@ -547,7 +547,7 @@ void Llb_ManResultPrint( Aig_Man_t * p, Vec_Ptr_t * vResult )
 int Llb_ManFlowBwdPath2_rec( Aig_Man_t * p, Aig_Obj_t * pObj )
 {
     Aig_Obj_t * pFanout;
-    assert( Aig_ObjIsNode(pObj) || Aig_ObjIsPi(pObj) || Aig_ObjIsConst1(pObj) );
+    assert( Aig_ObjIsNode(pObj) || Aig_ObjIsCi(pObj) || Aig_ObjIsConst1(pObj) );
     // skip visited nodes
     if ( Aig_ObjIsTravIdCurrent(p, pObj) )
         return 0;
@@ -607,7 +607,7 @@ void Llb_ManFlowLabelTfi_rec( Aig_Man_t * p, Aig_Obj_t * pObj )
     if ( Aig_ObjIsTravIdCurrent(p, pObj) )
         return;
     Aig_ObjSetTravIdCurrent(p, pObj);
-    if ( Aig_ObjIsPi(pObj) || Aig_ObjIsConst1(pObj) )
+    if ( Aig_ObjIsCi(pObj) || Aig_ObjIsConst1(pObj) )
         return;
     assert( Aig_ObjIsNode(pObj) );
     Llb_ManFlowLabelTfi_rec( p, Aig_ObjFanin0(pObj) );
@@ -638,7 +638,7 @@ void Llb_ManFlowUpdateCut( Aig_Man_t * p, Vec_Ptr_t * vMinCut )
     Aig_ManIncrementTravId(p);
     Aig_ManForEachObj( p, pObj, i )
     {
-        if ( !Aig_ObjIsPo(pObj) && !Aig_ObjIsNode(pObj) )
+        if ( !Aig_ObjIsCo(pObj) && !Aig_ObjIsNode(pObj) )
             continue;
         if ( Aig_ObjIsTravIdCurrent(p, pObj) || Aig_ObjIsTravIdPrevious(p, pObj) )
             continue;
@@ -708,7 +708,7 @@ int Llb_ManFlowVerifyCut_rec( Aig_Man_t * p, Aig_Obj_t * pObj )
     // visit the node
     if ( Aig_ObjIsConst1(pObj) )
         return 1;
-    if ( Aig_ObjIsPi(pObj) )
+    if ( Aig_ObjIsCi(pObj) )
         return 0;
     // explore the fanins
     assert( Aig_ObjIsNode(pObj) );
@@ -930,7 +930,7 @@ void Llb_ManFlowSetMarkA_rec( Aig_Obj_t * pObj )
     if ( pObj->fMarkA )
         return;
     pObj->fMarkA = 1;
-    if ( Aig_ObjIsPi(pObj) || Aig_ObjIsConst1(pObj) )
+    if ( Aig_ObjIsCi(pObj) || Aig_ObjIsConst1(pObj) )
         return;
     assert( Aig_ObjIsNode(pObj) );
     Llb_ManFlowSetMarkA_rec( Aig_ObjFanin0(pObj) );
diff --git a/src/proof/llb/llb3Nonlin.c b/src/proof/llb/llb3Nonlin.c
index 678a6fff..38d9b8ae 100644
--- a/src/proof/llb/llb3Nonlin.c
+++ b/src/proof/llb/llb3Nonlin.c
@@ -705,17 +705,17 @@ Llb_Mnn_t * Llb_MnnStart( Aig_Man_t * pInit, Aig_Man_t * pAig, Gia_ParLlb_t *  p
     p->pPars = pPars;
     p->dd    = Cudd_Init( Aig_ManObjNumMax(pAig), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
     p->ddG   = Cudd_Init( Aig_ManRegNum(pAig),    0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
-    p->ddR   = Cudd_Init( Aig_ManPiNum(pAig),     0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
+    p->ddR   = Cudd_Init( Aig_ManCiNum(pAig),     0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
     Cudd_AutodynEnable( p->dd,  CUDD_REORDER_SYMM_SIFT );
     Cudd_AutodynEnable( p->ddG, CUDD_REORDER_SYMM_SIFT );
     Cudd_AutodynEnable( p->ddR, CUDD_REORDER_SYMM_SIFT );
     p->vRings = Vec_PtrAlloc( 100 );
     // create leaves
-    p->vLeaves = Vec_PtrAlloc( Aig_ManPiNum(pAig) );
+    p->vLeaves = Vec_PtrAlloc( Aig_ManCiNum(pAig) );
     Aig_ManForEachCi( pAig, pObj, i )
         Vec_PtrPush( p->vLeaves, pObj );
     // create roots
-    p->vRoots = Vec_PtrAlloc( Aig_ManPoNum(pAig) );
+    p->vRoots = Vec_PtrAlloc( Aig_ManCoNum(pAig) );
     Saig_ManForEachLi( pAig, pObj, i )
         Vec_PtrPush( p->vRoots, pObj );
     // variables to quantify
diff --git a/src/proof/llb/llb4Cex.c b/src/proof/llb/llb4Cex.c
index 69ba6ab1..b5bdb36e 100644
--- a/src/proof/llb/llb4Cex.c
+++ b/src/proof/llb/llb4Cex.c
@@ -63,7 +63,7 @@ Abc_Cex_t * Llb4_Nonlin4TransformCex( Aig_Man_t * pAig, Vec_Ptr_t * vStates, int
 */
     // derive SAT solver
     nRegs = Aig_ManRegNum(pAig); pAig->nRegs = 0;
-    pCnf = Cnf_Derive( pAig, Aig_ManPoNum(pAig) );
+    pCnf = Cnf_Derive( pAig, Aig_ManCoNum(pAig) );
     pAig->nRegs = nRegs;
 //    Cnf_DataTranformPolarity( pCnf, 0 );
     // convert into SAT solver
@@ -249,11 +249,11 @@ Vec_Ptr_t * Llb4_Nonlin4VerifyCex( Aig_Man_t * pAig, Abc_Cex_t * p )
     }
 */
     assert( iBit == p->nBits );
-//    if ( Aig_ManPo(pAig, p->iPo)->fMarkB == 0 )
+//    if ( Aig_ManCo(pAig, p->iPo)->fMarkB == 0 )
 //        Vec_PtrFreeP( &vStates );
     for ( i = Saig_ManPoNum(pAig) - 1; i >= 0; i-- )
     {
-        if ( Aig_ManPo(pAig, i)->fMarkB )
+        if ( Aig_ManCo(pAig, i)->fMarkB )
         {
             p->iPo = i;
             break;
diff --git a/src/proof/llb/llb4Cluster.c b/src/proof/llb/llb4Cluster.c
index c151a618..7e325597 100644
--- a/src/proof/llb/llb4Cluster.c
+++ b/src/proof/llb/llb4Cluster.c
@@ -49,7 +49,7 @@ void Llb_Nonlin4FindOrder_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Int_t * v
         return;
     Aig_ObjSetTravIdCurrent( pAig, pObj );
     assert( Llb_ObjBddVar(vOrder, pObj) < 0 );
-    if ( Aig_ObjIsPi(pObj) )
+    if ( Aig_ObjIsCi(pObj) )
     {
         Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), (*pCounter)++ );
         return;
@@ -152,11 +152,11 @@ DdNode * Llb_Nonlin4FindPartitions_rec( DdManager * dd, Aig_Obj_t * pObj, Vec_In
     DdNode * bBdd, * bBdd0, * bBdd1, * bPart, * vVar;
     if ( Aig_ObjIsConst1(pObj) )
         return Cudd_ReadOne(dd); 
-    if ( Aig_ObjIsPi(pObj) )
+    if ( Aig_ObjIsCi(pObj) )
         return Cudd_bddIthVar( dd, Llb_ObjBddVar(vOrder, pObj) );
     if ( pObj->pData )
         return (DdNode *)pObj->pData;
-    if ( Aig_ObjIsPo(pObj) )
+    if ( Aig_ObjIsCo(pObj) )
     {
         bBdd0 = Cudd_NotCond( Llb_Nonlin4FindPartitions_rec(dd, Aig_ObjFanin0(pObj), vOrder, vRoots), Aig_ObjFaninC0(pObj) );
         bPart = Cudd_bddXnor( dd, Cudd_bddIthVar( dd, Llb_ObjBddVar(vOrder, pObj) ), bBdd0 );  Cudd_Ref( bPart );
diff --git a/src/proof/llb/llb4Nonlin.c b/src/proof/llb/llb4Nonlin.c
index 31f94acf..af8dad75 100644
--- a/src/proof/llb/llb4Nonlin.c
+++ b/src/proof/llb/llb4Nonlin.c
@@ -84,7 +84,7 @@ DdNode * Llb_Nonlin4ComputeBad( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * vO
     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) );
+    vNodes = Aig_ManDfsNodes( pAig, (Aig_Obj_t **)Vec_PtrArray(pAig->vCos), Saig_ManPoNum(pAig) );
     Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
     {
         if ( !Aig_ObjIsNode(pObj) )
@@ -273,7 +273,7 @@ void Llb_Nonlin4CreateOrder_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Int_t *
         return;
     Aig_ObjSetTravIdCurrent( pAig, pObj );
     assert( Llb_ObjBddVar(vOrder, pObj) < 0 );
-    if ( Aig_ObjIsPi(pObj) )
+    if ( Aig_ObjIsCi(pObj) )
     {
 //        if ( Saig_ObjIsLo(pAig, pObj) )
 //            Vec_IntWriteEntry( vOrder, Aig_ObjId(Saig_ObjLoToLi(pAig, pObj)), (*pCounter)++ );
@@ -371,7 +371,7 @@ printf( "Techmapping added %d pivots.\n", Vec_IntSize(vNodes) );
 //                Vec_IntWriteEntry( vOrder, Aig_ObjId(Saig_ObjLoToLi(pAig, pObj)), Counter++ );
             Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), Counter++ );
         }
-    assert( Counter <= Aig_ManPiNum(pAig) + Aig_ManRegNum(pAig) + (vNodes?Vec_IntSize(vNodes):0) );
+    assert( Counter <= Aig_ManCiNum(pAig) + Aig_ManRegNum(pAig) + (vNodes?Vec_IntSize(vNodes):0) );
     Aig_ManCleanMarkA( pAig );
     Vec_IntFreeP( &vNodes );
     return vOrder;
diff --git a/src/proof/llb/llb4Sweep.c b/src/proof/llb/llb4Sweep.c
index 292fb176..6b223ab9 100644
--- a/src/proof/llb/llb4Sweep.c
+++ b/src/proof/llb/llb4Sweep.c
@@ -49,7 +49,7 @@ void Llb_Nonlin4SweepOrder_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Int_t *
         return;
     Aig_ObjSetTravIdCurrent( pAig, pObj );
     assert( Llb_ObjBddVar(vOrder, pObj) < 0 );
-    if ( Aig_ObjIsPi(pObj) )
+    if ( Aig_ObjIsCi(pObj) )
     {
         Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), (*pCounter)++ );
         return;
@@ -102,7 +102,7 @@ Vec_Int_t * Llb_Nonlin4SweepOrder( Aig_Man_t * pAig, int * pCounter, int fSaveAl
             Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), Counter++ );
 //    assert( Counter == Aig_ManObjNum(pAig) - 1 ); // no dangling nodes
     if ( pCounter )
-        *pCounter = Counter - Aig_ManPiNum(pAig) - Aig_ManPoNum(pAig);
+        *pCounter = Counter - Aig_ManCiNum(pAig) - Aig_ManCoNum(pAig);
     return vOrder;
 }
 
@@ -211,11 +211,11 @@ DdNode * Llb_Nonlin4SweepPartitions_rec( DdManager * dd, Aig_Obj_t * pObj, Vec_I
     DdNode * bBdd, * bBdd0, * bBdd1, * bPart, * vVar;
     if ( Aig_ObjIsConst1(pObj) )
         return Cudd_ReadOne(dd); 
-    if ( Aig_ObjIsPi(pObj) )
+    if ( Aig_ObjIsCi(pObj) )
         return Cudd_bddIthVar( dd, Llb_ObjBddVar(vOrder, pObj) );
     if ( pObj->pData )
         return (DdNode *)pObj->pData;
-    if ( Aig_ObjIsPo(pObj) )
+    if ( Aig_ObjIsCo(pObj) )
     {
         bBdd0 = Cudd_NotCond( Llb_Nonlin4SweepPartitions_rec(dd, Aig_ObjFanin0(pObj), vOrder, vRoots), Aig_ObjFaninC0(pObj) );
         bPart = Cudd_bddXnor( dd, Cudd_bddIthVar( dd, Llb_ObjBddVar(vOrder, pObj) ), bBdd0 );  Cudd_Ref( bPart );
@@ -535,9 +535,9 @@ void Llb4_Nonlin4Sweep( Aig_Man_t * pAig, int nSweepMax, int nClusterMax, DdMana
     assert( Counter == nCutPoints );
     Aig_ManCleanMarkA( pAig );
     // compute the BAD states
-    ddBad = Llb4_Nonlin4SweepBadStates( pAig, vOrder, nCutPoints + Aig_ManPiNum(pAig) + Aig_ManPoNum(pAig) );
+    ddBad = Llb4_Nonlin4SweepBadStates( pAig, vOrder, nCutPoints + Aig_ManCiNum(pAig) + Aig_ManCoNum(pAig) );
     // compute the clusters
-    ddWork = Llb4_Nonlin4SweepGroups( pAig, vOrder, nCutPoints + Aig_ManPiNum(pAig) + Aig_ManPoNum(pAig), &vGroups, nClusterMax, fVerbose );
+    ddWork = Llb4_Nonlin4SweepGroups( pAig, vOrder, nCutPoints + Aig_ManCiNum(pAig) + Aig_ManCoNum(pAig), &vGroups, nClusterMax, fVerbose );
     // transfer the result from the Bad manager
 //printf( "Bad before = %d.\n", Cudd_DagSize(ddBad->bFunc) );
     ddWork->bFunc = Cudd_bddTransfer( ddBad, ddWork, ddBad->bFunc );   Cudd_Ref( ddWork->bFunc );
diff --git a/src/proof/pdr/pdrClass.c b/src/proof/pdr/pdrClass.c
index cbe5e1c2..5dd4c4a9 100644
--- a/src/proof/pdr/pdrClass.c
+++ b/src/proof/pdr/pdrClass.c
@@ -202,7 +202,7 @@ void Pdr_ManEquivClasses( Aig_Man_t * pAig )
         // report the result
         Abc_Print( 1, "F =%4d : Total = %6d. Nodes = %6d. RedRegs = %6d. Prop = %s\n", 
             f+1, Aig_ManNodeNum(pAig), Aig_ManNodeNum(pTemp), Pdr_ManCountMap(vMap), 
-            Aig_ObjChild0(Aig_ManPo(pTemp,0)) == Aig_ManConst0(pTemp) ? "proof" : "unknown" );
+            Aig_ObjChild0(Aig_ManCo(pTemp,0)) == Aig_ManConst0(pTemp) ? "proof" : "unknown" );
         // recreate the map
         Pdr_ManPrintMap( vMap );
         Vec_IntFree( vMap );
diff --git a/src/proof/pdr/pdrCnf.c b/src/proof/pdr/pdrCnf.c
index fddd292b..fcad15e0 100644
--- a/src/proof/pdr/pdrCnf.c
+++ b/src/proof/pdr/pdrCnf.c
@@ -114,7 +114,7 @@ int Pdr_ObjSatVar2( Pdr_Man_t * p, int k, Aig_Obj_t * pObj )
     if ( nVarCount == Vec_IntSize(vVar2Ids) )
         return iVarThis;
     assert( nVarCount + 1 == Vec_IntSize(vVar2Ids) );
-    if ( Aig_ObjIsPi(pObj) )
+    if ( Aig_ObjIsCi(pObj) )
         return iVarThis;
     nClauses = p->pCnf2->pObj2Count[Aig_ObjId(pObj)];
     iFirstClause = p->pCnf2->pObj2Clause[Aig_ObjId(pObj)];
@@ -269,8 +269,8 @@ static inline sat_solver * Pdr_ManNewSolver1( sat_solver * pSat, Pdr_Man_t * p,
     if ( p->pCnf1 == NULL )
     {
         int nRegs = p->pAig->nRegs;
-        p->pAig->nRegs = Aig_ManPoNum(p->pAig);
-        p->pCnf1 = Cnf_Derive( p->pAig, Aig_ManPoNum(p->pAig) );
+        p->pAig->nRegs = Aig_ManCoNum(p->pAig);
+        p->pCnf1 = Cnf_Derive( p->pAig, Aig_ManCoNum(p->pAig) );
         p->pAig->nRegs = nRegs;
         assert( p->vVar2Reg == NULL );
         p->vVar2Reg = Vec_IntStartFull( p->pCnf1->nVars );
diff --git a/src/proof/pdr/pdrSat.c b/src/proof/pdr/pdrSat.c
index c191654a..de661905 100644
--- a/src/proof/pdr/pdrSat.c
+++ b/src/proof/pdr/pdrSat.c
@@ -55,7 +55,7 @@ sat_solver * Pdr_ManCreateSolver( Pdr_Man_t * p, int k )
     Vec_VecExpand( p->vClauses, k );
     Vec_IntPush( p->vActVars, 0 );
     // add property cone
-    Pdr_ObjSatVar( p, k, Aig_ManPo(p->pAig, (p->pPars->iOutput==-1)?0:p->pPars->iOutput ) );
+    Pdr_ObjSatVar( p, k, Aig_ManCo(p->pAig, (p->pPars->iOutput==-1)?0:p->pPars->iOutput ) );
     return pSat;
 }
 
@@ -175,7 +175,7 @@ void Pdr_ManSetPropertyOutput( Pdr_Man_t * p, int k )
     sat_solver * pSat;
     int Lit, RetValue;
     pSat = Pdr_ManSolver(p, k);
-    Lit = toLitCond( Pdr_ObjSatVar(p, k, Aig_ManPo(p->pAig, (p->pPars->iOutput==-1)?0:p->pPars->iOutput)), 1 ); // neg literal
+    Lit = toLitCond( Pdr_ObjSatVar(p, k, Aig_ManCo(p->pAig, (p->pPars->iOutput==-1)?0:p->pPars->iOutput)), 1 ); // neg literal
     RetValue = sat_solver_addclause( pSat, &Lit, &Lit + 1 );
     assert( RetValue == 1 );
     sat_solver_compress( pSat );
@@ -278,7 +278,7 @@ int Pdr_ManCheckCube( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPr
     if ( pCube == NULL ) // solve the property
     {
         clk = clock();
-        Lit = toLit( Pdr_ObjSatVar(p, k, Aig_ManPo(p->pAig, (p->pPars->iOutput==-1)?0:p->pPars->iOutput)) ); // pos literal (property fails)
+        Lit = toLit( Pdr_ObjSatVar(p, k, Aig_ManCo(p->pAig, (p->pPars->iOutput==-1)?0:p->pPars->iOutput)) ); // pos literal (property fails)
         RetValue = sat_solver_solve( pSat, &Lit, &Lit + 1, nConfLimit, 0, 0, 0 );
         if ( RetValue == l_Undef )
             return -1;
diff --git a/src/proof/pdr/pdrTsim.c b/src/proof/pdr/pdrTsim.c
index 428c20c7..0547c308 100644
--- a/src/proof/pdr/pdrTsim.c
+++ b/src/proof/pdr/pdrTsim.c
@@ -81,13 +81,13 @@ void Pdr_ManCollectCone_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Int_t * vCi
     if ( Aig_ObjIsTravIdCurrent(pAig, pObj) )
         return;
     Aig_ObjSetTravIdCurrent(pAig, pObj);
-    if ( Aig_ObjIsPi(pObj) )
+    if ( Aig_ObjIsCi(pObj) )
     {
         Vec_IntPush( vCiObjs, Aig_ObjId(pObj) );
         return;
     }
     Pdr_ManCollectCone_rec( pAig, Aig_ObjFanin0(pObj), vCiObjs, vNodes );
-    if ( Aig_ObjIsPo(pObj) )
+    if ( Aig_ObjIsCo(pObj) )
         return;
     Pdr_ManCollectCone_rec( pAig, Aig_ObjFanin1(pObj), vCiObjs, vNodes );
     Vec_IntPush( vNodes, Aig_ObjId(pObj) );
@@ -133,7 +133,7 @@ int Pdr_ManExtendOneEval( Aig_Man_t * pAig, Aig_Obj_t * pObj )
     Value0 = Pdr_ManSimInfoGet( pAig, Aig_ObjFanin0(pObj) );
     if ( Aig_ObjFaninC0(pObj) )
         Value0 = Pdr_ManSimInfoNot( Value0 );
-    if ( Aig_ObjIsPo(pObj) )
+    if ( Aig_ObjIsCo(pObj) )
     {
         Pdr_ManSimInfoSet( pAig, pObj, Value0 );
         return Value0;
@@ -228,7 +228,7 @@ int Pdr_ManExtendOne( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Int_t * vUndo, Vec
             assert( Value2 == PDR_UND );
             Vec_IntPush( vUndo, Aig_ObjId(pFanout) );
             Vec_IntPush( vUndo, Value );
-            if ( Aig_ObjIsPo(pFanout) )
+            if ( Aig_ObjIsCo(pFanout) )
                 return 0;
             assert( Aig_ObjIsNode(pFanout) );
             Vec_IntPushOrder( vVis, Aig_ObjId(pFanout) );
@@ -318,8 +318,8 @@ void Pdr_ManPrintCex( Aig_Man_t * pAig, Vec_Int_t * vCiObjs, Vec_Int_t * vCiVals
 {
     Aig_Obj_t * pObj;
     int i;
-    char * pBuff = ABC_ALLOC( char, Aig_ManPiNum(pAig)+1 );
-    for ( i = 0; i < Aig_ManPiNum(pAig); i++ )
+    char * pBuff = ABC_ALLOC( char, Aig_ManCiNum(pAig)+1 );
+    for ( i = 0; i < Aig_ManCiNum(pAig); i++ )
         pBuff[i] = '-';
     pBuff[i] = 0;
     Aig_ManForEachObjVec( vCiObjs, pAig, pObj, i )
@@ -368,7 +368,7 @@ Pdr_Set_t * Pdr_ManTernarySim( Pdr_Man_t * p, int k, Pdr_Set_t * pCube )
     // collect CO objects
     Vec_IntClear( vCoObjs );
     if ( pCube == NULL ) // the target is the property output
-        Vec_IntPush( vCoObjs, Aig_ObjId(Aig_ManPo(p->pAig, (p->pPars->iOutput==-1)?0:p->pPars->iOutput)) ); 
+        Vec_IntPush( vCoObjs, Aig_ObjId(Aig_ManCo(p->pAig, (p->pPars->iOutput==-1)?0:p->pPars->iOutput)) ); 
     else // the target is the cube
     {
         for ( i = 0; i < pCube->nLits; i++ )
diff --git a/src/proof/pdr/pdrUtil.c b/src/proof/pdr/pdrUtil.c
index 97261a7f..9a2cffb2 100644
--- a/src/proof/pdr/pdrUtil.c
+++ b/src/proof/pdr/pdrUtil.c
@@ -613,7 +613,7 @@ int Pdr_NtkFindSatAssign_rec( Aig_Man_t * pAig, Aig_Obj_t * pNode, int Value, Pd
         return ((int)pNode->fMarkA == Value);
     Aig_ObjSetTravIdCurrent(pAig, pNode);
     pNode->fMarkA = Value;
-    if ( Aig_ObjIsPi(pNode) )
+    if ( Aig_ObjIsCi(pNode) )
     {
 //        if ( vSuppLits )
 //            Vec_IntPush( vSuppLits, Abc_Var2Lit( Aig_ObjPioNum(pNode), !Value ) );
diff --git a/src/proof/ssw/sswAig.c b/src/proof/ssw/sswAig.c
index 5cdced62..cd0f0c7a 100644
--- a/src/proof/ssw/sswAig.c
+++ b/src/proof/ssw/sswAig.c
@@ -148,7 +148,7 @@ Aig_Man_t * Ssw_FramesWithClasses( Ssw_Man_t * p )
     int i, f, iLits;
     assert( p->pFrames == NULL );
     assert( Aig_ManRegNum(p->pAig) > 0 );
-    assert( Aig_ManRegNum(p->pAig) < Aig_ManPiNum(p->pAig) );
+    assert( Aig_ManRegNum(p->pAig) < Aig_ManCiNum(p->pAig) );
     p->nConstrTotal = p->nConstrReduced = 0;
 
     // start the fraig package
@@ -216,7 +216,7 @@ Aig_Man_t * Ssw_SpeculativeReduction( Ssw_Man_t * p )
     int i;
     assert( p->pFrames == NULL );
     assert( Aig_ManRegNum(p->pAig) > 0 );
-    assert( Aig_ManRegNum(p->pAig) < Aig_ManPiNum(p->pAig) );
+    assert( Aig_ManRegNum(p->pAig) < Aig_ManCiNum(p->pAig) );
     p->nConstrTotal = p->nConstrReduced = 0;
  
     // start the fraig package
diff --git a/src/proof/ssw/sswBmc.c b/src/proof/ssw/sswBmc.c
index 0eabaa92..b2920177 100644
--- a/src/proof/ssw/sswBmc.c
+++ b/src/proof/ssw/sswBmc.c
@@ -51,7 +51,7 @@ Aig_Obj_t * Ssw_BmcUnroll_rec( Ssw_Frm_t * pFrm, Aig_Obj_t * pObj, int f )
         pRes = Aig_ManConst1( pFrm->pFrames );
     else if ( Saig_ObjIsPi(pFrm->pAig, pObj) )
         pRes = Aig_ObjCreateCi( pFrm->pFrames );
-    else if ( Aig_ObjIsPo(pObj) )
+    else if ( Aig_ObjIsCo(pObj) )
     {
         Ssw_BmcUnroll_rec( pFrm, Aig_ObjFanin0(pObj), f );
         pRes = Ssw_ObjChild0Fra_( pFrm, pObj, f );
diff --git a/src/proof/ssw/sswClass.c b/src/proof/ssw/sswClass.c
index 95f029d4..581b8aed 100644
--- a/src/proof/ssw/sswClass.c
+++ b/src/proof/ssw/sswClass.c
@@ -642,7 +642,7 @@ clk = clock();
         }
         else
         {
-            if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
+            if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsCi(pObj) )
                 continue;
             // skip the node with more that the given number of levels
             if ( nMaxLevs && (int)pObj->Level > nMaxLevs )
diff --git a/src/proof/ssw/sswCnf.c b/src/proof/ssw/sswCnf.c
index 1970c62f..e3b422d5 100644
--- a/src/proof/ssw/sswCnf.c
+++ b/src/proof/ssw/sswCnf.c
@@ -276,7 +276,7 @@ void Ssw_AddClausesSuper( Ssw_Sat_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vSuper )
 void Ssw_CollectSuper_rec( Aig_Obj_t * pObj, Vec_Ptr_t * vSuper, int fFirst, int fUseMuxes )
 {
     // if the new node is complemented or a PI, another gate begins
-    if ( Aig_IsComplement(pObj) || Aig_ObjIsPi(pObj) || 
+    if ( Aig_IsComplement(pObj) || Aig_ObjIsCi(pObj) || 
          (!fFirst && Aig_ObjRefs(pObj) > 1) || 
          (fUseMuxes && Aig_ObjIsMuxType(pObj)) )
     {
@@ -303,7 +303,7 @@ void Ssw_CollectSuper_rec( Aig_Obj_t * pObj, Vec_Ptr_t * vSuper, int fFirst, int
 void Ssw_CollectSuper( Aig_Obj_t * pObj, int fUseMuxes, Vec_Ptr_t * vSuper )
 {
     assert( !Aig_IsComplement(pObj) );
-    assert( !Aig_ObjIsPi(pObj) );
+    assert( !Aig_ObjIsCi(pObj) );
     Vec_PtrClear( vSuper );
     Ssw_CollectSuper_rec( pObj, vSuper, 1, fUseMuxes );
 }
@@ -329,7 +329,7 @@ void Ssw_ObjAddToFrontier( Ssw_Sat_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vFrontie
         return;
 //    pObj->fMarkA = 1;
     // save PIs (used by register correspondence)
-    if ( Aig_ObjIsPi(pObj) )
+    if ( Aig_ObjIsCi(pObj) )
         Vec_PtrPush( p->vUsedPis, pObj );
     Ssw_ObjSetSatNum( p, pObj, p->nSatVars++ );
     sat_solver_setnvars( p->pSat, 100 * (1 + p->nSatVars / 100) );
@@ -408,7 +408,7 @@ int Ssw_CnfGetNodeValue( Ssw_Sat_t * p, Aig_Obj_t * pObj )
         return sat_solver_var_value( p->pSat, nVarNum );
 //    if ( pObj->fMarkA == 1 )
 //        return 0;
-    if ( Aig_ObjIsPi(pObj) )
+    if ( Aig_ObjIsCi(pObj) )
         return 0;
     assert( Aig_ObjIsNode(pObj) );
     Value0 = Ssw_CnfGetNodeValue( p, Aig_ObjFanin0(pObj) );
diff --git a/src/proof/ssw/sswConstr.c b/src/proof/ssw/sswConstr.c
index 6d8a152d..82977edb 100644
--- a/src/proof/ssw/sswConstr.c
+++ b/src/proof/ssw/sswConstr.c
@@ -51,7 +51,7 @@ Aig_Man_t * Ssw_FramesWithConstraints( Aig_Man_t * p, int nFrames )
     int i, f;
     assert( Saig_ManConstrNum(p) > 0 );
     assert( Aig_ManRegNum(p) > 0 );
-    assert( Aig_ManRegNum(p) < Aig_ManPiNum(p) );
+    assert( Aig_ManRegNum(p) < Aig_ManCiNum(p) );
     // start the fraig package
     pFrames = Aig_ManStart( Aig_ManObjNumMax(p) * nFrames );
     // create latches for the first frame
@@ -165,7 +165,7 @@ int Ssw_ManSetConstrPhases_( Aig_Man_t * p, int nFrames, Vec_Int_t ** pvInits )
     assert( p->nConstrs > 0 );
     // create CNF
     nRegs = p->nRegs; p->nRegs = 0;
-    pCnf = Cnf_Derive( p, Aig_ManPoNum(p) );  
+    pCnf = Cnf_Derive( p, Aig_ManCoNum(p) );  
     p->nRegs = nRegs;  
     // create SAT solver
     pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, nFrames, 0 );
@@ -626,18 +626,18 @@ clk = clock();
     // create timeframes
     p->pFrames = Ssw_FramesWithClasses( p );
     // add constants
-    nConstrPairs = Aig_ManPoNum(p->pFrames)-Aig_ManRegNum(p->pAig);
+    nConstrPairs = Aig_ManCoNum(p->pFrames)-Aig_ManRegNum(p->pAig);
     assert( (nConstrPairs & 1) == 0 );
     for ( i = 0; i < nConstrPairs; i += 2 )
     {
-        pObj  = Aig_ManPo( p->pFrames, i   );
-        pObj2 = Aig_ManPo( p->pFrames, i+1 );
+        pObj  = Aig_ManCo( p->pFrames, i   );
+        pObj2 = Aig_ManCo( p->pFrames, i+1 );
         Ssw_NodesAreConstrained( p, Aig_ObjChild0(pObj), Aig_ObjChild0(pObj2) );
     }
     // build logic cones for register inputs
     for ( i = 0; i < Aig_ManRegNum(p->pAig); i++ )
     {
-        pObj  = Aig_ManPo( p->pFrames, nConstrPairs + i );
+        pObj  = Aig_ManCo( p->pFrames, nConstrPairs + i );
         Ssw_CnfNodeAddToSolver( p->pMSat, Aig_ObjFanin0(pObj) );//
     }
 
diff --git a/src/proof/ssw/sswCore.c b/src/proof/ssw/sswCore.c
index df48a5b8..c51d421c 100644
--- a/src/proof/ssw/sswCore.c
+++ b/src/proof/ssw/sswCore.c
@@ -191,13 +191,13 @@ void Ssw_ManUpdateEquivs( Ssw_Man_t * p, Aig_Man_t * pAig, int fVerbose )
     Aig_Obj_t * pObj;
     int i, nTotal = 0, nRemoved = 0;
     // collect the nodes in the cone of constraints
-    pArray  = (Aig_Obj_t **)Vec_PtrArray(pAig->vPos);
+    pArray  = (Aig_Obj_t **)Vec_PtrArray(pAig->vCos);
     pArray += Saig_ManPoNum(pAig) - Saig_ManConstrNum(pAig);
     vCones  = Aig_ManDfsNodes( pAig, pArray, Saig_ManConstrNum(pAig) );
     // remove all the node that are equiv to something and are in the cones
     Aig_ManForEachObj( pAig, pObj, i )
     {
-        if ( !Aig_ObjIsPi(pObj) && !Aig_ObjIsNode(pObj) )
+        if ( !Aig_ObjIsCi(pObj) && !Aig_ObjIsNode(pObj) )
             continue;
         if ( pAig->pReprs[i] != NULL )
             nTotal++;
@@ -213,7 +213,7 @@ void Ssw_ManUpdateEquivs( Ssw_Man_t * p, Aig_Man_t * pAig, int fVerbose )
         }
     }
     // collect statistics    
-    p->nConesTotal   = Aig_ManPiNum(pAig) + Aig_ManNodeNum(pAig);
+    p->nConesTotal   = Aig_ManCiNum(pAig) + Aig_ManNodeNum(pAig);
     p->nConesConstr  = Vec_PtrSize(vCones);
     p->nEquivsTotal  = nTotal;
     p->nEquivsConstr = nRemoved;
@@ -341,7 +341,7 @@ clk = clock();
                     printf( "R =%4d. ",   p->nRecycles-nRecycles );
                 }
                 printf( "F =%5d. %s ", p->nSatFailsReal-nSatFailsReal, 
-                    (Saig_ManPoNum(p->pAig)==1 && Ssw_ObjIsConst1Cand(p->pAig,Aig_ObjFanin0(Aig_ManPo(p->pAig,0))))? "+" : "-" );
+                    (Saig_ManPoNum(p->pAig)==1 && Ssw_ObjIsConst1Cand(p->pAig,Aig_ObjFanin0(Aig_ManCo(p->pAig,0))))? "+" : "-" );
                 ABC_PRT( "T", clock() - clk );
             } 
 //            if ( p->pPars->fDynamic && p->nSatCallsSat-nSatCallsSat < 100 )
diff --git a/src/proof/ssw/sswDyn.c b/src/proof/ssw/sswDyn.c
index 0f6002fa..f20a7b78 100644
--- a/src/proof/ssw/sswDyn.c
+++ b/src/proof/ssw/sswDyn.c
@@ -54,7 +54,7 @@ void Ssw_ManLabelPiNodes( Ssw_Man_t * p )
         Saig_ManForEachPi( p->pAig, pObj, i )
         {
             pObjFrames = Ssw_ObjFrame( p, pObj, f );
-            assert( Aig_ObjIsPi(pObjFrames) );
+            assert( Aig_ObjIsCi(pObjFrames) );
             assert( pObjFrames->fMarkB == 0 );
             pObjFrames->fMarkA = 1;
             pObjFrames->fMarkB = 1;
@@ -79,7 +79,7 @@ void Ssw_ManCollectPis_rec( Aig_Obj_t * pObj, Vec_Ptr_t * vNewPis )
     if ( pObj->fMarkA )
         return;
     pObj->fMarkA = 1;
-    if ( Aig_ObjIsPi(pObj) )
+    if ( Aig_ObjIsCi(pObj) )
     {
         Vec_PtrPush( vNewPis, pObj );
         return;
@@ -110,10 +110,10 @@ void Ssw_ManCollectPos_rec( Ssw_Man_t * p, Aig_Obj_t * pObj, Vec_Int_t * vNewPos
     pObj->fMarkB = 1;
     if ( pObj->Id > p->nSRMiterMaxId )
         return;
-    if ( Aig_ObjIsPo(pObj) )
+    if ( Aig_ObjIsCo(pObj) )
     {
         // skip if it is a register input PO
-        if ( Aig_ObjPioNum(pObj) >= Aig_ManPoNum(p->pFrames)-Aig_ManRegNum(p->pAig) )
+        if ( Aig_ObjPioNum(pObj) >= Aig_ManCoNum(p->pFrames)-Aig_ManRegNum(p->pAig) )
             return;
         // add the number of this constraint
         Vec_IntPush( vNewPos, Aig_ObjPioNum(pObj)/2 );
@@ -180,8 +180,8 @@ void Ssw_ManLoadSolver( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pObj )
     // check if the corresponding pairs are added
     Vec_IntForEachEntry( p->vNewPos, iConstr, i )
     {
-        pObj0 = Aig_ManPo( p->pFrames, 2*iConstr   );
-        pObj1 = Aig_ManPo( p->pFrames, 2*iConstr+1 );
+        pObj0 = Aig_ManCo( p->pFrames, 2*iConstr   );
+        pObj1 = Aig_ManCo( p->pFrames, 2*iConstr+1 );
 //        if ( pObj0->fMarkB && pObj1->fMarkB )
         if ( pObj0->fMarkB || pObj1->fMarkB )
         {
@@ -224,7 +224,7 @@ void Ssw_ManSweepTransferDyn( Ssw_Man_t * p )
             continue;
         }
         assert( !Aig_IsComplement(pObjFraig) );
-        assert( Aig_ObjIsPi(pObjFraig) );
+        assert( Aig_ObjIsCi(pObjFraig) );
         pInfo = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjPioNum(pObjFraig) );
         Ssw_SmlObjSetWord( p->pSml, pObj, pInfo[0], 0, 0 );
     }
@@ -235,7 +235,7 @@ void Ssw_ManSweepTransferDyn( Ssw_Man_t * p )
         {
             pObjFraig = Ssw_ObjFrame( p, pObj, f );
             assert( !Aig_IsComplement(pObjFraig) );
-            assert( Aig_ObjIsPi(pObjFraig) );
+            assert( Aig_ObjIsCi(pObjFraig) );
             pInfo = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjPioNum(pObjFraig) );
             Ssw_SmlObjSetWord( p->pSml, pObj, pInfo[0], 0, f );
         }
@@ -393,7 +393,7 @@ p->timeReduce += clock() - clk;
 
     // prepare simulation info
     assert( p->vSimInfo == NULL );
-    p->vSimInfo = Vec_PtrAllocSimInfo( Aig_ManPiNum(p->pFrames), 1 );
+    p->vSimInfo = Vec_PtrAllocSimInfo( Aig_ManCiNum(p->pFrames), 1 );
     Vec_PtrCleanSimInfo( p->vSimInfo, 0, 1 );
 
     // sweep internal nodes
diff --git a/src/proof/ssw/sswFilter.c b/src/proof/ssw/sswFilter.c
index 536316ff..5f467123 100644
--- a/src/proof/ssw/sswFilter.c
+++ b/src/proof/ssw/sswFilter.c
@@ -162,7 +162,7 @@ void Ssw_ManFindStartingState( Ssw_Man_t * p, Abc_Cex_t * pCex )
     }
     assert( iBit == pCex->nBits );
     // check that the output failed as expected -- cannot check because it is not an SRM!
-//    pObj = Aig_ManPo( p->pAig, pCex->iPo );
+//    pObj = Aig_ManCo( p->pAig, pCex->iPo );
 //    if ( pObj->fMarkB != 1 )
 //        printf( "The counter-example does not refine the output.\n" );
     // record the new pattern
diff --git a/src/proof/ssw/sswIslands.c b/src/proof/ssw/sswIslands.c
index 3173ec6f..8f54432d 100644
--- a/src/proof/ssw/sswIslands.c
+++ b/src/proof/ssw/sswIslands.c
@@ -85,14 +85,14 @@ void Ssw_MatchingStart( Aig_Man_t * p0, Aig_Man_t * p1, Vec_Int_t * vPairs )
     // make sure PIs are matched
     Saig_ManForEachPi( p0, pObj0, i )
     {
-        pObj1 = Aig_ManPi( p1, i );
+        pObj1 = Aig_ManCi( p1, i );
         assert( pObj0->pData == pObj1 );
         assert( pObj1->pData == pObj0 );
     }
     // make sure the POs are not matched
     Aig_ManForEachCo( p0, pObj0, i )
     {
-        pObj1 = Aig_ManPo( p1, i );
+        pObj1 = Aig_ManCo( p1, i );
         assert( pObj0->pData == NULL );
         assert( pObj1->pData == NULL );
     }
@@ -135,7 +135,7 @@ void Ssw_MatchingExtendOne( Aig_Man_t * p, Vec_Ptr_t * vNodes )
     Aig_ManIncrementTravId( p );
     Aig_ManForEachObj( p, pObj, i )
     {
-        if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
+        if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsCi(pObj) )
             continue;
         if ( pObj->pData != NULL )
             continue;
@@ -196,7 +196,7 @@ int Ssw_MatchingCountUnmached( Aig_Man_t * p )
     int i, Counter = 0;
     Aig_ManForEachObj( p, pObj, i )
     {
-        if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
+        if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsCi(pObj) )
             continue;
         if ( pObj->pData != NULL )
             continue;
@@ -230,8 +230,8 @@ void Ssw_MatchingExtend( Aig_Man_t * p0, Aig_Man_t * p1, int nDist, int fVerbose
         int nUnmached = Ssw_MatchingCountUnmached(p0);
         printf( "Extending islands by %d steps:\n", nDist );
         printf( "%2d : Total = %6d. Unmatched = %6d.  Ratio = %6.2f %%\n",
-            0, Aig_ManPiNum(p0) + Aig_ManNodeNum(p0), 
-            nUnmached, 100.0 * nUnmached/(Aig_ManPiNum(p0) + Aig_ManNodeNum(p0)) );
+            0, Aig_ManCiNum(p0) + Aig_ManNodeNum(p0), 
+            nUnmached, 100.0 * nUnmached/(Aig_ManCiNum(p0) + Aig_ManNodeNum(p0)) );
     }
     for ( d = 0; d < nDist; d++ )
     {
@@ -263,8 +263,8 @@ void Ssw_MatchingExtend( Aig_Man_t * p0, Aig_Man_t * p1, int nDist, int fVerbose
         {
             int nUnmached = Ssw_MatchingCountUnmached(p0);
             printf( "%2d : Total = %6d. Unmatched = %6d.  Ratio = %6.2f %%\n",
-                d+1, Aig_ManPiNum(p0) + Aig_ManNodeNum(p0), 
-                nUnmached, 100.0 * nUnmached/(Aig_ManPiNum(p0) + Aig_ManNodeNum(p0)) );
+                d+1, Aig_ManCiNum(p0) + Aig_ManNodeNum(p0), 
+                nUnmached, 100.0 * nUnmached/(Aig_ManCiNum(p0) + Aig_ManNodeNum(p0)) );
         }
     }
     Vec_PtrFree( vNodes0 );
@@ -335,15 +335,15 @@ Vec_Int_t * Ssw_MatchingPairs( Aig_Man_t * p0, Aig_Man_t * p1 )
     Aig_Obj_t * pObj0, * pObj1;
     int i;
     // check correctness
-    assert( Aig_ManPiNum(p0) == Aig_ManPiNum(p1) );
-    assert( Aig_ManPoNum(p0) == Aig_ManPoNum(p1) );
+    assert( Aig_ManCiNum(p0) == Aig_ManCiNum(p1) );
+    assert( Aig_ManCoNum(p0) == Aig_ManCoNum(p1) );
     assert( Aig_ManRegNum(p0) == Aig_ManRegNum(p1) );
     assert( Aig_ManObjNum(p0) == Aig_ManObjNum(p1) );
     // create complete pairs
     vPairsNew = Vec_IntAlloc( 2*Aig_ManObjNum(p0) );
     Aig_ManForEachObj( p0, pObj0, i )
     {
-        if ( Aig_ObjIsPo(pObj0) )
+        if ( Aig_ObjIsCo(pObj0) )
             continue;
         pObj1 = (Aig_Obj_t *)pObj0->pData;
         Vec_IntPush( vPairsNew, pObj0->Id );
@@ -390,7 +390,7 @@ Vec_Int_t * Ssw_MatchingMiter( Aig_Man_t * pMiter, Aig_Man_t * p0, Aig_Man_t * p
         assert( !Aig_IsComplement(pObj0) );
         assert( !Aig_IsComplement(pObj1) );
         assert( Aig_ObjType(pObj0) == Aig_ObjType(pObj1) );
-        if ( Aig_ObjIsPo(pObj0) )
+        if ( Aig_ObjIsCo(pObj0) )
             continue;
         assert( Aig_ObjIsNode(pObj0) || Saig_ObjIsLo(pMiter, pObj0) );
         assert( Aig_ObjIsNode(pObj1) || Saig_ObjIsLo(pMiter, pObj1) );
@@ -519,7 +519,7 @@ Vec_Int_t * Saig_StrSimPerformMatching_hack( Aig_Man_t * p0, Aig_Man_t * p1 )
     vPairs = Vec_IntAlloc( 100 );
     Aig_ManForEachObj( p0, pObj, i )
     {
-        if ( !Aig_ObjIsConst1(pObj) && !Aig_ObjIsPi(pObj) && !Aig_ObjIsNode(pObj) )
+        if ( !Aig_ObjIsConst1(pObj) && !Aig_ObjIsCi(pObj) && !Aig_ObjIsNode(pObj) )
             continue;
         Vec_IntPush( vPairs, i );
         Vec_IntPush( vPairs, i );
diff --git a/src/proof/ssw/sswLcorr.c b/src/proof/ssw/sswLcorr.c
index c41a74ef..ec6087f0 100644
--- a/src/proof/ssw/sswLcorr.c
+++ b/src/proof/ssw/sswLcorr.c
@@ -58,7 +58,7 @@ void Ssw_ManSweepTransfer( Ssw_Man_t * p )
             continue;
         }
         assert( !Aig_IsComplement(pObjFraig) );
-        assert( Aig_ObjIsPi(pObjFraig) );
+        assert( Aig_ObjIsCi(pObjFraig) );
         pInfo = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjPioNum(pObjFraig) );
         Ssw_SmlObjSetWord( p->pSml, pObj, pInfo[0], 0, 0 );
     }
@@ -160,8 +160,8 @@ void Ssw_ManSweepLatchOne( Ssw_Man_t * p, Aig_Obj_t * pObjRepr, Aig_Obj_t * pObj
 {
     Aig_Obj_t * pObjFraig, * pObjReprFraig, * pObjLi;
     int RetValue, clk;
-    assert( Aig_ObjIsPi(pObj) );
-    assert( Aig_ObjIsPi(pObjRepr) || Aig_ObjIsConst1(pObjRepr) );
+    assert( Aig_ObjIsCi(pObj) );
+    assert( Aig_ObjIsCi(pObjRepr) || Aig_ObjIsConst1(pObjRepr) );
     // check if it makes sense to skip some calls
     if ( p->nCallsCount > 100 && p->nCallsUnsat < p->nCallsSat )
     {
@@ -175,7 +175,7 @@ clk = clock();
     Ssw_ManBuildCone_rec( p, Aig_ObjFanin0(pObjLi) );
     pObjFraig = Ssw_ObjChild0Fra( p, pObjLi, 0 );
     // get the fraiged representative
-    if ( Aig_ObjIsPi(pObjRepr) )
+    if ( Aig_ObjIsCi(pObjRepr) )
     {
         pObjLi = Saig_ObjLoToLi( p->pAig, pObjRepr ); 
         Ssw_ManBuildCone_rec( p, Aig_ObjFanin0(pObjLi) );
@@ -264,7 +264,7 @@ int Ssw_ManSweepLatch( Ssw_Man_t * p )
 
     // prepare simulation info
     assert( p->vSimInfo == NULL );
-    p->vSimInfo = Vec_PtrAllocSimInfo( Aig_ManPiNum(p->pFrames), 1 );
+    p->vSimInfo = Vec_PtrAllocSimInfo( Aig_ManCiNum(p->pFrames), 1 );
     Vec_PtrCleanSimInfo( p->vSimInfo, 0, 1 );
 
     // go through the registers
diff --git a/src/proof/ssw/sswPairs.c b/src/proof/ssw/sswPairs.c
index 0aba942f..e356aa60 100644
--- a/src/proof/ssw/sswPairs.c
+++ b/src/proof/ssw/sswPairs.c
@@ -64,7 +64,7 @@ int Ssw_MiterStatus( Aig_Man_t * p, int fVerbose )
             continue;
         }
         // check if the output is a primary input
-        if ( p->nRegs == 0 && Aig_ObjIsPi(Aig_Regular(pChild)) )
+        if ( p->nRegs == 0 && Aig_ObjIsCi(Aig_Regular(pChild)) )
         {
             CountNonConst0++;
             continue;
diff --git a/src/proof/ssw/sswPart.c b/src/proof/ssw/sswPart.c
index d2f07dc8..5a3aea10 100644
--- a/src/proof/ssw/sswPart.c
+++ b/src/proof/ssw/sswPart.c
@@ -90,7 +90,7 @@ Aig_Man_t * Ssw_SignalCorrespondencePart( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
             pTemp = Aig_ManRegCreatePart( pAig, vPart, &nCountPis, &nCountRegs, NULL );
             Ioa_WriteAiger( pTemp, Buffer, 0, 0 );
             printf( "part%03d.aig : Reg = %4d. PI = %4d. (True = %4d. Regs = %4d.) And = %5d.\n", 
-                i, Vec_IntSize(vPart), Aig_ManPiNum(pTemp)-Vec_IntSize(vPart), nCountPis, nCountRegs, Aig_ManNodeNum(pTemp) );
+                i, Vec_IntSize(vPart), Aig_ManCiNum(pTemp)-Vec_IntSize(vPart), nCountPis, nCountRegs, Aig_ManNodeNum(pTemp) );
             Aig_ManStop( pTemp );
         }
     }
@@ -110,7 +110,7 @@ Aig_Man_t * Ssw_SignalCorrespondencePart( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
             nClasses = Aig_TransferMappedClasses( pAig, pTemp, pMapBack );
             if ( fVerbose )
                 printf( "%3d : Reg = %4d. PI = %4d. (True = %4d. Regs = %4d.) And = %5d. It = %3d. Cl = %5d.\n", 
-                    i, Vec_IntSize(vPart), Aig_ManPiNum(pTemp)-Vec_IntSize(vPart), nCountPis, nCountRegs, Aig_ManNodeNum(pTemp), pPars->nIters, nClasses );
+                    i, Vec_IntSize(vPart), Aig_ManCiNum(pTemp)-Vec_IntSize(vPart), nCountPis, nCountRegs, Aig_ManNodeNum(pTemp), pPars->nIters, nClasses );
             Aig_ManStop( pNew );
         }
         Aig_ManStop( pTemp );
diff --git a/src/proof/ssw/sswRarity.c b/src/proof/ssw/sswRarity.c
index 6e36ae12..445dda84 100644
--- a/src/proof/ssw/sswRarity.c
+++ b/src/proof/ssw/sswRarity.c
@@ -831,7 +831,7 @@ static Vec_Int_t * Ssw_RarFindStartingState( Aig_Man_t * pAig, Abc_Cex_t * pCex
     }
     assert( iBit == pCex->nBits );
     // check that the output failed as expected -- cannot check because it is not an SRM!
-//    pObj = Aig_ManPo( pAig, pCex->iPo );
+//    pObj = Aig_ManCo( pAig, pCex->iPo );
 //    if ( pObj->fMarkB != 1 )
 //        printf( "The counter-example does not refine the output.\n" );
     // record the new pattern
diff --git a/src/proof/ssw/sswRarity2.c b/src/proof/ssw/sswRarity2.c
index dce7ac3e..0851cf3d 100644
--- a/src/proof/ssw/sswRarity2.c
+++ b/src/proof/ssw/sswRarity2.c
@@ -282,7 +282,7 @@ static Vec_Int_t * Ssw_RarFindStartingState( Aig_Man_t * pAig, Abc_Cex_t * pCex
     }
     assert( iBit == pCex->nBits );
     // check that the output failed as expected -- cannot check because it is not an SRM!
-//    pObj = Aig_ManPo( pAig, pCex->iPo );
+//    pObj = Aig_ManCo( pAig, pCex->iPo );
 //    if ( pObj->fMarkB != 1 )
 //        printf( "The counter-example does not refine the output.\n" );
     // record the new pattern
diff --git a/src/proof/ssw/sswSim.c b/src/proof/ssw/sswSim.c
index 946224cd..b53e8baf 100644
--- a/src/proof/ssw/sswSim.c
+++ b/src/proof/ssw/sswSim.c
@@ -457,13 +457,13 @@ int * Ssw_SmlCheckOutputSavePattern( Ssw_Sml_t * p, Aig_Obj_t * pObjPo )
     // determine the best pattern
     BestPat = i * 32 + k;
     // fill in the counter-example data
-    pModel = ABC_ALLOC( int, Aig_ManPiNum(p->pAig)+1 );
+    pModel = ABC_ALLOC( int, Aig_ManCiNum(p->pAig)+1 );
     Aig_ManForEachCi( p->pAig, pObjPi, i )
     {
         pModel[i] = Abc_InfoHasBit(Ssw_ObjSim(p, pObjPi->Id), BestPat);
 //        printf( "%d", pModel[i] );
     }
-    pModel[Aig_ManPiNum(p->pAig)] = pObjPo->Id;
+    pModel[Aig_ManCiNum(p->pAig)] = pObjPo->Id;
 //    printf( "\n" );
     return pModel;
 }
@@ -484,7 +484,7 @@ int * Ssw_SmlCheckOutput( Ssw_Sml_t * p )
     Aig_Obj_t * pObj;
     int i;
     // make sure the reference simulation pattern does not detect the bug
-    pObj = Aig_ManPo( p->pAig, 0 );
+    pObj = Aig_ManCo( p->pAig, 0 );
     assert( Aig_ObjFanin0(pObj)->fPhase == (unsigned)Aig_ObjFaninC0(pObj) ); 
     Aig_ManForEachCo( p->pAig, pObj, i )
     {
@@ -514,7 +514,7 @@ void Ssw_SmlAssignRandom( Ssw_Sml_t * p, Aig_Obj_t * pObj )
 {
     unsigned * pSims;
     int i, f;
-    assert( Aig_ObjIsPi(pObj) );
+    assert( Aig_ObjIsCi(pObj) );
     pSims = Ssw_ObjSim( p, pObj->Id );
     for ( i = 0; i < p->nWordsTotal; i++ )
         pSims[i] = Ssw_ObjRandomSim();
@@ -540,7 +540,7 @@ void Ssw_SmlAssignRandomFrame( Ssw_Sml_t * p, Aig_Obj_t * pObj, int iFrame )
     unsigned * pSims;
     int i;
     assert( iFrame < p->nFrames );
-    assert( Aig_ObjIsPi(pObj) );
+    assert( Aig_ObjIsCi(pObj) );
     pSims = Ssw_ObjSim( p, pObj->Id ) + p->nWordsFrame * iFrame;
     for ( i = 0; i < p->nWordsFrame; i++ )
         pSims[i] = Ssw_ObjRandomSim();
@@ -562,7 +562,7 @@ void Ssw_SmlObjAssignConst( Ssw_Sml_t * p, Aig_Obj_t * pObj, int fConst1, int iF
     unsigned * pSims;
     int i;
     assert( iFrame < p->nFrames );
-    assert( Aig_ObjIsPi(pObj) );
+    assert( Aig_ObjIsCi(pObj) );
     pSims = Ssw_ObjSim( p, pObj->Id ) + p->nWordsFrame * iFrame;
     for ( i = 0; i < p->nWordsFrame; i++ )
         pSims[i] = fConst1? ~(unsigned)0 : 0;
@@ -584,7 +584,7 @@ void Ssw_SmlObjAssignConstWord( Ssw_Sml_t * p, Aig_Obj_t * pObj, int fConst1, in
     unsigned * pSims;
     assert( iFrame < p->nFrames );
     assert( iWord < p->nWordsFrame );
-    assert( Aig_ObjIsPi(pObj) );
+    assert( Aig_ObjIsCi(pObj) );
     pSims = Ssw_ObjSim( p, pObj->Id ) + p->nWordsFrame * iFrame;
     pSims[iWord] = fConst1? ~(unsigned)0 : 0;
 } 
@@ -604,7 +604,7 @@ void Ssw_SmlObjSetWord( Ssw_Sml_t * p, Aig_Obj_t * pObj, unsigned Word, int iWor
 {
     unsigned * pSims;
     assert( iFrame < p->nFrames );
-    assert( Aig_ObjIsPi(pObj) );
+    assert( Aig_ObjIsCi(pObj) );
     pSims = Ssw_ObjSim( p, pObj->Id ) + p->nWordsFrame * iFrame;
     pSims[iWord] = Word;
 } 
@@ -631,16 +631,16 @@ void Ssw_SmlAssignDist1( Ssw_Sml_t * p, unsigned * pPat )
         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 );
+        Limit = Abc_MinInt( Aig_ManCiNum(p->pAig), p->nWordsTotal * 32 - 1 );
         for ( i = 0; i < Limit; i++ )
-            Abc_InfoXorBit( Ssw_ObjSim( p, Aig_ManPi(p->pAig,i)->Id ), i+1 );
+            Abc_InfoXorBit( Ssw_ObjSim( p, Aig_ManCi(p->pAig,i)->Id ), i+1 );
     }
     else
     {
         int fUseDist1 = 0;
 
         // copy the PI info for each frame
-        nTruePis = Aig_ManPiNum(p->pAig) - Aig_ManRegNum(p->pAig);
+        nTruePis = Aig_ManCiNum(p->pAig) - Aig_ManRegNum(p->pAig);
         for ( f = 0; f < p->nFrames; f++ )
             Saig_ManForEachPi( p->pAig, pObj, i )
                 Ssw_SmlObjAssignConst( p, pObj, Abc_InfoHasBit(pPat, nTruePis * f + i), f );
@@ -648,14 +648,14 @@ void Ssw_SmlAssignDist1( Ssw_Sml_t * p, unsigned * pPat )
         k = 0;
         Saig_ManForEachLo( p->pAig, pObj, i )
             Ssw_SmlObjAssignConst( p, pObj, Abc_InfoHasBit(pPat, nTruePis * p->nFrames + k++), 0 );
-//        assert( p->pFrames == NULL || nTruePis * p->nFrames + k == Aig_ManPiNum(p->pFrames) );
+//        assert( p->pFrames == NULL || nTruePis * p->nFrames + k == Aig_ManCiNum(p->pFrames) );
 
         // flip one bit of the last frame
         if ( fUseDist1 ) //&& p->nFrames == 2 )
         {
             Limit = Abc_MinInt( nTruePis, p->nWordsFrame * 32 - 1 );
             for ( i = 0; i < Limit; i++ )
-                Abc_InfoXorBit( Ssw_ObjSim( p, Aig_ManPi(p->pAig, i)->Id ) + p->nWordsFrame*(p->nFrames-1), i+1 );
+                Abc_InfoXorBit( Ssw_ObjSim( p, Aig_ManCi(p->pAig, i)->Id ) + p->nWordsFrame*(p->nFrames-1), i+1 );
         }
     }
 }
@@ -684,7 +684,7 @@ void Ssw_SmlAssignDist1Plus( Ssw_Sml_t * p, unsigned * pPat )
     // set distance one PIs for the first frame
     Limit = Abc_MinInt( Saig_ManPiNum(p->pAig), p->nWordsFrame * 32 - 1 );
     for ( i = 0; i < Limit; i++ )
-        Abc_InfoXorBit( Ssw_ObjSim( p, Aig_ManPi(p->pAig, i)->Id ), i+1 );
+        Abc_InfoXorBit( Ssw_ObjSim( p, Aig_ManCi(p->pAig, i)->Id ), i+1 );
 
     // create random info for the remaining timeframes
     for ( f = 1; f < p->nFrames; f++ )
@@ -806,7 +806,7 @@ void Ssw_SmlNodeCopyFanin( Ssw_Sml_t * p, Aig_Obj_t * pObj, int iFrame )
     int fCompl, fCompl0, i;
     assert( iFrame < p->nFrames );
     assert( !Aig_IsComplement(pObj) );
-    assert( Aig_ObjIsPo(pObj) );
+    assert( Aig_ObjIsCo(pObj) );
     assert( iFrame == 0 || p->nWordsFrame < p->nWordsTotal );
     // get hold of the simulation information
     pSims  = Ssw_ObjSim(p, pObj->Id) + p->nWordsFrame * iFrame;
@@ -841,8 +841,8 @@ void Ssw_SmlNodeTransferNext( Ssw_Sml_t * p, Aig_Obj_t * pOut, Aig_Obj_t * pIn,
     assert( iFrame < p->nFrames );
     assert( !Aig_IsComplement(pOut) );
     assert( !Aig_IsComplement(pIn) );
-    assert( Aig_ObjIsPo(pOut) );
-    assert( Aig_ObjIsPi(pIn) );
+    assert( Aig_ObjIsCo(pOut) );
+    assert( Aig_ObjIsCi(pIn) );
     assert( iFrame == 0 || p->nWordsFrame < p->nWordsTotal );
     // get hold of the simulation information
     pSims0 = Ssw_ObjSim(p, pOut->Id) + p->nWordsFrame * iFrame;
@@ -869,8 +869,8 @@ void Ssw_SmlNodeTransferFirst( Ssw_Sml_t * p, Aig_Obj_t * pOut, Aig_Obj_t * pIn
     int i;
     assert( !Aig_IsComplement(pOut) );
     assert( !Aig_IsComplement(pIn) );
-    assert( Aig_ObjIsPo(pOut) );
-    assert( Aig_ObjIsPi(pIn) );
+    assert( Aig_ObjIsCo(pOut) );
+    assert( Aig_ObjIsCi(pIn) );
     assert( p->nWordsFrame < p->nWordsTotal );
     // get hold of the simulation information
     pSims0 = Ssw_ObjSim(p, pOut->Id) + p->nWordsFrame * (p->nFrames-1);
@@ -899,7 +899,7 @@ void Ssw_SmlInitialize( Ssw_Sml_t * p, int fInit )
     if ( fInit )
     {
         assert( Aig_ManRegNum(p->pAig) > 0 );
-        assert( Aig_ManRegNum(p->pAig) <= Aig_ManPiNum(p->pAig) );
+        assert( Aig_ManRegNum(p->pAig) <= Aig_ManCiNum(p->pAig) );
         // assign random info for primary inputs
         Saig_ManForEachPi( p->pAig, pObj, i )
             Ssw_SmlAssignRandom( p, pObj );
@@ -931,7 +931,7 @@ void Ssw_SmlInitializeSpecial( Ssw_Sml_t * p, Vec_Int_t * vInit )
     int Entry, i, nRegs;
     nRegs = Aig_ManRegNum(p->pAig);
     assert( nRegs > 0 );
-    assert( nRegs <= Aig_ManPiNum(p->pAig) );
+    assert( nRegs <= Aig_ManCiNum(p->pAig) );
     assert( Vec_IntSize(vInit) == nRegs * p->nWordsFrame );
     // assign random info for primary inputs
     Saig_ManForEachPi( p->pAig, pObj, i )
@@ -957,7 +957,7 @@ void Ssw_SmlReinitialize( Ssw_Sml_t * p )
     Aig_Obj_t * pObj, * pObjLi, * pObjLo;
     int i;
     assert( Aig_ManRegNum(p->pAig) > 0 );
-    assert( Aig_ManRegNum(p->pAig) < Aig_ManPiNum(p->pAig) );
+    assert( Aig_ManRegNum(p->pAig) < Aig_ManCiNum(p->pAig) );
     // assign random info for primary inputs
     Saig_ManForEachPi( p->pAig, pObj, i )
         Ssw_SmlAssignRandom( p, pObj );
@@ -1361,12 +1361,12 @@ Abc_Cex_t * Ssw_SmlGetCounterExample( Ssw_Sml_t * p )
             }
         break;
     }
-    assert( iPo < Aig_ManPoNum(p->pAig)-Aig_ManRegNum(p->pAig) );
+    assert( iPo < Aig_ManCoNum(p->pAig)-Aig_ManRegNum(p->pAig) );
     assert( iFrame < p->nFrames );
     assert( iBit < 32 * p->nWordsFrame );
 
     // allocate the counter example
-    pCex = Abc_CexAlloc( Aig_ManRegNum(p->pAig), Aig_ManPiNum(p->pAig) - Aig_ManRegNum(p->pAig), iFrame + 1 );
+    pCex = Abc_CexAlloc( Aig_ManRegNum(p->pAig), Aig_ManCiNum(p->pAig) - Aig_ManRegNum(p->pAig), iFrame + 1 );
     pCex->iPo    = iPo;
     pCex->iFrame = iFrame;
 
diff --git a/src/proof/ssw/sswSweep.c b/src/proof/ssw/sswSweep.c
index a3a8d1c8..550cb4ce 100644
--- a/src/proof/ssw/sswSweep.c
+++ b/src/proof/ssw/sswSweep.c
@@ -48,7 +48,7 @@ int Ssw_ManGetSatVarValue( Ssw_Man_t * p, Aig_Obj_t * pObj, int f )
     int fUseNoBoundary = 0;
     Aig_Obj_t * pObjFraig;
     int Value;
-//    assert( Aig_ObjIsPi(pObj) );
+//    assert( Aig_ObjIsCi(pObj) );
     pObjFraig = Ssw_ObjFrame( p, pObj, f );
     if ( fUseNoBoundary )
     {
@@ -86,12 +86,12 @@ void Ssw_CheckConstraints( Ssw_Man_t * p )
     Aig_Obj_t * pObj, * pObj2;
     int nConstrPairs, i;
     int Counter = 0;
-    nConstrPairs = Aig_ManPoNum(p->pFrames)-Aig_ManRegNum(p->pAig);
+    nConstrPairs = Aig_ManCoNum(p->pFrames)-Aig_ManRegNum(p->pAig);
     assert( (nConstrPairs & 1) == 0 );
     for ( i = 0; i < nConstrPairs; i += 2 )
     {
-        pObj  = Aig_ManPo( p->pFrames, i   );
-        pObj2 = Aig_ManPo( p->pFrames, i+1 );
+        pObj  = Aig_ManCo( p->pFrames, i   );
+        pObj2 = Aig_ManCo( p->pFrames, i+1 );
         if ( Ssw_NodesAreEquiv( p, Aig_ObjFanin0(pObj), Aig_ObjFanin0(pObj2) ) != 1 )
         {
             Ssw_NodesAreConstrained( p, Aig_ObjChild0(pObj), Aig_ObjChild0(pObj2) );
@@ -162,7 +162,7 @@ void Ssw_SmlAddPatternDyn( Ssw_Man_t * p )
     // iterate through the PIs of the frames
     Vec_PtrForEachEntry( Aig_Obj_t *, p->pMSat->vUsedPis, pObj, i )
     {
-        assert( Aig_ObjIsPi(pObj) );
+        assert( Aig_ObjIsCi(pObj) );
         nVarNum = Ssw_ObjSatNum( p->pMSat, pObj );
         assert( nVarNum > 0 );
         if ( sat_solver_var_value( p->pMSat->pSat, nVarNum ) )
@@ -373,18 +373,18 @@ clk = clock();
     // create timeframes
     p->pFrames = Ssw_FramesWithClasses( p );
     // add constants
-    nConstrPairs = Aig_ManPoNum(p->pFrames)-Aig_ManRegNum(p->pAig);
+    nConstrPairs = Aig_ManCoNum(p->pFrames)-Aig_ManRegNum(p->pAig);
     assert( (nConstrPairs & 1) == 0 );
     for ( i = 0; i < nConstrPairs; i += 2 )
     {
-        pObj  = Aig_ManPo( p->pFrames, i   );
-        pObj2 = Aig_ManPo( p->pFrames, i+1 );
+        pObj  = Aig_ManCo( p->pFrames, i   );
+        pObj2 = Aig_ManCo( p->pFrames, i+1 );
         Ssw_NodesAreConstrained( p, Aig_ObjChild0(pObj), Aig_ObjChild0(pObj2) );
     }
     // build logic cones for register inputs
     for ( i = 0; i < Aig_ManRegNum(p->pAig); i++ )
     {
-        pObj  = Aig_ManPo( p->pFrames, nConstrPairs + i );
+        pObj  = Aig_ManCo( p->pFrames, nConstrPairs + i );
         Ssw_CnfNodeAddToSolver( p->pMSat, Aig_ObjFanin0(pObj) );//
     }
     sat_solver_simplify( p->pMSat->pSat );
diff --git a/src/proof/ssw/sswUnique.c b/src/proof/ssw/sswUnique.c
index b5f6a853..8e989531 100644
--- a/src/proof/ssw/sswUnique.c
+++ b/src/proof/ssw/sswUnique.c
@@ -105,7 +105,7 @@ int Ssw_ManUniqueOne( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pObj, int fV
     k = 0;
     Vec_PtrForEachEntry( Aig_Obj_t *, p->vCommon, pTemp, i )
     {
-        assert( Aig_ObjIsPi(pTemp) );
+        assert( Aig_ObjIsCi(pTemp) );
         if ( !Saig_ObjIsLo(p->pAig, pTemp) )
             continue;
         assert( Aig_ObjPioNum(pTemp) > 0 );