Version abc90215

60 files changed, 376 insertions, 383 deletions

diff --git a/src/opt/cut/cut.h b/src/opt/cut/cut.h
index faa249f2..394138db 100644
--- a/src/opt/cut/cut.h
+++ b/src/opt/cut/cut.h
@@ -21,10 +21,6 @@
 #ifndef __CUT_H__
 #define __CUT_H__
 
-#ifdef __cplusplus
-extern "C" {
-#endif
-
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -33,6 +29,10 @@ extern "C" {
 ///                         PARAMETERS                               ///
 ////////////////////////////////////////////////////////////////////////
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 #define CUT_SIZE_MIN    3      // the min K of the K-feasible cut computation
 #define CUT_SIZE_MAX   12      // the max K of the K-feasible cut computation
 
diff --git a/src/opt/cut/cutMan.c b/src/opt/cut/cutMan.c
index 882567fd..28264e33 100644
--- a/src/opt/cut/cutMan.c
+++ b/src/opt/cut/cutMan.c
@@ -47,7 +47,7 @@ Cut_Man_t * Cut_ManStart( Cut_Params_t * pParams )
 //    extern int nTruthDsd;
 //    nTruthDsd = 0;
     assert( pParams->nVarsMax >= 3 && pParams->nVarsMax <= CUT_SIZE_MAX );
-    p = ALLOC( Cut_Man_t, 1 );
+    p = ABC_ALLOC( Cut_Man_t, 1 );
     memset( p, 0, sizeof(Cut_Man_t) );
     // set and correct parameters
     p->pParams = pParams;
@@ -82,7 +82,7 @@ Cut_Man_t * Cut_ManStart( Cut_Params_t * pParams )
             p->nTruthWords = Cut_TruthWords( pParams->nVarsMax );
             p->EntrySize += p->nTruthWords * sizeof(unsigned);
         }
-        p->puTemp[0] = ALLOC( unsigned, 4 * p->nTruthWords );
+        p->puTemp[0] = ABC_ALLOC( unsigned, 4 * p->nTruthWords );
         p->puTemp[1] = p->puTemp[0] + p->nTruthWords;
         p->puTemp[2] = p->puTemp[1] + p->nTruthWords;
         p->puTemp[3] = p->puTemp[2] + p->nTruthWords;
@@ -132,10 +132,10 @@ void Cut_ManStop( Cut_Man_t * p )
     if ( p->vNodeCuts )   Vec_IntFree( p->vNodeCuts );
     if ( p->vNodeStarts ) Vec_IntFree( p->vNodeStarts );
     if ( p->vCutPairs )   Vec_IntFree( p->vCutPairs );
-    if ( p->puTemp[0] )   free( p->puTemp[0] );
+    if ( p->puTemp[0] )   ABC_FREE( p->puTemp[0] );
 
     Extra_MmFixedStop( p->pMmCuts );
-    free( p );
+    ABC_FREE( p );
 }
 
 /**Function*************************************************************
@@ -176,11 +176,11 @@ void Cut_ManPrintStats( Cut_Man_t * p )
     if ( p->pParams->fMap && !p->pParams->fSeq )
     printf( "Mapping delay     = %8d.\n", p->nDelayMin );
 
-    PRT( "Merge ", p->timeMerge );
-    PRT( "Union ", p->timeUnion );
-    PRT( "Filter", p->timeFilter );
-    PRT( "Truth ", p->timeTruth );
-    PRT( "Map   ", p->timeMap );
+    ABC_PRT( "Merge ", p->timeMerge );
+    ABC_PRT( "Union ", p->timeUnion );
+    ABC_PRT( "Filter", p->timeFilter );
+    ABC_PRT( "Truth ", p->timeTruth );
+    ABC_PRT( "Map   ", p->timeMap );
 //    printf( "Nodes = %d. Multi = %d.  Cuts = %d. Multi = %d.\n", 
 //        p->nNodes, p->nNodesMulti, p->nCutsCur-p->nCutsTriv, p->nCutsMulti );
 //    printf( "Count0 = %d. Count1 = %d. Count2 = %d.\n\n", p->Count0, p->Count1, p->Count2 );
diff --git a/src/opt/cut/cutOracle.c b/src/opt/cut/cutOracle.c
index 4ec6bc05..32798f4f 100644
--- a/src/opt/cut/cutOracle.c
+++ b/src/opt/cut/cutOracle.c
@@ -74,7 +74,7 @@ Cut_Oracle_t * Cut_OracleStart( Cut_Man_t * pMan )
     assert( pMan->pParams->nVarsMax >= 3 && pMan->pParams->nVarsMax <= CUT_SIZE_MAX );
     assert( pMan->pParams->fRecord );
 
-    p = ALLOC( Cut_Oracle_t, 1 );
+    p = ABC_ALLOC( Cut_Oracle_t, 1 );
     memset( p, 0, sizeof(Cut_Oracle_t) );
 
     // set and correct parameters
@@ -130,7 +130,7 @@ void Cut_OracleStop( Cut_Oracle_t * p )
     {
         printf( "Cut computation statistics with oracle:\n" );
         printf( "Current cuts      = %8d. (Trivial = %d.)\n", p->nCuts-p->nCutsTriv, p->nCutsTriv );
-        PRT( "Total time ", p->timeTotal );
+        ABC_PRT( "Total time ", p->timeTotal );
     }
 
     Vec_PtrForEachEntry( p->vCutsNew, pCut, i )
@@ -145,7 +145,7 @@ void Cut_OracleStop( Cut_Oracle_t * p )
     if ( p->vCutPairs )   Vec_IntFree( p->vCutPairs );
 
     Extra_MmFixedStop( p->pMmCuts );
-    free( p ); 
+    ABC_FREE( p ); 
 }
 
 /**Function*************************************************************
diff --git a/src/opt/cut/cutPre22.c b/src/opt/cut/cutPre22.c
index 5ba860c9..bda612f7 100644
--- a/src/opt/cut/cutPre22.c
+++ b/src/opt/cut/cutPre22.c
@@ -398,7 +398,7 @@ void Cut_CellPrecompute()
     }
 
     printf( "BASIC: Total = %d. Good = %d. Entry = %d. ", (int)p->nTotal, (int)p->nGood, (int)sizeof(Cut_Cell_t) );
-    PRT( "Time", clock() - clk );
+    ABC_PRT( "Time", clock() - clk );
     printf( "Cells:  " );
     for ( i = 0; i <= 9; i++ )
         printf( "%d=%d ", i, p->nVarCounts[i] );
@@ -482,7 +482,7 @@ void Cut_CellPrecompute()
         }
 
         printf( "VAR %d: Total = %d. Good = %d. Entry = %d. ", k, p->nTotal, p->nGood, (int)sizeof(Cut_Cell_t) );
-        PRT( "Time", clock() - clk );
+        ABC_PRT( "Time", clock() - clk );
         printf( "Cells:  " );
         for ( i = 0; i <= 9; i++ )
             printf( "%d=%d ", i, p->nVarCounts[i] );
@@ -495,9 +495,9 @@ void Cut_CellPrecompute()
         printf( "\n" );
     }
 //    printf( "\n" );
-    PRT( "Supp ", p->timeSupp );
-    PRT( "Canon", p->timeCanon );
-    PRT( "Table", p->timeTable );
+    ABC_PRT( "Supp ", p->timeSupp );
+    ABC_PRT( "Canon", p->timeCanon );
+    ABC_PRT( "Table", p->timeTable );
 //    Cut_CManStop( p );
 }
 
@@ -517,7 +517,7 @@ int Cut_CellTableLookup( Cut_CMan_t * p, Cut_Cell_t * pCell )
     Cut_Cell_t ** pSlot, * pTemp;
     unsigned Hash;
     Hash = Extra_TruthHash( pCell->uTruth, Extra_TruthWordNum( pCell->nVars ) );
-    if ( !st_find_or_add( p->tTable, (char *)(PORT_PTRUINT_T)Hash, (char ***)&pSlot ) )
+    if ( !st_find_or_add( p->tTable, (char *)(ABC_PTRUINT_T)Hash, (char ***)&pSlot ) )
         *pSlot = NULL;
     for ( pTemp = *pSlot; pTemp; pTemp = pTemp->pNext )
     {
@@ -770,7 +770,7 @@ Cut_CMan_t * Cut_CManStart()
     int i, k;
     // start the manager
     assert( sizeof(unsigned) == 4 );
-    p = ALLOC( Cut_CMan_t, 1 );
+    p = ABC_ALLOC( Cut_CMan_t, 1 );
     memset( p, 0, sizeof(Cut_CMan_t) );
     // start the table and the memory manager
     p->tTable = st_init_table(st_ptrcmp,st_ptrhash);
@@ -799,7 +799,7 @@ void Cut_CManStop( Cut_CMan_t * p )
 {
     st_free_table( p->tTable );
     Extra_MmFixedStop( p->pMem );
-    free( p );
+    ABC_FREE( p );
 }
 /**Function*************************************************************
 
@@ -916,7 +916,7 @@ void Cut_CellDumpToFile()
 
     printf( "Library composed of %d functions is written into file \"%s\".  ", Counter, pFileName );
 
-    PRT( "Time", clock() - clk );
+    ABC_PRT( "Time", clock() - clk );
 }
 
 
@@ -962,7 +962,7 @@ int Cut_CellTruthLookup( unsigned * pTruth, int nVars )
 
     // check if the cell exists
     Hash = Extra_TruthHash( pCell->uTruth, Extra_TruthWordNum(pCell->nVars) );
-    if ( st_lookup( p->tTable, (char *)(PORT_PTRUINT_T)Hash, (char **)&pTemp ) )
+    if ( st_lookup( p->tTable, (char *)(ABC_PTRUINT_T)Hash, (char **)&pTemp ) )
     {
         for ( ; pTemp; pTemp = pTemp->pNext )
         {
diff --git a/src/opt/dec/dec.h b/src/opt/dec/dec.h
index d0d9981d..4042ac65 100644
--- a/src/opt/dec/dec.h
+++ b/src/opt/dec/dec.h
@@ -21,10 +21,6 @@
 #ifndef __DEC_H__
 #define __DEC_H__
 
-#ifdef __cplusplus
-extern "C" {
-#endif
-
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -33,6 +29,10 @@ extern "C" {
 ///                         PARAMETERS                               ///
 ////////////////////////////////////////////////////////////////////////
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                         BASIC TYPES                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -212,12 +212,12 @@ static inline Dec_Edge_t Dec_IntToEdge_( unsigned Edge )
 static inline Dec_Graph_t * Dec_GraphCreate( int nLeaves )   
 {
     Dec_Graph_t * pGraph;
-    pGraph = ALLOC( Dec_Graph_t, 1 );
+    pGraph = ABC_ALLOC( Dec_Graph_t, 1 );
     memset( pGraph, 0, sizeof(Dec_Graph_t) );
     pGraph->nLeaves = nLeaves;
     pGraph->nSize = nLeaves;
     pGraph->nCap = 2 * nLeaves + 50;
-    pGraph->pNodes = ALLOC( Dec_Node_t, pGraph->nCap );
+    pGraph->pNodes = ABC_ALLOC( Dec_Node_t, pGraph->nCap );
     memset( pGraph->pNodes, 0, sizeof(Dec_Node_t) * pGraph->nSize );
     return pGraph;
 }
@@ -236,7 +236,7 @@ static inline Dec_Graph_t * Dec_GraphCreate( int nLeaves )
 static inline Dec_Graph_t * Dec_GraphCreateConst0()   
 {
     Dec_Graph_t * pGraph;
-    pGraph = ALLOC( Dec_Graph_t, 1 );
+    pGraph = ABC_ALLOC( Dec_Graph_t, 1 );
     memset( pGraph, 0, sizeof(Dec_Graph_t) );
     pGraph->fConst = 1;
     pGraph->eRoot.fCompl = 1;
@@ -257,7 +257,7 @@ static inline Dec_Graph_t * Dec_GraphCreateConst0()
 static inline Dec_Graph_t * Dec_GraphCreateConst1()   
 {
     Dec_Graph_t * pGraph;
-    pGraph = ALLOC( Dec_Graph_t, 1 );
+    pGraph = ABC_ALLOC( Dec_Graph_t, 1 );
     memset( pGraph, 0, sizeof(Dec_Graph_t) );
     pGraph->fConst = 1;
     return pGraph;
@@ -297,8 +297,8 @@ static inline Dec_Graph_t * Dec_GraphCreateLeaf( int iLeaf, int nLeaves, int fCo
 ***********************************************************************/
 static inline void Dec_GraphFree( Dec_Graph_t * pGraph )   
 {
-    FREE( pGraph->pNodes );
-    free( pGraph );
+    ABC_FREE( pGraph->pNodes );
+    ABC_FREE( pGraph );
 }
 
 /**Function*************************************************************
@@ -560,7 +560,7 @@ static inline Dec_Node_t * Dec_GraphAppendNode( Dec_Graph_t * pGraph )
     Dec_Node_t * pNode;
     if ( pGraph->nSize == pGraph->nCap )
     {
-        pGraph->pNodes = REALLOC( Dec_Node_t, pGraph->pNodes, 2 * pGraph->nCap ); 
+        pGraph->pNodes = ABC_REALLOC( Dec_Node_t, pGraph->pNodes, 2 * pGraph->nCap ); 
         pGraph->nCap   = 2 * pGraph->nCap;
     }
     pNode = pGraph->pNodes + pGraph->nSize++;
diff --git a/src/opt/dec/decFactor.c b/src/opt/dec/decFactor.c
index 94205196..16e65b79 100644
--- a/src/opt/dec/decFactor.c
+++ b/src/opt/dec/decFactor.c
@@ -57,7 +57,7 @@ Dec_Graph_t * Dec_Factor( char * pSop )
     // derive the cover from the SOP representation
     pCover = Dec_ConvertSopToMvc( pSop );
 
-    // make sure the cover is CCS free (should be done before CST)
+    // make sure the cover is CCS ABC_FREE (should be done before CST)
     Mvc_CoverContain( pCover );
     // check for trivial functions
     if ( Mvc_CoverIsEmpty(pCover) )
@@ -130,7 +130,7 @@ Dec_Edge_t Dec_Factor_rec( Dec_Graph_t * pFForm, Mvc_Cover_t * pCover )
         return eNode;
     }
 
-    // make the quotient cube free
+    // make the quotient cube ABC_FREE
     Mvc_CoverMakeCubeFree( pQuo );
 
     // divide the cover by the quotient
diff --git a/src/opt/dec/decMan.c b/src/opt/dec/decMan.c
index 3d65ffc5..63a96966 100644
--- a/src/opt/dec/decMan.c
+++ b/src/opt/dec/decMan.c
@@ -43,13 +43,13 @@ Dec_Man_t * Dec_ManStart()
 {
     Dec_Man_t * p;
 //    int clk = clock();
-    p = ALLOC( Dec_Man_t, 1 );
+    p = ABC_ALLOC( Dec_Man_t, 1 );
     p->pMvcMem = Mvc_ManagerStart();
     p->vCubes = Vec_IntAlloc( 8 );
     p->vLits = Vec_IntAlloc( 8 );
     // canonical forms, phases, perms
     Extra_Truth4VarNPN( &p->puCanons, &p->pPhases, &p->pPerms, &p->pMap );
-//PRT( "NPN classes precomputation time", clock() - clk ); 
+//ABC_PRT( "NPN classes precomputation time", clock() - clk ); 
     return p;
 }
 
@@ -69,11 +69,11 @@ void Dec_ManStop( Dec_Man_t * p )
     Mvc_ManagerFree( p->pMvcMem );
     Vec_IntFree( p->vCubes );
     Vec_IntFree( p->vLits );
-    free( p->puCanons );
-    free( p->pPhases );
-    free( p->pPerms );
-    free( p->pMap );
-    free( p );
+    ABC_FREE( p->puCanons );
+    ABC_FREE( p->pPhases );
+    ABC_FREE( p->pPerms );
+    ABC_FREE( p->pMap );
+    ABC_FREE( p );
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/dec/decUtil.c b/src/opt/dec/decUtil.c
index aeabeac4..b8ae4b8a 100644
--- a/src/opt/dec/decUtil.c
+++ b/src/opt/dec/decUtil.c
@@ -110,17 +110,17 @@ unsigned Dec_GraphDeriveTruth( Dec_Graph_t * pGraph )
 
     // assign the elementary variables
     Dec_GraphForEachLeaf( pGraph, pNode, i )
-        pNode->pFunc = (void *)(PORT_PTRUINT_T)uTruths[i];
+        pNode->pFunc = (void *)(ABC_PTRUINT_T)uTruths[i];
 
     // compute the function for each internal node
     Dec_GraphForEachNode( pGraph, pNode, i )
     {
-        uTruth0 = (unsigned)(PORT_PTRUINT_T)Dec_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc;
-        uTruth1 = (unsigned)(PORT_PTRUINT_T)Dec_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc;
+        uTruth0 = (unsigned)(ABC_PTRUINT_T)Dec_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc;
+        uTruth1 = (unsigned)(ABC_PTRUINT_T)Dec_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc;
         uTruth0 = pNode->eEdge0.fCompl? ~uTruth0 : uTruth0;
         uTruth1 = pNode->eEdge1.fCompl? ~uTruth1 : uTruth1;
         uTruth = uTruth0 & uTruth1;
-        pNode->pFunc = (void *)(PORT_PTRUINT_T)uTruth;
+        pNode->pFunc = (void *)(ABC_PTRUINT_T)uTruth;
     }
 
     // complement the result if necessary
diff --git a/src/opt/fxu/fxu.c b/src/opt/fxu/fxu.c
index b49ef9aa..9102d289 100644
--- a/src/opt/fxu/fxu.c
+++ b/src/opt/fxu/fxu.c
@@ -44,7 +44,7 @@ static int s_MemoryPeak;
   The entries corresponding to the PI and objects with trivial covers are NULL.
   The number of extracted covers (not exceeding p->nNodesExt) is returned. 
   Two other things are important for the correct operation of this procedure:
-  (1) The input covers do not have duplicated fanins and are SCC-free. 
+  (1) The input covers do not have duplicated fanins and are SCC-ABC_FREE. 
   (2) The fanins array contains the numbers of the fanin objects.]
                
   SideEffects []
@@ -225,7 +225,7 @@ char * Fxu_MemFetch( Fxu_Matrix * p, int nBytes )
     s_MemoryTotal += nBytes;
     if ( s_MemoryPeak < s_MemoryTotal )
         s_MemoryPeak = s_MemoryTotal;
-//    return malloc( nBytes );
+//    return ABC_ALLOC( char, nBytes );
     return Extra_MmFixedEntryFetch( p->pMemMan );
 }
 
@@ -243,7 +243,7 @@ char * Fxu_MemFetch( Fxu_Matrix * p, int nBytes )
 void Fxu_MemRecycle( Fxu_Matrix * p, char * pItem, int nBytes )
 {
     s_MemoryTotal -= nBytes;
-//    free( pItem );
+//    ABC_FREE( pItem );
     Extra_MmFixedEntryRecycle( p->pMemMan, pItem );
 }
 
diff --git a/src/opt/fxu/fxu.h b/src/opt/fxu/fxu.h
index e6d0b69e..b9a56b23 100644
--- a/src/opt/fxu/fxu.h
+++ b/src/opt/fxu/fxu.h
@@ -19,10 +19,6 @@
 #ifndef __FXU_H__
 #define __FXU_H__
 
-#ifdef __cplusplus
-extern "C" {
-#endif
-
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -33,6 +29,10 @@ extern "C" {
 ///                         PARAMETERS                               ///
 ////////////////////////////////////////////////////////////////////////
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                    STRUCTURE DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/fxu/fxuCreate.c b/src/opt/fxu/fxuCreate.c
index 21dfd419..008cac46 100644
--- a/src/opt/fxu/fxuCreate.c
+++ b/src/opt/fxu/fxuCreate.c
@@ -98,13 +98,13 @@ Fxu_Matrix * Fxu_CreateMatrix( Fxu_Data_t * pData )
     // start the matrix
     p = Fxu_MatrixAllocate();
     // create the column labels 
-    p->ppVars = ALLOC( Fxu_Var *, 2 * (pData->nNodesOld + pData->nNodesExt) );
+    p->ppVars = ABC_ALLOC( Fxu_Var *, 2 * (pData->nNodesOld + pData->nNodesExt) );
     for ( i = 0; i < 2 * pData->nNodesOld; i++ )
         p->ppVars[i] = Fxu_MatrixAddVar( p );
 
     // allocate storage for all cube pairs at once
-    p->pppPairs = ALLOC( Fxu_Pair **, nCubesTotal + 100 );
-    p->ppPairs  = ALLOC( Fxu_Pair *,  nPairsStore + 100 );
+    p->pppPairs = ABC_ALLOC( Fxu_Pair **, nCubesTotal + 100 );
+    p->ppPairs  = ABC_ALLOC( Fxu_Pair *,  nPairsStore + 100 );
     memset( p->ppPairs, 0, sizeof(Fxu_Pair *) * nPairsStore );
     iCube = 0;
     iPair = 0;
@@ -133,7 +133,7 @@ Fxu_Matrix * Fxu_CreateMatrix( Fxu_Data_t * pData )
 
 
     // allocate room for the reordered literals
-    pOrder = ALLOC( int, nBitsMax );
+    pOrder = ABC_ALLOC( int, nBitsMax );
     // create the rows
     for ( i = 0; i < pData->nNodesOld; i++ )
     if ( (pSopCover = pData->vSops->pArray[i]) )
@@ -174,7 +174,7 @@ Fxu_Matrix * Fxu_CreateMatrix( Fxu_Data_t * pData )
                     Fxu_MatrixAddDivisor( p, pCube1, pCube2 );
         }
     }
-    FREE( pOrder );
+    ABC_FREE( pOrder );
 
     // consider the case when cube pairs should be preprocessed
     // before adding them to the set of divisors
diff --git a/src/opt/fxu/fxuHeapD.c b/src/opt/fxu/fxuHeapD.c
index c81ad818..9a8eb124 100644
--- a/src/opt/fxu/fxuHeapD.c
+++ b/src/opt/fxu/fxuHeapD.c
@@ -55,11 +55,11 @@ static void Fxu_HeapDoubleMoveDn( Fxu_HeapDouble * p, Fxu_Double * pDiv );
 Fxu_HeapDouble * Fxu_HeapDoubleStart()
 {
     Fxu_HeapDouble * p;
-    p = ALLOC( Fxu_HeapDouble, 1 );
+    p = ABC_ALLOC( Fxu_HeapDouble, 1 );
     memset( p, 0, sizeof(Fxu_HeapDouble) );
     p->nItems      = 0;
     p->nItemsAlloc = 10000;
-    p->pTree       = ALLOC( Fxu_Double *, p->nItemsAlloc + 1 );
+    p->pTree       = ABC_ALLOC( Fxu_Double *, p->nItemsAlloc + 1 );
     p->pTree[0]    = NULL;
     return p;
 }
@@ -79,7 +79,7 @@ Fxu_HeapDouble * Fxu_HeapDoubleStart()
 void Fxu_HeapDoubleResize( Fxu_HeapDouble * p )
 {
     p->nItemsAlloc *= 2;
-    p->pTree = REALLOC( Fxu_Double *, p->pTree, p->nItemsAlloc + 1 );
+    p->pTree = ABC_REALLOC( Fxu_Double *, p->pTree, p->nItemsAlloc + 1 );
 }
 
 /**Function*************************************************************
@@ -95,8 +95,8 @@ void Fxu_HeapDoubleResize( Fxu_HeapDouble * p )
 ***********************************************************************/
 void Fxu_HeapDoubleStop( Fxu_HeapDouble * p )
 {
-    free( p->pTree );
-    free( p );
+    ABC_FREE( p->pTree );
+    ABC_FREE( p );
 }
 
 
diff --git a/src/opt/fxu/fxuHeapS.c b/src/opt/fxu/fxuHeapS.c
index eaca8363..4a9bd3a4 100644
--- a/src/opt/fxu/fxuHeapS.c
+++ b/src/opt/fxu/fxuHeapS.c
@@ -55,11 +55,11 @@ static void Fxu_HeapSingleMoveDn( Fxu_HeapSingle * p, Fxu_Single * pSingle );
 Fxu_HeapSingle * Fxu_HeapSingleStart()
 {
     Fxu_HeapSingle * p;
-    p = ALLOC( Fxu_HeapSingle, 1 );
+    p = ABC_ALLOC( Fxu_HeapSingle, 1 );
     memset( p, 0, sizeof(Fxu_HeapSingle) );
     p->nItems      = 0;
     p->nItemsAlloc = 2000;
-    p->pTree       = ALLOC( Fxu_Single *, p->nItemsAlloc + 10 );
+    p->pTree       = ABC_ALLOC( Fxu_Single *, p->nItemsAlloc + 10 );
     p->pTree[0]    = NULL;
     return p;
 }
@@ -79,7 +79,7 @@ Fxu_HeapSingle * Fxu_HeapSingleStart()
 void Fxu_HeapSingleResize( Fxu_HeapSingle * p )
 {
     p->nItemsAlloc *= 2;
-    p->pTree = REALLOC( Fxu_Single *, p->pTree, p->nItemsAlloc + 10 );
+    p->pTree = ABC_REALLOC( Fxu_Single *, p->pTree, p->nItemsAlloc + 10 );
 }
 
 /**Function*************************************************************
@@ -97,9 +97,9 @@ void Fxu_HeapSingleStop( Fxu_HeapSingle * p )
 {
     int i;
     i = 0;
-    free( p->pTree );
+    ABC_FREE( p->pTree );
     i = 1;
-    free( p );
+    ABC_FREE( p );
 }
 
 
diff --git a/src/opt/fxu/fxuInt.h b/src/opt/fxu/fxuInt.h
index 4e3d72eb..7483c896 100644
--- a/src/opt/fxu/fxuInt.h
+++ b/src/opt/fxu/fxuInt.h
@@ -365,7 +365,7 @@ struct FxuSingle // 7 words
 #define Fxu_CubeForEachPair( pCube, pPair, i )\
   for ( i = 0;\
         i < pCube->pVar->nCubes &&\
-        (((unsigned)(PORT_PTRUINT_T)(pPair = pCube->pVar->ppPairs[pCube->iCube][i])) >= 0);\
+        (((unsigned)(ABC_PTRUINT_T)(pPair = pCube->pVar->ppPairs[pCube->iCube][i])) >= 0);\
         i++ )\
         if ( pPair )
 
@@ -421,8 +421,8 @@ extern void Fxu_MatrixRingVarsUnmark( Fxu_Matrix * p );
 // MEM_ALLOC: allocate the given number (Size) of items of type (Type)
 // MEM_FREE:  deallocate the pointer (Pointer) to the given number (Size) of items of type (Type)
 #ifdef USE_SYSTEM_MEMORY_MANAGEMENT
-#define MEM_ALLOC_FXU( Manager, Type, Size )          ((Type *)malloc( (Size) * sizeof(Type) ))
-#define MEM_FREE_FXU( Manager, Type, Size, Pointer )  if ( Pointer ) { free(Pointer); Pointer = NULL; }
+#define MEM_ALLOC_FXU( Manager, Type, Size )          ((Type *)ABC_ALLOC( char, (Size) * sizeof(Type) ))
+#define MEM_FREE_FXU( Manager, Type, Size, Pointer )  if ( Pointer ) { ABC_FREE(Pointer); Pointer = NULL; }
 #else
 #define MEM_ALLOC_FXU( Manager, Type, Size )\
         ((Type *)Fxu_MemFetch( Manager, (Size) * sizeof(Type) ))
diff --git a/src/opt/fxu/fxuMatrix.c b/src/opt/fxu/fxuMatrix.c
index 93ec7b90..590370c9 100644
--- a/src/opt/fxu/fxuMatrix.c
+++ b/src/opt/fxu/fxuMatrix.c
@@ -42,10 +42,10 @@ extern unsigned int Cudd_Prime( unsigned int p );
 Fxu_Matrix * Fxu_MatrixAllocate()
 {
     Fxu_Matrix * p;
-    p = ALLOC( Fxu_Matrix, 1 );
+    p = ABC_ALLOC( Fxu_Matrix, 1 );
     memset( p, 0, sizeof(Fxu_Matrix) );
     p->nTableSize = Cudd_Prime(10000);
-    p->pTable = ALLOC( Fxu_ListDouble, p->nTableSize );
+    p->pTable = ABC_ALLOC( Fxu_ListDouble, p->nTableSize );
     memset( p->pTable, 0, sizeof(Fxu_ListDouble) * p->nTableSize );
 #ifndef USE_SYSTEM_MEMORY_MANAGEMENT
     {
@@ -134,12 +134,12 @@ void Fxu_MatrixDelete( Fxu_Matrix * p )
 #endif
 
     Vec_PtrFree( p->vPairs );
-    FREE( p->pppPairs );
-    FREE( p->ppPairs );
-//    FREE( p->pPairsTemp );
-    FREE( p->pTable );
-    FREE( p->ppVars );
-    FREE( p );
+    ABC_FREE( p->pppPairs );
+    ABC_FREE( p->ppPairs );
+//    ABC_FREE( p->pPairsTemp );
+    ABC_FREE( p->pTable );
+    ABC_FREE( p->ppVars );
+    ABC_FREE( p );
 }
 
 
diff --git a/src/opt/fxu/fxuPair.c b/src/opt/fxu/fxuPair.c
index 87645cc7..62cc792b 100644
--- a/src/opt/fxu/fxuPair.c
+++ b/src/opt/fxu/fxuPair.c
@@ -86,7 +86,7 @@ void Fxu_PairCanonicize( Fxu_Cube ** ppCube1, Fxu_Cube ** ppCube2 )
             pLit2 = pLit2->pHNext;
             continue;
         }
-        assert( pLit1 && pLit2 ); // this is true if the covers are SCC-free
+        assert( pLit1 && pLit2 ); // this is true if the covers are SCC-ABC_FREE
         if ( pLit1->iVar > pLit2->iVar )
         { // swap the cubes
             pCubeTemp = *ppCube1;
@@ -149,7 +149,7 @@ unsigned Fxu_PairHashKeyArray( Fxu_Matrix * p, int piVarsC1[], int piVarsC2[], i
   Synopsis    [Computes the hash key of the divisor represented by the pair of cubes.]
 
   Description [Goes through the variables in both cubes. Skips the identical
-  ones (this corresponds to making the cubes cube-free). Computes the hash 
+  ones (this corresponds to making the cubes cube-ABC_FREE). Computes the hash 
   value of the cubes. Assigns the number of literals in the base and in the 
   cubes without base.]
                
@@ -178,7 +178,7 @@ unsigned Fxu_PairHashKey( Fxu_Matrix * p, Fxu_Cube * pCube1, Fxu_Cube * pCube2,
         if ( pLit1 && pLit2 )
         {
             if ( pLit1->iVar == pLit2->iVar )
-            { // ensure cube-free
+            { // ensure cube-ABC_FREE
                 pLit1 = pLit1->pHNext;
                 pLit2 = pLit2->pHNext;
                 // add this literal to the base
@@ -452,8 +452,8 @@ void Fxu_PairAllocStorage( Fxu_Var * pVar, int nCubes )
 //    assert( pVar->nCubes == 0 );
     pVar->nCubes  = nCubes;
     // allocate memory for all the pairs
-    pVar->ppPairs    = ALLOC( Fxu_Pair **, nCubes );
-    pVar->ppPairs[0] = ALLOC( Fxu_Pair *,  nCubes * nCubes );
+    pVar->ppPairs    = ABC_ALLOC( Fxu_Pair **, nCubes );
+    pVar->ppPairs[0] = ABC_ALLOC( Fxu_Pair *,  nCubes * nCubes );
     memset( pVar->ppPairs[0], 0, sizeof(Fxu_Pair *) * nCubes * nCubes );
     for ( k = 1; k < nCubes; k++ )
         pVar->ppPairs[k] = pVar->ppPairs[k-1] + nCubes;
@@ -497,8 +497,8 @@ void Fxu_PairFreeStorage( Fxu_Var * pVar )
 {
     if ( pVar->ppPairs )
     {
-        FREE( pVar->ppPairs[0] );
-        FREE( pVar->ppPairs );
+        ABC_FREE( pVar->ppPairs[0] );
+        ABC_FREE( pVar->ppPairs );
     }
 }
 
diff --git a/src/opt/fxu/fxuPrint.c b/src/opt/fxu/fxuPrint.c
index 232b109a..652a830e 100644
--- a/src/opt/fxu/fxuPrint.c
+++ b/src/opt/fxu/fxuPrint.c
@@ -161,7 +161,7 @@ void Fxu_MatrixPrintDivisorProfile( FILE * pFile, Fxu_Matrix * p )
     int i;
 
     WeightMax = Fxu_HeapDoubleReadMaxWeight( p->pHeapDouble );
-    pProfile = ALLOC( int, (WeightMax + 1) );
+    pProfile = ABC_ALLOC( int, (WeightMax + 1) );
     memset( pProfile, 0, sizeof(int) * (WeightMax + 1) );
 
     Counter1 = 0;
@@ -184,7 +184,7 @@ void Fxu_MatrixPrintDivisorProfile( FILE * pFile, Fxu_Matrix * p )
         if ( pProfile[i] )
             fprintf( pFile, "Weight   %3d divisors = %6d\n", i, pProfile[i] );
     fprintf( pFile, "End of divisor profile printout\n" );
-    FREE( pProfile );
+    ABC_FREE( pProfile );
 }
 
 
diff --git a/src/opt/fxu/fxuReduce.c b/src/opt/fxu/fxuReduce.c
index 38032bfa..6b892971 100644
--- a/src/opt/fxu/fxuReduce.c
+++ b/src/opt/fxu/fxuReduce.c
@@ -40,7 +40,7 @@ static int Fxu_CountPairDiffs( char * pCover, unsigned char pDiffs[] );
   number of pairs in existence. This procedure adds to the storage of
   divisors exactly the given number of pairs (nPairsMax) while taking
   first those pairs that have the smallest number of literals in their
-  cube-free form.]
+  cube-ABC_FREE form.]
                
   SideEffects []
 
@@ -64,7 +64,7 @@ int Fxu_PreprocessCubePairs( Fxu_Matrix * p, Vec_Ptr_t * vCovers, int nPairsTota
     assert( nPairsMax < nPairsTotal );
 
     // allocate storage for counter of diffs
-    pnLitsDiff = ALLOC( unsigned char, nPairsTotal );
+    pnLitsDiff = ABC_ALLOC( unsigned char, nPairsTotal );
     // go through the covers and precompute the distances between the pairs
     iPair    =  0;
     nBitsMax = -1;
@@ -83,7 +83,7 @@ int Fxu_PreprocessCubePairs( Fxu_Matrix * p, Vec_Ptr_t * vCovers, int nPairsTota
     assert( iPair == nPairsTotal );
 
     // allocate storage for counters of cube pairs by difference
-    pnPairCounters = ALLOC( int, 2 * nBitsMax );
+    pnPairCounters = ABC_ALLOC( int, 2 * nBitsMax );
     memset( pnPairCounters, 0, sizeof(int) * 2 * nBitsMax );
     // count the number of different pairs
     for ( k = 0; k < nPairsTotal; k++ )
@@ -92,16 +92,16 @@ int Fxu_PreprocessCubePairs( Fxu_Matrix * p, Vec_Ptr_t * vCovers, int nPairsTota
     // so that there would be exactly pPairsMax pairs
     if ( pnPairCounters[0] != 0 )
     {
-        printf( "The SOPs of the nodes are not cube-free. Run \"bdd; sop\" before \"fx\".\n" );
+        printf( "The SOPs of the nodes are not cube-ABC_FREE. Run \"bdd; sop\" before \"fx\".\n" );
         return 0;
     }
     if ( pnPairCounters[1] != 0 )
     {
-        printf( "The SOPs of the nodes are not SCC-free. Run \"bdd; sop\" before \"fx\".\n" );
+        printf( "The SOPs of the nodes are not SCC-ABC_FREE. Run \"bdd; sop\" before \"fx\".\n" );
         return 0;
     }
-    assert( pnPairCounters[0] == 0 ); // otherwise, covers are not dup-free
-    assert( pnPairCounters[1] == 0 ); // otherwise, covers are not SCC-free
+    assert( pnPairCounters[0] == 0 ); // otherwise, covers are not dup-ABC_FREE
+    assert( pnPairCounters[1] == 0 ); // otherwise, covers are not SCC-ABC_FREE
     nSum = 0;
     for ( k = 0; k < 2 * nBitsMax; k++ )
     {
@@ -113,7 +113,7 @@ int Fxu_PreprocessCubePairs( Fxu_Matrix * p, Vec_Ptr_t * vCovers, int nPairsTota
             break;
         }
     }
-    FREE( pnPairCounters );
+    ABC_FREE( pnPairCounters );
 
     // set to 0 all the pairs above the cut-off number and quantity
     iQuant = 0;
@@ -156,8 +156,8 @@ int Fxu_PreprocessCubePairs( Fxu_Matrix * p, Vec_Ptr_t * vCovers, int nPairsTota
                     }
         }
     assert( iPair == nPairsTotal );
-    FREE( pnLitsDiff );
-//PRT( "Preprocess", clock() - clk );
+    ABC_FREE( pnLitsDiff );
+//ABC_PRT( "Preprocess", clock() - clk );
     return 1;
 }
 
@@ -171,7 +171,7 @@ int Fxu_PreprocessCubePairs( Fxu_Matrix * p, Vec_Ptr_t * vCovers, int nPairsTota
   entries as there are different pairs of cubes in the cover: n(n-1)/2.
   Fills out the array pDiffs with the following info: For each cube
   pair, included in the array is the number of literals in both cubes
-  after they are made cube free.]
+  after they are made cube ABC_FREE.]
                
   SideEffects []
 
diff --git a/src/opt/fxu/fxuSelect.c b/src/opt/fxu/fxuSelect.c
index b9265487..20f5ab97 100644
--- a/src/opt/fxu/fxuSelect.c
+++ b/src/opt/fxu/fxuSelect.c
@@ -416,7 +416,7 @@ void Fxu_MatrixGetDoubleVars( Fxu_Matrix * p, Fxu_Double * pDouble,
         if ( pLit1 && pLit2 )
         {
             if ( pLit1->iVar == pLit2->iVar )
-            { // ensure cube-free
+            { // ensure cube-ABC_FREE
                 pLit1 = pLit1->pHNext;
                 pLit2 = pLit2->pHNext;
             }
diff --git a/src/opt/fxu/fxuSingle.c b/src/opt/fxu/fxuSingle.c
index d2e3607c..6e90a2a2 100644
--- a/src/opt/fxu/fxuSingle.c
+++ b/src/opt/fxu/fxuSingle.c
@@ -59,11 +59,11 @@ void Fxu_MatrixComputeSingles( Fxu_Matrix * p, int fUse0, int nSingleMax )
         int * pWeigtCounts, nDivCount, Weight, i, c;;
         assert( Vec_PtrSize(vSingles) % 3 == 0 );
         // count how many divisors have the given weight
-        pWeigtCounts = ALLOC( int, 1000 );
+        pWeigtCounts = ABC_ALLOC( int, 1000 );
         memset( pWeigtCounts, 0, sizeof(int) * 1000 );
         for ( i = 2; i < Vec_PtrSize(vSingles); i += 3 )
         {
-            Weight = (int)(PORT_PTRUINT_T)Vec_PtrEntry(vSingles, i);
+            Weight = (int)(ABC_PTRUINT_T)Vec_PtrEntry(vSingles, i);
             if ( Weight >= 999 )
                 pWeigtCounts[999]++;
             else
@@ -77,12 +77,12 @@ void Fxu_MatrixComputeSingles( Fxu_Matrix * p, int fUse0, int nSingleMax )
             if ( nDivCount >= nSingleMax )
                 break;
         }
-        free( pWeigtCounts );
+        ABC_FREE( pWeigtCounts );
         // collect singles with the given costs
         k = 0;
         for ( i = 2; i < Vec_PtrSize(vSingles); i += 3 )
         {
-            Weight = (int)(PORT_PTRUINT_T)Vec_PtrEntry(vSingles, i);
+            Weight = (int)(ABC_PTRUINT_T)Vec_PtrEntry(vSingles, i);
             if ( Weight < c )
                 continue;
             Vec_PtrWriteEntry( vSingles, k++, Vec_PtrEntry(vSingles, i-2) );
@@ -102,7 +102,7 @@ void Fxu_MatrixComputeSingles( Fxu_Matrix * p, int fUse0, int nSingleMax )
         Fxu_MatrixAddSingle( p, 
             Vec_PtrEntry(vSingles,i), 
             Vec_PtrEntry(vSingles,i+1), 
-            (int)(PORT_PTRUINT_T)Vec_PtrEntry(vSingles,i+2) );
+            (int)(ABC_PTRUINT_T)Vec_PtrEntry(vSingles,i+2) );
     }
     Vec_PtrFree( vSingles );
 }
@@ -159,7 +159,7 @@ void Fxu_MatrixComputeSinglesOneCollect( Fxu_Matrix * p, Fxu_Var * pVar, Vec_Ptr
         {
             Vec_PtrPush( vSingles, pVar2 );
             Vec_PtrPush( vSingles, pVar );
-            Vec_PtrPush( vSingles, (void *)(PORT_PTRUINT_T)WeightCur );
+            Vec_PtrPush( vSingles, (void *)(ABC_PTRUINT_T)WeightCur );
         }
     }
 
diff --git a/src/opt/fxu/fxuUpdate.c b/src/opt/fxu/fxuUpdate.c
index 274f79f6..cdbe313d 100644
--- a/src/opt/fxu/fxuUpdate.c
+++ b/src/opt/fxu/fxuUpdate.c
@@ -344,7 +344,7 @@ void Fxu_UpdateMatrixDoubleCreateCubes( Fxu_Matrix * p, Fxu_Cube * pCube1, Fxu_C
         if ( pLit1 && pLit2 )
         {
             if ( pLit1->iVar == pLit2->iVar )
-            { // skip the cube free part
+            { // skip the cube ABC_FREE part
                 pLit1 = pLit1->pHNext;
                 pLit2 = pLit2->pHNext;
                 nBase++;
diff --git a/src/opt/lpk/lpk.h b/src/opt/lpk/lpk.h
index 2a642db2..d7e4af29 100644
--- a/src/opt/lpk/lpk.h
+++ b/src/opt/lpk/lpk.h
@@ -21,10 +21,6 @@
 #ifndef __LPK_H__
 #define __LPK_H__
 
-#ifdef __cplusplus
-extern "C" {
-#endif 
-
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -33,6 +29,10 @@ extern "C" {
 ///                         PARAMETERS                               ///
 ////////////////////////////////////////////////////////////////////////
 
+#ifdef __cplusplus
+extern "C" {
+#endif 
+
 ////////////////////////////////////////////////////////////////////////
 ///                         BASIC TYPES                              ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/lpk/lpkAbcDsd.c b/src/opt/lpk/lpkAbcDsd.c
index a1cd9def..c2a46d3e 100644
--- a/src/opt/lpk/lpkAbcDsd.c
+++ b/src/opt/lpk/lpkAbcDsd.c
@@ -420,7 +420,7 @@ Kit_DsdPrint( stdout, pNtks[i] );
             pvBSets[i][k] = Lpk_MergeBoundSets( pvBSets[i+1][2*k+0], pvBSets[i+1][2*k+1], p->nLutK - nCofDepth );
     // compare bound-sets
     Lpk_FunCompareBoundSets( p, pvBSets[0][0], nCofDepth, uNonDecSupp, uLateArrSupp, pRes );
-    // free the bound sets
+    // ABC_FREE the bound sets
     for ( i = nCofDepth; i >= 0; i-- )
         for ( k = 0; k < (1<<i); k++ )
             Vec_IntFree( pvBSets[i][k] );
@@ -539,7 +539,7 @@ Lpk_Res_t * Lpk_DsdAnalize( Lpk_Man_t * pMan, Lpk_Fun_t * p, int nShared )
     }
 
 finish:
-    // free the networks
+    // ABC_FREE the networks
     for ( i = 0; i < (1<<nShared); i++ )
         if ( pNtks[i] )
             Kit_DsdNtkFree( pNtks[i] );
diff --git a/src/opt/lpk/lpkAbcUtil.c b/src/opt/lpk/lpkAbcUtil.c
index 3f917ce2..ae295624 100644
--- a/src/opt/lpk/lpkAbcUtil.c
+++ b/src/opt/lpk/lpkAbcUtil.c
@@ -42,7 +42,7 @@
 Lpk_Fun_t * Lpk_FunAlloc( int nVars )
 {
     Lpk_Fun_t * p;
-    p = (Lpk_Fun_t *)malloc( sizeof(Lpk_Fun_t) + sizeof(unsigned) * Kit_TruthWordNum(nVars) * 3 );
+    p = (Lpk_Fun_t *)ABC_ALLOC( char, sizeof(Lpk_Fun_t) + sizeof(unsigned) * Kit_TruthWordNum(nVars) * 3 );
     memset( p, 0, sizeof(Lpk_Fun_t) );
     return p;
 }
@@ -60,7 +60,7 @@ Lpk_Fun_t * Lpk_FunAlloc( int nVars )
 ***********************************************************************/
 void Lpk_FunFree( Lpk_Fun_t * p )
 {
-    free( p );
+    ABC_FREE( p );
 }
 
 /**Function*************************************************************
diff --git a/src/opt/lpk/lpkCore.c b/src/opt/lpk/lpkCore.c
index d8dd15b7..7cc4b154 100644
--- a/src/opt/lpk/lpkCore.c
+++ b/src/opt/lpk/lpkCore.c
@@ -45,7 +45,7 @@ void Lpk_IfManStart( Lpk_Man_t * p )
     If_Par_t * pPars;
     assert( p->pIfMan == NULL );
     // set defaults
-    pPars = ALLOC( If_Par_t, 1 );
+    pPars = ABC_ALLOC( If_Par_t, 1 );
     memset( pPars, 0, sizeof(If_Par_t) );
     // user-controlable paramters
     pPars->nLutSize    =  p->pPars->nLutSize;
@@ -75,7 +75,7 @@ void Lpk_IfManStart( Lpk_Man_t * p )
     // start the mapping manager and set its parameters
     p->pIfMan = If_ManStart( pPars );
     If_ManSetupSetAll( p->pIfMan, 1000 );
-    p->pIfMan->pPars->pTimesArr = ALLOC( float, 32 );
+    p->pIfMan->pPars->pTimesArr = ABC_ALLOC( float, 32 );
 }
 
 /**Function*************************************************************
@@ -100,7 +100,7 @@ int Lpk_NodeHasChanged( Lpk_Man_t * p, int iNode )
     Vec_PtrForEachEntry( vNodes, pTemp, i )
     {
         // check if the node has changed
-        pTemp = Abc_NtkObj( p->pNtk, (int)(PORT_PTRUINT_T)pTemp );
+        pTemp = Abc_NtkObj( p->pNtk, (int)(ABC_PTRUINT_T)pTemp );
         if ( pTemp == NULL )
             return 1;
         // check if the number of fanouts has changed
@@ -563,7 +563,7 @@ int Lpk_Resynthesize( Abc_Ntk_t * pNtk, Lpk_Par_t * pPars )
 /*
     // save the number of fanouts of all objects
     nObjMax = Abc_NtkObjNumMax( pNtk );
-    pnFanouts = ALLOC( int, nObjMax );
+    pnFanouts = ABC_ALLOC( int, nObjMax );
     memset( pnFanouts, 0, sizeof(int) * nObjMax );
     Abc_NtkForEachObj( pNtk, pObj, i )
         pnFanouts[pObj->Id] = Abc_ObjFanoutNum(pObj);
@@ -654,18 +654,18 @@ int Lpk_Resynthesize( Abc_Ntk_t * pNtk, Lpk_Par_t * pPars )
         p->timeTotal = clock() - clk;
         p->timeEval  = p->timeEval  - p->timeMap;
         p->timeOther = p->timeTotal - p->timeCuts - p->timeTruth - p->timeEval - p->timeMap;
-        PRTP( "Cuts  ", p->timeCuts,  p->timeTotal );
-        PRTP( "Truth ", p->timeTruth, p->timeTotal );
-        PRTP( "CSupps", p->timeSupps, p->timeTotal );
-        PRTP( "Eval  ", p->timeEval,  p->timeTotal );
-        PRTP( " MuxAn", p->timeEvalMuxAn, p->timeEval );
-        PRTP( " MuxSp", p->timeEvalMuxSp, p->timeEval );
-        PRTP( " DsdAn", p->timeEvalDsdAn, p->timeEval );
-        PRTP( " DsdSp", p->timeEvalDsdSp, p->timeEval );
-        PRTP( " Other", p->timeEval-p->timeEvalMuxAn-p->timeEvalMuxSp-p->timeEvalDsdAn-p->timeEvalDsdSp, p->timeEval );
-        PRTP( "Map   ", p->timeMap,   p->timeTotal );
-        PRTP( "Other ", p->timeOther, p->timeTotal );
-        PRTP( "TOTAL ", p->timeTotal, p->timeTotal );
+        ABC_PRTP( "Cuts  ", p->timeCuts,  p->timeTotal );
+        ABC_PRTP( "Truth ", p->timeTruth, p->timeTotal );
+        ABC_PRTP( "CSupps", p->timeSupps, p->timeTotal );
+        ABC_PRTP( "Eval  ", p->timeEval,  p->timeTotal );
+        ABC_PRTP( " MuxAn", p->timeEvalMuxAn, p->timeEval );
+        ABC_PRTP( " MuxSp", p->timeEvalMuxSp, p->timeEval );
+        ABC_PRTP( " DsdAn", p->timeEvalDsdAn, p->timeEval );
+        ABC_PRTP( " DsdSp", p->timeEvalDsdSp, p->timeEval );
+        ABC_PRTP( " Other", p->timeEval-p->timeEvalMuxAn-p->timeEvalMuxSp-p->timeEvalDsdAn-p->timeEvalDsdSp, p->timeEval );
+        ABC_PRTP( "Map   ", p->timeMap,   p->timeTotal );
+        ABC_PRTP( "Other ", p->timeOther, p->timeTotal );
+        ABC_PRTP( "TOTAL ", p->timeTotal, p->timeTotal );
     }
 
     Lpk_ManStop( p );
diff --git a/src/opt/lpk/lpkCut.c b/src/opt/lpk/lpkCut.c
index a2f46b09..6f0eed84 100644
--- a/src/opt/lpk/lpkCut.c
+++ b/src/opt/lpk/lpkCut.c
@@ -46,7 +46,7 @@ CloudNode * Lpk_CutTruthBdd_rec( CloudManager * dd, Hop_Man_t * pMan, Hop_Obj_t
     assert( !Hop_IsComplement(pObj) );
     if ( pObj->pData )
     {
-        assert( ((unsigned)(PORT_PTRUINT_T)pObj->pData) & 0xffff0000 );
+        assert( ((unsigned)(ABC_PTRUINT_T)pObj->pData) & 0xffff0000 );
         return pObj->pData;
     }
     // get the plan for a new truth table
@@ -103,7 +103,7 @@ CloudNode * Lpk_CutTruthBdd( Lpk_Man_t * p, Lpk_Cut_t * pCut )
         // set the initial truth tables at the fanins
         Abc_ObjForEachFanin( pObj, pFanin, k )
         {
-            assert( ((unsigned)(PORT_PTRUINT_T)pFanin->pCopy) & 0xffff0000 );
+            assert( ((unsigned)(ABC_PTRUINT_T)pFanin->pCopy) & 0xffff0000 );
             Hop_ManPi( pManHop, k )->pData = pFanin->pCopy;
         }
         // compute the truth table of internal nodes
@@ -138,7 +138,7 @@ unsigned * Lpk_CutTruth_rec( Hop_Man_t * pMan, Hop_Obj_t * pObj, int nVars, Vec_
     assert( !Hop_IsComplement(pObj) );
     if ( pObj->pData )
     {
-        assert( ((unsigned)(PORT_PTRUINT_T)pObj->pData) & 0xffff0000 );
+        assert( ((unsigned)(ABC_PTRUINT_T)pObj->pData) & 0xffff0000 );
         return pObj->pData;
     }
     // get the plan for a new truth table
@@ -194,7 +194,7 @@ unsigned * Lpk_CutTruth( Lpk_Man_t * p, Lpk_Cut_t * pCut, int fInv )
         // set the initial truth tables at the fanins
         Abc_ObjForEachFanin( pObj, pFanin, k )
         {
-            assert( ((unsigned)(PORT_PTRUINT_T)pFanin->pCopy) & 0xffff0000 );
+            assert( ((unsigned)(ABC_PTRUINT_T)pFanin->pCopy) & 0xffff0000 );
             Hop_ManPi( pManHop, k )->pData = pFanin->pCopy;
         }
         // compute the truth table of internal nodes
@@ -209,7 +209,7 @@ unsigned * Lpk_CutTruth( Lpk_Man_t * p, Lpk_Cut_t * pCut, int fInv )
     if ( fInv == 0 )
     {
         pTruth = Vec_PtrEntry( p->vTtNodes, iCount++ );
-        Kit_TruthCopy( pTruth, (unsigned *)(PORT_PTRUINT_T)pObj->pCopy, pCut->nLeaves );
+        Kit_TruthCopy( pTruth, (unsigned *)(ABC_PTRUINT_T)pObj->pCopy, pCut->nLeaves );
     }
     assert( iCount <= Vec_PtrSize(p->vTtNodes) );
     return pTruth;
@@ -244,14 +244,14 @@ void Lpk_NodeRecordImpact( Lpk_Man_t * p )
             if ( pNode->fMarkC )
                 continue;
             pNode->fMarkC = 1;
-            Vec_PtrPush( vNodes, (void *)(PORT_PTRUINT_T)pNode->Id );
-            Vec_PtrPush( vNodes, (void *)(PORT_PTRUINT_T)Abc_ObjFanoutNum(pNode) );
+            Vec_PtrPush( vNodes, (void *)(ABC_PTRUINT_T)pNode->Id );
+            Vec_PtrPush( vNodes, (void *)(ABC_PTRUINT_T)Abc_ObjFanoutNum(pNode) );
         }
     }
     // clear the marks
     Vec_PtrForEachEntry( vNodes, pNode, i )
     {
-        pNode = Abc_NtkObj( p->pNtk, (int)(PORT_PTRUINT_T)pNode );
+        pNode = Abc_NtkObj( p->pNtk, (int)(ABC_PTRUINT_T)pNode );
         pNode->fMarkC = 0;
         i++;
     }
@@ -281,7 +281,7 @@ int Lpk_NodeCutsCheckDsd( Lpk_Man_t * p, Lpk_Cut_t * pCut )
     {
         assert( pObj->fMarkA == 0 );
         pObj->fMarkA = 1;
-        pObj->pCopy = (void *)(PORT_PTRUINT_T)i;
+        pObj->pCopy = (void *)(ABC_PTRUINT_T)i;
     }
     // ref leaves pointed from the internal nodes
     nCands = 0;
@@ -290,7 +290,7 @@ int Lpk_NodeCutsCheckDsd( Lpk_Man_t * p, Lpk_Cut_t * pCut )
         fLeavesOnly = 1;
         Abc_ObjForEachFanin( pObj, pFanin, k )
             if ( pFanin->fMarkA )
-                p->pRefs[(int)(PORT_PTRUINT_T)pFanin->pCopy]++;
+                p->pRefs[(int)(ABC_PTRUINT_T)pFanin->pCopy]++;
             else
                 fLeavesOnly = 0;
         if ( fLeavesOnly )
@@ -304,7 +304,7 @@ int Lpk_NodeCutsCheckDsd( Lpk_Man_t * p, Lpk_Cut_t * pCut )
         Abc_ObjForEachFanin( pObj, pFanin, k )
         {
             assert( pFanin->fMarkA == 1 );
-            if ( p->pRefs[(int)(PORT_PTRUINT_T)pFanin->pCopy] > 1 )
+            if ( p->pRefs[(int)(ABC_PTRUINT_T)pFanin->pCopy] > 1 )
                 break;
         }
         if ( k == Abc_ObjFaninNum(pObj) )
diff --git a/src/opt/lpk/lpkInt.h b/src/opt/lpk/lpkInt.h
index 960599e4..26bb846a 100644
--- a/src/opt/lpk/lpkInt.h
+++ b/src/opt/lpk/lpkInt.h
@@ -21,10 +21,6 @@
 #ifndef __LPK_INT_H__
 #define __LPK_INT_H__
 
-#ifdef __cplusplus
-extern "C" {
-#endif 
-
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -38,6 +34,10 @@ extern "C" {
 ///                         PARAMETERS                               ///
 ////////////////////////////////////////////////////////////////////////
 
+#ifdef __cplusplus
+extern "C" {
+#endif 
+
 ////////////////////////////////////////////////////////////////////////
 ///                         BASIC TYPES                              ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/lpk/lpkMan.c b/src/opt/lpk/lpkMan.c
index af6a5307..024f724a 100644
--- a/src/opt/lpk/lpkMan.c
+++ b/src/opt/lpk/lpkMan.c
@@ -45,7 +45,7 @@ Lpk_Man_t * Lpk_ManStart( Lpk_Par_t * pPars )
     int i, nWords;
     assert( pPars->nLutsMax <= 16 );
     assert( pPars->nVarsMax > 0 && pPars->nVarsMax <= 16 );
-    p = ALLOC( Lpk_Man_t, 1 );
+    p = ABC_ALLOC( Lpk_Man_t, 1 );
     memset( p, 0, sizeof(Lpk_Man_t) );
     p->pPars = pPars;
     p->nCutsMax = LPK_CUTS_MAX;
@@ -61,7 +61,7 @@ Lpk_Man_t * Lpk_ManStart( Lpk_Par_t * pPars )
     p->vBddInv = Vec_IntAlloc( 256 );
     // allocate temporary storage for truth tables
     nWords = Kit_TruthWordNum(pPars->nVarsMax);
-    p->ppTruths[0][0] = ALLOC( unsigned, 32 * nWords );
+    p->ppTruths[0][0] = ABC_ALLOC( unsigned, 32 * nWords );
     p->ppTruths[1][0] = p->ppTruths[0][0] + 1 * nWords;
     for ( i = 1; i < 2; i++ )
         p->ppTruths[1][i] = p->ppTruths[1][0] + i * nWords;
@@ -91,7 +91,7 @@ Lpk_Man_t * Lpk_ManStart( Lpk_Par_t * pPars )
 void Lpk_ManStop( Lpk_Man_t * p )
 {
     int i;
-    free( p->ppTruths[0][0] );
+    ABC_FREE( p->ppTruths[0][0] );
     Vec_IntFree( p->vBddDir );
     Vec_IntFree( p->vBddInv );
     Vec_IntFree( p->vMemory );
@@ -102,7 +102,7 @@ void Lpk_ManStop( Lpk_Man_t * p )
     {
         void * pPars = p->pIfMan->pPars;
         If_ManStop( p->pIfMan );
-        free( pPars );
+        ABC_FREE( pPars );
     }
     if ( p->vLevels )
         Vec_VecFree( p->vLevels );
@@ -112,7 +112,7 @@ void Lpk_ManStop( Lpk_Man_t * p )
     Vec_IntFree( p->vCover );
     Vec_PtrFree( p->vTtElems );
     Vec_PtrFree( p->vTtNodes );
-    free( p );
+    ABC_FREE( p );
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/lpk/lpkMulti.c b/src/opt/lpk/lpkMulti.c
index 3d2093e7..b013570e 100644
--- a/src/opt/lpk/lpkMulti.c
+++ b/src/opt/lpk/lpkMulti.c
@@ -375,7 +375,7 @@ If_Obj_t * Lpk_MapTreeMulti( Lpk_Man_t * p, unsigned * pTruth, int nVars, If_Obj
 
     // allocate storage for cofactors
     nMemSize = Kit_TruthWordNum(nVars);
-    ppCofs[0][0] = ALLOC( unsigned, 32 * nMemSize );
+    ppCofs[0][0] = ABC_ALLOC( unsigned, 32 * nMemSize );
     nSize = 0;
     for ( i = 0; i < 4; i++ )
     for ( k = 0; k < 8; k++ )
@@ -492,11 +492,11 @@ If_Obj_t * Lpk_MapTreeMulti( Lpk_Man_t * p, unsigned * pTruth, int nVars, If_Obj
         printf( "Verification failed.\n" );
 
 
-    // free the networks
+    // ABC_FREE the networks
     for ( i = 0; i < 8; i++ )
         if ( ppNtks[i] )
             Kit_DsdNtkFree( ppNtks[i] );
-    free( ppCofs[0][0] );
+    ABC_FREE( ppCofs[0][0] );
 
     return pResult;
 }
diff --git a/src/opt/lpk/lpkSets.c b/src/opt/lpk/lpkSets.c
index 90e46863..6cb3f12d 100644
--- a/src/opt/lpk/lpkSets.c
+++ b/src/opt/lpk/lpkSets.c
@@ -362,7 +362,7 @@ unsigned Lpk_MapSuppRedDecSelect( Lpk_Man_t * p, unsigned * pTruth, int nVars, i
         Lpk_PrintSets( vSets0 );
         if ( fVerbose )
         Lpk_PrintSets( vSets1 );
-        // free the networks
+        // ABC_FREE the networks
         Kit_DsdNtkFree( ppNtks[0] );
         Kit_DsdNtkFree( ppNtks[1] );
         // evaluate the pair
diff --git a/src/opt/mfs/mfs.h b/src/opt/mfs/mfs.h
index bddb9328..375f93b7 100644
--- a/src/opt/mfs/mfs.h
+++ b/src/opt/mfs/mfs.h
@@ -21,10 +21,6 @@
 #ifndef __MFS_H__
 #define __MFS_H__
 
-#ifdef __cplusplus
-extern "C" {
-#endif
-
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -33,6 +29,10 @@ extern "C" {
 ///                         PARAMETERS                               ///
 ////////////////////////////////////////////////////////////////////////
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                         BASIC TYPES                              ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/mfs/mfsCore.c b/src/opt/mfs/mfsCore.c
index e8820acd..456b5d71 100644
--- a/src/opt/mfs/mfsCore.c
+++ b/src/opt/mfs/mfsCore.c
@@ -63,16 +63,15 @@ void Abc_NtkMfsParsDefault( Mfs_Par_t * pPars )
 int Abc_NtkMfsEdgePower( Mfs_Man_t * p, Abc_Obj_t * pNode )
 {
     Abc_Obj_t * pFanin;
-    float * pProbab = (float *)p->vProbs->pArray;
     int i;
     // try replacing area critical fanins
     Abc_ObjForEachFanin( pNode, pFanin, i )
     {
-        if ( pProbab[pFanin->Id] >= 0.4 )
+        if ( Abc_MfsObjProb(p, pFanin) >= 0.4 )
         {
             if ( Abc_NtkMfsSolveSatResub( p, pNode, i, 0, 0 ) )
                 return 1;
-        } else if ( pProbab[pFanin->Id] >= 0.3 )
+        } else if ( Abc_MfsObjProb(p, pFanin) >= 0.3 )
         {
             if ( Abc_NtkMfsSolveSatResub( p, pNode, i, 1, 0 ) )
                 return 1;
@@ -86,7 +85,6 @@ int Abc_WinNode(Mfs_Man_t * p, Abc_Obj_t *pNode)
 {
 //    int clk;
 //    Abc_Obj_t * pFanin;
-    float * pProbab = (float *)p->vProbs->pArray;
 //    int i;
 
     p->nNodesTried++;
@@ -120,7 +118,6 @@ int Abc_NtkMfsPowerResubNode( Mfs_Man_t * p, Abc_Obj_t * pNode )
 {
     int clk;
     Abc_Obj_t * pFanin;
-    float * pProbab = (float *)p->vProbs->pArray;
     int i;
 
     if (Abc_WinNode(p, pNode)  // something wrong
@@ -130,11 +127,11 @@ int Abc_NtkMfsPowerResubNode( Mfs_Man_t * p, Abc_Obj_t * pNode )
     // Abc_NtkMfsEdgePower( p, pNode );
     // try replacing area critical fanins
     Abc_ObjForEachFanin( pNode, pFanin, i )
-        if ( pProbab[pFanin->Id] >= 0.37 && Abc_NtkMfsSolveSatResub( p, pNode, i, 0, 0 ) )
+        if ( Abc_MfsObjProb(p, pFanin) >= 0.37 && Abc_NtkMfsSolveSatResub( p, pNode, i, 0, 0 ) )
             return 1;
 
     Abc_ObjForEachFanin( pNode, pFanin, i )
-        if ( pProbab[pFanin->Id] >= 0.1 && Abc_NtkMfsSolveSatResub( p, pNode, i, 1, 0 ) )
+        if ( Abc_MfsObjProb(p, pFanin) >= 0.1 && Abc_NtkMfsSolveSatResub( p, pNode, i, 1, 0 ) )
             return 1;
 
     if ( Abc_ObjFaninNum(pNode) == p->nFaninMax )
@@ -142,7 +139,7 @@ int Abc_NtkMfsPowerResubNode( Mfs_Man_t * p, Abc_Obj_t * pNode )
 
     // try replacing area critical fanins while adding two new fanins
     Abc_ObjForEachFanin( pNode, pFanin, i )
-            if ( pProbab[pFanin->Id] >= 0.37 && Abc_NtkMfsSolveSatResub2( p, pNode, i, -1 ) )
+            if ( Abc_MfsObjProb(p, pFanin) >= 0.37 && Abc_NtkMfsSolveSatResub2( p, pNode, i, -1 ) )
                 return 1;
         }
     return 0;
@@ -157,7 +154,6 @@ Abc_NtkMfsPowerResub( Mfs_Man_t * p, Mfs_Par_t * pPars)
     Abc_Obj_t *pFanin, *pNode;
     Abc_Ntk_t *pNtk = p->pNtk;
     int nFaninMax = Abc_NtkGetFaninMax(p->pNtk);
-    float * pProbab = (float *)p->vProbs->pArray;
 
     Abc_NtkForEachNode( pNtk, pNode, k )
     {
@@ -172,7 +168,7 @@ Abc_NtkMfsPowerResub( Mfs_Man_t * p, Mfs_Par_t * pPars)
         // Abc_NtkMfsEdgePower( p, pNode );
         // try replacing area critical fanins
         Abc_ObjForEachFanin( pNode, pFanin, i )
-            if ( pProbab[pFanin->Id] >= 0.35 && Abc_NtkMfsSolveSatResub( p, pNode, i, 0, 0 ) )
+            if ( Abc_MfsObjProb(p, pFanin) >= 0.35 && Abc_NtkMfsSolveSatResub( p, pNode, i, 0, 0 ) )
                 continue;
     }
 
@@ -189,7 +185,7 @@ Abc_NtkMfsPowerResub( Mfs_Man_t * p, Mfs_Par_t * pPars)
         // Abc_NtkMfsEdgePower( p, pNode );
         // try replacing area critical fanins
         Abc_ObjForEachFanin( pNode, pFanin, i )
-            if ( pProbab[pFanin->Id] >= 0.35 && Abc_NtkMfsSolveSatResub( p, pNode, i, 0, 0 ) )
+            if ( Abc_MfsObjProb(p, pFanin) >= 0.35 && Abc_NtkMfsSolveSatResub( p, pNode, i, 0, 0 ) )
                 continue;
     }
 
@@ -203,7 +199,7 @@ Abc_NtkMfsPowerResub( Mfs_Man_t * p, Mfs_Par_t * pPars)
             continue;
 
         Abc_ObjForEachFanin( pNode, pFanin, i )
-            if ( pProbab[pFanin->Id] >= 0.2 && Abc_NtkMfsSolveSatResub( p, pNode, i, 1, 0 ) )
+            if ( Abc_MfsObjProb(p, pFanin) >= 0.2 && Abc_NtkMfsSolveSatResub( p, pNode, i, 1, 0 ) )
                 continue;
     }
 /*
@@ -217,7 +213,7 @@ Abc_NtkMfsPowerResub( Mfs_Man_t * p, Mfs_Par_t * pPars)
             continue;
 
         Abc_ObjForEachFanin( pNode, pFanin, i )
-            if ( pProbab[pFanin->Id] >= 0.37 && Abc_NtkMfsSolveSatResub2( p, pNode, i, -1 ) )
+            if ( Abc_MfsObjProb(p, pFanin) >= 0.37 && Abc_NtkMfsSolveSatResub2( p, pNode, i, -1 ) )
                 continue;
     }
 */
@@ -456,7 +452,7 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars )
     if ( p->pCare )
     {
         Abc_NtkForEachCi( pNtk, pObj, i )
-            pObj->pData = (void *)(PORT_PTRUINT_T)i;
+            pObj->pData = (void *)(ABC_PTRUINT_T)i;
     }
 
     // compute levels
@@ -531,7 +527,7 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars )
                 1.0*p->nNodesGainedLevel/Vec_PtrSize(vNodes),
                 1.0*p->nTotConfLevel/Vec_PtrSize(vNodes),
                 100.0*p->nTimeOutsLevel/Vec_PtrSize(vNodes) );
-            PRT( "Time", clock() - clk2 );
+            ABC_PRT( "Time", clock() - clk2 );
             */
             }
         }
@@ -571,7 +567,7 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars )
 #endif
     }
 
-    // free the manager
+    // ABC_FREE the manager
     p->timeTotal = clock() - clk;
     Mfs_ManStop( p );
     return 1;
diff --git a/src/opt/mfs/mfsInt.h b/src/opt/mfs/mfsInt.h
index 9eb6e4a4..13f0bce2 100644
--- a/src/opt/mfs/mfsInt.h
+++ b/src/opt/mfs/mfsInt.h
@@ -21,10 +21,6 @@
 #ifndef __MFS_INT_H__
 #define __MFS_INT_H__
 
-#ifdef __cplusplus
-extern "C" {
-#endif
-
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -41,6 +37,10 @@ extern "C" {
 ///                         PARAMETERS                               ///
 ////////////////////////////////////////////////////////////////////////
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 #define MFS_FANIN_MAX   12
 
 typedef struct Mfs_Man_t_ Mfs_Man_t;
@@ -116,6 +116,8 @@ struct Mfs_Man_t_
     int                 timeTotal;
 };
 
+static inline float Abc_MfsObjProb( Mfs_Man_t * p, Abc_Obj_t * pObj ) { return (p->vProbs && pObj->Id < Vec_IntSize(p->vProbs))? Abc_Int2Float(Vec_IntEntry(p->vProbs,pObj->Id)) : 0.0; }
+
 ////////////////////////////////////////////////////////////////////////
 ///                         BASIC TYPES                              ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/mfs/mfsInter.c b/src/opt/mfs/mfsInter.c
index 6e50d444..8fc30056 100644
--- a/src/opt/mfs/mfsInter.c
+++ b/src/opt/mfs/mfsInter.c
@@ -239,7 +239,7 @@ unsigned * Abc_NtkMfsInterplateTruth( Mfs_Man_t * p, int * pCands, int nCands, i
     pSat = Abc_MfsCreateSolverResub( p, pCands, nCands, fInvert );
 
     // solve the problem
-    status = sat_solver_solve( pSat, NULL, NULL, (sint64)p->pPars->nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
+    status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)p->pPars->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
     if ( status != l_False )
     {
         p->nTimeOuts++;
@@ -339,7 +339,7 @@ Hop_Obj_t * Abc_NtkMfsInterplate( Mfs_Man_t * p, int * pCands, int nCands )
     pSat = Abc_MfsCreateSolverResub( p, pCands, nCands, 0 );
 
     // solve the problem
-    status = sat_solver_solve( pSat, NULL, NULL, (sint64)p->pPars->nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
+    status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)p->pPars->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
     if ( status != l_False )
     {
         p->nTimeOuts++;
diff --git a/src/opt/mfs/mfsMan.c b/src/opt/mfs/mfsMan.c
index 9a043ed8..e947bd52 100644
--- a/src/opt/mfs/mfsMan.c
+++ b/src/opt/mfs/mfsMan.c
@@ -43,7 +43,7 @@ Mfs_Man_t * Mfs_ManAlloc( Mfs_Par_t * pPars )
 {
     Mfs_Man_t * p;
     // start the manager
-    p = ALLOC( Mfs_Man_t, 1 );
+    p = ABC_ALLOC( Mfs_Man_t, 1 );
     memset( p, 0, sizeof(Mfs_Man_t) );
     p->pPars     = pPars;
     p->vProjVars = Vec_IntAlloc( 100 );
@@ -158,13 +158,13 @@ void Mfs_ManPrint( Mfs_Man_t * p )
             p->nNodesDec, 1.0 * p->nNodesDec / p->nNodesTried, p->nNodesGained, p->nTimeOuts );
     }
 /*
-    PRTP( "Win", p->timeWin            ,  p->timeTotal );
-    PRTP( "Div", p->timeDiv            ,  p->timeTotal );
-    PRTP( "Aig", p->timeAig            ,  p->timeTotal );
-    PRTP( "Cnf", p->timeCnf            ,  p->timeTotal );
-    PRTP( "Sat", p->timeSat-p->timeInt ,  p->timeTotal );
-    PRTP( "Int", p->timeInt            ,  p->timeTotal );
-    PRTP( "ALL", p->timeTotal          ,  p->timeTotal );
+    ABC_PRTP( "Win", p->timeWin            ,  p->timeTotal );
+    ABC_PRTP( "Div", p->timeDiv            ,  p->timeTotal );
+    ABC_PRTP( "Aig", p->timeAig            ,  p->timeTotal );
+    ABC_PRTP( "Cnf", p->timeCnf            ,  p->timeTotal );
+    ABC_PRTP( "Sat", p->timeSat-p->timeInt ,  p->timeTotal );
+    ABC_PRTP( "Int", p->timeInt            ,  p->timeTotal );
+    ABC_PRTP( "ALL", p->timeTotal          ,  p->timeTotal );
 */
 }
 
@@ -201,7 +201,7 @@ void Mfs_ManStop( Mfs_Man_t * p )
     Vec_IntFree( p->vProjVars );
     Vec_IntFree( p->vDivLits );
     Vec_PtrFree( p->vDivCexes );
-    free( p );
+    ABC_FREE( p );
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/mfs/mfsResub.c b/src/opt/mfs/mfsResub.c
index e9ea2c40..e49fd61d 100644
--- a/src/opt/mfs/mfsResub.c
+++ b/src/opt/mfs/mfsResub.c
@@ -100,7 +100,7 @@ int Abc_NtkMfsTryResubOnce( Mfs_Man_t * p, int * pCands, int nCands )
     unsigned * pData;
     int RetValue, iVar, i;
     p->nSatCalls++;
-    RetValue = sat_solver_solve( p->pSat, pCands, pCands + nCands, (sint64)p->pPars->nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
+    RetValue = sat_solver_solve( p->pSat, pCands, pCands + nCands, (ABC_INT64_T)p->pPars->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
 //    assert( RetValue == l_False || RetValue == l_True );
     if ( RetValue == l_False )
         return 1;
@@ -209,8 +209,6 @@ p->timeInt += clock() - clk;
     iVar = -1;
     while ( 1 )
     {
-        float * pProbab = (float *)(p->vProbs? p->vProbs->pArray : NULL);
-        assert( (pProbab != NULL) == p->pPars->fPower );
         if ( fVeryVerbose )
         {
             printf( "%3d: %2d ", p->nCexes, iVar );
@@ -231,7 +229,7 @@ p->timeInt += clock() - clk;
             {
                 Abc_Obj_t * pDiv = Vec_PtrEntry(p->vDivs, iVar);
                 // only accept the divisor if it is "cool"
-                if ( pProbab[Abc_ObjId(pDiv)] >= 0.15 )
+                if ( Abc_MfsObjProb(p, pDiv) >= 0.15 )
                     continue;
             }
             pData  = Vec_PtrEntry( p->vDivCexes, iVar );
@@ -355,8 +353,6 @@ p->timeInt += clock() - clk;
     while ( 1 )
     {
 #if 1 // sjang
-        float * pProbab = (float *)(p->vProbs? p->vProbs->pArray : NULL);
-        assert( (pProbab != NULL) == p->pPars->fPower );
 #endif
         if ( fVeryVerbose )
         {
@@ -381,7 +377,7 @@ p->timeInt += clock() - clk;
             {
                 Abc_Obj_t * pDiv = Vec_PtrEntry(p->vDivs, iVar);
                 // only accept the divisor if it is "cool"
-                if ( pProbab[Abc_ObjId(pDiv)] >= 0.12 )
+                if ( Abc_MfsObjProb(p, pDiv) >= 0.12 )
                     continue;
             }
 #endif
@@ -393,7 +389,7 @@ p->timeInt += clock() - clk;
                 {
                     Abc_Obj_t * pDiv = Vec_PtrEntry(p->vDivs, iVar2);
                     // only accept the divisor if it is "cool"
-                    if ( pProbab[Abc_ObjId(pDiv)] >= 0.12 )
+                    if ( Abc_MfsObjProb(p, pDiv) >= 0.12 )
                         continue;
                 }
 #endif
@@ -477,16 +473,15 @@ int Abc_NtkMfsEdgeSwapEval( Mfs_Man_t * p, Abc_Obj_t * pNode )
 int Abc_NtkMfsEdgePower( Mfs_Man_t * p, Abc_Obj_t * pNode )
 {
     Abc_Obj_t * pFanin;
-    float * pProbab = (float *)p->vProbs->pArray;
     int i;
     // try replacing area critical fanins
     Abc_ObjForEachFanin( pNode, pFanin, i )
     {
-        if ( pProbab[pFanin->Id] >= 0.35 )
+        if ( Abc_MfsObjProb(p, pFanin) >= 0.35 )
         {
             if ( Abc_NtkMfsSolveSatResub( p, pNode, i, 0, 0 ) )
                 return 1;
-        } else if ( pProbab[pFanin->Id] >= 0.25 ) // sjang
+        } else if ( Abc_MfsObjProb(p, pFanin) >= 0.25 ) // sjang
         {
             if ( Abc_NtkMfsSolveSatResub( p, pNode, i, 1, 0 ) )
                 return 1;
diff --git a/src/opt/mfs/mfsSat.c b/src/opt/mfs/mfsSat.c
index 6cc0f0fd..a35d67e4 100644
--- a/src/opt/mfs/mfsSat.c
+++ b/src/opt/mfs/mfsSat.c
@@ -46,7 +46,7 @@ int Abc_NtkMfsSolveSat_iter( Mfs_Man_t * p )
     if ( p->nTotConfLim && p->nTotConfLim <= p->pSat->stats.conflicts )
         return -1;
     nBTLimit = p->nTotConfLim? p->nTotConfLim - p->pSat->stats.conflicts : 0;
-    RetValue = sat_solver_solve( p->pSat, NULL, NULL, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
+    RetValue = sat_solver_solve( p->pSat, NULL, NULL, (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
     assert( RetValue == l_Undef || RetValue == l_True || RetValue == l_False );
     if ( RetValue == l_Undef )
         return -1;
diff --git a/src/opt/mfs/mfsStrash.c b/src/opt/mfs/mfsStrash.c
index 1153e4fd..578c2fbe 100644
--- a/src/opt/mfs/mfsStrash.c
+++ b/src/opt/mfs/mfsStrash.c
@@ -193,14 +193,14 @@ Aig_Man_t * Abc_NtkConstructAig( Mfs_Man_t * p, Abc_Obj_t * pNode )
         Aig_ManIncrementTravId( p->pCare );
         Vec_PtrForEachEntry( p->vSupp, pFanin, i )
         {
-            pPi = Aig_ManPi( p->pCare, (int)(PORT_PTRUINT_T)pFanin->pData );
+            pPi = Aig_ManPi( p->pCare, (int)(ABC_PTRUINT_T)pFanin->pData );
             Aig_ObjSetTravIdCurrent( p->pCare, pPi );
             pPi->pData = pFanin->pCopy;
         }
         // construct the constraints
         Vec_PtrForEachEntry( p->vSupp, pFanin, i )
         {
-            vOuts = Vec_PtrEntry( p->vSuppsInv, (int)(PORT_PTRUINT_T)pFanin->pData );
+            vOuts = Vec_PtrEntry( p->vSuppsInv, (int)(ABC_PTRUINT_T)pFanin->pData );
             Vec_IntForEachEntry( vOuts, iOut, k )
             {
                 pPo = Aig_ManPo( p->pCare, iOut );
@@ -280,7 +280,7 @@ Aig_Man_t * Abc_NtkAigForConstraints( Mfs_Man_t * p, Abc_Obj_t * pNode )
     Aig_ManIncrementTravId( p->pCare );
     Vec_PtrForEachEntry( p->vSupp, pFanin, i )
     {
-        pPi = Aig_ManPi( p->pCare, (int)(PORT_PTRUINT_T)pFanin->pData );
+        pPi = Aig_ManPi( p->pCare, (int)(ABC_PTRUINT_T)pFanin->pData );
         Aig_ObjSetTravIdCurrent( p->pCare, pPi );
         pPi->pData = Aig_ObjCreatePi(pMan);
     }
@@ -288,7 +288,7 @@ Aig_Man_t * Abc_NtkAigForConstraints( Mfs_Man_t * p, Abc_Obj_t * pNode )
     pObjRoot = Aig_ManConst1(pMan);
     Vec_PtrForEachEntry( p->vSupp, pFanin, i )
     {
-        vOuts = Vec_PtrEntry( p->vSuppsInv, (int)(PORT_PTRUINT_T)pFanin->pData );
+        vOuts = Vec_PtrEntry( p->vSuppsInv, (int)(ABC_PTRUINT_T)pFanin->pData );
         Vec_IntForEachEntry( vOuts, iOut, k )
         {
             pPo = Aig_ManPo( p->pCare, iOut );
diff --git a/src/opt/res/res.h b/src/opt/res/res.h
index 3c3431bf..88d985a3 100644
--- a/src/opt/res/res.h
+++ b/src/opt/res/res.h
@@ -21,10 +21,6 @@
 #ifndef __RES_H__
 #define __RES_H__
 
-#ifdef __cplusplus
-extern "C" {
-#endif
-
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -33,6 +29,10 @@ extern "C" {
 ///                         PARAMETERS                               ///
 ////////////////////////////////////////////////////////////////////////
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                         BASIC TYPES                              ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/res/resCore.c b/src/opt/res/resCore.c
index a19a1573..cce3b48a 100644
--- a/src/opt/res/resCore.c
+++ b/src/opt/res/resCore.c
@@ -93,7 +93,7 @@ extern int s_ResynTime;
 Res_Man_t * Res_ManAlloc( Res_Par_t * pPars )
 {
     Res_Man_t * p;
-    p = ALLOC( Res_Man_t, 1 );
+    p = ABC_ALLOC( Res_Man_t, 1 );
     memset( p, 0, sizeof(Res_Man_t) );
     assert( pPars->nWindow > 0 && pPars->nWindow < 100 );
     assert( pPars->nCands > 0 && pPars->nCands < 100 );
@@ -143,18 +143,18 @@ void Res_ManFree( Res_Man_t * p )
         printf( "Proved = %d.", p->nProvedSets );
         printf( "\n" );
 
-        PRTP( "Windowing  ", p->timeWin,      p->timeTotal );
-        PRTP( "Divisors   ", p->timeDiv,      p->timeTotal );
-        PRTP( "Strashing  ", p->timeAig,      p->timeTotal );
-        PRTP( "Simulation ", p->timeSim,      p->timeTotal );
-        PRTP( "Candidates ", p->timeCand,     p->timeTotal );
-        PRTP( "SAT solver ", p->timeSatTotal, p->timeTotal );
-        PRTP( "    sat    ", p->timeSatSat,   p->timeTotal );
-        PRTP( "    unsat  ", p->timeSatUnsat, p->timeTotal );
-        PRTP( "    simul  ", p->timeSatSim,   p->timeTotal );
-        PRTP( "Interpol   ", p->timeInt,      p->timeTotal );
-        PRTP( "Undating   ", p->timeUpd,      p->timeTotal );
-        PRTP( "TOTAL      ", p->timeTotal,    p->timeTotal );
+        ABC_PRTP( "Windowing  ", p->timeWin,      p->timeTotal );
+        ABC_PRTP( "Divisors   ", p->timeDiv,      p->timeTotal );
+        ABC_PRTP( "Strashing  ", p->timeAig,      p->timeTotal );
+        ABC_PRTP( "Simulation ", p->timeSim,      p->timeTotal );
+        ABC_PRTP( "Candidates ", p->timeCand,     p->timeTotal );
+        ABC_PRTP( "SAT solver ", p->timeSatTotal, p->timeTotal );
+        ABC_PRTP( "    sat    ", p->timeSatSat,   p->timeTotal );
+        ABC_PRTP( "    unsat  ", p->timeSatUnsat, p->timeTotal );
+        ABC_PRTP( "    simul  ", p->timeSatSim,   p->timeTotal );
+        ABC_PRTP( "Interpol   ", p->timeInt,      p->timeTotal );
+        ABC_PRTP( "Undating   ", p->timeUpd,      p->timeTotal );
+        ABC_PRTP( "TOTAL      ", p->timeTotal,    p->timeTotal );
     }
     Res_WinFree( p->pWin );
     if ( p->pAig ) Abc_NtkDelete( p->pAig );
@@ -165,7 +165,7 @@ void Res_ManFree( Res_Man_t * p )
     Vec_VecFree( p->vResubs );
     Vec_VecFree( p->vResubsW );
     Vec_VecFree( p->vLevels );
-    free( p );
+    ABC_FREE( p );
 }
 
 /**Function*************************************************************
diff --git a/src/opt/res/resInt.h b/src/opt/res/resInt.h
index 5aae46cc..172b5369 100644
--- a/src/opt/res/resInt.h
+++ b/src/opt/res/resInt.h
@@ -21,10 +21,6 @@
 #ifndef __RES_INT_H__
 #define __RES_INT_H__
 
-#ifdef __cplusplus
-extern "C" {
-#endif
-
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -35,6 +31,10 @@ extern "C" {
 ///                         PARAMETERS                               ///
 ////////////////////////////////////////////////////////////////////////
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                         BASIC TYPES                              ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/res/resSat.c b/src/opt/res/resSat.c
index 798e7abc..d5983942 100644
--- a/src/opt/res/resSat.c
+++ b/src/opt/res/resSat.c
@@ -63,50 +63,50 @@ void * Res_SatProveUnsat( Abc_Ntk_t * pAig, Vec_Ptr_t * vFanins )
 
     // assign unique numbers to each node
     nNodes = 0;
-    Abc_AigConst1(pAig)->pCopy = (void *)(PORT_PTRUINT_T)nNodes++;
+    Abc_AigConst1(pAig)->pCopy = (void *)(ABC_PTRUINT_T)nNodes++;
     Abc_NtkForEachPi( pAig, pObj, i )
-        pObj->pCopy = (void *)(PORT_PTRUINT_T)nNodes++;
+        pObj->pCopy = (void *)(ABC_PTRUINT_T)nNodes++;
     Vec_PtrForEachEntry( vNodes, pObj, i )
-        pObj->pCopy = (void *)(PORT_PTRUINT_T)nNodes++;
+        pObj->pCopy = (void *)(ABC_PTRUINT_T)nNodes++;
     Vec_PtrForEachEntry( vFanins, pObj, i ) // useful POs
-        pObj->pCopy = (void *)(PORT_PTRUINT_T)nNodes++;
+        pObj->pCopy = (void *)(ABC_PTRUINT_T)nNodes++;
 
     // start the solver
     pSat = sat_solver_new();
     sat_solver_store_alloc( pSat );
 
     // add clause for the constant node
-    Res_SatAddConst1( pSat, (int)(PORT_PTRUINT_T)Abc_AigConst1(pAig)->pCopy, 0 );
+    Res_SatAddConst1( pSat, (int)(ABC_PTRUINT_T)Abc_AigConst1(pAig)->pCopy, 0 );
     // add clauses for AND gates
     Vec_PtrForEachEntry( vNodes, pObj, i )
-        Res_SatAddAnd( pSat, (int)(PORT_PTRUINT_T)pObj->pCopy, 
-            (int)(PORT_PTRUINT_T)Abc_ObjFanin0(pObj)->pCopy, (int)(PORT_PTRUINT_T)Abc_ObjFanin1(pObj)->pCopy, Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj) );
+        Res_SatAddAnd( pSat, (int)(ABC_PTRUINT_T)pObj->pCopy, 
+            (int)(ABC_PTRUINT_T)Abc_ObjFanin0(pObj)->pCopy, (int)(ABC_PTRUINT_T)Abc_ObjFanin1(pObj)->pCopy, Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj) );
     Vec_PtrFree( vNodes );
     // add clauses for POs
     Vec_PtrForEachEntry( vFanins, pObj, i )
-        Res_SatAddEqual( pSat, (int)(PORT_PTRUINT_T)pObj->pCopy, 
-            (int)(PORT_PTRUINT_T)Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj) );
+        Res_SatAddEqual( pSat, (int)(ABC_PTRUINT_T)pObj->pCopy, 
+            (int)(ABC_PTRUINT_T)Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj) );
     // add trivial clauses
     pObj = Vec_PtrEntry(vFanins, 0);
-    Res_SatAddConst1( pSat, (int)(PORT_PTRUINT_T)pObj->pCopy, 0 ); // care-set
+    Res_SatAddConst1( pSat, (int)(ABC_PTRUINT_T)pObj->pCopy, 0 ); // care-set
     pObj = Vec_PtrEntry(vFanins, 1);
-    Res_SatAddConst1( pSat, (int)(PORT_PTRUINT_T)pObj->pCopy, 0 ); // on-set
+    Res_SatAddConst1( pSat, (int)(ABC_PTRUINT_T)pObj->pCopy, 0 ); // on-set
 
     // bookmark the clauses of A
     sat_solver_store_mark_clauses_a( pSat );
 
     // duplicate the clauses
     pObj = Vec_PtrEntry(vFanins, 1);
-    Sat_SolverDoubleClauses( pSat, (int)(PORT_PTRUINT_T)pObj->pCopy );
+    Sat_SolverDoubleClauses( pSat, (int)(ABC_PTRUINT_T)pObj->pCopy );
     // add the equality constraints
     Vec_PtrForEachEntryStart( vFanins, pObj, i, 2 )
-        Res_SatAddEqual( pSat, (int)(PORT_PTRUINT_T)pObj->pCopy, ((int)(PORT_PTRUINT_T)pObj->pCopy) + nNodes, 0 );
+        Res_SatAddEqual( pSat, (int)(ABC_PTRUINT_T)pObj->pCopy, ((int)(ABC_PTRUINT_T)pObj->pCopy) + nNodes, 0 );
 
     // bookmark the roots
     sat_solver_store_mark_roots( pSat );
 
     // solve the problem
-    status = sat_solver_solve( pSat, NULL, NULL, (sint64)10000, (sint64)0, (sint64)0, (sint64)0 );
+    status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)10000, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
     if ( status == l_False )
     {
         pCnf = sat_solver_store_release( pSat );
@@ -155,39 +155,39 @@ void * Res_SatSimulateConstr( Abc_Ntk_t * pAig, int fOnSet )
 
     // assign unique numbers to each node
     nNodes = 0;
-    Abc_AigConst1(pAig)->pCopy = (void *)(PORT_PTRUINT_T)nNodes++;
+    Abc_AigConst1(pAig)->pCopy = (void *)(ABC_PTRUINT_T)nNodes++;
     Abc_NtkForEachPi( pAig, pObj, i )
-        pObj->pCopy = (void *)(PORT_PTRUINT_T)nNodes++;
+        pObj->pCopy = (void *)(ABC_PTRUINT_T)nNodes++;
     Vec_PtrForEachEntry( vNodes, pObj, i )
-        pObj->pCopy = (void *)(PORT_PTRUINT_T)nNodes++;
+        pObj->pCopy = (void *)(ABC_PTRUINT_T)nNodes++;
     Vec_PtrForEachEntry( vFanins, pObj, i ) // useful POs
-        pObj->pCopy = (void *)(PORT_PTRUINT_T)nNodes++;
+        pObj->pCopy = (void *)(ABC_PTRUINT_T)nNodes++;
 
     // start the solver
     pSat = sat_solver_new();
 
     // add clause for the constant node
-    Res_SatAddConst1( pSat, (int)(PORT_PTRUINT_T)Abc_AigConst1(pAig)->pCopy, 0 );
+    Res_SatAddConst1( pSat, (int)(ABC_PTRUINT_T)Abc_AigConst1(pAig)->pCopy, 0 );
     // add clauses for AND gates
     Vec_PtrForEachEntry( vNodes, pObj, i )
-        Res_SatAddAnd( pSat, (int)(PORT_PTRUINT_T)pObj->pCopy, 
-            (int)(PORT_PTRUINT_T)Abc_ObjFanin0(pObj)->pCopy, (int)(PORT_PTRUINT_T)Abc_ObjFanin1(pObj)->pCopy, Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj) );
+        Res_SatAddAnd( pSat, (int)(ABC_PTRUINT_T)pObj->pCopy, 
+            (int)(ABC_PTRUINT_T)Abc_ObjFanin0(pObj)->pCopy, (int)(ABC_PTRUINT_T)Abc_ObjFanin1(pObj)->pCopy, Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj) );
     Vec_PtrFree( vNodes );
     // add clauses for the first PO
     pObj = Abc_NtkPo( pAig, 0 );
-    Res_SatAddEqual( pSat, (int)(PORT_PTRUINT_T)pObj->pCopy, 
-        (int)(PORT_PTRUINT_T)Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj) );
+    Res_SatAddEqual( pSat, (int)(ABC_PTRUINT_T)pObj->pCopy, 
+        (int)(ABC_PTRUINT_T)Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj) );
     // add clauses for the second PO
     pObj = Abc_NtkPo( pAig, 1 );
-    Res_SatAddEqual( pSat, (int)(PORT_PTRUINT_T)pObj->pCopy, 
-        (int)(PORT_PTRUINT_T)Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj) );
+    Res_SatAddEqual( pSat, (int)(ABC_PTRUINT_T)pObj->pCopy, 
+        (int)(ABC_PTRUINT_T)Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj) );
 
     // add trivial clauses
     pObj = Abc_NtkPo( pAig, 0 );
-    Res_SatAddConst1( pSat, (int)(PORT_PTRUINT_T)pObj->pCopy, 0 ); // care-set
+    Res_SatAddConst1( pSat, (int)(ABC_PTRUINT_T)pObj->pCopy, 0 ); // care-set
 
     pObj = Abc_NtkPo( pAig, 1 );
-    Res_SatAddConst1( pSat, (int)(PORT_PTRUINT_T)pObj->pCopy, !fOnSet ); // on-set
+    Res_SatAddConst1( pSat, (int)(ABC_PTRUINT_T)pObj->pCopy, !fOnSet ); // on-set
 
     Vec_PtrFree( vFanins );
     return pSat;
@@ -218,7 +218,7 @@ int Res_SatSimulate( Res_Sim_t * p, int nPatsLimit, int fOnSet )
 //printf( "Looking for %s:  ", fOnSet? "onset " : "offset" );
 
     // decide what problem should be solved
-    Lit = toLitCond( (int)(PORT_PTRUINT_T)Abc_NtkPo(p->pAig,1)->pCopy, !fOnSet );
+    Lit = toLitCond( (int)(ABC_PTRUINT_T)Abc_NtkPo(p->pAig,1)->pCopy, !fOnSet );
     if ( fOnSet )
     {
         iPat = p->nPats1;
@@ -254,8 +254,8 @@ int Res_SatSimulate( Res_Sim_t * p, int nPatsLimit, int fOnSet )
     for ( k = iPat; k < nPatsLimit; k++ )
     {
         // solve with the assumption
-//        status = sat_solver_solve( pSat, &Lit, &Lit + 1, (sint64)10000, (sint64)0, (sint64)0, (sint64)0 );
-        status = sat_solver_solve( pSat, NULL, NULL, (sint64)10000, (sint64)0, (sint64)0, (sint64)0 );
+//        status = sat_solver_solve( pSat, &Lit, &Lit + 1, (ABC_INT64_T)10000, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
+        status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)10000, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
         if ( status == l_False )
         {
 //printf( "Const %d\n", !fOnSet );
@@ -275,7 +275,7 @@ int Res_SatSimulate( Res_Sim_t * p, int nPatsLimit, int fOnSet )
             Vec_IntClear( vLits );
             for ( i = 0; i < p->nTruePis; i++ )
             {
-                Var = (int)(PORT_PTRUINT_T)Abc_NtkPi(p->pAig,i)->pCopy;
+                Var = (int)(ABC_PTRUINT_T)Abc_NtkPi(p->pAig,i)->pCopy;
                 value = (int)(pSat->model.ptr[Var] == l_True);
                 if ( value )
                     Abc_InfoSetBit( Vec_PtrEntry(vPats, i), k );
diff --git a/src/opt/res/resSim.c b/src/opt/res/resSim.c
index 5c1dd2b6..59b2b6ea 100644
--- a/src/opt/res/resSim.c
+++ b/src/opt/res/resSim.c
@@ -43,7 +43,7 @@
 Res_Sim_t * Res_SimAlloc( int nWords )
 {
     Res_Sim_t * p;
-    p = ALLOC( Res_Sim_t, 1 );
+    p = ABC_ALLOC( Res_Sim_t, 1 );
     memset( p, 0, sizeof(Res_Sim_t) );
     // simulation parameters
     p->nWords    = nWords;
@@ -128,7 +128,7 @@ void Res_SimFree( Res_Sim_t * p )
     Vec_PtrFree( p->vPats1 );
     Vec_PtrFree( p->vOuts );
     Vec_VecFree( p->vCands );
-    free( p );
+    ABC_FREE( p );
 }
 
 
diff --git a/src/opt/res/resWin.c b/src/opt/res/resWin.c
index a3648925..e46fdc70 100644
--- a/src/opt/res/resWin.c
+++ b/src/opt/res/resWin.c
@@ -44,7 +44,7 @@ Res_Win_t * Res_WinAlloc()
 {
     Res_Win_t * p;
     // start the manager
-    p = ALLOC( Res_Win_t, 1 );
+    p = ABC_ALLOC( Res_Win_t, 1 );
     memset( p, 0, sizeof(Res_Win_t) );
     // set internal parameters
     p->nFanoutLimit = 10;
@@ -78,7 +78,7 @@ void Res_WinFree( Res_Win_t * p )
     Vec_PtrFree( p->vNodes  );
     Vec_PtrFree( p->vDivs   );
     Vec_VecFree( p->vMatrix );
-    free( p );
+    ABC_FREE( p );
 }
 
 
diff --git a/src/opt/ret/retArea.c b/src/opt/ret/retArea.c
index 318147f5..63503916 100644
--- a/src/opt/ret/retArea.c
+++ b/src/opt/ret/retArea.c
@@ -264,22 +264,22 @@ int Abc_NtkRetimeMinAreaInitValues_rec( Abc_Obj_t * pObj )
     int i;
     // skip visited nodes
     if ( Abc_NodeIsTravIdCurrent(pObj) )
-        return (int)(PORT_PTRUINT_T)pObj->pCopy;
+        return (int)(ABC_PTRUINT_T)pObj->pCopy;
     Abc_NodeSetTravIdCurrent(pObj);
     // consider the case of a latch output
     if ( Abc_ObjIsBo(pObj) )
     {
         assert( Abc_ObjIsLatch(Abc_ObjFanin0(pObj)) );
-        pObj->pCopy = (void *)(PORT_PTRUINT_T)Abc_NtkRetimeMinAreaInitValues_rec( Abc_ObjFanin0(pObj) );
-        return (int)(PORT_PTRUINT_T)pObj->pCopy;
+        pObj->pCopy = (void *)(ABC_PTRUINT_T)Abc_NtkRetimeMinAreaInitValues_rec( Abc_ObjFanin0(pObj) );
+        return (int)(ABC_PTRUINT_T)pObj->pCopy;
     }
     assert( Abc_ObjIsNode(pObj) );
     // visit the fanins
     Abc_ObjForEachFanin( pObj, pFanin, i )
         Abc_NtkRetimeMinAreaInitValues_rec( pFanin );
     // compute the value of the node
-    pObj->pCopy = (void *)(PORT_PTRUINT_T)Abc_ObjSopSimulate(pObj);
-    return (int)(PORT_PTRUINT_T)pObj->pCopy;
+    pObj->pCopy = (void *)(ABC_PTRUINT_T)Abc_ObjSopSimulate(pObj);
+    return (int)(ABC_PTRUINT_T)pObj->pCopy;
 }
 
 /**Function*************************************************************
@@ -301,7 +301,7 @@ void Abc_NtkRetimeMinAreaInitValues( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMinCut )
     Abc_NtkIncrementTravId(pNtk);
     Abc_NtkForEachLatch( pNtk, pObj, i )
     {
-        pObj->pCopy = (void *)(PORT_PTRUINT_T)Abc_LatchIsInit1(pObj);
+        pObj->pCopy = (void *)(ABC_PTRUINT_T)Abc_LatchIsInit1(pObj);
         Abc_NodeSetTravIdCurrent( pObj );
     }
     // propagate initial values
@@ -478,7 +478,7 @@ void Abc_NtkRetimeMinAreaUpdateLatches( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMinCut, i
             Abc_ObjAddFanin( pLatch, pLatchIn );
             if ( fForward )
             {
-                pLatch->pData = (void *)(PORT_PTRUINT_T)(pObj->pCopy? ABC_INIT_ONE : ABC_INIT_ZERO);
+                pLatch->pData = (void *)(ABC_PTRUINT_T)(pObj->pCopy? ABC_INIT_ONE : ABC_INIT_ZERO);
                 // redirect edges to the unvisited fanouts of the node
                 Abc_NodeCollectFanouts( pObj, vNodes );
                 Vec_PtrForEachEntry( vNodes, pNext, k )
diff --git a/src/opt/ret/retCore.c b/src/opt/ret/retCore.c
index 47b2cbbc..9de1b723 100644
--- a/src/opt/ret/retCore.c
+++ b/src/opt/ret/retCore.c
@@ -94,7 +94,7 @@ int Abc_NtkRetime( Abc_Ntk_t * pNtk, int Mode, int fForwardOnly, int fBackwardOn
     {
         printf( "Reduction in area = %3d. Reduction in delay = %3d. ", 
             nLatches - Abc_NtkLatchNum(pNtk), nLevels - Abc_NtkLevel(pNtk) );
-        PRT( "Total runtime", clock() - clkTotal );
+        ABC_PRT( "Total runtime", clock() - clkTotal );
     }
     timeRetime = clock() - clkTotal;
     return RetValue;
diff --git a/src/opt/ret/retFlow.c b/src/opt/ret/retFlow.c
index bad4b7e7..7c17c1f6 100644
--- a/src/opt/ret/retFlow.c
+++ b/src/opt/ret/retFlow.c
@@ -228,7 +228,7 @@ Vec_Ptr_t * Abc_NtkMaxFlow( Abc_Ntk_t * pNtk, int fForward, int fVerbose )
     {
     printf( "L = %6d. %s max-flow = %6d.  Min-cut = %6d.  ", 
         Abc_NtkLatchNum(pNtk), fForward? "Forward " : "Backward", Flow, Vec_PtrSize(vMinCut) );
-PRT( "Time", clock() - clk );
+ABC_PRT( "Time", clock() - clk );
     }
 
 //    Abc_NtkMaxFlowPrintCut( pNtk, vMinCut );
diff --git a/src/opt/ret/retIncrem.c b/src/opt/ret/retIncrem.c
index 140e5dcc..233fb436 100644
--- a/src/opt/ret/retIncrem.c
+++ b/src/opt/ret/retIncrem.c
@@ -113,7 +113,7 @@ st_table * Abc_NtkRetimePrepareLatches( Abc_Ntk_t * pNtk )
     Abc_NtkForEachLatch( pNtk, pLatch, i )
     {
         // map latch into its true number
-        st_insert( tLatches, (void *)(PORT_PTRUINT_T)pLatch, (void *)(PORT_PTRUINT_T)(i-nOffSet) );
+        st_insert( tLatches, (void *)(ABC_PTRUINT_T)pLatch, (void *)(ABC_PTRUINT_T)(i-nOffSet) );
         // disconnect LI     
         pLatchIn = Abc_ObjFanin0(pLatch);
         pFanin = Abc_ObjFanin0(pLatchIn);
@@ -194,7 +194,7 @@ int Abc_NtkRetimeFinalizeLatches( Abc_Ntk_t * pNtk, st_table * tLatches, int nId
         Vec_PtrPush( vCosNew, pLatchIn );
         Vec_PtrPush( vBoxesNew, pLatch );
     }
-    // free useless Cis/Cos
+    // ABC_FREE useless Cis/Cos
     Vec_PtrForEachEntry( vCisOld, pObj, i )
         if ( !Abc_ObjIsPi(pObj) && Abc_ObjFaninNum(pObj) == 0 && Abc_ObjFanoutNum(pObj) == 0 )
             Abc_NtkDeleteObj(pObj);
@@ -320,7 +320,7 @@ void Abc_NtkRetimeNode( Abc_Obj_t * pObj, int fForward, int fInitial )
     {
         // compute the initial value
         if ( fInitial )
-            pObj->pCopy = (void *)(PORT_PTRUINT_T)Abc_ObjSopSimulate( pObj );
+            pObj->pCopy = (void *)(ABC_PTRUINT_T)Abc_ObjSopSimulate( pObj );
         // collect fanins
         Abc_NodeCollectFanins( pObj, vNodes );
         // make the node point to the fanins fanins
@@ -400,10 +400,10 @@ int Abc_NtkRetimeCheckCompatibleLatchFanouts( Abc_Obj_t * pObj )
             continue;
         if ( Init == -1 )
         {
-            Init = (int)(PORT_PTRUINT_T)pObj->pData;
+            Init = (int)(ABC_PTRUINT_T)pObj->pData;
             nLatches++;
         }
-        else if ( Init == (int)(PORT_PTRUINT_T)pObj->pData )
+        else if ( Init == (int)(ABC_PTRUINT_T)pObj->pData )
             nLatches++;
     }
     return nLatches;
diff --git a/src/opt/ret/retInit.c b/src/opt/ret/retInit.c
index 8de0ef47..72b384d9 100644
--- a/src/opt/ret/retInit.c
+++ b/src/opt/ret/retInit.c
@@ -57,9 +57,9 @@ Vec_Int_t * Abc_NtkRetimeInitialValues( Abc_Ntk_t * pNtkCone, Vec_Int_t * vValue
         printf( "The miter for initial state computation has %d AIG nodes. ", Abc_NtkNodeNum(pNtkMiter) );
     // solve the miter
     clk = clock();
-    RetValue = Abc_NtkMiterSat( pNtkMiter, (sint64)500000, (sint64)50000000, 0, NULL, NULL );
+    RetValue = Abc_NtkMiterSat( pNtkMiter, (ABC_INT64_T)500000, (ABC_INT64_T)50000000, 0, NULL, NULL );
     if ( fVerbose ) 
-        { PRT( "SAT solving time", clock() - clk ); }
+        { ABC_PRT( "SAT solving time", clock() - clk ); }
     // analyze the result
     if ( RetValue == 1 )
         printf( "Abc_NtkRetimeInitialValues(): The problem is unsatisfiable. DC latch values are used.\n" );
@@ -100,9 +100,9 @@ int Abc_ObjSopSimulate( Abc_Obj_t * pObj )
         Abc_CubeForEachVar( pCube, Value, v )
         {
             if ( Value == '0' )
-                ResVar = 1 ^ ((int)(PORT_PTRUINT_T)Abc_ObjFanin(pObj, v)->pCopy);
+                ResVar = 1 ^ ((int)(ABC_PTRUINT_T)Abc_ObjFanin(pObj, v)->pCopy);
             else if ( Value == '1' )
-                ResVar = (int)(PORT_PTRUINT_T)Abc_ObjFanin(pObj, v)->pCopy;
+                ResVar = (int)(ABC_PTRUINT_T)Abc_ObjFanin(pObj, v)->pCopy;
             else
                 continue;
             ResAnd &= ResVar;
@@ -134,17 +134,17 @@ int Abc_NtkRetimeVerifyModel( Abc_Ntk_t * pNtkCone, Vec_Int_t * vValues, int * p
     assert( Abc_NtkIsSopLogic(pNtkCone) );
     // set the PIs
     Abc_NtkForEachPi( pNtkCone, pObj, i )
-        pObj->pCopy = (void *)(PORT_PTRUINT_T)pModel[i];
+        pObj->pCopy = (void *)(ABC_PTRUINT_T)pModel[i];
     // simulate the internal nodes
     vNodes = Abc_NtkDfs( pNtkCone, 0 );
     Vec_PtrForEachEntry( vNodes, pObj, i )
-        pObj->pCopy = (void *)(PORT_PTRUINT_T)Abc_ObjSopSimulate( pObj );
+        pObj->pCopy = (void *)(ABC_PTRUINT_T)Abc_ObjSopSimulate( pObj );
     Vec_PtrFree( vNodes );
     // compare the outputs
     Abc_NtkForEachPo( pNtkCone, pObj, i )
         pObj->pCopy = Abc_ObjFanin0(pObj)->pCopy;
     Abc_NtkForEachPo( pNtkCone, pObj, i )
-        Counter += (Vec_IntEntry(vValues, i) != (int)(PORT_PTRUINT_T)pObj->pCopy);
+        Counter += (Vec_IntEntry(vValues, i) != (int)(ABC_PTRUINT_T)pObj->pCopy);
     if ( Counter > 0 )
         printf( "%d outputs (out of %d) have a value mismatch.\n", Counter, Abc_NtkPoNum(pNtkCone) );
     return 1;
@@ -167,7 +167,7 @@ void Abc_NtkRetimeTranferToCopy( Abc_Ntk_t * pNtk )
     int i;
     Abc_NtkForEachObj( pNtk, pObj, i )
         if ( Abc_ObjIsLatch(pObj) )
-            pObj->pCopy = (void *)(PORT_PTRUINT_T)Abc_LatchIsInit1(pObj);
+            pObj->pCopy = (void *)(ABC_PTRUINT_T)Abc_LatchIsInit1(pObj);
 }
 
 /**Function*************************************************************
@@ -187,7 +187,7 @@ void Abc_NtkRetimeTranferFromCopy( Abc_Ntk_t * pNtk )
     int i;
     Abc_NtkForEachObj( pNtk, pObj, i )
         if ( Abc_ObjIsLatch(pObj) )
-            pObj->pData = (void *)(PORT_PTRUINT_T)(pObj->pCopy? ABC_INIT_ONE : ABC_INIT_ZERO);
+            pObj->pData = (void *)(ABC_PTRUINT_T)(pObj->pCopy? ABC_INIT_ONE : ABC_INIT_ZERO);
 }
 
 /**Function*************************************************************
@@ -230,10 +230,10 @@ void Abc_NtkRetimeInsertLatchValues( Abc_Ntk_t * pNtk, Vec_Int_t * vValues )
     int i, Counter = 0;
     Abc_NtkForEachObj( pNtk, pObj, i )
         if ( Abc_ObjIsLatch(pObj) )
-            pObj->pCopy = (void *)(PORT_PTRUINT_T)Counter++;
+            pObj->pCopy = (void *)(ABC_PTRUINT_T)Counter++;
     Abc_NtkForEachObj( pNtk, pObj, i )
         if ( Abc_ObjIsLatch(pObj) )
-            pObj->pData = (void *)(PORT_PTRUINT_T)(vValues? (Vec_IntEntry(vValues,(int)(PORT_PTRUINT_T)pObj->pCopy)? ABC_INIT_ONE : ABC_INIT_ZERO) : ABC_INIT_DC);
+            pObj->pData = (void *)(ABC_PTRUINT_T)(vValues? (Vec_IntEntry(vValues,(int)(ABC_PTRUINT_T)pObj->pCopy)? ABC_INIT_ONE : ABC_INIT_ZERO) : ABC_INIT_DC);
 }
 
 /**Function*************************************************************
@@ -316,22 +316,22 @@ void Abc_NtkCycleInitStateSop( Abc_Ntk_t * pNtk, int nFrames, int fVerbose )
     srand( 0x12341234 );
     // initialize the values
     Abc_NtkForEachPi( pNtk, pObj, i )
-        pObj->pCopy = (void *)(PORT_PTRUINT_T)(rand() & 1);
+        pObj->pCopy = (void *)(ABC_PTRUINT_T)(rand() & 1);
     Abc_NtkForEachLatch( pNtk, pObj, i )
-        pObj->pCopy = (void *)(PORT_PTRUINT_T)Abc_LatchIsInit1(pObj);
+        pObj->pCopy = (void *)(ABC_PTRUINT_T)Abc_LatchIsInit1(pObj);
     // simulate for the given number of timeframes
     vNodes = Abc_NtkDfs( pNtk, 0 );
     for ( f = 0; f < nFrames; f++ )
     {
         // simulate internal nodes
         Vec_PtrForEachEntry( vNodes, pObj, i )
-            pObj->pCopy = (void *)(PORT_PTRUINT_T)Abc_ObjSopSimulate( pObj );
+            pObj->pCopy = (void *)(ABC_PTRUINT_T)Abc_ObjSopSimulate( pObj );
         // bring the results to the COs
         Abc_NtkForEachCo( pNtk, pObj, i )
             pObj->pCopy = Abc_ObjFanin0(pObj)->pCopy;
         // assign PI values
         Abc_NtkForEachPi( pNtk, pObj, i )
-            pObj->pCopy = (void *)(PORT_PTRUINT_T)(rand() & 1);
+            pObj->pCopy = (void *)(ABC_PTRUINT_T)(rand() & 1);
         // transfer the latch values
         Abc_NtkForEachLatch( pNtk, pObj, i )
             Abc_ObjFanout0(pObj)->pCopy = Abc_ObjFanin0(pObj)->pCopy;
@@ -339,7 +339,7 @@ void Abc_NtkCycleInitStateSop( Abc_Ntk_t * pNtk, int nFrames, int fVerbose )
     Vec_PtrFree( vNodes );
     // set the final values
     Abc_NtkForEachLatch( pNtk, pObj, i )
-        pObj->pData = (void *)(PORT_PTRUINT_T)(Abc_ObjFanout0(pObj)->pCopy ? ABC_INIT_ONE : ABC_INIT_ZERO);
+        pObj->pData = (void *)(ABC_PTRUINT_T)(Abc_ObjFanout0(pObj)->pCopy ? ABC_INIT_ONE : ABC_INIT_ZERO);
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/ret/retLvalue.c b/src/opt/ret/retLvalue.c
index 26f51f09..02d9cac2 100644
--- a/src/opt/ret/retLvalue.c
+++ b/src/opt/ret/retLvalue.c
@@ -37,8 +37,8 @@ static Vec_Ptr_t * Abc_ManCollectLatches( Abc_Ntk_t * pNtk );
 static int         Abc_NtkRetimeUsingLags( Abc_Ntk_t * pNtk, Vec_Int_t * vLags, int fVerbose );
 
 static inline int  Abc_NodeComputeLag( int LValue, int Fi )          { return (LValue + (1<<16)*Fi)/Fi - (1<<16) - (int)(LValue % Fi == 0);     }
-static inline int  Abc_NodeGetLValue( Abc_Obj_t * pNode )            { return (int)(PORT_PTRUINT_T)pNode->pCopy;        }
-static inline void Abc_NodeSetLValue( Abc_Obj_t * pNode, int Value ) { pNode->pCopy = (void *)(PORT_PTRUINT_T)Value;    }
+static inline int  Abc_NodeGetLValue( Abc_Obj_t * pNode )            { return (int)(ABC_PTRUINT_T)pNode->pCopy;        }
+static inline void Abc_NodeSetLValue( Abc_Obj_t * pNode, int Value ) { pNode->pCopy = (void *)(ABC_PTRUINT_T)Value;    }
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
diff --git a/src/opt/rwr/rwr.h b/src/opt/rwr/rwr.h
index 64e916e2..5adc3b4b 100644
--- a/src/opt/rwr/rwr.h
+++ b/src/opt/rwr/rwr.h
@@ -21,10 +21,6 @@
 #ifndef __RWR_H__
 #define __RWR_H__
 
-#ifdef __cplusplus
-extern "C" {
-#endif
-
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -36,6 +32,10 @@ extern "C" {
 ///                         PARAMETERS                               ///
 ////////////////////////////////////////////////////////////////////////
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                         BASIC TYPES                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -111,10 +111,10 @@ struct Rwr_Node_t_ // 24 bytes
 };
 
 // manipulation of complemented attributes
-static inline bool         Rwr_IsComplement( Rwr_Node_t * p )    { return (bool)(((PORT_PTRUINT_T)p) & 01);           }
-static inline Rwr_Node_t * Rwr_Regular( Rwr_Node_t * p )         { return (Rwr_Node_t *)((PORT_PTRUINT_T)(p) & ~01);  }
-static inline Rwr_Node_t * Rwr_Not( Rwr_Node_t * p )             { return (Rwr_Node_t *)((PORT_PTRUINT_T)(p) ^  01);  }
-static inline Rwr_Node_t * Rwr_NotCond( Rwr_Node_t * p, int c )  { return (Rwr_Node_t *)((PORT_PTRUINT_T)(p) ^ (c));  }
+static inline bool         Rwr_IsComplement( Rwr_Node_t * p )    { return (bool)(((ABC_PTRUINT_T)p) & 01);           }
+static inline Rwr_Node_t * Rwr_Regular( Rwr_Node_t * p )         { return (Rwr_Node_t *)((ABC_PTRUINT_T)(p) & ~01);  }
+static inline Rwr_Node_t * Rwr_Not( Rwr_Node_t * p )             { return (Rwr_Node_t *)((ABC_PTRUINT_T)(p) ^  01);  }
+static inline Rwr_Node_t * Rwr_NotCond( Rwr_Node_t * p, int c )  { return (Rwr_Node_t *)((ABC_PTRUINT_T)(p) ^ (c));  }
 
 ////////////////////////////////////////////////////////////////////////
 ///                      MACRO DEFINITIONS                           ///
diff --git a/src/opt/rwr/rwrDec.c b/src/opt/rwr/rwrDec.c
index ae01b896..81c7e307 100644
--- a/src/opt/rwr/rwrDec.c
+++ b/src/opt/rwr/rwrDec.c
@@ -49,7 +49,7 @@ void Rwr_ManPreprocess( Rwr_Man_t * p )
     Rwr_Node_t * pNode;
     int i, k;
     // put the nodes into the structure
-    p->pMapInv  = ALLOC( unsigned short, 222 );
+    p->pMapInv  = ABC_ALLOC( unsigned short, 222 );
     memset( p->pMapInv, 0, sizeof(unsigned short) * 222 );
     p->vClasses = Vec_VecStart( 222 );
     for ( i = 0; i < p->nFuncs; i++ )
diff --git a/src/opt/rwr/rwrExp.c b/src/opt/rwr/rwrExp.c
index 5729cdbc..543cae07 100644
--- a/src/opt/rwr/rwrExp.c
+++ b/src/opt/rwr/rwrExp.c
@@ -64,14 +64,14 @@ static Rwr_Man5_t * s_pManRwrExp5 = NULL;
 void Rwt_Man4ExploreStart()
 {
     Rwr_Man4_t * p;
-    p = ALLOC( Rwr_Man4_t, 1 );
+    p = ABC_ALLOC( Rwr_Man4_t, 1 );
     memset( p, 0, sizeof(Rwr_Man4_t) );
     // canonical forms
     p->nFuncs    = (1<<16);
     // canonical forms, phases, perms
     Extra_Truth4VarNPN( &p->puCanons, NULL, NULL, NULL );
     // counters
-    p->pnCounts  = ALLOC( int, p->nFuncs );
+    p->pnCounts  = ABC_ALLOC( int, p->nFuncs );
     memset( p->pnCounts, 0, sizeof(int) * p->nFuncs );
     s_pManRwrExp4 = p;
 }
@@ -124,8 +124,8 @@ void Rwt_Man4ExplorePrint()
     printf( "Number of cuts considered       = %8d.\n", nCuts );
     printf( "Classes occurring at least once = %8d.\n", nClasses );
     // print the distribution of classes
-    pDistrib = ALLOC( int, CountMax + 1 );
-    pReprs   = ALLOC( int, CountMax + 1 );
+    pDistrib = ABC_ALLOC( int, CountMax + 1 );
+    pReprs   = ABC_ALLOC( int, CountMax + 1 );
     memset( pDistrib, 0, sizeof(int)*(CountMax + 1) );
     for ( i = 0; i < s_pManRwrExp4->nFuncs; i++ )
     {
@@ -141,8 +141,8 @@ void Rwt_Man4ExplorePrint()
             Extra_PrintBinary( stdout, (unsigned*)&(pReprs[i]), 16 ); 
             printf( "\n" );
         }
-    free( pDistrib );
-    free( pReprs );
+    ABC_FREE( pDistrib );
+    ABC_FREE( pReprs );
     // write into a file all classes above limit (5)
     CountWrite = 0;
     pFile = fopen( "npnclass_stats4.txt", "w" );
@@ -175,7 +175,7 @@ void Rwt_Man4ExplorePrint()
 void Rwt_Man5ExploreStart()
 {
     Rwr_Man5_t * p;
-    p = ALLOC( Rwr_Man5_t, 1 );
+    p = ABC_ALLOC( Rwr_Man5_t, 1 );
     memset( p, 0, sizeof(Rwr_Man5_t) );
     p->tTableNN  = stmm_init_table( st_numcmp, st_numhash );
     p->tTableNPN = stmm_init_table( st_numcmp, st_numhash );
@@ -199,7 +199,7 @@ void Rwt_Man5ExploreStart()
 void Rwt_Man5ExploreCount( unsigned uTruth )
 {
     int * pCounter;
-    if ( !stmm_find_or_add( s_pManRwrExp5->tTableNN, (char *)(PORT_PTRUINT_T)uTruth, (char***)&pCounter ) )
+    if ( !stmm_find_or_add( s_pManRwrExp5->tTableNN, (char *)(ABC_PTRUINT_T)uTruth, (char***)&pCounter ) )
         *pCounter = 0;
     (*pCounter)++;
 }
@@ -240,8 +240,8 @@ void Rwt_Man5ExplorePrint()
     printf( "The largest number of occurence = %8d.\n", CountMax );
 
     // print the distribution of classes
-    pDistrib = ALLOC( int, CountMax + 1 );
-    pReprs   = ALLOC( unsigned, CountMax + 1 );
+    pDistrib = ABC_ALLOC( int, CountMax + 1 );
+    pReprs   = ABC_ALLOC( unsigned, CountMax + 1 );
     memset( pDistrib, 0, sizeof(int)*(CountMax + 1) );
     stmm_foreach_item( s_pManRwrExp5->tTableNN, gen, (char **)&uTruth, (char **)&Counter )
     {
@@ -257,8 +257,8 @@ void Rwt_Man5ExplorePrint()
             Extra_PrintBinary( stdout, pReprs + i, 32 ); 
             printf( "\n" );
         }
-    free( pDistrib );
-    free( pReprs );
+    ABC_FREE( pDistrib );
+    ABC_FREE( pReprs );
 
 
     // put them into an array
@@ -271,7 +271,7 @@ void Rwt_Man5ExplorePrint()
     pFile = fopen( "nnclass_stats5.txt", "w" );
     Vec_IntForEachEntry( vClassesNN, uTruth, i )
     {
-        if ( !stmm_lookup( s_pManRwrExp5->tTableNN, (char *)(PORT_PTRUINT_T)uTruth, (char **)&Counter ) )
+        if ( !stmm_lookup( s_pManRwrExp5->tTableNN, (char *)(ABC_PTRUINT_T)uTruth, (char **)&Counter ) )
         {
             assert( 0 );
         }
@@ -288,16 +288,16 @@ clk = clock();
     {
         int * pCounter;
         uTruthC = Extra_TruthCanonNPN( uTruth, 5 );
-        if ( !stmm_find_or_add( s_pManRwrExp5->tTableNPN, (char *)(PORT_PTRUINT_T)uTruthC, (char***)&pCounter ) )
+        if ( !stmm_find_or_add( s_pManRwrExp5->tTableNPN, (char *)(ABC_PTRUINT_T)uTruthC, (char***)&pCounter ) )
             *pCounter = 0;
-        if ( !stmm_lookup( s_pManRwrExp5->tTableNN, (char *)(PORT_PTRUINT_T)uTruth, (char **)&Counter ) )
+        if ( !stmm_lookup( s_pManRwrExp5->tTableNN, (char *)(ABC_PTRUINT_T)uTruth, (char **)&Counter ) )
         {
             assert( 0 );
         }
         (*pCounter) += Counter;
     }
     printf( "The numbe of NPN classes = %d.\n", stmm_count(s_pManRwrExp5->tTableNPN) );
-PRT( "Computing NPN classes", clock() - clk );
+ABC_PRT( "Computing NPN classes", clock() - clk );
 
     // put them into an array
     vClassesNPN = Vec_IntAlloc( stmm_count(s_pManRwrExp5->tTableNPN) );
@@ -309,7 +309,7 @@ PRT( "Computing NPN classes", clock() - clk );
     pFile = fopen( "npnclass_stats5.txt", "w" );
     Vec_IntForEachEntry( vClassesNPN, uTruth, i )
     {
-        if ( !stmm_lookup( s_pManRwrExp5->tTableNPN, (char *)(PORT_PTRUINT_T)uTruth, (char **)&Counter ) )
+        if ( !stmm_lookup( s_pManRwrExp5->tTableNPN, (char *)(ABC_PTRUINT_T)uTruth, (char **)&Counter ) )
         {
             assert( 0 );
         }
diff --git a/src/opt/rwr/rwrMan.c b/src/opt/rwr/rwrMan.c
index 87a080c7..e7d21164 100644
--- a/src/opt/rwr/rwrMan.c
+++ b/src/opt/rwr/rwrMan.c
@@ -47,7 +47,7 @@ Rwr_Man_t * Rwr_ManStart( bool fPrecompute )
     Rwr_Man_t * p;
     int clk = clock();
 clk = clock();
-    p = ALLOC( Rwr_Man_t, 1 );
+    p = ABC_ALLOC( Rwr_Man_t, 1 );
     memset( p, 0, sizeof(Rwr_Man_t) );
     p->nFuncs = (1<<16);
     pManDec   = Abc_FrameReadManDec();
@@ -58,7 +58,7 @@ clk = clock();
     // initialize practical NPN classes
     p->pPractical  = Rwr_ManGetPractical( p );
     // create the table
-    p->pTable = ALLOC( Rwr_Node_t *, p->nFuncs );
+    p->pTable = ABC_ALLOC( Rwr_Node_t *, p->nFuncs );
     memset( p->pTable, 0, sizeof(Rwr_Node_t *) * p->nFuncs );
     // create the elementary nodes
     p->pMmNode  = Extra_MmFixedStart( sizeof(Rwr_Node_t) );
@@ -119,11 +119,11 @@ void Rwr_ManStop( Rwr_Man_t * p )
     Vec_PtrFree( p->vFanins );
     Vec_PtrFree( p->vFaninsCur );
     Extra_MmFixedStop( p->pMmNode );
-    FREE( p->pMapInv );
-    free( p->pTable );
-    free( p->pPractical );
-    free( p->pPerms4 );
-    free( p );
+    ABC_FREE( p->pMapInv );
+    ABC_FREE( p->pTable );
+    ABC_FREE( p->pPractical );
+    ABC_FREE( p->pPerms4 );
+    ABC_FREE( p );
 }
 
 /**Function*************************************************************
@@ -151,13 +151,13 @@ void Rwr_ManPrintStats( Rwr_Man_t * p )
     printf( "Nodes considered  = %8d.\n", p->nNodesConsidered );
     printf( "Nodes rewritten   = %8d.\n", p->nNodesRewritten );
     printf( "Gain              = %8d. (%6.2f %%).\n", p->nNodesBeg-p->nNodesEnd, 100.0*(p->nNodesBeg-p->nNodesEnd)/p->nNodesBeg );
-    PRT( "Start       ", p->timeStart );
-    PRT( "Cuts        ", p->timeCut );
-    PRT( "Resynthesis ", p->timeRes );
-    PRT( "    Mffc    ", p->timeMffc );
-    PRT( "    Eval    ", p->timeEval );
-    PRT( "Update      ", p->timeUpdate );
-    PRT( "TOTAL       ", p->timeTotal );
+    ABC_PRT( "Start       ", p->timeStart );
+    ABC_PRT( "Cuts        ", p->timeCut );
+    ABC_PRT( "Resynthesis ", p->timeRes );
+    ABC_PRT( "    Mffc    ", p->timeMffc );
+    ABC_PRT( "    Eval    ", p->timeEval );
+    ABC_PRT( "Update      ", p->timeUpdate );
+    ABC_PRT( "TOTAL       ", p->timeTotal );
 
 /*
     printf( "The scores are:\n" );
diff --git a/src/opt/rwr/rwrUtil.c b/src/opt/rwr/rwrUtil.c
index b2add2bf..8da3b6eb 100644
--- a/src/opt/rwr/rwrUtil.c
+++ b/src/opt/rwr/rwrUtil.c
@@ -78,7 +78,7 @@ void Rwr_ManWriteToArray( Rwr_Man_t * p )
     Extra_PrintHex( pFile, 0, 4 );
     fprintf( pFile, " \n};\n" );
     fclose( pFile );
-    printf( "The number of nodes saved = %d.   ", nEntries );  PRT( "Saving", clock() - clk );
+    printf( "The number of nodes saved = %d.   ", nEntries );  ABC_PRT( "Saving", clock() - clk );
 }
 
 /**Function*************************************************************
@@ -127,7 +127,7 @@ void Rwr_ManLoadFromArray( Rwr_Man_t * p, int fVerbose )
     if ( fVerbose )
     {
         printf( "The number of classes = %d. Canonical nodes = %d.\n", p->nClasses, p->nAdded );
-        printf( "The number of nodes loaded = %d.  ", nEntries );  PRT( "Loading", clock() - clk );
+        printf( "The number of nodes loaded = %d.  ", nEntries );  ABC_PRT( "Loading", clock() - clk );
     }
 }
 
@@ -151,7 +151,7 @@ void Rwr_ManWriteToFile( Rwr_Man_t * p, char * pFileName )
     int i, nEntries, clk = clock();
     // prepare the buffer
     nEntries = p->vForest->nSize - 5;
-    pBuffer = ALLOC( unsigned, nEntries * 2 );
+    pBuffer = ABC_ALLOC( unsigned, nEntries * 2 );
     for ( i = 0; i < nEntries; i++ )
     {
         pNode = p->vForest->pArray[i+5];
@@ -164,9 +164,9 @@ void Rwr_ManWriteToFile( Rwr_Man_t * p, char * pFileName )
     pFile = fopen( pFileName, "wb" );
     fwrite( &nEntries, sizeof(int), 1, pFile );
     fwrite( pBuffer, sizeof(unsigned), nEntries * 2, pFile );
-    free( pBuffer );
+    ABC_FREE( pBuffer );
     fclose( pFile );
-    printf( "The number of nodes saved = %d.   ", nEntries );  PRT( "Saving", clock() - clk );
+    printf( "The number of nodes saved = %d.   ", nEntries );  ABC_PRT( "Saving", clock() - clk );
 }
 
 /**Function*************************************************************
@@ -196,7 +196,7 @@ void Rwr_ManLoadFromFile( Rwr_Man_t * p, char * pFileName )
         return;
     }
     fread( &nEntries, sizeof(int), 1, pFile );
-    pBuffer = ALLOC( unsigned, nEntries * 2 );
+    pBuffer = ABC_ALLOC( unsigned, nEntries * 2 );
     fread( pBuffer, sizeof(unsigned), nEntries * 2, pFile );
     fclose( pFile );
     // reconstruct the forest
@@ -218,9 +218,9 @@ void Rwr_ManLoadFromFile( Rwr_Man_t * p, char * pFileName )
 //        Rwr_ManTryNode( p, p0, p1, Level, Volume );
         Rwr_ManAddNode( p, p0, p1, fExor, Level, Volume + fExor );
     }
-    free( pBuffer );
+    ABC_FREE( pBuffer );
     printf( "The number of classes = %d. Canonical nodes = %d.\n", p->nClasses, p->nAdded );
-    printf( "The number of nodes loaded = %d.   ", nEntries );  PRT( "Loading", clock() - clk );
+    printf( "The number of nodes loaded = %d.   ", nEntries );  ABC_PRT( "Loading", clock() - clk );
 }
 
 
@@ -260,7 +260,7 @@ char * Rwr_ManGetPractical( Rwr_Man_t * p )
 {
     char * pPractical;
     int i;
-    pPractical = ALLOC( char, p->nFuncs );
+    pPractical = ABC_ALLOC( char, p->nFuncs );
     memset( pPractical, 0, sizeof(char) * p->nFuncs );
     pPractical[0] = 1;
     for ( i = 1; ; i++ )
diff --git a/src/opt/sim/sim.h b/src/opt/sim/sim.h
index 7fcf5ae6..89eaafac 100644
--- a/src/opt/sim/sim.h
+++ b/src/opt/sim/sim.h
@@ -21,10 +21,6 @@
 #ifndef __SIM_H__
 #define __SIM_H__
 
-#ifdef __cplusplus
-extern "C" {
-#endif
-
 /*
     The ideas realized in this package are described in the paper:
     "Detecting Symmetries in Boolean Functions using Circuit Representation, 
@@ -39,6 +35,10 @@ extern "C" {
 ///                         PARAMETERS                               ///
 ////////////////////////////////////////////////////////////////////////
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                         BASIC TYPES                              ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/sim/simMan.c b/src/opt/sim/simMan.c
index 139a1a05..6a86e25f 100644
--- a/src/opt/sim/simMan.c
+++ b/src/opt/sim/simMan.c
@@ -45,7 +45,7 @@ Sym_Man_t * Sym_ManStart( Abc_Ntk_t * pNtk, int fVerbose )
     Sym_Man_t * p;
     int i, v; 
     // start the manager
-    p = ALLOC( Sym_Man_t, 1 );
+    p = ABC_ALLOC( Sym_Man_t, 1 );
     memset( p, 0, sizeof(Sym_Man_t) );
     p->pNtk = pNtk;
     p->vNodes     = Abc_NtkDfs( pNtk, 0 );
@@ -66,9 +66,9 @@ Sym_Man_t * Sym_ManStart( Abc_Ntk_t * pNtk, int fVerbose )
         p->vMatrNonSymms->pArray[i] = Extra_BitMatrixStart( p->nInputs );
     }
     // temporary patterns
-    p->uPatRand = ALLOC( unsigned, p->nSimWords );
-    p->uPatCol  = ALLOC( unsigned, p->nSimWords );
-    p->uPatRow  = ALLOC( unsigned, p->nSimWords );
+    p->uPatRand = ABC_ALLOC( unsigned, p->nSimWords );
+    p->uPatCol  = ABC_ALLOC( unsigned, p->nSimWords );
+    p->uPatRow  = ABC_ALLOC( unsigned, p->nSimWords );
     p->vVarsU   = Vec_IntStart( 100 );
     p->vVarsV   = Vec_IntStart( 100 );
     // compute supports
@@ -77,7 +77,7 @@ Sym_Man_t * Sym_ManStart( Abc_Ntk_t * pNtk, int fVerbose )
     for ( i = 0; i < p->nOutputs; i++ )
         for ( v = 0; v < p->nInputs; v++ )
             if ( Sim_SuppFunHasVar( p->vSuppFun, i, v ) )
-                Vec_VecPush( p->vSupports, i, (void *)(PORT_PTRUINT_T)v );
+                Vec_VecPush( p->vSupports, i, (void *)(ABC_PTRUINT_T)v );
     return p;
 }
 
@@ -112,10 +112,10 @@ void Sym_ManStop( Sym_Man_t * p )
     Vec_IntFree( p->vPairsTotal );
     Vec_IntFree( p->vPairsSym );
     Vec_IntFree( p->vPairsNonSym );
-    FREE( p->uPatRand );
-    FREE( p->uPatCol );
-    FREE( p->uPatRow );
-    free( p );
+    ABC_FREE( p->uPatRand );
+    ABC_FREE( p->uPatCol );
+    ABC_FREE( p->uPatRow );
+    ABC_FREE( p );
 }
 
 /**Function*************************************************************
@@ -139,13 +139,13 @@ void Sym_ManPrintStats( Sym_Man_t * p )
     printf( "Total var pairs    = %8d.\n", p->nPairsTotal );
     printf( "Sat runs SAT       = %8d.\n", p->nSatRunsSat );
     printf( "Sat runs UNSAT     = %8d.\n", p->nSatRunsUnsat );
-    PRT( "Structural  ", p->timeStruct );
-    PRT( "Simulation  ", p->timeSim );
-    PRT( "Matrix      ", p->timeMatr );
-    PRT( "Counting    ", p->timeCount );
-    PRT( "Fraiging    ", p->timeFraig );
-    PRT( "SAT         ", p->timeSat );
-    PRT( "TOTAL       ", p->timeTotal );
+    ABC_PRT( "Structural  ", p->timeStruct );
+    ABC_PRT( "Simulation  ", p->timeSim );
+    ABC_PRT( "Matrix      ", p->timeMatr );
+    ABC_PRT( "Counting    ", p->timeCount );
+    ABC_PRT( "Fraiging    ", p->timeFraig );
+    ABC_PRT( "SAT         ", p->timeSat );
+    ABC_PRT( "TOTAL       ", p->timeTotal );
 }
 
 
@@ -164,7 +164,7 @@ Sim_Man_t * Sim_ManStart( Abc_Ntk_t * pNtk, int fLightweight )
 {
     Sim_Man_t * p;
     // start the manager
-    p = ALLOC( Sim_Man_t, 1 );
+    p = ABC_ALLOC( Sim_Man_t, 1 );
     memset( p, 0, sizeof(Sim_Man_t) );
     p->pNtk = pNtk;
     p->nInputs    = Abc_NtkCiNum(p->pNtk);
@@ -213,7 +213,7 @@ void Sim_ManStop( Sim_Man_t * p )
     if ( p->pMmPat )       Extra_MmFixedStop( p->pMmPat );
     if ( p->vFifo )        Vec_PtrFree( p->vFifo );
     if ( p->vDiffs )       Vec_IntFree( p->vDiffs );
-    free( p );
+    ABC_FREE( p );
 }
 
 /**Function*************************************************************
@@ -235,11 +235,11 @@ void Sim_ManPrintStats( Sim_Man_t * p )
     printf( "Total struct supps = %8d.\n", Sim_UtilCountSuppSizes(p, 1) );
     printf( "Sat runs SAT       = %8d.\n", p->nSatRunsSat );
     printf( "Sat runs UNSAT     = %8d.\n", p->nSatRunsUnsat );
-    PRT( "Simulation  ", p->timeSim );
-    PRT( "Traversal   ", p->timeTrav );
-    PRT( "Fraiging    ", p->timeFraig );
-    PRT( "SAT         ", p->timeSat );
-    PRT( "TOTAL       ", p->timeTotal );
+    ABC_PRT( "Simulation  ", p->timeSim );
+    ABC_PRT( "Traversal   ", p->timeTrav );
+    ABC_PRT( "Fraiging    ", p->timeFraig );
+    ABC_PRT( "SAT         ", p->timeSat );
+    ABC_PRT( "TOTAL       ", p->timeTotal );
 }
 
 
diff --git a/src/opt/sim/simSupp.c b/src/opt/sim/simSupp.c
index e6ba853c..f84fedc4 100644
--- a/src/opt/sim/simSupp.c
+++ b/src/opt/sim/simSupp.c
@@ -319,7 +319,7 @@ void Sim_ComputeSuppSetTargets( Sim_Man_t * p )
         // find vars in the structural support that are not in the functional support
         Sim_UtilInfoDetectNews( pSuppFun, pSuppStr, p->nSuppWords, p->vDiffs );
         Vec_IntForEachEntry( p->vDiffs, Num, k )
-            Vec_VecPush( p->vSuppTargs, Num, (void *)(PORT_PTRUINT_T)i );
+            Vec_VecPush( p->vSuppTargs, Num, (void *)(ABC_PTRUINT_T)i );
     }
 }
 
@@ -460,7 +460,7 @@ void Sim_SolveTargetsUsingSat( Sim_Man_t * p, int Limit )
     Vec_VecForEachEntryReverse( p->vSuppTargs, pEntry, Input, k )
     {
         p->nSatRuns++;
-        Output = (int)(PORT_PTRUINT_T)pEntry;
+        Output = (int)(ABC_PTRUINT_T)pEntry;
 
         // set up the miter for the two cofactors of this output w.r.t. this input
         pMiter = Abc_NtkMiterForCofactors( p->pNtk, Output, Input, -1 );
@@ -545,7 +545,7 @@ int Sim_NtkSimTwoPats_rec( Abc_Obj_t * pNode )
 {
     int Value0, Value1;
     if ( Abc_NodeIsTravIdCurrent( pNode ) )
-        return (int)(PORT_PTRUINT_T)pNode->pCopy;
+        return (int)(ABC_PTRUINT_T)pNode->pCopy;
     Abc_NodeSetTravIdCurrent( pNode );
     Value0 = Sim_NtkSimTwoPats_rec( Abc_ObjFanin0(pNode) );
     Value1 = Sim_NtkSimTwoPats_rec( Abc_ObjFanin1(pNode) );
@@ -553,7 +553,7 @@ int Sim_NtkSimTwoPats_rec( Abc_Obj_t * pNode )
         Value0 = ~Value0;
     if ( Abc_ObjFaninC1(pNode) )
         Value1 = ~Value1;
-    pNode->pCopy = (Abc_Obj_t *)(PORT_PTRUINT_T)(Value0 & Value1);
+    pNode->pCopy = (Abc_Obj_t *)(ABC_PTRUINT_T)(Value0 & Value1);
     return Value0 & Value1;
 }
 
diff --git a/src/opt/sim/simSymStr.c b/src/opt/sim/simSymStr.c
index d52c4328..9ff2f590 100644
--- a/src/opt/sim/simSymStr.c
+++ b/src/opt/sim/simSymStr.c
@@ -96,7 +96,7 @@ void Sim_SymmsStructCompute( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMatrs, Vec_Ptr_t * v
 //        if ( !Abc_NodeIsConst(pTemp) )
             Vec_IntFree( SIM_READ_SYMMS(pTemp) );
     Vec_PtrFree( vNodes );
-    free( pMap );
+    ABC_FREE( pMap );
 }
 
 /**Function*************************************************************
@@ -471,7 +471,7 @@ int * Sim_SymmsCreateMap( Abc_Ntk_t * pNtk )
     int * pMap;
     Abc_Obj_t * pNode;
     int i;
-    pMap = ALLOC( int, Abc_NtkObjNumMax(pNtk) );
+    pMap = ABC_ALLOC( int, Abc_NtkObjNumMax(pNtk) );
     for ( i = 0; i < Abc_NtkObjNumMax(pNtk); i++ )
         pMap[i] = -1;
     Abc_NtkForEachCi( pNtk, pNode, i )
diff --git a/src/opt/sim/simUtils.c b/src/opt/sim/simUtils.c
index b74f3abe..dba487d8 100644
--- a/src/opt/sim/simUtils.c
+++ b/src/opt/sim/simUtils.c
@@ -57,7 +57,7 @@ Vec_Ptr_t * Sim_UtilInfoAlloc( int nSize, int nWords, bool fClean )
     int i;
     assert( nSize > 0 && nWords > 0 );
     vInfo = Vec_PtrAlloc( nSize );
-    vInfo->pArray[0] = ALLOC( unsigned, nSize * nWords );
+    vInfo->pArray[0] = ABC_ALLOC( unsigned, nSize * nWords );
     if ( fClean )
         memset( vInfo->pArray[0], 0, sizeof(unsigned) * nSize * nWords );
     for ( i = 1; i < nSize; i++ )
@@ -79,7 +79,7 @@ Vec_Ptr_t * Sim_UtilInfoAlloc( int nSize, int nWords, bool fClean )
 ***********************************************************************/
 void Sim_UtilInfoFree( Vec_Ptr_t * p )
 {
-    free( p->pArray[0] );
+    ABC_FREE( p->pArray[0] );
     Vec_PtrFree( p );
 }