Version abc90215

17 files changed, 234 insertions, 230 deletions

diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h
index e7cd0550..a2c10367 100644
--- a/src/aig/fra/fra.h
+++ b/src/aig/fra/fra.h
@@ -21,10 +21,6 @@
 #ifndef __FRA_H__
 #define __FRA_H__
 
-#ifdef __cplusplus
-extern "C" {
-#endif 
-
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -45,6 +41,10 @@ extern "C" {
 ///                         PARAMETERS                               ///
 ////////////////////////////////////////////////////////////////////////
 
+#ifdef __cplusplus
+extern "C" {
+#endif 
+
 ////////////////////////////////////////////////////////////////////////
 ///                         BASIC TYPES                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -215,8 +215,8 @@ struct Fra_Man_t_
     sat_solver *     pSat;              // SAT solver
     int              nSatVars;          // the number of variables currently used
     Vec_Ptr_t *      vPiVars;           // the PIs of the cone used 
-    sint64           nBTLimitGlobal;    // resource limit
-    sint64           nInsLimitGlobal;   // resource limit
+    ABC_INT64_T           nBTLimitGlobal;    // resource limit
+    ABC_INT64_T           nInsLimitGlobal;   // resource limit
     Vec_Ptr_t **     pMemFanins;        // the arrays of fanins for some FRAIG nodes
     int *            pMemSatNums;       // the array of SAT numbers for some FRAIG nodes
     int              nMemAlloc;         // allocated size of the arrays for FRAIG varnums and fanins
@@ -290,7 +290,7 @@ static inline int          Fra_ImpCreate( int Left, int Right )
 ////////////////////////////////////////////////////////////////////////
 
 /*=== fraCec.c ========================================================*/
-extern int                 Fra_FraigSat( Aig_Man_t * pMan, sint64 nConfLimit, sint64 nInsLimit, int fFlipBits, int fAndOuts, int fVerbose );
+extern int                 Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fFlipBits, int fAndOuts, int fVerbose );
 extern int                 Fra_FraigCec( Aig_Man_t ** ppAig, int nConfLimit, int fVerbose );
 extern int                 Fra_FraigCecPartitioned( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nConfLimit, int nPartSize, int fSmart, int fVerbose );
 /*=== fraClass.c ========================================================*/
@@ -376,7 +376,7 @@ extern void                Fra_SmlSimulate( Fra_Man_t * p, int fInit );
 extern void                Fra_SmlResimulate( Fra_Man_t * p );
 extern Fra_Sml_t *         Fra_SmlStart( Aig_Man_t * pAig, int nPref, int nFrames, int nWordsFrame );
 extern void                Fra_SmlStop( Fra_Sml_t * p );
-extern Fra_Sml_t *         Fra_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int nFrames, int nWords );
+extern Fra_Sml_t *         Fra_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int nFrames, int nWords, int fCheckMiter );
 extern Fra_Sml_t *         Fra_SmlSimulateComb( Aig_Man_t * pAig, int nWords );
 extern Fra_Cex_t *         Fra_SmlGetCounterExample( Fra_Sml_t * p );
 extern Fra_Cex_t *         Fra_SmlCopyCounterExample( Aig_Man_t * pAig, Aig_Man_t * pFrames, int * pModel );
diff --git a/src/aig/fra/fraBmc.c b/src/aig/fra/fraBmc.c
index 411ca2c1..689d7d67 100644
--- a/src/aig/fra/fraBmc.c
+++ b/src/aig/fra/fraBmc.c
@@ -188,13 +188,13 @@ void Fra_BmcFilterImplications( Fra_Man_t * p, Fra_Bmc_t * pBmc )
 Fra_Bmc_t * Fra_BmcStart( Aig_Man_t * pAig, int nPref, int nDepth )
 {
     Fra_Bmc_t * p;
-    p = ALLOC( Fra_Bmc_t, 1 );
+    p = ABC_ALLOC( Fra_Bmc_t, 1 );
     memset( p, 0, sizeof(Fra_Bmc_t) );
     p->pAig = pAig;
     p->nPref = nPref;
     p->nDepth = nDepth;
     p->nFramesAll = nPref + nDepth;
-    p->pObjToFrames  = ALLOC( Aig_Obj_t *, p->nFramesAll * Aig_ManObjNumMax(pAig) );
+    p->pObjToFrames  = ABC_ALLOC( Aig_Obj_t *, p->nFramesAll * Aig_ManObjNumMax(pAig) );
     memset( p->pObjToFrames, 0, sizeof(Aig_Obj_t *) * p->nFramesAll * Aig_ManObjNumMax(pAig) );
     return p;
 }
@@ -215,9 +215,9 @@ void Fra_BmcStop( Fra_Bmc_t * p )
     Aig_ManStop( p->pAigFrames );
     if ( p->pAigFraig )
         Aig_ManStop( p->pAigFraig );
-    free( p->pObjToFrames );
-    free( p->pObjToFraig );
-    free( p );
+    ABC_FREE( p->pObjToFrames );
+    ABC_FREE( p->pObjToFraig );
+    ABC_FREE( p );
 }
 
 /**Function*************************************************************
@@ -253,7 +253,7 @@ Aig_Man_t * Fra_BmcFrames( Fra_Bmc_t * p, int fKeepPos )
         Bmc_ObjSetFrames( pObj, 0, Aig_ManConst0(pAigFrames) );
 
     // add timeframes
-    pLatches = ALLOC( Aig_Obj_t *, Aig_ManRegNum(p->pAig) );
+    pLatches = ABC_ALLOC( Aig_Obj_t *, Aig_ManRegNum(p->pAig) );
     for ( f = 0; f < p->nFramesAll; f++ )
     {
         // add internal nodes of this frame
@@ -275,7 +275,7 @@ Aig_Man_t * Fra_BmcFrames( Fra_Bmc_t * p, int fKeepPos )
             Bmc_ObjSetFrames( pObj, f+1, pLatches[k++] );
         assert( k == Aig_ManRegNum(p->pAig) );
     }
-    free( pLatches );
+    ABC_FREE( pLatches );
     if ( fKeepPos )
     {
         for ( f = 0; f < p->nFramesAll; f++ )
@@ -333,7 +333,7 @@ void Fra_BmcPerform( Fra_Man_t * p, int nPref, int nDepth )
         printf( "Original AIG = %d. Init %d frames = %d. Fraig = %d.  ", 
             Aig_ManNodeNum(p->pBmc->pAig), p->pBmc->nFramesAll, 
             Aig_ManNodeNum(p->pBmc->pAigFrames), Aig_ManNodeNum(p->pBmc->pAigFraig) );
-        PRT( "Time", clock() - clk );
+        ABC_PRT( "Time", clock() - clk );
         printf( "Before BMC: " );  
 //        Fra_ClassesPrint( p->pCla, 0 );
         printf( "Const = %5d. Class = %5d. Lit = %5d. ", 
@@ -360,7 +360,7 @@ void Fra_BmcPerform( Fra_Man_t * p, int nPref, int nDepth )
             printf( "Imp = %5d. ", Vec_IntSize(p->pCla->vImps) );
         printf( "\n" );
     }
-    // free the BMC manager
+    // ABC_FREE the BMC manager
     Fra_BmcStop( p->pBmc );  
     p->pBmc = NULL;
 }
@@ -397,7 +397,7 @@ void Fra_BmcPerformSimple( Aig_Man_t * pAig, int nFrames, int nBTLimit, int fRew
         printf( "Time-frames (%d):  PI/PO = %d/%d.  Node = %6d. Lev = %5d.  ", 
             nFrames, Aig_ManPiNum(pBmc->pAigFrames), Aig_ManPoNum(pBmc->pAigFrames), 
             Aig_ManNodeNum(pBmc->pAigFrames), Aig_ManLevelNum(pBmc->pAigFrames) );
-        PRT( "Time", clock() - clk );
+        ABC_PRT( "Time", clock() - clk );
     }
     if ( fRewrite )
     {
@@ -408,7 +408,7 @@ void Fra_BmcPerformSimple( Aig_Man_t * pAig, int nFrames, int nBTLimit, int fRew
         {
             printf( "Time-frames after rewriting:  Node = %6d. Lev = %5d.  ", 
                 Aig_ManNodeNum(pBmc->pAigFrames), Aig_ManLevelNum(pBmc->pAigFrames) );
-            PRT( "Time", clock() - clk );
+            ABC_PRT( "Time", clock() - clk );
         }
     }
     clk = clock();
@@ -422,7 +422,7 @@ void Fra_BmcPerformSimple( Aig_Man_t * pAig, int nFrames, int nBTLimit, int fRew
         if ( pBmc->pAigFraig->pData )
         {
             pAig->pSeqModel = Fra_SmlCopyCounterExample( pAig, pBmc->pAigFrames, pBmc->pAigFraig->pData );
-            FREE( pBmc->pAigFraig->pData );
+            ABC_FREE( pBmc->pAigFraig->pData );
         }
         else if ( iOutput >= 0 )
             pAig->pSeqModel = Fra_SmlTrivCounterExample( pAig, iOutput );
@@ -432,10 +432,10 @@ void Fra_BmcPerformSimple( Aig_Man_t * pAig, int nFrames, int nBTLimit, int fRew
         printf( "Fraiged init frames: Node = %6d. Lev = %5d.  ", 
             pBmc->pAigFraig? Aig_ManNodeNum(pBmc->pAigFraig) : -1,
             pBmc->pAigFraig? Aig_ManLevelNum(pBmc->pAigFraig) : -1 );
-        PRT( "Time", clock() - clk );
+        ABC_PRT( "Time", clock() - clk );
     }
     Fra_BmcStop( pBmc );  
-    free( pTemp );
+    ABC_FREE( pTemp );
 }
 
 
diff --git a/src/aig/fra/fraCec.c b/src/aig/fra/fraCec.c
index 2cdf203d..0cc6748c 100644
--- a/src/aig/fra/fraCec.c
+++ b/src/aig/fra/fraCec.c
@@ -40,7 +40,7 @@
   SeeAlso     []
 
 ***********************************************************************/
-int Fra_FraigSat( Aig_Man_t * pMan, sint64 nConfLimit, sint64 nInsLimit, int fFlipBits, int fAndOuts, int fVerbose )
+int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fFlipBits, int fAndOuts, int fVerbose )
 {
     sat_solver * pSat;
     Cnf_Dat_t * pCnf;
@@ -91,13 +91,13 @@ int Fra_FraigSat( Aig_Man_t * pMan, sint64 nConfLimit, sint64 nInsLimit, int fFl
 
 
 //    printf( "Created SAT problem with %d variable and %d clauses. ", sat_solver_nvars(pSat), sat_solver_nclauses(pSat) );
-//    PRT( "Time", clock() - clk );
+//    ABC_PRT( "Time", clock() - clk );
 
     // simplify the problem
     clk = clock();
     status = sat_solver_simplify(pSat);
 //    printf( "Simplified the problem to %d variables and %d clauses. ", sat_solver_nvars(pSat), sat_solver_nclauses(pSat) );
-//    PRT( "Time", clock() - clk );
+//    ABC_PRT( "Time", clock() - clk );
     if ( status == 0 )
     {
         Vec_IntFree( vCiIds );
@@ -110,7 +110,7 @@ int Fra_FraigSat( Aig_Man_t * pMan, sint64 nConfLimit, sint64 nInsLimit, int fFl
     clk = clock();
     if ( fVerbose )
         pSat->verbosity = 1;
-    status = sat_solver_solve( pSat, NULL, NULL, (sint64)nConfLimit, (sint64)nInsLimit, (sint64)0, (sint64)0 );
+    status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)nInsLimit, (ABC_INT64_T)0, (ABC_INT64_T)0 );
     if ( status == l_Undef )
     {
 //        printf( "The problem timed out.\n" );
@@ -128,7 +128,7 @@ int Fra_FraigSat( Aig_Man_t * pMan, sint64 nConfLimit, sint64 nInsLimit, int fFl
     }
     else
         assert( 0 );
-//    PRT( "SAT sat_solver time", clock() - clk );
+//    ABC_PRT( "SAT sat_solver time", clock() - clk );
 //    printf( "The number of conflicts = %d.\n", (int)pSat->sat_solver_stats.conflicts );
  
     // if the problem is SAT, get the counterexample
@@ -136,7 +136,7 @@ int Fra_FraigSat( Aig_Man_t * pMan, sint64 nConfLimit, sint64 nInsLimit, int fFl
     {
         pMan->pData = Sat_SolverGetModel( pSat, vCiIds->pArray, vCiIds->nSize );
     }
-    // free the sat_solver
+    // ABC_FREE the sat_solver
     if ( fVerbose )
         Sat_SolverPrintStats( stdout, pSat );
 //sat_solver_store_write( pSat, "trace.cnf" );
@@ -176,18 +176,18 @@ int Fra_FraigCec( Aig_Man_t ** ppAig, int nConfLimit, int fVerbose )
 //    assert( RetValue == -1 );
     if ( RetValue == 0 )
     {
-        pAig->pData = ALLOC( int, Aig_ManPiNum(pAig) );
+        pAig->pData = ABC_ALLOC( int, Aig_ManPiNum(pAig) );
         memset( pAig->pData, 0, sizeof(int) * Aig_ManPiNum(pAig) );
         return RetValue;
     }
 
     // if SAT only, solve without iteration
 clk = clock();
-    RetValue = Fra_FraigSat( pAig, (sint64)2*nBTLimitStart, (sint64)0, 1, 0, 0 );
+    RetValue = Fra_FraigSat( pAig, (ABC_INT64_T)2*nBTLimitStart, (ABC_INT64_T)0, 1, 0, 0 );
     if ( fVerbose )
     {
         printf( "Initial SAT:      Nodes = %6d.  ", Aig_ManNodeNum(pAig) );
-PRT( "Time", clock() - clk );
+ABC_PRT( "Time", clock() - clk );
     }
     if ( RetValue >= 0 )
         return RetValue;
@@ -199,7 +199,7 @@ clk = clock();
     if ( fVerbose )
     {
         printf( "Rewriting:        Nodes = %6d.  ", Aig_ManNodeNum(pAig) );
-PRT( "Time", clock() - clk );
+ABC_PRT( "Time", clock() - clk );
     }
 
     // perform the loop
@@ -218,7 +218,7 @@ clk = clock();
         if ( fVerbose )
         {
             printf( "Fraiging (i=%d):   Nodes = %6d.  ", i+1, Aig_ManNodeNum(pAig) );
-PRT( "Time", clock() - clk );
+ABC_PRT( "Time", clock() - clk );
         }
 
         // check the miter status
@@ -233,7 +233,7 @@ clk = clock();
         if ( fVerbose )
         {
             printf( "Rewriting:        Nodes = %6d.  ", Aig_ManNodeNum(pAig) );
-PRT( "Time", clock() - clk );
+ABC_PRT( "Time", clock() - clk );
         } 
 
         // check the miter status
@@ -251,11 +251,11 @@ PRT( "Time", clock() - clk );
     if ( RetValue == -1 )
     {
 clk = clock();
-        RetValue = Fra_FraigSat( pAig, (sint64)nBTLimitLast, (sint64)0, 1, 0, 0 );
+        RetValue = Fra_FraigSat( pAig, (ABC_INT64_T)nBTLimitLast, (ABC_INT64_T)0, 1, 0, 0 );
         if ( fVerbose )
         {
             printf( "Final SAT:            Nodes = %6d.  ", Aig_ManNodeNum(pAig) );
-PRT( "Time", clock() - clk );
+ABC_PRT( "Time", clock() - clk );
         }
     }
 
@@ -318,7 +318,7 @@ int Fra_FraigCecPartitioned( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nConfLimi
         printf( "Timed out after verifying %d partitions (out of %d).\n", nOutputs, Vec_PtrSize(vParts) );
         fflush( stdout );
     }
-    // free intermediate results
+    // ABC_FREE intermediate results
     Vec_PtrForEachEntry( vParts, pAig, i )
         Aig_ManStop( pAig );
     Vec_PtrFree( vParts );
@@ -373,17 +373,17 @@ int Fra_FraigCecTop( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nConfLimit, int n
     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 );
     }
     else
     {
         printf( "Networks are UNDECIDED.   " );
-PRT( "Time", clock() - clkTotal );
+ABC_PRT( "Time", clock() - clkTotal );
     }
     fflush( stdout );
     return RetValue;
diff --git a/src/aig/fra/fraClass.c b/src/aig/fra/fraClass.c
index 064d2b9c..8554b312 100644
--- a/src/aig/fra/fraClass.c
+++ b/src/aig/fra/fraClass.c
@@ -57,10 +57,10 @@ static inline void         Fra_ObjSetNext( Aig_Obj_t ** ppNexts, Aig_Obj_t * pOb
 Fra_Cla_t * Fra_ClassesStart( Aig_Man_t * pAig )
 {
     Fra_Cla_t * p;
-    p = ALLOC( Fra_Cla_t, 1 );
+    p = ABC_ALLOC( Fra_Cla_t, 1 );
     memset( p, 0, sizeof(Fra_Cla_t) );
     p->pAig = pAig;
-    p->pMemRepr  = ALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pAig) );
+    p->pMemRepr  = ABC_ALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pAig) );
     memset( p->pMemRepr, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(pAig) );
     p->vClasses     = Vec_PtrAlloc( 100 );
     p->vClasses1    = Vec_PtrAlloc( 100 );
@@ -86,15 +86,15 @@ Fra_Cla_t * Fra_ClassesStart( Aig_Man_t * pAig )
 ***********************************************************************/
 void Fra_ClassesStop( Fra_Cla_t * p )
 {
-    FREE( p->pMemClasses );
-    FREE( p->pMemRepr );
+    ABC_FREE( p->pMemClasses );
+    ABC_FREE( p->pMemRepr );
     if ( p->vClassesTemp ) Vec_PtrFree( p->vClassesTemp );
     if ( p->vClassNew )    Vec_PtrFree( p->vClassNew );
     if ( p->vClassOld )    Vec_PtrFree( p->vClassOld );
     if ( p->vClasses1 )    Vec_PtrFree( p->vClasses1 );
     if ( p->vClasses )     Vec_PtrFree( p->vClasses );
     if ( p->vImps )        Vec_IntFree( p->vImps );
-    free( p );
+    ABC_FREE( p );
 }
 
 /**Function*************************************************************
@@ -278,8 +278,8 @@ void Fra_ClassesPrepare( Fra_Cla_t * p, int fLatchCorr, int nMaxLevs )
 
     // allocate the hash table hashing simulation info into nodes
     nTableSize = Aig_PrimeCudd( Aig_ManObjNumMax(p->pAig) );
-    ppTable = ALLOC( Aig_Obj_t *, nTableSize ); 
-    ppNexts = ALLOC( Aig_Obj_t *, nTableSize ); 
+    ppTable = ABC_ALLOC( Aig_Obj_t *, nTableSize ); 
+    ppNexts = ABC_ALLOC( Aig_Obj_t *, nTableSize ); 
     memset( ppTable, 0, sizeof(Aig_Obj_t *) * nTableSize );
 
     // add all the nodes to the hash table
@@ -338,7 +338,7 @@ void Fra_ClassesPrepare( Fra_Cla_t * p, int fLatchCorr, int nMaxLevs )
         }
 
     // allocate room for classes
-    p->pMemClasses = ALLOC( Aig_Obj_t *, 2*(nEntries + Vec_PtrSize(p->vClasses1)) );
+    p->pMemClasses = ABC_ALLOC( Aig_Obj_t *, 2*(nEntries + Vec_PtrSize(p->vClasses1)) );
     p->pMemClassesFree = p->pMemClasses + 2*nEntries;
  
     // copy the entries into storage in the topological order
@@ -374,8 +374,8 @@ void Fra_ClassesPrepare( Fra_Cla_t * p, int fLatchCorr, int nMaxLevs )
         // increment the number of entries
         nEntries += k;
     }
-    free( ppTable );
-    free( ppNexts );
+    ABC_FREE( ppTable );
+    ABC_FREE( ppNexts );
     // now it is time to refine the classes
     Fra_ClassesRefine( p );
 //    Fra_ClassesPrint( p, 0 );
@@ -587,7 +587,7 @@ int Fra_ClassesRefine1( Fra_Cla_t * p, int fRefineNewClass, int * pSkipped )
 void Fra_ClassesTest( Fra_Cla_t * p, int Id1, int Id2 )
 {
     Aig_Obj_t ** pClass;
-    p->pMemClasses = ALLOC( Aig_Obj_t *, 4 );
+    p->pMemClasses = ABC_ALLOC( Aig_Obj_t *, 4 );
     pClass = p->pMemClasses;
     assert( Id1 < Id2 );
     pClass[0] = Aig_ManObj( p->pAig, Id1 );
@@ -620,7 +620,7 @@ void Fra_ClassesLatchCorr( Fra_Man_t * p )
         Fra_ClassObjSetRepr( pObj, Aig_ManConst1(p->pManAig) );
     }
     // allocate room for classes
-    p->pCla->pMemClasses = ALLOC( Aig_Obj_t *, 2*(nEntries + Vec_PtrSize(p->pCla->vClasses1)) );
+    p->pCla->pMemClasses = ABC_ALLOC( Aig_Obj_t *, 2*(nEntries + Vec_PtrSize(p->pCla->vClasses1)) );
     p->pCla->pMemClassesFree = p->pCla->pMemClasses + 2*nEntries;
 }
 
@@ -644,7 +644,7 @@ void Fra_ClassesPostprocess( Fra_Cla_t * p )
     // perform combinational simulation
     pComb = Fra_SmlSimulateComb( p->pAig, 32 );
     // compute the weight of each node in the classes
-    pWeights = ALLOC( int, Aig_ManObjNumMax(p->pAig) );
+    pWeights = ABC_ALLOC( int, Aig_ManObjNumMax(p->pAig) );
     memset( pWeights, 0, sizeof(int) * Aig_ManObjNumMax(p->pAig) );
     Aig_ManForEachObj( p->pAig, pObj, i )
     { 
@@ -686,7 +686,7 @@ void Fra_ClassesPostprocess( Fra_Cla_t * p )
             Vec_PtrWriteEntry( p->vClasses, k++, ppClass );
     Vec_PtrShrink( p->vClasses, k );
     printf( "After: Const = %6d. Class = %6d. \n", Vec_PtrSize(p->vClasses1), Vec_PtrSize(p->vClasses) );
-    free( pWeights );
+    ABC_FREE( pWeights );
 }
 
 /**Function*************************************************************
@@ -804,13 +804,13 @@ Aig_Man_t * Fra_ClassesDeriveAig( Fra_Cla_t * p, int nFramesK )
     pManFraig->pName = Aig_UtilStrsav( p->pAig->pName );
     pManFraig->pSpec = Aig_UtilStrsav( p->pAig->pSpec );
     // allocate place for the node mapping
-    ppEquivs = ALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) );
+    ppEquivs = ABC_ALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) );
     Fra_ObjSetEqu( ppEquivs, Aig_ManConst1(p->pAig), Aig_ManConst1(pManFraig) );
     // create latches for the first frame
     Aig_ManForEachLoSeq( p->pAig, pObj, i )
         Fra_ObjSetEqu( ppEquivs, pObj, Aig_ObjCreatePi(pManFraig) );
     // add timeframes
-    pLatches = ALLOC( Aig_Obj_t *, Aig_ManRegNum(p->pAig) );
+    pLatches = ABC_ALLOC( Aig_Obj_t *, Aig_ManRegNum(p->pAig) );
     for ( f = 0; f < nFramesAll; f++ )
     {
         // create PIs for this frame
@@ -839,8 +839,8 @@ Aig_Man_t * Fra_ClassesDeriveAig( Fra_Cla_t * p, int nFramesK )
         Aig_ManForEachLoSeq( p->pAig, pObj, i )
             Fra_ObjSetEqu( ppEquivs, pObj, pLatches[k++] );
     }
-    free( pLatches );
-    free( ppEquivs );
+    ABC_FREE( pLatches );
+    ABC_FREE( ppEquivs );
     // mark the asserts
     assert( Aig_ManPoNum(pManFraig) % nFramesAll == 0 );
 printf( "Assert miters = %6d. Output miters = %6d.\n", 
diff --git a/src/aig/fra/fraClau.c b/src/aig/fra/fraClau.c
index 919d0000..96d06380 100644
--- a/src/aig/fra/fraClau.c
+++ b/src/aig/fra/fraClau.c
@@ -152,7 +152,7 @@ int * Fra_ClauCreateMapping( Vec_Int_t * vSatVarsFrom, Vec_Int_t * vSatVarsTo, i
 {
     int * pMapping, Var, i;
     assert( Vec_IntSize(vSatVarsFrom) == Vec_IntSize(vSatVarsTo) );
-    pMapping = ALLOC( int, nVarsMax );
+    pMapping = ABC_ALLOC( int, nVarsMax );
     for ( i = 0; i < nVarsMax; i++ )
         pMapping[i] = -1;
     Vec_IntForEachEntry( vSatVarsFrom, Var, i )
@@ -174,10 +174,10 @@ int * Fra_ClauCreateMapping( Vec_Int_t * vSatVarsFrom, Vec_Int_t * vSatVarsTo, i
 ***********************************************************************/
 void Fra_ClauStop( Cla_Man_t * p )
 {
-    free( p->pMapCsMainToCsTest );
-    free( p->pMapCsTestToCsMain );
-    free( p->pMapCsTestToNsTest );
-    free( p->pMapCsTestToNsBmc  );
+    ABC_FREE( p->pMapCsMainToCsTest );
+    ABC_FREE( p->pMapCsTestToCsMain );
+    ABC_FREE( p->pMapCsTestToNsTest );
+    ABC_FREE( p->pMapCsTestToNsBmc  );
     Vec_IntFree( p->vSatVarsMainCs );
     Vec_IntFree( p->vSatVarsTestCs );
     Vec_IntFree( p->vSatVarsTestNs );
@@ -191,7 +191,7 @@ void Fra_ClauStop( Cla_Man_t * p )
     if ( p->pSatMain ) sat_solver_delete( p->pSatMain );
     if ( p->pSatTest ) sat_solver_delete( p->pSatTest );
     if ( p->pSatBmc )  sat_solver_delete( p->pSatBmc );
-    free( p );
+    ABC_FREE( p );
 }
 
 /**Function*************************************************************
@@ -217,7 +217,7 @@ Cla_Man_t * Fra_ClauStart( Aig_Man_t * pMan )
     assert( Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan) == 1 );
 
     // start the manager
-    p = ALLOC( Cla_Man_t, 1 );
+    p = ABC_ALLOC( Cla_Man_t, 1 );
     memset( p, 0, sizeof(Cla_Man_t) );
     p->vCexMain0 = Vec_IntAlloc( Aig_ManRegNum(pMan) );
     p->vCexMain  = Vec_IntAlloc( Aig_ManRegNum(pMan) );
@@ -362,7 +362,7 @@ int Fra_ClauCheckProperty( Cla_Man_t * p, Vec_Int_t * vCex )
     int nBTLimit = 0;
     int RetValue, iVar, i;
     sat_solver_act_var_clear( p->pSatMain );
-    RetValue = sat_solver_solve( p->pSatMain, NULL, NULL, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
+    RetValue = sat_solver_solve( p->pSatMain, NULL, NULL, (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
     Vec_IntClear( vCex );
     if ( RetValue == l_False )
         return 1;
@@ -396,7 +396,7 @@ int Fra_ClauCheckBmc( Cla_Man_t * p, Vec_Int_t * vClause )
     int nBTLimit = 0;
     int RetValue;
     RetValue = sat_solver_solve( p->pSatBmc, Vec_IntArray(vClause), Vec_IntArray(vClause) + Vec_IntSize(vClause), 
-        (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
+        (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
     if ( RetValue == l_False )
         return 1;
     assert( RetValue == l_True );
@@ -458,7 +458,7 @@ int Fra_ClauCheckClause( Cla_Man_t * p, Vec_Int_t * vClause, Vec_Int_t * vCex )
     Vec_IntPush( p->vCexAssm, toLitCond(i,0) ); // positive helper
     // try to solve
     RetValue = sat_solver_solve( p->pSatTest, Vec_IntArray(p->vCexAssm), Vec_IntArray(p->vCexAssm) + Vec_IntSize(p->vCexAssm), 
-        (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
+        (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
     if ( vCex )
         Vec_IntClear( vCex );
     if ( RetValue == l_False )
diff --git a/src/aig/fra/fraClaus.c b/src/aig/fra/fraClaus.c
index 91b70702..e5fe3f40 100644
--- a/src/aig/fra/fraClaus.c
+++ b/src/aig/fra/fraClaus.c
@@ -98,7 +98,7 @@ int Fra_ClausRunBmc( Clu_Man_t * p )
     for ( i = 0; i < p->nPref + p->nFrames; i++ )
     {
         Lits[0] = i * nLitsTot + toLitCond( p->pCnf->pVarNums[pObj->Id], 0 ); 
-        RetValue = sat_solver_solve( p->pSatBmc, Lits, Lits + 1, (sint64)p->nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
+        RetValue = sat_solver_solve( p->pSatBmc, Lits, Lits + 1, (ABC_INT64_T)p->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
         if ( RetValue != l_False )
             return 0;
     }
@@ -121,14 +121,14 @@ int Fra_ClausRunSat( Clu_Man_t * p )
     Aig_Obj_t * pObj;
     int * pLits;
     int i, RetValue;
-    pLits = ALLOC( int, p->nFrames + 1 );
+    pLits = ABC_ALLOC( int, p->nFrames + 1 );
     // set the output literals
     pObj = Aig_ManPo(p->pAig, 0);
     for ( i = 0; i <= p->nFrames; i++ )
         pLits[i] = i * 2 * p->pCnf->nVars + toLitCond( p->pCnf->pVarNums[pObj->Id], i != p->nFrames ); 
     // try to solve the problem
-    RetValue = sat_solver_solve( p->pSatMain, pLits, pLits + p->nFrames + 1, (sint64)p->nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
-    free( pLits );
+    RetValue = sat_solver_solve( p->pSatMain, pLits, pLits + p->nFrames + 1, (ABC_INT64_T)p->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
+    ABC_FREE( pLits );
     if ( RetValue == l_False )
         return 1;
     // get the counter-example
@@ -153,7 +153,7 @@ int Fra_ClausRunSat0( Clu_Man_t * p )
     int Lits[2], RetValue;
     pObj = Aig_ManPo(p->pAig, 0);
     Lits[0] = toLitCond( p->pCnf->pVarNums[pObj->Id], 0 ); 
-    RetValue = sat_solver_solve( p->pSatMain, Lits, Lits + 1, (sint64)p->nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
+    RetValue = sat_solver_solve( p->pSatMain, Lits, Lits + 1, (ABC_INT64_T)p->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
     if ( RetValue == l_False )
         return 1;
     return 0;
@@ -350,7 +350,7 @@ int Fra_ClausSelectClauses( Clu_Man_t * p )
     assert( Vec_IntSize(p->vClauses) > p->nClausesMax );   
     // count how many implications have each cost
     CostMax = p->nSimWords * 32 + 1;
-    pCostCount = ALLOC( int, CostMax );
+    pCostCount = ABC_ALLOC( int, CostMax );
     memset( pCostCount, 0, sizeof(int) * CostMax );
     Vec_IntForEachEntry( p->vCosts, Cost, i )
     {
@@ -380,7 +380,7 @@ int Fra_ClausSelectClauses( Clu_Man_t * p )
         }
         Vec_IntWriteEntry( p->vCosts, i, -1 );
     }
-    free( pCostCount );
+    ABC_FREE( pCostCount );
     p->nClauses = nClauCount;
 if ( p->fVerbose )
 printf( "Selected %d clauses. Cost range: [%d < %d < %d]\n", nClauCount, 1, c, CostMax );
@@ -608,7 +608,7 @@ int Fra_ClausProcessClauses( Clu_Man_t * p, int fRefs )
 clk = clock();
 //    srand( 0xAABBAABB );
     Aig_ManRandom(1);
-    pSeq = Fra_SmlSimulateSeq( p->pAig, 0, p->nPref + p->nSimFrames, p->nSimWords/p->nSimFrames );
+    pSeq = Fra_SmlSimulateSeq( p->pAig, 0, p->nPref + p->nSimFrames, p->nSimWords/p->nSimFrames, 1 );
     if ( p->fTarget && pSeq->fNonConstOut )
     {
         printf( "Property failed after sequential simulation!\n" );
@@ -617,7 +617,7 @@ clk = clock();
     }
 if ( p->fVerbose )
 {
-PRT( "Sim-seq", clock() - clk );
+ABC_PRT( "Sim-seq", clock() - clk );
 }
 
 
@@ -627,7 +627,7 @@ clk = clock();
     Fra_ClausCollectLatchClauses( p, pSeq );
 if ( p->fVerbose )
 {
-PRT( "Lat-cla", clock() - clk );
+ABC_PRT( "Lat-cla", clock() - clk );
 }
     }
 
@@ -638,7 +638,7 @@ clk = clock();
 //    pManCut = Aig_ComputeCuts( p->pAig, 10, 4, 0, 1 );
 if ( p->fVerbose )
 {
-PRT( "Cuts   ", clock() - clk );
+ABC_PRT( "Cuts   ", clock() - clk );
 }
 
     // collect sequential info for each cut
@@ -656,7 +656,7 @@ clk = clock();
             }
 if ( p->fVerbose )
 {
-PRT( "Infoseq", clock() - clk );
+ABC_PRT( "Infoseq", clock() - clk );
 }
     Fra_SmlStop( pSeq );
 
@@ -667,7 +667,7 @@ clk = clock();
     pComb = Fra_SmlSimulateComb( p->pAig, p->nSimWords + p->nSimWordsPref  );
 if ( p->fVerbose )
 {
-PRT( "Sim-cmb", clock() - clk );
+ABC_PRT( "Sim-cmb", clock() - clk );
 }
 
     // collect combinational info for each cut
@@ -692,7 +692,7 @@ clk = clock();
 //    Aig_ManCutStop( pManCut );
 if ( p->fVerbose )
 {
-PRT( "Infocmb", clock() - clk );
+ABC_PRT( "Infocmb", clock() - clk );
 }
 
     if ( p->fVerbose )
@@ -732,7 +732,7 @@ int Fra_ClausProcessClauses2( Clu_Man_t * p, int fRefs )
 clk = clock();
 //    srand( 0xAABBAABB );
     Aig_ManRandom(1);
-    pSeq = Fra_SmlSimulateSeq( p->pAig, 0, p->nPref + p->nSimFrames, p->nSimWords/p->nSimFrames );
+    pSeq = Fra_SmlSimulateSeq( p->pAig, 0, p->nPref + p->nSimFrames, p->nSimWords/p->nSimFrames, 1  );
     if ( p->fTarget && pSeq->fNonConstOut )
     {
         printf( "Property failed after sequential simulation!\n" );
@@ -741,7 +741,7 @@ clk = clock();
     }
 if ( p->fVerbose )
 {
-//PRT( "Sim-seq", clock() - clk );
+//ABC_PRT( "Sim-seq", clock() - clk );
 }
 
     // perform combinational simulation
@@ -751,7 +751,7 @@ clk = clock();
     pComb = Fra_SmlSimulateComb( p->pAig, p->nSimWords + p->nSimWordsPref  );
 if ( p->fVerbose )
 {
-//PRT( "Sim-cmb", clock() - clk );
+//ABC_PRT( "Sim-cmb", clock() - clk );
 }
 
 
@@ -761,7 +761,7 @@ clk = clock();
     Fra_ClausCollectLatchClauses( p, pSeq );
 if ( p->fVerbose )
 {
-//PRT( "Lat-cla", clock() - clk );
+//ABC_PRT( "Lat-cla", clock() - clk );
 }
     }
 
@@ -772,7 +772,7 @@ clk = clock();
     pManCut = Aig_ComputeCuts( p->pAig, p->nCutsMax, p->nLutSize, 0, p->fVerbose );
 if ( p->fVerbose )
 {
-//PRT( "Cuts   ", clock() - clk );
+//ABC_PRT( "Cuts   ", clock() - clk );
 }
 
     // collect combinational info for each cut
@@ -805,7 +805,7 @@ clk = clock();
     {
     printf( "Node = %5d. Cuts = %7d. Clauses = %6d. Clause/cut = %6.2f.\n", 
         Aig_ManNodeNum(p->pAig), nCuts, Vec_IntSize(p->vClauses), 1.0*Vec_IntSize(p->vClauses)/nCuts );
-    PRT( "Processing sim-info to find candidate clauses (unoptimized)", clock() - clk );
+    ABC_PRT( "Processing sim-info to find candidate clauses (unoptimized)", clock() - clk );
     }
 
     // filter out clauses that are contained in the already proven clauses
@@ -852,7 +852,7 @@ clk = clock();
             // check the clause
             for ( k = Beg; k < End; k++ )
                 pStart[k] = lit_neg( pStart[k] );
-            RetValue = sat_solver_solve( p->pSatMain, pStart + Beg, pStart + End, (sint64)p->nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
+            RetValue = sat_solver_solve( p->pSatMain, pStart + Beg, pStart + End, (ABC_INT64_T)p->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
             for ( k = Beg; k < End; k++ )
                 pStart[k] = lit_neg( pStart[k] );
             // the clause holds
@@ -924,7 +924,7 @@ int Fra_ClausBmcClauses( Clu_Man_t * p )
 
             for ( k = Beg; k < End; k++ )
                 pStart[k] = lit_neg( pStart[k] );
-            RetValue = sat_solver_solve( p->pSatBmc, pStart + Beg, pStart + End, (sint64)p->nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
+            RetValue = sat_solver_solve( p->pSatBmc, pStart + Beg, pStart + End, (ABC_INT64_T)p->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
             for ( k = Beg; k < End; k++ )
                 pStart[k] = lit_neg( pStart[k] );
 
@@ -1292,7 +1292,7 @@ int Fra_ClausInductiveClauses( Clu_Man_t * p )
 
         for ( k = Beg; k < End; k++ )
             pStart[k] = lit_neg( pStart[k] );
-        RetValue = sat_solver_solve( p->pSatMain, pStart + Beg, pStart + End, (sint64)p->nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
+        RetValue = sat_solver_solve( p->pSatMain, pStart + Beg, pStart + End, (ABC_INT64_T)p->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
         for ( k = Beg; k < End; k++ )
             pStart[k] = lit_neg( pStart[k] );
 
@@ -1359,7 +1359,7 @@ int Fra_ClausInductiveClauses( Clu_Man_t * p )
 Clu_Man_t * Fra_ClausAlloc( Aig_Man_t * pAig, int nFrames, int nPref, int nClausesMax, int nLutSize, int nLevels, int nCutsMax, int nBatches, int fStepUp, int fTarget, int fVerbose, int fVeryVerbose )
 {
     Clu_Man_t * p;
-    p = ALLOC( Clu_Man_t, 1 );
+    p = ABC_ALLOC( Clu_Man_t, 1 );
     memset( p, 0, sizeof(Clu_Man_t) );
     p->pAig          = pAig;
     p->nFrames       = nFrames;
@@ -1412,7 +1412,7 @@ void Fra_ClausFree( Clu_Man_t * p )
     if ( p->pCnf )      Cnf_DataFree( p->pCnf );
     if ( p->pSatMain )  sat_solver_delete( p->pSatMain );
     if ( p->pSatBmc )   sat_solver_delete( p->pSatBmc );
-    free( p );
+    ABC_FREE( p );
 }
 
 
@@ -1540,7 +1540,7 @@ void Fra_ClausWriteIndClauses( Clu_Man_t * p )
     int * pStart, * pVar2Id; 
     int Beg, End, i, k;
     // create mapping from SAT vars to node IDs
-    pVar2Id = ALLOC( int, p->pCnf->nVars );
+    pVar2Id = ABC_ALLOC( int, p->pCnf->nVars );
     memset( pVar2Id, 0xFF, sizeof(int) * p->pCnf->nVars );
     for ( i = 0; i < Aig_ManObjNumMax(p->pAig); i++ )
         if ( p->pCnf->pVarNums[i] >= 0 )
@@ -1564,7 +1564,7 @@ void Fra_ClausWriteIndClauses( Clu_Man_t * p )
         Aig_ObjCreatePo( pNew, pClause );
         Beg = End;
     }
-    free( pVar2Id );
+    ABC_FREE( pVar2Id );
     Aig_ManCleanup( pNew );
     pName = Ioa_FileNameGenericAppend( p->pAig->pName, "_care.aig" );
     printf( "Care one-hotness clauses will be written into file \"%s\".\n", pName );
@@ -1624,7 +1624,7 @@ void Fra_ClausEstimateCoverage( Clu_Man_t * p )
     Aig_ManRandom(1);
     pComb = Fra_SmlSimulateComb( p->pAig, nCombSimWords );
     // create mapping from SAT vars to node IDs
-    pVar2Id = ALLOC( int, p->pCnf->nVars );
+    pVar2Id = ABC_ALLOC( int, p->pCnf->nVars );
     memset( pVar2Id, 0, sizeof(int) * p->pCnf->nVars );
     for ( i = 0; i < Aig_ManObjNumMax(p->pAig); i++ )
         if ( p->pCnf->pVarNums[i] >= 0 )
@@ -1654,11 +1654,11 @@ void Fra_ClausEstimateCoverage( Clu_Man_t * p )
     for ( w = 0; w < nCombSimWords; w++ )
         nCovered += Aig_WordCountOnes( pResultTot[w] );
     Fra_SmlStop( pComb );
-    free( pVar2Id );
+    ABC_FREE( pVar2Id );
     // print the result
     printf( "Care states ratio = %f. ", 1.0 * (nCombSimWords * 32 - nCovered) / (nCombSimWords * 32) );
     printf( "(%d out of %d patterns)  ", nCombSimWords * 32 - nCovered, nCombSimWords * 32 );
-    PRT( "Time", clock() - clk );
+    ABC_PRT( "Time", clock() - clk );
 }
 
 
@@ -1686,7 +1686,7 @@ if ( p->fVerbose )
 {
     printf( "PARAMETERS: Frames = %d. Pref = %d. Clauses max = %d. Cut size = %d.\n", nFrames, nPref, nClausesMax, nLutSize );
     printf( "Level max = %d. Cuts max = %d. Batches = %d. Increment cut size = %s.\n", nLevels, nCutsMax, nBatches, fStepUp? "yes":"no" );
-//PRT( "Sim-seq", clock() - clk );
+//ABC_PRT( "Sim-seq", clock() - clk );
 }
 
     assert( !p->fTarget || Aig_ManPoNum(pAig) - Aig_ManRegNum(pAig) == 1 );
@@ -1700,7 +1700,7 @@ clk = clock();
 //        p->pAig->nRegs--;
 if ( fVerbose )
 {
-//PRT( "CNF    ", clock() - clk );
+//ABC_PRT( "CNF    ", clock() - clk );
 }
 
     // check BMC
@@ -1720,7 +1720,7 @@ clk = clock();
     }
 if ( fVerbose )
 {
-//PRT( "SAT-bmc", clock() - clk );
+//ABC_PRT( "SAT-bmc", clock() - clk );
 }
 
     // start the SAT solver
@@ -1751,7 +1751,7 @@ clk = clock();
         }
         if ( fVerbose )
         {
-//        PRT( "SAT-ind", clock() - clk );
+//        ABC_PRT( "SAT-ind", clock() - clk );
         }
  
         // collect the candidate inductive clauses using 4-cuts
@@ -1763,7 +1763,7 @@ clk = clock();
         p->nSimWordsPref = p->nPref*p->nSimWords/p->nSimFrames;
         nClausesBeg = p->nClauses;
 
-    //PRT( "Clauses", clock() - clk );
+    //ABC_PRT( "Clauses", clock() - clk );
 
 
         // check clauses using BMC
@@ -1775,7 +1775,7 @@ clk = clock();
             if ( fVerbose )
             {
                 printf( "BMC disproved %d clauses.  ", Counter );
-                PRT( "Time", clock() - clk );
+                ABC_PRT( "Time", clock() - clk );
             }
         }
 
@@ -1794,7 +1794,7 @@ clk = clock();
             {
             printf( "End = %5d. Exs = %5d.  ", p->nClauses, p->nCexes );
     //        printf( "\n" );
-            PRT( "Time", clock() - clk );
+            ABC_PRT( "Time", clock() - clk );
             }
             clk = clock();
         }
@@ -1809,14 +1809,14 @@ clk = clock();
                 printf( "Property FAILS during refinement.  " );
             else
                 printf( "Property HOLDS inductively after strengthening.  " );
-            PRT( "Time  ", clock() - clkTotal );
+            ABC_PRT( "Time  ", clock() - clkTotal );
             if ( !p->fFail )
                 break;
         }
         else
         {
             printf( "Finished proving inductive clauses. " );
-            PRT( "Time  ", clock() - clkTotal );
+            ABC_PRT( "Time  ", clock() - clkTotal );
         }
     }
 
diff --git a/src/aig/fra/fraCnf.c b/src/aig/fra/fraCnf.c
index d96fe8a1..27da3fc5 100644
--- a/src/aig/fra/fraCnf.c
+++ b/src/aig/fra/fraCnf.c
@@ -131,7 +131,7 @@ void Fra_AddClausesSuper( Fra_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vSuper )
     assert( Aig_ObjIsNode( pNode ) );
     // create storage for literals
     nLits = Vec_PtrSize(vSuper) + 1;
-    pLits = ALLOC( int, nLits );
+    pLits = ABC_ALLOC( int, nLits );
     // suppose AND-gate is A & B = C
     // add !A => !C   or   A + !C
     Vec_PtrForEachEntry( vSuper, pFanin, i )
@@ -147,7 +147,7 @@ void Fra_AddClausesSuper( Fra_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vSuper )
     pLits[nLits-1] = toLitCond(Fra_ObjSatNum(pNode), 0);
     RetValue = sat_solver_addclause( p->pSat, pLits, pLits + nLits );
     assert( RetValue );
-    free( pLits );
+    ABC_FREE( pLits );
 }
 
 /**Function*************************************************************
diff --git a/src/aig/fra/fraHot.c b/src/aig/fra/fraHot.c
index b2156193..c4472121 100644
--- a/src/aig/fra/fraHot.c
+++ b/src/aig/fra/fraHot.c
@@ -378,7 +378,7 @@ void Fra_OneHotEstimateCoverage( Fra_Man_t * p, Vec_Int_t * vOneHots )
     // print the result
     printf( "Care states ratio = %f. ", 1.0 * (nSimWords * 32 - nCovered) / (nSimWords * 32) );
     printf( "(%d out of %d patterns)  ", nSimWords * 32 - nCovered, nSimWords * 32 );
-    PRT( "Time", clock() - clk );
+    ABC_PRT( "Time", clock() - clk );
 }
 
 /**Function*************************************************************
diff --git a/src/aig/fra/fraImp.c b/src/aig/fra/fraImp.c
index e2bee834..d579146e 100644
--- a/src/aig/fra/fraImp.c
+++ b/src/aig/fra/fraImp.c
@@ -64,7 +64,7 @@ static inline int * Fra_SmlCountOnes( Fra_Sml_t * p )
 {
     Aig_Obj_t * pObj;
     int i, * pnBits; 
-    pnBits = ALLOC( int, Aig_ManObjNumMax(p->pAig) );  
+    pnBits = ABC_ALLOC( int, Aig_ManObjNumMax(p->pAig) );  
     memset( pnBits, 0, sizeof(int) * Aig_ManObjNumMax(p->pAig) );
     Aig_ManForEachObj( p->pAig, pObj, i )
         pnBits[i] = Fra_SmlCountOnesOne( p, i );
@@ -159,7 +159,7 @@ Vec_Ptr_t * Fra_SmlSortUsingOnes( Fra_Sml_t * p, int fLatchCorr )
     // count number of nodes having that many 1s
     nNodes = 0;
     nBits = p->nWordsTotal * 32;
-    pnNodes = ALLOC( int, nBits + 1 );
+    pnNodes = ABC_ALLOC( int, nBits + 1 );
     memset( pnNodes, 0, sizeof(int) * (nBits + 1) );
     Aig_ManForEachObj( p->pAig, pObj, i )
     {
@@ -183,7 +183,7 @@ Vec_Ptr_t * Fra_SmlSortUsingOnes( Fra_Sml_t * p, int fLatchCorr )
         nNodes++;
     }
     // allocate memory for all the nodes
-    pMemory = ALLOC( int, nNodes + nBits + 1 );  
+    pMemory = ABC_ALLOC( int, nNodes + nBits + 1 );  
     // markup the memory for each node
     vNodes = Vec_PtrAlloc( nBits + 1 );
     Vec_PtrPush( vNodes, pMemory );
@@ -222,8 +222,8 @@ Vec_Ptr_t * Fra_SmlSortUsingOnes( Fra_Sml_t * p, int fLatchCorr )
         nTotal += pnNodes[i];
     }
     assert( nTotal == nNodes + nBits + 1 );
-    free( pnNodes );
-    free( pnBits );
+    ABC_FREE( pnNodes );
+    ABC_FREE( pnBits );
     return vNodes;
 }
 
@@ -244,7 +244,7 @@ Vec_Int_t * Fra_SmlSelectMaxCost( Vec_Int_t * vImps, int * pCosts, int nCostMax,
     int * pCostCount, nImpCount, Imp, i, c;
     assert( Vec_IntSize(vImps) >= nImpLimit );
     // count how many implications have each cost
-    pCostCount = ALLOC( int, nCostMax + 1 );
+    pCostCount = ABC_ALLOC( int, nCostMax + 1 );
     memset( pCostCount, 0, sizeof(int) * (nCostMax + 1) );
     for ( i = 0; i < Vec_IntSize(vImps); i++ )
     {
@@ -271,7 +271,7 @@ Vec_Int_t * Fra_SmlSelectMaxCost( Vec_Int_t * vImps, int * pCosts, int nCostMax,
         if ( Vec_IntSize( vImpsNew ) == nImpLimit )
             break;
     }
-    free( pCostCount );
+    ABC_FREE( pCostCount );
     if ( pCostRange )
         *pCostRange = c;
     return vImpsNew;
@@ -329,7 +329,7 @@ Vec_Int_t * Fra_ImpDerive( Fra_Man_t * p, int nImpMaxLimit, int nImpUseLimit, in
     assert( nImpMaxLimit > 0 && nImpUseLimit > 0 && nImpUseLimit <= nImpMaxLimit );
     // normalize both managers
     pComb = Fra_SmlSimulateComb( p->pManAig, nSimWords );
-    pSeq = Fra_SmlSimulateSeq( p->pManAig, p->pPars->nFramesP, nSimWords, 1 );
+    pSeq = Fra_SmlSimulateSeq( p->pManAig, p->pPars->nFramesP, nSimWords, 1, 1  );
     // get the nodes sorted by the number of 1s
     vNodes = Fra_SmlSortUsingOnes( pSeq, fLatchCorr );
     // count the total number of implications
@@ -340,7 +340,7 @@ Vec_Int_t * Fra_ImpDerive( Fra_Man_t * p, int nImpMaxLimit, int nImpUseLimit, in
         nImpsTotal++;
 
     // compute implications and their costs
-    pImpCosts = ALLOC( int, nImpMaxLimit );
+    pImpCosts = ABC_ALLOC( int, nImpMaxLimit );
     vImps = Vec_IntAlloc( nImpMaxLimit );
     for ( k = pSeq->nWordsTotal * 32; k > 0; k-- )
         for ( i = k - 1; i > 0; i-- )
@@ -384,8 +384,11 @@ finish:
     }
 
     // dealloc
-    free( pImpCosts ); 
-    free( Vec_PtrEntry(vNodes, 0) );
+    ABC_FREE( pImpCosts ); 
+    {
+    void * pTemp = Vec_PtrEntry(vNodes, 0);
+    ABC_FREE( pTemp );
+    }
     Vec_PtrFree( vNodes );
     // reorder implications topologically
     qsort( (void *)Vec_IntArray(vImps), Vec_IntSize(vImps), sizeof(int), 
@@ -396,7 +399,7 @@ printf( "Implications: All = %d. Try = %d. NonSeq = %d. Comb = %d. Res = %d.\n",
     nImpsTotal, nImpsTried, nImpsNonSeq, nImpsComb, nImpsCollected );
 printf( "Implication weight: Min = %d. Pivot = %d. Max = %d.   ", 
        CostMin, CostRange, CostMax );
-PRT( "Time", clock() - clk );
+ABC_PRT( "Time", clock() - clk );
 }
     return vImps;
 }
@@ -665,9 +668,9 @@ int Fra_ImpVerifyUsingSimulation( Fra_Man_t * p )
     if ( p->pCla->vImps == NULL || Vec_IntSize(p->pCla->vImps) == 0 )
         return 0;
     // simulate the AIG manager with combinational patterns
-    pSeq = Fra_SmlSimulateSeq( p->pManAig, p->pPars->nFramesP, nFrames, nSimWords );
+    pSeq = Fra_SmlSimulateSeq( p->pManAig, p->pPars->nFramesP, nFrames, nSimWords, 1  );
     // go through the implications and check how many of them do not hold
-    pfFails = ALLOC( char, Vec_IntSize(p->pCla->vImps) );
+    pfFails = ABC_ALLOC( char, Vec_IntSize(p->pCla->vImps) );
     memset( pfFails, 0, sizeof(char) * Vec_IntSize(p->pCla->vImps) );
     Vec_IntForEachEntry( p->pCla->vImps, Imp, i )
     {
@@ -679,7 +682,7 @@ int Fra_ImpVerifyUsingSimulation( Fra_Man_t * p )
     Counter = 0;
     for ( i = 0; i < Vec_IntSize(p->pCla->vImps); i++ )
         Counter += pfFails[i];
-    free( pfFails );
+    ABC_FREE( pfFails );
     Fra_SmlStop( pSeq );
     return Counter;
 }
diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c
index c8b35b28..4f3812c6 100644
--- a/src/aig/fra/fraInd.c
+++ b/src/aig/fra/fraInd.c
@@ -198,7 +198,7 @@ void Fra_FramesAddMore( Aig_Man_t * p, int nFrames )
         pObj->pData = pObj;
     // iterate and add objects
     nNodesOld = Aig_ManObjNumMax(p);
-    pLatches = ALLOC( Aig_Obj_t *, Aig_ManRegNum(p) );
+    pLatches = ABC_ALLOC( Aig_Obj_t *, Aig_ManRegNum(p) );
     for ( f = 0; f < nFrames; f++ )
     {
         // clean latch inputs and outputs
@@ -230,7 +230,7 @@ void Fra_FramesAddMore( Aig_Man_t * p, int nFrames )
                 pObj->pData = NULL;
         }
     }
-    free( pLatches );
+    ABC_FREE( pLatches );
 }
 
 
@@ -308,7 +308,7 @@ Aig_Man_t * Fra_FraigInductionPart( Aig_Man_t * pAig, Fra_Ssw_t * pPars )
                 i, Vec_IntSize(vPart), Aig_ManPiNum(pTemp)-Vec_IntSize(vPart), nCountPis, nCountRegs, Aig_ManNodeNum(pTemp), pPars->nIters, nClasses );
         Aig_ManStop( pNew );
         Aig_ManStop( pTemp );
-        free( pMapBack );
+        ABC_FREE( pMapBack );
     }
     // remap the AIG
     pNew = Aig_ManDupRepr( pAig, 0 );
@@ -320,7 +320,7 @@ Aig_Man_t * Fra_FraigInductionPart( Aig_Man_t * pAig, Fra_Ssw_t * pPars )
     pPars->fVerbose = fVerbose;
     if ( fVerbose )
     {
-        PRT( "Total time", clock() - clk );
+        ABC_PRT( "Total time", clock() - clk );
     }
     return pNew;
 }
@@ -420,10 +420,10 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, Fra_Ssw_t * pParams )
         // refine the classes with more simulation rounds
 if ( pPars->fVerbose )
 printf( "Simulating %d AIG nodes for %d cycles ... ", Aig_ManNodeNum(pManAig), pPars->nFramesP + 32 );
-        p->pSml = Fra_SmlSimulateSeq( pManAig, pPars->nFramesP, 32, 1 ); //pPars->nFramesK + 1, 1 );  
+        p->pSml = Fra_SmlSimulateSeq( pManAig, pPars->nFramesP, 32, 1, 1  ); //pPars->nFramesK + 1, 1 );  
 if ( pPars->fVerbose ) 
 {
-PRT( "Time", clock() - clk );
+ABC_PRT( "Time", clock() - clk );
 }
         Fra_ClassesPrepare( p->pCla, p->pPars->fLatchCorr, p->pPars->nMaxLevs );
 //        Fra_ClassesPostprocess( p->pCla );
@@ -556,7 +556,7 @@ clk2 = clock();
         Fra_FraigSweep( p );
         if ( pPars->fVerbose )
         {
-            PRT( "T", clock() - clk3 );
+            ABC_PRT( "T", clock() - clk3 );
         } 
 
 //        Sat_SolverPrintStats( stdout, p->pSat );
@@ -589,7 +589,7 @@ clk2 = clock();
             printf( "Implications failing the simulation test = %d (out of %d).  ", Temp, Vec_IntSize(p->pCla->vImps) );
         else
             printf( "All %d implications have passed the simulation test.  ", Vec_IntSize(p->pCla->vImps) );
-        PRT( "Time", clock() - clk );
+        ABC_PRT( "Time", clock() - clk );
     }
 */
 
@@ -629,7 +629,7 @@ p->timeTotal = clock() - clk;
     p->nLitsEnd  = Fra_ClassesCountLits( p->pCla );
     p->nNodesEnd = Aig_ManNodeNum(pManAigNew);
     p->nRegsEnd  = Aig_ManRegNum(pManAigNew);
-    // free the manager
+    // ABC_FREE the manager
 finish:
     Fra_ManStop( p );
     // check the output
diff --git a/src/aig/fra/fraIndVer.c b/src/aig/fra/fraIndVer.c
index efc516c9..71faa346 100644
--- a/src/aig/fra/fraIndVer.c
+++ b/src/aig/fra/fraIndVer.c
@@ -150,7 +150,7 @@ int Fra_InvariantVerify( Aig_Man_t * pAig, int nFrames, Vec_Int_t * vClauses, Ve
     if ( CounterBase || CounterInd )
         return 0;
     printf( "Invariant verification: %d clauses verified correctly.  ", Vec_IntSize(vClauses) );
-    PRT( "Time", clock() - clk );
+    ABC_PRT( "Time", clock() - clk );
     return 1;
 }
 
diff --git a/src/aig/fra/fraLcr.c b/src/aig/fra/fraLcr.c
index d3be9842..16912f46 100644
--- a/src/aig/fra/fraLcr.c
+++ b/src/aig/fra/fraLcr.c
@@ -77,12 +77,12 @@ struct Fra_Lcr_t_
 Fra_Lcr_t * Lcr_ManAlloc( Aig_Man_t * pAig )
 {
     Fra_Lcr_t * p;
-    p = ALLOC( Fra_Lcr_t, 1 );
+    p = ABC_ALLOC( Fra_Lcr_t, 1 );
     memset( p, 0, sizeof(Fra_Lcr_t) );
     p->pAig = pAig;
-    p->pInToOutPart = ALLOC( int, Aig_ManPiNum(pAig) );
+    p->pInToOutPart = ABC_ALLOC( int, Aig_ManPiNum(pAig) );
     memset( p->pInToOutPart, 0, sizeof(int) * Aig_ManPiNum(pAig) );
-    p->pInToOutNum = ALLOC( int, Aig_ManPiNum(pAig) );
+    p->pInToOutNum = ABC_ALLOC( int, Aig_ManPiNum(pAig) );
     memset( p->pInToOutNum, 0, sizeof(int) * Aig_ManPiNum(pAig) );
     p->vFraigs = Vec_PtrAlloc( 1000 );
     return p;
@@ -106,12 +106,12 @@ void Lcr_ManPrint( Fra_Lcr_t * p )
     printf( "NBeg = %d. NEnd = %d. (Gain = %6.2f %%).  RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n", 
         p->nNodesBeg, p->nNodesEnd, 100.0*(p->nNodesBeg-p->nNodesEnd)/p->nNodesBeg, 
         p->nRegsBeg, p->nRegsEnd, 100.0*(p->nRegsBeg-p->nRegsEnd)/p->nRegsBeg );
-    PRT( "AIG simulation  ", p->timeSim  );
-    PRT( "AIG partitioning", p->timePart );
-    PRT( "AIG rebuiding   ", p->timeTrav );
-    PRT( "FRAIGing        ", p->timeFraig );
-    PRT( "AIG updating    ", p->timeUpdate );
-    PRT( "TOTAL RUNTIME   ", p->timeTotal );
+    ABC_PRT( "AIG simulation  ", p->timeSim  );
+    ABC_PRT( "AIG partitioning", p->timePart );
+    ABC_PRT( "AIG rebuiding   ", p->timeTrav );
+    ABC_PRT( "FRAIGing        ", p->timeFraig );
+    ABC_PRT( "AIG updating    ", p->timeUpdate );
+    ABC_PRT( "TOTAL RUNTIME   ", p->timeTotal );
 }
 
 /**Function*************************************************************
@@ -136,9 +136,9 @@ void Lcr_ManFree( Fra_Lcr_t * p )
     Vec_PtrFree( p->vFraigs );
     if ( p->pCla  )     Fra_ClassesStop( p->pCla );
     if ( p->vParts  )   Vec_VecFree( (Vec_Vec_t *)p->vParts );
-    free( p->pInToOutPart );
-    free( p->pInToOutNum );
-    free( p );
+    ABC_FREE( p->pInToOutPart );
+    ABC_FREE( p->pInToOutNum );
+    ABC_FREE( p );
 }
 
 /**Function*************************************************************
@@ -157,7 +157,7 @@ Fra_Man_t * Fra_LcrAigPrepare( Aig_Man_t * pAig )
     Fra_Man_t * p;
     Aig_Obj_t * pObj;
     int i;
-    p = ALLOC( Fra_Man_t, 1 );
+    p = ABC_ALLOC( Fra_Man_t, 1 );
     memset( p, 0, sizeof(Fra_Man_t) );
 //    Aig_ManForEachPi( pAig, pObj, i )
     Aig_ManForEachObj( pAig, pObj, i )
@@ -550,10 +550,10 @@ Aig_Man_t * Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int nFramesP, int nC
 clk2 = clock();
 if ( fVerbose )
 printf( "Simulating AIG with %d nodes for %d cycles ...  ", Aig_ManNodeNum(pAig), nFramesP + 32 );
-    pSml = Fra_SmlSimulateSeq( pAig, nFramesP, 32, 1 ); 
+    pSml = Fra_SmlSimulateSeq( pAig, nFramesP, 32, 1, 1  ); 
 if ( fVerbose ) 
 {
-PRT( "Time", clock() - clk2 );
+ABC_PRT( "Time", clock() - clk2 );
 }
 timeSim = clock() - clk2;
 
@@ -592,7 +592,7 @@ printf( "Partitioning AIG ...  " );
     Aig_ManStop( pAigPart );
 if ( fVerbose ) 
 {
-PRT( "Time", clock() - clk2 );
+ABC_PRT( "Time", clock() - clk2 );
 p->timePart += clock() - clk2;
 }
 
@@ -636,7 +636,7 @@ p->timeFraig += clock() - clk2;
                 Aig_ManDumpBlif( pAigPart, Name, NULL, NULL );
             }
 printf( "Finished part %4d (out of %4d).  ", i, Vec_PtrSize(p->vParts) );
-PRT( "Time", clock() - clk3 );
+ABC_PRT( "Time", clock() - clk3 );
 */
 
             Aig_ManStop( pAigPart );
@@ -648,7 +648,7 @@ PRT( "Time", clock() - clk3 );
             printf( "%3d : Const = %6d. Class = %6d.  L = %6d. Part = %3d.  ", 
                 nIter, Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses), 
                 Fra_ClassesCountLits(p->pCla), Vec_PtrSize(p->vParts) );
-            PRT( "T", clock() - clk3 );
+            ABC_PRT( "T", clock() - clk3 );
         }
         // refine the classes
         Fra_LcrAigPrepareTwo( p->pAig, pTemp );
@@ -690,7 +690,7 @@ p->timeTotal = clock() - clk;
     p->nNodesEnd = Aig_ManNodeNum(pAigNew);
     p->nRegsEnd  = Aig_ManRegNum(pAigNew);
 finish:
-    free( pTemp );
+    ABC_FREE( pTemp );
     Lcr_ManFree( p );
     if ( pnIter ) *pnIter = nIter;
     return pAigNew;
diff --git a/src/aig/fra/fraMan.c b/src/aig/fra/fraMan.c
index b8cf13c5..8bdd147d 100644
--- a/src/aig/fra/fraMan.c
+++ b/src/aig/fra/fraMan.c
@@ -104,7 +104,7 @@ Fra_Man_t * Fra_ManStart( Aig_Man_t * pManAig, Fra_Par_t * pPars )
     Aig_Obj_t * pObj;
     int i;
     // allocate the fraiging manager
-    p = ALLOC( Fra_Man_t, 1 );
+    p = ABC_ALLOC( Fra_Man_t, 1 );
     memset( p, 0, sizeof(Fra_Man_t) );
     p->pPars      = pPars;
     p->pManAig    = pManAig;
@@ -112,12 +112,12 @@ Fra_Man_t * Fra_ManStart( Aig_Man_t * pManAig, Fra_Par_t * pPars )
     p->nFramesAll = pPars->nFramesK + 1;
     // allocate storage for sim pattern
     p->nPatWords  = Aig_BitWordNum( (Aig_ManPiNum(pManAig) - Aig_ManRegNum(pManAig)) * p->nFramesAll + Aig_ManRegNum(pManAig) );
-    p->pPatWords  = ALLOC( unsigned, p->nPatWords ); 
+    p->pPatWords  = ABC_ALLOC( unsigned, p->nPatWords ); 
     p->vPiVars    = Vec_PtrAlloc( 100 );
     // equivalence classes
     p->pCla       = Fra_ClassesStart( pManAig );
     // allocate other members
-    p->pMemFraig  = ALLOC( Aig_Obj_t *, p->nSizeAlloc * p->nFramesAll );
+    p->pMemFraig  = ABC_ALLOC( Aig_Obj_t *, p->nSizeAlloc * p->nFramesAll );
     memset( p->pMemFraig, 0, sizeof(Aig_Obj_t *) * p->nSizeAlloc * p->nFramesAll );
     // set random number generator
 //    srand( 0xABCABC );
@@ -150,8 +150,8 @@ void Fra_ManClean( Fra_Man_t * p, int nNodesMax )
     if ( p->nMemAlloc < nNodesMax )
     {
         int nMemAllocNew = nNodesMax + 5000;
-        p->pMemFanins = REALLOC( Vec_Ptr_t *, p->pMemFanins, nMemAllocNew );
-        p->pMemSatNums = REALLOC( int, p->pMemSatNums, nMemAllocNew );
+        p->pMemFanins = ABC_REALLOC( Vec_Ptr_t *, p->pMemFanins, nMemAllocNew );
+        p->pMemSatNums = ABC_REALLOC( int, p->pMemSatNums, nMemAllocNew );
         p->nMemAlloc = nMemAllocNew;
     }
     // prepare for the new run
@@ -191,9 +191,9 @@ Aig_Man_t * Fra_ManPrepareComb( Fra_Man_t * p )
         pObj->pData = p;
     // allocate memory for mapping FRAIG nodes into SAT numbers and fanins
     p->nMemAlloc = p->nSizeAlloc;
-    p->pMemFanins = ALLOC( Vec_Ptr_t *, p->nMemAlloc );
+    p->pMemFanins = ABC_ALLOC( Vec_Ptr_t *, p->nMemAlloc );
     memset( p->pMemFanins, 0, sizeof(Vec_Ptr_t *) * p->nMemAlloc );
-    p->pMemSatNums = ALLOC( int, p->nMemAlloc );
+    p->pMemSatNums = ABC_ALLOC( int, p->nMemAlloc );
     memset( p->pMemSatNums, 0, sizeof(int) * p->nMemAlloc );
     // make sure the satisfying assignment is node assigned
     assert( pManFraig->pData == NULL );
@@ -242,7 +242,7 @@ void Fra_ManStop( Fra_Man_t * p )
     if ( p->pManAig )
     {
         if ( p->pManAig->pObjCopies )
-            free( p->pManAig->pObjCopies );
+            ABC_FREE( p->pManAig->pObjCopies );
         p->pManAig->pObjCopies = p->pMemFraig;
         p->pMemFraig = NULL;
     }
@@ -254,11 +254,11 @@ void Fra_ManStop( Fra_Man_t * p )
     if ( p->pSml )      Fra_SmlStop( p->pSml );
     if ( p->vCex )      Vec_IntFree( p->vCex );
     if ( p->vOneHots )  Vec_IntFree( p->vOneHots );
-    FREE( p->pMemFraig );
-    FREE( p->pMemFanins );
-    FREE( p->pMemSatNums );
-    FREE( p->pPatWords );
-    free( p );
+    ABC_FREE( p->pMemFraig );
+    ABC_FREE( p->pMemFanins );
+    ABC_FREE( p->pMemSatNums );
+    ABC_FREE( p->pPatWords );
+    ABC_FREE( p );
 }
 
 /**Function*************************************************************
@@ -284,19 +284,19 @@ void Fra_ManPrint( Fra_Man_t * p )
         p->nRegsBeg, p->nRegsEnd, 100.0*(p->nRegsBeg-p->nRegsEnd)/(p->nRegsBeg?p->nRegsBeg:1) );
     if ( p->pSat )             Sat_SolverPrintStats( stdout, p->pSat );
     if ( p->pPars->fUse1Hot )  Fra_OneHotEstimateCoverage( p, p->vOneHots );
-    PRT( "AIG simulation  ", p->pSml->timeSim  );
-    PRT( "AIG traversal   ", p->timeTrav );
+    ABC_PRT( "AIG simulation  ", p->pSml->timeSim  );
+    ABC_PRT( "AIG traversal   ", p->timeTrav );
     if ( p->timeRwr )
     {
-    PRT( "AIG rewriting   ", p->timeRwr  );
+    ABC_PRT( "AIG rewriting   ", p->timeRwr  );
     }
-    PRT( "SAT solving     ", p->timeSat  );
-    PRT( "    Unsat       ", p->timeSatUnsat );
-    PRT( "    Sat         ", p->timeSatSat   );
-    PRT( "    Fail        ", p->timeSatFail  );
-    PRT( "Class refining  ", p->timeRef   );
-    PRT( "TOTAL RUNTIME   ", p->timeTotal );
-    if ( p->time1 ) { PRT( "time1           ", p->time1 ); }
+    ABC_PRT( "SAT solving     ", p->timeSat  );
+    ABC_PRT( "    Unsat       ", p->timeSatUnsat );
+    ABC_PRT( "    Sat         ", p->timeSatSat   );
+    ABC_PRT( "    Fail        ", p->timeSatFail  );
+    ABC_PRT( "Class refining  ", p->timeRef   );
+    ABC_PRT( "TOTAL RUNTIME   ", p->timeTotal );
+    if ( p->time1 ) { ABC_PRT( "time1           ", p->time1 ); }
     if ( p->nSpeculs )
     printf( "Speculations = %d.\n", p->nSpeculs );
     fflush( stdout );
diff --git a/src/aig/fra/fraPart.c b/src/aig/fra/fraPart.c
index 1766b978..6dfbd2e9 100644
--- a/src/aig/fra/fraPart.c
+++ b/src/aig/fra/fraPart.c
@@ -59,7 +59,7 @@ void Fra_ManPartitionTest( Aig_Man_t * p, int nComLim )
     // compute supports
 clk = clock();
     vSupps = (Vec_Vec_t *)Aig_ManSupports( p );
-PRT( "Supports", clock() - clk );
+ABC_PRT( "Supports", clock() - clk );
     // remove last entry
     Aig_ManForEachPo( p, pObj, i )
     {
@@ -76,9 +76,9 @@ clk = clock();
     {
         vSup = Vec_VecEntry( vSupps, i );
         Vec_IntForEachEntry( vSup, Entry, k )
-            Vec_VecPush( vSuppsIn, Entry, (void *)(PORT_PTRUINT_T)i );
+            Vec_VecPush( vSuppsIn, Entry, (void *)(ABC_PTRUINT_T)i );
     }
-PRT( "Inverse ", clock() - clk );
+ABC_PRT( "Inverse ", clock() - clk );
 
 clk = clock();
     // compute extended supports
@@ -153,7 +153,7 @@ clk = clock();
 */
     }
 //    Bar_ProgressStop( pProgress );
-PRT( "Scanning", clock() - clk );
+ABC_PRT( "Scanning", clock() - clk );
 
     // print cumulative statistics
     printf( "PIs = %6d. POs = %6d. Lim = %3d.   AveS = %3d. SN = %3d. R = %4.2f Max = %5d.\n",
@@ -193,7 +193,7 @@ void Fra_ManPartitionTest2( Aig_Man_t * p )
     // compute supports
 clk = clock();
     vSupps = (Vec_Vec_t *)Aig_ManSupports( p );
-PRT( "Supports", clock() - clk );
+ABC_PRT( "Supports", clock() - clk );
     // remove last entry
     Aig_ManForEachPo( p, pObj, i )
     {
@@ -212,13 +212,13 @@ clk = clock();
             break;
         vSup = Vec_VecEntry( vSupps, i );
         Vec_IntForEachEntry( vSup, Entry, k )
-            Vec_VecPush( vSuppsIn, Entry, (void *)(PORT_PTRUINT_T)i );
+            Vec_VecPush( vSuppsIn, Entry, (void *)(ABC_PTRUINT_T)i );
     }
-PRT( "Inverse ", clock() - clk );
+ABC_PRT( "Inverse ", clock() - clk );
 
     // create affective supports
 clk = clock();
-    pSupp = ALLOC( char, Aig_ManPiNum(p) );
+    pSupp = ABC_ALLOC( char, Aig_ManPiNum(p) );
     Aig_ManForEachPo( p, pObj, i )
     {
         if ( i % 50 != 0 )
@@ -248,9 +248,9 @@ clk = clock();
         printf( "%d(%d) ", Vec_IntSize(vSup), Counter );
     }
     printf( "\n" );
-PRT( "Extension ", clock() - clk );
+ABC_PRT( "Extension ", clock() - clk );
 
-    free( pSupp );
+    ABC_FREE( pSupp );
     Vec_VecFree( vSupps );
     Vec_VecFree( vSuppsIn );
 }
diff --git a/src/aig/fra/fraSat.c b/src/aig/fra/fraSat.c
index 8332fa77..c2eaf453 100644
--- a/src/aig/fra/fraSat.c
+++ b/src/aig/fra/fraSat.c
@@ -101,7 +101,7 @@ clk = clock();
     pLits[1] = toLitCond( Fra_ObjSatNum(pNew), pOld->fPhase == pNew->fPhase );
 //Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 );
     RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2, 
-        (sint64)nBTLimit, (sint64)0, 
+        (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, 
         p->nBTLimitGlobal, p->nInsLimitGlobal );
 p->timeSat += clock() - clk;
     if ( RetValue1 == l_False )
@@ -145,7 +145,7 @@ clk = clock();
     pLits[0] = toLitCond( Fra_ObjSatNum(pOld), 1 );
     pLits[1] = toLitCond( Fra_ObjSatNum(pNew), pOld->fPhase ^ pNew->fPhase );
     RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2, 
-        (sint64)nBTLimit, (sint64)0, 
+        (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, 
         p->nBTLimitGlobal, p->nInsLimitGlobal );
 p->timeSat += clock() - clk;
     if ( RetValue1 == l_False )
@@ -177,12 +177,12 @@ p->timeSatFail += clock() - clk;
     // check BDD proof
     {
         int RetVal;
-        PRT( "Sat", clock() - clk2 );
+        ABC_PRT( "Sat", clock() - clk2 );
         clk2 = clock();
         RetVal = Fra_NodesAreEquivBdd( pOld, pNew );
 //        printf( "%d ", RetVal );
         assert( RetVal );
-        PRT( "Bdd", clock() - clk2 );
+        ABC_PRT( "Bdd", clock() - clk2 );
         printf( "\n" );
     }
 */
@@ -263,7 +263,7 @@ clk = clock();
     pLits[1] = toLitCond( Fra_ObjSatNum(pNew), !fComplR );
 //Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 );
     RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2, 
-        (sint64)nBTLimit, (sint64)0, 
+        (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, 
         p->nBTLimitGlobal, p->nInsLimitGlobal );
 p->timeSat += clock() - clk;
     if ( RetValue1 == l_False )
@@ -370,7 +370,7 @@ clk = clock();
     pLits[1] = toLitCond( Fra_ObjSatNum(pNew), !fComplR );
 //Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 );
     RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2, 
-        (sint64)nBTLimit, (sint64)0, 
+        (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, 
         p->nBTLimitGlobal, p->nInsLimitGlobal );
 p->timeSat += clock() - clk;
     if ( RetValue1 == l_False )
@@ -447,7 +447,7 @@ int Fra_NodeIsConst( Fra_Man_t * p, Aig_Obj_t * pNew )
 clk = clock();
     pLits[0] = toLitCond( Fra_ObjSatNum(pNew), pNew->fPhase );
     RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 1, 
-        (sint64)p->pPars->nBTLimitMiter, (sint64)0, 
+        (ABC_INT64_T)p->pPars->nBTLimitMiter, (ABC_INT64_T)0, 
         p->nBTLimitGlobal, p->nInsLimitGlobal );
 p->timeSat += clock() - clk;
     if ( RetValue1 == l_False )
diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c
index 7545059f..a97af278 100644
--- a/src/aig/fra/fraSec.c
+++ b/src/aig/fra/fraSec.c
@@ -121,7 +121,7 @@ clk = clock();
     {
         printf( "Sequential cleanup:   Latches = %5d. Nodes = %6d. ", 
             Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
-PRT( "Time", clock() - clk );
+ABC_PRT( "Time", clock() - clk );
     }
     RetValue = Fra_FraigMiterStatus( pNew );
     if ( RetValue >= 0 )
@@ -140,7 +140,7 @@ clk = clock();
         {
             printf( "Phase abstraction:    Latches = %5d. Nodes = %6d. ", 
                 Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
-PRT( "Time", clock() - clk );
+ABC_PRT( "Time", clock() - clk );
         }
     }
 
@@ -155,7 +155,7 @@ clk = clock();
     {
         printf( "Forward retiming:     Latches = %5d. Nodes = %6d. ", 
             Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
-PRT( "Time", clock() - clk );
+ABC_PRT( "Time", clock() - clk );
     }
     }
      
@@ -199,9 +199,9 @@ clk = clock();
             printf( "The counter-example is invalid because of phase abstraction.\n" );
         else
         {
-        FREE( p->pSeqModel );
+        ABC_FREE( p->pSeqModel );
         p->pSeqModel = Ssw_SmlDupCounterExample( pTemp->pSeqModel, Aig_ManRegNum(p) );
-        FREE( pTemp->pSeqModel );
+        ABC_FREE( pTemp->pSeqModel );
         }
     }
     if ( pNew == NULL )
@@ -212,12 +212,12 @@ clk = clock();
             if ( !pParSec->fSilent )
             {
                 printf( "Networks are NOT EQUIVALENT after simulation.   " );
-PRT( "Time", clock() - clkTotal );
+ABC_PRT( "Time", clock() - clkTotal );
             }
             if ( pParSec->fReportSolution && !pParSec->fRecursive )
             {
             printf( "SOLUTION: FAIL       " );
-PRT( "Time", clock() - clkTotal );
+ABC_PRT( "Time", clock() - clkTotal );
             }
             Aig_ManStop( pTemp );
             return RetValue;
@@ -233,7 +233,7 @@ PRT( "Time", clock() - clkTotal );
     {
         printf( "Latch-corr (I=%3d):   Latches = %5d. Nodes = %6d. ", 
             nIter, Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
-PRT( "Time", clock() - clk );
+ABC_PRT( "Time", clock() - clk );
     }
     }
 /*
@@ -261,7 +261,7 @@ clk = clock();
     {
         printf( "Fraiging:             Latches = %5d. Nodes = %6d. ", 
             Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
-PRT( "Time", clock() - clk );
+ABC_PRT( "Time", clock() - clk );
     }
     }
 
@@ -302,7 +302,7 @@ clk = clock();
     {
     printf( "Min-reg retiming:     Latches = %5d. Nodes = %6d. ", 
         Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
-PRT( "Time", clock() - clk );
+ABC_PRT( "Time", clock() - clk );
     }
     }
 
@@ -370,7 +370,7 @@ clk = clock();
         { 
             printf( "K-step (K=%2d,I=%3d):  Latches = %5d. Nodes = %6d. ", 
                 nFrames, pPars2->nIters, Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
-PRT( "Time", clock() - clk );
+ABC_PRT( "Time", clock() - clk );
         }
         if ( RetValue != -1 )
             break;
@@ -392,9 +392,9 @@ clk = clock();
         {
             printf( "Min-reg retiming:     Latches = %5d. Nodes = %6d. ", 
                 Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
-PRT( "Time", clock() - clk );
-        }
+ABC_PRT( "Time", clock() - clk );
         }
+        }  
 
         if ( pNew->nRegs )
             pNew = Aig_ManConstReduce( pNew, 0 );
@@ -410,19 +410,19 @@ clk = clock();
         {
             printf( "Rewriting:            Latches = %5d. Nodes = %6d. ", 
                 Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
-PRT( "Time", clock() - clk );
+ABC_PRT( "Time", clock() - clk );
         } 
 
         // perform sequential simulation
         if ( pNew->nRegs )
         {
 clk = clock();
-        pSml = Fra_SmlSimulateSeq( pNew, 0, 128 * nFrames, 1 + 16/(1+Aig_ManNodeNum(pNew)/1000) ); 
+        pSml = Fra_SmlSimulateSeq( pNew, 0, 128 * nFrames, 1 + 16/(1+Aig_ManNodeNum(pNew)/1000), 1  ); 
         if ( pParSec->fVerbose )
         {
             printf( "Seq simulation  :     Latches = %5d. Nodes = %6d. ", 
                 Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
-PRT( "Time", clock() - clk );
+ABC_PRT( "Time", clock() - clk );
         }
         if ( pSml->fNonConstOut )
         {
@@ -432,9 +432,9 @@ PRT( "Time", clock() - clk );
                 printf( "The counter-example is invalid because of phase abstraction.\n" );
             else
             {
-            FREE( p->pSeqModel );
+            ABC_FREE( p->pSeqModel );
             p->pSeqModel = Ssw_SmlDupCounterExample( pNew->pSeqModel, Aig_ManRegNum(p) );
-            FREE( pNew->pSeqModel );
+            ABC_FREE( pNew->pSeqModel );
             }
 
             Fra_SmlStop( pSml );
@@ -443,12 +443,12 @@ PRT( "Time", clock() - clk );
             if ( !pParSec->fSilent )
             {
                 printf( "Networks are NOT EQUIVALENT after simulation.   " );
-PRT( "Time", clock() - clkTotal );
+ABC_PRT( "Time", clock() - clkTotal );
             }
             if ( pParSec->fReportSolution && !pParSec->fRecursive )
             {
             printf( "SOLUTION: FAIL       " );
-PRT( "Time", clock() - clkTotal );
+ABC_PRT( "Time", clock() - clkTotal );
             }
             return RetValue;
         }
@@ -481,7 +481,7 @@ clk = clock();
             if ( pNewOrpos->pSeqModel )
             {
                 Ssw_Cex_t * pCex;
-                FREE( pNew->pSeqModel );
+                ABC_FREE( pNew->pSeqModel );
                 pCex = pNew->pSeqModel = pNewOrpos->pSeqModel; pNewOrpos->pSeqModel = NULL;
                 pCex->iPo = Ssw_SmlFindOutputCounterExample( pNew, pNew->pSeqModel );
             }
@@ -498,7 +498,7 @@ clk = clock();
             printf( "Property UNDECIDED after interpolation.  " );
         else
             assert( 0 ); 
-PRT( "Time", clock() - clk );
+ABC_PRT( "Time", clock() - clk );
         }
     }
 
@@ -518,12 +518,12 @@ finish:
         if ( !pParSec->fSilent )
         {
             printf( "Networks are equivalent.   " );
-PRT( "Time", clock() - clkTotal );
+ABC_PRT( "Time", clock() - clkTotal );
         }
         if ( pParSec->fReportSolution && !pParSec->fRecursive )
         {
         printf( "SOLUTION: PASS       " );
-PRT( "Time", clock() - clkTotal );
+ABC_PRT( "Time", clock() - clkTotal );
         }
     }
     else if ( RetValue == 0 )
@@ -531,12 +531,12 @@ PRT( "Time", clock() - clkTotal );
         if ( !pParSec->fSilent )
         {
             printf( "Networks are NOT EQUIVALENT.   " );
-PRT( "Time", clock() - clkTotal );
+ABC_PRT( "Time", clock() - clkTotal );
         }
         if ( pParSec->fReportSolution && !pParSec->fRecursive )
         {
         printf( "SOLUTION: FAIL       " );
-PRT( "Time", clock() - clkTotal );
+ABC_PRT( "Time", clock() - clkTotal );
         }
     }
     else 
@@ -544,12 +544,12 @@ PRT( "Time", clock() - clkTotal );
         if ( !pParSec->fSilent )
         {
             printf( "Networks are UNDECIDED.   " );
-PRT( "Time", clock() - clkTotal );
+ABC_PRT( "Time", clock() - clkTotal );
         }
         if ( pParSec->fReportSolution && !pParSec->fRecursive )
         {
         printf( "SOLUTION: UNDECIDED  " );
-PRT( "Time", clock() - clkTotal );
+ABC_PRT( "Time", clock() - clkTotal );
         }
         if ( !TimeOut && !pParSec->fSilent )
         {
@@ -566,9 +566,9 @@ PRT( "Time", clock() - clkTotal );
             printf( "The counter-example is invalid because of phase abstraction.\n" );
         else
         {
-        FREE( p->pSeqModel );
+        ABC_FREE( p->pSeqModel );
         p->pSeqModel = Ssw_SmlDupCounterExample( pNew->pSeqModel, Aig_ManRegNum(p) );
-        FREE( pNew->pSeqModel );
+        ABC_FREE( pNew->pSeqModel );
         }
     }
     if ( ppResult != NULL )
diff --git a/src/aig/fra/fraSim.c b/src/aig/fra/fraSim.c
index d1d73a03..aff21219 100644
--- a/src/aig/fra/fraSim.c
+++ b/src/aig/fra/fraSim.c
@@ -293,7 +293,7 @@ void Fra_SmlCheckOutputSavePattern( Fra_Man_t * p, Aig_Obj_t * pObjPo )
     // determine the best pattern
     BestPat = i * 32 + k;
     // fill in the counter-example data
-    pModel = ALLOC( int, Aig_ManPiNum(p->pManFraig)+1 );
+    pModel = ABC_ALLOC( int, Aig_ManPiNum(p->pManFraig)+1 );
     Aig_ManForEachPi( p->pManAig, pObjPi, i )
     {
         pModel[i] = Aig_InfoHasBit(Fra_ObjSim(p->pSml, pObjPi->Id), BestPat);
@@ -804,7 +804,7 @@ printf( "Refined classes  = %5d.   Changes = %4d.   Lits = %6d.\n", Vec_PtrSize(
 Fra_Sml_t * Fra_SmlStart( Aig_Man_t * pAig, int nPref, int nFrames, int nWordsFrame )
 {
     Fra_Sml_t * p;
-    p = (Fra_Sml_t *)malloc( sizeof(Fra_Sml_t) + sizeof(unsigned) * Aig_ManObjNumMax(pAig) * (nPref + nFrames) * nWordsFrame );
+    p = (Fra_Sml_t *)ABC_ALLOC( char, sizeof(Fra_Sml_t) + sizeof(unsigned) * Aig_ManObjNumMax(pAig) * (nPref + nFrames) * nWordsFrame );
     memset( p, 0, sizeof(Fra_Sml_t) + sizeof(unsigned) * (nPref + nFrames) * nWordsFrame );
     p->pAig        = pAig;
     p->nPref       = nPref;
@@ -828,7 +828,7 @@ Fra_Sml_t * Fra_SmlStart( Aig_Man_t * pAig, int nPref, int nFrames, int nWordsFr
 ***********************************************************************/
 void Fra_SmlStop( Fra_Sml_t * p )
 {
-    free( p );
+    ABC_FREE( p );
 }
 
 
@@ -863,12 +863,13 @@ Fra_Sml_t * Fra_SmlSimulateComb( Aig_Man_t * pAig, int nWords )
   SeeAlso     []
 
 ***********************************************************************/
-Fra_Sml_t * Fra_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int nFrames, int nWords )
+Fra_Sml_t * Fra_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int nFrames, int nWords, int fCheckMiter )
 {
     Fra_Sml_t * p;
     p = Fra_SmlStart( pAig, nPref, nFrames, nWords );
     Fra_SmlInitialize( p, 1 );
     Fra_SmlSimulateOne( p );
+    if ( fCheckMiter )
     p->fNonConstOut = Fra_SmlCheckNonConstOutputs( p );
     return p;
 }
@@ -888,7 +889,7 @@ Fra_Cex_t * Fra_SmlAllocCounterExample( int nRegs, int nRealPis, int nFrames )
 {
     Fra_Cex_t * pCex;
     int nWords = Aig_BitWordNum( nRegs + nRealPis * nFrames );
-    pCex = (Fra_Cex_t *)malloc( sizeof(Fra_Cex_t) + sizeof(unsigned) * nWords );
+    pCex = (Fra_Cex_t *)ABC_ALLOC( char, sizeof(Fra_Cex_t) + sizeof(unsigned) * nWords );
     memset( pCex, 0, sizeof(Fra_Cex_t) + sizeof(unsigned) * nWords );
     pCex->nRegs  = nRegs;
     pCex->nPis   = nRealPis;
@@ -909,7 +910,7 @@ Fra_Cex_t * Fra_SmlAllocCounterExample( int nRegs, int nRealPis, int nFrames )
 ***********************************************************************/
 void Fra_SmlFreeCounterExample( Fra_Cex_t * pCex )
 {
-    free( pCex );
+    ABC_FREE( pCex );
 }
 
 /**Function*************************************************************