Version abc90215

64 files changed, 1073 insertions, 1076 deletions

diff --git a/src/bdd/cas/cas.h b/src/bdd/cas/cas.h
index fcc9f890..68a5c3a0 100644
--- a/src/bdd/cas/cas.h
+++ b/src/bdd/cas/cas.h
@@ -21,10 +21,6 @@
 #ifndef __CAS_H__
 #define __CAS_H__
 
-#ifdef __cplusplus
-extern "C" {
-#endif
-
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -33,6 +29,10 @@ extern "C" {
 ///                         PARAMETERS                               ///
 ////////////////////////////////////////////////////////////////////////
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 #define MAXINPUTS   1024
 #define MAXOUTPUTS  1024
 
diff --git a/src/bdd/cas/casCore.c b/src/bdd/cas/casCore.c
index a27e994f..4010235c 100644
--- a/src/bdd/cas/casCore.c
+++ b/src/bdd/cas/casCore.c
@@ -265,7 +265,7 @@ int Abc_CascadeExperiment( char * pFileGeneric, DdManager * dd, DdNode ** pOutpu
 
     // release the names
     for ( i = 0; i < nNames; i++ )
-        free( pNames[i] );
+        ABC_FREE( pNames[i] );
 
 
 //fprintf( pTable, "\n" );
@@ -437,7 +437,7 @@ void Experiment2( BFunc * pFunc )
 
     // release the names
     for ( i = 0; i < nNames; i++ )
-        free( pNames[i] );
+        ABC_FREE( pNames[i] );
 
 
     
diff --git a/src/bdd/cas/casDec.c b/src/bdd/cas/casDec.c
index 3435f30d..25309d32 100644
--- a/src/bdd/cas/casDec.c
+++ b/src/bdd/cas/casDec.c
@@ -151,7 +151,7 @@ int CreateDecomposedNetwork( DdManager * dd, DdNode * aFunc, char ** pNames, int
     nLuts     = 0;
     do
     {
-        p = (LUT*) malloc( sizeof(LUT) );
+        p = (LUT*) ABC_ALLOC( char, sizeof(LUT) );
         memset( p, 0, sizeof(LUT) );
 
         if ( nVarsRem + PrevMulti <= s_LutSize ) // this is the last LUT
@@ -194,9 +194,9 @@ int CreateDecomposedNetwork( DdManager * dd, DdNode * aFunc, char ** pNames, int
 
 
         // there should be as many columns, codes, and nodes, as there are columns on this level
-        p->pbCols  = (DdNode **) malloc( p->nCols * sizeof(DdNode *) );
-        p->pbCodes = (DdNode **) malloc( p->nCols * sizeof(DdNode *) );
-        p->paNodes = (DdNode **) malloc( p->nCols * sizeof(DdNode *) );
+        p->pbCols  = (DdNode **) ABC_ALLOC( char, p->nCols * sizeof(DdNode *) );
+        p->pbCodes = (DdNode **) ABC_ALLOC( char, p->nCols * sizeof(DdNode *) );
+        p->paNodes = (DdNode **) ABC_ALLOC( char, p->nCols * sizeof(DdNode *) );
 
         pLuts[nLuts] = p;
         nLuts++;
@@ -316,7 +316,7 @@ printf( "Stage %3d: In = %3d  InP = %3d  Cols = %5d  Multi = %2d  Simple = %2d
             DdNode ** pbTemp;
             int k, v;
 
-            pbTemp = (DdNode **) malloc( p->nCols * sizeof(DdNode *) );
+            pbTemp = (DdNode **) ABC_ALLOC( char, p->nCols * sizeof(DdNode *) );
 
             // create the identical permutation
             for ( v = 0; v < dd->size; v++ )
@@ -336,7 +336,7 @@ printf( "Stage %3d: In = %3d  InP = %3d  Cols = %5d  Multi = %2d  Simple = %2d
                 Cudd_RecursiveDeref( dd, p->pbCodes[k] );
                 p->pbCodes[k] = pbTemp[k];
             }
-            free( pbTemp );
+            ABC_FREE( pbTemp );
         }
     } 
     if ( fVerbose )
@@ -402,10 +402,10 @@ printf( "Stage %3d: In = %3d  InP = %3d  Cols = %5d  Multi = %2d  Simple = %2d
         }
         Cudd_RecursiveDeref( dd, p->bRelation );
 
-        free( p->pbCols );
-        free( p->pbCodes );
-        free( p->paNodes );
-        free( p );
+        ABC_FREE( p->pbCols );
+        ABC_FREE( p->pbCodes );
+        ABC_FREE( p->paNodes );
+        ABC_FREE( p );
     }
 
     return 1;
@@ -490,11 +490,11 @@ void WriteLUTSintoBLIFfile( FILE * pFile, DdManager * dd, LUT ** pLuts, int nLut
         for ( v = 0; v < dd->size; v++ )
         {
             if ( pNamesLocalIn[v] )
-                free( pNamesLocalIn[v] );
+                ABC_FREE( pNamesLocalIn[v] );
             pNamesLocalIn[v] = NULL;
         }
         for ( v = 0; v < p->nMulti; v++ )
-            free( pNamesLocalOut[v] );
+            ABC_FREE( pNamesLocalOut[v] );
     }
 }
 
diff --git a/src/bdd/cudd/cuddAPI.c b/src/bdd/cudd/cuddAPI.c
index a16b82cf..cbba4d95 100644
--- a/src/bdd/cudd/cuddAPI.c
+++ b/src/bdd/cudd/cuddAPI.c
@@ -514,7 +514,7 @@ Cudd_zddVarsFromBddVars(
         dd->univ[i]->index = dd->invpermZ[i];
     }
     } else {
-    permutation = ALLOC(int,dd->sizeZ);
+    permutation = ABC_ALLOC(int,dd->sizeZ);
     if (permutation == NULL) {
         dd->errorCode = CUDD_MEMORY_OUT;
         return(0);
@@ -529,7 +529,7 @@ Cudd_zddVarsFromBddVars(
         permutation[i] = i;
     }
     res = Cudd_zddShuffleHeap(dd, permutation);
-    FREE(permutation);
+    ABC_FREE(permutation);
     if (res == 0) return(0);
     }
     /* Copy and expand the variable group tree if it exists. */
@@ -549,12 +549,12 @@ Cudd_zddVarsFromBddVars(
     if (multiplicity > 1) {
     char *vmask, *lmask;
 
-    vmask = ALLOC(char, dd->size);
+    vmask = ABC_ALLOC(char, dd->size);
     if (vmask == NULL) {
         dd->errorCode = CUDD_MEMORY_OUT;
         return(0);
     }
-    lmask =  ALLOC(char, dd->size);
+    lmask =  ABC_ALLOC(char, dd->size);
     if (lmask == NULL) {
         dd->errorCode = CUDD_MEMORY_OUT;
         return(0);
@@ -563,8 +563,8 @@ Cudd_zddVarsFromBddVars(
         vmask[i] = lmask[i] = 0;
     }
     res = addMultiplicityGroups(dd,dd->treeZ,multiplicity,vmask,lmask);
-    FREE(vmask);
-    FREE(lmask);
+    ABC_FREE(vmask);
+    ABC_FREE(lmask);
     if (res == 0) return(0);
     }
     return(1);
@@ -653,7 +653,7 @@ Cudd_AutodynEnable(
     if ((unsigned) unique->nextDead > unique->deadMask) {
     unique->nextDead = 0;
     }
-    unique->deathRow = REALLOC(DdNodePtr, unique->deathRow,
+    unique->deathRow = ABC_REALLOC(DdNodePtr, unique->deathRow,
     unique->deathRowDepth);
 #endif
     return;
@@ -1740,7 +1740,7 @@ Cudd_ReadGarbageCollectionTime(
 
   Synopsis    [Returns the number of nodes freed.]
 
-  Description [Returns the number of nodes returned to the free list if the
+  Description [Returns the number of nodes returned to the ABC_FREE list if the
   keeping of this statistic is enabled; -1 otherwise. This statistic is
   enabled only if the package is compiled with DD_STATS defined.]
 
@@ -3078,7 +3078,7 @@ Cudd_PrintInfo(
   Synopsis    [Reports the peak number of nodes.]
 
   Description [Reports the peak number of nodes. This number includes
-  node on the free list. At the peak, the number of nodes on the free
+  node on the ABC_FREE list. At the peak, the number of nodes on the ABC_FREE
   list is guaranteed to be less than DD_MEM_CHUNK.]
 
   SideEffects [None]
@@ -3244,7 +3244,7 @@ Cudd_AddHook(
     }
     /* The function was not in the list. Create a new item and append it
     ** to the end of the list. */
-    newHook = ALLOC(DdHook,1);
+    newHook = ABC_ALLOC(DdHook,1);
     if (newHook == NULL) {
     dd->errorCode = CUDD_MEMORY_OUT;
     return(0);
@@ -3298,7 +3298,7 @@ Cudd_RemoveHook(
     while (nextHook != NULL) {
     if (nextHook->f == f) {
         *hook = nextHook->next;
-        FREE(nextHook);
+        ABC_FREE(nextHook);
         return(1);
     }
     hook = &(nextHook->next);
diff --git a/src/bdd/cudd/cuddAddWalsh.c b/src/bdd/cudd/cuddAddWalsh.c
index 90a57b3c..3022b73d 100644
--- a/src/bdd/cudd/cuddAddWalsh.c
+++ b/src/bdd/cudd/cuddAddWalsh.c
@@ -146,14 +146,14 @@ Cudd_addResidue(
     tc = options & CUDD_RESIDUE_TC;
 
     /* Allocate and initialize working arrays. */
-    array[0] = ALLOC(DdNode *,m);
+    array[0] = ABC_ALLOC(DdNode *,m);
     if (array[0] == NULL) {
     dd->errorCode = CUDD_MEMORY_OUT;
     return(NULL);
     }
-    array[1] = ALLOC(DdNode *,m);
+    array[1] = ABC_ALLOC(DdNode *,m);
     if (array[1] == NULL) {
-    FREE(array[0]);
+    ABC_FREE(array[0]);
     dd->errorCode = CUDD_MEMORY_OUT;
     return(NULL);
     }
@@ -168,8 +168,8 @@ Cudd_addResidue(
         for (j = 0; j < i; j++) {
         Cudd_RecursiveDeref(dd,array[1][j]);
         }
-        FREE(array[0]);
-        FREE(array[1]);
+        ABC_FREE(array[0]);
+        ABC_FREE(array[1]);
         return(NULL);
     }
     cuddRef(tmp);
@@ -193,8 +193,8 @@ Cudd_addResidue(
         for (j = 0; j < m; j++) {
         Cudd_RecursiveDeref(dd,array[previous][j]);
         }
-        FREE(array[0]);
-        FREE(array[1]);
+        ABC_FREE(array[0]);
+        ABC_FREE(array[1]);
         return(NULL);
     }
     cuddRef(var);
@@ -208,8 +208,8 @@ Cudd_addResidue(
         for (j = 0; j < m; j++) {
             Cudd_RecursiveDeref(dd,array[previous][j]);
         }
-        FREE(array[0]);
-        FREE(array[1]);
+        ABC_FREE(array[0]);
+        ABC_FREE(array[1]);
         return(NULL);
         }
         cuddRef(tmp);
@@ -234,8 +234,8 @@ Cudd_addResidue(
     }
     res = array[(n - 1) & 1][0];
 
-    FREE(array[0]);
-    FREE(array[1]);
+    ABC_FREE(array[0]);
+    ABC_FREE(array[1]);
 
     cuddDeref(res);
     return(res);
diff --git a/src/bdd/cudd/cuddAnneal.c b/src/bdd/cudd/cuddAnneal.c
index 3d8b56b9..32155603 100644
--- a/src/bdd/cudd/cuddAnneal.c
+++ b/src/bdd/cudd/cuddAnneal.c
@@ -153,7 +153,7 @@ cuddAnnealing(
 
     /* Keep track of the best order. */
     BestCost = size;
-    BestOrder = ALLOC(int,nvars);
+    BestOrder = ABC_ALLOC(int,nvars);
     if (BestOrder == NULL) {
     table->errorCode = CUDD_MEMORY_OUT;
     return(0);
@@ -218,7 +218,7 @@ cuddAnnealing(
         }
 
         if (!result) {
-        FREE(BestOrder);
+        ABC_FREE(BestOrder);
         return(0);
         }
 
@@ -245,7 +245,7 @@ cuddAnnealing(
     }
 
     result = restoreOrder(table,BestOrder,lower,upper);
-    FREE(BestOrder);
+    ABC_FREE(BestOrder);
     if (!result) return(0);
 #ifdef DD_STATS
     fprintf(table->out,"#:N_EXCHANGE %8d : total exchanges\n",ecount);
diff --git a/src/bdd/cudd/cuddApa.c b/src/bdd/cudd/cuddApa.c
index 47ab51e8..13e80ce2 100644
--- a/src/bdd/cudd/cuddApa.c
+++ b/src/bdd/cudd/cuddApa.c
@@ -121,7 +121,7 @@ DdApaNumber
 Cudd_NewApaNumber(
   int  digits)
 {
-    return(ALLOC(DdApaDigit, digits));
+    return(ABC_ALLOC(DdApaDigit, digits));
 
 } /* end of Cudd_NewApaNumber */
 
@@ -519,9 +519,9 @@ Cudd_ApaPrintDecimal(
     work = Cudd_NewApaNumber(digits);
     if (work == NULL)
     return(0);
-    decimal = ALLOC(unsigned char, decimalDigits);
+    decimal = ABC_ALLOC(unsigned char, decimalDigits);
     if (decimal == NULL) {
-    FREE(work);
+    ABC_FREE(work);
     return(0);
     }
     Cudd_ApaCopy(digits,number,work);
@@ -529,7 +529,7 @@ Cudd_ApaPrintDecimal(
     remainder = Cudd_ApaShortDivision(digits,work,(DdApaDigit) 10,work);
     decimal[i] = remainder;
     }
-    FREE(work);
+    ABC_FREE(work);
 
     leadingzero = 1;
     for (i = 0; i < decimalDigits; i++) {
@@ -537,12 +537,12 @@ Cudd_ApaPrintDecimal(
     if ((!leadingzero) || (i == (decimalDigits - 1))) {
         result = fprintf(fp,"%1d",decimal[i]);
         if (result == EOF) {
-        FREE(decimal);
+        ABC_FREE(decimal);
         return(0);
         }
     }
     }
-    FREE(decimal);
+    ABC_FREE(decimal);
     return(1);
 
 } /* end of Cudd_ApaPrintDecimal */
@@ -576,9 +576,9 @@ Cudd_ApaPrintExponential(
     work = Cudd_NewApaNumber(digits);
     if (work == NULL)
     return(0);
-    decimal = ALLOC(unsigned char, decimalDigits);
+    decimal = ABC_ALLOC(unsigned char, decimalDigits);
     if (decimal == NULL) {
-    FREE(work);
+    ABC_FREE(work);
     return(0);
     }
     Cudd_ApaCopy(digits,number,work);
@@ -588,17 +588,17 @@ Cudd_ApaPrintExponential(
     decimal[i] = remainder;
     if (remainder != 0) first = i; /* keep track of MS non-zero */
     }
-    FREE(work);
+    ABC_FREE(work);
     last = ddMin(first + precision, decimalDigits);
 
     for (i = first; i < last; i++) {
     result = fprintf(fp,"%s%1d",i == first+1 ? "." : "", decimal[i]);
     if (result == EOF) {
-        FREE(decimal);
+        ABC_FREE(decimal);
         return(0);
     }
     }
-    FREE(decimal);
+    ABC_FREE(decimal);
     result = fprintf(fp,"e+%d",decimalDigits - first - 1);
     if (result == EOF) {
     return(0);
@@ -647,31 +647,31 @@ Cudd_ApaCountMinterm(
     Cudd_ApaPowerOfTwo(*digits,max,nvars);
     min = Cudd_NewApaNumber(*digits);
     if (min == NULL) {
-    FREE(max);
+    ABC_FREE(max);
     return(NULL);
     }
     Cudd_ApaSetToLiteral(*digits,min,0);
     table = st_init_table(st_ptrcmp,st_ptrhash);
     if (table == NULL) {
-    FREE(max);
-    FREE(min);
+    ABC_FREE(max);
+    ABC_FREE(min);
     return(NULL);
     }
     i = cuddApaCountMintermAux(Cudd_Regular(node),*digits,max,min,table);
     if (i == NULL) {
-    FREE(max);
-    FREE(min);
+    ABC_FREE(max);
+    ABC_FREE(min);
     st_foreach(table, cuddApaStCountfree, NULL);
     st_free_table(table);
     return(NULL);
     }
     count = Cudd_NewApaNumber(*digits);
     if (count == NULL) {
-    FREE(max);
-    FREE(min);
+    ABC_FREE(max);
+    ABC_FREE(min);
     st_foreach(table, cuddApaStCountfree, NULL);
     st_free_table(table);
-    if (Cudd_Regular(node)->ref == 1) FREE(i);
+    if (Cudd_Regular(node)->ref == 1) ABC_FREE(i);
     return(NULL);
     }
     if (Cudd_IsComplement(node)) {
@@ -679,11 +679,11 @@ Cudd_ApaCountMinterm(
     } else {
     Cudd_ApaCopy(*digits,i,count);
     }
-    FREE(max);
-    FREE(min);
+    ABC_FREE(max);
+    ABC_FREE(min);
     st_foreach(table, cuddApaStCountfree, NULL);
     st_free_table(table);
-    if (Cudd_Regular(node)->ref == 1) FREE(i);
+    if (Cudd_Regular(node)->ref == 1) ABC_FREE(i);
     return(count);
 
 } /* end of Cudd_ApaCountMinterm */
@@ -717,7 +717,7 @@ Cudd_ApaPrintMinterm(
     if (count == NULL)
     return(0);
     result = Cudd_ApaPrintDecimal(fp,digits,count);
-    FREE(count);
+    ABC_FREE(count);
     if (fprintf(fp,"\n") == EOF) {
     return(0);
     }
@@ -757,7 +757,7 @@ Cudd_ApaPrintMintermExp(
     if (count == NULL)
     return(0);
     result = Cudd_ApaPrintExponential(fp,digits,count,precision);
-    FREE(count);
+    ABC_FREE(count);
     if (fprintf(fp,"\n") == EOF) {
     return(0);
     }
@@ -798,8 +798,8 @@ Cudd_ApaPrintDensity(
     density = Cudd_NewApaNumber(digits);
     remainder = Cudd_ApaIntDivision(digits,count,size,density);
     result = Cudd_ApaPrintDecimal(fp,digits,density);
-    FREE(count);
-    FREE(density);
+    ABC_FREE(count);
+    ABC_FREE(density);
     fractional = (unsigned int)((double)remainder / size * 1000000);
     if (fprintf(fp,".%u\n", fractional) == EOF) {
     return(0);
@@ -869,13 +869,13 @@ cuddApaCountMintermAux(
     if (mint1 == NULL) return(NULL);
     mint2 = cuddApaCountMintermAux(Cudd_Regular(Ne), digits, max, min, table);
     if (mint2 == NULL) {
-    if (Nt->ref == 1) FREE(mint1);
+    if (Nt->ref == 1) ABC_FREE(mint1);
     return(NULL);
     }
     mint = Cudd_NewApaNumber(digits);
     if (mint == NULL) {
-    if (Nt->ref == 1) FREE(mint1);
-    if (Cudd_Regular(Ne)->ref == 1) FREE(mint2);
+    if (Nt->ref == 1) ABC_FREE(mint1);
+    if (Cudd_Regular(Ne)->ref == 1) ABC_FREE(mint2);
     return(NULL);
     }
     if (Cudd_IsComplement(Ne)) {
@@ -888,12 +888,12 @@ cuddApaCountMintermAux(
     /* If the refernce count of a child is 1, its minterm count
     ** hasn't been stored in table.  Therefore, it must be explicitly
     ** freed here. */
-    if (Nt->ref == 1) FREE(mint1);
-    if (Cudd_Regular(Ne)->ref == 1) FREE(mint2);
+    if (Nt->ref == 1) ABC_FREE(mint1);
+    if (Cudd_Regular(Ne)->ref == 1) ABC_FREE(mint2);
     
     if (node->ref > 1) {
     if (st_insert(table, (char *)node, (char *)mint) == ST_OUT_OF_MEM) {
-        FREE(mint);
+        ABC_FREE(mint);
         return(NULL);
     }
     }
@@ -922,7 +922,7 @@ cuddApaStCountfree(
     DdApaNumber    d;
 
     d = (DdApaNumber) value;
-    FREE(d);
+    ABC_FREE(d);
     return(ST_CONTINUE);
 
 } /* end of cuddApaStCountfree */
diff --git a/src/bdd/cudd/cuddApprox.c b/src/bdd/cudd/cuddApprox.c
index debcf48b..c575b54b 100644
--- a/src/bdd/cudd/cuddApprox.c
+++ b/src/bdd/cudd/cuddApprox.c
@@ -510,9 +510,9 @@ cuddUnderApprox(
     result = UAmarkNodes(dd, f, info, threshold, safe, quality);
     if (result == 0) {
     (void) fprintf(dd->err, "Out-of-memory; Cannot subset\n");
-    FREE(info->page);
+    ABC_FREE(info->page);
     st_free_table(info->table);
-    FREE(info);
+    ABC_FREE(info);
     dd->errorCode = CUDD_MEMORY_OUT;
     return(NULL);
     }
@@ -524,9 +524,9 @@ cuddUnderApprox(
     (void) fprintf(dd->err, "Wrong prediction: %d versus actual %d\n",
                info->size, Cudd_DagSize(subset));
 #endif
-    FREE(info->page);
+    ABC_FREE(info->page);
     st_free_table(info->table);
-    FREE(info);
+    ABC_FREE(info);
 
 #ifdef DD_DEBUG
     if (subset != NULL) {
@@ -600,9 +600,9 @@ cuddRemapUnderApprox(
     result = RAmarkNodes(dd, f, info, threshold, quality);
     if (result == 0) {
     (void) fprintf(dd->err, "Out-of-memory; Cannot subset\n");
-    FREE(info->page);
+    ABC_FREE(info->page);
     st_free_table(info->table);
-    FREE(info);
+    ABC_FREE(info);
     dd->errorCode = CUDD_MEMORY_OUT;
     return(NULL);
     }
@@ -614,9 +614,9 @@ cuddRemapUnderApprox(
     (void) fprintf(dd->err, "Wrong prediction: %d versus actual %d\n",
                info->size, Cudd_DagSize(subset));
 #endif
-    FREE(info->page);
+    ABC_FREE(info->page);
     st_free_table(info->table);
-    FREE(info);
+    ABC_FREE(info);
 
 #ifdef DD_DEBUG
     if (subset != NULL) {
@@ -694,9 +694,9 @@ cuddBiasedUnderApprox(
     if (result == CARE_ERROR) {
     (void) fprintf(dd->err, "Out-of-memory; Cannot subset\n");
     cuddHashTableQuit(cache);
-    FREE(info->page);
+    ABC_FREE(info->page);
     st_free_table(info->table);
-    FREE(info);
+    ABC_FREE(info);
     dd->errorCode = CUDD_MEMORY_OUT;
     return(NULL);
     }
@@ -706,9 +706,9 @@ cuddBiasedUnderApprox(
     result = BAmarkNodes(dd, f, info, threshold, quality1, quality0);
     if (result == 0) {
     (void) fprintf(dd->err, "Out-of-memory; Cannot subset\n");
-    FREE(info->page);
+    ABC_FREE(info->page);
     st_free_table(info->table);
-    FREE(info);
+    ABC_FREE(info);
     dd->errorCode = CUDD_MEMORY_OUT;
     return(NULL);
     }
@@ -720,9 +720,9 @@ cuddBiasedUnderApprox(
     (void) fprintf(dd->err, "Wrong prediction: %d versus actual %d\n",
                info->size, Cudd_DagSize(subset));
 #endif
-    FREE(info->page);
+    ABC_FREE(info->page);
     st_free_table(info->table);
-    FREE(info);
+    ABC_FREE(info);
 
 #ifdef DD_DEBUG
     if (subset != NULL) {
@@ -891,7 +891,7 @@ gatherInfo(
     numVars = DBL_MAX_EXP - 1;
     }
 
-    info = ALLOC(ApproxInfo,1);
+    info = ABC_ALLOC(ApproxInfo,1);
     if (info == NULL) {
     dd->errorCode = CUDD_MEMORY_OUT;
     return(NULL);
@@ -905,17 +905,17 @@ gatherInfo(
     ** efficiently because we have counted the number of nodes of the
     ** BDD. info->index points to the next available entry in the array
     ** that stores the per-node information. */
-    info->page = ALLOC(NodeData,info->size);
+    info->page = ABC_ALLOC(NodeData,info->size);
     if (info->page == NULL) {
     dd->errorCode = CUDD_MEMORY_OUT;
-    FREE(info);
+    ABC_FREE(info);
     return(NULL);
     }
     memset(info->page, 0, info->size * sizeof(NodeData)); /* clear all page */
     info->table = st_init_table(st_ptrcmp,st_ptrhash);
     if (info->table == NULL) {
-    FREE(info->page);
-    FREE(info);
+    ABC_FREE(info->page);
+    ABC_FREE(info);
     return(NULL);
     }
     /* We visit the DAG in post-order DFS. Hence, the constant node is
@@ -923,8 +923,8 @@ gatherInfo(
 
     /* Info for the constant node: Initialize only fields different from 0. */
     if (st_insert(info->table, (char *)info->one, (char *)info->page) == ST_OUT_OF_MEM) {
-    FREE(info->page);
-    FREE(info);
+    ABC_FREE(info->page);
+    ABC_FREE(info);
     st_free_table(info->table);
     return(NULL);
     }
@@ -933,9 +933,9 @@ gatherInfo(
 
     infoTop = gatherInfoAux(node,info,parity);
     if (infoTop == NULL) {
-    FREE(info->page);
+    ABC_FREE(info->page);
     st_free_table(info->table);
-    FREE(info);
+    ABC_FREE(info);
     return(NULL);
     }
     if (Cudd_IsComplement(node)) {
diff --git a/src/bdd/cudd/cuddBddCorr.c b/src/bdd/cudd/cuddBddCorr.c
index c99324a8..a532f31d 100644
--- a/src/bdd/cudd/cuddBddCorr.c
+++ b/src/bdd/cudd/cuddBddCorr.c
@@ -230,7 +230,7 @@ bddCorrelationAux(
     }
     /* From now on, f is regular. */
     
-    entry = ALLOC(HashEntry,1);
+    entry = ABC_ALLOC(HashEntry,1);
     if (entry == NULL) {
     dd->errorCode = CUDD_MEMORY_OUT;
     return(CUDD_OUT_OF_MEM);
@@ -243,7 +243,7 @@ bddCorrelationAux(
     */
     if (st_lookup(table, (char *)entry, (char **)&dummy)) {
     min = *dummy;
-    FREE(entry);
+    ABC_FREE(entry);
     return(min);
     }
 
@@ -259,17 +259,17 @@ bddCorrelationAux(
 
     min1 = bddCorrelationAux(dd, Fv, Gv, table) / 2.0;
     if (min1 == (double)CUDD_OUT_OF_MEM) {
-    FREE(entry);
+    ABC_FREE(entry);
     return(CUDD_OUT_OF_MEM);
     }
     min2 = bddCorrelationAux(dd, Fnv, Gnv, table) / 2.0; 
     if (min2 == (double)CUDD_OUT_OF_MEM) {
-    FREE(entry);
+    ABC_FREE(entry);
     return(CUDD_OUT_OF_MEM);
     }
     min = (min1+min2);
     
-    pmin = ALLOC(double,1);
+    pmin = ABC_ALLOC(double,1);
     if (pmin == NULL) {
     dd->errorCode = CUDD_MEMORY_OUT;
     return((double)CUDD_OUT_OF_MEM);
@@ -277,8 +277,8 @@ bddCorrelationAux(
     *pmin = min;
 
     if (st_insert(table,(char *)entry, (char *)pmin) == ST_OUT_OF_MEM) {
-    FREE(entry);
-    FREE(pmin);
+    ABC_FREE(entry);
+    ABC_FREE(pmin);
     return((double)CUDD_OUT_OF_MEM);
     }
     return(min);
@@ -333,7 +333,7 @@ bddCorrelationWeightsAux(
     }
     /* From now on, f is regular. */
     
-    entry = ALLOC(HashEntry,1);
+    entry = ABC_ALLOC(HashEntry,1);
     if (entry == NULL) {
     dd->errorCode = CUDD_MEMORY_OUT;
     return((double)CUDD_OUT_OF_MEM);
@@ -346,7 +346,7 @@ bddCorrelationWeightsAux(
     */
     if (st_lookup(table, (char *)entry, (char **)&dummy)) {
     min = *dummy;
-    FREE(entry);
+    ABC_FREE(entry);
     return(min);
     }
 
@@ -368,17 +368,17 @@ bddCorrelationWeightsAux(
 
     min1 = bddCorrelationWeightsAux(dd, Fv, Gv, prob, table) * prob[index];
     if (min1 == (double)CUDD_OUT_OF_MEM) {
-    FREE(entry);
+    ABC_FREE(entry);
     return((double)CUDD_OUT_OF_MEM);
     }
     min2 = bddCorrelationWeightsAux(dd, Fnv, Gnv, prob, table) * (1.0 - prob[index]); 
     if (min2 == (double)CUDD_OUT_OF_MEM) {
-    FREE(entry);
+    ABC_FREE(entry);
     return((double)CUDD_OUT_OF_MEM);
     }
     min = (min1+min2);
     
-    pmin = ALLOC(double,1);
+    pmin = ABC_ALLOC(double,1);
     if (pmin == NULL) {
     dd->errorCode = CUDD_MEMORY_OUT;
     return((double)CUDD_OUT_OF_MEM);
@@ -386,8 +386,8 @@ bddCorrelationWeightsAux(
     *pmin = min;
 
     if (st_insert(table,(char *)entry, (char *)pmin) == ST_OUT_OF_MEM) {
-    FREE(entry);
-    FREE(pmin);
+    ABC_FREE(entry);
+    ABC_FREE(pmin);
     return((double)CUDD_OUT_OF_MEM);
     }
     return(min);
@@ -472,9 +472,9 @@ CorrelCleanUp(
     HashEntry *entry;
 
     entry = (HashEntry *) key;
-    FREE(entry);
+    ABC_FREE(entry);
     d = (double *)value;
-    FREE(d);
+    ABC_FREE(d);
     return ST_CONTINUE;
 
 } /* end of CorrelCleanUp */
diff --git a/src/bdd/cudd/cuddCache.c b/src/bdd/cudd/cuddCache.c
index d9e40921..e4aa0299 100644
--- a/src/bdd/cudd/cuddCache.c
+++ b/src/bdd/cudd/cuddCache.c
@@ -118,7 +118,7 @@ cuddInitCache(
     ** initial cache size. */
     logSize = cuddComputeFloorLog2(ddMax(cacheSize,unique->slots/2));
     cacheSize = 1 << logSize;
-    unique->acache = ALLOC(DdCache,cacheSize+1);
+    unique->acache = ABC_ALLOC(DdCache,cacheSize+1);
     if (unique->acache == NULL) {
     unique->errorCode = CUDD_MEMORY_OUT;
     return(0);
@@ -741,14 +741,14 @@ cuddCacheProfile(
     imax = imin = 0;
     totalcount = 0.0;
 
-    hystogramQ = ALLOC(double, nbins);
+    hystogramQ = ABC_ALLOC(double, nbins);
     if (hystogramQ == NULL) {
     table->errorCode = CUDD_MEMORY_OUT;
     return(0);
     }
-    hystogramR = ALLOC(double, nbins);
+    hystogramR = ABC_ALLOC(double, nbins);
     if (hystogramR == NULL) {
-    FREE(hystogramQ);
+    ABC_FREE(hystogramQ);
     table->errorCode = CUDD_MEMORY_OUT;
     return(0);
     }
@@ -825,8 +825,8 @@ cuddCacheProfile(
     if (retval == EOF) return(0);
     }
 
-    FREE(hystogramQ);
-    FREE(hystogramR);
+    ABC_FREE(hystogramQ);
+    ABC_FREE(hystogramR);
 #else
     for (i = 0; i < slots; i++) {
     nzeroes += cache[i].h == 0;
@@ -888,7 +888,7 @@ cuddCacheResize(
 
     saveHandler = MMoutOfMemory;
     MMoutOfMemory = Cudd_OutOfMem;
-    table->acache = cache = ALLOC(DdCache,slots+1);
+    table->acache = cache = ABC_ALLOC(DdCache,slots+1);
     MMoutOfMemory = saveHandler;
     /* If we fail to allocate the new table we just give up. */
     if (cache == NULL) {
@@ -944,7 +944,7 @@ cuddCacheResize(
     }
     }
 
-    FREE(oldacache);
+    ABC_FREE(oldacache);
 
     /* Reinitialize measurements so as to avoid division by 0 and
     ** immediate resizing.
diff --git a/src/bdd/cudd/cuddCompose.c b/src/bdd/cudd/cuddCompose.c
index 8c858051..43d65a5d 100644
--- a/src/bdd/cudd/cuddCompose.c
+++ b/src/bdd/cudd/cuddCompose.c
@@ -260,7 +260,7 @@ Cudd_addSwapVariables(
     int     i, j, k;
     int     *permut;
 
-    permut = ALLOC(int,dd->size);
+    permut = ABC_ALLOC(int,dd->size);
     if (permut == NULL) {
     dd->errorCode = CUDD_MEMORY_OUT;
     return(NULL);
@@ -274,7 +274,7 @@ Cudd_addSwapVariables(
     }
 
     swapped = Cudd_addPermute(dd,f,permut);
-    FREE(permut);
+    ABC_FREE(permut);
 
     return(swapped);
 
@@ -393,7 +393,7 @@ Cudd_SetVarMap (
     if (manager->map != NULL) {
     cuddCacheFlush(manager);
     } else {
-    manager->map = ALLOC(int,manager->maxSize);
+    manager->map = ABC_ALLOC(int,manager->maxSize);
     if (manager->map == NULL) {
         manager->errorCode = CUDD_MEMORY_OUT;
         return(0);
@@ -441,7 +441,7 @@ Cudd_bddSwapVariables(
     int     i, j, k;
     int     *permut;
 
-    permut = ALLOC(int,dd->size);
+    permut = ABC_ALLOC(int,dd->size);
     if (permut == NULL) {
     dd->errorCode = CUDD_MEMORY_OUT;
     return(NULL);
@@ -455,7 +455,7 @@ Cudd_bddSwapVariables(
     }
 
     swapped = Cudd_bddPermute(dd,f,permut);
-    FREE(permut);
+    ABC_FREE(permut);
 
     return(swapped);
 
@@ -488,7 +488,7 @@ Cudd_bddAdjPermuteX(
     int     i, j, k;
     int     *permut;
 
-    permut = ALLOC(int,dd->size);
+    permut = ABC_ALLOC(int,dd->size);
     if (permut == NULL) {
     dd->errorCode = CUDD_MEMORY_OUT;
     return(NULL);
@@ -502,7 +502,7 @@ Cudd_bddAdjPermuteX(
     }
 
     swapped = Cudd_bddPermute(dd,B,permut);
-    FREE(permut);
+    ABC_FREE(permut);
 
     return(swapped);
 
@@ -1520,17 +1520,17 @@ cuddAddNonSimComposeRecur(
     }
 
     /* Allocate two new vectors for the cofactors of vector. */
-    vect1 = ALLOC(DdNode *,lastsub);
+    vect1 = ABC_ALLOC(DdNode *,lastsub);
     if (vect1 == NULL) {
     dd->errorCode = CUDD_MEMORY_OUT;
     Cudd_RecursiveDeref(dd,key1);
     return(NULL);
     }
-    vect0 = ALLOC(DdNode *,lastsub);
+    vect0 = ABC_ALLOC(DdNode *,lastsub);
     if (vect0 == NULL) {
     dd->errorCode = CUDD_MEMORY_OUT;
     Cudd_RecursiveDeref(dd,key1);
-    FREE(vect1);
+    ABC_FREE(vect1);
     return(NULL);
     }
 
@@ -1552,15 +1552,15 @@ cuddAddNonSimComposeRecur(
 
     /* Recur on children. */
     T = cuddAddNonSimComposeRecur(dd,f1,vect1,key1,cube1,lastsub);
-    FREE(vect1);
+    ABC_FREE(vect1);
     if (T == NULL) {
     Cudd_RecursiveDeref(dd,key1);
-    FREE(vect0);
+    ABC_FREE(vect0);
     return(NULL);
     }
     cuddRef(T);
     E = cuddAddNonSimComposeRecur(dd,f0,vect0,key0,cube1,lastsub);
-    FREE(vect0);
+    ABC_FREE(vect0);
     if (E == NULL) {
     Cudd_RecursiveDeref(dd,key1);
     Cudd_RecursiveDeref(dd,T);
diff --git a/src/bdd/cudd/cuddDecomp.c b/src/bdd/cudd/cuddDecomp.c
index 35a77b8c..871a99bb 100644
--- a/src/bdd/cudd/cuddDecomp.c
+++ b/src/bdd/cudd/cuddDecomp.c
@@ -130,7 +130,7 @@ static int cuddConjunctsAux ARGS((DdManager * dd, DdNode * f, DdNode ** c1, DdNo
 
   SideEffects [The factors are returned in an array as side effects.
   The array is allocated by this function. It is the caller's responsibility
-  to free it. On successful completion, the conjuncts are already
+  to ABC_FREE it. On successful completion, the conjuncts are already
   referenced. If the function returns 0, the array for the conjuncts is
   not allocated. If the function returns 1, the only factor equals the
   function to be decomposed.]
@@ -182,7 +182,7 @@ Cudd_bddApproxConjDecomp(
 
     if (glocal != DD_ONE(dd)) {
     if (hlocal != DD_ONE(dd)) {
-        *conjuncts = ALLOC(DdNode *,2);
+        *conjuncts = ABC_ALLOC(DdNode *,2);
         if (*conjuncts == NULL) {
         Cudd_RecursiveDeref(dd,glocal);
         Cudd_RecursiveDeref(dd,hlocal);
@@ -194,7 +194,7 @@ Cudd_bddApproxConjDecomp(
         return(2);
     } else {
         Cudd_RecursiveDeref(dd,hlocal);
-        *conjuncts = ALLOC(DdNode *,1);
+        *conjuncts = ABC_ALLOC(DdNode *,1);
         if (*conjuncts == NULL) {
         Cudd_RecursiveDeref(dd,glocal);
         dd->errorCode = CUDD_MEMORY_OUT;
@@ -205,7 +205,7 @@ Cudd_bddApproxConjDecomp(
     }
     } else {
     Cudd_RecursiveDeref(dd,glocal);
-    *conjuncts = ALLOC(DdNode *,1);
+    *conjuncts = ABC_ALLOC(DdNode *,1);
     if (*conjuncts == NULL) {
         Cudd_RecursiveDeref(dd,hlocal);
         dd->errorCode = CUDD_MEMORY_OUT;
@@ -229,7 +229,7 @@ Cudd_bddApproxConjDecomp(
 
   SideEffects [The two disjuncts are returned in an array as side effects.
   The array is allocated by this function. It is the caller's responsibility
-  to free it. On successful completion, the disjuncts are already
+  to ABC_FREE it. On successful completion, the disjuncts are already
   referenced. If the function returns 0, the array for the disjuncts is
   not allocated. If the function returns 1, the only factor equals the
   function to be decomposed.]
@@ -268,7 +268,7 @@ Cudd_bddApproxDisjDecomp(
 
   SideEffects [The factors are returned in an array as side effects.
   The array is allocated by this function. It is the caller's responsibility
-  to free it. On successful completion, the conjuncts are already
+  to ABC_FREE it. On successful completion, the conjuncts are already
   referenced. If the function returns 0, the array for the conjuncts is
   not allocated. If the function returns 1, the only factor equals the
   function to be decomposed.]
@@ -365,7 +365,7 @@ Cudd_bddIterConjDecomp(
 
     if (old[0] != DD_ONE(dd)) {
     if (old[1] != DD_ONE(dd)) {
-        *conjuncts = ALLOC(DdNode *,2);
+        *conjuncts = ABC_ALLOC(DdNode *,2);
         if (*conjuncts == NULL) {
         Cudd_RecursiveDeref(dd,old[0]);
         Cudd_RecursiveDeref(dd,old[1]);
@@ -377,7 +377,7 @@ Cudd_bddIterConjDecomp(
         return(2);
     } else {
         Cudd_RecursiveDeref(dd,old[1]);
-        *conjuncts = ALLOC(DdNode *,1);
+        *conjuncts = ABC_ALLOC(DdNode *,1);
         if (*conjuncts == NULL) {
         Cudd_RecursiveDeref(dd,old[0]);
         dd->errorCode = CUDD_MEMORY_OUT;
@@ -388,7 +388,7 @@ Cudd_bddIterConjDecomp(
     }
     } else {
     Cudd_RecursiveDeref(dd,old[0]);
-    *conjuncts = ALLOC(DdNode *,1);
+    *conjuncts = ABC_ALLOC(DdNode *,1);
     if (*conjuncts == NULL) {
         Cudd_RecursiveDeref(dd,old[1]);
         dd->errorCode = CUDD_MEMORY_OUT;
@@ -412,7 +412,7 @@ Cudd_bddIterConjDecomp(
 
   SideEffects [The two disjuncts are returned in an array as side effects.
   The array is allocated by this function. It is the caller's responsibility
-  to free it. On successful completion, the disjuncts are already
+  to ABC_FREE it. On successful completion, the disjuncts are already
   referenced. If the function returns 0, the array for the disjuncts is
   not allocated. If the function returns 1, the only factor equals the
   function to be decomposed.]
@@ -452,7 +452,7 @@ Cudd_bddIterDisjDecomp(
 
   SideEffects [The two factors are returned in an array as side effects.
   The array is allocated by this function. It is the caller's responsibility
-  to free it. On successful completion, the conjuncts are already
+  to ABC_FREE it. On successful completion, the conjuncts are already
   referenced. If the function returns 0, the array for the conjuncts is
   not allocated. If the function returns 1, the only factor equals the
   function to be decomposed.]
@@ -484,7 +484,7 @@ Cudd_bddGenConjDecomp(
 
     if (glocal != one) {
     if (hlocal != one) {
-        *conjuncts = ALLOC(DdNode *,2);
+        *conjuncts = ABC_ALLOC(DdNode *,2);
         if (*conjuncts == NULL) {
         Cudd_RecursiveDeref(dd,glocal);
         Cudd_RecursiveDeref(dd,hlocal);
@@ -496,7 +496,7 @@ Cudd_bddGenConjDecomp(
         return(2);
     } else {
         Cudd_RecursiveDeref(dd,hlocal);
-        *conjuncts = ALLOC(DdNode *,1);
+        *conjuncts = ABC_ALLOC(DdNode *,1);
         if (*conjuncts == NULL) {
         Cudd_RecursiveDeref(dd,glocal);
         dd->errorCode = CUDD_MEMORY_OUT;
@@ -507,7 +507,7 @@ Cudd_bddGenConjDecomp(
     }
     } else {
     Cudd_RecursiveDeref(dd,glocal);
-    *conjuncts = ALLOC(DdNode *,1);
+    *conjuncts = ABC_ALLOC(DdNode *,1);
     if (*conjuncts == NULL) {
         Cudd_RecursiveDeref(dd,hlocal);
         dd->errorCode = CUDD_MEMORY_OUT;
@@ -531,7 +531,7 @@ Cudd_bddGenConjDecomp(
 
   SideEffects [The two disjuncts are returned in an array as side effects.
   The array is allocated by this function. It is the caller's responsibility
-  to free it. On successful completion, the disjuncts are already
+  to ABC_FREE it. On successful completion, the disjuncts are already
   referenced. If the function returns 0, the array for the disjuncts is
   not allocated. If the function returns 1, the only factor equals the
   function to be decomposed.]
@@ -571,7 +571,7 @@ Cudd_bddGenDisjDecomp(
 
   SideEffects [The two factors are returned in an array as side effects.
   The array is allocated by this function. It is the caller's responsibility
-  to free it. On successful completion, the conjuncts are already
+  to ABC_FREE it. On successful completion, the conjuncts are already
   referenced. If the function returns 0, the array for the conjuncts is
   not allocated. If the function returns 1, the only factor equals the
   function to be decomposed.]
@@ -594,7 +594,7 @@ Cudd_bddVarConjDecomp(
     support = Cudd_Support(dd,f);
     if (support == NULL) return(0);
     if (Cudd_IsConstant(support)) {
-    *conjuncts = ALLOC(DdNode *,1);
+    *conjuncts = ABC_ALLOC(DdNode *,1);
     if (*conjuncts == NULL) {
         dd->errorCode = CUDD_MEMORY_OUT;
         return(0);
@@ -639,7 +639,7 @@ Cudd_bddVarConjDecomp(
 
     if (glocal != DD_ONE(dd)) {
     if (hlocal != DD_ONE(dd)) {
-        *conjuncts = ALLOC(DdNode *,2);
+        *conjuncts = ABC_ALLOC(DdNode *,2);
         if (*conjuncts == NULL) {
         Cudd_RecursiveDeref(dd,glocal);
         Cudd_RecursiveDeref(dd,hlocal);
@@ -651,7 +651,7 @@ Cudd_bddVarConjDecomp(
         return(2);
     } else {
         Cudd_RecursiveDeref(dd,hlocal);
-        *conjuncts = ALLOC(DdNode *,1);
+        *conjuncts = ABC_ALLOC(DdNode *,1);
         if (*conjuncts == NULL) {
         Cudd_RecursiveDeref(dd,glocal);
         dd->errorCode = CUDD_MEMORY_OUT;
@@ -662,7 +662,7 @@ Cudd_bddVarConjDecomp(
     }
     } else {
     Cudd_RecursiveDeref(dd,glocal);
-    *conjuncts = ALLOC(DdNode *,1);
+    *conjuncts = ABC_ALLOC(DdNode *,1);
     if (*conjuncts == NULL) {
         Cudd_RecursiveDeref(dd,hlocal);
         dd->errorCode = CUDD_MEMORY_OUT;
@@ -689,7 +689,7 @@ Cudd_bddVarConjDecomp(
 
   SideEffects [The two disjuncts are returned in an array as side effects.
   The array is allocated by this function. It is the caller's responsibility
-  to free it. On successful completion, the disjuncts are already
+  to ABC_FREE it. On successful completion, the disjuncts are already
   referenced. If the function returns 0, the array for the disjuncts is
   not allocated. If the function returns 1, the only factor equals the
   function to be decomposed.]
@@ -777,7 +777,7 @@ CreateBotDist(
     */
     distance = (distanceNv > distanceNnv) ? (distanceNv+1) : (distanceNnv + 1);
 
-    nodeStat = ALLOC(NodeStat, 1);
+    nodeStat = ABC_ALLOC(NodeStat, 1);
     if (nodeStat == NULL) {
     return(0);
     }
@@ -847,7 +847,7 @@ CountMinterms(
     /* store 
      */
 
-    dummy = ALLOC(double, 1);
+    dummy = ABC_ALLOC(double, 1);
     if (dummy == NULL) return(-1.0);
     *dummy = min;
     if (st_insert(mintermTable, (char *)node, (char *)dummy) == ST_OUT_OF_MEM) {
@@ -876,7 +876,7 @@ ConjunctsFree(
 {
     Cudd_RecursiveDeref(dd, factors->g);
     Cudd_RecursiveDeref(dd, factors->h);
-    FREE(factors);
+    ABC_FREE(factors);
     return;
 
 } /* end of ConjunctsFree */
@@ -978,7 +978,7 @@ CheckTablesCacheAndReturn(
     /* if both dont exist in table, we know one exists(either g or h).
      * Therefore store the other and proceed
      */
-    factors = ALLOC(Conjuncts, 1);
+    factors = ABC_ALLOC(Conjuncts, 1);
     if (factors == NULL) return(NULL);
     if ((pairValue == BOTH_H) || (pairValue == H_ST)) {
     if (g != one) {
@@ -1041,7 +1041,7 @@ CheckTablesCacheAndReturn(
         
     /* cache the result for this node */
     if (st_insert(cacheTable, (char *)node, (char *)factors) == ST_OUT_OF_MEM) {
-    FREE(factors);
+    ABC_FREE(factors);
     return(NULL);
     }
 
@@ -1078,7 +1078,7 @@ PickOnePair(
     Conjuncts *factors;
     int oneRef, twoRef;
     
-    factors = ALLOC(Conjuncts, 1);
+    factors = ABC_ALLOC(Conjuncts, 1);
     if (factors == NULL) return(NULL);
 
     /* count the number of pointers to pair 2 */
@@ -1120,7 +1120,7 @@ PickOnePair(
         value |= 1;
         if (st_insert(ghTable, (char *)Cudd_Regular(factors->g),
                   (char *)(long)value) == ST_OUT_OF_MEM) {
-            FREE(factors);
+            ABC_FREE(factors);
             return(NULL);
         }
         }
@@ -1128,7 +1128,7 @@ PickOnePair(
         value = 1;
         if (st_insert(ghTable, (char *)Cudd_Regular(factors->g),
               (char *)(long)value) == ST_OUT_OF_MEM) {
-        FREE(factors);
+        ABC_FREE(factors);
         return(NULL);
         }
     }
@@ -1142,7 +1142,7 @@ PickOnePair(
         value |= 2;
         if (st_insert(ghTable, (char *)Cudd_Regular(factors->h),
                   (char *)(long)value) == ST_OUT_OF_MEM) {
-            FREE(factors);
+            ABC_FREE(factors);
             return(NULL);
         }
         }        
@@ -1150,7 +1150,7 @@ PickOnePair(
         value = 2;
         if (st_insert(ghTable, (char *)Cudd_Regular(factors->h),
               (char *)(long)value) == ST_OUT_OF_MEM) {
-        FREE(factors);
+        ABC_FREE(factors);
         return(NULL);
         }
     }
@@ -1159,7 +1159,7 @@ PickOnePair(
     /* Store factors in cache table for later use. */
     if (st_insert(cacheTable, (char *)node, (char *)factors) ==
         ST_OUT_OF_MEM) {
-    FREE(factors);
+    ABC_FREE(factors);
     return(NULL);
     }
 
@@ -1208,7 +1208,7 @@ CheckInTables(
     return NULL;
     }
     
-    factors = ALLOC(Conjuncts, 1);
+    factors = ABC_ALLOC(Conjuncts, 1);
     if (factors == NULL) {
     *outOfMem = 1;
     return NULL;
@@ -1236,7 +1236,7 @@ CheckInTables(
         if (st_insert(ghTable, (char *)Cudd_Regular(h1),
               (char *)(long)value) == ST_OUT_OF_MEM) {
         *outOfMem = 1;
-        FREE(factors);
+        ABC_FREE(factors);
         return(NULL);
         }
     }
@@ -1249,7 +1249,7 @@ CheckInTables(
         if (st_insert(ghTable, (char *)Cudd_Regular(h1),
               (char *)(long)value) == ST_OUT_OF_MEM) {
         *outOfMem = 1;
-        FREE(factors);
+        ABC_FREE(factors);
         return(NULL);
         }
     }
@@ -1262,7 +1262,7 @@ CheckInTables(
         if (st_insert(ghTable, (char *)Cudd_Regular(g1),
               (char *)(long)value) == ST_OUT_OF_MEM) {
         *outOfMem = 1;
-        FREE(factors);
+        ABC_FREE(factors);
         return(NULL);
         }
     }
@@ -1275,7 +1275,7 @@ CheckInTables(
         if (st_insert(ghTable, (char *)Cudd_Regular(g1),
               (char *)(long)value) == ST_OUT_OF_MEM) {
         *outOfMem = 1;
-        FREE(factors);
+        ABC_FREE(factors);
         return(NULL);
         }
     }
@@ -1288,7 +1288,7 @@ CheckInTables(
         if (st_insert(ghTable, (char *)Cudd_Regular(h2),
               (char *)(long)value) == ST_OUT_OF_MEM) {
         *outOfMem = 1;
-        FREE(factors);
+        ABC_FREE(factors);
         return(NULL);
         }
     }
@@ -1301,7 +1301,7 @@ CheckInTables(
         if (st_insert(ghTable, (char *)Cudd_Regular(h2),
               (char *)(long)value) == ST_OUT_OF_MEM) {
         *outOfMem = 1;
-        FREE(factors);
+        ABC_FREE(factors);
         return(NULL);
         }
     }
@@ -1314,7 +1314,7 @@ CheckInTables(
         if (st_insert(ghTable, (char *)Cudd_Regular(g2),
               (char *)(long)value) == ST_OUT_OF_MEM) {
         *outOfMem = 1;
-        FREE(factors);
+        ABC_FREE(factors);
         return(NULL);
         }
     }
@@ -1327,7 +1327,7 @@ CheckInTables(
         if (st_insert(ghTable, (char *)Cudd_Regular(g2),
               (char *)(long)value) == ST_OUT_OF_MEM) {
         *outOfMem = 1;
-        FREE(factors);
+        ABC_FREE(factors);
         return(NULL);
         }
     }
@@ -1340,7 +1340,7 @@ CheckInTables(
         if (st_insert(ghTable, (char *)Cudd_Regular(h1),
               (char *)(long)value) == ST_OUT_OF_MEM) {
         *outOfMem = 1;
-        FREE(factors);
+        ABC_FREE(factors);
         return(NULL);
         }
     }
@@ -1353,7 +1353,7 @@ CheckInTables(
         if (st_insert(ghTable, (char *)Cudd_Regular(g1),
               (char *)(long)value) == ST_OUT_OF_MEM) {
         *outOfMem = 1;
-        FREE(factors);
+        ABC_FREE(factors);
         return(NULL);
         }
     }
@@ -1366,7 +1366,7 @@ CheckInTables(
         if (st_insert(ghTable, (char *)Cudd_Regular(h2),
               (char *)(long)value) == ST_OUT_OF_MEM) {
         *outOfMem = 1;
-        FREE(factors);
+        ABC_FREE(factors);
         return(NULL);
         }
     }
@@ -1379,7 +1379,7 @@ CheckInTables(
         if (st_insert(ghTable, (char *)Cudd_Regular(g2),
               (char *)(long)value) == ST_OUT_OF_MEM) {
         *outOfMem = 1;
-        FREE(factors);
+        ABC_FREE(factors);
         return(NULL);
         }
     }
@@ -1389,7 +1389,7 @@ CheckInTables(
     if (st_insert(cacheTable, (char *)node, (char *)factors) ==
         ST_OUT_OF_MEM) {
     *outOfMem = 1;
-    FREE(factors);
+    ABC_FREE(factors);
     return(NULL);
     }
     return factors;
@@ -1438,7 +1438,7 @@ ZeroCase(
     /* Seprate variable and child */
     if (factorsNv->g == one) {
     Cudd_RecursiveDeref(dd, factorsNv->g);
-    factors = ALLOC(Conjuncts, 1);
+    factors = ABC_ALLOC(Conjuncts, 1);
     if (factors == NULL) {
         dd->errorCode = CUDD_MEMORY_OUT;
         Cudd_RecursiveDeref(dd, factorsNv->h);
@@ -1452,7 +1452,7 @@ ZeroCase(
         dd->errorCode = CUDD_MEMORY_OUT;
         Cudd_RecursiveDeref(dd, factorsNv->h); 
         Cudd_RecursiveDeref(dd, x);
-        FREE(factors);
+        ABC_FREE(factors);
         return NULL;
     }
     
@@ -1472,7 +1472,7 @@ ZeroCase(
     /* Seprate variable and child */
     if (factorsNv->h == one) {
     Cudd_RecursiveDeref(dd, factorsNv->h);
-    factors = ALLOC(Conjuncts, 1);
+    factors = ABC_ALLOC(Conjuncts, 1);
     if (factors == NULL) {
         dd->errorCode = CUDD_MEMORY_OUT;
         Cudd_RecursiveDeref(dd, factorsNv->g);
@@ -1486,7 +1486,7 @@ ZeroCase(
         dd->errorCode = CUDD_MEMORY_OUT;
         Cudd_RecursiveDeref(dd, factorsNv->g);
         Cudd_RecursiveDeref(dd, x);
-        FREE(factors);
+        ABC_FREE(factors);
         return(NULL);
     }
     /* store x in h table,  the other node is already in the table */
@@ -1617,7 +1617,7 @@ ZeroCase(
     Cudd_RecursiveDeref(dd, g2);
     Cudd_RecursiveDeref(dd, h2);
     } else {
-    /* now free what was created and not used */
+    /* now ABC_FREE what was created and not used */
     if ((factors->g == g1) || (factors->g == h1)) {
         Cudd_RecursiveDeref(dd, g2);
         Cudd_RecursiveDeref(dd, h2);
@@ -1676,7 +1676,7 @@ BuildConjuncts(
 
     /* if f is constant, return (f,f) */
     if (Cudd_IsConstant(node)) {
-    factors = ALLOC(Conjuncts, 1);
+    factors = ABC_ALLOC(Conjuncts, 1);
     if (factors == NULL) {
         dd->errorCode = CUDD_MEMORY_OUT;
         return(NULL);
@@ -1705,7 +1705,7 @@ BuildConjuncts(
     if (((nodeStat->localRef > maxLocalRef*2/3) &&
      (distance < approxDistance*2/3)) ||
         (distance <= approxDistance/4)) {
-    factors = ALLOC(Conjuncts, 1);
+    factors = ABC_ALLOC(Conjuncts, 1);
     if (factors == NULL) {
         dd->errorCode = CUDD_MEMORY_OUT;
         return(NULL);
@@ -1737,7 +1737,7 @@ BuildConjuncts(
         value = 1;
         if (st_insert(ghTable, (char *)Cudd_Regular(node), (char *)(long)value) == ST_OUT_OF_MEM) {
         dd->errorCode = CUDD_MEMORY_OUT;
-        FREE(factors);
+        ABC_FREE(factors);
         return NULL;
         }
     } else {
@@ -1747,7 +1747,7 @@ BuildConjuncts(
         value = 2;
         if (st_insert(ghTable, (char *)Cudd_Regular(node), (char *)(long)value) == ST_OUT_OF_MEM) {
         dd->errorCode = CUDD_MEMORY_OUT;
-        FREE(factors);
+        ABC_FREE(factors);
         return NULL;
         }
     }
@@ -1804,7 +1804,7 @@ BuildConjuncts(
         /* is responsible for freeing factorsNv */
         factors = ZeroCase(dd, node, factorsNv, ghTable,
                    cacheTable, switched);
-        if (freeNv) FREE(factorsNv);
+        if (freeNv) ABC_FREE(factorsNv);
         return(factors);
     }
     }
@@ -1817,7 +1817,7 @@ BuildConjuncts(
     if (factorsNnv == NULL) {
         Cudd_RecursiveDeref(dd, factorsNv->g);
         Cudd_RecursiveDeref(dd, factorsNv->h);
-        if (freeNv) FREE(factorsNv);
+        if (freeNv) ABC_FREE(factorsNv);
         return(NULL);
     }
     freeNnv = FactorsNotStored(factorsNnv);
@@ -1830,7 +1830,7 @@ BuildConjuncts(
         /* is responsible for freeing factorsNv */
         factors = ZeroCase(dd, node, factorsNnv, ghTable,
                    cacheTable, switched);
-        if (freeNnv) FREE(factorsNnv);
+        if (freeNnv) ABC_FREE(factorsNnv);
         return(factors);
     }
     }
@@ -1857,8 +1857,8 @@ BuildConjuncts(
     Cudd_RecursiveDeref(dd, factorsNv->h);
     Cudd_RecursiveDeref(dd, factorsNnv->g);
     Cudd_RecursiveDeref(dd, factorsNnv->h);
-    if (freeNv) FREE(factorsNv);
-    if (freeNnv) FREE(factorsNnv);
+    if (freeNv) ABC_FREE(factorsNv);
+    if (freeNnv) ABC_FREE(factorsNnv);
     return(NULL);
     }
 
@@ -1871,8 +1871,8 @@ BuildConjuncts(
     Cudd_RecursiveDeref(dd, factorsNnv->g);
     Cudd_RecursiveDeref(dd, factorsNnv->h);
     Cudd_RecursiveDeref(dd, g1);
-    if (freeNv) FREE(factorsNv);
-    if (freeNnv) FREE(factorsNnv);
+    if (freeNv) ABC_FREE(factorsNv);
+    if (freeNnv) ABC_FREE(factorsNnv);
     return(NULL);
     }
 
@@ -1886,8 +1886,8 @@ BuildConjuncts(
     Cudd_RecursiveDeref(dd, factorsNnv->h);
     Cudd_RecursiveDeref(dd, g1);
     Cudd_RecursiveDeref(dd, h1);
-    if (freeNv) FREE(factorsNv);
-    if (freeNnv) FREE(factorsNnv);
+    if (freeNv) ABC_FREE(factorsNv);
+    if (freeNnv) ABC_FREE(factorsNnv);
     return(NULL);
     }
     cuddRef(g2);
@@ -1903,15 +1903,15 @@ BuildConjuncts(
     Cudd_RecursiveDeref(dd, g1);
     Cudd_RecursiveDeref(dd, h1);
     Cudd_RecursiveDeref(dd, g2);
-    if (freeNv) FREE(factorsNv);
-    if (freeNnv) FREE(factorsNnv);
+    if (freeNv) ABC_FREE(factorsNv);
+    if (freeNnv) ABC_FREE(factorsNnv);
     return(NULL);
     }
     cuddRef(h2);
     Cudd_RecursiveDeref(dd, factorsNv->h);
     Cudd_RecursiveDeref(dd, factorsNnv->g);
-    if (freeNv) FREE(factorsNv);
-    if (freeNnv) FREE(factorsNnv);
+    if (freeNv) ABC_FREE(factorsNv);
+    if (freeNnv) ABC_FREE(factorsNnv);
 
     /* check for each pair in tables and choose one */
     factors = CheckInTables(node, g1, h1, g2, h2, ghTable, cacheTable, &outOfMem);
@@ -1943,7 +1943,7 @@ BuildConjuncts(
     Cudd_RecursiveDeref(dd, g2);
     Cudd_RecursiveDeref(dd, h2);
     } else {
-    /* now free what was created and not used */
+    /* now ABC_FREE what was created and not used */
     if ((factors->g == g1) || (factors->g == h1)) {
         Cudd_RecursiveDeref(dd, g2);
         Cudd_RecursiveDeref(dd, h2);
@@ -2000,7 +2000,7 @@ cuddConjunctsAux(
     if (distanceTable == NULL) goto outOfMem;
     
     /* make the entry for the constant */
-    nodeStat = ALLOC(NodeStat, 1);
+    nodeStat = ABC_ALLOC(NodeStat, 1);
     if (nodeStat == NULL) goto outOfMem;
     nodeStat->distance = 0;
     nodeStat->localRef = 1;
@@ -2024,7 +2024,7 @@ cuddConjunctsAux(
     stGen = st_init_gen(distanceTable);
     if (stGen == NULL) goto outOfMem;
     while(st_gen(stGen, (char **)&key, (char **)&value)) {
-        FREE(value);
+        ABC_FREE(value);
     }
     st_free_gen(stGen); stGen = NULL;
     st_free_table(distanceTable);
@@ -2061,11 +2061,11 @@ cuddConjunctsAux(
                  approxDistance, maxLocalRef, ghTable, mintermTable);
     if (factors == NULL) goto outOfMem;
 
-    /* free up tables */
+    /* ABC_FREE up tables */
     stGen = st_init_gen(distanceTable);
     if (stGen == NULL) goto outOfMem;
     while(st_gen(stGen, (char **)&key, (char **)&value)) {
-    FREE(value);
+    ABC_FREE(value);
     }
     st_free_gen(stGen); stGen = NULL;
     st_free_table(distanceTable); distanceTable = NULL;
@@ -2074,7 +2074,7 @@ cuddConjunctsAux(
     stGen = st_init_gen(mintermTable);
     if (stGen == NULL) goto outOfMem;
     while(st_gen(stGen, (char **)&key, (char **)&value)) {
-    FREE(value);
+    ABC_FREE(value);
     }
     st_free_gen(stGen); stGen = NULL;
     st_free_table(mintermTable); mintermTable = NULL;
@@ -2086,7 +2086,7 @@ cuddConjunctsAux(
     *c2 = factors->h;
     cuddRef(*c1);
     cuddRef(*c2);
-    if (freeFactors) FREE(factors);
+    if (freeFactors) ABC_FREE(factors);
     
 #if 0    
     if ((*c1 == f) && (!Cudd_IsConstant(f))) {
@@ -2121,7 +2121,7 @@ outOfMem:
     stGen = st_init_gen(distanceTable);
     if (stGen == NULL) goto outOfMem;
     while(st_gen(stGen, (char **)&key, (char **)&value)) {
-        FREE(value);
+        ABC_FREE(value);
     }
     st_free_gen(stGen); stGen = NULL;
     st_free_table(distanceTable); distanceTable = NULL;
@@ -2130,7 +2130,7 @@ outOfMem:
     stGen = st_init_gen(mintermTable);
     if (stGen == NULL) goto outOfMem;
     while(st_gen(stGen, (char **)&key, (char **)&value)) {
-        FREE(value);
+        ABC_FREE(value);
     }
     st_free_gen(stGen); stGen = NULL;
     st_free_table(mintermTable); mintermTable = NULL;
diff --git a/src/bdd/cudd/cuddExact.c b/src/bdd/cudd/cuddExact.c
index 6852be68..9472dd8b 100644
--- a/src/bdd/cudd/cuddExact.c
+++ b/src/bdd/cudd/cuddExact.c
@@ -188,19 +188,19 @@ cuddExact(
     newOrder = getMatrix(maxBinomial, size);
     if (newOrder == NULL) goto cuddExactOutOfMem;
 
-    newCost = ALLOC(int, maxBinomial);
+    newCost = ABC_ALLOC(int, maxBinomial);
     if (newCost == NULL) goto cuddExactOutOfMem;
 
     oldOrder = getMatrix(maxBinomial, size);
     if (oldOrder == NULL) goto cuddExactOutOfMem;
 
-    oldCost = ALLOC(int, maxBinomial);
+    oldCost = ABC_ALLOC(int, maxBinomial);
     if (oldCost == NULL) goto cuddExactOutOfMem;
 
-    bestOrder = ALLOC(DdHalfWord, size);
+    bestOrder = ABC_ALLOC(DdHalfWord, size);
     if (bestOrder == NULL) goto cuddExactOutOfMem;
 
-    mask = ALLOC(char, nvars);
+    mask = ABC_ALLOC(char, nvars);
     if (mask == NULL) goto cuddExactOutOfMem;
 
     symmInfo = initSymmInfo(table, lower, upper);
@@ -289,22 +289,22 @@ cuddExact(
 
     freeMatrix(newOrder);
     freeMatrix(oldOrder);
-    FREE(bestOrder);
-    FREE(oldCost);
-    FREE(newCost);
-    FREE(symmInfo);
-    FREE(mask);
+    ABC_FREE(bestOrder);
+    ABC_FREE(oldCost);
+    ABC_FREE(newCost);
+    ABC_FREE(symmInfo);
+    ABC_FREE(mask);
     return(1);
 
 cuddExactOutOfMem:
 
     if (newOrder != NULL) freeMatrix(newOrder);
     if (oldOrder != NULL) freeMatrix(oldOrder);
-    if (bestOrder != NULL) FREE(bestOrder);
-    if (oldCost != NULL) FREE(oldCost);
-    if (newCost != NULL) FREE(newCost);
-    if (symmInfo != NULL) FREE(symmInfo);
-    if (mask != NULL) FREE(mask);
+    if (bestOrder != NULL) ABC_FREE(bestOrder);
+    if (oldCost != NULL) ABC_FREE(oldCost);
+    if (newCost != NULL) ABC_FREE(newCost);
+    if (symmInfo != NULL) ABC_FREE(symmInfo);
+    if (mask != NULL) ABC_FREE(mask);
     table->errorCode = CUDD_MEMORY_OUT;
     return(0);
 
@@ -335,7 +335,7 @@ getMaxBinomial(
 
     k = (n & ~1) >> 1;
 
-    numerator = ALLOC(int,k);
+    numerator = ABC_ALLOC(int,k);
     if (numerator == NULL) return(-1);
     
     for (i = 0; i < k; i++)
@@ -358,7 +358,7 @@ getMaxBinomial(
     for (i = 0; i < k; i++)
     result *= numerator[i];
 
-    FREE(numerator);
+    ABC_FREE(numerator);
     return(result);
 
 }  /* end of getMaxBinomial */
@@ -440,9 +440,9 @@ getMatrix(
     int i;
 
     if (cols*rows == 0) return(NULL);
-    matrix = ALLOC(DdHalfWord *, rows);
+    matrix = ABC_ALLOC(DdHalfWord *, rows);
     if (matrix == NULL) return(NULL);
-    matrix[0] = ALLOC(DdHalfWord, cols*rows);
+    matrix[0] = ABC_ALLOC(DdHalfWord, cols*rows);
     if (matrix[0] == NULL) return(NULL);
     for (i = 1; i < rows; i++) {
     matrix[i] = matrix[i-1] + cols;
@@ -467,8 +467,8 @@ static void
 freeMatrix(
   DdHalfWord ** matrix)
 {
-    FREE(matrix[0]);
-    FREE(matrix);
+    ABC_FREE(matrix[0]);
+    ABC_FREE(matrix);
     return;
 
 } /* end of freeMatrix */
@@ -956,7 +956,7 @@ initSymmInfo(
     int level, index, next, nextindex;
     DdHalfWord *symmInfo;
 
-    symmInfo =  ALLOC(DdHalfWord, table->size);
+    symmInfo =  ABC_ALLOC(DdHalfWord, table->size);
     if (symmInfo == NULL) return(NULL);
 
     for (level = lower; level <= upper; level++) {
diff --git a/src/bdd/cudd/cuddExport.c b/src/bdd/cudd/cuddExport.c
index d148be42..18caeaa0 100644
--- a/src/bdd/cudd/cuddExport.c
+++ b/src/bdd/cudd/cuddExport.c
@@ -119,7 +119,7 @@ Cudd_DumpBlif(
     int        i;
 
     /* Build a bit array with the support of f. */
-    sorted = ALLOC(int,nvars);
+    sorted = ABC_ALLOC(int,nvars);
     if (sorted == NULL) {
     dd->errorCode = CUDD_MEMORY_OUT;
     goto failure;
@@ -136,7 +136,7 @@ Cudd_DumpBlif(
     scan = cuddT(scan);
     }
     Cudd_RecursiveDeref(dd,support);
-    support = NULL; /* so that we do not try to free it in case of failure */
+    support = NULL; /* so that we do not try to ABC_FREE it in case of failure */
 
     /* Write the header (.model .inputs .outputs). */
     if (mname == NULL) {
@@ -157,7 +157,7 @@ Cudd_DumpBlif(
             if (retval == EOF) goto failure;
         }
     }
-    FREE(sorted);
+    ABC_FREE(sorted);
     sorted = NULL;
 
     /* Write the .output line. */
@@ -184,7 +184,7 @@ Cudd_DumpBlif(
     return(1);
 
 failure:
-    if (sorted != NULL) FREE(sorted);
+    if (sorted != NULL) ABC_FREE(sorted);
     if (support != NULL) Cudd_RecursiveDeref(dd,support);
     return(0);
 
@@ -325,7 +325,7 @@ Cudd_DumpDot(
     long    refAddr, diff, mask;
 
     /* Build a bit array with the support of f. */
-    sorted = ALLOC(int,nvars);
+    sorted = ABC_ALLOC(int,nvars);
     if (sorted == NULL) {
     dd->errorCode = CUDD_MEMORY_OUT;
     goto failure;
@@ -342,7 +342,7 @@ Cudd_DumpDot(
     scan = cuddT(scan);
     }
     Cudd_RecursiveDeref(dd,support);
-    support = NULL; /* so that we do not try to free it in case of failure */
+    support = NULL; /* so that we do not try to ABC_FREE it in case of failure */
 
     /* Initialize symbol table for visited nodes. */
     visited = st_init_table(st_ptrcmp, st_ptrhash);
@@ -549,11 +549,11 @@ Cudd_DumpDot(
     if (retval == EOF) goto failure;
 
     st_free_table(visited);
-    FREE(sorted);
+    ABC_FREE(sorted);
     return(1);
 
 failure:
-    if (sorted != NULL) FREE(sorted);
+    if (sorted != NULL) ABC_FREE(sorted);
     if (support != NULL) Cudd_RecursiveDeref(dd,support);
     if (visited != NULL) st_free_table(visited);
     return(0);
@@ -750,7 +750,7 @@ Cudd_DumpDDcal(
     st_free_table(visited);
 
     /* Build a bit array with the support of f. */
-    sorted = ALLOC(int,nvars);
+    sorted = ABC_ALLOC(int,nvars);
     if (sorted == NULL) {
     dd->errorCode = CUDD_MEMORY_OUT;
     goto failure;
@@ -767,7 +767,7 @@ Cudd_DumpDDcal(
     scan = cuddT(scan);
     }
     Cudd_RecursiveDeref(dd,support);
-    support = NULL; /* so that we do not try to free it in case of failure */
+    support = NULL; /* so that we do not try to ABC_FREE it in case of failure */
     for (i = 0; i < nvars; i++) {
         if (sorted[dd->invperm[i]]) {
         if (inames == NULL || inames[dd->invperm[i]] == NULL) {
@@ -780,7 +780,7 @@ Cudd_DumpDDcal(
     retval = fprintf(fp,"%s", i == nvars - 1 ? "\n" : " * ");
     if (retval == EOF) goto failure;
     }
-    FREE(sorted);
+    ABC_FREE(sorted);
     sorted = NULL;
 
     /* Initialize symbol table for visited nodes. */
@@ -822,7 +822,7 @@ Cudd_DumpDDcal(
     return(1);
 
 failure:
-    if (sorted != NULL) FREE(sorted);
+    if (sorted != NULL) ABC_FREE(sorted);
     if (support != NULL) Cudd_RecursiveDeref(dd,support);
     if (visited != NULL) st_free_table(visited);
     return(0);
diff --git a/src/bdd/cudd/cuddGenCof.c b/src/bdd/cudd/cuddGenCof.c
index 142ee27e..660526ee 100644
--- a/src/bdd/cudd/cuddGenCof.c
+++ b/src/bdd/cudd/cuddGenCof.c
@@ -302,7 +302,7 @@ Cudd_bddConstrainDecomp(
     int i;
 
     /* Create an initialize decomposition array. */
-    decomp = ALLOC(DdNode *,dd->size);
+    decomp = ABC_ALLOC(DdNode *,dd->size);
     if (decomp == NULL) {
     dd->errorCode = CUDD_MEMORY_OUT;
     return(NULL);
@@ -322,7 +322,7 @@ Cudd_bddConstrainDecomp(
     res = cuddBddConstrainDecomp(dd,f,decomp);
     } while (dd->reordered == 1);
     if (res == 0) {
-    FREE(decomp);
+    ABC_FREE(decomp);
     return(NULL);
     }
     /* Missing components are constant ones. */
@@ -442,7 +442,7 @@ Cudd_bddCharToVect(
 
     if (f == Cudd_Not(DD_ONE(dd))) return(NULL);
 
-    vect = ALLOC(DdNode *, dd->size);
+    vect = ABC_ALLOC(DdNode *, dd->size);
     if (vect == NULL) {
     dd->errorCode = CUDD_MEMORY_OUT;
     return(NULL);
@@ -464,7 +464,7 @@ Cudd_bddCharToVect(
     }
     } while (dd->reordered == 1);
     if (res == NULL) {
-    FREE(vect);
+    ABC_FREE(vect);
     return(NULL);
     }
     return(vect);
@@ -1460,14 +1460,14 @@ cuddBddLICMarkEdges(
     */
 
     /* Check the cache. */
-    key = ALLOC(MarkCacheKey, 1);
+    key = ABC_ALLOC(MarkCacheKey, 1);
     if (key == NULL) {
     dd->errorCode = CUDD_MEMORY_OUT;
     return(CUDD_OUT_OF_MEM);
     }
     key->f = f; key->c = c;
     if (st_lookup(cache, (char *)key, (char **)&res)) {
-    FREE(key);
+    ABC_FREE(key);
     if (comple) {
         if (res == DD_LIC_0) res = DD_LIC_1;
         else if (res == DD_LIC_1) res = DD_LIC_0;
@@ -1498,12 +1498,12 @@ cuddBddLICMarkEdges(
 
     resT = cuddBddLICMarkEdges(dd, Fv, Cv, table, cache);
     if (resT == CUDD_OUT_OF_MEM) {
-    FREE(key);
+    ABC_FREE(key);
     return(CUDD_OUT_OF_MEM);
     }
     resE = cuddBddLICMarkEdges(dd, Fnv, Cnv, table, cache);
     if (resE == CUDD_OUT_OF_MEM) {
-    FREE(key);
+    ABC_FREE(key);
     return(CUDD_OUT_OF_MEM);
     }
 
@@ -1515,7 +1515,7 @@ cuddBddLICMarkEdges(
     } else if (retval == 1) {
         *slot = (char *) (ptrint)((int)((ptrint) *slot) | (resT << 2) | resE);
     } else {
-        FREE(key);
+        ABC_FREE(key);
         return(CUDD_OUT_OF_MEM);
     }
     }
@@ -1523,7 +1523,7 @@ cuddBddLICMarkEdges(
     /* Cache result. */
     res = resT | resE;
     if (st_insert(cache, (char *)key, (char *)(ptrint)res) == ST_OUT_OF_MEM) {
-    FREE(key);
+    ABC_FREE(key);
     return(CUDD_OUT_OF_MEM);
     }
 
@@ -1730,7 +1730,7 @@ MarkCacheCleanUp(
     MarkCacheKey *entry;
 
     entry = (MarkCacheKey *) key;
-    FREE(entry);
+    ABC_FREE(entry);
     return ST_CONTINUE;
 
 } /* end of MarkCacheCleanUp */
diff --git a/src/bdd/cudd/cuddGenetic.c b/src/bdd/cudd/cuddGenetic.c
index 9fe03dad..3b10aecb 100644
--- a/src/bdd/cudd/cuddGenetic.c
+++ b/src/bdd/cudd/cuddGenetic.c
@@ -176,7 +176,7 @@ cuddGa(
     if (popsize < 4) popsize = 4;    /* enforce minimum population size */
 
     /* Allocate population table. */
-    storedd = ALLOC(int,(popsize+2)*(numvars+1));
+    storedd = ABC_ALLOC(int,(popsize+2)*(numvars+1));
     if (storedd == NULL) {
     table->errorCode = CUDD_MEMORY_OUT;
     return(0);
@@ -190,10 +190,10 @@ cuddGa(
     ** one has a repeat count greater than 1. This copy is the one pointed
     ** by the computed table.
     */
-    repeat = ALLOC(int,popsize);
+    repeat = ABC_ALLOC(int,popsize);
     if (repeat == NULL) {
     table->errorCode = CUDD_MEMORY_OUT;
-    FREE(storedd);
+    ABC_FREE(storedd);
     return(0);
     }
     for (i = 0; i < popsize; i++) {
@@ -202,8 +202,8 @@ cuddGa(
     computed = st_init_table(array_compare,array_hash);
     if (computed == NULL) {
     table->errorCode = CUDD_MEMORY_OUT;
-    FREE(storedd);
-    FREE(repeat);
+    ABC_FREE(storedd);
+    ABC_FREE(repeat);
     return(0);
     }
 
@@ -215,8 +215,8 @@ cuddGa(
 
     /* Store the initial order in the computed table. */
     if (st_insert(computed,(char *)storedd,(char *) 0) == ST_OUT_OF_MEM) {
-    FREE(storedd);
-    FREE(repeat);
+    ABC_FREE(storedd);
+    ABC_FREE(repeat);
     st_free_table(computed);
     return(0);
     }
@@ -234,16 +234,16 @@ cuddGa(
     */
     if (!make_random(table,lower)) {
     table->errorCode = CUDD_MEMORY_OUT;
-    FREE(storedd);
-    FREE(repeat);
+    ABC_FREE(storedd);
+    ABC_FREE(repeat);
     st_free_table(computed);
     return(0);
     }
     for (i = 1; i < popsize; i++) {
     result = build_dd(table,i,lower,upper);    /* build and sift order */
     if (!result) {
-        FREE(storedd);
-        FREE(repeat);
+        ABC_FREE(storedd);
+        ABC_FREE(repeat);
         st_free_table(computed);
         return(0);
     }
@@ -252,8 +252,8 @@ cuddGa(
     } else {
         if (st_insert(computed,(char *)&STOREDD(i,0),(char *)(long)i) ==
         ST_OUT_OF_MEM) {
-        FREE(storedd);
-        FREE(repeat);
+        ABC_FREE(storedd);
+        ABC_FREE(repeat);
         st_free_table(computed);
         return(0);
         }
@@ -295,8 +295,8 @@ cuddGa(
     for (m = 0; m < cross; m++) {
     if (!PMX(table->size)) {    /* perform one crossover */
         table->errorCode = CUDD_MEMORY_OUT;
-        FREE(storedd);
-        FREE(repeat);
+        ABC_FREE(storedd);
+        ABC_FREE(repeat);
         st_free_table(computed);
         return(0);
     }
@@ -306,8 +306,8 @@ cuddGa(
     for (i = popsize; i <= popsize+1; i++) {
         result = build_dd(table,i,lower,upper); /* build and sift child */
         if (!result) {
-        FREE(storedd);
-        FREE(repeat);
+        ABC_FREE(storedd);
+        ABC_FREE(repeat);
         st_free_table(computed);
         return(0);
         }
@@ -325,8 +325,8 @@ cuddGa(
         result = st_lookup(computed,(char *)&STOREDD(large,0),(char
         **)&index);
         if (!result) {
-            FREE(storedd);
-            FREE(repeat);
+            ABC_FREE(storedd);
+            ABC_FREE(repeat);
             st_free_table(computed);
             return(0);
         }
@@ -335,8 +335,8 @@ cuddGa(
             int *pointer = &STOREDD(index,0);
             result = st_delete(computed, (char **)&pointer,NULL);
             if (!result) {
-            FREE(storedd);
-            FREE(repeat);
+            ABC_FREE(storedd);
+            ABC_FREE(repeat);
             st_free_table(computed);
             return(0);
             }
@@ -354,8 +354,8 @@ cuddGa(
         } else {
             if (st_insert(computed,(char *)&STOREDD(large,0),
             (char *)(long)large) == ST_OUT_OF_MEM) {
-            FREE(storedd);
-            FREE(repeat);
+            ABC_FREE(storedd);
+            ABC_FREE(repeat);
             st_free_table(computed);
             return(0);
             }
@@ -380,8 +380,8 @@ cuddGa(
     st_free_table(computed);
     computed = NULL;
     result = build_dd(table,small,lower,upper);
-    FREE(storedd);
-    FREE(repeat);
+    ABC_FREE(storedd);
+    ABC_FREE(repeat);
     return(result);
 
 } /* end of cuddGa */
@@ -413,7 +413,7 @@ make_random(
     int    *used;        /* is a number already in a permutation */
     int    next;        /* next random number without repetitions */
 
-    used = ALLOC(int,numvars);
+    used = ABC_ALLOC(int,numvars);
     if (used == NULL) {
     table->errorCode = CUDD_MEMORY_OUT;
     return(0);
@@ -453,7 +453,7 @@ make_random(
 #endif
 #endif
     }
-    FREE(used);
+    ABC_FREE(used);
     return(1);
 
 } /* end of make_random */
@@ -761,20 +761,20 @@ PMX(
     int     i;        /* loop vars */
     int        u,v;        /* aux vars */
 
-    inv1 = ALLOC(int,maxvar);
+    inv1 = ABC_ALLOC(int,maxvar);
     if (inv1 == NULL) {
     return(0);
     }
-    inv2 = ALLOC(int,maxvar);
+    inv2 = ABC_ALLOC(int,maxvar);
     if (inv2 == NULL) {
-    FREE(inv1);
+    ABC_FREE(inv1);
     return(0);
     }
 
     /* Choose two orders from the population using roulette wheel. */
     if (!roulette(&mom,&dad)) {
-    FREE(inv1);
-    FREE(inv2);
+    ABC_FREE(inv1);
+    ABC_FREE(inv2);
     return(0);
     }
 
@@ -851,8 +851,8 @@ PMX(
     (void) fprintf(table->out,"\n");
 #endif
 
-    FREE(inv1);
-    FREE(inv2);
+    ABC_FREE(inv1);
+    ABC_FREE(inv2);
     return(1);
 
 } /* end of PMX */
@@ -879,7 +879,7 @@ roulette(
     double spin;
     int i;
 
-    wheel = ALLOC(double,popsize);
+    wheel = ABC_ALLOC(double,popsize);
     if (wheel == NULL) {
     return(0);
     }
@@ -914,7 +914,7 @@ roulette(
     } while (i == *p1);
     *p2 = i;
 
-    FREE(wheel);
+    ABC_FREE(wheel);
     return(1);
 
 } /* end of roulette */
diff --git a/src/bdd/cudd/cuddGroup.c b/src/bdd/cudd/cuddGroup.c
index fbf8b6dd..3d987400 100644
--- a/src/bdd/cudd/cuddGroup.c
+++ b/src/bdd/cudd/cuddGroup.c
@@ -697,17 +697,17 @@ ddGroupSifting(
     /* Order variables to sift. */
     entry = NULL;
     sifted = NULL;
-    var = ALLOC(int,nvars);
+    var = ABC_ALLOC(int,nvars);
     if (var == NULL) {
     table->errorCode = CUDD_MEMORY_OUT;
     goto ddGroupSiftingOutOfMem;
     }
-    entry = ALLOC(int,nvars);
+    entry = ABC_ALLOC(int,nvars);
     if (entry == NULL) {
     table->errorCode = CUDD_MEMORY_OUT;
     goto ddGroupSiftingOutOfMem;
     }
-    sifted = ALLOC(int,nvars);
+    sifted = ABC_ALLOC(int,nvars);
     if (sifted == NULL) {
     table->errorCode = CUDD_MEMORY_OUT;
     goto ddGroupSiftingOutOfMem;
@@ -838,16 +838,16 @@ ddGroupSifting(
       if (lazyFlag) ddSetVarHandled(table, xindex);
     } /* for */
 
-    FREE(sifted);
-    FREE(var);
-    FREE(entry);
+    ABC_FREE(sifted);
+    ABC_FREE(var);
+    ABC_FREE(entry);
 
     return(1);
 
 ddGroupSiftingOutOfMem:
-    if (entry != NULL)    FREE(entry);
-    if (var != NULL)    FREE(var);
-    if (sifted != NULL)    FREE(sifted);
+    if (entry != NULL)    ABC_FREE(entry);
+    if (var != NULL)    ABC_FREE(var);
+    if (sifted != NULL)    ABC_FREE(sifted);
 
     return(0);
 
diff --git a/src/bdd/cudd/cuddHarwell.c b/src/bdd/cudd/cuddHarwell.c
index 59394ce4..45ff736c 100644
--- a/src/bdd/cudd/cuddHarwell.c
+++ b/src/bdd/cudd/cuddHarwell.c
@@ -223,12 +223,12 @@ Cudd_addHarwell(
     /* Allocate or reallocate arrays for variables as needed */
     if (*nx == 0) {
     if (lnx > 0) {
-        *x = lx = ALLOC(DdNode *,lnx);
+        *x = lx = ABC_ALLOC(DdNode *,lnx);
         if (lx == NULL) {
         dd->errorCode = CUDD_MEMORY_OUT;
         return(0);
         }
-        *xn = lxn =  ALLOC(DdNode *,lnx);
+        *xn = lxn =  ABC_ALLOC(DdNode *,lnx);
         if (lxn == NULL) {
         dd->errorCode = CUDD_MEMORY_OUT;
         return(0);
@@ -237,12 +237,12 @@ Cudd_addHarwell(
         *x = *xn = NULL;
     }
     } else if (lnx > *nx) {
-    *x = lx = REALLOC(DdNode *, *x, lnx);
+    *x = lx = ABC_REALLOC(DdNode *, *x, lnx);
     if (lx == NULL) {
         dd->errorCode = CUDD_MEMORY_OUT;
         return(0);
     }
-    *xn = lxn =  REALLOC(DdNode *, *xn, lnx);
+    *xn = lxn =  ABC_REALLOC(DdNode *, *xn, lnx);
     if (lxn == NULL) {
         dd->errorCode = CUDD_MEMORY_OUT;
         return(0);
@@ -253,12 +253,12 @@ Cudd_addHarwell(
     }
     if (*ny == 0) {
     if (lny >0) {
-        *y = ly = ALLOC(DdNode *,lny);
+        *y = ly = ABC_ALLOC(DdNode *,lny);
         if (ly == NULL) {
         dd->errorCode = CUDD_MEMORY_OUT;
         return(0);
         }
-        *yn_ = lyn = ALLOC(DdNode *,lny);
+        *yn_ = lyn = ABC_ALLOC(DdNode *,lny);
         if (lyn == NULL) {
         dd->errorCode = CUDD_MEMORY_OUT;
         return(0);
@@ -267,12 +267,12 @@ Cudd_addHarwell(
         *y = *yn_ = NULL;
     }
     } else if (lny > *ny) {
-    *y = ly = REALLOC(DdNode *, *y, lny);
+    *y = ly = ABC_REALLOC(DdNode *, *y, lny);
     if (ly == NULL) {
         dd->errorCode = CUDD_MEMORY_OUT;
         return(0);
     }
-    *yn_ = lyn = REALLOC(DdNode *, *yn_, lny);
+    *yn_ = lyn = ABC_REALLOC(DdNode *, *yn_, lny);
     if (lyn == NULL) {
         dd->errorCode = CUDD_MEMORY_OUT;
         return(0);
@@ -323,12 +323,12 @@ Cudd_addHarwell(
     }
     
     /* Read structure data */
-    colptr = ALLOC(int, ncol+1);
+    colptr = ABC_ALLOC(int, ncol+1);
     if (colptr == NULL) {
     dd->errorCode = CUDD_MEMORY_OUT;
     return(0);
     }
-    rowind = ALLOC(int, nnzero);
+    rowind = ABC_ALLOC(int, nnzero);
     if (rowind == NULL) {
     dd->errorCode = CUDD_MEMORY_OUT;
     return(0);
@@ -337,12 +337,12 @@ Cudd_addHarwell(
     for (i=0; i<ncol+1; i++) {
     err = fscanf(fp, " %d ", &u);
     if (err == EOF){ 
-        FREE(colptr);
-        FREE(rowind);
+        ABC_FREE(colptr);
+        ABC_FREE(rowind);
         return(0);
     } else if (err != 1) {
-        FREE(colptr);
-        FREE(rowind);
+        ABC_FREE(colptr);
+        ABC_FREE(rowind);
         return(0);
     }
     colptr[i] = u - 1;
@@ -350,19 +350,19 @@ Cudd_addHarwell(
     if (colptr[0] != 0) {
     (void) fprintf(dd->err,"%s: Unexpected colptr[0] (%d)\n",
                key,colptr[0]);
-    FREE(colptr);
-    FREE(rowind);
+    ABC_FREE(colptr);
+    ABC_FREE(rowind);
     return(0);
     }
     for (i=0; i<nnzero; i++) {
     err = fscanf(fp, " %d ", &u);
     if (err == EOF){ 
-        FREE(colptr);
-        FREE(rowind);
+        ABC_FREE(colptr);
+        ABC_FREE(rowind);
         return(0);
     } else if (err != 1) {
-        FREE(colptr);
-        FREE(rowind);
+        ABC_FREE(colptr);
+        ABC_FREE(rowind);
         return(0);
     }
     rowind[i] = u - 1;
@@ -381,8 +381,8 @@ Cudd_addHarwell(
         }
         if (w == NULL) {
         Cudd_RecursiveDeref(dd, cubey);
-        FREE(colptr);
-        FREE(rowind);
+        ABC_FREE(colptr);
+        ABC_FREE(rowind);
         return(0);
         }
         cuddRef(w);
@@ -395,16 +395,16 @@ Cudd_addHarwell(
         err = fscanf(fp, " %lf ", &val);
         if (err == EOF || err != 1){ 
         Cudd_RecursiveDeref(dd, cubey);
-        FREE(colptr);
-        FREE(rowind);
+        ABC_FREE(colptr);
+        ABC_FREE(rowind);
         return(0);
         }
         /* Create new Constant node if necessary */
         cubex = cuddUniqueConst(dd, (CUDD_VALUE_TYPE) val);
         if (cubex == NULL) {
         Cudd_RecursiveDeref(dd, cubey);
-        FREE(colptr);
-        FREE(rowind);
+        ABC_FREE(colptr);
+        ABC_FREE(rowind);
         return(0);
         }
         cuddRef(cubex);
@@ -418,8 +418,8 @@ Cudd_addHarwell(
         if (w == NULL) {
             Cudd_RecursiveDeref(dd, cubey);
             Cudd_RecursiveDeref(dd, cubex);
-            FREE(colptr);
-            FREE(rowind);
+            ABC_FREE(colptr);
+            ABC_FREE(rowind);
             return(0);
         }
         cuddRef(w);
@@ -431,8 +431,8 @@ Cudd_addHarwell(
         if (minterm1 == NULL) {
         Cudd_RecursiveDeref(dd, cubey);
         Cudd_RecursiveDeref(dd, cubex);
-        FREE(colptr);
-        FREE(rowind);
+        ABC_FREE(colptr);
+        ABC_FREE(rowind);
         return(0);
         }
         cuddRef(minterm1);
@@ -440,8 +440,8 @@ Cudd_addHarwell(
         w = Cudd_addApply(dd, Cudd_addPlus, *E, minterm1);
         if (w == NULL) {
         Cudd_RecursiveDeref(dd, cubey);
-        FREE(colptr);
-        FREE(rowind);
+        ABC_FREE(colptr);
+        ABC_FREE(rowind);
         return(0);
         }
         cuddRef(w);
@@ -451,8 +451,8 @@ Cudd_addHarwell(
     }
     Cudd_RecursiveDeref(dd, cubey);
     }
-    FREE(colptr);
-    FREE(rowind);
+    ABC_FREE(colptr);
+    ABC_FREE(rowind);
 
     /* Read right-hand sides */
     for (j=0; j<nrhs; j++) {
diff --git a/src/bdd/cudd/cuddInit.c b/src/bdd/cudd/cuddInit.c
index 8e06a425..20a88b11 100644
--- a/src/bdd/cudd/cuddInit.c
+++ b/src/bdd/cudd/cuddInit.c
@@ -123,7 +123,7 @@ Cudd_Init(
 
     saveHandler = MMoutOfMemory;
     MMoutOfMemory = Cudd_OutOfMem;
-    unique->stash = ALLOC(char,(maxMemory / DD_STASH_FRACTION) + 4);
+    unique->stash = ABC_ALLOC(char,(maxMemory / DD_STASH_FRACTION) + 4);
     MMoutOfMemory = saveHandler;
     if (unique->stash == NULL) {
     (void) fprintf(unique->err,"Unable to set aside memory\n");
@@ -155,7 +155,7 @@ Cudd_Init(
     one = unique->one;
     zero = Cudd_Not(one);
     /* Create the projection functions. */
-    unique->vars = ALLOC(DdNodePtr,unique->maxSize);
+    unique->vars = ABC_ALLOC(DdNodePtr,unique->maxSize);
     if (unique->vars == NULL) {
     unique->errorCode = CUDD_MEMORY_OUT;
     return(NULL);
@@ -193,7 +193,7 @@ void
 Cudd_Quit(
   DdManager * unique)
 {
-    if (unique->stash != NULL) FREE(unique->stash);
+    if (unique->stash != NULL) ABC_FREE(unique->stash);
     cuddFreeTable(unique);
 
 } /* end of Cudd_Quit */
@@ -223,7 +223,7 @@ cuddZddInitUniv(
     DdNode    *p, *res;
     int        i;
 
-    zdd->univ = ALLOC(DdNodePtr, zdd->sizeZ);
+    zdd->univ = ABC_ALLOC(DdNodePtr, zdd->sizeZ);
     if (zdd->univ == NULL) {
     zdd->errorCode = CUDD_MEMORY_OUT;
     return(0);
@@ -237,7 +237,7 @@ cuddZddInitUniv(
     res = cuddUniqueInterZdd(zdd, index, p, p);
     if (res == NULL) {
         Cudd_RecursiveDerefZdd(zdd,p);
-        FREE(zdd->univ);
+        ABC_FREE(zdd->univ);
         return(0);
     }
     cuddRef(res);
@@ -271,7 +271,7 @@ cuddZddFreeUniv(
 {
     if (zdd->univ) {
     Cudd_RecursiveDerefZdd(zdd, zdd->univ[0]);
-    FREE(zdd->univ);
+    ABC_FREE(zdd->univ);
     }
 
 } /* end of cuddZddFreeUniv */
diff --git a/src/bdd/cudd/cuddInt.h b/src/bdd/cudd/cuddInt.h
index a5d0cf16..df843e33 100644
--- a/src/bdd/cudd/cuddInt.h
+++ b/src/bdd/cudd/cuddInt.h
@@ -346,7 +346,7 @@ struct DdManager {    /* specialized DD symbol table */
     long *linear;        /* linear transform matrix */
     /* Memory Management */
     DdNode **memoryList;    /* memory manager for symbol table */
-    DdNode *nextFree;        /* list of free nodes */
+    DdNode *nextFree;        /* list of ABC_FREE nodes */
     char *stash;        /* memory reserve */
 #ifndef DD_NO_DEATH_ROW
     DdNode **deathRow;        /* queue for dereferencing */
@@ -410,7 +410,7 @@ struct DdManager {    /* specialized DD symbol table */
     double cacheLastInserts;    /* insertions at the last cache resizing */
     double cachedeletions;    /* number of deletions during garbage coll. */
 #ifdef DD_STATS
-    double nodesFreed;        /* number of nodes returned to the free list */
+    double nodesFreed;        /* number of nodes returned to the ABC_FREE list */
     double nodesDropped;    /* number of nodes killed by dereferencing */
 #endif
     unsigned int peakLiveNodes;    /* maximum number of live nodes */
@@ -481,10 +481,10 @@ typedef struct DdLevelQueue {
 
 /**Macro***********************************************************************
 
-  Synopsis    [Adds node to the head of the free list.]
+  Synopsis    [Adds node to the head of the ABC_FREE list.]
 
-  Description [Adds node to the head of the free list.  Does not
-  deallocate memory chunks that become free.  This function is also
+  Description [Adds node to the head of the ABC_FREE list.  Does not
+  deallocate memory chunks that become ABC_FREE.  This function is also
   used by the dynamic reordering functions.]
 
   SideEffects [None]
diff --git a/src/bdd/cudd/cuddInteract.c b/src/bdd/cudd/cuddInteract.c
index 96613639..3745b408 100644
--- a/src/bdd/cudd/cuddInteract.c
+++ b/src/bdd/cudd/cuddInteract.c
@@ -217,7 +217,7 @@ cuddInitInteract(
     int n = table->size;
 
     words = ((n * (n-1)) >> (1 + LOGBPL)) + 1;
-    table->interact = interact = ALLOC(long,words);
+    table->interact = interact = ABC_ALLOC(long,words);
     if (interact == NULL) {
     table->errorCode = CUDD_MEMORY_OUT;
     return(0);
@@ -226,10 +226,10 @@ cuddInitInteract(
     interact[i] = 0;
     }
 
-    support = ALLOC(int,n);
+    support = ABC_ALLOC(int,n);
     if (support == NULL) {
     table->errorCode = CUDD_MEMORY_OUT;
-    FREE(interact);
+    ABC_FREE(interact);
     return(0);
     }
 
@@ -259,7 +259,7 @@ cuddInitInteract(
     }
     ddClearGlobal(table);
 
-    FREE(support);
+    ABC_FREE(support);
     return(1);
 
 } /* end of cuddInitInteract */
diff --git a/src/bdd/cudd/cuddLCache.c b/src/bdd/cudd/cuddLCache.c
index 8bd37ba0..97546cda 100644
--- a/src/bdd/cudd/cuddLCache.c
+++ b/src/bdd/cudd/cuddLCache.c
@@ -158,7 +158,7 @@ cuddLocalCacheInit(
     DdLocalCache *cache;
     int logSize;
 
-    cache = ALLOC(DdLocalCache,1);
+    cache = ABC_ALLOC(DdLocalCache,1);
     if (cache == NULL) {
     manager->errorCode = CUDD_MEMORY_OUT;
     return(NULL);
@@ -172,10 +172,10 @@ cuddLocalCacheInit(
     logSize = cuddComputeFloorLog2(ddMax(cacheSize,manager->slots/2));
     cacheSize = 1 << logSize;
     cache->item = (DdLocalCacheItem *)
-    ALLOC(char, cacheSize * cache->itemsize);
+    ABC_ALLOC(char, cacheSize * cache->itemsize);
     if (cache->item == NULL) {
     manager->errorCode = CUDD_MEMORY_OUT;
-    FREE(cache);
+    ABC_FREE(cache);
     return(NULL);
     }
     cache->slots = cacheSize;
@@ -218,8 +218,8 @@ cuddLocalCacheQuit(
     cache->manager->memused -=
     cache->slots * cache->itemsize + sizeof(DdLocalCache);
     cuddLocalCacheRemoveFromList(cache);
-    FREE(cache->item);
-    FREE(cache);
+    ABC_FREE(cache->item);
+    ABC_FREE(cache);
 
     return;
 
@@ -422,7 +422,7 @@ cuddLocalCacheProfile(
     imax = imin = nzeroes = 0;
     totalcount = 0.0;
 
-    hystogram = ALLOC(long, nbins);
+    hystogram = ABC_ALLOC(long, nbins);
     if (hystogram == NULL) {
     return(0);
     }
@@ -482,7 +482,7 @@ cuddLocalCacheProfile(
     if (retval == EOF) return(0);
     }
 
-    FREE(hystogram);
+    ABC_FREE(hystogram);
     return(1);
 
 } /* end of cuddLocalCacheProfile */
@@ -514,7 +514,7 @@ cuddHashTableInit(
 #pragma pointer_size save
 #pragma pointer_size short
 #endif
-    hash = ALLOC(DdHashTable, 1);
+    hash = ABC_ALLOC(DdHashTable, 1);
     if (hash == NULL) {
     manager->errorCode = CUDD_MEMORY_OUT;
     return(NULL);
@@ -530,10 +530,10 @@ cuddHashTableInit(
     logSize = cuddComputeFloorLog2(initSize);
     hash->numBuckets = 1 << logSize;
     hash->shift = sizeof(int) * 8 - logSize;
-    hash->bucket = ALLOC(DdHashItem *, hash->numBuckets);
+    hash->bucket = ABC_ALLOC(DdHashItem *, hash->numBuckets);
     if (hash->bucket == NULL) {
     manager->errorCode = CUDD_MEMORY_OUT;
-    FREE(hash);
+    ABC_FREE(hash);
     return(NULL);
     }
     memset(hash->bucket, 0, hash->numBuckets * sizeof(DdHashItem *));
@@ -583,12 +583,12 @@ cuddHashTableQuit(
     memlist = hash->memoryList;
     while (memlist != NULL) {
     nextmem = (DdHashItem **) memlist[0];
-    FREE(memlist);
+    ABC_FREE(memlist);
     memlist = nextmem;
     }
 
-    FREE(hash->bucket);
-    FREE(hash);
+    ABC_FREE(hash->bucket);
+    ABC_FREE(hash);
 #ifdef __osf__
 #pragma pointer_size restore
 #endif
@@ -658,7 +658,7 @@ cuddHashTableInsert(
   is an entry for the given key in the table; NULL otherwise. If the
   entry is present, its reference counter is decremented if not
   saturated. If the counter reaches 0, the value of the entry is
-  dereferenced, and the entry is returned to the free list.]
+  dereferenced, and the entry is returned to the ABC_FREE list.]
 
   SideEffects [None]
 
@@ -773,7 +773,7 @@ cuddHashTableInsert1(
   Returns the value associated to the key if there is an entry for the given
   key in the table; NULL otherwise. If the entry is present, its reference
   counter is decremented if not saturated. If the counter reaches 0, the
-  value of the entry is dereferenced, and the entry is returned to the free
+  value of the entry is dereferenced, and the entry is returned to the ABC_FREE
   list.]
 
   SideEffects [None]
@@ -882,7 +882,7 @@ cuddHashTableInsert2(
   Returns the value associated to the key if there is an entry for the given
   key in the table; NULL otherwise. If the entry is present, its reference
   counter is decremented if not saturated. If the counter reaches 0, the
-  value of the entry is dereferenced, and the entry is returned to the free
+  value of the entry is dereferenced, and the entry is returned to the ABC_FREE
   list.]
 
   SideEffects [None]
@@ -994,7 +994,7 @@ cuddHashTableInsert3(
   Returns the value associated to the key if there is an entry for the given
   key in the table; NULL otherwise. If the entry is present, its reference
   counter is decremented if not saturated. If the counter reaches 0, the
-  value of the entry is dereferenced, and the entry is returned to the free
+  value of the entry is dereferenced, and the entry is returned to the ABC_FREE
   list.]
 
   SideEffects [None]
@@ -1090,7 +1090,7 @@ cuddLocalCacheResize(
     saveHandler = MMoutOfMemory;
     MMoutOfMemory = Cudd_OutOfMem;
     cache->item = item =
-    (DdLocalCacheItem *) ALLOC(char, slots * cache->itemsize);
+    (DdLocalCacheItem *) ABC_ALLOC(char, slots * cache->itemsize);
     MMoutOfMemory = saveHandler;
     /* If we fail to allocate the new table we just give up. */
     if (item == NULL) {
@@ -1121,7 +1121,7 @@ cuddLocalCacheResize(
     }
     }
 
-    FREE(olditem);
+    ABC_FREE(olditem);
 
     /* Reinitialize measurements so as to avoid division by 0 and
     ** immediate resizing.
@@ -1272,7 +1272,7 @@ cuddHashTableResize(
 #pragma pointer_size save
 #pragma pointer_size short
 #endif
-    buckets = ALLOC(DdHashItem *, numBuckets);
+    buckets = ABC_ALLOC(DdHashItem *, numBuckets);
     MMoutOfMemory = saveHandler;
     if (buckets == NULL) {
     hash->maxsize <<= 1;
@@ -1335,7 +1335,7 @@ cuddHashTableResize(
         }
     }
     }
-    FREE(oldBuckets);
+    ABC_FREE(oldBuckets);
     return(1);
 
 } /* end of cuddHashTableResize */
@@ -1373,14 +1373,14 @@ cuddHashTableAlloc(
     if (hash->nextFree == NULL) {
     saveHandler = MMoutOfMemory;
     MMoutOfMemory = Cudd_OutOfMem;
-    mem = (DdHashItem **) ALLOC(char,(DD_MEM_CHUNK+1) * itemsize);
+    mem = (DdHashItem **) ABC_ALLOC(char,(DD_MEM_CHUNK+1) * itemsize);
     MMoutOfMemory = saveHandler;
 #ifdef __osf__
 #pragma pointer_size restore
 #endif
     if (mem == NULL) {
         if (hash->manager->stash != NULL) {
-        FREE(hash->manager->stash);
+        ABC_FREE(hash->manager->stash);
         hash->manager->stash = NULL;
         /* Inhibit resizing of tables. */
         hash->manager->maxCacheHard = hash->manager->cacheSlots - 1;
@@ -1395,7 +1395,7 @@ cuddHashTableAlloc(
 #pragma pointer_size save
 #pragma pointer_size short
 #endif
-        mem = (DdHashItem **) ALLOC(char,(DD_MEM_CHUNK+1) * itemsize);
+        mem = (DdHashItem **) ABC_ALLOC(char,(DD_MEM_CHUNK+1) * itemsize);
 #ifdef __osf__
 #pragma pointer_size restore
 #endif
diff --git a/src/bdd/cudd/cuddLevelQ.c b/src/bdd/cudd/cuddLevelQ.c
index 3cc8e8d8..28823a83 100644
--- a/src/bdd/cudd/cuddLevelQ.c
+++ b/src/bdd/cudd/cuddLevelQ.c
@@ -21,7 +21,7 @@
   pointers.  The level queue functions make sure that each node
   appears at most once in the queue. They do so by keeping a hash
   table where the node is used as key.  Queue items are recycled via a
-  free list for efficiency.
+  ABC_FREE list for efficiency.
   
   Internal procedures provided by this module:
                 <ul>
@@ -125,7 +125,7 @@ static int hashResize ARGS((DdLevelQueue *queue));
   Description [Initializes a level queue. A level queue is a queue
   where inserts are based on the levels of the nodes. Within each
   level the policy is FIFO. Level queues are useful in traversing a
-  BDD top-down. Queue items are kept in a free list when dequeued for
+  BDD top-down. Queue items are kept in a ABC_FREE list when dequeued for
   efficiency. Returns a pointer to the new queue if successful; NULL
   otherwise.]
 
@@ -143,7 +143,7 @@ cuddLevelQueueInit(
     DdLevelQueue *queue;
     int logSize;
 
-    queue = ALLOC(DdLevelQueue,1);
+    queue = ABC_ALLOC(DdLevelQueue,1);
     if (queue == NULL)
     return(NULL);
 #ifdef __osf__
@@ -151,12 +151,12 @@ cuddLevelQueueInit(
 #pragma pointer_size short
 #endif
     /* Keep pointers to the insertion points for all levels. */
-    queue->last = ALLOC(DdQueueItem *, levels);
+    queue->last = ABC_ALLOC(DdQueueItem *, levels);
 #ifdef __osf__
 #pragma pointer_size restore
 #endif
     if (queue->last == NULL) {
-    FREE(queue);
+    ABC_FREE(queue);
     return(NULL);
     }
     /* Use a hash table to test for uniqueness. */
@@ -168,13 +168,13 @@ cuddLevelQueueInit(
 #pragma pointer_size save
 #pragma pointer_size short
 #endif
-    queue->buckets = ALLOC(DdQueueItem *, queue->numBuckets);
+    queue->buckets = ABC_ALLOC(DdQueueItem *, queue->numBuckets);
 #ifdef __osf__
 #pragma pointer_size restore
 #endif
     if (queue->buckets == NULL) {
-    FREE(queue->last);
-    FREE(queue);
+    ABC_FREE(queue->last);
+    ABC_FREE(queue);
     return(NULL);
     }
 #ifdef __osf__
@@ -218,16 +218,16 @@ cuddLevelQueueQuit(
     while (queue->freelist != NULL) {
     item = queue->freelist;
     queue->freelist = item->next;
-    FREE(item);
+    ABC_FREE(item);
     }
     while (queue->first != NULL) {
     item = (DdQueueItem *) queue->first;
     queue->first = item->next;
-    FREE(item);
+    ABC_FREE(item);
     }
-    FREE(queue->buckets);
-    FREE(queue->last);
-    FREE(queue);
+    ABC_FREE(queue->buckets);
+    ABC_FREE(queue->last);
+    ABC_FREE(queue);
     return;
 
 } /* end of cuddLevelQueueQuit */
@@ -263,9 +263,9 @@ cuddLevelQueueEnqueue(
     item = hashLookup(queue,key);
     if (item != NULL) return(item);
 
-    /* Get a free item from either the free list or the memory manager. */
+    /* Get a ABC_FREE item from either the ABC_FREE list or the memory manager. */
     if (queue->freelist == NULL) {
-    item = (DdQueueItem *) ALLOC(char, queue->itemsize);
+    item = (DdQueueItem *) ABC_ALLOC(char, queue->itemsize);
     if (item == NULL)
         return(NULL);
     } else {
@@ -335,7 +335,7 @@ cuddLevelQueueDequeue(
     queue->last[level] = NULL;
 
     queue->first = item->next;
-    /* Put item on the free list. */
+    /* Put item on the ABC_FREE list. */
     item->next = queue->freelist;
     queue->freelist = item;
     /* Update stats. */
@@ -504,7 +504,7 @@ hashResize(
 #pragma pointer_size save
 #pragma pointer_size short
 #endif
-    buckets = queue->buckets = ALLOC(DdQueueItem *, numBuckets);
+    buckets = queue->buckets = ABC_ALLOC(DdQueueItem *, numBuckets);
     if (buckets == NULL) {
     queue->maxsize <<= 1;
     return(1);
@@ -527,7 +527,7 @@ hashResize(
         item = next;
     }
     }
-    FREE(oldBuckets);
+    ABC_FREE(oldBuckets);
     return(1);
 
 } /* end of hashResize */
diff --git a/src/bdd/cudd/cuddLinear.c b/src/bdd/cudd/cuddLinear.c
index 95624a9e..30537e6c 100644
--- a/src/bdd/cudd/cuddLinear.c
+++ b/src/bdd/cudd/cuddLinear.c
@@ -251,12 +251,12 @@ cuddLinearAndSifting(
     }
 
     /* Find order in which to sift variables. */
-    entry = ALLOC(int,size);
+    entry = ABC_ALLOC(int,size);
     if (entry == NULL) {
     table->errorCode = CUDD_MEMORY_OUT;
     goto cuddLinearAndSiftingOutOfMem;
     }
-    var = ALLOC(int,size);
+    var = ABC_ALLOC(int,size);
     if (var == NULL) {
     table->errorCode = CUDD_MEMORY_OUT;
     goto cuddLinearAndSiftingOutOfMem;
@@ -295,8 +295,8 @@ cuddLinearAndSifting(
 #endif
     }
 
-    FREE(var);
-    FREE(entry);
+    ABC_FREE(var);
+    ABC_FREE(entry);
 
 #ifdef DD_STATS
     (void) fprintf(table->out,"\n#:L_LINSIFT %8d: linear trans.",
@@ -307,8 +307,8 @@ cuddLinearAndSifting(
 
 cuddLinearAndSiftingOutOfMem:
 
-    if (entry != NULL) FREE(entry);
-    if (var != NULL) FREE(var);
+    if (entry != NULL) ABC_FREE(entry);
+    if (var != NULL) ABC_FREE(var);
 
     return(0); 
 
@@ -1220,7 +1220,7 @@ cuddInitLinear(
     nvars = table->size;
     wordsPerRow = ((nvars - 1) >> LOGBPL) + 1;
     words = wordsPerRow * nvars;
-    table->linear = linear = ALLOC(long,words);
+    table->linear = linear = ABC_ALLOC(long,words);
     if (linear == NULL) {
     table->errorCode = CUDD_MEMORY_OUT;
     return(0);
@@ -1269,7 +1269,7 @@ cuddResizeLinear(
     nvars = table->size;
     wordsPerRow = ((nvars - 1) >> LOGBPL) + 1;
     words = wordsPerRow * nvars;
-    table->linear = linear = ALLOC(long,words);
+    table->linear = linear = ABC_ALLOC(long,words);
     if (linear == NULL) {
     table->errorCode = CUDD_MEMORY_OUT;
     return(0);
@@ -1285,7 +1285,7 @@ cuddResizeLinear(
         linear[word] = oldLinear[oldWord];
     }
     }
-    FREE(oldLinear);
+    ABC_FREE(oldLinear);
 
     /* Add elements to the diagonal. */
     for (i = oldNvars; i < nvars; i++) {
diff --git a/src/bdd/cudd/cuddMatMult.c b/src/bdd/cudd/cuddMatMult.c
index 345e7921..75e5a732 100644
--- a/src/bdd/cudd/cuddMatMult.c
+++ b/src/bdd/cudd/cuddMatMult.c
@@ -110,7 +110,7 @@ Cudd_addMatrixMultiply(
 
     /* Array vars says what variables are "summation" variables. */
     nvars = dd->size;
-    vars = ALLOC(int,nvars);
+    vars = ABC_ALLOC(int,nvars);
     if (vars == NULL) {
     dd->errorCode = CUDD_MEMORY_OUT;
     return(NULL);
@@ -126,7 +126,7 @@ Cudd_addMatrixMultiply(
     dd->reordered = 0;
     res = addMMRecur(dd,A,B,-1,vars);
     } while (dd->reordered == 1);
-    FREE(vars);
+    ABC_FREE(vars);
     return(res);
 
 } /* end of Cudd_addMatrixMultiply */
@@ -220,7 +220,7 @@ Cudd_addTriangle(
     DdNode *res, *cube;
 
     nvars = dd->size;
-    vars = ALLOC(int, nvars);
+    vars = ABC_ALLOC(int, nvars);
     if (vars == NULL) {
     dd->errorCode = CUDD_MEMORY_OUT;
     return(NULL);
@@ -229,7 +229,7 @@ Cudd_addTriangle(
     for (i = 0; i < nz; i++) vars[z[i]->index] = i;
     cube = Cudd_addComputeCube(dd, z, NULL, nz);
     if (cube == NULL) {
-    FREE(vars);
+    ABC_FREE(vars);
     return(NULL);
     }
     cuddRef(cube);
@@ -241,7 +241,7 @@ Cudd_addTriangle(
     if (res != NULL) cuddRef(res);
     Cudd_RecursiveDeref(dd,cube);
     if (res != NULL) cuddDeref(res);
-    FREE(vars);
+    ABC_FREE(vars);
     return(res);
 
 } /* end of Cudd_addTriangle */
diff --git a/src/bdd/cudd/cuddPriority.c b/src/bdd/cudd/cuddPriority.c
index 2895fa0b..af07c7f0 100644
--- a/src/bdd/cudd/cuddPriority.c
+++ b/src/bdd/cudd/cuddPriority.c
@@ -157,7 +157,7 @@ Cudd_PrioritySelect(
     /* Create z variables if needed. */
     if (z == NULL) {
     if (Pi != NULL) return(NULL);
-    z = ALLOC(DdNode *,n);
+    z = ABC_ALLOC(DdNode *,n);
     if (z == NULL) {
         dd->errorCode = CUDD_MEMORY_OUT;
         return(NULL);
@@ -212,7 +212,7 @@ Cudd_PrioritySelect(
 endgame:
     if (zcube != NULL) Cudd_RecursiveDeref(dd,zcube);
     if (createdZ) {
-    FREE(z);
+    ABC_FREE(z);
     }
     if (createdPi) {
     Cudd_RecursiveDeref(dd,Pi);
diff --git a/src/bdd/cudd/cuddRead.c b/src/bdd/cudd/cuddRead.c
index 2c4a86d8..8e4ea60c 100644
--- a/src/bdd/cudd/cuddRead.c
+++ b/src/bdd/cudd/cuddRead.c
@@ -154,16 +154,16 @@ Cudd_addRead(
     for (lnx=0; u > 0; lnx++) {
     u >>= 1;
     }
-    /* Here we rely on the fact that REALLOC of a null pointer is
-    ** translates to an ALLOC.
+    /* Here we rely on the fact that ABC_REALLOC of a null pointer is
+    ** translates to an ABC_ALLOC.
     */
     if (lnx > *nx) {
-    *x = lx = REALLOC(DdNode *, *x, lnx);
+    *x = lx = ABC_REALLOC(DdNode *, *x, lnx);
     if (lx == NULL) {
         dd->errorCode = CUDD_MEMORY_OUT;
         return(0);
     }
-    *xn = lxn =  REALLOC(DdNode *, *xn, lnx);
+    *xn = lxn =  ABC_REALLOC(DdNode *, *xn, lnx);
     if (lxn == NULL) {
         dd->errorCode = CUDD_MEMORY_OUT;
         return(0);
@@ -177,16 +177,16 @@ Cudd_addRead(
     for (lny=0; v > 0; lny++) {
     v >>= 1;
     }
-    /* Here we rely on the fact that REALLOC of a null pointer is
-    ** translates to an ALLOC.
+    /* Here we rely on the fact that ABC_REALLOC of a null pointer is
+    ** translates to an ABC_ALLOC.
     */
     if (lny > *ny) {
-    *y = ly = REALLOC(DdNode *, *y, lny);
+    *y = ly = ABC_REALLOC(DdNode *, *y, lny);
     if (ly == NULL) {
         dd->errorCode = CUDD_MEMORY_OUT;
         return(0);
     }
-    *yn_ = lyn =  REALLOC(DdNode *, *yn_, lny);
+    *yn_ = lyn =  ABC_REALLOC(DdNode *, *yn_, lny);
     if (lyn == NULL) {
         dd->errorCode = CUDD_MEMORY_OUT;
         return(0);
@@ -375,7 +375,7 @@ Cudd_bddRead(
     u >>= 1;
     }
     if (lnx > *nx) {
-    *x = lx = REALLOC(DdNode *, *x, lnx);
+    *x = lx = ABC_REALLOC(DdNode *, *x, lnx);
     if (lx == NULL) {
         dd->errorCode = CUDD_MEMORY_OUT;
         return(0);
@@ -390,7 +390,7 @@ Cudd_bddRead(
     v >>= 1;
     }
     if (lny > *ny) {
-    *y = ly = REALLOC(DdNode *, *y, lny);
+    *y = ly = ABC_REALLOC(DdNode *, *y, lny);
     if (ly == NULL) {
         dd->errorCode = CUDD_MEMORY_OUT;
         return(0);
diff --git a/src/bdd/cudd/cuddRef.c b/src/bdd/cudd/cuddRef.c
index a9241f3d..7cb5d41b 100644
--- a/src/bdd/cudd/cuddRef.c
+++ b/src/bdd/cudd/cuddRef.c
@@ -312,7 +312,7 @@ Cudd_DelayedDerefBdd(
         void (*saveHandler)(long) = MMoutOfMemory;
         DdNodePtr *newRow;
         MMoutOfMemory = Cudd_OutOfMem;
-        newRow = REALLOC(DdNodePtr,table->deathRow,2*table->deathRowDepth);
+        newRow = ABC_REALLOC(DdNodePtr,table->deathRow,2*table->deathRowDepth);
         MMoutOfMemory = saveHandler;
         if (newRow == NULL) {
         table->nextDead = 0;
@@ -671,7 +671,7 @@ cuddShrinkDeathRow(
     if ((unsigned) table->nextDead > table->deadMask) {
         table->nextDead = 0;
     }
-    table->deathRow = REALLOC(DdNodePtr, table->deathRow,
+    table->deathRow = ABC_REALLOC(DdNodePtr, table->deathRow,
                    table->deathRowDepth);
     }
 #endif
diff --git a/src/bdd/cudd/cuddReorder.c b/src/bdd/cudd/cuddReorder.c
index 4e62ce34..7c2fac39 100644
--- a/src/bdd/cudd/cuddReorder.c
+++ b/src/bdd/cudd/cuddReorder.c
@@ -329,18 +329,18 @@ Cudd_ShuffleHeap(
     table->peakLiveNodes = table->keys;
     }
 
-    perm = ALLOC(int, table->size);
+    perm = ABC_ALLOC(int, table->size);
     for (i = 0; i < table->size; i++)
     perm[permutation[i]] = i;
     if (!ddCheckPermuation(table,table->tree,perm,permutation)) {
-    FREE(perm);
+    ABC_FREE(perm);
     return(0);
     }
     if (!ddUpdateMtrTree(table,table->tree,perm,permutation)) {
-    FREE(perm);
+    ABC_FREE(perm);
     return(0);
     }
-    FREE(perm);
+    ABC_FREE(perm);
 
     result = ddShuffle(table,permutation);
 
@@ -381,14 +381,14 @@ cuddDynamicAllocNode(
     extern void (*MMoutOfMemory)(long);
     void (*saveHandler)(long);
 
-    if (table->nextFree == NULL) {        /* free list is empty */
+    if (table->nextFree == NULL) {        /* ABC_FREE list is empty */
     /* Try to allocate a new block. */
     saveHandler = MMoutOfMemory;
     MMoutOfMemory = Cudd_OutOfMem;
-    mem = (DdNodePtr *) ALLOC(DdNode, DD_MEM_CHUNK + 1);
+    mem = (DdNodePtr *) ABC_ALLOC(DdNode, DD_MEM_CHUNK + 1);
     MMoutOfMemory = saveHandler;
     if (mem == NULL && table->stash != NULL) {
-        FREE(table->stash);
+        ABC_FREE(table->stash);
         table->stash = NULL;
         /* Inhibit resizing of tables. */
         table->maxCacheHard = table->cacheSlots - 1;
@@ -396,7 +396,7 @@ cuddDynamicAllocNode(
         for (i = 0; i < table->size; i++) {
         table->subtables[i].maxKeys <<= 2;
         }
-        mem = (DdNodePtr *) ALLOC(DdNode,DD_MEM_CHUNK + 1);
+        mem = (DdNodePtr *) ABC_ALLOC(DdNode,DD_MEM_CHUNK + 1);
     }
     if (mem == NULL) {
         /* Out of luck. Call the default handler to do
@@ -438,7 +438,7 @@ cuddDynamicAllocNode(
 
         table->nextFree = &list[0];
     }
-    } /* if free list empty */
+    } /* if ABC_FREE list empty */
 
     node = table->nextFree;
     table->nextFree = node->next;
@@ -485,12 +485,12 @@ cuddSifting(
 
     /* Find order in which to sift variables. */
     var = NULL;
-    entry = ALLOC(int,size);
+    entry = ABC_ALLOC(int,size);
     if (entry == NULL) {
     table->errorCode = CUDD_MEMORY_OUT;
     goto cuddSiftingOutOfMem;
     }
-    var = ALLOC(int,size);
+    var = ABC_ALLOC(int,size);
     if (var == NULL) {
     table->errorCode = CUDD_MEMORY_OUT;
     goto cuddSiftingOutOfMem;
@@ -530,15 +530,15 @@ cuddSifting(
 #endif
     }
 
-    FREE(var);
-    FREE(entry);
+    ABC_FREE(var);
+    ABC_FREE(entry);
 
     return(1);
 
 cuddSiftingOutOfMem:
 
-    if (entry != NULL) FREE(entry);
-    if (var != NULL) FREE(var);
+    if (entry != NULL) ABC_FREE(entry);
+    if (var != NULL) ABC_FREE(var);
 
     return(0); 
 
@@ -858,7 +858,7 @@ cuddSwapInPlace(
         /* Try to allocate new table. Be ready to back off. */
         saveHandler = MMoutOfMemory;
         MMoutOfMemory = Cudd_OutOfMem;
-        newxlist = ALLOC(DdNodePtr, newxslots);
+        newxlist = ABC_ALLOC(DdNodePtr, newxslots);
         MMoutOfMemory = saveHandler;
         if (newxlist == NULL) {
         (void) fprintf(table->err, "Unable to resize subtable %d for lack of memory\n", i);
@@ -873,7 +873,7 @@ cuddSwapInPlace(
             ddMin(table->maxCacheHard, DD_MAX_CACHE_TO_SLOTS_RATIO
               * table->slots) - 2 * (int) table->cacheSlots;
         table->memused += (newxslots - xslots) * sizeof(DdNodePtr);
-        FREE(xlist);
+        ABC_FREE(xlist);
         xslots =  newxslots;
         xshift = newxshift;
         xlist = newxlist;
@@ -1224,7 +1224,7 @@ cuddBddAlignToZdd(
     if (M * table->size != table->sizeZ)
     return(0);
     /* Create and initialize the inverse permutation array. */
-    invperm = ALLOC(int,table->size);
+    invperm = ABC_ALLOC(int,table->size);
     if (invperm == NULL) {
     table->errorCode = CUDD_MEMORY_OUT;
     return(0);
@@ -1250,9 +1250,9 @@ cuddBddAlignToZdd(
     if (result == 0) return(0);
 
     result = ddShuffle(table, invperm);
-    FREE(invperm);
+    ABC_FREE(invperm);
     /* Free interaction matrix. */
-    FREE(table->interact);
+    ABC_FREE(table->interact);
     /* Fix the BDD variable group tree. */
     bddFixTree(table,table->tree);
     return(result);
@@ -1827,7 +1827,7 @@ ddReorderPostprocess(
 #endif
 
     /* Free interaction matrix. */
-    FREE(table->interact);
+    ABC_FREE(table->interact);
 
     return(1);
 
diff --git a/src/bdd/cudd/cuddSat.c b/src/bdd/cudd/cuddSat.c
index 1755a1c1..a1fb79f7 100644
--- a/src/bdd/cudd/cuddSat.c
+++ b/src/bdd/cudd/cuddSat.c
@@ -933,7 +933,7 @@ freePathPair(
     cuddPathPair *pair;
 
     pair = (cuddPathPair *) value;
-    FREE(pair);
+    ABC_FREE(pair);
     return(ST_CONTINUE);
 
 } /* end of freePathPair */
@@ -1010,7 +1010,7 @@ getShortest(
     }
     }
 
-    my_pair = ALLOC(cuddPathPair, 1);
+    my_pair = ABC_ALLOC(cuddPathPair, 1);
     if (my_pair == NULL) {
     if (Cudd_IsComplement(root)) {
         int tmp = res_pair.pos;
@@ -1190,7 +1190,7 @@ getLargest(
     res_pair.neg = ddMin(pair_T.neg, pair_E.neg) + 1;
     }
 
-    my_pair = ALLOC(cuddPathPair, 1);
+    my_pair = ABC_ALLOC(cuddPathPair, 1);
     if (my_pair == NULL) {    /* simlpy do not cache this result */
     if (Cudd_IsComplement(root)) {
         int tmp = res_pair.pos;
diff --git a/src/bdd/cudd/cuddSign.c b/src/bdd/cudd/cuddSign.c
index fcaa65c4..d58c1b43 100644
--- a/src/bdd/cudd/cuddSign.c
+++ b/src/bdd/cudd/cuddSign.c
@@ -123,7 +123,7 @@ Cudd_CofMinterm(
     size = dd->size;
     values = ddCofMintermAux(dd, node, table);
     if (values != NULL) {
-    result = ALLOC(double,size + 1);
+    result = ABC_ALLOC(double,size + 1);
     if (result != NULL) {
 #ifdef DD_STATS
         table_mem += (size + 1) * sizeof(double);
@@ -148,7 +148,7 @@ Cudd_CofMinterm(
 #ifdef DD_STATS
     table_mem += table->num_bins * sizeof(st_table_entry *);
 #endif
-    if (Cudd_Regular(node)->ref == 1) FREE(values);
+    if (Cudd_Regular(node)->ref == 1) ABC_FREE(values);
     st_foreach(table, cuddStCountfree, NULL);
     st_free_table(table);
 #ifdef DD_STATS
@@ -226,7 +226,7 @@ ddCofMintermAux(
     } else {
     localSize = size - cuddI(dd,N->index) + 1;
     }
-    values = ALLOC(double, localSize);
+    values = ABC_ALLOC(double, localSize);
     if (values == NULL) {
     dd->errorCode = CUDD_MEMORY_OUT;
     return(NULL);
@@ -273,13 +273,13 @@ ddCofMintermAux(
         }
         values[i] = (vT + vE) / 2.0;
     }
-    if (Cudd_Regular(Nv)->ref == 1) FREE(valuesT);
-    if (Cudd_Regular(Nnv)->ref == 1) FREE(valuesE);
+    if (Cudd_Regular(Nv)->ref == 1) ABC_FREE(valuesT);
+    if (Cudd_Regular(Nnv)->ref == 1) ABC_FREE(valuesE);
     }
 
     if (N->ref > 1) {
     if (st_add_direct(table, (char *) node, (char *) values) == ST_OUT_OF_MEM) {
-        FREE(values);
+        ABC_FREE(values);
         return(NULL);
     }
 #ifdef DD_STATS
diff --git a/src/bdd/cudd/cuddSolve.c b/src/bdd/cudd/cuddSolve.c
index d9c4a2e7..a78055f3 100644
--- a/src/bdd/cudd/cuddSolve.c
+++ b/src/bdd/cudd/cuddSolve.c
@@ -103,7 +103,7 @@ Cudd_SolveEqn(
     DdNode *res;
     int *temp;
 
-    *yIndex = temp = ALLOC(int, n);
+    *yIndex = temp = ABC_ALLOC(int, n);
     if (temp == NULL) {
     bdd->errorCode = CUDD_MEMORY_OUT;
     (void) fprintf(bdd->out,
@@ -149,7 +149,7 @@ Cudd_VerifySol(
     res = cuddVerifySol(bdd, F, G, yIndex, n);
     } while (bdd->reordered == 1);
 
-    FREE(yIndex);
+    ABC_FREE(yIndex);
 
     return(res);
 
diff --git a/src/bdd/cudd/cuddSplit.c b/src/bdd/cudd/cuddSplit.c
index e21ea7cb..1f9a0425 100644
--- a/src/bdd/cudd/cuddSplit.c
+++ b/src/bdd/cudd/cuddSplit.c
@@ -129,7 +129,7 @@ Cudd_SplitSet(
     /* varSeen is used to mark the variables that are encountered
     ** while traversing the BDD S.
     */
-    varSeen = ALLOC(int, size);
+    varSeen = ABC_ALLOC(int, size);
     if (varSeen == NULL) {
         manager->errorCode = CUDD_MEMORY_OUT;
         return(NULL);
@@ -148,13 +148,13 @@ Cudd_SplitSet(
         result = selectMintermsFromUniverse(manager,varSeen,m);
         if (result)
         cuddRef(result);
-        FREE(varSeen);
+        ABC_FREE(varSeen);
     } else {
         mtable = st_init_table(st_ptrcmp,st_ptrhash);
         if (mtable == NULL) {
         (void) fprintf(manager->out,
                    "Cudd_SplitSet: out-of-memory.\n");
-        FREE(varSeen);
+        ABC_FREE(varSeen);
         manager->errorCode = CUDD_MEMORY_OUT;
         return(NULL);
         }
@@ -166,7 +166,7 @@ Cudd_SplitSet(
         if (m == num) {
         st_foreach(mtable,cuddStCountfree,NIL(char));
         st_free_table(mtable);
-        FREE(varSeen);
+        ABC_FREE(varSeen);
         return(S);
         }
         
@@ -175,7 +175,7 @@ Cudd_SplitSet(
         cuddRef(result);
         st_foreach(mtable,cuddStCountfree,NULL);
         st_free_table(mtable);
-        FREE(varSeen);
+        ABC_FREE(varSeen);
     }
     } while (manager->reordered == 1);
 
@@ -485,7 +485,7 @@ selectMintermsFromUniverse(
     if(varSeen[i] == 0)
         numVars++;
     }
-    vars = ALLOC(DdNode *, numVars);
+    vars = ABC_ALLOC(DdNode *, numVars);
     if (!vars) {
     manager->errorCode = CUDD_MEMORY_OUT;
     return(NULL);
@@ -509,7 +509,7 @@ selectMintermsFromUniverse(
 
     for (i = 0; i < numVars; i++)
     Cudd_RecursiveDeref(manager,vars[i]);
-    FREE(vars);
+    ABC_FREE(vars);
 
     return(result);
 
@@ -640,7 +640,7 @@ bddAnnotateMintermCount(
     return ((double)CUDD_OUT_OF_MEM);
     min_N  = min_v + min_nv;
 
-    pmin = ALLOC(double,1);
+    pmin = ABC_ALLOC(double,1);
     if (pmin == NULL) {
     manager->errorCode = CUDD_MEMORY_OUT;
     return((double)CUDD_OUT_OF_MEM);
@@ -648,7 +648,7 @@ bddAnnotateMintermCount(
     *pmin = min_N;
 
     if (st_insert(table,(char *)node, (char *)pmin) == ST_OUT_OF_MEM) {
-    FREE(pmin);
+    ABC_FREE(pmin);
     return((double)CUDD_OUT_OF_MEM);
     }
     
diff --git a/src/bdd/cudd/cuddSubsetHB.c b/src/bdd/cudd/cuddSubsetHB.c
index 24d41ce5..59f8e6d2 100644
--- a/src/bdd/cudd/cuddSubsetHB.c
+++ b/src/bdd/cudd/cuddSubsetHB.c
@@ -336,7 +336,7 @@ cuddSubsetHeavyBranch(
     dd->errorCode = CUDD_INTERNAL_ERROR;
     }
 
-    size = ALLOC(int, 1);
+    size = ABC_ALLOC(int, 1);
     if (size == NULL) {
     dd->errorCode = CUDD_MEMORY_OUT;
     return(NULL);
@@ -385,23 +385,23 @@ cuddSubsetHeavyBranch(
     st_free_table(storeTable);
 
     for (i = 0; i <= page; i++) {
-    FREE(mintermPages[i]);
+    ABC_FREE(mintermPages[i]);
     }
-    FREE(mintermPages);
+    ABC_FREE(mintermPages);
     for (i = 0; i <= page; i++) {
-    FREE(nodePages[i]);
+    ABC_FREE(nodePages[i]);
     }
-    FREE(nodePages);
+    ABC_FREE(nodePages);
     for (i = 0; i <= page; i++) {
-    FREE(lightNodePages[i]);
+    ABC_FREE(lightNodePages[i]);
     }
-    FREE(lightNodePages);
+    ABC_FREE(lightNodePages);
     for (i = 0; i <= nodeDataPage; i++) {
-    FREE(nodeDataPages[i]);
+    ABC_FREE(nodeDataPages[i]);
     }
-    FREE(nodeDataPages);
+    ABC_FREE(nodeDataPages);
     st_free_table(visitedTable);
-    FREE(size);
+    ABC_FREE(size);
 #if 0
     (void) Cudd_DebugCheck(dd);
     (void) Cudd_CheckKeys(dd);
@@ -455,10 +455,10 @@ ResizeNodeDataPages(
      * INITIAL_PAGES
      */
     if (nodeDataPage == maxNodeDataPages) {
-    newNodeDataPages = ALLOC(NodeData_t *,maxNodeDataPages + INITIAL_PAGES);
+    newNodeDataPages = ABC_ALLOC(NodeData_t *,maxNodeDataPages + INITIAL_PAGES);
     if (newNodeDataPages == NULL) {
-        for (i = 0; i < nodeDataPage; i++) FREE(nodeDataPages[i]);
-        FREE(nodeDataPages);
+        for (i = 0; i < nodeDataPage; i++) ABC_FREE(nodeDataPages[i]);
+        ABC_FREE(nodeDataPages);
         memOut = 1;
         return;
     } else {
@@ -467,16 +467,16 @@ ResizeNodeDataPages(
         }
         /* Increase total page count */
         maxNodeDataPages += INITIAL_PAGES;
-        FREE(nodeDataPages);
+        ABC_FREE(nodeDataPages);
         nodeDataPages = newNodeDataPages;
     }
     }
     /* Allocate a new page */
     currentNodeDataPage = nodeDataPages[nodeDataPage] =
-    ALLOC(NodeData_t ,nodeDataPageSize);
+    ABC_ALLOC(NodeData_t ,nodeDataPageSize);
     if (currentNodeDataPage == NULL) {
-    for (i = 0; i < nodeDataPage; i++) FREE(nodeDataPages[i]);
-    FREE(nodeDataPages);
+    for (i = 0; i < nodeDataPage; i++) ABC_FREE(nodeDataPages[i]);
+    ABC_FREE(nodeDataPages);
     memOut = 1;
     return;
     }
@@ -515,10 +515,10 @@ ResizeCountMintermPages(
      * INITIAL_PAGES
      */
     if (page == maxPages) {
-    newMintermPages = ALLOC(double *,maxPages + INITIAL_PAGES);
+    newMintermPages = ABC_ALLOC(double *,maxPages + INITIAL_PAGES);
     if (newMintermPages == NULL) {
-        for (i = 0; i < page; i++) FREE(mintermPages[i]);
-        FREE(mintermPages);
+        for (i = 0; i < page; i++) ABC_FREE(mintermPages[i]);
+        ABC_FREE(mintermPages);
         memOut = 1;
         return;
     } else {
@@ -527,15 +527,15 @@ ResizeCountMintermPages(
         }
         /* Increase total page count */
         maxPages += INITIAL_PAGES;
-        FREE(mintermPages);
+        ABC_FREE(mintermPages);
         mintermPages = newMintermPages;
     }
     }
     /* Allocate a new page */
-    currentMintermPage = mintermPages[page] = ALLOC(double,pageSize);
+    currentMintermPage = mintermPages[page] = ABC_ALLOC(double,pageSize);
     if (currentMintermPage == NULL) {
-    for (i = 0; i < page; i++) FREE(mintermPages[i]);
-    FREE(mintermPages);
+    for (i = 0; i < page; i++) ABC_FREE(mintermPages[i]);
+    ABC_FREE(mintermPages);
     memOut = 1;
     return;
     }
@@ -574,57 +574,57 @@ ResizeCountNodePages(
      * by INITIAL_PAGES.
      */
     if (page == maxPages) {
-    newNodePages = ALLOC(int *,maxPages + INITIAL_PAGES);
+    newNodePages = ABC_ALLOC(int *,maxPages + INITIAL_PAGES);
     if (newNodePages == NULL) {
-        for (i = 0; i < page; i++) FREE(nodePages[i]);
-        FREE(nodePages);
-        for (i = 0; i < page; i++) FREE(lightNodePages[i]);
-        FREE(lightNodePages);
+        for (i = 0; i < page; i++) ABC_FREE(nodePages[i]);
+        ABC_FREE(nodePages);
+        for (i = 0; i < page; i++) ABC_FREE(lightNodePages[i]);
+        ABC_FREE(lightNodePages);
         memOut = 1;
         return;
     } else {
         for (i = 0; i < maxPages; i++) {
         newNodePages[i] = nodePages[i];
         }
-        FREE(nodePages);
+        ABC_FREE(nodePages);
         nodePages = newNodePages;
     }
 
-    newNodePages = ALLOC(int *,maxPages + INITIAL_PAGES);
+    newNodePages = ABC_ALLOC(int *,maxPages + INITIAL_PAGES);
     if (newNodePages == NULL) {
-        for (i = 0; i < page; i++) FREE(nodePages[i]);
-        FREE(nodePages);
-        for (i = 0; i < page; i++) FREE(lightNodePages[i]);
-        FREE(lightNodePages);
+        for (i = 0; i < page; i++) ABC_FREE(nodePages[i]);
+        ABC_FREE(nodePages);
+        for (i = 0; i < page; i++) ABC_FREE(lightNodePages[i]);
+        ABC_FREE(lightNodePages);
         memOut = 1;
         return;
     } else {
         for (i = 0; i < maxPages; i++) {
         newNodePages[i] = lightNodePages[i];
         }
-        FREE(lightNodePages);
+        ABC_FREE(lightNodePages);
         lightNodePages = newNodePages;
     }
     /* Increase total page count */
     maxPages += INITIAL_PAGES;
     }
     /* Allocate a new page */
-    currentNodePage = nodePages[page] = ALLOC(int,pageSize);
+    currentNodePage = nodePages[page] = ABC_ALLOC(int,pageSize);
     if (currentNodePage == NULL) {
-    for (i = 0; i < page; i++) FREE(nodePages[i]);
-    FREE(nodePages);
-    for (i = 0; i < page; i++) FREE(lightNodePages[i]);
-    FREE(lightNodePages);
+    for (i = 0; i < page; i++) ABC_FREE(nodePages[i]);
+    ABC_FREE(nodePages);
+    for (i = 0; i < page; i++) ABC_FREE(lightNodePages[i]);
+    ABC_FREE(lightNodePages);
     memOut = 1;
     return;
     }
     /* Allocate a new page */
-    currentLightNodePage = lightNodePages[page] = ALLOC(int,pageSize);
+    currentLightNodePage = lightNodePages[page] = ABC_ALLOC(int,pageSize);
     if (currentLightNodePage == NULL) {
-    for (i = 0; i <= page; i++) FREE(nodePages[i]);
-    FREE(nodePages);
-    for (i = 0; i < page; i++) FREE(lightNodePages[i]);
-    FREE(lightNodePages);
+    for (i = 0; i <= page; i++) ABC_FREE(nodePages[i]);
+    ABC_FREE(nodePages);
+    for (i = 0; i < page; i++) ABC_FREE(lightNodePages[i]);
+    ABC_FREE(lightNodePages);
     memOut = 1;
     return;
     }
@@ -703,8 +703,8 @@ SubsetCountMintermAux(
     /* if page index is at the bottom, then create a new page */
     if (pageIndex == pageSize) ResizeCountMintermPages();
     if (memOut) {
-        for (i = 0; i <= nodeDataPage; i++) FREE(nodeDataPages[i]);
-        FREE(nodeDataPages);
+        for (i = 0; i <= nodeDataPage; i++) ABC_FREE(nodeDataPages[i]);
+        ABC_FREE(nodeDataPages);
         st_free_table(table);
         return(0.0);
     }
@@ -719,8 +719,8 @@ SubsetCountMintermAux(
     /* Note I allocate the struct here. Freeing taken care of later */
     if (nodeDataPageIndex == nodeDataPageSize) ResizeNodeDataPages();
     if (memOut) {
-        for (i = 0; i <= page; i++) FREE(mintermPages[i]);
-        FREE(mintermPages);
+        for (i = 0; i <= page; i++) ABC_FREE(mintermPages[i]);
+        ABC_FREE(mintermPages);
         st_free_table(table);
         return(0.0);
     }
@@ -736,10 +736,10 @@ SubsetCountMintermAux(
     /* insert entry for the node in the table */
     if (st_insert(table,(char *)node, (char *)newEntry) == ST_OUT_OF_MEM) {
         memOut = 1;
-        for (i = 0; i <= page; i++) FREE(mintermPages[i]);
-        FREE(mintermPages);
-        for (i = 0; i <= nodeDataPage; i++) FREE(nodeDataPages[i]);
-        FREE(nodeDataPages);
+        for (i = 0; i <= page; i++) ABC_FREE(mintermPages[i]);
+        ABC_FREE(mintermPages);
+        for (i = 0; i <= nodeDataPage; i++) ABC_FREE(nodeDataPages[i]);
+        ABC_FREE(nodeDataPages);
         st_free_table(table);
         return(0.0);
     }
@@ -780,35 +780,35 @@ SubsetCountMinterm(
     table = st_init_table(st_ptrcmp,st_ptrhash);
     if (table == NULL) goto OUT_OF_MEM;
     maxPages = INITIAL_PAGES;
-    mintermPages = ALLOC(double *,maxPages);
+    mintermPages = ABC_ALLOC(double *,maxPages);
     if (mintermPages == NULL) {
     st_free_table(table);
     goto OUT_OF_MEM;
     }
     page = 0;
-    currentMintermPage = ALLOC(double,pageSize);
+    currentMintermPage = ABC_ALLOC(double,pageSize);
     mintermPages[page] = currentMintermPage;
     if (currentMintermPage == NULL) {
-    FREE(mintermPages);
+    ABC_FREE(mintermPages);
     st_free_table(table);
     goto OUT_OF_MEM;
     }
     pageIndex = 0;
     maxNodeDataPages = INITIAL_PAGES;
-    nodeDataPages = ALLOC(NodeData_t *, maxNodeDataPages);
+    nodeDataPages = ABC_ALLOC(NodeData_t *, maxNodeDataPages);
     if (nodeDataPages == NULL) {
-    for (i = 0; i <= page ; i++) FREE(mintermPages[i]);
-    FREE(mintermPages);
+    for (i = 0; i <= page ; i++) ABC_FREE(mintermPages[i]);
+    ABC_FREE(mintermPages);
     st_free_table(table);
     goto OUT_OF_MEM;
     }
     nodeDataPage = 0;
-    currentNodeDataPage = ALLOC(NodeData_t ,nodeDataPageSize);
+    currentNodeDataPage = ABC_ALLOC(NodeData_t ,nodeDataPageSize);
     nodeDataPages[nodeDataPage] = currentNodeDataPage;
     if (currentNodeDataPage == NULL) {
-    for (i = 0; i <= page ; i++) FREE(mintermPages[i]);
-    FREE(mintermPages);
-    FREE(nodeDataPages);
+    for (i = 0; i <= page ; i++) ABC_FREE(mintermPages[i]);
+    ABC_FREE(mintermPages);
+    ABC_FREE(nodeDataPages);
     st_free_table(table);
     goto OUT_OF_MEM;
     }
@@ -915,10 +915,10 @@ SubsetCountNodesAux(
     /* store the node count of the lighter child. */
     if (pageIndex == pageSize) ResizeCountNodePages();
     if (memOut) {
-        for (i = 0; i <= page; i++) FREE(mintermPages[i]);
-        FREE(mintermPages);
-        for (i = 0; i <= nodeDataPage; i++) FREE(nodeDataPages[i]);
-        FREE(nodeDataPages);
+        for (i = 0; i <= page; i++) ABC_FREE(mintermPages[i]);
+        ABC_FREE(mintermPages);
+        for (i = 0; i <= nodeDataPage; i++) ABC_FREE(nodeDataPages[i]);
+        ABC_FREE(nodeDataPages);
         st_free_table(table);
         return(0);
     }
@@ -935,10 +935,10 @@ SubsetCountNodesAux(
     /* store the node count of the lighter child. */
     if (pageIndex == pageSize) ResizeCountNodePages();
     if (memOut) {
-        for (i = 0; i <= page; i++) FREE(mintermPages[i]);
-        FREE(mintermPages);
-        for (i = 0; i <= nodeDataPage; i++) FREE(nodeDataPages[i]);
-        FREE(nodeDataPages);
+        for (i = 0; i <= page; i++) ABC_FREE(mintermPages[i]);
+        ABC_FREE(mintermPages);
+        for (i = 0; i <= nodeDataPage; i++) ABC_FREE(nodeDataPages[i]);
+        ABC_FREE(nodeDataPages);
         st_free_table(table);
         return(0);
     }
@@ -962,10 +962,10 @@ SubsetCountNodesAux(
     if (st_lookup(table, (char *)Cudd_Not(node), (char **)&dummyNBar) == 1)  {
     if (pageIndex == pageSize) ResizeCountNodePages();
     if (memOut) {
-        for (i = 0; i < page; i++) FREE(mintermPages[i]);
-        FREE(mintermPages);
-        for (i = 0; i < nodeDataPage; i++) FREE(nodeDataPages[i]);
-        FREE(nodeDataPages);
+        for (i = 0; i < page; i++) ABC_FREE(mintermPages[i]);
+        ABC_FREE(mintermPages);
+        for (i = 0; i < nodeDataPage; i++) ABC_FREE(nodeDataPages[i]);
+        ABC_FREE(nodeDataPages);
         st_free_table(table);
         return(0);
     }
@@ -977,10 +977,10 @@ SubsetCountNodesAux(
      */
     if (pageIndex == pageSize) ResizeCountNodePages();
     if (memOut) {
-        for (i = 0; i < page; i++) FREE(mintermPages[i]);
-        FREE(mintermPages);
-        for (i = 0; i < nodeDataPage; i++) FREE(nodeDataPages[i]);
-        FREE(nodeDataPages);
+        for (i = 0; i < page; i++) ABC_FREE(mintermPages[i]);
+        ABC_FREE(mintermPages);
+        for (i = 0; i < nodeDataPage; i++) ABC_FREE(nodeDataPages[i]);
+        ABC_FREE(nodeDataPages);
         st_free_table(table);
         return(0);
     }
@@ -1023,42 +1023,42 @@ SubsetCountNodes(
 
     max = pow(2.0,(double) nvars);
     maxPages = INITIAL_PAGES;
-    nodePages = ALLOC(int *,maxPages);
+    nodePages = ABC_ALLOC(int *,maxPages);
     if (nodePages == NULL)  {
     goto OUT_OF_MEM;
     }
 
-    lightNodePages = ALLOC(int *,maxPages);
+    lightNodePages = ABC_ALLOC(int *,maxPages);
     if (lightNodePages == NULL) {
-    for (i = 0; i <= page; i++) FREE(mintermPages[i]);
-    FREE(mintermPages);
-    for (i = 0; i <= nodeDataPage; i++) FREE(nodeDataPages[i]);
-    FREE(nodeDataPages);
-    FREE(nodePages);
+    for (i = 0; i <= page; i++) ABC_FREE(mintermPages[i]);
+    ABC_FREE(mintermPages);
+    for (i = 0; i <= nodeDataPage; i++) ABC_FREE(nodeDataPages[i]);
+    ABC_FREE(nodeDataPages);
+    ABC_FREE(nodePages);
     goto OUT_OF_MEM;
     }
 
     page = 0;
-    currentNodePage = nodePages[page] = ALLOC(int,pageSize);
+    currentNodePage = nodePages[page] = ABC_ALLOC(int,pageSize);
     if (currentNodePage == NULL) {
-    for (i = 0; i <= page; i++) FREE(mintermPages[i]);
-    FREE(mintermPages);
-    for (i = 0; i <= nodeDataPage; i++) FREE(nodeDataPages[i]);
-    FREE(nodeDataPages);
-    FREE(lightNodePages);
-    FREE(nodePages);
+    for (i = 0; i <= page; i++) ABC_FREE(mintermPages[i]);
+    ABC_FREE(mintermPages);
+    for (i = 0; i <= nodeDataPage; i++) ABC_FREE(nodeDataPages[i]);
+    ABC_FREE(nodeDataPages);
+    ABC_FREE(lightNodePages);
+    ABC_FREE(nodePages);
     goto OUT_OF_MEM;
     }
 
-    currentLightNodePage = lightNodePages[page] = ALLOC(int,pageSize);
+    currentLightNodePage = lightNodePages[page] = ABC_ALLOC(int,pageSize);
     if (currentLightNodePage == NULL) {
-    for (i = 0; i <= page; i++) FREE(mintermPages[i]);
-    FREE(mintermPages);
-    for (i = 0; i <= nodeDataPage; i++) FREE(nodeDataPages[i]);
-    FREE(nodeDataPages);
-    FREE(currentNodePage);
-    FREE(lightNodePages);
-    FREE(nodePages);
+    for (i = 0; i <= page; i++) ABC_FREE(mintermPages[i]);
+    ABC_FREE(mintermPages);
+    for (i = 0; i <= nodeDataPage; i++) ABC_FREE(nodeDataPages[i]);
+    ABC_FREE(nodeDataPages);
+    ABC_FREE(currentNodePage);
+    ABC_FREE(lightNodePages);
+    ABC_FREE(nodePages);
     goto OUT_OF_MEM;
     }
 
diff --git a/src/bdd/cudd/cuddSubsetSP.c b/src/bdd/cudd/cuddSubsetSP.c
index e3d39a0e..25c22b88 100644
--- a/src/bdd/cudd/cuddSubsetSP.c
+++ b/src/bdd/cudd/cuddSubsetSP.c
@@ -311,7 +311,7 @@ cuddSubsetShortPaths(
     if (Cudd_IsConstant(f))
     return (f);
 
-    pathLengthArray = ALLOC(unsigned int, numVars+1);
+    pathLengthArray = ABC_ALLOC(unsigned int, numVars+1);
     for (i = 0; i < numVars+1; i++) pathLengthArray[i] = 0;
 
 
@@ -324,18 +324,18 @@ cuddSubsetShortPaths(
     if ((pathTable == NULL) || (memOut)) {
     if (pathTable != NULL)
         st_free_table(pathTable);
-    FREE(pathLengthArray);
+    ABC_FREE(pathLengthArray);
     return (NIL(DdNode));
     }
 
-    excess = ALLOC(unsigned int, 1);
+    excess = ABC_ALLOC(unsigned int, 1);
     *excess = 0;
     maxpath = AssessPathLength(pathLengthArray, threshold, numVars, excess,
                    dd->err);
 
     if (maxpath != (unsigned) (numVars + 1)) {
 
-    info = ALLOC(struct AssortedInfo, 1);
+    info = ABC_ALLOC(struct AssortedInfo, 1);
     info->maxpath = maxpath;
     info->findShortestPath = 0;
     info->thresholdReached = *excess;
@@ -412,17 +412,17 @@ cuddSubsetShortPaths(
     st_free_table(info->maxpathTable);
     st_foreach(pathTable, stPathTableDdFree, (char *)dd);
 
-    FREE(info);
+    ABC_FREE(info);
 
     } else {/* if threshold larger than size of dd */
     subset = f;
     cuddRef(subset);
     }
-    FREE(excess);
+    ABC_FREE(excess);
     st_free_table(pathTable);
-    FREE(pathLengthArray);
-    for (i = 0; i <= nodeDistPage; i++) FREE(nodeDistPages[i]);
-    FREE(nodeDistPages);
+    ABC_FREE(pathLengthArray);
+    for (i = 0; i <= nodeDistPage; i++) ABC_FREE(nodeDistPages[i]);
+    ABC_FREE(nodeDistPages);
 
 #ifdef DD_DEBUG
     /* check containment of subset in f */
@@ -483,10 +483,10 @@ ResizeNodeDistPages(
      * INITIAL_PAGES
      */
     if (nodeDistPage == maxNodeDistPages) {
-    newNodeDistPages = ALLOC(NodeDist_t *,maxNodeDistPages + INITIAL_PAGES);
+    newNodeDistPages = ABC_ALLOC(NodeDist_t *,maxNodeDistPages + INITIAL_PAGES);
     if (newNodeDistPages == NULL) {
-        for (i = 0; i < nodeDistPage; i++) FREE(nodeDistPages[i]);
-        FREE(nodeDistPages);
+        for (i = 0; i < nodeDistPage; i++) ABC_FREE(nodeDistPages[i]);
+        ABC_FREE(nodeDistPages);
         memOut = 1;
         return;
     } else {
@@ -495,16 +495,16 @@ ResizeNodeDistPages(
         }
         /* Increase total page count */
         maxNodeDistPages += INITIAL_PAGES;
-        FREE(nodeDistPages);
+        ABC_FREE(nodeDistPages);
         nodeDistPages = newNodeDistPages;
     }
     }
     /* Allocate a new page */
-    currentNodeDistPage = nodeDistPages[nodeDistPage] = ALLOC(NodeDist_t,
+    currentNodeDistPage = nodeDistPages[nodeDistPage] = ABC_ALLOC(NodeDist_t,
                                   nodeDistPageSize);
     if (currentNodeDistPage == NULL) {
-    for (i = 0; i < nodeDistPage; i++) FREE(nodeDistPages[i]);
-    FREE(nodeDistPages);
+    for (i = 0; i < nodeDistPage; i++) ABC_FREE(nodeDistPages[i]);
+    ABC_FREE(nodeDistPages);
     memOut = 1;
     return;
     }
@@ -544,10 +544,10 @@ ResizeQueuePages(
      * INITIAL_PAGES
      */
     if (queuePage == maxQueuePages) {
-    newQueuePages = ALLOC(DdNode **,maxQueuePages + INITIAL_PAGES);
+    newQueuePages = ABC_ALLOC(DdNode **,maxQueuePages + INITIAL_PAGES);
     if (newQueuePages == NULL) {
-        for (i = 0; i < queuePage; i++) FREE(queuePages[i]);
-        FREE(queuePages);
+        for (i = 0; i < queuePage; i++) ABC_FREE(queuePages[i]);
+        ABC_FREE(queuePages);
         memOut = 1;
         return;
     } else {
@@ -556,15 +556,15 @@ ResizeQueuePages(
         }
         /* Increase total page count */
         maxQueuePages += INITIAL_PAGES;
-        FREE(queuePages);
+        ABC_FREE(queuePages);
         queuePages = newQueuePages;
     }
     }
     /* Allocate a new page */
-    currentQueuePage = queuePages[queuePage] = ALLOC(DdNode *,queuePageSize);
+    currentQueuePage = queuePages[queuePage] = ABC_ALLOC(DdNode *,queuePageSize);
     if (currentQueuePage == NULL) {
-    for (i = 0; i < queuePage; i++) FREE(queuePages[i]);
-    FREE(queuePages);
+    for (i = 0; i < queuePage; i++) ABC_FREE(queuePages[i]);
+    ABC_FREE(queuePages);
     memOut = 1;
     return;
     }
@@ -667,8 +667,8 @@ CreateTopDist(
             if (nodeDistPageIndex == nodeDistPageSize)
             ResizeNodeDistPages();
             if (memOut) {
-            for (i = 0; i <= queuePage; i++) FREE(queuePages[i]);
-            FREE(queuePages);
+            for (i = 0; i <= queuePage; i++) ABC_FREE(queuePages[i]);
+            ABC_FREE(queuePages);
             st_free_table(pathTable);
             return;
             }
@@ -697,10 +697,10 @@ CreateTopDist(
                   (char *)nodeStat) == ST_OUT_OF_MEM) {
             memOut = 1;
             for (i = 0; i <= nodeDistPage; i++)
-                FREE(nodeDistPages[i]);
-            FREE(nodeDistPages);
-            for (i = 0; i <= queuePage; i++) FREE(queuePages[i]);
-            FREE(queuePages);
+                ABC_FREE(nodeDistPages[i]);
+            ABC_FREE(nodeDistPages);
+            for (i = 0; i <= queuePage; i++) ABC_FREE(queuePages[i]);
+            ABC_FREE(queuePages);
             st_free_table(pathTable);
             return;
             }
@@ -714,8 +714,8 @@ CreateTopDist(
             if (queuePageIndex == queuePageSize) ResizeQueuePages();
             if (memOut) {
             for (i = 0; i <= nodeDistPage; i++)
-                FREE(nodeDistPages[i]);
-            FREE(nodeDistPages);
+                ABC_FREE(nodeDistPages[i]);
+            ABC_FREE(nodeDistPages);
             st_free_table(pathTable);
             return;
             }
@@ -733,8 +733,8 @@ CreateTopDist(
             if (queuePageIndex == queuePageSize) ResizeQueuePages();
             if (memOut) {
                 for (i = 0; i <= nodeDistPage; i++)
-                FREE(nodeDistPages[i]);
-                FREE(nodeDistPages);
+                ABC_FREE(nodeDistPages[i]);
+                ABC_FREE(nodeDistPages);
                 st_free_table(pathTable);
                 return;
 
@@ -1000,31 +1000,31 @@ CreatePathTable(
 
     /* initializing pages for info about each node */
     maxNodeDistPages = INITIAL_PAGES;
-    nodeDistPages = ALLOC(NodeDist_t *, maxNodeDistPages);
+    nodeDistPages = ABC_ALLOC(NodeDist_t *, maxNodeDistPages);
     if (nodeDistPages == NULL) {
     goto OUT_OF_MEM;
     }
     nodeDistPage = 0;
     currentNodeDistPage = nodeDistPages[nodeDistPage] =
-    ALLOC(NodeDist_t, nodeDistPageSize);
+    ABC_ALLOC(NodeDist_t, nodeDistPageSize);
     if (currentNodeDistPage == NULL) {
-    for (i = 0; i <= nodeDistPage; i++) FREE(nodeDistPages[i]);
-    FREE(nodeDistPages);
+    for (i = 0; i <= nodeDistPage; i++) ABC_FREE(nodeDistPages[i]);
+    ABC_FREE(nodeDistPages);
     goto OUT_OF_MEM;
     }
     nodeDistPageIndex = 0;
 
     /* Initializing pages for the BFS search queue, implemented as an array. */
     maxQueuePages = INITIAL_PAGES;
-    queuePages = ALLOC(DdNode **, maxQueuePages);
+    queuePages = ABC_ALLOC(DdNode **, maxQueuePages);
     if (queuePages == NULL) {
     goto OUT_OF_MEM;
     }
     queuePage = 0;
-    currentQueuePage  = queuePages[queuePage] = ALLOC(DdNode *, queuePageSize);
+    currentQueuePage  = queuePages[queuePage] = ABC_ALLOC(DdNode *, queuePageSize);
     if (currentQueuePage == NULL) {
-    for (i = 0; i <= queuePage; i++) FREE(queuePages[i]);
-    FREE(queuePages);
+    for (i = 0; i <= queuePage; i++) ABC_FREE(queuePages[i]);
+    ABC_FREE(queuePages);
     goto OUT_OF_MEM;
     }
     queuePageIndex = 0;
@@ -1042,10 +1042,10 @@ CreatePathTable(
 
     if (nodeDistPageIndex == nodeDistPageSize) ResizeNodeDistPages();
     if (memOut) {
-    for (i = 0; i <= nodeDistPage; i++) FREE(nodeDistPages[i]);
-    FREE(nodeDistPages);
-    for (i = 0; i <= queuePage; i++) FREE(queuePages[i]);
-    FREE(queuePages);
+    for (i = 0; i <= nodeDistPage; i++) ABC_FREE(nodeDistPages[i]);
+    ABC_FREE(nodeDistPages);
+    for (i = 0; i <= queuePage; i++) ABC_FREE(queuePages[i]);
+    ABC_FREE(queuePages);
     st_free_table(pathTable);
     goto OUT_OF_MEM;
     }
@@ -1063,10 +1063,10 @@ CreatePathTable(
     insertValue = st_insert(pathTable, (char *)N, (char *)nodeStat);
     if (insertValue == ST_OUT_OF_MEM) {
     memOut = 1;
-    for (i = 0; i <= nodeDistPage; i++) FREE(nodeDistPages[i]);
-    FREE(nodeDistPages);
-    for (i = 0; i <= queuePage; i++) FREE(queuePages[i]);
-    FREE(queuePages);
+    for (i = 0; i <= nodeDistPage; i++) ABC_FREE(nodeDistPages[i]);
+    ABC_FREE(nodeDistPages);
+    for (i = 0; i <= queuePage; i++) ABC_FREE(queuePages[i]);
+    ABC_FREE(queuePages);
     st_free_table(pathTable);
     goto OUT_OF_MEM;
     } else if (insertValue == 1) {
@@ -1101,9 +1101,9 @@ CreatePathTable(
      */
     if (!CreateBotDist(node, pathTable, pathLengthArray, fp)) return(NULL);
 
-    /* free BFS queue pages as no longer required */
-    for (i = 0; i <= queuePage; i++) FREE(queuePages[i]);
-    FREE(queuePages);
+    /* ABC_FREE BFS queue pages as no longer required */
+    for (i = 0; i <= queuePage; i++) ABC_FREE(queuePages[i]);
+    ABC_FREE(queuePages);
     return(pathTable);
 
 OUT_OF_MEM:
@@ -1595,7 +1595,7 @@ BuildSubsetBdd(
 
 /**Function********************************************************************
 
-  Synopsis     [Procedure to free te result dds stored in the NodeDist pages.]
+  Synopsis     [Procedure to ABC_FREE te result dds stored in the NodeDist pages.]
 
   Description [None]
 
diff --git a/src/bdd/cudd/cuddSymmetry.c b/src/bdd/cudd/cuddSymmetry.c
index aef6abc6..a608a21f 100644
--- a/src/bdd/cudd/cuddSymmetry.c
+++ b/src/bdd/cudd/cuddSymmetry.c
@@ -308,12 +308,12 @@ cuddSymmSifting(
 
     /* Find order in which to sift variables. */
     var = NULL;
-    entry = ALLOC(int,size);
+    entry = ABC_ALLOC(int,size);
     if (entry == NULL) {
     table->errorCode = CUDD_MEMORY_OUT;
     goto ddSymmSiftingOutOfMem;
     }
-    var = ALLOC(int,size);
+    var = ABC_ALLOC(int,size);
     if (var == NULL) {
     table->errorCode = CUDD_MEMORY_OUT;
     goto ddSymmSiftingOutOfMem;
@@ -357,8 +357,8 @@ cuddSymmSifting(
     }
     }
 
-    FREE(var);
-    FREE(entry);
+    ABC_FREE(var);
+    ABC_FREE(entry);
 
     ddSymmSummary(table, lower, upper, &symvars, &symgroups);
 
@@ -373,8 +373,8 @@ cuddSymmSifting(
 
 ddSymmSiftingOutOfMem:
 
-    if (entry != NULL) FREE(entry);
-    if (var != NULL) FREE(var);
+    if (entry != NULL) ABC_FREE(entry);
+    if (var != NULL) ABC_FREE(var);
 
     return(0);
 
@@ -429,12 +429,12 @@ cuddSymmSiftingConv(
 
     /* Find order in which to sift variables. */
     var = NULL;
-    entry = ALLOC(int,size);
+    entry = ABC_ALLOC(int,size);
     if (entry == NULL) {
     table->errorCode = CUDD_MEMORY_OUT;
     goto ddSymmSiftingConvOutOfMem;
     }
-    var = ALLOC(int,size);
+    var = ABC_ALLOC(int,size);
     if (var == NULL) {
     table->errorCode = CUDD_MEMORY_OUT;
     goto ddSymmSiftingConvOutOfMem;
@@ -538,15 +538,15 @@ cuddSymmSiftingConv(
            symgroups);
 #endif
 
-    FREE(var);
-    FREE(entry);
+    ABC_FREE(var);
+    ABC_FREE(entry);
 
     return(1+symvars);
 
 ddSymmSiftingConvOutOfMem:
 
-    if (entry != NULL) FREE(entry);
-    if (var != NULL) FREE(var);
+    if (entry != NULL) ABC_FREE(entry);
+    if (var != NULL) ABC_FREE(var);
 
     return(0);
 
diff --git a/src/bdd/cudd/cuddTable.c b/src/bdd/cudd/cuddTable.c
index 458f19e6..3c76c1af 100644
--- a/src/bdd/cudd/cuddTable.c
+++ b/src/bdd/cudd/cuddTable.c
@@ -205,7 +205,7 @@ cuddAllocNode(
     extern void (*MMoutOfMemory)(long);
     void (*saveHandler)(long);
 
-    if (unique->nextFree == NULL) {    /* free list is empty */
+    if (unique->nextFree == NULL) {    /* ABC_FREE list is empty */
     /* Check for exceeded limits. */
     if ((unique->keys - unique->dead) + (unique->keysZ - unique->deadZ) >
         unique->maxLive) {
@@ -224,7 +224,7 @@ cuddAllocNode(
         /* Try to allocate a new block. */
         saveHandler = MMoutOfMemory;
         MMoutOfMemory = Cudd_OutOfMem;
-        mem = (DdNodePtr *) ALLOC(DdNode,DD_MEM_CHUNK + 1);
+        mem = (DdNodePtr *) ABC_ALLOC(DdNode,DD_MEM_CHUNK + 1);
         MMoutOfMemory = saveHandler;
         if (mem == NULL) {
         /* No more memory: Try collecting garbage. If this succeeds,
@@ -235,12 +235,12 @@ cuddAllocNode(
             ** any. If this succeeeds, mem != NULL and
             ** unique->nextFree still NULL. */
             if (unique->stash != NULL) {
-            FREE(unique->stash);
+            ABC_FREE(unique->stash);
             unique->stash = NULL;
             /* Inhibit resizing of tables. */
             cuddSlowTableGrowth(unique);
             /* Now try again. */
-            mem = (DdNodePtr *) ALLOC(DdNode,DD_MEM_CHUNK + 1);
+            mem = (DdNodePtr *) ABC_ALLOC(DdNode,DD_MEM_CHUNK + 1);
             }
             if (mem == NULL) {
             /* Out of luck. Call the default handler to do
@@ -310,7 +310,7 @@ cuddInitTable(
   unsigned int numSlots /* Initial size of the BDD subtables */,
   unsigned int looseUpTo /* Limit for fast table growth */)
 {
-    DdManager    *unique = ALLOC(DdManager,1);
+    DdManager    *unique = ABC_ALLOC(DdManager,1);
     int        i, j;
     DdNodePtr    *nodelist;
     DdNode    *sentinel;
@@ -355,38 +355,38 @@ cuddInitTable(
     unique->gcEnabled = 1;
     unique->allocated = 0;
     unique->reclaimed = 0;
-    unique->subtables = ALLOC(DdSubtable,unique->maxSize);
+    unique->subtables = ABC_ALLOC(DdSubtable,unique->maxSize);
     if (unique->subtables == NULL) {
     unique->errorCode = CUDD_MEMORY_OUT;
     return(0);
     }
-    unique->subtableZ = ALLOC(DdSubtable,unique->maxSizeZ);
+    unique->subtableZ = ABC_ALLOC(DdSubtable,unique->maxSizeZ);
     if (unique->subtableZ == NULL) {
     unique->errorCode = CUDD_MEMORY_OUT;
     return(0);
     }
-    unique->perm = ALLOC(int,unique->maxSize);
+    unique->perm = ABC_ALLOC(int,unique->maxSize);
     if (unique->perm == NULL) {
     unique->errorCode = CUDD_MEMORY_OUT;
     return(0);
     }
-    unique->invperm = ALLOC(int,unique->maxSize);
+    unique->invperm = ABC_ALLOC(int,unique->maxSize);
     if (unique->invperm == NULL) {
     unique->errorCode = CUDD_MEMORY_OUT;
     return(0);
     }
-    unique->permZ = ALLOC(int,unique->maxSizeZ);
+    unique->permZ = ABC_ALLOC(int,unique->maxSizeZ);
     if (unique->permZ == NULL) {
     unique->errorCode = CUDD_MEMORY_OUT;
     return(0);
     }
-    unique->invpermZ = ALLOC(int,unique->maxSizeZ);
+    unique->invpermZ = ABC_ALLOC(int,unique->maxSizeZ);
     if (unique->invpermZ == NULL) {
     unique->errorCode = CUDD_MEMORY_OUT;
     return(0);
     }
     unique->map = NULL;
-    unique->stack = ALLOC(DdNodePtr,ddMax(unique->maxSize,unique->maxSizeZ)+1);
+    unique->stack = ABC_ALLOC(DdNodePtr,ddMax(unique->maxSize,unique->maxSizeZ)+1);
     if (unique->stack == NULL) {
     unique->errorCode = CUDD_MEMORY_OUT;
     return(0);
@@ -395,7 +395,7 @@ cuddInitTable(
 
 #ifndef DD_NO_DEATH_ROW
     unique->deathRowDepth = 1 << cuddComputeFloorLog2(unique->looseUpTo >> 2);
-    unique->deathRow = ALLOC(DdNodePtr,unique->deathRowDepth);
+    unique->deathRow = ABC_ALLOC(DdNodePtr,unique->deathRowDepth);
     if (unique->deathRow == NULL) {
     unique->errorCode = CUDD_MEMORY_OUT;
     return(0);
@@ -419,7 +419,7 @@ cuddInitTable(
     unique->subtables[i].varHandled = 0;
     unique->subtables[i].varToBeGrouped = CUDD_LAZY_NONE;
 
-    nodelist = unique->subtables[i].nodelist = ALLOC(DdNodePtr,slots);
+    nodelist = unique->subtables[i].nodelist = ABC_ALLOC(DdNodePtr,slots);
     if (nodelist == NULL) {
         unique->errorCode = CUDD_MEMORY_OUT;
         return(NULL);
@@ -436,7 +436,7 @@ cuddInitTable(
     unique->subtableZ[i].keys = 0;
     unique->subtableZ[i].dead = 0;
     unique->subtableZ[i].maxKeys = slots * DD_MAX_SUBTABLE_DENSITY;
-    nodelist = unique->subtableZ[i].nodelist = ALLOC(DdNodePtr,slots);
+    nodelist = unique->subtableZ[i].nodelist = ABC_ALLOC(DdNodePtr,slots);
     if (nodelist == NULL) {
         unique->errorCode = CUDD_MEMORY_OUT;
         return(NULL);
@@ -452,7 +452,7 @@ cuddInitTable(
     unique->constants.keys = 0;
     unique->constants.dead = 0;
     unique->constants.maxKeys = slots * DD_MAX_SUBTABLE_DENSITY;
-    nodelist = unique->constants.nodelist = ALLOC(DdNodePtr,slots);
+    nodelist = unique->constants.nodelist = ABC_ALLOC(DdNodePtr,slots);
     if (nodelist == NULL) {
     unique->errorCode = CUDD_MEMORY_OUT;
     return(NULL);
@@ -558,35 +558,35 @@ cuddFreeTable(
     if (unique->univ != NULL) cuddZddFreeUniv(unique);
     while (memlist != NULL) {
         next = (DdNodePtr *) memlist[0];    /* link to next block */
-    FREE(memlist);
+    ABC_FREE(memlist);
     memlist = next;
     }
     unique->nextFree = NULL;
     unique->memoryList = NULL;
 
     for (i = 0; i < unique->size; i++) {
-    FREE(unique->subtables[i].nodelist);
+    ABC_FREE(unique->subtables[i].nodelist);
     }
     for (i = 0; i < unique->sizeZ; i++) {
-    FREE(unique->subtableZ[i].nodelist);
-    }
-    FREE(unique->constants.nodelist);
-    FREE(unique->subtables);
-    FREE(unique->subtableZ);
-    FREE(unique->acache);
-    FREE(unique->perm);
-    FREE(unique->permZ);
-    FREE(unique->invperm);
-    FREE(unique->invpermZ);
-    FREE(unique->vars);
-    if (unique->map != NULL) FREE(unique->map);
-    FREE(unique->stack);
+    ABC_FREE(unique->subtableZ[i].nodelist);
+    }
+    ABC_FREE(unique->constants.nodelist);
+    ABC_FREE(unique->subtables);
+    ABC_FREE(unique->subtableZ);
+    ABC_FREE(unique->acache);
+    ABC_FREE(unique->perm);
+    ABC_FREE(unique->permZ);
+    ABC_FREE(unique->invperm);
+    ABC_FREE(unique->invpermZ);
+    ABC_FREE(unique->vars);
+    if (unique->map != NULL) ABC_FREE(unique->map);
+    ABC_FREE(unique->stack);
 #ifndef DD_NO_DEATH_ROW
-    FREE(unique->deathRow);
+    ABC_FREE(unique->deathRow);
 #endif
     if (unique->tree != NULL) Mtr_FreeTree(unique->tree);
     if (unique->treeZ != NULL) Mtr_FreeTree(unique->treeZ);
-    if (unique->linear != NULL) FREE(unique->linear);
+    if (unique->linear != NULL) ABC_FREE(unique->linear);
     while (unique->preGCHook != NULL)
     Cudd_RemoveHook(unique,unique->preGCHook->f,CUDD_PRE_GC_HOOK);
     while (unique->postGCHook != NULL)
@@ -597,7 +597,7 @@ cuddFreeTable(
     while (unique->postReorderingHook != NULL)
     Cudd_RemoveHook(unique,unique->postReorderingHook->f,
             CUDD_POST_REORDERING_HOOK);
-    FREE(unique);
+    ABC_FREE(unique);
 
 } /* end of cuddFreeTable */
 
@@ -699,7 +699,7 @@ cuddGarbageCollect(
     cuddLocalCacheClearDead(unique);
     }
 
-    /* Now return dead nodes to free list. Count them for sanity check. */
+    /* Now return dead nodes to ABC_FREE list. Count them for sanity check. */
     totalDeleted = 0;
 #ifndef DD_UNSORTED_FREE_LIST
     tree = NULL;
@@ -905,7 +905,7 @@ cuddGarbageCollectZdd(
     }
     }
 
-    /* Now return dead nodes to free list. Count them for sanity check. */
+    /* Now return dead nodes to ABC_FREE list. Count them for sanity check. */
     totalDeleted = 0;
 #ifndef DD_UNSORTED_FREE_LIST
     tree = NULL;
@@ -1535,7 +1535,7 @@ cuddRehash(
 
     saveHandler = MMoutOfMemory;
     MMoutOfMemory = Cudd_OutOfMem;
-    nodelist = ALLOC(DdNodePtr, slots);
+    nodelist = ABC_ALLOC(DdNodePtr, slots);
     MMoutOfMemory = saveHandler;
     if (nodelist == NULL) {
         (void) fprintf(unique->err,
@@ -1544,7 +1544,7 @@ cuddRehash(
         /* Prevent frequent resizing attempts. */
         (void) cuddGarbageCollect(unique,1);
         if (unique->stash != NULL) {
-        FREE(unique->stash);
+        ABC_FREE(unique->stash);
         unique->stash = NULL;
         /* Inhibit resizing of tables. */
         cuddSlowTableGrowth(unique);
@@ -1580,7 +1580,7 @@ cuddRehash(
         }
         *evenP = *oddP = sentinel;
     }
-    FREE(oldnodelist);
+    ABC_FREE(oldnodelist);
 
 #ifdef DD_VERBOSE
     (void) fprintf(unique->err,
@@ -1602,7 +1602,7 @@ cuddRehash(
     shift = oldshift - 1;
     saveHandler = MMoutOfMemory;
     MMoutOfMemory = Cudd_OutOfMem;
-    nodelist = ALLOC(DdNodePtr, slots);
+    nodelist = ABC_ALLOC(DdNodePtr, slots);
     MMoutOfMemory = saveHandler;
     if (nodelist == NULL) {
         int j;
@@ -1633,7 +1633,7 @@ cuddRehash(
         node = next;
         }
     }
-    FREE(oldnodelist);
+    ABC_FREE(oldnodelist);
 
 #ifdef DD_VERBOSE
     (void) fprintf(unique->err,
@@ -1681,7 +1681,7 @@ cuddShrinkSubtable(
     slots = oldslots >> 1;
     saveHandler = MMoutOfMemory;
     MMoutOfMemory = Cudd_OutOfMem;
-    nodelist = ALLOC(DdNodePtr, slots);
+    nodelist = ABC_ALLOC(DdNodePtr, slots);
     MMoutOfMemory = saveHandler;
     if (nodelist == NULL) {
     return;
@@ -1730,7 +1730,7 @@ cuddShrinkSubtable(
         node = next;
     }
     }
-    FREE(oldnodelist);
+    ABC_FREE(oldnodelist);
 
     unique->memused += ((long) slots - (long) oldslots) * sizeof(DdNode *);
     unique->slots += slots - oldslots;
@@ -1815,7 +1815,7 @@ cuddInsertSubtables(
         unique->perm[oldsize+i] = level + i;
         unique->invperm[level+i] = oldsize + i;
         newnodelist = unique->subtables[level+i].nodelist =
-        ALLOC(DdNodePtr, numSlots);
+        ABC_ALLOC(DdNodePtr, numSlots);
         if (newnodelist == NULL) {
         unique->errorCode = CUDD_MEMORY_OUT;
         return(0);
@@ -1841,40 +1841,40 @@ cuddInsertSubtables(
         unique->maxSize, newsize);
 #endif
     /* Allocate memory for new arrays (except nodelists). */
-    newsubtables = ALLOC(DdSubtable,newsize);
+    newsubtables = ABC_ALLOC(DdSubtable,newsize);
     if (newsubtables == NULL) {
         unique->errorCode = CUDD_MEMORY_OUT;
         return(0);
     }
-    newvars = ALLOC(DdNodePtr,newsize);
+    newvars = ABC_ALLOC(DdNodePtr,newsize);
     if (newvars == NULL) {
         unique->errorCode = CUDD_MEMORY_OUT;
-        FREE(newsubtables);
+        ABC_FREE(newsubtables);
         return(0);
     }
-    newperm = ALLOC(int,newsize);
+    newperm = ABC_ALLOC(int,newsize);
     if (newperm == NULL) {
         unique->errorCode = CUDD_MEMORY_OUT;
-        FREE(newsubtables);
-        FREE(newvars);
+        ABC_FREE(newsubtables);
+        ABC_FREE(newvars);
         return(0);
     }
-    newinvperm = ALLOC(int,newsize);
+    newinvperm = ABC_ALLOC(int,newsize);
     if (newinvperm == NULL) {
         unique->errorCode = CUDD_MEMORY_OUT;
-        FREE(newsubtables);
-        FREE(newvars);
-        FREE(newperm);
+        ABC_FREE(newsubtables);
+        ABC_FREE(newvars);
+        ABC_FREE(newperm);
         return(0);
     }
     if (unique->map != NULL) {
-        newmap = ALLOC(int,newsize);
+        newmap = ABC_ALLOC(int,newsize);
         if (newmap == NULL) {
         unique->errorCode = CUDD_MEMORY_OUT;
-        FREE(newsubtables);
-        FREE(newvars);
-        FREE(newperm);
-        FREE(newinvperm);
+        ABC_FREE(newsubtables);
+        ABC_FREE(newvars);
+        ABC_FREE(newperm);
+        ABC_FREE(newinvperm);
         return(0);
         }
         unique->memused += (newsize - unique->maxSize) * sizeof(int);
@@ -1919,7 +1919,7 @@ cuddInsertSubtables(
 
         newperm[oldsize + i - level] = i;
         newinvperm[i] = oldsize + i - level;
-        newnodelist = newsubtables[i].nodelist = ALLOC(DdNodePtr, numSlots);
+        newnodelist = newsubtables[i].nodelist = ABC_ALLOC(DdNodePtr, numSlots);
         if (newnodelist == NULL) {
         /* We are going to leak some memory.  We should clean up. */
         unique->errorCode = CUDD_MEMORY_OUT;
@@ -1957,23 +1957,23 @@ cuddInsertSubtables(
         for (i = oldsize; i < oldsize + n; i++) {
         newmap[i] = i;
         }
-        FREE(unique->map);
+        ABC_FREE(unique->map);
         unique->map = newmap;
     }
-    /* Install the new tables and free the old ones. */
-    FREE(unique->subtables);
+    /* Install the new tables and ABC_FREE the old ones. */
+    ABC_FREE(unique->subtables);
     unique->subtables = newsubtables;
     unique->maxSize = newsize;
-    FREE(unique->vars);
+    ABC_FREE(unique->vars);
     unique->vars = newvars;
-    FREE(unique->perm);
+    ABC_FREE(unique->perm);
     unique->perm = newperm;
-    FREE(unique->invperm);
+    ABC_FREE(unique->invperm);
     unique->invperm = newinvperm;
     /* Update the stack for iterative procedures. */
     if (newsize > unique->maxSizeZ) {
-        FREE(unique->stack);
-        unique->stack = ALLOC(DdNodePtr,newsize + 1);
+        ABC_FREE(unique->stack);
+        unique->stack = ABC_ALLOC(DdNodePtr,newsize + 1);
         if (unique->stack == NULL) {
         unique->errorCode = CUDD_MEMORY_OUT;
         return(0);
@@ -2016,7 +2016,7 @@ cuddInsertSubtables(
         unique->subtables[j].maxKeys  =
             unique->subtables[j+n].maxKeys;
         unique->subtables[j].dead     = unique->subtables[j+n].dead;
-        FREE(unique->subtables[j].nodelist);
+        ABC_FREE(unique->subtables[j].nodelist);
         unique->subtables[j].nodelist =
             unique->subtables[j+n].nodelist;
         unique->subtables[j+n].nodelist = NULL;
@@ -2134,7 +2134,7 @@ cuddDestroySubtables(
 #ifdef DD_DEBUG
     assert(subtables[level].keys == 0);
 #endif
-    FREE(nodelist);
+    ABC_FREE(nodelist);
     unique->memused -= sizeof(DdNodePtr) * subtables[level].slots;
     unique->slots -= subtables[level].slots;
     unique->dead -= subtables[level].dead;
@@ -2174,7 +2174,7 @@ cuddDestroySubtables(
     ** an out-of-bounds access to unique->vars would result. */
     if (unique->map != NULL) {
     cuddCacheFlush(unique);
-    FREE(unique->map);
+    ABC_FREE(unique->map);
     unique->map = NULL;
     }
 
@@ -2228,7 +2228,7 @@ cuddResizeTableZdd(
         unique->permZ[i] = i;
         unique->invpermZ[i] = i;
         newnodelist = unique->subtableZ[i].nodelist =
-        ALLOC(DdNodePtr, numSlots);
+        ABC_ALLOC(DdNodePtr, numSlots);
         if (newnodelist == NULL) {
         unique->errorCode = CUDD_MEMORY_OUT;
         return(0);
@@ -2248,17 +2248,17 @@ cuddResizeTableZdd(
                "Increasing the ZDD table size from %d to %d\n",
         unique->maxSizeZ, newsize);
 #endif
-    newsubtables = ALLOC(DdSubtable,newsize);
+    newsubtables = ABC_ALLOC(DdSubtable,newsize);
     if (newsubtables == NULL) {
         unique->errorCode = CUDD_MEMORY_OUT;
         return(0);
     }
-    newperm = ALLOC(int,newsize);
+    newperm = ABC_ALLOC(int,newsize);
     if (newperm == NULL) {
         unique->errorCode = CUDD_MEMORY_OUT;
         return(0);
     }
-    newinvperm = ALLOC(int,newsize);
+    newinvperm = ABC_ALLOC(int,newsize);
     if (newinvperm == NULL) {
         unique->errorCode = CUDD_MEMORY_OUT;
         return(0);
@@ -2266,8 +2266,8 @@ cuddResizeTableZdd(
     unique->memused += (newsize - unique->maxSizeZ) * ((numSlots+1) *
         sizeof(DdNode *) + 2 * sizeof(int) + sizeof(DdSubtable));
     if (newsize > unique->maxSize) {
-        FREE(unique->stack);
-        unique->stack = ALLOC(DdNodePtr,newsize + 1);
+        ABC_FREE(unique->stack);
+        unique->stack = ABC_ALLOC(DdNodePtr,newsize + 1);
         if (unique->stack == NULL) {
         unique->errorCode = CUDD_MEMORY_OUT;
         return(0);
@@ -2296,7 +2296,7 @@ cuddResizeTableZdd(
         newsubtables[i].dead = 0;
         newperm[i] = i;
         newinvperm[i] = i;
-        newnodelist = newsubtables[i].nodelist = ALLOC(DdNodePtr, numSlots);
+        newnodelist = newsubtables[i].nodelist = ABC_ALLOC(DdNodePtr, numSlots);
         if (newnodelist == NULL) {
         unique->errorCode = CUDD_MEMORY_OUT;
         return(0);
@@ -2305,12 +2305,12 @@ cuddResizeTableZdd(
         newnodelist[j] = NULL;
         }
     }
-    FREE(unique->subtableZ);
+    ABC_FREE(unique->subtableZ);
     unique->subtableZ = newsubtables;
     unique->maxSizeZ = newsize;
-    FREE(unique->permZ);
+    ABC_FREE(unique->permZ);
     unique->permZ = newperm;
-    FREE(unique->invpermZ);
+    ABC_FREE(unique->invpermZ);
     unique->invpermZ = newinvperm;
     }
     unique->slots += (index + 1 - unique->sizeZ) * numSlots;
@@ -2428,7 +2428,7 @@ ddRehashZdd(
 
     saveHandler = MMoutOfMemory;
     MMoutOfMemory = Cudd_OutOfMem;
-    nodelist = ALLOC(DdNodePtr, slots);
+    nodelist = ABC_ALLOC(DdNodePtr, slots);
     MMoutOfMemory = saveHandler;
     if (nodelist == NULL) {
     int j;
@@ -2458,7 +2458,7 @@ ddRehashZdd(
         node = next;
     }
     }
-    FREE(oldnodelist);
+    ABC_FREE(oldnodelist);
 
 #ifdef DD_VERBOSE
     (void) fprintf(unique->err,
@@ -2523,10 +2523,10 @@ ddResizeTable(
         unique->perm[i] = i;
         unique->invperm[i] = i;
         newnodelist = unique->subtables[i].nodelist =
-        ALLOC(DdNodePtr, numSlots);
+        ABC_ALLOC(DdNodePtr, numSlots);
         if (newnodelist == NULL) {
         for (j = oldsize; j < i; j++) {
-            FREE(unique->subtables[j].nodelist);
+            ABC_FREE(unique->subtables[j].nodelist);
         }
         unique->errorCode = CUDD_MEMORY_OUT;
         return(0);
@@ -2551,39 +2551,39 @@ ddResizeTable(
                "Increasing the table size from %d to %d\n",
                unique->maxSize, newsize);
 #endif
-    newsubtables = ALLOC(DdSubtable,newsize);
+    newsubtables = ABC_ALLOC(DdSubtable,newsize);
     if (newsubtables == NULL) {
         unique->errorCode = CUDD_MEMORY_OUT;
         return(0);
     }
-    newvars = ALLOC(DdNodePtr,newsize);
+    newvars = ABC_ALLOC(DdNodePtr,newsize);
     if (newvars == NULL) {
-        FREE(newsubtables);
+        ABC_FREE(newsubtables);
         unique->errorCode = CUDD_MEMORY_OUT;
         return(0);
     }
-    newperm = ALLOC(int,newsize);
+    newperm = ABC_ALLOC(int,newsize);
     if (newperm == NULL) {
-        FREE(newsubtables);
-        FREE(newvars);
+        ABC_FREE(newsubtables);
+        ABC_FREE(newvars);
         unique->errorCode = CUDD_MEMORY_OUT;
         return(0);
     }
-    newinvperm = ALLOC(int,newsize);
+    newinvperm = ABC_ALLOC(int,newsize);
     if (newinvperm == NULL) {
-        FREE(newsubtables);
-        FREE(newvars);
-        FREE(newperm);
+        ABC_FREE(newsubtables);
+        ABC_FREE(newvars);
+        ABC_FREE(newperm);
         unique->errorCode = CUDD_MEMORY_OUT;
         return(0);
     }
     if (unique->map != NULL) {
-        newmap = ALLOC(int,newsize);
+        newmap = ABC_ALLOC(int,newsize);
         if (newmap == NULL) {
-        FREE(newsubtables);
-        FREE(newvars);
-        FREE(newperm);
-        FREE(newinvperm);
+        ABC_FREE(newsubtables);
+        ABC_FREE(newvars);
+        ABC_FREE(newperm);
+        ABC_FREE(newinvperm);
         unique->errorCode = CUDD_MEMORY_OUT;
         return(0);
         }
@@ -2592,15 +2592,15 @@ ddResizeTable(
     unique->memused += (newsize - unique->maxSize) * ((numSlots+1) *
         sizeof(DdNode *) + 2 * sizeof(int) + sizeof(DdSubtable));
     if (newsize > unique->maxSizeZ) {
-        FREE(unique->stack);
-        unique->stack = ALLOC(DdNodePtr,newsize + 1);
+        ABC_FREE(unique->stack);
+        unique->stack = ABC_ALLOC(DdNodePtr,newsize + 1);
         if (unique->stack == NULL) {
-        FREE(newsubtables);
-        FREE(newvars);
-        FREE(newperm);
-        FREE(newinvperm);
+        ABC_FREE(newsubtables);
+        ABC_FREE(newvars);
+        ABC_FREE(newperm);
+        ABC_FREE(newinvperm);
         if (unique->map != NULL) {
-            FREE(newmap);
+            ABC_FREE(newmap);
         }
         unique->errorCode = CUDD_MEMORY_OUT;
         return(0);
@@ -2642,7 +2642,7 @@ ddResizeTable(
 
         newperm[i] = i;
         newinvperm[i] = i;
-        newnodelist = newsubtables[i].nodelist = ALLOC(DdNodePtr, numSlots);
+        newnodelist = newsubtables[i].nodelist = ABC_ALLOC(DdNodePtr, numSlots);
         if (newnodelist == NULL) {
         unique->errorCode = CUDD_MEMORY_OUT;
         return(0);
@@ -2658,17 +2658,17 @@ ddResizeTable(
         for (i = oldsize; i <= index; i++) {
         newmap[i] = i;
         }
-        FREE(unique->map);
+        ABC_FREE(unique->map);
         unique->map = newmap;
     }
-    FREE(unique->subtables);
+    ABC_FREE(unique->subtables);
     unique->subtables = newsubtables;
     unique->maxSize = newsize;
-    FREE(unique->vars);
+    ABC_FREE(unique->vars);
     unique->vars = newvars;
-    FREE(unique->perm);
+    ABC_FREE(unique->perm);
     unique->perm = newperm;
-    FREE(unique->invperm);
+    ABC_FREE(unique->invperm);
     unique->invperm = newinvperm;
     }
 
@@ -2695,7 +2695,7 @@ ddResizeTable(
         unique->vars[j] = NULL;
         }
         for (j = oldsize; j <= index; j++) {
-        FREE(unique->subtables[j].nodelist);
+        ABC_FREE(unique->subtables[j].nodelist);
         unique->subtables[j].nodelist = NULL;
         }
         unique->size = oldsize;
diff --git a/src/bdd/cudd/cuddUtil.c b/src/bdd/cudd/cuddUtil.c
index bc1a17eb..7e0eb22a 100644
--- a/src/bdd/cudd/cuddUtil.c
+++ b/src/bdd/cudd/cuddUtil.c
@@ -180,14 +180,14 @@ Cudd_PrintMinterm(
 
     background = manager->background;
     zero = Cudd_Not(manager->one);
-    list = ALLOC(int,manager->size);
+    list = ABC_ALLOC(int,manager->size);
     if (list == NULL) {
     manager->errorCode = CUDD_MEMORY_OUT;
     return(0);
     }
     for (i = 0; i < manager->size; i++) list[i] = 2;
     ddPrintMintermAux(manager,node,list);
-    FREE(list);
+    ABC_FREE(list);
     return(1);
 
 } /* end of Cudd_PrintMinterm */
@@ -221,7 +221,7 @@ Cudd_bddPrintCover(
     DdNode *cover;
 #endif
 
-    array = ALLOC(int, Cudd_ReadSize(dd));
+    array = ABC_ALLOC(int, Cudd_ReadSize(dd));
     if (array == NULL) return(0);
     lb = l;
     cuddRef(lb);
@@ -235,7 +235,7 @@ Cudd_bddPrintCover(
     implicant = Cudd_LargestCube(dd,lb,&length);
     if (implicant == NULL) {
         Cudd_RecursiveDeref(dd,lb);
-        FREE(array);
+        ABC_FREE(array);
         return(0);
     }
     cuddRef(implicant);
@@ -243,7 +243,7 @@ Cudd_bddPrintCover(
     if (prime == NULL) {
         Cudd_RecursiveDeref(dd,lb);
         Cudd_RecursiveDeref(dd,implicant);
-        FREE(array);
+        ABC_FREE(array);
         return(0);
     }
     cuddRef(prime);
@@ -252,7 +252,7 @@ Cudd_bddPrintCover(
     if (tmp == NULL) {
         Cudd_RecursiveDeref(dd,lb);
         Cudd_RecursiveDeref(dd,prime);
-        FREE(array);
+        ABC_FREE(array);
         return(0);
     }
     cuddRef(tmp);
@@ -262,7 +262,7 @@ Cudd_bddPrintCover(
     if (result == 0) {
         Cudd_RecursiveDeref(dd,lb);
         Cudd_RecursiveDeref(dd,prime);
-        FREE(array);
+        ABC_FREE(array);
         return(0);
     }
     for (q = 0; q < dd->size; q++) {
@@ -287,7 +287,7 @@ Cudd_bddPrintCover(
         Cudd_RecursiveDeref(dd,cover);
         Cudd_RecursiveDeref(dd,lb);
         Cudd_RecursiveDeref(dd,prime);
-        FREE(array);
+        ABC_FREE(array);
         return(0);
     }
     cuddRef(tmp);
@@ -298,7 +298,7 @@ Cudd_bddPrintCover(
     }
     (void) fprintf(dd->out, "\n");
     Cudd_RecursiveDeref(dd,lb);
-    FREE(array);
+    ABC_FREE(array);
 #ifdef DD_DEBUG
     if (!Cudd_bddLeq(dd,cover,u) || !Cudd_bddLeq(dd,l,cover)) {
         Cudd_RecursiveDeref(dd,cover);
@@ -707,7 +707,7 @@ Cudd_Support(
 
     /* 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;
     return(NULL);
@@ -745,7 +745,7 @@ Cudd_Support(
     }
     } while (dd->reordered == 1);
 
-    FREE(support);
+    ABC_FREE(support);
     if (res != NULL) cuddDeref(res);
     return(res);
 
@@ -775,7 +775,7 @@ Cudd_SupportIndex(
 
     /* 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;
     return(NULL);
@@ -818,7 +818,7 @@ Cudd_SupportSize(
 
     /* 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;
     return(CUDD_OUT_OF_MEM);
@@ -837,7 +837,7 @@ Cudd_SupportSize(
     if (support[i] == 1) count++;
     }
 
-    FREE(support);
+    ABC_FREE(support);
     return(count);
 
 } /* end of Cudd_SupportSize */
@@ -870,7 +870,7 @@ Cudd_VectorSupport(
 
     /* 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;
     return(NULL);
@@ -899,7 +899,7 @@ Cudd_VectorSupport(
         if (tmp == NULL) {
         Cudd_RecursiveDeref(dd,res);
         Cudd_RecursiveDeref(dd,var);
-        FREE(support);
+        ABC_FREE(support);
         return(NULL);
         }
         cuddRef(tmp);
@@ -909,7 +909,7 @@ Cudd_VectorSupport(
     }
     }
 
-    FREE(support);
+    ABC_FREE(support);
     cuddDeref(res);
     return(res);
 
@@ -941,7 +941,7 @@ Cudd_VectorSupportIndex(
 
     /* 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;
     return(NULL);
@@ -990,7 +990,7 @@ Cudd_VectorSupportSize(
 
     /* 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;
     return(CUDD_OUT_OF_MEM);
@@ -1013,7 +1013,7 @@ Cudd_VectorSupportSize(
     if (support[i] == 1) count++;
     }
 
-    FREE(support);
+    ABC_FREE(support);
     return(count);
 
 } /* end of Cudd_VectorSupportSize */
@@ -1050,15 +1050,15 @@ Cudd_ClassifySupport(
 
     /* Allocate and initialize support arrays for ddSupportStep. */
     size = ddMax(dd->size, dd->sizeZ);
-    supportF = ALLOC(int,size);
+    supportF = ABC_ALLOC(int,size);
     if (supportF == NULL) {
     dd->errorCode = CUDD_MEMORY_OUT;
     return(0);
     }
-    supportG = ALLOC(int,size);
+    supportG = ABC_ALLOC(int,size);
     if (supportG == NULL) {
     dd->errorCode = CUDD_MEMORY_OUT;
-    FREE(supportF);
+    ABC_FREE(supportF);
     return(0);
     }
     for (i = 0; i < size; i++) {
@@ -1087,7 +1087,7 @@ Cudd_ClassifySupport(
         Cudd_RecursiveDeref(dd,*onlyF);
         Cudd_RecursiveDeref(dd,*onlyG);
         Cudd_RecursiveDeref(dd,var);
-        FREE(supportF); FREE(supportG);
+        ABC_FREE(supportF); ABC_FREE(supportG);
         return(0);
         }
         cuddRef(tmp);
@@ -1100,7 +1100,7 @@ Cudd_ClassifySupport(
         Cudd_RecursiveDeref(dd,*onlyF);
         Cudd_RecursiveDeref(dd,*onlyG);
         Cudd_RecursiveDeref(dd,var);
-        FREE(supportF); FREE(supportG);
+        ABC_FREE(supportF); ABC_FREE(supportG);
         return(0);
         }
         cuddRef(tmp);
@@ -1113,7 +1113,7 @@ Cudd_ClassifySupport(
         Cudd_RecursiveDeref(dd,*onlyF);
         Cudd_RecursiveDeref(dd,*onlyG);
         Cudd_RecursiveDeref(dd,var);
-        FREE(supportF); FREE(supportG);
+        ABC_FREE(supportF); ABC_FREE(supportG);
         return(0);
         }
         cuddRef(tmp);
@@ -1123,7 +1123,7 @@ Cudd_ClassifySupport(
     Cudd_RecursiveDeref(dd,var);
     }
 
-    FREE(supportF); FREE(supportG);
+    ABC_FREE(supportF); ABC_FREE(supportG);
     cuddDeref(*common); cuddDeref(*onlyF); cuddDeref(*onlyG);
     return(1);
 
@@ -1254,15 +1254,15 @@ Cudd_bddPickOneMinterm(
     DdNode *old, *neW;
 
     size = dd->size;
-    string = ALLOC(char, size);
+    string = ABC_ALLOC(char, size);
     if (string == NULL) {
     dd->errorCode = CUDD_MEMORY_OUT;
     return(NULL);
     }
-    indices = ALLOC(int,n);
+    indices = ABC_ALLOC(int,n);
     if (indices == NULL) {
     dd->errorCode = CUDD_MEMORY_OUT;
-    FREE(string);
+    ABC_FREE(string);
     return(NULL);
     }
 
@@ -1272,8 +1272,8 @@ Cudd_bddPickOneMinterm(
 
     result = Cudd_bddPickOneCube(dd,f,string);
     if (result == 0) {
-    FREE(string);
-    FREE(indices);
+    ABC_FREE(string);
+    ABC_FREE(indices);
     return(NULL);
     }
 
@@ -1290,8 +1290,8 @@ Cudd_bddPickOneMinterm(
     for (i = n-1; i >= 0; i--) {
     neW = Cudd_bddAnd(dd,old,Cudd_NotCond(vars[i],string[indices[i]]==0));
     if (neW == NULL) {
-        FREE(string);
-        FREE(indices);
+        ABC_FREE(string);
+        ABC_FREE(indices);
         Cudd_RecursiveDeref(dd,old);
         return(NULL);
     }
@@ -1312,8 +1312,8 @@ Cudd_bddPickOneMinterm(
     cuddDeref(old);
 #endif
 
-    FREE(string);
-    FREE(indices);
+    ABC_FREE(string);
+    ABC_FREE(indices);
     return(old);
 
 }  /* end of Cudd_bddPickOneMinterm */
@@ -1366,29 +1366,29 @@ Cudd_bddPickArbitraryMinterms(
     }
 
     size = dd->size;
-    string = ALLOC(char *, k);
+    string = ABC_ALLOC(char *, k);
     if (string == NULL) {
     dd->errorCode = CUDD_MEMORY_OUT;
     return(NULL);
     }
     for (i = 0; i < k; i++) {
-    string[i] = ALLOC(char, size + 1);
+    string[i] = ABC_ALLOC(char, size + 1);
     if (string[i] == NULL) {
         for (j = 0; j < i; j++)
-        FREE(string[i]);
-        FREE(string);
+        ABC_FREE(string[i]);
+        ABC_FREE(string);
         dd->errorCode = CUDD_MEMORY_OUT;
         return(NULL);
     }
     for (j = 0; j < size; j++) string[i][j] = '2';
     string[i][size] = '\0';
     }
-    indices = ALLOC(int,n);
+    indices = ABC_ALLOC(int,n);
     if (indices == NULL) {
     dd->errorCode = CUDD_MEMORY_OUT;
     for (i = 0; i < k; i++)
-        FREE(string[i]);
-    FREE(string);
+        ABC_FREE(string[i]);
+    ABC_FREE(string);
     return(NULL);
     }
 
@@ -1399,29 +1399,29 @@ Cudd_bddPickArbitraryMinterms(
     result = ddPickArbitraryMinterms(dd,f,n,k,string);
     if (result == 0) {
     for (i = 0; i < k; i++)
-        FREE(string[i]);
-    FREE(string);
-    FREE(indices);
+        ABC_FREE(string[i]);
+    ABC_FREE(string);
+    ABC_FREE(indices);
     return(NULL);
     }
 
-    old = ALLOC(DdNode *, k);
+    old = ABC_ALLOC(DdNode *, k);
     if (old == NULL) {
     dd->errorCode = CUDD_MEMORY_OUT;
     for (i = 0; i < k; i++)
-        FREE(string[i]);
-    FREE(string);
-    FREE(indices);
+        ABC_FREE(string[i]);
+    ABC_FREE(string);
+    ABC_FREE(indices);
     return(NULL);
     }
-    saveString = ALLOC(char, size + 1);
+    saveString = ABC_ALLOC(char, size + 1);
     if (saveString == NULL) {
     dd->errorCode = CUDD_MEMORY_OUT;
     for (i = 0; i < k; i++)
-        FREE(string[i]);
-    FREE(string);
-    FREE(indices);
-    FREE(old);
+        ABC_FREE(string[i]);
+    ABC_FREE(string);
+    ABC_FREE(indices);
+    ABC_FREE(old);
     return(NULL);
     }
     saveFlag = 0;
@@ -1488,14 +1488,14 @@ Cudd_bddPickArbitraryMinterms(
         neW = Cudd_bddAnd(dd,old[i],vars[j]);
         }
         if (neW == NULL) {
-        FREE(saveString);
+        ABC_FREE(saveString);
         for (l = 0; l < k; l++)
-            FREE(string[l]);
-        FREE(string);
-        FREE(indices);
+            ABC_FREE(string[l]);
+        ABC_FREE(string);
+        ABC_FREE(indices);
         for (l = 0; l <= i; l++)
             Cudd_RecursiveDeref(dd,old[l]);
-        FREE(old);
+        ABC_FREE(old);
         return(NULL);
         }
         cuddRef(neW);
@@ -1505,25 +1505,25 @@ Cudd_bddPickArbitraryMinterms(
 
     /* Test. */
     if (!Cudd_bddLeq(dd,old[i],f)) {
-        FREE(saveString);
+        ABC_FREE(saveString);
         for (l = 0; l < k; l++)
-        FREE(string[l]);
-        FREE(string);
-        FREE(indices);
+        ABC_FREE(string[l]);
+        ABC_FREE(string);
+        ABC_FREE(indices);
         for (l = 0; l <= i; l++)
         Cudd_RecursiveDeref(dd,old[l]);
-        FREE(old);
+        ABC_FREE(old);
         return(NULL);
     }
     }
 
-    FREE(saveString);
+    ABC_FREE(saveString);
     for (i = 0; i < k; i++) {
     cuddDeref(old[i]);
-    FREE(string[i]);
+    ABC_FREE(string[i]);
     }
-    FREE(string);
-    FREE(indices);
+    ABC_FREE(string);
+    ABC_FREE(indices);
     return(old);
 
 }  /* end of Cudd_bddPickArbitraryMinterms */
@@ -1576,7 +1576,7 @@ Cudd_SubsetWithMaskVars(
     zero = Cudd_Not(dd->one);
     size = dd->size;
     
-    weight = ALLOC(double,size);
+    weight = ABC_ALLOC(double,size);
     if (weight == NULL) {
     dd->errorCode = CUDD_MEMORY_OUT;
     return(NULL);
@@ -1596,15 +1596,15 @@ Cudd_SubsetWithMaskVars(
     Cudd_RecursiveDeref(dd,cof);
     }
 
-    string = ALLOC(char, size + 1);
+    string = ABC_ALLOC(char, size + 1);
     if (string == NULL) {
     dd->errorCode = CUDD_MEMORY_OUT;
     return(NULL);
     }
-    mask = ALLOC(int, size);
+    mask = ABC_ALLOC(int, size);
     if (mask == NULL) {
     dd->errorCode = CUDD_MEMORY_OUT;
-    FREE(string);
+    ABC_FREE(string);
     return(NULL);
     }
     for (i = 0; i < size; i++) {
@@ -1612,11 +1612,11 @@ Cudd_SubsetWithMaskVars(
     mask[i] = 0;
     }
     string[size] = '\0';
-    indices = ALLOC(int,nvars);
+    indices = ABC_ALLOC(int,nvars);
     if (indices == NULL) {
     dd->errorCode = CUDD_MEMORY_OUT;
-    FREE(string);
-    FREE(mask);
+    ABC_FREE(string);
+    ABC_FREE(mask);
     return(NULL);
     }
     for (i = 0; i < nvars; i++) {
@@ -1625,9 +1625,9 @@ Cudd_SubsetWithMaskVars(
 
     result = ddPickRepresentativeCube(dd,f,nvars,weight,string);
     if (result == 0) {
-    FREE(string);
-    FREE(mask);
-    FREE(indices);
+    ABC_FREE(string);
+    ABC_FREE(mask);
+    ABC_FREE(indices);
     return(NULL);
     }
 
@@ -1642,9 +1642,9 @@ Cudd_SubsetWithMaskVars(
     } else
         continue;
     if (newCube == NULL) {
-        FREE(string);
-        FREE(mask);
-        FREE(indices);
+        ABC_FREE(string);
+        ABC_FREE(mask);
+        ABC_FREE(indices);
         Cudd_RecursiveDeref(dd,cube);
         return(NULL);
     }
@@ -1683,9 +1683,9 @@ Cudd_SubsetWithMaskVars(
     } else
         continue;
     if (newCube == NULL) {
-        FREE(string);
-        FREE(mask);
-        FREE(indices);
+        ABC_FREE(string);
+        ABC_FREE(mask);
+        ABC_FREE(indices);
         Cudd_RecursiveDeref(dd,cube);
         return(NULL);
     }
@@ -1706,10 +1706,10 @@ Cudd_SubsetWithMaskVars(
     subset = NULL;
     }
 
-    FREE(string);
-    FREE(mask);
-    FREE(indices);
-    FREE(weight);
+    ABC_FREE(string);
+    ABC_FREE(mask);
+    ABC_FREE(indices);
+    ABC_FREE(weight);
     return(subset);
 
 } /* end of Cudd_SubsetWithMaskVars */
@@ -1757,7 +1757,7 @@ Cudd_FirstCube(
     if (dd == NULL || f == NULL) return(NULL);
 
     /* Allocate generator an initialize it. */
-    gen = ALLOC(DdGen,1);
+    gen = ABC_ALLOC(DdGen,1);
     if (gen == NULL) {
     dd->errorCode = CUDD_MEMORY_OUT;
     return(NULL);
@@ -1773,10 +1773,10 @@ Cudd_FirstCube(
     gen->node = NULL;
 
     nvars = dd->size;
-    gen->gen.cubes.cube = ALLOC(int,nvars);
+    gen->gen.cubes.cube = ABC_ALLOC(int,nvars);
     if (gen->gen.cubes.cube == NULL) {
     dd->errorCode = CUDD_MEMORY_OUT;
-    FREE(gen);
+    ABC_FREE(gen);
     return(NULL);
     }
     for (i = 0; i < nvars; i++) gen->gen.cubes.cube[i] = 2;
@@ -1785,11 +1785,11 @@ Cudd_FirstCube(
     ** because a path may have nodes at all levels, including the
     ** constant level.
     */
-    gen->stack.stack = ALLOC(DdNode *, nvars+1);
+    gen->stack.stack = ABC_ALLOC(DdNode *, nvars+1);
     if (gen->stack.stack == NULL) {
     dd->errorCode = CUDD_MEMORY_OUT;
-    FREE(gen->gen.cubes.cube);
-    FREE(gen);
+    ABC_FREE(gen->gen.cubes.cube);
+    ABC_FREE(gen);
     return(NULL);
     }
     for (i = 0; i <= nvars; i++) gen->stack.stack[i] = NULL;
@@ -2172,7 +2172,7 @@ Cudd_FirstNode(
     if (dd == NULL || f == NULL) return(NULL);
 
     /* Allocate generator an initialize it. */
-    gen = ALLOC(DdGen,1);
+    gen = ABC_ALLOC(DdGen,1);
     if (gen == NULL) {
     dd->errorCode = CUDD_MEMORY_OUT;
     return(NULL);
@@ -2189,7 +2189,7 @@ Cudd_FirstNode(
 
     gen->gen.nodes.visited = st_init_table(st_ptrcmp,st_ptrhash);
     if (gen->gen.nodes.visited == NULL) {
-    FREE(gen);
+    ABC_FREE(gen);
     return(NULL);
     }
 
@@ -2197,7 +2197,7 @@ Cudd_FirstNode(
     retval = cuddCollectNodes(Cudd_Regular(f),gen->gen.nodes.visited);
     if (retval == 0) {
     st_free_table(gen->gen.nodes.visited);
-    FREE(gen);
+    ABC_FREE(gen);
     return(NULL);
     }
 
@@ -2205,7 +2205,7 @@ Cudd_FirstNode(
     gen->gen.nodes.stGen = st_init_gen(gen->gen.nodes.visited);
     if (gen->gen.nodes.stGen == NULL) {
     st_free_table(gen->gen.nodes.visited);
-    FREE(gen);
+    ABC_FREE(gen);
     return(NULL);
     }
 
@@ -2276,8 +2276,8 @@ Cudd_GenFree(
     switch (gen->type) {
     case CUDD_GEN_CUBES:
     case CUDD_GEN_ZDD_PATHS:
-    FREE(gen->gen.cubes.cube);
-    FREE(gen->stack.stack);
+    ABC_FREE(gen->gen.cubes.cube);
+    ABC_FREE(gen->stack.stack);
     break;
     case CUDD_GEN_NODES:
     st_free_gen(gen->gen.nodes.stGen);
@@ -2286,7 +2286,7 @@ Cudd_GenFree(
     default:
     return(0);
     }
-    FREE(gen);
+    ABC_FREE(gen);
     return(0);
 
 } /* end of Cudd_GenFree */
@@ -2679,7 +2679,7 @@ cuddStCountfree(
     double    *d;
 
     d = (double *)value;
-    FREE(d);
+    ABC_FREE(d);
     return(ST_CONTINUE);
 
 } /* end of cuddStCountfree */
@@ -3233,7 +3233,7 @@ ddCountPathAux(
     if (paths2 == (double)CUDD_OUT_OF_MEM) return((double)CUDD_OUT_OF_MEM);
     paths = paths1 + paths2;
     
-    ppaths = ALLOC(double,1);
+    ppaths = ABC_ALLOC(double,1);
     if (ppaths == NULL) {
     return((double)CUDD_OUT_OF_MEM);
     }
@@ -3241,7 +3241,7 @@ ddCountPathAux(
     *ppaths = paths;
 
     if (st_add_direct(table,(char *)node, (char *)ppaths) == ST_OUT_OF_MEM) {
-    FREE(ppaths);
+    ABC_FREE(ppaths);
     return((double)CUDD_OUT_OF_MEM);
     }
     return(paths);
@@ -3371,7 +3371,7 @@ ddCountPathsToNonZero(
     if (paths2 == (double)CUDD_OUT_OF_MEM) return((double)CUDD_OUT_OF_MEM);
     paths = paths1 + paths2;
 
-    ppaths = ALLOC(double,1);
+    ppaths = ABC_ALLOC(double,1);
     if (ppaths == NULL) {
     return((double)CUDD_OUT_OF_MEM);
     }
@@ -3379,7 +3379,7 @@ ddCountPathsToNonZero(
     *ppaths = paths;
 
     if (st_add_direct(table,(char *)N, (char *)ppaths) == ST_OUT_OF_MEM) {
-    FREE(ppaths);
+    ABC_FREE(ppaths);
     return((double)CUDD_OUT_OF_MEM);
     }
     return(paths);
diff --git a/src/bdd/cudd/cuddWindow.c b/src/bdd/cudd/cuddWindow.c
index 9ceb79b2..b97e3358 100644
--- a/src/bdd/cudd/cuddWindow.c
+++ b/src/bdd/cudd/cuddWindow.c
@@ -253,7 +253,7 @@ ddWindowConv2(
     if (high-low < 1) return(ddWindowConv2(table,low,high));
 
     nwin = high-low;
-    events = ALLOC(int,nwin);
+    events = ABC_ALLOC(int,nwin);
     if (events == NULL) {
     table->errorCode = CUDD_MEMORY_OUT;
     return(0);
@@ -270,13 +270,13 @@ ddWindowConv2(
         size = res;
         res = cuddSwapInPlace(table,x+low,x+low+1);
         if (res == 0) {
-            FREE(events);
+            ABC_FREE(events);
             return(0);
         }
         if (res >= size) { /* no improvement: undo permutation */
             res = cuddSwapInPlace(table,x+low,x+low+1);
             if (res == 0) {
-            FREE(events);
+            ABC_FREE(events);
             return(0);
             }
         }
@@ -304,7 +304,7 @@ ddWindowConv2(
 #endif
     } while (newevent);
 
-    FREE(events);
+    ABC_FREE(events);
 
     return(1);
 
@@ -487,7 +487,7 @@ ddWindowConv3(
     if (high-low < 2) return(ddWindowConv2(table,low,high));
 
     nwin = high-low-1;
-    events = ALLOC(int,nwin);
+    events = ABC_ALLOC(int,nwin);
     if (events == NULL) {
     table->errorCode = CUDD_MEMORY_OUT;
     return(0);
@@ -524,7 +524,7 @@ ddWindowConv3(
             newevent = 1;
             break;
         default:
-            FREE(events);
+            ABC_FREE(events);
             return(0);
         }
         events[x] = 0;
@@ -546,7 +546,7 @@ ddWindowConv3(
 #endif
     } while (newevent);
 
-    FREE(events);
+    ABC_FREE(events);
 
     return(1);
 
@@ -888,7 +888,7 @@ ddWindowConv4(
     if (high-low < 3) return(ddWindowConv3(table,low,high));
 
     nwin = high-low-2;
-    events = ALLOC(int,nwin);
+    events = ABC_ALLOC(int,nwin);
     if (events == NULL) {
     table->errorCode = CUDD_MEMORY_OUT;
     return(0);
@@ -967,7 +967,7 @@ ddWindowConv4(
             newevent = 1;
             break;
         default:
-            FREE(events);
+            ABC_FREE(events);
             return(0);
         }
         events[x] = 0;
@@ -989,7 +989,7 @@ ddWindowConv4(
 #endif
     } while (newevent);
 
-    FREE(events);
+    ABC_FREE(events);
 
     return(1);
 
diff --git a/src/bdd/cudd/cuddZddCount.c b/src/bdd/cudd/cuddZddCount.c
index 6c6ec1df..bc8a1ee4 100644
--- a/src/bdd/cudd/cuddZddCount.c
+++ b/src/bdd/cudd/cuddZddCount.c
@@ -205,13 +205,13 @@ cuddZddCountStep(
     res = cuddZddCountStep(cuddE(P), table, base, empty) +
     cuddZddCountStep(cuddT(P), table, base, empty);
 
-    dummy = ALLOC(int, 1);
+    dummy = ABC_ALLOC(int, 1);
     if (dummy == NULL) {
     return(CUDD_OUT_OF_MEM);
     }
     *dummy = res;
     if (st_insert(table, (char *)P, (char *)dummy) == ST_OUT_OF_MEM) {
-    FREE(dummy);
+    ABC_FREE(dummy);
     return(CUDD_OUT_OF_MEM);
     }
 
@@ -255,13 +255,13 @@ cuddZddCountDoubleStep(
     res = cuddZddCountDoubleStep(cuddE(P), table, base, empty) +
     cuddZddCountDoubleStep(cuddT(P), table, base, empty);
 
-    dummy = ALLOC(double, 1);
+    dummy = ABC_ALLOC(double, 1);
     if (dummy == NULL) {
     return((double)CUDD_OUT_OF_MEM);
     }
     *dummy = res;
     if (st_insert(table, (char *)P, (char *)dummy) == ST_OUT_OF_MEM) {
-    FREE(dummy);
+    ABC_FREE(dummy);
     return((double)CUDD_OUT_OF_MEM);
     }
 
@@ -291,7 +291,7 @@ st_zdd_countfree(
     int    *d;
 
     d = (int *)value;
-    FREE(d);
+    ABC_FREE(d);
     return(ST_CONTINUE);
 
 } /* end of st_zdd_countfree */
@@ -318,7 +318,7 @@ st_zdd_count_dbl_free(
     double    *d;
 
     d = (double *)value;
-    FREE(d);
+    ABC_FREE(d);
     return(ST_CONTINUE);
 
 } /* end of st_zdd_count_dbl_free */
diff --git a/src/bdd/cudd/cuddZddGroup.c b/src/bdd/cudd/cuddZddGroup.c
index c26ea533..8845dc49 100644
--- a/src/bdd/cudd/cuddZddGroup.c
+++ b/src/bdd/cudd/cuddZddGroup.c
@@ -624,17 +624,17 @@ zddGroupSifting(
     /* Order variables to sift. */
     entry = NULL;
     sifted = NULL;
-    var = ALLOC(int,nvars);
+    var = ABC_ALLOC(int,nvars);
     if (var == NULL) {
     table->errorCode = CUDD_MEMORY_OUT;
     goto zddGroupSiftingOutOfMem;
     }
-    entry = ALLOC(int,nvars);
+    entry = ABC_ALLOC(int,nvars);
     if (entry == NULL) {
     table->errorCode = CUDD_MEMORY_OUT;
     goto zddGroupSiftingOutOfMem;
     }
-    sifted = ALLOC(int,nvars);
+    sifted = ABC_ALLOC(int,nvars);
     if (sifted == NULL) {
     table->errorCode = CUDD_MEMORY_OUT;
     goto zddGroupSiftingOutOfMem;
@@ -700,16 +700,16 @@ zddGroupSifting(
 #endif
     } /* for */
 
-    FREE(sifted);
-    FREE(var);
-    FREE(entry);
+    ABC_FREE(sifted);
+    ABC_FREE(var);
+    ABC_FREE(entry);
 
     return(1);
 
 zddGroupSiftingOutOfMem:
-    if (entry != NULL)    FREE(entry);
-    if (var != NULL)    FREE(var);
-    if (sifted != NULL)    FREE(sifted);
+    if (entry != NULL)    ABC_FREE(entry);
+    if (var != NULL)    ABC_FREE(var);
+    if (sifted != NULL)    ABC_FREE(sifted);
 
     return(0);
 
diff --git a/src/bdd/cudd/cuddZddLin.c b/src/bdd/cudd/cuddZddLin.c
index ef2cd298..4d4135d1 100644
--- a/src/bdd/cudd/cuddZddLin.c
+++ b/src/bdd/cudd/cuddZddLin.c
@@ -140,12 +140,12 @@ cuddZddLinearSifting(
 
     /* Find order in which to sift variables. */
     var = NULL;
-    zdd_entry = ALLOC(int, size);
+    zdd_entry = ABC_ALLOC(int, size);
     if (zdd_entry == NULL) {
     table->errorCode = CUDD_MEMORY_OUT;
     goto cuddZddSiftingOutOfMem;
     }
-    var = ALLOC(int, size);
+    var = ABC_ALLOC(int, size);
     if (var == NULL) {
     table->errorCode = CUDD_MEMORY_OUT;
     goto cuddZddSiftingOutOfMem;
@@ -184,15 +184,15 @@ cuddZddLinearSifting(
 #endif
     }
 
-    FREE(var);
-    FREE(zdd_entry);
+    ABC_FREE(var);
+    ABC_FREE(zdd_entry);
 
     return(1);
 
 cuddZddSiftingOutOfMem:
 
-    if (zdd_entry != NULL) FREE(zdd_entry);
-    if (var != NULL) FREE(var);
+    if (zdd_entry != NULL) ABC_FREE(zdd_entry);
+    if (var != NULL) ABC_FREE(var);
 
     return(0);
 
diff --git a/src/bdd/cudd/cuddZddReord.c b/src/bdd/cudd/cuddZddReord.c
index 6e7d3438..4c6e394b 100644
--- a/src/bdd/cudd/cuddZddReord.c
+++ b/src/bdd/cudd/cuddZddReord.c
@@ -338,7 +338,7 @@ cuddZddAlignToBdd(
     if (M * table->size != table->sizeZ)
     return(0);
     /* Create and initialize the inverse permutation array. */
-    invpermZ = ALLOC(int,table->sizeZ);
+    invpermZ = ABC_ALLOC(int,table->sizeZ);
     if (invpermZ == NULL) {
     table->errorCode = CUDD_MEMORY_OUT;
     return(0);
@@ -358,7 +358,7 @@ cuddZddAlignToBdd(
     cuddGarbageCollectZdd(table,0);
 
     result = zddShuffle(table, invpermZ);
-    FREE(invpermZ);
+    ABC_FREE(invpermZ);
     /* Fix the ZDD variable group tree. */
     zddFixTree(table,table->treeZ);
     return(result);
@@ -852,12 +852,12 @@ cuddZddSifting(
 
     /* Find order in which to sift variables. */
     var = NULL;
-    zdd_entry = ALLOC(int, size);
+    zdd_entry = ABC_ALLOC(int, size);
     if (zdd_entry == NULL) {
     table->errorCode = CUDD_MEMORY_OUT;
     goto cuddZddSiftingOutOfMem;
     }
-    var = ALLOC(int, size);
+    var = ABC_ALLOC(int, size);
     if (var == NULL) {
     table->errorCode = CUDD_MEMORY_OUT;
     goto cuddZddSiftingOutOfMem;
@@ -896,15 +896,15 @@ cuddZddSifting(
 #endif
     }
 
-    FREE(var);
-    FREE(zdd_entry);
+    ABC_FREE(var);
+    ABC_FREE(zdd_entry);
 
     return(1);
 
 cuddZddSiftingOutOfMem:
 
-    if (zdd_entry != NULL) FREE(zdd_entry);
-    if (var != NULL) FREE(var);
+    if (zdd_entry != NULL) ABC_FREE(zdd_entry);
+    if (var != NULL) ABC_FREE(var);
 
     return(0);
 
@@ -1438,7 +1438,7 @@ zddReorderPostprocess(
     slots = oldslots >> 1;
     saveHandler = MMoutOfMemory;
     MMoutOfMemory = Cudd_OutOfMem;
-    nodelist = ALLOC(DdNodePtr, slots);
+    nodelist = ABC_ALLOC(DdNodePtr, slots);
     MMoutOfMemory = saveHandler;
     if (nodelist == NULL) {
         return(1);
@@ -1467,7 +1467,7 @@ zddReorderPostprocess(
         node = next;
         }
     }
-    FREE(oldnodelist);
+    ABC_FREE(oldnodelist);
 
     table->memused += (slots - oldslots) * sizeof(DdNode *);
     table->slots += slots - oldslots;
diff --git a/src/bdd/cudd/cuddZddSymm.c b/src/bdd/cudd/cuddZddSymm.c
index 0930e077..c752c394 100644
--- a/src/bdd/cudd/cuddZddSymm.c
+++ b/src/bdd/cudd/cuddZddSymm.c
@@ -292,12 +292,12 @@ cuddZddSymmSifting(
 
     /* Find order in which to sift variables. */
     var = NULL;
-    zdd_entry = ALLOC(int, nvars);
+    zdd_entry = ABC_ALLOC(int, nvars);
     if (zdd_entry == NULL) {
     table->errorCode = CUDD_MEMORY_OUT;
     goto cuddZddSymmSiftingOutOfMem;
     }
-    var = ALLOC(int, nvars);
+    var = ABC_ALLOC(int, nvars);
     if (var == NULL) {
     table->errorCode = CUDD_MEMORY_OUT;
     goto cuddZddSymmSiftingOutOfMem;
@@ -344,8 +344,8 @@ cuddZddSymmSifting(
     }
     }
 
-    FREE(var);
-    FREE(zdd_entry);
+    ABC_FREE(var);
+    ABC_FREE(zdd_entry);
 
     cuddZddSymmSummary(table, lower, upper, &symvars, &symgroups);
 
@@ -359,9 +359,9 @@ cuddZddSymmSifting(
 cuddZddSymmSiftingOutOfMem:
 
     if (zdd_entry != NULL)
-    FREE(zdd_entry);
+    ABC_FREE(zdd_entry);
     if (var != NULL)
-    FREE(var);
+    ABC_FREE(var);
 
     return(0);
 
@@ -417,12 +417,12 @@ cuddZddSymmSiftingConv(
 
     /* Find order in which to sift variables. */
     var = NULL;
-    zdd_entry = ALLOC(int, nvars);
+    zdd_entry = ABC_ALLOC(int, nvars);
     if (zdd_entry == NULL) {
     table->errorCode = CUDD_MEMORY_OUT;
     goto cuddZddSymmSiftingConvOutOfMem;
     }
-    var = ALLOC(int, nvars);
+    var = ABC_ALLOC(int, nvars);
     if (var == NULL) {
     table->errorCode = CUDD_MEMORY_OUT;
     goto cuddZddSymmSiftingConvOutOfMem;
@@ -532,17 +532,17 @@ cuddZddSymmSiftingConv(
            symgroups);
 #endif
 
-    FREE(var);
-    FREE(zdd_entry);
+    ABC_FREE(var);
+    ABC_FREE(zdd_entry);
 
     return(1+symvars);
 
 cuddZddSymmSiftingConvOutOfMem:
 
     if (zdd_entry != NULL)
-    FREE(zdd_entry);
+    ABC_FREE(zdd_entry);
     if (var != NULL)
-    FREE(var);
+    ABC_FREE(var);
 
     return(0);
 
diff --git a/src/bdd/cudd/cuddZddUtil.c b/src/bdd/cudd/cuddZddUtil.c
index 616d16d4..efa73d15 100644
--- a/src/bdd/cudd/cuddZddUtil.c
+++ b/src/bdd/cudd/cuddZddUtil.c
@@ -105,14 +105,14 @@ Cudd_zddPrintMinterm(
     int        *list;
 
     size = (int)zdd->sizeZ;
-    list = ALLOC(int, size);
+    list = ABC_ALLOC(int, size);
     if (list == NULL) {
     zdd->errorCode = CUDD_MEMORY_OUT;
     return(0);
     }
     for (i = 0; i < size; i++) list[i] = 3; /* bogus value should disappear */
     zdd_print_minterm_aux(zdd, node, 0, list);
-    FREE(list);
+    ABC_FREE(list);
     return(1);
 
 } /* end of Cudd_zddPrintMinterm */
@@ -140,14 +140,14 @@ Cudd_zddPrintCover(
 
     size = (int)zdd->sizeZ;
     if (size % 2 != 0) return(0); /* number of variables should be even */
-    list = ALLOC(int, size);
+    list = ABC_ALLOC(int, size);
     if (list == NULL) {
     zdd->errorCode = CUDD_MEMORY_OUT;
     return(0);
     }
     for (i = 0; i < size; i++) list[i] = 3; /* bogus value should disappear */
     zddPrintCoverAux(zdd, node, 0, list);
-    FREE(list);
+    ABC_FREE(list);
     return(1);
 
 } /* end of Cudd_zddPrintCover */
@@ -251,7 +251,7 @@ Cudd_zddFirstPath(
     if (zdd == NULL || f == NULL) return(NULL);
 
     /* Allocate generator an initialize it. */
-    gen = ALLOC(DdGen,1);
+    gen = ABC_ALLOC(DdGen,1);
     if (gen == NULL) {
     zdd->errorCode = CUDD_MEMORY_OUT;
     return(NULL);
@@ -267,10 +267,10 @@ Cudd_zddFirstPath(
     gen->node = NULL;
 
     nvars = zdd->sizeZ;
-    gen->gen.cubes.cube = ALLOC(int,nvars);
+    gen->gen.cubes.cube = ABC_ALLOC(int,nvars);
     if (gen->gen.cubes.cube == NULL) {
     zdd->errorCode = CUDD_MEMORY_OUT;
-    FREE(gen);
+    ABC_FREE(gen);
     return(NULL);
     }
     for (i = 0; i < nvars; i++) gen->gen.cubes.cube[i] = 2;
@@ -279,11 +279,11 @@ Cudd_zddFirstPath(
     ** because a path may have nodes at all levels, including the
     ** constant level.
     */
-    gen->stack.stack = ALLOC(DdNode *, nvars+1);
+    gen->stack.stack = ABC_ALLOC(DdNode *, nvars+1);
     if (gen->stack.stack == NULL) {
     zdd->errorCode = CUDD_MEMORY_OUT;
-    FREE(gen->gen.cubes.cube);
-    FREE(gen);
+    ABC_FREE(gen->gen.cubes.cube);
+    ABC_FREE(gen);
     return(NULL);
     }
     for (i = 0; i <= nvars; i++) gen->stack.stack[i] = NULL;
@@ -450,7 +450,7 @@ Cudd_zddCoverPathToString(
     if (nvars & 1) return(NULL);
     nvars >>= 1;
     if (str == NULL) {
-    res = ALLOC(char, nvars+1);
+    res = ABC_ALLOC(char, nvars+1);
     if (res == NULL) return(NULL);
     } else {
     res = str;
@@ -532,7 +532,7 @@ Cudd_zddDumpDot(
     long    refAddr, diff, mask;
 
     /* Build a bit array with the support of f. */
-    sorted = ALLOC(int,nvars);
+    sorted = ABC_ALLOC(int,nvars);
     if (sorted == NULL) {
     dd->errorCode = CUDD_MEMORY_OUT;
     goto failure;
@@ -551,7 +551,7 @@ Cudd_zddDumpDot(
     }
     Cudd_RecursiveDeref(dd,support);
     }
-    support = NULL; /* so that we do not try to free it in case of failure */
+    support = NULL; /* so that we do not try to ABC_FREE it in case of failure */
 
     /* Initialize symbol table for visited nodes. */
     visited = st_init_table(st_ptrcmp, st_ptrhash);
@@ -744,11 +744,11 @@ Cudd_zddDumpDot(
     if (retval == EOF) goto failure;
 
     st_free_table(visited);
-    FREE(sorted);
+    ABC_FREE(sorted);
     return(1);
 
 failure:
-    if (sorted != NULL) FREE(sorted);
+    if (sorted != NULL) ABC_FREE(sorted);
     if (support != NULL) Cudd_RecursiveDeref(dd,support);
     if (visited != NULL) st_free_table(visited);
     return(0);
diff --git a/src/bdd/dsd/dsd.h b/src/bdd/dsd/dsd.h
index 4a16bfc1..affdbe6f 100644
--- a/src/bdd/dsd/dsd.h
+++ b/src/bdd/dsd/dsd.h
@@ -28,18 +28,6 @@
 #ifndef __DSD_H__
 #define __DSD_H__
 
-#ifdef __cplusplus
-extern "C" {
-#endif
-
-////////////////////////////////////////////////////////////////////////
-///                      TYPEDEF DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-typedef struct Dsd_Manager_t_   Dsd_Manager_t;
-typedef struct Dsd_Node_t_      Dsd_Node_t;
-typedef enum   Dsd_Type_t_      Dsd_Type_t;
-
 ////////////////////////////////////////////////////////////////////////
 ///                    STRUCTURE DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -48,6 +36,10 @@ typedef enum   Dsd_Type_t_      Dsd_Type_t;
 ///                         PARAMETERS                               ///
 ////////////////////////////////////////////////////////////////////////
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 // types of DSD nodes
 enum Dsd_Type_t_ { 
     DSD_NODE_NONE   = 0,
@@ -59,14 +51,22 @@ enum Dsd_Type_t_ {
 };
 
 ////////////////////////////////////////////////////////////////////////
+///                      TYPEDEF DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Dsd_Manager_t_   Dsd_Manager_t;
+typedef struct Dsd_Node_t_      Dsd_Node_t;
+typedef enum   Dsd_Type_t_      Dsd_Type_t;
+
+////////////////////////////////////////////////////////////////////////
 ///                       MACRO DEFINITIONS                          ///
 ////////////////////////////////////////////////////////////////////////
 
 // complementation and testing for pointers for decomposition entries
-#define Dsd_IsComplement(p)  (((int)((PORT_PTRUINT_T) (p) & 01)))
-#define Dsd_Regular(p)       ((Dsd_Node_t *)((PORT_PTRUINT_T)(p) & ~01)) 
-#define Dsd_Not(p)           ((Dsd_Node_t *)((PORT_PTRUINT_T)(p) ^ 01)) 
-#define Dsd_NotCond(p,c)     ((Dsd_Node_t *)((PORT_PTRUINT_T)(p) ^ (c)))
+#define Dsd_IsComplement(p)  (((int)((ABC_PTRUINT_T) (p) & 01)))
+#define Dsd_Regular(p)       ((Dsd_Node_t *)((ABC_PTRUINT_T)(p) & ~01)) 
+#define Dsd_Not(p)           ((Dsd_Node_t *)((ABC_PTRUINT_T)(p) ^ 01)) 
+#define Dsd_NotCond(p,c)     ((Dsd_Node_t *)((ABC_PTRUINT_T)(p) ^ (c)))
 
 ////////////////////////////////////////////////////////////////////////
 ///                         ITERATORS                                ///
diff --git a/src/bdd/dsd/dsdCheck.c b/src/bdd/dsd/dsdCheck.c
index ce466a71..926237ca 100644
--- a/src/bdd/dsd/dsdCheck.c
+++ b/src/bdd/dsd/dsdCheck.c
@@ -61,7 +61,7 @@ void Dsd_CheckCacheAllocate( int nEntries )
 {
     int nRequested;
 
-    pCache = ALLOC( Dds_Cache_t, 1 );
+    pCache = ABC_ALLOC( Dds_Cache_t, 1 );
     memset( pCache, 0, sizeof(Dds_Cache_t) );
 
     // check what is the size of the current cache
@@ -73,7 +73,7 @@ void Dsd_CheckCacheAllocate( int nEntries )
             Dsd_CheckCacheDeallocate();
         // allocate memory for the hash table
         pCache->nTableSize = nRequested;
-        pCache->pTable = ALLOC( Dsd_Entry_t, nRequested );
+        pCache->pTable = ABC_ALLOC( Dsd_Entry_t, nRequested );
     }
     // otherwise, there is no need to allocate, just clean
     Dsd_CheckCacheClear();
@@ -93,8 +93,8 @@ void Dsd_CheckCacheAllocate( int nEntries )
 ******************************************************************************/
 void Dsd_CheckCacheDeallocate()
 {
-    free( pCache->pTable );
-    free( pCache );
+    ABC_FREE( pCache->pTable );
+    ABC_FREE( pCache );
 }
 
 /**Function********************************************************************
@@ -183,7 +183,7 @@ int Dsd_CheckRootFunctionIdentity_rec( DdManager * dd, DdNode * bF1, DdNode * bF
          pCache->pTable[HKey].bX[3] == bC2 )
     {
         pCache->nSuccess++;
-        return (int)(PORT_PTRUINT_T)pCache->pTable[HKey].bX[4]; // the last bit records the result (yes/no)
+        return (int)(ABC_PTRUINT_T)pCache->pTable[HKey].bX[4]; // the last bit records the result (yes/no)
     }
     else
     {
@@ -302,7 +302,7 @@ int Dsd_CheckRootFunctionIdentity_rec( DdManager * dd, DdNode * bF1, DdNode * bF
         // set cache
         for ( i = 0; i < 4; i++ )
             pCache->pTable[HKey].bX[i] = bA[i];
-        pCache->pTable[HKey].bX[4] = (DdNode*)(PORT_PTRUINT_T)RetValue;
+        pCache->pTable[HKey].bX[4] = (DdNode*)(ABC_PTRUINT_T)RetValue;
 
         return RetValue;
     }
diff --git a/src/bdd/dsd/dsdLocal.c b/src/bdd/dsd/dsdLocal.c
index 6dd6e7d1..98b6d7d0 100644
--- a/src/bdd/dsd/dsdLocal.c
+++ b/src/bdd/dsd/dsdLocal.c
@@ -57,12 +57,12 @@ DdNode * Dsd_TreeGetPrimeFunction( DdManager * dd, Dsd_Node_t * pNode )
     DdNode * bFunc, * bRes, * bTemp;
     st_table * pCache;
     
-    pPermute  = ALLOC( int, dd->size );
-    pVar2Form = ALLOC( int, dd->size );
-    pForm2Var = ALLOC( int, dd->size );
+    pPermute  = ABC_ALLOC( int, dd->size );
+    pVar2Form = ABC_ALLOC( int, dd->size );
+    pForm2Var = ABC_ALLOC( int, dd->size );
 
-    pbCube0 = ALLOC( DdNode *, dd->size );
-    pbCube1 = ALLOC( DdNode *, dd->size );
+    pbCube0 = ABC_ALLOC( DdNode *, dd->size );
+    pbCube1 = ABC_ALLOC( DdNode *, dd->size );
 
     // remap the global function in such a way that
     // the support variables of each formal input are adjacent
@@ -119,11 +119,11 @@ DdNode * Dsd_TreeGetPrimeFunction( DdManager * dd, Dsd_Node_t * pNode )
     Cudd_RecursiveDeref( dd, bTemp );
 ////////////
 */
-    FREE(pPermute);
-    FREE(pVar2Form);
-    FREE(pForm2Var);
-    FREE(pbCube0);
-    FREE(pbCube1);
+    ABC_FREE(pPermute);
+    ABC_FREE(pVar2Form);
+    ABC_FREE(pForm2Var);
+    ABC_FREE(pbCube0);
+    ABC_FREE(pbCube1);
 
     Cudd_Deref( bRes );
     return bRes;
diff --git a/src/bdd/dsd/dsdMan.c b/src/bdd/dsd/dsdMan.c
index 6e43f0f4..6df6a15e 100644
--- a/src/bdd/dsd/dsdMan.c
+++ b/src/bdd/dsd/dsdMan.c
@@ -49,15 +49,15 @@ Dsd_Manager_t * Dsd_ManagerStart( DdManager * dd, int nSuppMax, int fVerbose )
 
     assert( nSuppMax <= dd->size );
 
-    dMan = ALLOC( Dsd_Manager_t, 1 );
+    dMan = ABC_ALLOC( Dsd_Manager_t, 1 );
     memset( dMan, 0, sizeof(Dsd_Manager_t) );
     dMan->dd          = dd;
     dMan->nInputs     = nSuppMax;
     dMan->fVerbose    = fVerbose;
     dMan->nRoots      = 0;
     dMan->nRootsAlloc = 50;
-    dMan->pRoots      = (Dsd_Node_t **) malloc( dMan->nRootsAlloc * sizeof(Dsd_Node_t *) );
-    dMan->pInputs     = (Dsd_Node_t **) malloc( dMan->nInputs     * sizeof(Dsd_Node_t *) );
+    dMan->pRoots      = (Dsd_Node_t **) ABC_ALLOC( char, dMan->nRootsAlloc * sizeof(Dsd_Node_t *) );
+    dMan->pInputs     = (Dsd_Node_t **) ABC_ALLOC( char, dMan->nInputs     * sizeof(Dsd_Node_t *) );
 
     // create the primary inputs and insert them into the table
     dMan->Table       = st_init_table(st_ptrcmp, st_ptrhash);
@@ -103,9 +103,9 @@ void Dsd_ManagerStop( Dsd_Manager_t * dMan )
     st_foreach_item( dMan->Table, gen, (char**)&bFunc, (char**)&pNode )
         Dsd_TreeNodeDelete( dMan->dd, Dsd_Regular(pNode) );
     st_free_table(dMan->Table);
-    free( dMan->pInputs );
-    free( dMan->pRoots );
-    free( dMan );
+    ABC_FREE( dMan->pInputs );
+    ABC_FREE( dMan->pRoots );
+    ABC_FREE( dMan );
     Dsd_CheckCacheDeallocate();
 }
 
diff --git a/src/bdd/dsd/dsdProc.c b/src/bdd/dsd/dsdProc.c
index 45c0986f..0192346c 100644
--- a/src/bdd/dsd/dsdProc.c
+++ b/src/bdd/dsd/dsdProc.c
@@ -129,9 +129,9 @@ s_Loops2Useless = 0;
     if ( pDsdMan->nRootsAlloc < nFuncs )
     {
         if ( pDsdMan->nRootsAlloc > 0 )
-            free( pDsdMan->pRoots );
+            ABC_FREE( pDsdMan->pRoots );
         pDsdMan->nRootsAlloc = nFuncs;
-        pDsdMan->pRoots = (Dsd_Node_t **) malloc( pDsdMan->nRootsAlloc * sizeof(Dsd_Node_t *) );
+        pDsdMan->pRoots = (Dsd_Node_t **) ABC_ALLOC( char, pDsdMan->nRootsAlloc * sizeof(Dsd_Node_t *) );
     }
 
     if ( pDsdMan->fVerbose )
diff --git a/src/bdd/dsd/dsdTree.c b/src/bdd/dsd/dsdTree.c
index 5d69f2f4..a4641afc 100644
--- a/src/bdd/dsd/dsdTree.c
+++ b/src/bdd/dsd/dsdTree.c
@@ -56,13 +56,13 @@ static int s_GateSizeMax;
 Dsd_Node_t * Dsd_TreeNodeCreate( int Type, int nDecs, int BlockNum )
 {
     // allocate memory for this node 
-    Dsd_Node_t * p = (Dsd_Node_t *) malloc( sizeof(Dsd_Node_t) );
+    Dsd_Node_t * p = (Dsd_Node_t *) ABC_ALLOC( char, sizeof(Dsd_Node_t) );
     memset( p, 0, sizeof(Dsd_Node_t) );
     p->Type       = Type;       // the type of this block
     p->nDecs      = nDecs;      // the number of decompositions
     if ( p->nDecs )
     {
-        p->pDecs      = (Dsd_Node_t **) malloc( p->nDecs * sizeof(Dsd_Node_t *) );
+        p->pDecs      = (Dsd_Node_t **) ABC_ALLOC( char, p->nDecs * sizeof(Dsd_Node_t *) );
         p->pDecs[0]   = NULL;
     }
     return p;
@@ -83,8 +83,8 @@ void Dsd_TreeNodeDelete( DdManager * dd, Dsd_Node_t * pNode )
 {
     if ( pNode->G )  Cudd_RecursiveDeref( dd, pNode->G );
     if ( pNode->S )  Cudd_RecursiveDeref( dd, pNode->S );
-    FREE( pNode->pDecs );
-    FREE( pNode );
+    ABC_FREE( pNode->pDecs );
+    ABC_FREE( pNode );
 }
 
 /**Function*************************************************************
@@ -555,7 +555,7 @@ Dsd_Node_t ** Dsd_TreeCollectNodesDfs( Dsd_Manager_t * pDsdMan, int * pnNodes )
 
     nNodesAlloc = Dsd_TreeCountNonTerminalNodes(pDsdMan);
     nNodes  = 0;
-    ppNodes = ALLOC( Dsd_Node_t *, nNodesAlloc );
+    ppNodes = ABC_ALLOC( Dsd_Node_t *, nNodesAlloc );
     for ( i = 0; i < pDsdMan->nRoots; i++ )
         Dsd_TreeCollectNodesDfs_rec( Dsd_Regular(pDsdMan->pRoots[i]), ppNodes, &nNodes );
     Dsd_TreeUnmark( pDsdMan );
@@ -583,7 +583,7 @@ Dsd_Node_t ** Dsd_TreeCollectNodesDfsOne( Dsd_Manager_t * pDsdMan, Dsd_Node_t *
     int nNodes, nNodesAlloc;
     nNodesAlloc = Dsd_TreeCountNonTerminalNodesOne(pNode);
     nNodes  = 0;
-    ppNodes = ALLOC( Dsd_Node_t *, nNodesAlloc );
+    ppNodes = ABC_ALLOC( Dsd_Node_t *, nNodesAlloc );
     Dsd_TreeCollectNodesDfs_rec( Dsd_Regular(pNode), ppNodes, &nNodes );
     Dsd_TreeUnmark_rec(Dsd_Regular(pNode));
     assert( nNodesAlloc == nNodes );
@@ -682,7 +682,7 @@ void Dsd_TreePrint_rec( FILE * pFile, Dsd_Node_t * pNode, int fComp, char * pInp
         fprintf( pFile, "%s = ", pOutputName );
     else
         fprintf( pFile, "NOT(%s) = ", pOutputName );
-    pInputNums = ALLOC( int, pNode->nDecs );
+    pInputNums = ABC_ALLOC( int, pNode->nDecs );
     if ( pNode->Type == DSD_NODE_CONST1 )
     {
          fprintf( pFile, " Constant 1.\n" );
@@ -815,7 +815,7 @@ void Dsd_TreePrint_rec( FILE * pFile, Dsd_Node_t * pNode, int fComp, char * pInp
                 Dsd_TreePrint_rec( pFile, Dsd_Regular( pNode->pDecs[i] ), 0, pInputNames, Buffer, nOffset + 6, pSigCounter, fShortNames );
             }
     }
-    free( pInputNums );
+    ABC_FREE( pInputNums );
 }
 
 /**Function*************************************************************
@@ -863,7 +863,7 @@ void Dsd_NodePrint_rec( FILE * pFile, Dsd_Node_t * pNode, int fComp, char * pOut
         fprintf( pFile, "%s = ", pOutputName );
     else
         fprintf( pFile, "NOT(%s) = ", pOutputName );
-    pInputNums = ALLOC( int, pNode->nDecs );
+    pInputNums = ABC_ALLOC( int, pNode->nDecs );
     if ( pNode->Type == DSD_NODE_CONST1 )
     {
         fprintf( pFile, " Constant 1.\n" );
@@ -984,7 +984,7 @@ void Dsd_NodePrint_rec( FILE * pFile, Dsd_Node_t * pNode, int fComp, char * pOut
                 Dsd_NodePrint_rec( pFile, Dsd_Regular( pNode->pDecs[i] ), 0, Buffer, nOffset + 6, pSigCounter );
             }
     }
-    free( pInputNums );
+    ABC_FREE( pInputNums );
 }
 
 
diff --git a/src/bdd/epd/epd.c b/src/bdd/epd/epd.c
index a80240bc..50da97c4 100644
--- a/src/bdd/epd/epd.c
+++ b/src/bdd/epd/epd.c
@@ -45,7 +45,7 @@ EpdAlloc()
 {
   EpDouble    *epd;
 
-  epd = ALLOC(EpDouble, 1);
+  epd = ABC_ALLOC(EpDouble, 1);
   return(epd);
 }
 
@@ -88,7 +88,7 @@ EpdCmp(const char *key1, const char *key2)
 void
 EpdFree(EpDouble *epd)
 {
-  FREE(epd);
+  ABC_FREE(epd);
 }
 
 
diff --git a/src/bdd/mtr/mtrBasic.c b/src/bdd/mtr/mtrBasic.c
index 94105282..428fa0b1 100644
--- a/src/bdd/mtr/mtrBasic.c
+++ b/src/bdd/mtr/mtrBasic.c
@@ -92,7 +92,7 @@ Mtr_AllocNode(
 {
     MtrNode *node;
 
-    node = ALLOC(MtrNode,1);
+    node = ABC_ALLOC(MtrNode,1);
     return node;
 
 } /* Mtr_AllocNode */
@@ -113,7 +113,7 @@ void
 Mtr_DeallocNode(
   MtrNode * node /* node to be deallocated */)
 {
-    FREE(node);
+    ABC_FREE(node);
     return;
 
 } /* end of Mtr_DeallocNode */
diff --git a/src/bdd/parse/parseCore.c b/src/bdd/parse/parseCore.c
index 88888379..85200dd9 100644
--- a/src/bdd/parse/parseCore.c
+++ b/src/bdd/parse/parseCore.c
@@ -156,7 +156,7 @@ DdNode * Parse_FormulaParser( FILE * pOutput, char * pFormulaInit, int nVars, in
     }
 
     // copy the formula
-    pFormula = ALLOC( char, strlen(pFormulaInit) + 3 );
+    pFormula = ABC_ALLOC( char, strlen(pFormulaInit) + 3 );
     sprintf( pFormula, "(%s)", pFormulaInit );
 
     // start the stacks
@@ -335,7 +335,7 @@ DdNode * Parse_FormulaParser( FILE * pOutput, char * pFormulaInit, int nVars, in
                     if ( Parse_ParserPerformTopOp( dd, pStackFn, Oper ) == NULL )
                     {
                         fprintf( pOutput, "Parse_FormulaParser(): Unknown operation\n" );
-                        free( pFormula );
+                        ABC_FREE( pFormula );
                         return NULL;
                     }
                 }
@@ -382,7 +382,8 @@ DdNode * Parse_FormulaParser( FILE * pOutput, char * pFormulaInit, int nVars, in
             for ( i = 0; pTemp[i] && pTemp[i] != ' ' && pTemp[i] != '\t' && pTemp[i] != '\r' && pTemp[i] != '\n' && 
                          pTemp[i] != PARSE_SYM_AND1 && pTemp[i] != PARSE_SYM_AND2 && pTemp[i] != PARSE_SYM_XOR1 &&
                          pTemp[i] != PARSE_SYM_XOR2 && pTemp[i] != PARSE_SYM_XOR3 && pTemp[i] != PARSE_SYM_XOR  &&
-                         pTemp[i] != PARSE_SYM_OR1  && pTemp[i] != PARSE_SYM_OR2  && pTemp[i] != PARSE_SYM_CLOSE;
+                         pTemp[i] != PARSE_SYM_OR1  && pTemp[i] != PARSE_SYM_OR2  && pTemp[i] != PARSE_SYM_CLOSE &&
+                         pTemp[i] != PARSE_SYM_NEGAFT;
                   i++ )
             {}
             for ( v = 0; v < nVars; v++ ) 
@@ -446,7 +447,7 @@ DdNode * Parse_FormulaParser( FILE * pOutput, char * pFormulaInit, int nVars, in
                     if ( Parse_ParserPerformTopOp( dd, pStackFn, Oper2 ) == NULL )
                     {
                         fprintf( pOutput, "Parse_FormulaParser(): Unknown operation\n" );
-                        free( pFormula );
+                        ABC_FREE( pFormula );
                         return NULL;
                     }
                     Parse_StackOpPush( pStackOp,  Oper1 );     // push the last operation back
@@ -471,7 +472,7 @@ DdNode * Parse_FormulaParser( FILE * pOutput, char * pFormulaInit, int nVars, in
                     Parse_StackFnFree(pStackFn);
                     Parse_StackOpFree(pStackOp);
                     Cudd_Deref( bFunc );
-                    free( pFormula );
+                    ABC_FREE( pFormula );
                     return bFunc;
                 }
                 else
@@ -482,7 +483,7 @@ DdNode * Parse_FormulaParser( FILE * pOutput, char * pFormulaInit, int nVars, in
         else
             fprintf( pOutput, "Parse_FormulaParser(): The input string is empty\n" );
     }
-    free( pFormula );
+    ABC_FREE( pFormula );
     return NULL;
 }
 
diff --git a/src/bdd/parse/parseEqn.c b/src/bdd/parse/parseEqn.c
index 02d83966..eceecc0c 100644
--- a/src/bdd/parse/parseEqn.c
+++ b/src/bdd/parse/parseEqn.c
@@ -91,7 +91,7 @@ Hop_Obj_t * Parse_FormulaParserEqn( FILE * pOutput, char * pFormInit, Vec_Ptr_t
     }
 
     // copy the formula
-    pFormula = ALLOC( char, strlen(pFormInit) + 3 );
+    pFormula = ABC_ALLOC( char, strlen(pFormInit) + 3 );
     sprintf( pFormula, "(%s)", pFormInit );
 
     // start the stacks
@@ -182,7 +182,7 @@ Hop_Obj_t * Parse_FormulaParserEqn( FILE * pOutput, char * pFormInit, Vec_Ptr_t
                     if ( Parse_ParserPerformTopOp( pMan, pStackFn, Oper ) == NULL )
                     {
                         fprintf( pOutput, "Parse_FormulaParserEqn(): Unknown operation\n" );
-                        free( pFormula );
+                        ABC_FREE( pFormula );
                         return NULL;
                     }
                 }
@@ -273,7 +273,7 @@ Hop_Obj_t * Parse_FormulaParserEqn( FILE * pOutput, char * pFormInit, Vec_Ptr_t
                     if ( Parse_ParserPerformTopOp( pMan, pStackFn, Oper2 ) == NULL )
                     {
                         fprintf( pOutput, "Parse_FormulaParserEqn(): Unknown operation\n" );
-                        free( pFormula );
+                        ABC_FREE( pFormula );
                         return NULL;
                     }
                     Parse_StackOpPush( pStackOp,  Oper1 );     // push the last operation back
@@ -298,7 +298,7 @@ Hop_Obj_t * Parse_FormulaParserEqn( FILE * pOutput, char * pFormInit, Vec_Ptr_t
                     Parse_StackFnFree(pStackFn);
                     Parse_StackOpFree(pStackOp);
 //                    Cudd_Deref( gFunc );
-                    free( pFormula );
+                    ABC_FREE( pFormula );
                     return gFunc;
                 }
                 else
@@ -309,7 +309,7 @@ Hop_Obj_t * Parse_FormulaParserEqn( FILE * pOutput, char * pFormInit, Vec_Ptr_t
         else
             fprintf( pOutput, "Parse_FormulaParserEqn(): The input string is empty\n" );
     }
-    free( pFormula );
+    ABC_FREE( pFormula );
     return NULL;
 }
 
diff --git a/src/bdd/parse/parseStack.c b/src/bdd/parse/parseStack.c
index cd7cd7e3..7ce488f1 100644
--- a/src/bdd/parse/parseStack.c
+++ b/src/bdd/parse/parseStack.c
@@ -54,9 +54,9 @@ struct ParseStackOpStruct
 Parse_StackFn_t * Parse_StackFnStart( int nDepth )
 {
     Parse_StackFn_t * p;
-    p = ALLOC( Parse_StackFn_t, 1 );
+    p = ABC_ALLOC( Parse_StackFn_t, 1 );
     memset( p, 0, sizeof(Parse_StackFn_t) );
-    p->pData = ALLOC( void *, nDepth );
+    p->pData = ABC_ALLOC( void *, nDepth );
     p->Size = nDepth;
     return p;
 }
@@ -132,8 +132,8 @@ void * Parse_StackFnPop( Parse_StackFn_t * p )
 ***********************************************************************/
 void Parse_StackFnFree( Parse_StackFn_t * p )
 {
-    FREE( p->pData );
-    FREE( p );
+    ABC_FREE( p->pData );
+    ABC_FREE( p );
 }
 
 
@@ -153,9 +153,9 @@ void Parse_StackFnFree( Parse_StackFn_t * p )
 Parse_StackOp_t * Parse_StackOpStart( int nDepth )
 {
     Parse_StackOp_t * p;
-    p = ALLOC( Parse_StackOp_t, 1 );
+    p = ABC_ALLOC( Parse_StackOp_t, 1 );
     memset( p, 0, sizeof(Parse_StackOp_t) );
-    p->pData = ALLOC( int, nDepth );
+    p->pData = ABC_ALLOC( int, nDepth );
     p->Size = nDepth;
     return p;
 }
@@ -231,8 +231,8 @@ int Parse_StackOpPop( Parse_StackOp_t * p )
 ***********************************************************************/
 void Parse_StackOpFree( Parse_StackOp_t * p )
 {
-    FREE( p->pData );
-    FREE( p );
+    ABC_FREE( p->pData );
+    ABC_FREE( p );
 }
 
 
diff --git a/src/bdd/reo/reo.h b/src/bdd/reo/reo.h
index 24e12c32..2f9c421e 100644
--- a/src/bdd/reo/reo.h
+++ b/src/bdd/reo/reo.h
@@ -19,20 +19,18 @@
 #ifndef __REO_H__
 #define __REO_H__
 
-#ifdef __cplusplus
-extern "C" {
-#endif
-
 #include <stdio.h>
 #include <stdlib.h>
 #include "extra.h"
 
-//#pragma warning( disable : 4514 )
-
 ////////////////////////////////////////////////////////////////////////
 ///                     MACRO DEFINITIONS                            ///
 ////////////////////////////////////////////////////////////////////////
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 // reordering parameters
 #define REO_REORDER_LIMIT      1.15  // determines the quality/runtime trade-off
 #define REO_QUAL_PAR              3  // the quality [1 = simple lower bound, 2 = strict, larger = heuristic]
@@ -171,9 +169,9 @@ struct _reo_man
 };
 
 // used to manipulate units
-#define Unit_Regular(u)     ((reo_unit *)((PORT_PTRUINT_T)(u) & ~01))
-#define Unit_Not(u)         ((reo_unit *)((PORT_PTRUINT_T)(u) ^ 01))
-#define Unit_NotCond(u,c)   ((reo_unit *)((PORT_PTRUINT_T)(u) ^ (c)))
+#define Unit_Regular(u)     ((reo_unit *)((ABC_PTRUINT_T)(u) & ~01))
+#define Unit_Not(u)         ((reo_unit *)((ABC_PTRUINT_T)(u) ^ 01))
+#define Unit_NotCond(u,c)   ((reo_unit *)((ABC_PTRUINT_T)(u) ^ (c)))
 #define Unit_IsConstant(u)  ((int)((u)->lev == REO_CONST_LEVEL))
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/bdd/reo/reoApi.c b/src/bdd/reo/reoApi.c
index e833dabd..000489ed 100644
--- a/src/bdd/reo/reoApi.c
+++ b/src/bdd/reo/reoApi.c
@@ -48,7 +48,7 @@ reo_man * Extra_ReorderInit( int nDdVarsMax, int nNodesMax )
 {
     reo_man * p;
     // allocate and clean the data structure
-    p = ALLOC( reo_man, 1 );
+    p = ABC_ALLOC( reo_man, 1 );
     memset( p, 0, sizeof(reo_man) );
     // resize the manager to meet user's needs    
     reoResizeStructures( p, nDdVarsMax, nNodesMax, 100 );
@@ -75,21 +75,21 @@ reo_man * Extra_ReorderInit( int nDdVarsMax, int nNodesMax )
 ***********************************************************************/
 void Extra_ReorderQuit( reo_man * p )
 {
-    free( p->pTops );
-    free( p->pSupp );
-    free( p->pOrderInt );
-    free( p->pWidthCofs );
-    free( p->pMapToPlanes );
-    free( p->pMapToDdVarsOrig );
-    free( p->pMapToDdVarsFinal );
-    free( p->pPlanes );
-    free( p->pVarCosts );
-    free( p->pLevelOrder );
-    free( p->HTable );
-    free( p->pRefNodes );
+    ABC_FREE( p->pTops );
+    ABC_FREE( p->pSupp );
+    ABC_FREE( p->pOrderInt );
+    ABC_FREE( p->pWidthCofs );
+    ABC_FREE( p->pMapToPlanes );
+    ABC_FREE( p->pMapToDdVarsOrig );
+    ABC_FREE( p->pMapToDdVarsFinal );
+    ABC_FREE( p->pPlanes );
+    ABC_FREE( p->pVarCosts );
+    ABC_FREE( p->pLevelOrder );
+    ABC_FREE( p->HTable );
+    ABC_FREE( p->pRefNodes );
     reoUnitsStopDispenser( p );
-    free( p->pMemChunks );
-    free( p );
+    ABC_FREE( p->pMemChunks );
+    ABC_FREE( p );
 }
 
 /**Function*************************************************************
diff --git a/src/bdd/reo/reoCore.c b/src/bdd/reo/reoCore.c
index 3782631c..a37bae13 100644
--- a/src/bdd/reo/reoCore.c
+++ b/src/bdd/reo/reoCore.c
@@ -22,8 +22,6 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-#define CALLOC(type, num)  ((type *) calloc((long)(num), (long)sizeof(type)))
-
 static int  reoRecursiveDeref( reo_unit * pUnit );
 static int  reoCheckZeroRefs( reo_plane * pPlane );
 static int  reoCheckLevels( reo_man * p );
@@ -217,7 +215,7 @@ s_AplAfter  = p->nAplEnd;
 
         if ( p->pOrder == NULL )
         {
-            pOrder = ALLOC( int, p->nSupp );
+            pOrder = ABC_ALLOC( int, p->nSupp );
             for ( i = 0; i < p->nSupp; i++ )
                 pOrder[ p->pMapToDdVarsFinal[i] ] = p->pMapToDdVarsOrig[ p->pOrderInt[i] ]; 
         }
@@ -246,7 +244,7 @@ s_AplAfter  = p->nAplEnd;
             printf( "REO: Internal verification is okay!\n" );
 
         if ( p->pOrder == NULL )
-            free( pOrder );
+            ABC_FREE( pOrder );
     }
 
     // recycle the data structure
@@ -270,35 +268,35 @@ void reoResizeStructures( reo_man * p, int nDdVarsMax, int nNodesMax, int nFuncs
     // resize data structures depending on the number of variables in the DD manager
     if ( p->nSuppAlloc == 0 )
     {
-        p->pSupp             = ALLOC( int,        nDdVarsMax + 1 );
-        p->pOrderInt         = ALLOC( int,        nDdVarsMax + 1 );
-        p->pMapToPlanes      = ALLOC( int,        nDdVarsMax + 1 );
-        p->pMapToDdVarsOrig  = ALLOC( int,        nDdVarsMax + 1 );
-        p->pMapToDdVarsFinal = ALLOC( int,        nDdVarsMax + 1 );
-        p->pPlanes           = CALLOC( reo_plane, nDdVarsMax + 1 );
-        p->pVarCosts         = ALLOC( double,     nDdVarsMax + 1 );
-        p->pLevelOrder       = ALLOC( int,        nDdVarsMax + 1 );
+        p->pSupp             = ABC_ALLOC( int,        nDdVarsMax + 1 );
+        p->pOrderInt         = ABC_ALLOC( int,        nDdVarsMax + 1 );
+        p->pMapToPlanes      = ABC_ALLOC( int,        nDdVarsMax + 1 );
+        p->pMapToDdVarsOrig  = ABC_ALLOC( int,        nDdVarsMax + 1 );
+        p->pMapToDdVarsFinal = ABC_ALLOC( int,        nDdVarsMax + 1 );
+        p->pPlanes           = ABC_CALLOC( reo_plane, nDdVarsMax + 1 );
+        p->pVarCosts         = ABC_ALLOC( double,     nDdVarsMax + 1 );
+        p->pLevelOrder       = ABC_ALLOC( int,        nDdVarsMax + 1 );
         p->nSuppAlloc        = nDdVarsMax + 1;
     }
     else if ( p->nSuppAlloc < nDdVarsMax )
     {
-        free( p->pSupp );
-        free( p->pOrderInt );
-        free( p->pMapToPlanes );
-        free( p->pMapToDdVarsOrig );
-        free( p->pMapToDdVarsFinal );
-        free( p->pPlanes );
-        free( p->pVarCosts );
-        free( p->pLevelOrder );
-
-        p->pSupp             = ALLOC( int,        nDdVarsMax + 1 );
-        p->pOrderInt         = ALLOC( int,        nDdVarsMax + 1 );
-        p->pMapToPlanes      = ALLOC( int,        nDdVarsMax + 1 );
-        p->pMapToDdVarsOrig  = ALLOC( int,        nDdVarsMax + 1 );
-        p->pMapToDdVarsFinal = ALLOC( int,        nDdVarsMax + 1 );
-        p->pPlanes           = CALLOC( reo_plane, nDdVarsMax + 1 );
-        p->pVarCosts         = ALLOC( double,     nDdVarsMax + 1 );
-        p->pLevelOrder       = ALLOC( int,        nDdVarsMax + 1 );
+        ABC_FREE( p->pSupp );
+        ABC_FREE( p->pOrderInt );
+        ABC_FREE( p->pMapToPlanes );
+        ABC_FREE( p->pMapToDdVarsOrig );
+        ABC_FREE( p->pMapToDdVarsFinal );
+        ABC_FREE( p->pPlanes );
+        ABC_FREE( p->pVarCosts );
+        ABC_FREE( p->pLevelOrder );
+
+        p->pSupp             = ABC_ALLOC( int,        nDdVarsMax + 1 );
+        p->pOrderInt         = ABC_ALLOC( int,        nDdVarsMax + 1 );
+        p->pMapToPlanes      = ABC_ALLOC( int,        nDdVarsMax + 1 );
+        p->pMapToDdVarsOrig  = ABC_ALLOC( int,        nDdVarsMax + 1 );
+        p->pMapToDdVarsFinal = ABC_ALLOC( int,        nDdVarsMax + 1 );
+        p->pPlanes           = ABC_CALLOC( reo_plane, nDdVarsMax + 1 );
+        p->pVarCosts         = ABC_ALLOC( double,     nDdVarsMax + 1 );
+        p->pLevelOrder       = ABC_ALLOC( int,        nDdVarsMax + 1 );
         p->nSuppAlloc        = nDdVarsMax + 1;
     }
 
@@ -310,10 +308,10 @@ void reoResizeStructures( reo_man * p, int nDdVarsMax, int nNodesMax, int nFuncs
         p->nRefNodesAlloc  = 3*nNodesMax + 1;
         p->nMemChunksAlloc = (10*nNodesMax + 1)/REO_CHUNK_SIZE + 1;
 
-        p->HTable          = CALLOC( reo_hash,  p->nTableSize );
-        p->pRefNodes       = ALLOC( DdNode *,   p->nRefNodesAlloc );
-        p->pWidthCofs      = ALLOC( reo_unit *, p->nRefNodesAlloc );
-        p->pMemChunks      = ALLOC( reo_unit *, p->nMemChunksAlloc );
+        p->HTable          = ABC_CALLOC( reo_hash,  p->nTableSize );
+        p->pRefNodes       = ABC_ALLOC( DdNode *,   p->nRefNodesAlloc );
+        p->pWidthCofs      = ABC_ALLOC( reo_unit *, p->nRefNodesAlloc );
+        p->pMemChunks      = ABC_ALLOC( reo_unit *, p->nMemChunksAlloc );
     }
     else if ( p->nNodesMaxAlloc < nNodesMax )
     {
@@ -325,29 +323,29 @@ void reoResizeStructures( reo_man * p, int nDdVarsMax, int nNodesMax, int nFuncs
         p->nRefNodesAlloc  = 3*nNodesMax + 1;
         p->nMemChunksAlloc = (10*nNodesMax + 1)/REO_CHUNK_SIZE + 1;
 
-        free( p->HTable );
-        free( p->pRefNodes );
-        free( p->pWidthCofs );
-        p->HTable          = CALLOC( reo_hash,    p->nTableSize );
-        p->pRefNodes       = ALLOC(  DdNode *,    p->nRefNodesAlloc );
-        p->pWidthCofs      = ALLOC(  reo_unit *,  p->nRefNodesAlloc );
+        ABC_FREE( p->HTable );
+        ABC_FREE( p->pRefNodes );
+        ABC_FREE( p->pWidthCofs );
+        p->HTable          = ABC_CALLOC( reo_hash,    p->nTableSize );
+        p->pRefNodes       = ABC_ALLOC(  DdNode *,    p->nRefNodesAlloc );
+        p->pWidthCofs      = ABC_ALLOC(  reo_unit *,  p->nRefNodesAlloc );
         // p->pMemChunks should be reallocated because it contains pointers currently in use
-        pTemp              = ALLOC(  reo_unit *,  p->nMemChunksAlloc );
+        pTemp              = ABC_ALLOC(  reo_unit *,  p->nMemChunksAlloc );
         memmove( pTemp, p->pMemChunks, sizeof(reo_unit *) * nMemChunksAllocPrev );
-        free( p->pMemChunks );
+        ABC_FREE( p->pMemChunks );
         p->pMemChunks      = pTemp;
     }
 
     // resize the data structures depending on the number of functions
     if ( p->nTopsAlloc == 0 )
     {
-        p->pTops      = ALLOC( reo_unit *, nFuncs );
+        p->pTops      = ABC_ALLOC( reo_unit *, nFuncs );
         p->nTopsAlloc = nFuncs;
     }
     else if ( p->nTopsAlloc < nFuncs )
     {
-        free( p->pTops );
-        p->pTops      = ALLOC( reo_unit *, nFuncs );
+        ABC_FREE( p->pTops );
+        p->pTops      = ABC_ALLOC( reo_unit *, nFuncs );
         p->nTopsAlloc = nFuncs;
     }
 }
diff --git a/src/bdd/reo/reoProfile.c b/src/bdd/reo/reoProfile.c
index 84a0bc19..8a48d809 100644
--- a/src/bdd/reo/reoProfile.c
+++ b/src/bdd/reo/reoProfile.c
@@ -132,8 +132,8 @@ void reoProfileWidthStart( reo_man * p )
     int v;
 
     // allocate and clean the storage for starting and stopping levels
-    pWidthStart = ALLOC( int, p->nSupp + 1 );
-    pWidthStop  = ALLOC( int, p->nSupp + 1 );
+    pWidthStart = ABC_ALLOC( int, p->nSupp + 1 );
+    pWidthStop  = ABC_ALLOC( int, p->nSupp + 1 );
     memset( pWidthStart, 0, sizeof(int) * (p->nSupp + 1) );
     memset( pWidthStop, 0, sizeof(int) * (p->nSupp + 1) );
 
@@ -200,8 +200,8 @@ void reoProfileWidthStart( reo_man * p )
 //        printf( "Level %2d: Width = %5d. Correct = %d.\n", v, Temp, p->pPlanes[v].statsWidth );
     }
     p->nWidthBeg = p->nWidthCur;
-    free( pWidthStart );
-    free( pWidthStop );
+    ABC_FREE( pWidthStart );
+    ABC_FREE( pWidthStop );
 }
 
 /**Function********************************************************************
diff --git a/src/bdd/reo/reoSwap.c b/src/bdd/reo/reoSwap.c
index d3a9c7a5..0e829407 100644
--- a/src/bdd/reo/reoSwap.c
+++ b/src/bdd/reo/reoSwap.c
@@ -233,7 +233,7 @@ double reoReorderSwapAdjacentVars( reo_man * p, int lev0, int fMovingUp )
     // (2) walk through the uppoer level, and tranform all the remaning nodes 
     //     while employing cache for the new lower level
     // (3) walk through the old lower level, find those nodes whose ref counters are not zero, 
-    //     and move them to the new uppoer level, free other nodes
+    //     and move them to the new uppoer level, ABC_FREE other nodes
 
     // (1) walk through the upper level, find units without cofactors in the lower level 
     //     and move them to the new lower level (while adding to the cache)
@@ -759,7 +759,7 @@ double reoReorderSwapAdjacentVars( reo_man * p, int lev0, int fMovingUp )
     }
 
     // (3) walk through the old lower level, find those nodes whose ref counters are not zero, 
-    //     and move them to the new uppoer level, free other nodes
+    //     and move them to the new uppoer level, ABC_FREE other nodes
     for ( pLoop = pListOld1; pLoop; )
     {
         pUnit = pLoop;
diff --git a/src/bdd/reo/reoTest.c b/src/bdd/reo/reoTest.c
index 82f3d5f5..f0e70cf9 100644
--- a/src/bdd/reo/reoTest.c
+++ b/src/bdd/reo/reoTest.c
@@ -115,9 +115,9 @@ DdNode * Extra_ReorderCudd( DdManager * dd, DdNode * aFunc, int pPermuteReo[] )
     // start the reordering manager
     if ( ddReorder == NULL )
     {
-        Permute       = ALLOC( int, dd->size );
-        PermuteReo1   = ALLOC( int, dd->size );
-        PermuteReo2   = ALLOC( int, dd->size );
+        Permute       = ABC_ALLOC( int, dd->size );
+        PermuteReo1   = ABC_ALLOC( int, dd->size );
+        PermuteReo2   = ABC_ALLOC( int, dd->size );
         ddReorder = Cudd_Init( dd->size, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
         Cudd_AutodynDisable(ddReorder);
     }
diff --git a/src/bdd/reo/reoTransfer.c b/src/bdd/reo/reoTransfer.c
index 26a6689e..ec02ac0c 100644
--- a/src/bdd/reo/reoTransfer.c
+++ b/src/bdd/reo/reoTransfer.c
@@ -69,7 +69,7 @@ reo_unit * reoTransferNodesToUnits_rec( reo_man * p, DdNode * F )
     if ( cuddIsConstant(F) )
     {
         pUnit->lev    = REO_CONST_LEVEL;
-        pUnit->pE     = (reo_unit*)((int)(PORT_PTRUINT_T)(cuddV(F)));
+        pUnit->pE     = (reo_unit*)((int)(ABC_PTRUINT_T)(cuddV(F)));
         pUnit->pT     = NULL;
         // check if the diagram that is being reordering has complement edges
         if ( F != dd->one )
@@ -89,7 +89,7 @@ reo_unit * reoTransferNodesToUnits_rec( reo_man * p, DdNode * F )
     // add to the hash table
     if ( F->ref != 1 )
     {
-        // the next free entry is already found - it is pointed to by HKey
+        // the next ABC_FREE entry is already found - it is pointed to by HKey
         // while we traversed the diagram, the hash entry to which HKey points,
         // might have been used. Make sure that its signature is different.
         for ( ; p->HTable[HKey].Sign == p->Signature; HKey = (HKey+1) % p->nTableSize );
@@ -139,7 +139,7 @@ DdNode * reoTransferUnitsToNodes_rec( reo_man * p, reo_unit * pUnit )
     // treat the case of constants
     if ( Unit_IsConstant(pUnit) )
     {
-        bRes = cuddUniqueConst( dd, ((double)((int)(PORT_PTRUINT_T)(pUnit->pE))) );
+        bRes = cuddUniqueConst( dd, ((double)((int)(ABC_PTRUINT_T)(pUnit->pE))) );
         cuddRef( bRes );
     }
     else
diff --git a/src/bdd/reo/reoUnits.c b/src/bdd/reo/reoUnits.c
index 52137027..f8bca7ad 100644
--- a/src/bdd/reo/reoUnits.c
+++ b/src/bdd/reo/reoUnits.c
@@ -30,7 +30,7 @@ static void reoUnitsAddToFreeUnitList( reo_man * p );
 
 /**Function*************************************************************
 
-  Synopsis    [Extract the next unit from the free unit list.]
+  Synopsis    [Extract the next unit from the ABC_FREE unit list.]
 
   Description []
 
@@ -54,7 +54,7 @@ reo_unit * reoUnitsGetNextUnit(reo_man * p )
 
 /**Function*************************************************************
 
-  Synopsis    [Returns the unit to the free unit list.]
+  Synopsis    [Returns the unit to the ABC_FREE unit list.]
 
   Description []
 
@@ -72,7 +72,7 @@ void reoUnitsRecycleUnit( reo_man * p, reo_unit * pUnit )
 
 /**Function*************************************************************
 
-  Synopsis    [Returns the list of units to the free unit list.]
+  Synopsis    [Returns the list of units to the ABC_FREE unit list.]
 
   Description []
 
@@ -112,7 +112,7 @@ void reoUnitsStopDispenser( reo_man * p )
 {
     int i;
     for ( i = 0; i < p->nMemChunks; i++ )
-        free( p->pMemChunks[i] );
+        ABC_FREE( p->pMemChunks[i] );
 //    printf("\nThe number of chunks used is %d, each of them %d units\n", p->nMemChunks, REO_CHUNK_SIZE );
     p->nMemChunks = 0;
 }
@@ -167,7 +167,7 @@ void reoUnitsAddToFreeUnitList( reo_man * p )
     }
     // allocate the next chunk
     assert( p->pUnitFreeList == NULL );
-    p->pUnitFreeList = ALLOC( reo_unit, REO_CHUNK_SIZE );
+    p->pUnitFreeList = ABC_ALLOC( reo_unit, REO_CHUNK_SIZE );
     // split chunks into list-connected units
     for ( c = 0; c < REO_CHUNK_SIZE-1; c++ )
         (p->pUnitFreeList + c)->Next = p->pUnitFreeList + c + 1;