Version abc90215

14 files changed, 180 insertions, 238 deletions

diff --git a/src/misc/extra/extra.h b/src/misc/extra/extra.h
index d7a3e98c..f81479b3 100644
--- a/src/misc/extra/extra.h
+++ b/src/misc/extra/extra.h
@@ -29,10 +29,6 @@
 #ifndef __EXTRA_H__
 #define __EXTRA_H__
 
-#ifdef __cplusplus
-extern "C" {
-#endif
-
 #ifdef _WIN32
 #define inline __inline // compatible with MS VS 6.0
 #endif
@@ -46,14 +42,12 @@ extern "C" {
 #include <string.h>
 #include <assert.h>
 #include <time.h>
+#include "abc_global.h"
 #include "st.h"
 #include "cuddInt.h"
-#include "port_type.h"
 
-// catch memory leaks in Visual Studio
-#ifdef _DEBUG
-#define _CRTDBG_MAP_ALLOC
-#include <crtdbg.h>
+#ifdef __cplusplus
+extern "C" {
 #endif
 
 /*---------------------------------------------------------------------------*/
@@ -76,25 +70,9 @@ extern "C" {
 /* Macro declarations                                                        */
 /*---------------------------------------------------------------------------*/
 
-#ifdef WIN32
-#define ABC_DLLEXPORT __declspec(dllexport)
-#define ABC_DLLIMPORT __declspec(dllimport)
-#else  /* defined(WIN32) */
-#define ABC_DLLIMPORT
-#endif /* defined(WIN32) */
-
-#ifndef ABC_DLL
-#define ABC_DLL ABC_DLLIMPORT
-#endif
-
 typedef unsigned char      uint8;
 typedef unsigned short     uint16;
 typedef unsigned int       uint32;
-#ifdef WIN32
-typedef unsigned __int64   uint64;
-#else
-typedef unsigned long long uint64;
-#endif
 
 /* constants of the manager */
 #define     b0     Cudd_Not((dd)->one)
@@ -106,34 +84,21 @@ typedef unsigned long long uint64;
 
 // hash key macros
 #define hashKey1(a,TSIZE) \
-((PORT_PTRUINT_T)(a) % TSIZE)
+((ABC_PTRUINT_T)(a) % TSIZE)
 
 #define hashKey2(a,b,TSIZE) \
-(((PORT_PTRUINT_T)(a) + (PORT_PTRUINT_T)(b) * DD_P1) % TSIZE)
+(((ABC_PTRUINT_T)(a) + (ABC_PTRUINT_T)(b) * DD_P1) % TSIZE)
 
 #define hashKey3(a,b,c,TSIZE) \
-(((((PORT_PTRUINT_T)(a) + (PORT_PTRUINT_T)(b)) * DD_P1 + (PORT_PTRUINT_T)(c)) * DD_P2 ) % TSIZE)
+(((((ABC_PTRUINT_T)(a) + (ABC_PTRUINT_T)(b)) * DD_P1 + (ABC_PTRUINT_T)(c)) * DD_P2 ) % TSIZE)
 
 #define hashKey4(a,b,c,d,TSIZE) \
-((((((PORT_PTRUINT_T)(a) + (PORT_PTRUINT_T)(b)) * DD_P1 + (PORT_PTRUINT_T)(c)) * DD_P2 + \
-   (PORT_PTRUINT_T)(d)) * DD_P3) % TSIZE)
+((((((ABC_PTRUINT_T)(a) + (ABC_PTRUINT_T)(b)) * DD_P1 + (ABC_PTRUINT_T)(c)) * DD_P2 + \
+   (ABC_PTRUINT_T)(d)) * DD_P3) % TSIZE)
 
 #define hashKey5(a,b,c,d,e,TSIZE) \
-(((((((PORT_PTRUINT_T)(a) + (PORT_PTRUINT_T)(b)) * DD_P1 + (PORT_PTRUINT_T)(c)) * DD_P2 + \
-   (PORT_PTRUINT_T)(d)) * DD_P3 + (PORT_PTRUINT_T)(e)) * DD_P1) % TSIZE)
-
-#ifndef PRT
-#define PRT(a,t)  printf("%s = ", (a)); printf("%6.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC))
-#define PRTn(a,t)  printf("%s = ", (a)); printf("%6.2f sec  ", (float)(t)/(float)(CLOCKS_PER_SEC))
-#endif
-
-#ifndef PRTP
-#define PRTP(a,t,T)  printf("%s = ", (a)); printf("%6.2f sec (%6.2f %%)\n", (float)(t)/(float)(CLOCKS_PER_SEC), (T)? 100.0*(t)/(T) : 0.0)
-#endif
-
-#ifndef PRB
-#define PRB(dd,f)       printf("%s = ", #f); Extra_bddPrint(dd,f); printf("\n")
-#endif
+(((((((ABC_PTRUINT_T)(a) + (ABC_PTRUINT_T)(b)) * DD_P1 + (ABC_PTRUINT_T)(c)) * DD_P2 + \
+   (ABC_PTRUINT_T)(d)) * DD_P3 + (ABC_PTRUINT_T)(e)) * DD_P1) % TSIZE)
 
 /*===========================================================================*/
 /*     Various Utilities                                                     */
@@ -229,6 +194,10 @@ extern DdNode *     Extra_zddPrimes( DdManager * dd, DdNode * F );
 extern void         Extra_bddPermuteArray( DdManager * dd, DdNode ** bNodesIn, DdNode ** bNodesOut, int nNodes, int *permut );
 extern DdNode *     Extra_bddComputeCube( DdManager * dd, DdNode ** bXVars, int nVars );
 
+#ifndef ABC_PRB
+#define ABC_PRB(dd,f)       printf("%s = ", #f); Extra_bddPrint(dd,f); printf("\n")
+#endif
+
 /*=== extraBddKmap.c ================================================================*/
 
 /* displays the Karnaugh Map of a function */
@@ -617,33 +586,6 @@ extern unsigned    Extra_TruthSemiCanonicize( unsigned * pInOut, unsigned * pAux
 
 /*=== extraUtilUtil.c ================================================================*/
 
-#ifndef ABS
-#define ABS(a)            ((a) < 0 ? -(a) : (a))
-#endif
-
-#ifndef MAX
-#define MAX(a,b)        ((a) > (b) ? (a) : (b))
-#endif
-
-#ifndef MIN
-#define MIN(a,b)        ((a) < (b) ? (a) : (b))
-#endif
-
-#ifndef ALLOC
-#define ALLOC(type, num)     ((type *) malloc(sizeof(type) * (num)))
-#endif
-
-#ifndef FREE
-#define FREE(obj)             ((obj) ? (free((char *) (obj)), (obj) = 0) : 0)
-#endif
-
-#ifndef REALLOC
-#define REALLOC(type, obj, num)    \
-        ((obj) ? ((type *) realloc((char *)(obj), sizeof(type) * (num))) : \
-         ((type *) malloc(sizeof(type) * (num))))
-#endif
-
-
 extern long          Extra_CpuTime();
 extern double        Extra_CpuTimeDouble();
 extern int           Extra_GetSoftDataLimit();
diff --git a/src/misc/extra/extraBddAuto.c b/src/misc/extra/extraBddAuto.c
index 11612ef4..ebafb3a8 100644
--- a/src/misc/extra/extraBddAuto.c
+++ b/src/misc/extra/extraBddAuto.c
@@ -159,7 +159,7 @@ DdNode * Extra_bddSpaceFromFunctionFast( DdManager * dd, DdNode * bFunc )
     int i, lev;
 
     // get the support
-    pSupport = ALLOC( int, ddMax(dd->size,dd->sizeZ) );
+    pSupport = ABC_ALLOC( int, ddMax(dd->size,dd->sizeZ) );
     Extra_SupportArray( dd, bFunc, pSupport );
     nSupp = 0;
     for ( i = 0; i < dd->size; i++ )
@@ -171,14 +171,14 @@ DdNode * Extra_bddSpaceFromFunctionFast( DdManager * dd, DdNode * bFunc )
     {
         printf( "Cannot derive linear space, because DD manager does not have enough variables.\n" );
         fflush( stdout );
-        free( pSupport );
+        ABC_FREE( pSupport );
         return NULL;
     }
 
     // create the permutation arrays
-    pPermute     = ALLOC( int, dd->size );
-    pPermuteBack = ALLOC( int, dd->size );
-    pCompose     = ALLOC( DdNode *, dd->size );
+    pPermute     = ABC_ALLOC( int, dd->size );
+    pPermuteBack = ABC_ALLOC( int, dd->size );
+    pCompose     = ABC_ALLOC( DdNode *, dd->size );
     for ( i = 0; i < dd->size; i++ )
     {
         pPermute[i]     = i;
@@ -225,10 +225,10 @@ DdNode * Extra_bddSpaceFromFunctionFast( DdManager * dd, DdNode * bFunc )
 
     for ( i = 0; i < dd->size; i++ )
         Cudd_RecursiveDeref( dd, pCompose[i] );
-    free( pPermute );
-    free( pPermuteBack );
-    free( pCompose );
-    free( pSupport );
+    ABC_FREE( pPermute );
+    ABC_FREE( pPermuteBack );
+    ABC_FREE( pCompose );
+    ABC_FREE( pSupport );
 
     Cudd_Deref( bSpace );
     return bSpace;
@@ -500,11 +500,11 @@ DdNode ** Extra_bddSpaceExorGates( DdManager * dd, DdNode * bFuncRed, DdNode * z
     DdNode * zExor, * zTemp;
 
     // get the set of non-canonical variables
-    pVarsNonCan = ALLOC( int, ddMax(dd->size,dd->sizeZ) );
+    pVarsNonCan = ABC_ALLOC( int, ddMax(dd->size,dd->sizeZ) );
     Extra_SupportArray( dd, bFuncRed, pVarsNonCan );
 
     // allocate storage for the EXOR sets
-    pzRes = ALLOC( DdNode *, dd->size );
+    pzRes = ABC_ALLOC( DdNode *, dd->size );
     memset( pzRes, 0, sizeof(DdNode *) * dd->size );
 
     // go through all the equations
@@ -536,7 +536,7 @@ DdNode ** Extra_bddSpaceExorGates( DdManager * dd, DdNode * bFuncRed, DdNode * z
     }
     Cudd_RecursiveDerefZdd( dd, zEquRem );
 
-    free( pVarsNonCan );
+    ABC_FREE( pVarsNonCan );
     return pzRes;
 }
 
@@ -575,7 +575,7 @@ DdNode * extraBddSpaceFromFunction( DdManager * dd, DdNode * bF, DdNode * bG )
     // both bFunc and bCore are not constants
 
     // the operation is commutative - normalize the problem
-    if ( (unsigned)(PORT_PTRUINT_T)bF > (unsigned)(PORT_PTRUINT_T)bG )
+    if ( (unsigned)(ABC_PTRUINT_T)bF > (unsigned)(ABC_PTRUINT_T)bG )
         return extraBddSpaceFromFunction(dd, bG, bF);
 
 
diff --git a/src/misc/extra/extraBddCas.c b/src/misc/extra/extraBddCas.c
index 29382bfb..ccf7397d 100644
--- a/src/misc/extra/extraBddCas.c
+++ b/src/misc/extra/extraBddCas.c
@@ -226,7 +226,7 @@ Extra_bddEncodingNonStrict(
 //    s_EncSearchTime += clock() - clk;
 
     // allocate the temporary storage for the columns
-    s_pbTemp = (DdNode **) malloc( nColumns * sizeof(DdNode *) );
+    s_pbTemp = (DdNode **)ABC_ALLOC( char, nColumns * sizeof(DdNode *) );
 
 //    clk = clock();
     bResult = CreateTheCodes_rec( dd, bEncoded, 0, pCVars );   Cudd_Ref( bResult );
@@ -236,7 +236,7 @@ Extra_bddEncodingNonStrict(
     Cudd_RecursiveDeref( dd, bEncoded );
 //    Cudd_RecursiveDeref( dd, aEncoded );
 
-    free( s_pbTemp );
+    ABC_FREE( s_pbTemp );
 
     *pSimple = s_nVarsBest;
     Cudd_Deref( bResult );
@@ -306,7 +306,7 @@ st_table * Extra_bddNodePathsUnderCut( DdManager * dd, DdNode * bFunc, int CutLe
         st_foreach_item( Visited, gen, (char**)&aNode, (char**)&p ) 
         {
             Cudd_RecursiveDeref( dd, p->bSum );
-            free( p );
+            ABC_FREE( p );
         }
         st_free_table( Visited );
     }
@@ -394,7 +394,7 @@ int Extra_bddNodePathsUnderCutArray( DdManager * dd, DdNode ** paNodes, DdNode *
         st_foreach_item( Visited, gen, (char**)&aNode, (char**)&p ) 
         {
             Cudd_RecursiveDeref( dd, p->bSum );
-            free( p );
+            ABC_FREE( p );
         }
         st_free_table( Visited );
     }
@@ -1123,7 +1123,7 @@ void CountNodeVisits_rec( DdManager * dd, DdNode * aFunc, st_table * Visited )
     assert( !Cudd_IsComplement(aFunc) );
 
     // create the new traversal entry
-    p = (traventry *) malloc( sizeof(traventry) );
+    p = (traventry *) ABC_ALLOC( char, sizeof(traventry) );
     // set the initial sum of edges to zero BDD
     p->bSum = b0;   Cudd_Ref( b0 );
     // set the starting number of incoming edges
diff --git a/src/misc/extra/extraBddImage.c b/src/misc/extra/extraBddImage.c
index 23c1c682..11d60a40 100644
--- a/src/misc/extra/extraBddImage.c
+++ b/src/misc/extra/extraBddImage.c
@@ -170,7 +170,7 @@ Extra_ImageTree_t * Extra_bddImageStart(
     pNodes = Extra_CreateNodes( dd, nParts + 1, pParts, dd->size, pVars );
     
     // create the tree
-    pTree = ALLOC( Extra_ImageTree_t, 1 );
+    pTree = ABC_ALLOC( Extra_ImageTree_t, 1 );
     memset( pTree, 0, sizeof(Extra_ImageTree_t) );
     pTree->pCare = pNodes[nParts];
     pTree->fVerbose = fVerbose;
@@ -181,7 +181,7 @@ Extra_ImageTree_t * Extra_bddImageStart(
     // make sure the variables are gone
     for ( v = 0; v < dd->size; v++ )
         assert( pVars[v] == NULL );
-    FREE( pVars );
+    ABC_FREE( pVars );
 
     // merge the topmost nodes
     while ( (pTree->pRoot = Extra_MergeTopNodes( dd, nParts + 1, pNodes )) == NULL );
@@ -189,7 +189,7 @@ Extra_ImageTree_t * Extra_bddImageStart(
     // make sure the nodes are gone
     for ( v = 0; v < nParts + 1; v++ )
         assert( pNodes[v] == NULL );
-    FREE( pNodes );
+    ABC_FREE( pNodes );
 
 //    if ( fVerbose )
 //        Extra_bddImagePrintTree( pTree );
@@ -199,7 +199,7 @@ Extra_ImageTree_t * Extra_bddImageStart(
 
     // clean the partitions
     Extra_DeleteParts_rec( pTree->pRoot );
-    FREE( pParts );
+    ABC_FREE( pParts );
     return pTree;
 }
 
@@ -229,9 +229,9 @@ DdNode * Extra_bddImageCompute( Extra_ImageTree_t * pTree, DdNode * bCare )
         if ( bRem != b1 )
         {
 printf( "Original care set support: " );
-PRB( dd, pTree->bCareSupp );
+ABC_PRB( dd, pTree->bCareSupp );
 printf( "Current care set support: " );
-PRB( dd, bSupp );
+ABC_PRB( dd, bSupp );
             Cudd_RecursiveDeref( dd, bSupp );
             Cudd_RecursiveDeref( dd, bRem );
             printf( "The care set depends on some vars that were not in the care set during scheduling.\n" );
@@ -272,7 +272,7 @@ void Extra_bddImageTreeDelete( Extra_ImageTree_t * pTree )
     if ( pTree->bCareSupp )
         Cudd_RecursiveDeref( pTree->pRoot->dd, pTree->bCareSupp );
     Extra_bddImageTreeDelete_rec( pTree->pRoot );
-    FREE( pTree );
+    ABC_FREE( pTree );
 }
 
 /**Function*************************************************************
@@ -317,11 +317,11 @@ Extra_ImagePart_t ** Extra_CreateParts( DdManager * dd,
     int i;
 
     // start the partitions
-    pParts = ALLOC( Extra_ImagePart_t *, nParts + 1 );
+    pParts = ABC_ALLOC( Extra_ImagePart_t *, nParts + 1 );
     // create structures for each variable
     for ( i = 0; i < nParts; i++ )
     {
-        pParts[i] = ALLOC( Extra_ImagePart_t, 1 );
+        pParts[i] = ABC_ALLOC( Extra_ImagePart_t, 1 );
         pParts[i]->bFunc  = pbParts[i];                           Cudd_Ref( pParts[i]->bFunc );
         pParts[i]->bSupp  = Cudd_Support( dd, pParts[i]->bFunc ); Cudd_Ref( pParts[i]->bSupp );
         pParts[i]->nSupp  = Extra_bddSuppSize( dd, pParts[i]->bSupp );
@@ -329,7 +329,7 @@ Extra_ImagePart_t ** Extra_CreateParts( DdManager * dd,
         pParts[i]->iPart  = i;
     }
     // add the care set as the last partition
-    pParts[nParts] = ALLOC( Extra_ImagePart_t, 1 );
+    pParts[nParts] = ABC_ALLOC( Extra_ImagePart_t, 1 );
     pParts[nParts]->bFunc = bCare;                                     Cudd_Ref( pParts[nParts]->bFunc );
     pParts[nParts]->bSupp = Cudd_Support( dd, pParts[nParts]->bFunc ); Cudd_Ref( pParts[nParts]->bSupp );
     pParts[nParts]->nSupp = Extra_bddSuppSize( dd, pParts[nParts]->bSupp );
@@ -359,11 +359,11 @@ Extra_ImageVar_t ** Extra_CreateVars( DdManager * dd,
     int nVarsTotal, iVar, p, Counter;
 
     // put all the functions into one array
-    pbFuncs = ALLOC( DdNode *, nParts );
+    pbFuncs = ABC_ALLOC( DdNode *, nParts );
     for ( p = 0; p < nParts; p++ )
         pbFuncs[p] = pParts[p]->bSupp;
     bSupp = Cudd_VectorSupport( dd, pbFuncs, nParts );  Cudd_Ref( bSupp );
-    FREE( pbFuncs );
+    ABC_FREE( pbFuncs );
 
     // remove the NS vars
     bCubeNs = Cudd_bddComputeCube( dd, pbVars, NULL, nVars );        Cudd_Ref( bCubeNs );
@@ -375,13 +375,13 @@ Extra_ImageVar_t ** Extra_CreateVars( DdManager * dd,
     nVarsTotal = Extra_bddSuppSize( dd, bSupp );
 
     // start the variables
-    pVars = ALLOC( Extra_ImageVar_t *, dd->size );
+    pVars = ABC_ALLOC( Extra_ImageVar_t *, dd->size );
     memset( pVars, 0, sizeof(Extra_ImageVar_t *) * dd->size );
     // create structures for each variable
     for ( bSuppTemp = bSupp; bSuppTemp != b1; bSuppTemp = cuddT(bSuppTemp) )
     {
         iVar = bSuppTemp->index;
-        pVars[iVar] = ALLOC( Extra_ImageVar_t, 1 );
+        pVars[iVar] = ABC_ALLOC( Extra_ImageVar_t, 1 );
         pVars[iVar]->iNum = iVar;
         // collect all the parts this var belongs to
         Counter = 0;
@@ -428,11 +428,11 @@ Extra_ImageNode_t ** Extra_CreateNodes( DdManager * dd,
     Extra_ImagePart_t * pPart;    // the partition (temporary)
 */
     // start the partitions
-    pNodes = ALLOC( Extra_ImageNode_t *, nParts );
+    pNodes = ABC_ALLOC( Extra_ImageNode_t *, nParts );
     // create structures for each leaf nodes
     for ( i = 0; i < nParts; i++ )
     {
-        pNodes[i] = ALLOC( Extra_ImageNode_t, 1 );
+        pNodes[i] = ABC_ALLOC( Extra_ImageNode_t, 1 );
         memset( pNodes[i], 0, sizeof(Extra_ImageNode_t) );
         pNodes[i]->dd    = dd;
         pNodes[i]->pPart = pParts[i];
@@ -459,7 +459,7 @@ Extra_ImageNode_t ** Extra_CreateNodes( DdManager * dd,
         }
         // remove these  variables
         Cudd_RecursiveDeref( dd, pVars[v]->bParts );
-        FREE( pVars[v] );
+        ABC_FREE( pVars[v] );
     }
 
     // assign the leaf node images
@@ -494,9 +494,9 @@ Extra_ImageNode_t ** Extra_CreateNodes( DdManager * dd,
     for ( i = 0; i < nParts; i++ )
     {
         pNode = pNodes[i];
-PRB( dd, pNode->bCube );
-PRB( dd, pNode->pPart->bFunc );
-PRB( dd, pNode->pPart->bSupp );
+ABC_PRB( dd, pNode->bCube );
+ABC_PRB( dd, pNode->pPart->bFunc );
+ABC_PRB( dd, pNode->pPart->bSupp );
 printf( "\n" );
     }
 */
@@ -525,7 +525,7 @@ void Extra_DeleteParts_rec( Extra_ImageNode_t * pNode )
     pPart = pNode->pPart;
     Cudd_RecursiveDeref( pNode->dd, pPart->bFunc );
     Cudd_RecursiveDeref( pNode->dd, pPart->bSupp );
-    FREE( pNode->pPart );
+    ABC_FREE( pNode->pPart );
 }
 
 /**Function*************************************************************
@@ -550,7 +550,7 @@ void Extra_bddImageTreeDelete_rec( Extra_ImageNode_t * pNode )
     if ( pNode->bImage )
         Cudd_RecursiveDeref( pNode->dd, pNode->bImage );
     assert( pNode->pPart == NULL );
-    FREE( pNode );
+    ABC_FREE( pNode );
 }
 
 /**Function*************************************************************
@@ -663,11 +663,11 @@ int Extra_BuildTreeNode( DdManager * dd,
                 Cudd_RecursiveDeref( dd, bTemp );
                 // clean this var
                 Cudd_RecursiveDeref( dd, pVars[v]->bParts );
-                FREE( pVars[v] );
+                ABC_FREE( pVars[v] );
             }
         // clean the best var
         Cudd_RecursiveDeref( dd, pVars[iVarBest]->bParts );
-        FREE( pVars[iVarBest] );
+        ABC_FREE( pVars[iVarBest] );
 
         // combines two nodes
         pNode = Extra_CombineTwoNodes( dd, bCube, pNode1, pNode2 );
@@ -783,7 +783,7 @@ Extra_ImageNode_t * Extra_CombineTwoNodes( DdManager * dd, DdNode * bCube,
     Extra_ImagePart_t * pPart;
 
     // create a new partition
-    pPart = ALLOC( Extra_ImagePart_t, 1 );
+    pPart = ABC_ALLOC( Extra_ImagePart_t, 1 );
     memset( pPart, 0, sizeof(Extra_ImagePart_t) );
     // create the function
     pPart->bFunc = Cudd_bddAndAbstract( dd, pNode1->pPart->bFunc, pNode2->pPart->bFunc, bCube );
@@ -796,12 +796,12 @@ Extra_ImageNode_t * Extra_CombineTwoNodes( DdManager * dd, DdNode * bCube,
     pPart->nNodes = Cudd_DagSize( pPart->bFunc );
     pPart->iPart = -1;
 /*
-PRB( dd, pNode1->pPart->bSupp );
-PRB( dd, pNode2->pPart->bSupp );
-PRB( dd, pPart->bSupp );
+ABC_PRB( dd, pNode1->pPart->bSupp );
+ABC_PRB( dd, pNode2->pPart->bSupp );
+ABC_PRB( dd, pPart->bSupp );
 */
     // create a new node
-    pNode = ALLOC( Extra_ImageNode_t, 1 );
+    pNode = ABC_ALLOC( Extra_ImageNode_t, 1 );
     memset( pNode, 0, sizeof(Extra_ImageNode_t) );
     pNode->dd     = dd;
     pNode->pPart  = pPart;
@@ -1013,7 +1013,7 @@ void Extra_bddImagePrintTree_rec( Extra_ImageNode_t * pNode, int Offset )
         printf( "<%d> ", pNode->pPart->iPart );
         if ( Cube != NULL )
         {
-            PRB( pNode->dd, Cube );
+            ABC_PRB( pNode->dd, Cube );
         }
         else
             printf( "\n" );
@@ -1023,7 +1023,7 @@ void Extra_bddImagePrintTree_rec( Extra_ImageNode_t * pNode, int Offset )
     printf( "<*> " );
     if ( Cube != NULL )
     {
-        PRB( pNode->dd, Cube );
+        ABC_PRB( pNode->dd, Cube );
     }
     else
         printf( "\n" );
@@ -1069,7 +1069,7 @@ Extra_ImageTree2_t * Extra_bddImageStart2(
     DdNode * bCubeAll, * bCubeNot, * bTemp;
     int i;
 
-    pTree = ALLOC( Extra_ImageTree2_t, 1 );
+    pTree = ABC_ALLOC( Extra_ImageTree2_t, 1 );
     pTree->dd = dd;
     pTree->bImage = NULL;
 
@@ -1130,7 +1130,7 @@ void Extra_bddImageTreeDelete2( Extra_ImageTree2_t * pTree )
         Cudd_RecursiveDeref( pTree->dd, pTree->bCube );
     if ( pTree->bImage )
         Cudd_RecursiveDeref( pTree->dd, pTree->bImage );
-    FREE( pTree );
+    ABC_FREE( pTree );
 }
 
 /**Function*************************************************************
diff --git a/src/misc/extra/extraBddMisc.c b/src/misc/extra/extraBddMisc.c
index 8b8bdd81..e17d1744 100644
--- a/src/misc/extra/extraBddMisc.c
+++ b/src/misc/extra/extraBddMisc.c
@@ -112,7 +112,7 @@ DdNode * Extra_TransferLevelByLevel( DdManager * ddSource, DdManager * ddDestina
 
     nMin = ddMin(ddSource->size, ddDestination->size);
     nMax = ddMax(ddSource->size, ddDestination->size);
-    pPermute = ALLOC( int, nMax );
+    pPermute = ABC_ALLOC( int, nMax );
     // set up the variable permutation
     for ( i = 0; i < nMin; i++ )
         pPermute[ ddSource->invperm[i] ] = ddDestination->invperm[i];
@@ -122,7 +122,7 @@ DdNode * Extra_TransferLevelByLevel( DdManager * ddSource, DdManager * ddDestina
             pPermute[ ddSource->invperm[i] ] = -1;
     }
     bRes = Extra_TransferPermute( ddSource, ddDestination, f, pPermute );
-    FREE( pPermute );
+    ABC_FREE( pPermute );
     return bRes;
 }
 
@@ -145,7 +145,7 @@ DdNode * Extra_bddRemapUp(
     DdNode * bSupp, * bTemp, * bRes;
     int Counter;
 
-    pPermute = ALLOC( int, dd->size );
+    pPermute = ABC_ALLOC( int, dd->size );
 
     // get support
     bSupp = Cudd_Support( dd, bF );    Cudd_Ref( bSupp );
@@ -164,7 +164,7 @@ DdNode * Extra_bddRemapUp(
 
     // return
     Cudd_Deref( bRes );
-    free( pPermute );
+    ABC_FREE( pPermute );
     return bRes;
 }
 
@@ -584,7 +584,7 @@ DdNode *  Extra_bddFindOneCube( DdManager * dd, DdNode * bF )
     int v;
 
     // get the vector of variables in the cube
-    s_Temp = ALLOC( char, dd->size );
+    s_Temp = ABC_ALLOC( char, dd->size );
     Cudd_bddPickOneCube( dd, bF, s_Temp );
 
     // start the cube
@@ -603,7 +603,7 @@ DdNode *  Extra_bddFindOneCube( DdManager * dd, DdNode * bF )
             Cudd_RecursiveDeref( dd, bTemp );
         }
     Cudd_Deref(bCube);
-    free( s_Temp );
+    ABC_FREE( s_Temp );
     return bCube;
 }
 
@@ -745,7 +745,7 @@ DdNode * Extra_bddSupportNegativeCube( DdManager * dd, DdNode * f )
 
     /* Allocate and initialize support array for ddSupportStep. */
     size = ddMax( dd->size, dd->sizeZ );
-    support = ALLOC( int, size );
+    support = ABC_ALLOC( int, size );
     if ( support == NULL )
     {
         dd->errorCode = CUDD_MEMORY_OUT;
@@ -793,7 +793,7 @@ DdNode * Extra_bddSupportNegativeCube( DdManager * dd, DdNode * f )
     }
     while ( dd->reordered == 1 );
 
-    FREE( support );
+    ABC_FREE( support );
     if ( res != NULL )
         cuddDeref( res );
     return ( res );
diff --git a/src/misc/extra/extraBddSymm.c b/src/misc/extra/extraBddSymm.c
index 666814f6..e42130d4 100644
--- a/src/misc/extra/extraBddSymm.c
+++ b/src/misc/extra/extraBddSymm.c
@@ -207,12 +207,12 @@ Extra_SymmInfo_t * Extra_SymmPairsAllocate( int nVars )
     Extra_SymmInfo_t * p;
 
     // allocate and clean the storage for symmetry info
-    p = ALLOC( Extra_SymmInfo_t, 1 );
+    p = ABC_ALLOC( Extra_SymmInfo_t, 1 );
     memset( p, 0, sizeof(Extra_SymmInfo_t) );
     p->nVars     = nVars;
-    p->pVars     = ALLOC( int, nVars );  
-    p->pSymms    = ALLOC( char *, nVars );  
-    p->pSymms[0] = ALLOC( char  , nVars * nVars );
+    p->pVars     = ABC_ALLOC( int, nVars );  
+    p->pSymms    = ABC_ALLOC( char *, nVars );  
+    p->pSymms[0] = ABC_ALLOC( char  , nVars * nVars );
     memset( p->pSymms[0], 0, nVars * nVars * sizeof(char) );
 
     for ( i = 1; i < nVars; i++ )
@@ -234,10 +234,10 @@ Extra_SymmInfo_t * Extra_SymmPairsAllocate( int nVars )
 ******************************************************************************/
 void Extra_SymmPairsDissolve( Extra_SymmInfo_t * p )
 {
-    free( p->pVars );
-    free( p->pSymms[0] );
-    free( p->pSymms    );
-    free( p );
+    ABC_FREE( p->pVars );
+    ABC_FREE( p->pSymms[0] );
+    ABC_FREE( p->pSymms    );
+    ABC_FREE( p );
 } /* end of Extra_SymmPairsDissolve */
 
 /**Function********************************************************************
@@ -298,7 +298,7 @@ Extra_SymmInfo_t * Extra_SymmPairsCreateFromZdd( DdManager * dd, DdNode * zPairs
     p = Extra_SymmPairsAllocate( nSuppSize );
 
     // allocate the storage for the temporary map
-    pMapVars2Nums = ALLOC( int, dd->size );
+    pMapVars2Nums = ABC_ALLOC( int, dd->size );
     memset( pMapVars2Nums, 0, dd->size * sizeof(int) );
 
     // assign the variables
@@ -337,7 +337,7 @@ Extra_SymmInfo_t * Extra_SymmPairsCreateFromZdd( DdManager * dd, DdNode * zPairs
     } // for each cube 
     Cudd_RecursiveDerefZdd( dd, zSet );
 
-    FREE( pMapVars2Nums );
+    ABC_FREE( pMapVars2Nums );
     return p;
 
 } /* end of Extra_SymmPairsCreateFromZdd */
diff --git a/src/misc/extra/extraBddUnate.c b/src/misc/extra/extraBddUnate.c
index 92396c38..715731bd 100644
--- a/src/misc/extra/extraBddUnate.c
+++ b/src/misc/extra/extraBddUnate.c
@@ -153,10 +153,10 @@ Extra_UnateInfo_t *  Extra_UnateInfoAllocate( int nVars )
 {
     Extra_UnateInfo_t * p;
     // allocate and clean the storage for unateness info
-    p = ALLOC( Extra_UnateInfo_t, 1 );
+    p = ABC_ALLOC( Extra_UnateInfo_t, 1 );
     memset( p, 0, sizeof(Extra_UnateInfo_t) );
     p->nVars     = nVars;
-    p->pVars     = ALLOC( Extra_UnateVar_t, nVars );  
+    p->pVars     = ABC_ALLOC( Extra_UnateVar_t, nVars );  
     memset( p->pVars, 0, nVars * sizeof(Extra_UnateVar_t) );
     return p;
 } /* end of Extra_UnateInfoAllocate */
@@ -174,8 +174,8 @@ Extra_UnateInfo_t *  Extra_UnateInfoAllocate( int nVars )
 ******************************************************************************/
 void Extra_UnateInfoDissolve( Extra_UnateInfo_t * p )
 {
-    free( p->pVars );
-    free( p );
+    ABC_FREE( p->pVars );
+    ABC_FREE( p );
 } /* end of Extra_UnateInfoDissolve */
 
 /**Function********************************************************************
@@ -193,7 +193,7 @@ void Extra_UnateInfoPrint( Extra_UnateInfo_t * p )
 {
     char * pBuffer;
     int i;
-    pBuffer = ALLOC( char, p->nVarsMax+1 );
+    pBuffer = ABC_ALLOC( char, p->nVarsMax+1 );
     memset( pBuffer, ' ', p->nVarsMax );
     pBuffer[p->nVarsMax] = 0;
     for ( i = 0; i < p->nVars; i++ )
@@ -204,7 +204,7 @@ void Extra_UnateInfoPrint( Extra_UnateInfo_t * p )
         else
             pBuffer[ p->pVars[i].iVar ] = '.';
     printf( "%s\n", pBuffer );
-    free( pBuffer );
+    ABC_FREE( pBuffer );
 } /* end of Extra_UnateInfoPrint */
 
 
@@ -234,7 +234,7 @@ Extra_UnateInfo_t * Extra_UnateInfoCreateFromZdd( DdManager * dd, DdNode * zPair
     p = Extra_UnateInfoAllocate( nSuppSize );
 
     // allocate the storage for the temporary map
-    pMapVars2Nums = ALLOC( int, dd->size );
+    pMapVars2Nums = ABC_ALLOC( int, dd->size );
     memset( pMapVars2Nums, 0, dd->size * sizeof(int) );
 
     // assign the variables
@@ -269,7 +269,7 @@ Extra_UnateInfo_t * Extra_UnateInfoCreateFromZdd( DdManager * dd, DdNode * zPair
 
     } // for each cube 
     Cudd_RecursiveDerefZdd( dd, zSet );
-    FREE( pMapVars2Nums );
+    ABC_FREE( pMapVars2Nums );
     return p;
 
 } /* end of Extra_UnateInfoCreateFromZdd */
diff --git a/src/misc/extra/extraUtilBitMatrix.c b/src/misc/extra/extraUtilBitMatrix.c
index b860a538..dd63e05c 100644
--- a/src/misc/extra/extraUtilBitMatrix.c
+++ b/src/misc/extra/extraUtilBitMatrix.c
@@ -79,14 +79,14 @@ Extra_BitMat_t * Extra_BitMatrixStart( int nSize )
 {
     Extra_BitMat_t * p;
     int i;
-    p = ALLOC( Extra_BitMat_t, 1 );
+    p = ABC_ALLOC( Extra_BitMat_t, 1 );
     memset( p, 0, sizeof(Extra_BitMat_t) );
     p->nSize     = nSize;
     p->nBitShift = (sizeof(unsigned) == 4) ?  5:  6;
     p->uMask     = (sizeof(unsigned) == 4) ? 31: 63;
     p->nWords    = nSize / (8 * sizeof(unsigned)) + ((nSize % (8 * sizeof(unsigned))) > 0);
-    p->ppData    = ALLOC( unsigned *, nSize );
-    p->ppData[0] = ALLOC( unsigned, nSize * p->nWords );
+    p->ppData    = ABC_ALLOC( unsigned *, nSize );
+    p->ppData[0] = ABC_ALLOC( unsigned, nSize * p->nWords );
     memset( p->ppData[0], 0, sizeof(unsigned) * nSize * p->nWords );
     for ( i = 1; i < nSize; i++ )
         p->ppData[i] = p->ppData[i-1] + p->nWords;
@@ -122,9 +122,9 @@ void Extra_BitMatrixClean( Extra_BitMat_t * p )
 ***********************************************************************/
 void Extra_BitMatrixStop( Extra_BitMat_t * p )
 {
-    FREE( p->ppData[0] );
-    FREE( p->ppData );
-    FREE( p );
+    ABC_FREE( p->ppData[0] );
+    ABC_FREE( p->ppData );
+    ABC_FREE( p );
 }
 
 /**Function*************************************************************
diff --git a/src/misc/extra/extraUtilFile.c b/src/misc/extra/extraUtilFile.c
index 44dff1e0..96cf8601 100644
--- a/src/misc/extra/extraUtilFile.c
+++ b/src/misc/extra/extraUtilFile.c
@@ -98,7 +98,7 @@ char * Extra_FileGetSimilarName( char * pFileNameWrong, char * pS1, char * pS2,
             }
         }
     }
-    FREE( pFileGen );
+    ABC_FREE( pFileGen );
     if ( pFile )
     {
         fclose( pFile );
@@ -238,7 +238,7 @@ char * Extra_FileRead( FILE * pFile )
     // move the file current reading position to the beginning
     rewind( pFile ); 
     // load the contents of the file into memory
-    pBuffer = ALLOC( char, nFileSize + 3 );
+    pBuffer = ABC_ALLOC( char, nFileSize + 3 );
     fread( pBuffer, nFileSize, 1, pFile );
     // terminate the string with '\0'
     pBuffer[ nFileSize + 0] = '\n';
@@ -482,9 +482,9 @@ char * Extra_StringAppend( char * pStrGiven, char * pStrAdd )
     char * pTemp;
     if ( pStrGiven )
     {
-        pTemp = ALLOC( char, strlen(pStrGiven) + strlen(pStrAdd) + 2 );
+        pTemp = ABC_ALLOC( char, strlen(pStrGiven) + strlen(pStrAdd) + 2 );
         sprintf( pTemp, "%s%s", pStrGiven, pStrAdd );
-        free( pStrGiven );
+        ABC_FREE( pStrGiven );
     }
     else
         pTemp = Extra_UtilStrsav( pStrAdd );
diff --git a/src/misc/extra/extraUtilMemory.c b/src/misc/extra/extraUtilMemory.c
index e672afbb..626d58b5 100644
--- a/src/misc/extra/extraUtilMemory.c
+++ b/src/misc/extra/extraUtilMemory.c
@@ -35,7 +35,7 @@ struct Extra_MmFixed_t_
     int           nEntriesAlloc; // the total number of entries allocated
     int           nEntriesUsed;  // the number of entries in use
     int           nEntriesMax;   // the max number of entries in use
-    char *        pEntriesFree;  // the linked list of free entries
+    char *        pEntriesFree;  // the linked list of ABC_FREE entries
 
     // this is where the memory is stored
     int           nChunkSize;    // the size of one chunk
@@ -52,8 +52,8 @@ struct Extra_MmFlex_t_
 {
     // information about individual entries
     int           nEntriesUsed;  // the number of entries allocated
-    char *        pCurrent;      // the current pointer to free memory
-    char *        pEnd;          // the first entry outside the free memory
+    char *        pCurrent;      // the current pointer to ABC_FREE memory
+    char *        pEnd;          // the first entry outside the ABC_FREE memory
 
     // this is where the memory is stored
     int           nChunkSize;    // the size of one chunk
@@ -120,7 +120,7 @@ Extra_MmFixed_t * Extra_MmFixedStart( int nEntrySize )
 {
     Extra_MmFixed_t * p;
 
-    p = ALLOC( Extra_MmFixed_t, 1 );
+    p = ABC_ALLOC( Extra_MmFixed_t, 1 );
     memset( p, 0, sizeof(Extra_MmFixed_t) );
 
     p->nEntrySize    = nEntrySize;
@@ -137,7 +137,7 @@ Extra_MmFixed_t * Extra_MmFixedStart( int nEntrySize )
 
     p->nChunksAlloc  = 64;
     p->nChunks       = 0;
-    p->pChunks       = ALLOC( char *, p->nChunksAlloc );
+    p->pChunks       = ABC_ALLOC( char *, p->nChunksAlloc );
 
     p->nMemoryUsed   = 0;
     p->nMemoryAlloc  = 0;
@@ -180,9 +180,9 @@ void Extra_MmFixedStop( Extra_MmFixed_t * p )
     if ( p == NULL )
         return;
     for ( i = 0; i < p->nChunks; i++ )
-        free( p->pChunks[i] );
-    free( p->pChunks );
-    free( p );
+        ABC_FREE( p->pChunks[i] );
+    ABC_FREE( p->pChunks );
+    ABC_FREE( p );
 }
 
 /**Function*************************************************************
@@ -201,16 +201,16 @@ char * Extra_MmFixedEntryFetch( Extra_MmFixed_t * p )
     char * pTemp;
     int i;
 
-    // check if there are still free entries
+    // check if there are still ABC_FREE entries
     if ( p->nEntriesUsed == p->nEntriesAlloc )
     { // need to allocate more entries
         assert( p->pEntriesFree == NULL );
         if ( p->nChunks == p->nChunksAlloc )
         {
             p->nChunksAlloc *= 2;
-            p->pChunks = REALLOC( char *, p->pChunks, p->nChunksAlloc ); 
+            p->pChunks = ABC_REALLOC( char *, p->pChunks, p->nChunksAlloc ); 
         }
-        p->pEntriesFree = ALLOC( char, p->nEntrySize * p->nChunkSize );
+        p->pEntriesFree = ABC_ALLOC( char, p->nEntrySize * p->nChunkSize );
         p->nMemoryAlloc += p->nEntrySize * p->nChunkSize;
         // transform these entries into a linked list
         pTemp = p->pEntriesFree;
@@ -230,7 +230,7 @@ char * Extra_MmFixedEntryFetch( Extra_MmFixed_t * p )
     p->nEntriesUsed++;
     if ( p->nEntriesMax < p->nEntriesUsed )
         p->nEntriesMax = p->nEntriesUsed;
-    // return the first entry in the free entry list
+    // return the first entry in the ABC_FREE entry list
     pTemp = p->pEntriesFree;
     p->pEntriesFree = *((char **)pTemp);
     return pTemp;
@@ -251,7 +251,7 @@ void Extra_MmFixedEntryRecycle( Extra_MmFixed_t * p, char * pEntry )
 {
     // decrement the counter of used entries
     p->nEntriesUsed--;
-    // add the entry to the linked list of free entries
+    // add the entry to the linked list of ABC_FREE entries
     *((char **)pEntry) = p->pEntriesFree;
     p->pEntriesFree = pEntry;
 }
@@ -274,7 +274,7 @@ void Extra_MmFixedRestart( Extra_MmFixed_t * p )
 
     // deallocate all chunks except the first one
     for ( i = 1; i < p->nChunks; i++ )
-        free( p->pChunks[i] );
+        ABC_FREE( p->pChunks[i] );
     p->nChunks = 1;
     // transform these entries into a linked list
     pTemp = p->pChunks[0];
@@ -285,7 +285,7 @@ void Extra_MmFixedRestart( Extra_MmFixed_t * p )
     }
     // set the last link
     *((char **)pTemp) = NULL;
-    // set the free entry list
+    // set the ABC_FREE entry list
     p->pEntriesFree  = p->pChunks[0];
     // set the correct statistics
     p->nMemoryAlloc  = p->nEntrySize * p->nChunkSize;
@@ -342,7 +342,7 @@ Extra_MmFlex_t * Extra_MmFlexStart()
 { 
     Extra_MmFlex_t * p;
 //printf( "allocing flex\n" );
-    p = ALLOC( Extra_MmFlex_t, 1 );
+    p = ABC_ALLOC( Extra_MmFlex_t, 1 );
     memset( p, 0, sizeof(Extra_MmFlex_t) );
 
     p->nEntriesUsed  = 0;
@@ -352,7 +352,7 @@ Extra_MmFlex_t * Extra_MmFlexStart()
     p->nChunkSize    = (1 << 12);
     p->nChunksAlloc  = 64;
     p->nChunks       = 0;
-    p->pChunks       = ALLOC( char *, p->nChunksAlloc );
+    p->pChunks       = ABC_ALLOC( char *, p->nChunksAlloc );
 
     p->nMemoryUsed   = 0;
     p->nMemoryAlloc  = 0;
@@ -396,9 +396,9 @@ void Extra_MmFlexStop( Extra_MmFlex_t * p )
         return;
 //printf( "deleting flex\n" );
     for ( i = 0; i < p->nChunks; i++ )
-        free( p->pChunks[i] );
-    free( p->pChunks );
-    free( p );
+        ABC_FREE( p->pChunks[i] );
+    ABC_FREE( p->pChunks );
+    ABC_FREE( p );
 }
 
 /**Function*************************************************************
@@ -415,13 +415,13 @@ void Extra_MmFlexStop( Extra_MmFlex_t * p )
 char * Extra_MmFlexEntryFetch( Extra_MmFlex_t * p, int nBytes )
 {
     char * pTemp;
-    // check if there are still free entries
+    // check if there are still ABC_FREE entries
     if ( p->pCurrent == NULL || p->pCurrent + nBytes > p->pEnd )
     { // need to allocate more entries
         if ( p->nChunks == p->nChunksAlloc )
         {
             p->nChunksAlloc *= 2;
-            p->pChunks = REALLOC( char *, p->pChunks, p->nChunksAlloc ); 
+            p->pChunks = ABC_REALLOC( char *, p->pChunks, p->nChunksAlloc ); 
         }
         if ( nBytes > p->nChunkSize )
         {
@@ -429,7 +429,7 @@ char * Extra_MmFlexEntryFetch( Extra_MmFlex_t * p, int nBytes )
             // (ideally, this should never happen)
             p->nChunkSize = 2 * nBytes;
         }
-        p->pCurrent = ALLOC( char, p->nChunkSize );
+        p->pCurrent = ABC_ALLOC( char, p->nChunkSize );
         p->pEnd     = p->pCurrent + p->nChunkSize;
         p->nMemoryAlloc += p->nChunkSize;
         // add the chunk to the chunk storage
@@ -479,7 +479,7 @@ int Extra_MmFlexReadMemUsage( Extra_MmFlex_t * p )
   are employed internally. Calling this procedure with nSteps equal
   to 10 results in 10 hierarchically arranged internal memory managers, 
   which can allocate up to 4096 (1Kb) entries. Requests for larger 
-  entries are handed over to malloc() and then free()ed.]
+  entries are handed over to malloc() and then ABC_FREE()ed.]
                
   SideEffects []
 
@@ -490,16 +490,16 @@ Extra_MmStep_t * Extra_MmStepStart( int nSteps )
 {
     Extra_MmStep_t * p;
     int i, k;
-    p = ALLOC( Extra_MmStep_t, 1 );
+    p = ABC_ALLOC( Extra_MmStep_t, 1 );
     memset( p, 0, sizeof(Extra_MmStep_t) );
     p->nMems = nSteps;
     // start the fixed memory managers
-    p->pMems = ALLOC( Extra_MmFixed_t *, p->nMems );
+    p->pMems = ABC_ALLOC( Extra_MmFixed_t *, p->nMems );
     for ( i = 0; i < p->nMems; i++ )
         p->pMems[i] = Extra_MmFixedStart( (8<<i) );
     // set up the mapping of the required memory size into the corresponding manager
     p->nMapSize = (4<<p->nMems);
-    p->pMap = ALLOC( Extra_MmFixed_t *, p->nMapSize+1 );
+    p->pMap = ABC_ALLOC( Extra_MmFixed_t *, p->nMapSize+1 );
     p->pMap[0] = NULL;
     for ( k = 1; k <= 4; k++ )
         p->pMap[k] = p->pMems[0];
@@ -530,12 +530,12 @@ void Extra_MmStepStop( Extra_MmStep_t * p )
     if ( p->pLargeChunks ) 
     {
       for ( i = 0; i < p->nLargeChunks; i++ )
-          free( p->pLargeChunks[i] );
-      free( p->pLargeChunks );
+          ABC_FREE( p->pLargeChunks[i] );
+      ABC_FREE( p->pLargeChunks );
     }
-    free( p->pMems );
-    free( p->pMap );
-    free( p );
+    ABC_FREE( p->pMems );
+    ABC_FREE( p->pMap );
+    ABC_FREE( p );
 }
 
 /**Function*************************************************************
@@ -556,15 +556,15 @@ char * Extra_MmStepEntryFetch( Extra_MmStep_t * p, int nBytes )
     if ( nBytes > p->nMapSize )
     {
 //        printf( "Allocating %d bytes.\n", nBytes );
-//        return ALLOC( char, nBytes );
+//        return ABC_ALLOC( char, nBytes );
         if ( p->nLargeChunks == p->nLargeChunksAlloc )
         {
             if ( p->nLargeChunksAlloc == 0 )
                 p->nLargeChunksAlloc = 32;
             p->nLargeChunksAlloc *= 2;
-            p->pLargeChunks = REALLOC( void *, p->pLargeChunks, p->nLargeChunksAlloc );
+            p->pLargeChunks = ABC_REALLOC( void *, p->pLargeChunks, p->nLargeChunksAlloc );
         }
-        p->pLargeChunks[ p->nLargeChunks++ ] = ALLOC( char, nBytes );
+        p->pLargeChunks[ p->nLargeChunks++ ] = ABC_ALLOC( char, nBytes );
         return p->pLargeChunks[ p->nLargeChunks - 1 ];
     }
     return Extra_MmFixedEntryFetch( p->pMap[nBytes] );
@@ -588,7 +588,7 @@ void Extra_MmStepEntryRecycle( Extra_MmStep_t * p, char * pEntry, int nBytes )
         return;
     if ( nBytes > p->nMapSize )
     {
-//        free( pEntry );
+//        ABC_FREE( pEntry );
         return;
     }
     Extra_MmFixedEntryRecycle( p->pMap[nBytes], pEntry );
diff --git a/src/misc/extra/extraUtilMisc.c b/src/misc/extra/extraUtilMisc.c
index 48fca0ba..293b23e7 100644
--- a/src/misc/extra/extraUtilMisc.c
+++ b/src/misc/extra/extraUtilMisc.c
@@ -265,8 +265,8 @@ int Extra_Factorial( int n )
 
   Description [The number of permutations in the array is n!. The number of
   entries in each permutation is n. Therefore, the resulting array is a 
-  two-dimentional array of the size: n! x n. To free the resulting array,
-  call free() on the pointer returned by this procedure.]
+  two-dimentional array of the size: n! x n. To ABC_FREE the resulting array,
+  call ABC_FREE() on the pointer returned by this procedure.]
 
   SideEffects []
 
@@ -397,8 +397,8 @@ unsigned Extra_TruthPermute( unsigned Truth, char * pPerms, int nVars, int fReve
 
     assert( nVars < 6 );
     nMints  = (1 << nVars);
-    pMints  = ALLOC( int, nMints );
-    pMintsP = ALLOC( int, nMints );
+    pMints  = ABC_ALLOC( int, nMints );
+    pMintsP = ABC_ALLOC( int, nMints );
     for ( i = 0; i < nMints; i++ )
         pMints[i] = i;
 
@@ -418,8 +418,8 @@ unsigned Extra_TruthPermute( unsigned Truth, char * pPerms, int nVars, int fReve
                 Result |= (1 << pMintsP[m]);
     }
 
-    free( pMints );
-    free( pMintsP );
+    ABC_FREE( pMints );
+    ABC_FREE( pMintsP );
 
     return Result;
 }
@@ -546,7 +546,7 @@ unsigned Extra_TruthCanonP( unsigned uTruth, int nVars )
     }
     else if ( nVarsOld != nVars )
     {
-        free( pPerms );
+        ABC_FREE( pPerms );
         nPerms = Extra_Factorial( nVars );   
         pPerms = Extra_Permutations( nVars );
         nVarsOld = nVars;
@@ -589,7 +589,7 @@ unsigned Extra_TruthCanonNP( unsigned uTruth, int nVars )
     }
     else if ( nVarsOld != nVars )
     {
-        free( pPerms );
+        ABC_FREE( pPerms );
         nPerms = Extra_Factorial( nVars );   
         pPerms = Extra_Permutations( nVars );
         nVarsOld = nVars;
@@ -637,7 +637,7 @@ unsigned Extra_TruthCanonNPN( unsigned uTruth, int nVars )
     }
     else if ( nVarsOld != nVars )
     {
-        free( pPerms );
+        ABC_FREE( pPerms );
         nPerms = Extra_Factorial( nVars );   
         pPerms = Extra_Permutations( nVars );
         nVarsOld = nVars;
@@ -687,10 +687,10 @@ void Extra_Truth4VarNPN( unsigned short ** puCanons, char ** puPhases, char ** p
     int i, k;
 
     nFuncs  = (1 << 16);
-    uCanons = ALLOC( unsigned short, nFuncs );
-    uPhases = ALLOC( char, nFuncs );
-    uPerms  = ALLOC( char, nFuncs );
-    uMap    = ALLOC( unsigned char, nFuncs );
+    uCanons = ABC_ALLOC( unsigned short, nFuncs );
+    uPhases = ABC_ALLOC( char, nFuncs );
+    uPerms  = ABC_ALLOC( char, nFuncs );
+    uMap    = ABC_ALLOC( unsigned char, nFuncs );
     memset( uCanons, 0, sizeof(unsigned short) * nFuncs );
     memset( uPhases, 0, sizeof(char) * nFuncs );
     memset( uPerms,  0, sizeof(char) * nFuncs );
@@ -751,23 +751,23 @@ void Extra_Truth4VarNPN( unsigned short ** puCanons, char ** puPhases, char ** p
     }
     uPhases[(1<<16)-1] = 16;
     assert( nClasses == 222 );
-    free( pPerms4 );
+    ABC_FREE( pPerms4 );
     if ( puCanons ) 
         *puCanons = uCanons;
     else
-        free( uCanons );
+        ABC_FREE( uCanons );
     if ( puPhases ) 
         *puPhases = uPhases;
     else
-        free( uPhases );
+        ABC_FREE( uPhases );
     if ( puPerms ) 
         *puPerms = uPerms;
     else
-        free( uPerms );
+        ABC_FREE( uPerms );
     if ( puMap ) 
         *puMap = uMap;
     else
-        free( uMap );
+        ABC_FREE( uMap );
 }
 
 /**Function*************************************************************
@@ -790,9 +790,9 @@ void Extra_Truth3VarN( unsigned ** puCanons, char *** puPhases, char ** ppCounte
     int nFuncs, nClasses, i;
 
     nFuncs  = (1 << 8);
-    uCanons = ALLOC( unsigned, nFuncs );
+    uCanons = ABC_ALLOC( unsigned, nFuncs );
     memset( uCanons, 0, sizeof(unsigned) * nFuncs );
-    pCounters = ALLOC( char, nFuncs );
+    pCounters = ABC_ALLOC( char, nFuncs );
     memset( pCounters, 0, sizeof(char) * nFuncs );
     uPhases = (char **)Extra_ArrayAlloc( nFuncs, nPhasesMax, sizeof(char) );
     nClasses = 0;
@@ -826,15 +826,15 @@ void Extra_Truth3VarN( unsigned ** puCanons, char *** puPhases, char ** ppCounte
     if ( puCanons ) 
         *puCanons = uCanons;
     else
-        free( uCanons );
+        ABC_FREE( uCanons );
     if ( puPhases ) 
         *puPhases = uPhases;
     else
-        free( uPhases );
+        ABC_FREE( uPhases );
     if ( ppCounters ) 
         *ppCounters = pCounters;
     else
-        free( pCounters );
+        ABC_FREE( pCounters );
 //    printf( "The number of 3N-classes = %d.\n", nClasses );
 }
 
@@ -857,9 +857,9 @@ void Extra_Truth4VarN( unsigned short ** puCanons, char *** puPhases, char ** pp
     int nFuncs, nClasses, i;
 
     nFuncs  = (1 << 16);
-    uCanons = ALLOC( unsigned short, nFuncs );
+    uCanons = ABC_ALLOC( unsigned short, nFuncs );
     memset( uCanons, 0, sizeof(unsigned short) * nFuncs );
-    pCounters = ALLOC( char, nFuncs );
+    pCounters = ABC_ALLOC( char, nFuncs );
     memset( pCounters, 0, sizeof(char) * nFuncs );
     uPhases = (char **)Extra_ArrayAlloc( nFuncs, nPhasesMax, sizeof(char) );
     nClasses = 0;
@@ -892,15 +892,15 @@ void Extra_Truth4VarN( unsigned short ** puCanons, char *** puPhases, char ** pp
     if ( puCanons ) 
         *puCanons = uCanons;
     else
-        free( uCanons );
+        ABC_FREE( uCanons );
     if ( puPhases ) 
         *puPhases = uPhases;
     else
-        free( uPhases );
+        ABC_FREE( uPhases );
     if ( ppCounters ) 
         *ppCounters = pCounters;
     else
-        free( pCounters );
+        ABC_FREE( pCounters );
 //    printf( "The number of 4N-classes = %d.\n", nClasses );
 }
 
@@ -921,7 +921,7 @@ void ** Extra_ArrayAlloc( int nCols, int nRows, int Size )
     char * pBuffer;
     int i;
     assert( nCols > 0 && nRows > 0 && Size > 0 );
-    pBuffer = ALLOC( char, nCols * (sizeof(void *) + nRows * Size) );
+    pBuffer = ABC_ALLOC( char, nCols * (sizeof(void *) + nRows * Size) );
     pRes = (void **)pBuffer;
     pRes[0] = pBuffer + nCols * sizeof(void *);
     for ( i = 1; i < nCols; i++ )
diff --git a/src/misc/extra/extraUtilProgress.c b/src/misc/extra/extraUtilProgress.c
index 6b6d5132..5e3b0f06 100644
--- a/src/misc/extra/extraUtilProgress.c
+++ b/src/misc/extra/extraUtilProgress.c
@@ -62,7 +62,7 @@ ProgressBar * Extra_ProgressBarStart( FILE * pFile, int nItemsTotal )
     extern void * Abc_FrameGetGlobalFrame();
 
     if ( !Abc_FrameShowProgress(Abc_FrameGetGlobalFrame()) ) return NULL;
-    p = ALLOC( ProgressBar, 1 );
+    p = ABC_ALLOC( ProgressBar, 1 );
     memset( p, 0, sizeof(ProgressBar) );
     p->pFile       = pFile;
     p->nItemsTotal = nItemsTotal;
@@ -118,7 +118,7 @@ void Extra_ProgressBarStop( ProgressBar * p )
 {
     if ( p == NULL ) return;
     Extra_ProgressBarClean( p );
-    FREE( p );
+    ABC_FREE( p );
 }
 
 /**Function*************************************************************
diff --git a/src/misc/extra/extraUtilReader.c b/src/misc/extra/extraUtilReader.c
index b6a53fbc..46179e50 100644
--- a/src/misc/extra/extraUtilReader.c
+++ b/src/misc/extra/extraUtilReader.c
@@ -96,7 +96,7 @@ Extra_FileReader_t * Extra_FileReaderAlloc( char * pFileName,
         return NULL;
     }
     // start the file reader    
-    p = ALLOC( Extra_FileReader_t, 1 );
+    p = ABC_ALLOC( Extra_FileReader_t, 1 );
     memset( p, 0, sizeof(Extra_FileReader_t) );
     p->pFileName   = pFileName;
     p->pFile       = pFile;
@@ -113,7 +113,7 @@ Extra_FileReader_t * Extra_FileReaderAlloc( char * pFileName,
     p->nFileSize = ftell( pFile );  
     rewind( pFile ); 
     // allocate the buffer
-    p->pBuffer = ALLOC( char, EXTRA_BUFFER_SIZE+1 );
+    p->pBuffer = ABC_ALLOC( char, EXTRA_BUFFER_SIZE+1 );
     p->nBufferSize = EXTRA_BUFFER_SIZE;
     p->pBufferCur  = p->pBuffer;
     // determine how many chars to read
@@ -146,10 +146,10 @@ void Extra_FileReaderFree( Extra_FileReader_t * p )
 {
     if ( p->pFile )
         fclose( p->pFile );
-    FREE( p->pBuffer );
+    ABC_FREE( p->pBuffer );
     Vec_PtrFree( p->vTokens );
     Vec_IntFree( p->vLines );
-    free( p );
+    ABC_FREE( p );
 }
 
 /**Function*************************************************************
diff --git a/src/misc/extra/extraUtilUtil.c b/src/misc/extra/extraUtilUtil.c
index 7165a0cd..3f0dd365 100644
--- a/src/misc/extra/extraUtilUtil.c
+++ b/src/misc/extra/extraUtilUtil.c
@@ -169,7 +169,7 @@ char * Extra_UtilStrsav( char *s )
        return s;
     }
     else {
-       return strcpy(ALLOC(char, strlen(s)+1), s);
+       return strcpy(ABC_ALLOC(char, strlen(s)+1), s);
     }
 }
 
@@ -199,7 +199,7 @@ char * Extra_UtilTildeExpand( char *fname )
 
     home     = getenv("HOME");
     length   = n_tildes * strlen(home) + strlen(fname);
-    expanded = ALLOC(char, length + 1);
+    expanded = ABC_ALLOC(char, length + 1);
 
     j = 0;
     for (i = 0; i < (int)strlen(fname); i++){
@@ -279,22 +279,22 @@ char * Extra_UtilFileSearch(char *file, char *path, char *mode)
     if (strcmp(path, ".") == 0) {
         buffer = Extra_UtilStrsav(file);
     } else {
-        buffer = ALLOC(char, strlen(path) + strlen(file) + 4);
+        buffer = ABC_ALLOC(char, strlen(path) + strlen(file) + 4);
         (void) sprintf(buffer, "%s/%s", path, file);
     }
     filename = Extra_UtilTildeExpand(buffer);
-    FREE(buffer);
+    ABC_FREE(buffer);
 
     /* see if we can access it */
     if (Extra_UtilCheckFile(filename, mode)) {
-        FREE(save_path);
+        ABC_FREE(save_path);
         return filename;
     }
-    FREE(filename);
+    ABC_FREE(filename);
     path = ++cp;
     } while (! quit); 
 
-    FREE(save_path);
+    ABC_FREE(save_path);
     return 0;
 }
 
@@ -390,7 +390,7 @@ double Extra_CpuTimeDouble()
 ***********************************************************************/
 void Extra_MemTest()
 {
-    malloc( 1002 );
+    ABC_ALLOC( char, 1002 );
 }
 
 ////////////////////////////////////////////////////////////////////////