Version abc90215

20 files changed, 154 insertions, 169 deletions

diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h
index 84ff272a..3db3e396 100644
--- a/src/aig/saig/saig.h
+++ b/src/aig/saig/saig.h
@@ -21,10 +21,6 @@
 #ifndef __SAIG_H__
 #define __SAIG_H__
 
-#ifdef __cplusplus
-extern "C" {
-#endif
-
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -35,6 +31,10 @@ extern "C" {
 ///                         PARAMETERS                               ///
 ////////////////////////////////////////////////////////////////////////
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                         BASIC TYPES                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -134,7 +134,7 @@ extern int               Saig_MvManSimulate( Aig_Man_t * pAig, int fVerbose );
 /*=== saigStrSim.c ==========================================================*/
 extern Vec_Int_t *       Saig_StrSimPerformMatching( Aig_Man_t * p0, Aig_Man_t * p1, int nDist, int fVerbose, Aig_Man_t ** ppMiter );
 /*=== saigSwitch.c ==========================================================*/
-extern Vec_Int_t *       Saig_ManComputeSwitchProbs( Aig_Man_t * p, int nFrames, int nPref, int fProbOne );
+extern Vec_Int_t *       Saig_ManComputeSwitchProb2s( Aig_Man_t * p, int nFrames, int nPref, int fProbOne );
 /*=== saigSynch.c ==========================================================*/
 extern Aig_Man_t *       Saig_ManDupInitZero( Aig_Man_t * p );
 /*=== saigTrans.c ==========================================================*/
diff --git a/src/aig/saig/saigAbs.c b/src/aig/saig/saigAbs.c
index d2a45b4e..c9e76626 100644
--- a/src/aig/saig/saigAbs.c
+++ b/src/aig/saig/saigAbs.c
@@ -54,7 +54,7 @@ Vec_Int_t * Saig_AbsSolverUnsatCore( sat_solver * pSat, int nConfMax, int fVerbo
     Intp_Man_t * pManProof;
     int RetValue, clk = clock();
     // solve the problem
-    RetValue = sat_solver_solve( pSat, NULL, NULL, (sint64)nConfMax, (sint64)0, (sint64)0, (sint64)0 );
+    RetValue = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)nConfMax, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
     if ( RetValue == l_Undef )
     {
         printf( "Conflict limit is reached.\n" );
@@ -68,7 +68,7 @@ Vec_Int_t * Saig_AbsSolverUnsatCore( sat_solver * pSat, int nConfMax, int fVerbo
     if ( fVerbose )
     {
         printf( "SAT solver returned UNSAT after %d conflicts.  ", pSat->stats.conflicts );
-        PRT( "Time", clock() - clk );
+        ABC_PRT( "Time", clock() - clk );
     }
     assert( RetValue == l_False );
     pSatCnf = sat_solver_store_release( pSat ); 
@@ -81,7 +81,7 @@ Vec_Int_t * Saig_AbsSolverUnsatCore( sat_solver * pSat, int nConfMax, int fVerbo
     if ( fVerbose )
     {
         printf( "SAT core contains %d clauses (out of %d).  ", Vec_IntSize(vCore), pSat->stats.clauses );
-        PRT( "Time", clock() - clk );
+        ABC_PRT( "Time", clock() - clk );
     }
     return vCore;
 }
@@ -458,7 +458,7 @@ Vec_Int_t * Saig_AbsCollectRegistersDyn( Aig_Man_t * p, Vec_Ptr_t * vFrames, Vec
     Vec_PtrForEachEntry( vFrames, pCnf, f )
         nSatVars += pCnf->nVars;
     // mark register variables
-    pVars = ALLOC( int, nSatVars );
+    pVars = ABC_ALLOC( int, nSatVars );
     for ( i = 0; i < nSatVars; i++ )
         pVars[i] = -1;
     Vec_PtrForEachEntry( vFrames, pCnf, f )
@@ -485,7 +485,7 @@ Vec_Int_t * Saig_AbsCollectRegistersDyn( Aig_Man_t * p, Vec_Ptr_t * vFrames, Vec
         }
     }
     // mark used registers
-    pFlops = CALLOC( int, Aig_ManRegNum(p) );
+    pFlops = ABC_CALLOC( int, Aig_ManRegNum(p) );
     Vec_IntForEachEntry( vCore, iClause, i )
     {
         nSatClauses = 0;
@@ -513,8 +513,8 @@ Vec_Int_t * Saig_AbsCollectRegistersDyn( Aig_Man_t * p, Vec_Ptr_t * vFrames, Vec
     for ( i = 0; i < Aig_ManRegNum(p); i++ )
         if ( pFlops[i] )
             Vec_IntPush( vFlops, i );
-    free( pFlops );
-    free( pVars );
+    ABC_FREE( pFlops );
+    ABC_FREE( pVars );
     return vFlops;
 }
 
@@ -536,7 +536,7 @@ Vec_Int_t * Saig_AbsCollectRegisters( Cnf_Dat_t * pCnf, int nFrames, Vec_Int_t *
     int * pVars, * pFlops;
     int i, iClause, iReg, * piLit;
     // mark register variables
-    pVars = ALLOC( int, pCnf->nVars );
+    pVars = ABC_ALLOC( int, pCnf->nVars );
     for ( i = 0; i < pCnf->nVars; i++ )
         pVars[i] = -1;
     Saig_ManForEachLi( pCnf->pMan, pObj, i )
@@ -544,7 +544,7 @@ Vec_Int_t * Saig_AbsCollectRegisters( Cnf_Dat_t * pCnf, int nFrames, Vec_Int_t *
     Saig_ManForEachLo( pCnf->pMan, pObj, i )
         pVars[ pCnf->pVarNums[pObj->Id] ] = i;
     // mark used registers
-    pFlops = CALLOC( int, Aig_ManRegNum(pCnf->pMan) );
+    pFlops = ABC_CALLOC( int, Aig_ManRegNum(pCnf->pMan) );
     Vec_IntForEachEntry( vCore, iClause, i )
     {
         // skip auxiliary clauses
@@ -564,8 +564,8 @@ Vec_Int_t * Saig_AbsCollectRegisters( Cnf_Dat_t * pCnf, int nFrames, Vec_Int_t *
     for ( i = 0; i < Aig_ManRegNum(pCnf->pMan); i++ )
         if ( pFlops[i] )
             Vec_IntPush( vFlops, i );
-    free( pFlops );
-    free( pVars );
+    ABC_FREE( pFlops );
+    ABC_FREE( pVars );
     return vFlops;
 }
 
@@ -806,7 +806,7 @@ Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax,
         if ( fVerbose )
         {
             printf( "SAT solver: Vars = %7d. Clauses = %7d.  ", pSat->size, pSat->stats.clauses );
-            PRT( "Time", clock() - clk2 );
+            ABC_PRT( "Time", clock() - clk2 );
         }
         // compute UNSAT core
         vCore = Saig_AbsSolverUnsatCore( pSat, nConfMax, fVerbose );
@@ -831,7 +831,7 @@ Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax,
         if ( fVerbose )
         {
             printf( "The number of relevant registers is %d (out of %d).  ", Vec_IntSize(vFlops), Aig_ManRegNum(p) );
-            PRT( "Time", clock() - clk );
+            ABC_PRT( "Time", clock() - clk );
         }
     }
 /*
diff --git a/src/aig/saig/saigBmc.c b/src/aig/saig/saigBmc.c
index 7cccce96..d56d97a9 100644
--- a/src/aig/saig/saigBmc.c
+++ b/src/aig/saig/saigBmc.c
@@ -27,7 +27,7 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-#define AIG_VISITED       ((Aig_Obj_t *)(PORT_PTRUINT_T)1)
+#define AIG_VISITED       ((Aig_Obj_t *)(ABC_PTRUINT_T)1)
 
 typedef struct Saig_Bmc_t_ Saig_Bmc_t;
 struct Saig_Bmc_t_
@@ -88,7 +88,7 @@ Saig_Bmc_t * Saig_BmcManStart( Aig_Man_t * pAig, int nFramesMax, int nNodesMax,
     Aig_Obj_t * pObj;
     int i, Lit;
     assert( Aig_ManRegNum(pAig) > 0 );
-    p = (Saig_Bmc_t *)malloc( sizeof(Saig_Bmc_t) );
+    p = (Saig_Bmc_t *)ABC_ALLOC( char, sizeof(Saig_Bmc_t) );
     memset( p, 0, sizeof(Saig_Bmc_t) );
     // set parameters
     p->nFramesMax   = nFramesMax;
@@ -141,7 +141,7 @@ void Saig_BmcManStop( Saig_Bmc_t * p )
     sat_solver_delete( p->pSat );
     Vec_PtrFree( p->vTargets );
     Vec_PtrFree( p->vVisited );
-    free( p );
+    ABC_FREE( p );
 }
 
 /**Function*************************************************************
@@ -311,7 +311,7 @@ void Saig_BmcInterval( Saig_Bmc_t * p )
             // check if the node is gone
             Vec_PtrForEachEntry( p->vVisited, pObj, i )
             {
-                iFrame = (int)(PORT_PTRINT_T)Vec_PtrEntry( p->vVisited, 1+i++ );
+                iFrame = (int)(ABC_PTRINT_T)Vec_PtrEntry( p->vVisited, 1+i++ );
                 pRes = Saig_BmcObjFrame( p, pObj, iFrame );
                 if ( Aig_ObjIsNone( Aig_Regular(pRes) ) )
                     Saig_BmcObjSetFrame( p, pObj, iFrame, NULL );
@@ -524,7 +524,7 @@ int Saig_BmcSolveTargets( Saig_Bmc_t * p )
             return l_Undef;
         VarNum = Saig_BmcSatNum( p, Aig_Regular(pObj) );
         Lit = toLitCond( VarNum, Aig_IsComplement(pObj) );
-        RetValue = sat_solver_solve( p->pSat, &Lit, &Lit + 1, (sint64)p->nConfMaxOne, (sint64)0, (sint64)0, (sint64)0 );
+        RetValue = sat_solver_solve( p->pSat, &Lit, &Lit + 1, (ABC_INT64_T)p->nConfMaxOne, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
         if ( RetValue == l_False ) // unsat
             continue;
         if ( RetValue == l_Undef ) // undecided
@@ -614,7 +614,7 @@ void Saig_BmcPerform( Aig_Man_t * pAig, int nFramesMax, int nNodesMax, int nConf
         {
             printf( "%3d : F = %3d. O =%4d.  And = %7d. Var = %7d. Conf = %7d. ", 
                 Iter, p->iFrameLast, p->iOutputLast, Aig_ManNodeNum(p->pFrm), p->nSatVars, (int)p->pSat->stats.conflicts );   
-            PRT( "Time", clock() - clk2 );
+            ABC_PRT( "Time", clock() - clk2 );
         }
         if ( RetValue != l_False )
             break;
@@ -624,7 +624,7 @@ void Saig_BmcPerform( Aig_Man_t * pAig, int nFramesMax, int nNodesMax, int nConf
             p->iOutputFail, p->iFrameFail );
     else // if ( RetValue == l_False || RetValue == l_Undef )
         printf( "No output was asserted in %d frames.  ", p->iFramePrev-1 );
-    PRT( "Time", clock() - clk );
+    ABC_PRT( "Time", clock() - clk );
     if ( RetValue != l_True )
     {
         if ( p->iFrameLast >= p->nFramesMax )
diff --git a/src/aig/saig/saigBmc2.c b/src/aig/saig/saigBmc2.c
index 5776cd4a..8ba02528 100644
--- a/src/aig/saig/saigBmc2.c
+++ b/src/aig/saig/saigBmc2.c
@@ -199,7 +199,7 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim
         printf( "Time-frames (%d):  PI/PO = %d/%d.  Node = %6d. Lev = %5d.  ", 
             nFrames, Aig_ManPiNum(pFrames), Aig_ManPoNum(pFrames), 
             Aig_ManNodeNum(pFrames), Aig_ManLevelNum(pFrames) );
-        PRT( "Time", clock() - clk );
+        ABC_PRT( "Time", clock() - clk );
         fflush( stdout );
     }
     // rewrite the timeframes
@@ -213,7 +213,7 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim
         {
             printf( "Time-frames after rewriting:  Node = %6d. Lev = %5d.  ", 
                 Aig_ManNodeNum(pFrames), Aig_ManLevelNum(pFrames) );
-            PRT( "Time", clock() - clk );
+            ABC_PRT( "Time", clock() - clk );
             fflush( stdout );
         }
     }
@@ -230,7 +230,7 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim
     if ( fVerbose )
     {
         printf( "CNF: Variables = %6d. Clauses = %7d. Literals = %8d. ", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals );
-        PRT( "Time", clock() - clk );
+        ABC_PRT( "Time", clock() - clk );
         fflush( stdout );
     }
     status = sat_solver_simplify(pSat);
@@ -254,13 +254,13 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim
                     i % Saig_ManPoNum(pAig), i / Saig_ManPoNum(pAig) );
             }
             clk = clock();
-            status = sat_solver_solve( pSat, &Lit, &Lit + 1, (sint64)nConfLimit, (sint64)0, (sint64)0, (sint64)0 );
+            status = sat_solver_solve( pSat, &Lit, &Lit + 1, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
             if ( fVerbose && (i % Saig_ManPoNum(pAig) == Saig_ManPoNum(pAig) - 1) )
             {
                 printf( "Solved %2d outputs of frame %3d.  ", 
                     Saig_ManPoNum(pAig), i / Saig_ManPoNum(pAig) );
                 printf( "Conf =%8.0f. Imp =%11.0f. ", (double)pSat->stats.conflicts, (double)pSat->stats.propagations );
-                PRT( "T", clock() - clkPart );
+                ABC_PRT( "T", clock() - clkPart );
                 clkPart = clock();
                 fflush( stdout );
             }
@@ -284,7 +284,7 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim
                 int * pModel = Sat_SolverGetModel( pSat, vCiIds->pArray, vCiIds->nSize );
                 pModel[Aig_ManPiNum(pFrames)] = pObj->Id;
                 pAig->pSeqModel = Fra_SmlCopyCounterExample( pAig, pFrames, pModel );
-                free( pModel );
+                ABC_FREE( pModel );
                 Vec_IntFree( vCiIds );
 
 //                if ( piFrame )
diff --git a/src/aig/saig/saigHaig.c b/src/aig/saig/saigHaig.c
index 8a75ae1f..1c7aa025 100644
--- a/src/aig/saig/saigHaig.c
+++ b/src/aig/saig/saigHaig.c
@@ -273,7 +273,7 @@ clk = clock();
             return 0;
         }
     }
-PRT( "Preparation", clock() - clk );
+ABC_PRT( "Preparation", clock() - clk );
 
 
     // check in the second timeframe
@@ -291,7 +291,7 @@ clk = clock();
         Lits[0] = toLitCond( pCnf->pVarNums[pObj1->Id], 0 );
         Lits[1] = toLitCond( pCnf->pVarNums[pObj2->Id], 1 );
 
-        RetValue1 = sat_solver_solve( pSat, Lits, Lits + 2, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
+        RetValue1 = sat_solver_solve( pSat, Lits, Lits + 2, (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
         if ( RetValue1 == l_False )
         {
             Lits[0] = lit_neg( Lits[0] );
@@ -303,7 +303,7 @@ clk = clock();
         Lits[0]++;
         Lits[1]--;
 
-        RetValue2 = sat_solver_solve( pSat, Lits, Lits + 2, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
+        RetValue2 = sat_solver_solve( pSat, Lits, Lits + 2, (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
         if ( RetValue2 == l_False )
         {
             Lits[0] = lit_neg( Lits[0] );
@@ -323,7 +323,7 @@ clk = clock();
 //            break;
     }
     printf( "                                                          \r" );
-PRT( "Solving    ", clock() - clk );
+ABC_PRT( "Solving    ", clock() - clk );
 clkVerif = clock() - clk;
     if ( Counter )
         printf( "Verification failed for %d out of %d assertions.\n", Counter, pFrames->nAsserts/2 );
@@ -479,7 +479,7 @@ clk = clock();
             return 0;
         }
     }
-PRT( "Preparation", clock() - clk );
+ABC_PRT( "Preparation", clock() - clk );
 
 
     // check in the second timeframe
@@ -496,12 +496,12 @@ clk = clock();
             Lits[0] = toLitCond( pCnf->pVarNums[pObj1->Id]+Delta, 0 );
             Lits[1] = toLitCond( pCnf->pVarNums[pObj2->Id]+Delta, 0 );
 
-            RetValue1 = sat_solver_solve( pSat, Lits, Lits + 2, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
+            RetValue1 = sat_solver_solve( pSat, Lits, Lits + 2, (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
 
             Lits[0]++;
             Lits[1]++;
 
-            RetValue2 = sat_solver_solve( pSat, Lits, Lits + 2, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
+            RetValue2 = sat_solver_solve( pSat, Lits, Lits + 2, (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
 
             if ( RetValue1 != l_False || RetValue2 != l_False )
                 Counter++;
@@ -511,12 +511,12 @@ clk = clock();
             Lits[0] = toLitCond( pCnf->pVarNums[pObj1->Id]+Delta, 0 );
             Lits[1] = toLitCond( pCnf->pVarNums[pObj2->Id]+Delta, 1 );
 
-            RetValue1 = sat_solver_solve( pSat, Lits, Lits + 2, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
+            RetValue1 = sat_solver_solve( pSat, Lits, Lits + 2, (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
 
             Lits[0]++;
             Lits[1]--;
 
-            RetValue2 = sat_solver_solve( pSat, Lits, Lits + 2, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
+            RetValue2 = sat_solver_solve( pSat, Lits, Lits + 2, (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
 
             if ( RetValue1 != l_False || RetValue2 != l_False )
                 Counter++;
@@ -527,7 +527,7 @@ clk = clock();
 //        if ( i / 2 > 1000 )
 //            break;
     }
-PRT( "Solving    ", clock() - clk );
+ABC_PRT( "Solving    ", clock() - clk );
     if ( Counter )
         printf( "Verification failed for %d out of %d classes.\n", Counter, Vec_IntSize(pHaig->vEquPairs)/2 );
     else
@@ -634,7 +634,7 @@ clk = clock();
     // remove structural hashing table
     Aig_TableClear( pNew->pManHaig );
     pNew->pManHaig->vEquPairs = Vec_IntAlloc( 10000 );
-PRT( "HAIG setup time", clock() - clk );
+ABC_PRT( "HAIG setup time", clock() - clk );
 
 clk = clock();
     if ( fSeqHaig )
@@ -682,7 +682,7 @@ clk = clock();
             Aig_ManStop( pTemp );
         }
     } 
-PRT( "Synthesis time ", clock() - clk );
+ABC_PRT( "Synthesis time ", clock() - clk );
 clkSynth = clock() - clk;
 
     // use the haig for verification
diff --git a/src/aig/saig/saigInd.c b/src/aig/saig/saigInd.c
index 69c250f6..1c26e5df 100644
--- a/src/aig/saig/saigInd.c
+++ b/src/aig/saig/saigInd.c
@@ -121,13 +121,13 @@ int Saig_ManInduction( Aig_Man_t * p, int nFramesMax, int nConfMax, int fVerbose
         }
         // run the SAT solver
         nConfPrev = pSat->stats.conflicts;
-        status = sat_solver_solve( pSat, NULL, NULL, (sint64)nConfMax, 0, 0, 0 );
+        status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)nConfMax, 0, 0, 0 );
         if ( fVerbose )
         {
             printf( "%3d : PI = %5d. PO = %5d. AIG = %5d. Var = %6d. Conf = %6d. ",
                 f+1, Aig_ManPiNum(pAigPart), Aig_ManPoNum(pAigPart), Aig_ManNodeNum(pAigPart), 
                 nSatVarNum, pSat->stats.conflicts-nConfPrev );
-            PRT( "Time", clock() - clk );
+            ABC_PRT( "Time", clock() - clk );
         }
         if ( status == l_Undef )
             break;
diff --git a/src/aig/saig/saigIoa.c b/src/aig/saig/saigIoa.c
index 70870fe9..d049489e 100644
--- a/src/aig/saig/saigIoa.c
+++ b/src/aig/saig/saigIoa.c
@@ -348,7 +348,7 @@ Aig_Man_t * Saig_ManReadBlif( char * pFileName )
         {
             extern double pow( double x, double y );
             int Size = (int)pow(10.0, (double)(strlen(pToken) - 1));
-            pNum2Id = CALLOC( int, Size );
+            pNum2Id = ABC_CALLOC( int, Size );
         }
 
         // other tokens
@@ -383,7 +383,7 @@ Aig_Man_t * Saig_ManReadBlif( char * pFileName )
     // add non-node objects to the mapping
     Aig_ManForEachPi( p, pNode, i )
         pNum2Id[pNode->Id] = pNode->Id;
-//    FREE( pNum2Id );
+//    ABC_FREE( pNum2Id );
     p->pData = pNum2Id;
     // check the new manager
     Aig_ManSetRegNum( p, nRegs );
diff --git a/src/aig/saig/saigMiter.c b/src/aig/saig/saigMiter.c
index 6c4b3af0..174a3e97 100644
--- a/src/aig/saig/saigMiter.c
+++ b/src/aig/saig/saigMiter.c
@@ -526,13 +526,13 @@ int Saig_ManDemiterSimple( Aig_Man_t * p, Aig_Man_t ** ppAig0, Aig_Man_t ** ppAi
     if ( ppAig0 )
     {
         *ppAig0 = Aig_ManDupNodesHalf( p, vSet0, 0 );
-        FREE( (*ppAig0)->pName );
+        ABC_FREE( (*ppAig0)->pName );
         (*ppAig0)->pName = Aig_UtilStrsav( "part0" );
     }
     if ( ppAig1 )
     {
         *ppAig1 = Aig_ManDupNodesHalf( p, vSet1, 1 );
-        FREE( (*ppAig1)->pName );
+        ABC_FREE( (*ppAig1)->pName );
         (*ppAig1)->pName = Aig_UtilStrsav( "part1" );
     }
     Vec_PtrFree( vSet0 );
@@ -596,13 +596,13 @@ int Saig_ManDemiterSimpleDiff( Aig_Man_t * p, Aig_Man_t ** ppAig0, Aig_Man_t **
     if ( ppAig0 )
     {
         *ppAig0 = Aig_ManDupNodesAll( p, vSet0 );
-        FREE( (*ppAig0)->pName );
+        ABC_FREE( (*ppAig0)->pName );
         (*ppAig0)->pName = Aig_UtilStrsav( "part0" );
     }
     if ( ppAig1 )
     {
         *ppAig1 = Aig_ManDupNodesAll( p, vSet1 );
-        FREE( (*ppAig1)->pName );
+        ABC_FREE( (*ppAig1)->pName );
         (*ppAig1)->pName = Aig_UtilStrsav( "part1" );
     }
     Vec_PtrFree( vSet0 );
@@ -768,14 +768,14 @@ int Saig_ManDemiter( Aig_Man_t * p, Aig_Man_t ** ppAig0, Aig_Man_t ** ppAig1 )
     {
         assert( 0 );
         *ppAig0 = Aig_ManDupNodesHalf( p, vSet0, 0 ); // not ready
-        FREE( (*ppAig0)->pName );
+        ABC_FREE( (*ppAig0)->pName );
         (*ppAig0)->pName = Aig_UtilStrsav( "part0" );
     }
     if ( ppAig1 )
     {
         assert( 0 );
         *ppAig1 = Aig_ManDupNodesHalf( p, vSet1, 1 ); // not ready
-        FREE( (*ppAig1)->pName );
+        ABC_FREE( (*ppAig1)->pName );
         (*ppAig1)->pName = Aig_UtilStrsav( "part1" );
     }
     Vec_PtrFree( vSet0 );
@@ -891,12 +891,12 @@ int Ssw_SecSpecial( Aig_Man_t * pPart0, Aig_Man_t * pPart1, int nFrames, int fVe
     if ( RetValue == 1 )
     {
         printf( "Networks are equivalent.   " );
-PRT( "Time", clock() - clkTotal );
+ABC_PRT( "Time", clock() - clkTotal );
     }
     else if ( RetValue == 0 )
     {
         printf( "Networks are NOT EQUIVALENT.   " );
-PRT( "Time", clock() - clkTotal );
+ABC_PRT( "Time", clock() - clkTotal );
         if ( pMiterCec->pData == NULL )
             printf( "Counter-example is not available.\n" );
         else
@@ -919,7 +919,7 @@ PRT( "Time", clock() - clkTotal );
     else
     {
         printf( "Networks are UNDECIDED.   " );
-PRT( "Time", clock() - clkTotal );
+ABC_PRT( "Time", clock() - clkTotal );
     }
     fflush( stdout );
     Aig_ManStop( pMiterCec );
diff --git a/src/aig/saig/saigPhase.c b/src/aig/saig/saigPhase.c
index c6d84066..9b09598c 100644
--- a/src/aig/saig/saigPhase.c
+++ b/src/aig/saig/saigPhase.c
@@ -139,14 +139,14 @@ static inline void       Saig_TsiSetNext( unsigned * pState, int nWords, unsigne
 Saig_Tsim_t * Saig_TsiStart( Aig_Man_t * pAig )
 {
     Saig_Tsim_t * p;
-    p = (Saig_Tsim_t *)malloc( sizeof(Saig_Tsim_t) );
+    p = (Saig_Tsim_t *)ABC_ALLOC( char, sizeof(Saig_Tsim_t) );
     memset( p, 0, sizeof(Saig_Tsim_t) );
     p->pAig    = pAig;
     p->nWords  = Aig_BitWordNum( 2*Aig_ManRegNum(pAig) );
     p->vStates = Vec_PtrAlloc( 1000 );
     p->pMem    = Aig_MmFixedStart( sizeof(unsigned) * p->nWords + sizeof(unsigned *), 10000 );
     p->nBins   = Aig_PrimeCudd(TSIM_MAX_ROUNDS/2);
-    p->pBins   = ALLOC( unsigned *, p->nBins );
+    p->pBins   = ABC_ALLOC( unsigned *, p->nBins );
     memset( p->pBins, 0, sizeof(unsigned *) * p->nBins );
     return p;
 }
@@ -168,8 +168,8 @@ void Saig_TsiStop( Saig_Tsim_t * p )
         Vec_IntFree( p->vNonXRegs );
     Aig_MmFixedStop( p->pMem, 0 );
     Vec_PtrFree( p->vStates );
-    free( p->pBins );
-    free( p );
+    ABC_FREE( p->pBins );
+    ABC_FREE( p );
 }
 
 /**Function*************************************************************
@@ -696,7 +696,7 @@ Aig_Man_t * Saig_ManPerformAbstraction( Saig_Tsim_t * pTsi, int nFrames, int fVe
     assert( Vec_IntSize(pTsi->vNonXRegs) > 0 );
 
     // create mapping for the frames nodes
-    pObjMap = ALLOC( Aig_Obj_t *, nFrames * Aig_ManObjNumMax(pAig) );
+    pObjMap = ABC_ALLOC( Aig_Obj_t *, nFrames * Aig_ManObjNumMax(pAig) );
     memset( pObjMap, 0, sizeof(Aig_Obj_t *) * nFrames * Aig_ManObjNumMax(pAig) );
 
     // start the fraig package
@@ -762,7 +762,7 @@ Aig_Man_t * Saig_ManPerformAbstraction( Saig_Tsim_t * pTsi, int nFrames, int fVe
 //Aig_ManPrintStats( pFrames );
 //    Aig_ManPiCleanup( pFrames );
 //Aig_ManPrintStats( pFrames );
-    free( pObjMap );
+    ABC_FREE( pObjMap );
     return pFrames;
 }
 
diff --git a/src/aig/saig/saigRetFwd.c b/src/aig/saig/saigRetFwd.c
index b6321da6..8178d26e 100644
--- a/src/aig/saig/saigRetFwd.c
+++ b/src/aig/saig/saigRetFwd.c
@@ -51,7 +51,7 @@ Aig_Obj_t ** Aig_ManStaticFanoutStart( Aig_Man_t * p )
     int i, nFanouts, nFanoutsAlloc;
     // allocate fanouts
     nFanoutsAlloc = 2 * Aig_ManObjNumMax(p) - Aig_ManPiNum(p) - Aig_ManPoNum(p);
-    ppFanouts = ALLOC( Aig_Obj_t *, nFanoutsAlloc );
+    ppFanouts = ABC_ALLOC( Aig_Obj_t *, nFanoutsAlloc );
     // mark up storage
     nFanouts = 0;
     Aig_ManForEachObj( p, pObj, i )
@@ -122,7 +122,7 @@ void Saig_ManMarkAutonomous( Aig_Man_t * p )
     Aig_ManMarkAutonomous_rec( p, Aig_ManConst1(p) );
     Saig_ManForEachPi( p, pObj, i )
         Aig_ManMarkAutonomous_rec( p, pObj );
-    free( ppFanouts );
+    ABC_FREE( ppFanouts );
     // disconnect LIs/LOs and label unreachable registers
     Saig_ManForEachLiLo( p, pObjLi, pObjLo, i )
     {
@@ -220,7 +220,7 @@ Aig_Man_t * Saig_ManRetimeForward( Aig_Man_t * p, int nMaxIters, int fVerbose )
         {
             printf( "%2d : And = %6d. Reg = %5d. Unret = %5d. Move = %6d. ", 
                 i + 1, Aig_ManNodeNum(pTemp), Aig_ManRegNum(pTemp), nRegFixed, nRegMoves );
-            PRT( "Time", clock() - clk );
+            ABC_PRT( "Time", clock() - clk );
         }
         if ( pTemp != p )
             Aig_ManStop( pTemp );
@@ -229,7 +229,7 @@ Aig_Man_t * Saig_ManRetimeForward( Aig_Man_t * p, int nMaxIters, int fVerbose )
     pNew = Aig_ManReduceLaches( pNew, fVerbose );
     if ( fVerbose )
     {
-        PRT( "Register sharing time", clock() - clk );
+        ABC_PRT( "Register sharing time", clock() - clk );
     }
     return pNew;
 }
diff --git a/src/aig/saig/saigRetMin.c b/src/aig/saig/saigRetMin.c
index 1820ae9a..b9204f44 100644
--- a/src/aig/saig/saigRetMin.c
+++ b/src/aig/saig/saigRetMin.c
@@ -61,7 +61,7 @@ Vec_Int_t * Saig_ManRetimeInitState( Aig_Man_t * p )
         Cnf_DataFree( pCnf );
         return NULL;
     }
-    RetValue = sat_solver_solve( pSat, NULL, NULL, (sint64)nConfLimit, (sint64)0, (sint64)0, (sint64)0 );
+    RetValue = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
     assert( RetValue != l_Undef );
     // create counter-example
     if ( RetValue == l_True )
@@ -119,7 +119,7 @@ int Saig_ManRetimeUnsatCore( Aig_Man_t * p, int fVerbose )
     }
     sat_solver_store_mark_roots( pSat ); 
     // solve the problem
-    RetValue = sat_solver_solve( pSat, NULL, NULL, (sint64)nConfLimit, (sint64)0, (sint64)0, (sint64)0 );
+    RetValue = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
     assert( RetValue != l_Undef );
     assert( RetValue == l_False );
     pSatCnf = sat_solver_store_release( pSat ); 
@@ -132,7 +132,7 @@ int Saig_ManRetimeUnsatCore( Aig_Man_t * p, int fVerbose )
     // derive the set of variables on which the core depends
     // collect the variable numbers
     nVars = 0;
-    pVars = ALLOC( int, pCnf->nVars );
+    pVars = ABC_ALLOC( int, pCnf->nVars );
     memset( pVars, 0, sizeof(int) * pCnf->nVars );
     Vec_IntForEachEntry( vCore, iClause, i )
     {
@@ -170,7 +170,7 @@ int Saig_ManRetimeUnsatCore( Aig_Man_t * p, int fVerbose )
         }
     if ( fVerbose )
         printf( "UNSAT core: %d clauses, %d variables, %d POs.  ", Vec_IntSize(vCore), nVars, nPos );
-    free( pVars );
+    ABC_FREE( pVars );
     Vec_IntFree( vCore );
     Cnf_DataFree( pCnf );
     return iBadPo;
diff --git a/src/aig/saig/saigSimExt.c b/src/aig/saig/saigSimExt.c
index 49c85ff4..ead0ece5 100644
--- a/src/aig/saig/saigSimExt.c
+++ b/src/aig/saig/saigSimExt.c
@@ -309,7 +309,7 @@ clk = clock();
     if ( fVerbose )
     {
         printf( "Total new PIs = %3d. Non-removable PIs = %3d.  ", Saig_ManPiNum(p)-iFirstPi, Vec_IntSize(vRes) );
-PRT( "Time", clock() - clk );
+ABC_PRT( "Time", clock() - clk );
     }
     Vec_PtrFree( vSimInfo );
     Aig_ManFanoutStop( p );
diff --git a/src/aig/saig/saigSimFast.c b/src/aig/saig/saigSimFast.c
index 09bb6a06..05f77f8a 100644
--- a/src/aig/saig/saigSimFast.c
+++ b/src/aig/saig/saigSimFast.c
@@ -108,7 +108,7 @@ Faig_Man_t * Faig_ManAlloc( Aig_Man_t * pAig )
     int nWords;
 //    assert( Faig_ManIsCorrect(pAig) );
     nWords = 2 * Aig_ManNodeNum(pAig) + Aig_ManPoNum(pAig);
-    p = (Faig_Man_t *)ALLOC( char, sizeof(Faig_Man_t) + sizeof(int) * nWords );
+    p = (Faig_Man_t *)ABC_ALLOC( char, sizeof(Faig_Man_t) + sizeof(int) * nWords );
 //printf( "Allocating %7.2f Mb.\n", 1.0 * (sizeof(Faig_Man_t) + sizeof(int) * nWords)/(1<<20) );
     memset( p, 0, sizeof(Faig_Man_t) );
     p->nPis   = Aig_ManPiNum(pAig) - Aig_ManRegNum(pAig);
@@ -247,8 +247,8 @@ static inline unsigned Faig_SimulateTransferShift( unsigned uOld, unsigned uNew
 ***********************************************************************/
 int * Faig_ManSimulateFrames( Faig_Man_t * p, int nFrames, int nPref, int fTrans )
 {
-    int * pNumOnes = CALLOC( unsigned, p->nObjs );
-    unsigned * pSimInfo = ALLOC( unsigned, p->nObjs );
+    int * pNumOnes = ABC_CALLOC( unsigned, p->nObjs );
+    unsigned * pSimInfo = ABC_ALLOC( unsigned, p->nObjs );
     int f, i;
 //printf( "Allocating %7.2f Mb.\n", 1.0 * 4 * p->nObjs/(1<<20) );
 //printf( "Allocating %7.2f Mb.\n", 1.0 * 4 * p->nObjs/(1<<20) );
@@ -287,7 +287,7 @@ int * Faig_ManSimulateFrames( Faig_Man_t * p, int nFrames, int nPref, int fTrans
                 pNumOnes[i] += Aig_WordCountOnes( pSimInfo[i] );
         }
     }
-    free( pSimInfo );
+    ABC_FREE( pSimInfo );
     return pNumOnes;
 }
 
@@ -336,7 +336,7 @@ float Faig_ManComputeProbOne( int nOnes, int nSimWords )
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Int_t * Faig_ManComputeSwitchProbs( Aig_Man_t * p, int nFrames, int nPref, int fProbOne )
+Vec_Int_t * Faig_ManComputeSwitchProbs4( Aig_Man_t * p, int nFrames, int nPref, int fProbOne )
 {
     extern char * Abc_FrameReadFlag( char * pFlag ); 
     int fTrans = 1;
@@ -351,7 +351,7 @@ Vec_Int_t * Faig_ManComputeSwitchProbs( Aig_Man_t * p, int nFrames, int nPref, i
     pSwitching = (float *)vSwitching->pArray;
 clk = clock();
     pAig = Faig_ManCreate( p );
-//PRT( "\nCreation  ", clock() - clk );
+//ABC_PRT( "\nCreation  ", clock() - clk );
     Aig_ManRandom( 1 );
     // get the number of  frames to simulate
     // if the parameter "seqsimframes" is defined, use it
@@ -368,7 +368,7 @@ clk = clock();
 //printf( "Simulating %d frames.\n", nFramesReal );
 clk = clock();
     pProbs = Faig_ManSimulateFrames( pAig, nFramesReal, nPref, fTrans );
-//PRT( "Simulation", clock() - clk );
+//ABC_PRT( "Simulation", clock() - clk );
 clk = clock();
     if ( fTrans )
     {
@@ -412,10 +412,10 @@ clk = clock();
             pSwitching[pObj->Id] = Faig_ManComputeSwitching( pProbs[Counter++], nFramesReal - nPref );
         assert( Counter == pAig->nObjs );
     }
-    free( pProbs );
-    free( pAig );
-//PRT( "Switch    ", clock() - clk );
-//PRT( "TOTAL     ", clock() - clkTotal );
+    ABC_FREE( pProbs );
+    ABC_FREE( pAig );
+//ABC_PRT( "Switch    ", clock() - clk );
+//ABC_PRT( "TOTAL     ", clock() - clkTotal );
     return vSwitching;
 }
 
@@ -430,9 +430,10 @@ clk = clock();
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Int_t * Saig_ManComputeSwitchProbs( Aig_Man_t * p, int nFrames, int nPref, int fProbOne )
+Vec_Int_t * Saig_ManComputeSwitchProb3s( Aig_Man_t * p, int nFrames, int nPref, int fProbOne )
 {
-    return Faig_ManComputeSwitchProbs( p, nFrames, nPref, fProbOne );
+//    return Faig_ManComputeSwitchProbs( p, nFrames, nPref, fProbOne );
+    return NULL;
 }
 
 
diff --git a/src/aig/saig/saigSimMv.c b/src/aig/saig/saigSimMv.c
index 0e250a74..9bc6416b 100644
--- a/src/aig/saig/saigSimMv.c
+++ b/src/aig/saig/saigSimMv.c
@@ -129,7 +129,7 @@ Saig_MvObj_t * Saig_ManCreateReducedAig( Aig_Man_t * p, Vec_Ptr_t ** pvFlops )
     Aig_Obj_t * pObj;
     int i;
     *pvFlops = Vec_PtrAlloc( Aig_ManRegNum(p) );
-    pAig = CALLOC( Saig_MvObj_t, Aig_ManObjNumMax(p)+1 );
+    pAig = ABC_CALLOC( Saig_MvObj_t, Aig_ManObjNumMax(p)+1 );
     Aig_ManForEachObj( p, pObj, i )
     {
         pEntry = pAig + i;
@@ -171,8 +171,8 @@ static inline int Saig_MvCreateObj( Saig_MvMan_t * p, int iFan0, int iFan1 )
     Saig_MvAnd_t * pNode;
     if ( p->nObjs == p->nObjsAlloc )
     {
-        p->pAigNew = REALLOC( Saig_MvAnd_t, p->pAigNew, 2*p->nObjsAlloc );
-        p->pLevels = REALLOC( unsigned char, p->pLevels, 2*p->nObjsAlloc );
+        p->pAigNew = ABC_REALLOC( Saig_MvAnd_t, p->pAigNew, 2*p->nObjsAlloc );
+        p->pLevels = ABC_REALLOC( unsigned char, p->pLevels, 2*p->nObjsAlloc );
         p->nObjsAlloc *= 2;
     }
     pNode = p->pAigNew + p->nObjs;
@@ -202,7 +202,7 @@ Saig_MvMan_t * Saig_MvManStart( Aig_Man_t * pAig )
     Saig_MvMan_t * p;
     int i;
     assert( Aig_ManRegNum(pAig) > 0 );
-    p = (Saig_MvMan_t *)ALLOC( Saig_MvMan_t, 1 );
+    p = (Saig_MvMan_t *)ABC_ALLOC( Saig_MvMan_t, 1 );
     memset( p, 0, sizeof(Saig_MvMan_t) );
     // set parameters
     p->pAig         = pAig;
@@ -213,23 +213,23 @@ Saig_MvMan_t * Saig_MvManStart( Aig_Man_t * pAig )
     // compacted AIG
     p->pAigOld      = Saig_ManCreateReducedAig( pAig, &p->vFlops );
     p->nTStatesSize = Aig_PrimeCudd( p->nStatesMax );
-    p->pTStates     = CALLOC( int, p->nTStatesSize );
+    p->pTStates     = ABC_CALLOC( int, p->nTStatesSize );
     p->pMemStates   = Aig_MmFixedStart( sizeof(int) * (p->nFlops+1), p->nStatesMax );
     p->vStates      = Vec_PtrAlloc( p->nStatesMax );
     Vec_PtrPush( p->vStates, NULL );
-    p->pRegsUndef   = CALLOC( int, p->nFlops );
-    p->pRegsValues  = ALLOC( int *, p->nFlops );
-    p->pRegsValues[0] = ALLOC( int, p->nValuesMax * p->nFlops );
+    p->pRegsUndef   = ABC_CALLOC( int, p->nFlops );
+    p->pRegsValues  = ABC_ALLOC( int *, p->nFlops );
+    p->pRegsValues[0] = ABC_ALLOC( int, p->nValuesMax * p->nFlops );
     for ( i = 1; i < p->nFlops; i++ )
         p->pRegsValues[i] = p->pRegsValues[i-1] + p->nValuesMax;
-    p->nRegsValues  = CALLOC( int, p->nFlops );
+    p->nRegsValues  = ABC_CALLOC( int, p->nFlops );
     p->vTired       = Vec_PtrAlloc( 100 );
     // internal AIG
     p->nObjsAlloc   = 1000000;
-    p->pAigNew      = ALLOC( Saig_MvAnd_t, p->nObjsAlloc );
+    p->pAigNew      = ABC_ALLOC( Saig_MvAnd_t, p->nObjsAlloc );
     p->nTNodesSize  = Aig_PrimeCudd( p->nObjsAlloc / 3 );
-    p->pTNodes      = CALLOC( int, p->nTNodesSize );
-    p->pLevels      = ALLOC( unsigned char, p->nObjsAlloc );
+    p->pTNodes      = ABC_CALLOC( int, p->nTNodesSize );
+    p->pLevels      = ABC_ALLOC( unsigned char, p->nObjsAlloc );
     Saig_MvCreateObj( p, 0, 0 );
     return p;
 }
@@ -251,16 +251,16 @@ void Saig_MvManStop( Saig_MvMan_t * p )
     Vec_PtrFree( p->vStates );
     Vec_PtrFree( p->vFlops );
     Vec_PtrFree( p->vTired );
-    free( p->pRegsValues[0] );
-    free( p->pRegsValues );
-    free( p->nRegsValues );
-    free( p->pRegsUndef );
-    free( p->pAigOld );
-    free( p->pTStates );
-    free( p->pAigNew );
-    free( p->pTNodes );
-    free( p->pLevels );
-    free( p );
+    ABC_FREE( p->pRegsValues[0] );
+    ABC_FREE( p->pRegsValues );
+    ABC_FREE( p->nRegsValues );
+    ABC_FREE( p->pRegsUndef );
+    ABC_FREE( p->pAigOld );
+    ABC_FREE( p->pTStates );
+    ABC_FREE( p->pAigNew );
+    ABC_FREE( p->pTNodes );
+    ABC_FREE( p->pLevels );
+    ABC_FREE( p );
 }
 
 /**Function*************************************************************
@@ -661,7 +661,7 @@ int Saig_MvManSimulate( Aig_Man_t * pAig, int fVerbose )
     int f, i, k, iRegMax, iState, clk = clock();
     // start the manager
     p = Saig_MvManStart( pAig );
-PRT( "Constructing the problem", clock() - clk );
+ABC_PRT( "Constructing the problem", clock() - clk );
     clk = clock();
     // initiliaze registers
     Vec_PtrForEachEntry( p->vFlops, pEntry, i )
@@ -710,7 +710,7 @@ PRT( "Constructing the problem", clock() - clk );
                 pEntry->Value = Saig_MvUndef();
         }
     }
-PRT( "Multi-value simulation", clock() - clk );
+ABC_PRT( "Multi-value simulation", clock() - clk );
     // implement equivalences
     Saig_MvManPostProcess( p, iState-1 );
     Saig_MvManStop( p );
diff --git a/src/aig/saig/saigSimSeq.c b/src/aig/saig/saigSimSeq.c
index 26783346..c527b152 100644
--- a/src/aig/saig/saigSimSeq.c
+++ b/src/aig/saig/saigSimSeq.c
@@ -52,7 +52,7 @@ struct Raig_Man_t_
     int             nWordsAlloc;  // the number of allocated entries
     int             nMems;        // the number of used entries  
     int             nMemsMax;     // the max number of used entries 
-    int             MemFree;      // next free entry
+    int             MemFree;      // next ABC_FREE entry
 };
 
 static inline int  Raig_Var2Lit( int Var, int fCompl )  { return Var + Var + fCompl; }
@@ -146,7 +146,7 @@ Raig_Man_t * Raig_ManCreate( Aig_Man_t * pAig )
     Aig_Obj_t * pObj;
     int i, nObjs;
     Aig_ManCleanData( pAig );
-    p = (Raig_Man_t *)ALLOC( Raig_Man_t, 1 );
+    p = (Raig_Man_t *)ABC_ALLOC( Raig_Man_t, 1 );
     memset( p, 0, sizeof(Raig_Man_t) );
     p->pAig = pAig;
     p->nPis = Saig_ManPiNum(pAig);
@@ -155,10 +155,10 @@ Raig_Man_t * Raig_ManCreate( Aig_Man_t * pAig )
     p->nCos = Aig_ManPoNum(pAig);
     p->nNodes = Aig_ManNodeNum(pAig);
     nObjs = p->nCis + p->nCos + p->nNodes + 2;
-    p->pFans0 = ALLOC( int, nObjs );
-    p->pFans1 = ALLOC( int, nObjs );
-    p->pRefs = ALLOC( int, nObjs );
-    p->pSims = CALLOC( unsigned, nObjs );
+    p->pFans0 = ABC_ALLOC( int, nObjs );
+    p->pFans1 = ABC_ALLOC( int, nObjs );
+    p->pRefs = ABC_ALLOC( int, nObjs );
+    p->pSims = ABC_CALLOC( unsigned, nObjs );
     p->vCis2Ids = Vec_IntAlloc( Aig_ManPiNum(pAig) );
     // add objects (0=unused; 1=const1)
     p->nObjs = 2;
@@ -202,12 +202,12 @@ void Raig_ManDelete( Raig_Man_t * p )
     Vec_IntFree( p->vCis2Ids );
     Vec_IntFree( p->vLos );
     Vec_IntFree( p->vLis );
-    FREE( p->pFans0 );
-    FREE( p->pFans1 );
-    FREE( p->pRefs );
-    FREE( p->pSims );
-    FREE( p->pMems );
-    FREE( p );
+    ABC_FREE( p->pFans0 );
+    ABC_FREE( p->pFans1 );
+    ABC_FREE( p->pRefs );
+    ABC_FREE( p->pSims );
+    ABC_FREE( p->pMems );
+    ABC_FREE( p );
 }
 
 /**Function*************************************************************
@@ -236,7 +236,7 @@ unsigned * Raig_ManSimRef( Raig_Man_t * p, int i )
             p->nMems = 1;
         }
         p->nWordsAlloc *= 2;
-        p->pMems = REALLOC( unsigned, p->pMems, p->nWordsAlloc );
+        p->pMems = ABC_REALLOC( unsigned, p->pMems, p->nWordsAlloc );
         memset( p->pMems, 0xff, sizeof(unsigned) * (p->nWords + 1) );
         pPlace = &p->MemFree;
         for ( Ent = p->nMems * (p->nWords + 1); 
@@ -421,7 +421,7 @@ Ssw_Cex_t * Raig_ManGenerateCounter( Aig_Man_t * pAig, int iFrame, int iOut, int
     // fill in the binary data
     Aig_ManRandom( 1 );
     Counter = p->nRegs;
-    pData = ALLOC( unsigned, nWords );
+    pData = ABC_ALLOC( unsigned, nWords );
     for ( f = 0; f <= iFrame; f++, Counter += p->nPis )
     for ( i = 0; i < Aig_ManPiNum(pAig); i++ )
     {
@@ -433,7 +433,7 @@ Ssw_Cex_t * Raig_ManGenerateCounter( Aig_Man_t * pAig, int iFrame, int iOut, int
         if ( Aig_InfoHasBit( pData, iPat ) )
             Aig_InfoSetBit( p->pData, Counter + iPioId );
     }
-    free( pData );
+    ABC_FREE( pData );
     return p;
 }
 
@@ -500,7 +500,7 @@ int Raig_ManSimulate( Aig_Man_t * pAig, int nWords, int nIters, int TimeLimit, i
             p->nMemsMax, 
             1.0*(p->nObjs * 16)/(1<<20), 
             1.0*(p->nMemsMax * 4 * (nWords+1))/(1<<20) );
-        PRT( "Total time", clock() - clkTotal );
+        ABC_PRT( "Total time", clock() - clkTotal );
     }
     Raig_ManDelete( p );
     return RetValue > 0;
diff --git a/src/aig/saig/saigStrSim.c b/src/aig/saig/saigStrSim.c
index ce4b8e05..9e50c9b6 100644
--- a/src/aig/saig/saigStrSim.c
+++ b/src/aig/saig/saigStrSim.c
@@ -396,9 +396,9 @@ int Saig_StrSimDetectUnique( Aig_Man_t * p0, Aig_Man_t * p1 )
 
     // allocate the hash table hashing simulation info into nodes
     nTableSize = Aig_PrimeCudd( Aig_ManObjNum(p0)/2 );
-    ppTable = CALLOC( Aig_Obj_t *, nTableSize ); 
-    ppNexts = CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p0) ); 
-    ppCands = CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p0) ); 
+    ppTable = ABC_CALLOC( Aig_Obj_t *, nTableSize ); 
+    ppNexts = ABC_CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p0) ); 
+    ppCands = ABC_CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p0) ); 
 
     // hash nodes of the first AIG 
     Aig_ManForEachObj( p0, pObj, i )
@@ -453,9 +453,9 @@ int Saig_StrSimDetectUnique( Aig_Man_t * p0, Aig_Man_t * p1 )
 
     // cleanup
     Aig_ManCleanMarkA( p0 );
-    free( ppTable );
-    free( ppNexts );
-    free( ppCands );
+    ABC_FREE( ppTable );
+    ABC_FREE( ppNexts );
+    ABC_FREE( ppCands );
     return Counter;
 }
 
@@ -926,7 +926,7 @@ Vec_Int_t * Saig_StrSimPerformMatching( Aig_Man_t * p0, Aig_Man_t * p1, int nDis
                 i, nMatches,
                 nFlops, 100.0*nFlops/Aig_ManRegNum(pPart0),
                 nNodes, 100.0*nNodes/Aig_ManNodeNum(pPart0) );
-            PRT( "Time", clock() - clk );
+            ABC_PRT( "Time", clock() - clk );
         }
         if ( i == 20 )
             break;
@@ -959,7 +959,7 @@ Vec_Int_t * Saig_StrSimPerformMatching( Aig_Man_t * p0, Aig_Man_t * p1, int nDis
     Aig_ManFanoutStop( pPart1 );
     Aig_ManStop( pPart0 );
     Aig_ManStop( pPart1 );
-    PRT( "Total runtime", clock() - clkTotal );
+    ABC_PRT( "Total runtime", clock() - clkTotal );
     return vPairs;
 }
 
diff --git a/src/aig/saig/saigSwitch.c b/src/aig/saig/saigSwitch.c
index 684551be..122483d2 100644
--- a/src/aig/saig/saigSwitch.c
+++ b/src/aig/saig/saigSwitch.c
@@ -63,7 +63,7 @@ Saig_SimObj_t * Saig_ManCreateMan( Aig_Man_t * p )
     Saig_SimObj_t * pAig, * pEntry;
     Aig_Obj_t * pObj;
     int i;
-    pAig = CALLOC( Saig_SimObj_t, Aig_ManObjNumMax(p)+1 );
+    pAig = ABC_CALLOC( Saig_SimObj_t, Aig_ManObjNumMax(p)+1 );
 //    printf( "Allocating %7.2f Mb.\n", 1.0 * sizeof(Saig_SimObj_t) * (Aig_ManObjNumMax(p)+1)/(1<<20) );
     Aig_ManForEachObj( p, pObj, i )
     {
@@ -258,7 +258,7 @@ float Saig_ManComputeProbOnePlus( int nOnes, int nSimWords, int fCompl )
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Int_t * Saig_ManComputeSwitchProbs_old( Aig_Man_t * p, int nFrames, int nPref, int fProbOne )
+Vec_Int_t * Saig_ManComputeSwitchProb4s( Aig_Man_t * p, int nFrames, int nPref, int fProbOne )
 {
     extern char * Abc_FrameReadFlag( char * pFlag ); 
     Saig_SimObj_t * pAig, * pEntry;
@@ -269,7 +269,7 @@ Vec_Int_t * Saig_ManComputeSwitchProbs_old( Aig_Man_t * p, int nFrames, int nPre
     pSwitching = (float *)vSwitching->pArray;
 clk = clock();
     pAig = Saig_ManCreateMan( p );
-//PRT( "\nCreation  ", clock() - clk );
+//ABC_PRT( "\nCreation  ", clock() - clk );
 
     Aig_ManRandom( 1 );
     // get the number of  frames to simulate
@@ -287,7 +287,7 @@ clk = clock();
 //printf( "Simulating %d frames.\n", nFramesReal );
 clk = clock();
     Saig_ManSimulateFrames( pAig, nFramesReal, nPref );
-//PRT( "Simulation", clock() - clk );
+//ABC_PRT( "Simulation", clock() - clk );
 clk = clock();
     for ( pEntry = pAig; pEntry->Type != AIG_OBJ_VOID; pEntry++ )
     {
@@ -312,9 +312,9 @@ clk = clock();
             pSwitching[pEntry-pAig] = Saig_ManComputeSwitching( pEntry->Number, nFramesReal - nPref );
 //printf( "%3d : %7.2f\n", pEntry-pAig, pSwitching[pEntry-pAig] );
     }
-    free( pAig );
-//PRT( "Switch    ", clock() - clk );
-//PRT( "TOTAL     ", clock() - clkTotal );
+    ABC_FREE( pAig );
+//ABC_PRT( "Switch    ", clock() - clk );
+//ABC_PRT( "TOTAL     ", clock() - clkTotal );
 
 //    Aig_CManCreate( p );
     return vSwitching;
@@ -356,7 +356,7 @@ struct Aig_CMan_t_
 Aig_CMan_t * Aig_CManStart( int nIns, int nNodes, int nOuts )
 {
     Aig_CMan_t * p;
-    p = (Aig_CMan_t *)ALLOC( char, sizeof(Aig_CMan_t) + 2*(2*nNodes + nOuts) );
+    p = (Aig_CMan_t *)ABC_ALLOC( char, sizeof(Aig_CMan_t) + 2*(2*nNodes + nOuts) );
     memset( p, 0, sizeof(Aig_CMan_t) );
     // set parameters
     p->nIns = nIns;
@@ -383,7 +383,7 @@ Aig_CMan_t * Aig_CManStart( int nIns, int nNodes, int nOuts )
 ***********************************************************************/
 void Aig_CManStop( Aig_CMan_t * p )
 {
-    free( p );
+    ABC_FREE( p );
 }
 
 /**Function*************************************************************
@@ -559,22 +559,6 @@ Aig_CMan_t * Aig_CManCreate( Aig_Man_t * p )
     return pCMan;
 }
 
-/**Function*************************************************************
-
-  Synopsis    [Compute switching probabilities of all nodes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Int_t * Saig_ManComputeSwitchProbs2( Aig_Man_t * p, int nFrames, int nPref, int fProbOne )
-{
-    return NULL;
-}
-
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/saig/saigSynch.c b/src/aig/saig/saigSynch.c
index c52f2f48..ff46634e 100644
--- a/src/aig/saig/saigSynch.c
+++ b/src/aig/saig/saigSynch.c
@@ -280,7 +280,7 @@ int Saig_SynchCountX( Aig_Man_t * pAig, Vec_Ptr_t * vSimInfo, int nWords, int *
     int * pCounters, i, w, b;
     int iPatBest, iTernMin;
     // count the number of ternary values in each pattern
-    pCounters = CALLOC( int, nWords * 16 );
+    pCounters = ABC_CALLOC( int, nWords * 16 );
     Saig_ManForEachLi( pAig, pObj, i )
     {
         pSim = Vec_PtrEntry( vSimInfo, pObj->Id );
@@ -300,7 +300,7 @@ int Saig_SynchCountX( Aig_Man_t * pAig, Vec_Ptr_t * vSimInfo, int nWords, int *
             if ( iTernMin == 0 )
                 break;
         }
-    free( pCounters );
+    ABC_FREE( pCounters );
     *piPat = iPatBest;
     return iTernMin;
 }
@@ -512,7 +512,7 @@ clk = clock();
         printf( "Design 1: Synchronizing sequence of length %4d is found. ", Vec_StrSize(vSequence) / Saig_ManPiNum(pAig) );
     if ( fVerbose )
     {
-        PRT( "Time", clock() - clk );
+        ABC_PRT( "Time", clock() - clk );
     }
     else
         printf( "\n" );
@@ -588,7 +588,7 @@ Aig_Man_t * Saig_Synchronize( Aig_Man_t * pAig1, Aig_Man_t * pAig2, int nWords,
         printf( "Design 1: Synchronizing sequence of length %4d is found. ", Vec_StrSize(vSeq1) / Saig_ManPiNum(pAig1) );
     if ( fVerbose )
     {
-        PRT( "Time", clock() - clk );
+        ABC_PRT( "Time", clock() - clk );
     }
     else
         printf( "\n" );
@@ -602,7 +602,7 @@ Aig_Man_t * Saig_Synchronize( Aig_Man_t * pAig1, Aig_Man_t * pAig2, int nWords,
         printf( "Design 2: Synchronizing sequence of length %4d is found. ", Vec_StrSize(vSeq2) / Saig_ManPiNum(pAig2) );
     if ( fVerbose )
     {
-        PRT( "Time", clock() - clk );
+        ABC_PRT( "Time", clock() - clk );
     }
     else
         printf( "\n" );
@@ -646,7 +646,7 @@ Aig_Man_t * Saig_Synchronize( Aig_Man_t * pAig1, Aig_Man_t * pAig2, int nWords,
     if ( fVerbose )
     {
         printf( "Miter of the synchronized designs is constructed.         " );
-        PRT( "Time", clock() - clk );
+        ABC_PRT( "Time", clock() - clk );
     }
     return pMiter;
 }
diff --git a/src/aig/saig/saigTrans.c b/src/aig/saig/saigTrans.c
index c1c2d8e9..f50af285 100644
--- a/src/aig/saig/saigTrans.c
+++ b/src/aig/saig/saigTrans.c
@@ -386,7 +386,7 @@ clk = clock();
     {
         Aig_ManPrintStats( pFrames );
         Aig_ManPrintStats( pFraig );
-PRT( "Fraiging", clock() - clk );
+ABC_PRT( "Fraiging", clock() - clk );
     }
     Aig_ManStop( pFraig );
     assert( pFrames->pReprs != NULL );
@@ -397,12 +397,12 @@ PRT( "Fraiging", clock() - clk );
     // create reduced initialized timeframes
 clk = clock();
     pRes2 = Saig_ManFramesInitialMapped( pAig, nFrames, nFramesMax, fInit );
-PRT( "Mapped", clock() - clk );
-    // free mapping
+ABC_PRT( "Mapped", clock() - clk );
+    // ABC_FREE mapping
     Saig_ManStopMap2( pAig );
 clk = clock();
     pRes1 = Saig_ManFramesInitialMapped( pAig, nFrames, nFramesMax, fInit );
-PRT( "Normal", clock() - clk );
+ABC_PRT( "Normal", clock() - clk );
     // report the results
     if ( fVerbose )
     {
diff --git a/src/aig/saig/saigWnd.c b/src/aig/saig/saigWnd.c
index 5524e19f..10202f1b 100644
--- a/src/aig/saig/saigWnd.c
+++ b/src/aig/saig/saigWnd.c
@@ -99,7 +99,7 @@ Vec_Ptr_t * Saig_ManWindowOutline( Aig_Man_t * p, Aig_Obj_t * pObj, int nDist )
     Vec_Ptr_t * vNodes;
     Aig_Obj_t * pObjLi, * pObjLo;
     int * pDists, i;
-    pDists = CALLOC( int, Aig_ManObjNumMax(p) );
+    pDists = ABC_CALLOC( int, Aig_ManObjNumMax(p) );
     vNodes = Vec_PtrAlloc( 1000 );
     Aig_ManIncrementTravId( p );
     Saig_ManWindowOutline_rec( p, pObj, nDist, vNodes, pDists );
@@ -108,7 +108,7 @@ Vec_Ptr_t * Saig_ManWindowOutline( Aig_Man_t * p, Aig_Obj_t * pObj, int nDist )
     Saig_ManForEachLiLo( p, pObjLi, pObjLo, i )
         assert( Aig_ObjIsTravIdCurrent(p, pObjLi) == 
                 Aig_ObjIsTravIdCurrent(p, pObjLo) );
-    free( pDists );
+    ABC_FREE( pDists );
     return vNodes;
 }