Version abc90215

14 files changed, 78 insertions, 78 deletions

diff --git a/src/aig/ssw/ssw.h b/src/aig/ssw/ssw.h
index b3222fca..adb98401 100644
--- a/src/aig/ssw/ssw.h
+++ b/src/aig/ssw/ssw.h
@@ -21,10 +21,6 @@
 #ifndef __SSW_H__
 #define __SSW_H__
 
-#ifdef __cplusplus
-extern "C" { 
-#endif
-
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -33,6 +29,10 @@ extern "C" {
 ///                         PARAMETERS                               ///
 ////////////////////////////////////////////////////////////////////////
 
+#ifdef __cplusplus
+extern "C" { 
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                         BASIC TYPES                              ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/ssw/sswAig.c b/src/aig/ssw/sswAig.c
index 97f0a755..62e93d2d 100644
--- a/src/aig/ssw/sswAig.c
+++ b/src/aig/ssw/sswAig.c
@@ -42,7 +42,7 @@
 Ssw_Frm_t * Ssw_FrmStart( Aig_Man_t * pAig )
 {
     Ssw_Frm_t * p;
-    p = ALLOC( Ssw_Frm_t, 1 ); 
+    p = ABC_ALLOC( Ssw_Frm_t, 1 ); 
     memset( p, 0, sizeof(Ssw_Frm_t) );
     p->pAig          = pAig;
     p->nObjs         = Aig_ManObjNumMax( pAig );
@@ -69,7 +69,7 @@ void Ssw_FrmStop( Ssw_Frm_t * p )
     if ( p->pFrames )
         Aig_ManStop( p->pFrames );
     Vec_PtrFree( p->vAig2Frm );
-    free( p );
+    ABC_FREE( p );
 }
 
 /**Function*************************************************************
diff --git a/src/aig/ssw/sswBmc.c b/src/aig/ssw/sswBmc.c
index 93859c01..86d04424 100644
--- a/src/aig/ssw/sswBmc.c
+++ b/src/aig/ssw/sswBmc.c
@@ -161,7 +161,7 @@ int Ssw_BmcDynamic( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int fVerbo
                 printf( "Solving output %2d of frame %3d ... \r", 
                     i % Saig_ManPoNum(pAig), i / Saig_ManPoNum(pAig) );
             }
-            status = sat_solver_solve( pSat->pSat, &Lit, &Lit + 1, (sint64)nConfLimit, (sint64)0, (sint64)0, (sint64)0 );
+            status = sat_solver_solve( pSat->pSat, &Lit, &Lit + 1, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
             if ( status == l_False )
             {
 /*
@@ -199,7 +199,7 @@ int Ssw_BmcDynamic( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int fVerbo
             printf( "Conf =%8.0f. Var =%8d. AIG=%9d. ", 
                 (double)pSat->pSat->stats.conflicts, 
                 pSat->nSatVars, Aig_ManNodeNum(pFrm->pFrames) );
-            PRT( "T", clock() - clkPart );
+            ABC_PRT( "T", clock() - clkPart );
             clkPart = clock();
             fflush( stdout );
         }
diff --git a/src/aig/ssw/sswClass.c b/src/aig/ssw/sswClass.c
index 3528ae27..5d0be217 100644
--- a/src/aig/ssw/sswClass.c
+++ b/src/aig/ssw/sswClass.c
@@ -136,11 +136,11 @@ static inline Aig_Obj_t ** Ssw_ObjRemoveClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr
 Ssw_Cla_t * Ssw_ClassesStart( Aig_Man_t * pAig )
 {
     Ssw_Cla_t * p;
-    p = ALLOC( Ssw_Cla_t, 1 );
+    p = ABC_ALLOC( Ssw_Cla_t, 1 );
     memset( p, 0, sizeof(Ssw_Cla_t) );
     p->pAig         = pAig;
-    p->pId2Class    = CALLOC( Aig_Obj_t **, Aig_ManObjNumMax(pAig) );
-    p->pClassSizes  = CALLOC( int, Aig_ManObjNumMax(pAig) );
+    p->pId2Class    = ABC_CALLOC( Aig_Obj_t **, Aig_ManObjNumMax(pAig) );
+    p->pClassSizes  = ABC_CALLOC( int, Aig_ManObjNumMax(pAig) );
     p->vClassOld    = Vec_PtrAlloc( 100 );
     p->vClassNew    = Vec_PtrAlloc( 100 );
     p->vRefined     = Vec_PtrAlloc( 1000 );
@@ -187,10 +187,10 @@ void Ssw_ClassesStop( Ssw_Cla_t * p )
     if ( p->vClassNew )    Vec_PtrFree( p->vClassNew );
     if ( p->vClassOld )    Vec_PtrFree( p->vClassOld );
     Vec_PtrFree( p->vRefined );
-    FREE( p->pId2Class );
-    FREE( p->pClassSizes );
-    FREE( p->pMemClasses );
-    free( p );
+    ABC_FREE( p->pId2Class );
+    ABC_FREE( p->pClassSizes );
+    ABC_FREE( p->pMemClasses );
+    ABC_FREE( p );
 }
 
 /**Function*************************************************************
@@ -500,8 +500,8 @@ int Ssw_ClassesPrepareRehash( Ssw_Cla_t * p, Vec_Ptr_t * vCands )
 
     // allocate the hash table hashing simulation info into nodes
     nTableSize = Aig_PrimeCudd( Vec_PtrSize(vCands)/2 );
-    ppTable = CALLOC( Aig_Obj_t *, nTableSize ); 
-    ppNexts = CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) ); 
+    ppTable = ABC_CALLOC( Aig_Obj_t *, nTableSize ); 
+    ppNexts = ABC_CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) ); 
 
     // sort through the candidates
     nEntries = 0;
@@ -568,8 +568,8 @@ int Ssw_ClassesPrepareRehash( Ssw_Cla_t * p, Vec_Ptr_t * vCands )
     }
     p->pMemClassesFree += nEntries2;
     assert( nEntries == nEntries2 );
-    free( ppTable );
-    free( ppNexts );
+    ABC_FREE( ppTable );
+    ABC_FREE( ppNexts );
     // now it is time to refine the classes
     return Ssw_ClassesRefine( p, 1 );
 }
@@ -615,7 +615,7 @@ if ( fVerbose )
     printf( "Allocated %.2f Mb to store simulation information.\n", 
         1.0*(sizeof(unsigned) * Aig_ManObjNumMax(pAig) * nFrames * nWords)/(1<<20) );
     printf( "Initial simulation of %d frames with %d words.     ", nFrames, nWords );
-    PRT( "Time", clock() - clk );
+    ABC_PRT( "Time", clock() - clk );
 }
 
     // set comparison procedures
@@ -643,7 +643,7 @@ clk = clock();
     }
 
     // allocate room for classes
-    p->pMemClasses = ALLOC( Aig_Obj_t *, Vec_PtrSize(vCands) );
+    p->pMemClasses = ABC_ALLOC( Aig_Obj_t *, Vec_PtrSize(vCands) );
     p->pMemClassesFree = p->pMemClasses;
 
     // now it is time to refine the classes
@@ -651,7 +651,7 @@ clk = clock();
 if ( fVerbose )
 {
     printf( "Collecting candidate equivalence classes.        " );
-PRT( "Time", clock() - clk );
+ABC_PRT( "Time", clock() - clk );
 }
 
 clk = clock();
@@ -677,7 +677,7 @@ if ( fVerbose )
 {
     printf( "Simulation of %d frames with %d words (%2d rounds). ", 
         nFrames, nWords, i-1 );
-    PRT( "Time", clock() - clk );
+    ABC_PRT( "Time", clock() - clk );
 }
     Ssw_ClassesCheck( p );
 //    Ssw_ClassesPrint( p, 0 );
@@ -723,7 +723,7 @@ Ssw_Cla_t * Ssw_ClassesPrepareSimple( Aig_Man_t * pAig, int fLatchCorr, int nMax
         p->nCands1++;
     }
     // allocate room for classes
-    p->pMemClassesFree = p->pMemClasses = ALLOC( Aig_Obj_t *, p->nCands1 );
+    p->pMemClassesFree = p->pMemClasses = ABC_ALLOC( Aig_Obj_t *, p->nCands1 );
 //    Ssw_ClassesPrint( p, 0 );
     return p;
 }
@@ -754,7 +754,7 @@ Ssw_Cla_t * Ssw_ClassesPrepareTargets( Aig_Man_t * pAig )
         p->nCands1++;
     }
     // allocate room for classes
-    p->pMemClassesFree = p->pMemClasses = ALLOC( Aig_Obj_t *, p->nCands1 );
+    p->pMemClassesFree = p->pMemClasses = ABC_ALLOC( Aig_Obj_t *, p->nCands1 );
 //    Ssw_ClassesPrint( p, 0 );
     return p;
 }
@@ -783,7 +783,7 @@ Ssw_Cla_t * Ssw_ClassesPreparePairs( Aig_Man_t * pAig, Vec_Int_t ** pvClasses )
     for ( i = 0; i < Aig_ManObjNumMax(pAig); i++ )
         nTotalObjs += pvClasses[i] ? Vec_IntSize(pvClasses[i]) : 0; 
     // allocate memory for classes
-    p->pMemClasses = ALLOC( Aig_Obj_t *, nTotalObjs );
+    p->pMemClasses = ABC_ALLOC( Aig_Obj_t *, nTotalObjs );
     // create constant-1 class
     if ( pvClasses[0] )
     Vec_IntForEachEntry( pvClasses[0], Entry, i )
@@ -845,7 +845,7 @@ Ssw_Cla_t * Ssw_ClassesPreparePairsSimple( Aig_Man_t * pMiter, Vec_Int_t * vPair
     // start the classes
     p = Ssw_ClassesStart( pMiter );
     // allocate memory for classes
-    p->pMemClasses = ALLOC( Aig_Obj_t *, Vec_IntSize(vPairs) );
+    p->pMemClasses = ABC_ALLOC( Aig_Obj_t *, Vec_IntSize(vPairs) );
     // create classes
     for ( i = 0; i < Vec_IntSize(vPairs); i += 2 )
     {
diff --git a/src/aig/ssw/sswCnf.c b/src/aig/ssw/sswCnf.c
index c5ea9b28..73fa0b02 100644
--- a/src/aig/ssw/sswCnf.c
+++ b/src/aig/ssw/sswCnf.c
@@ -43,7 +43,7 @@ Ssw_Sat_t * Ssw_SatStart( int fPolarFlip )
 {
     Ssw_Sat_t * p;
     int Lit;
-    p = ALLOC( Ssw_Sat_t, 1 ); 
+    p = ABC_ALLOC( Ssw_Sat_t, 1 ); 
     memset( p, 0, sizeof(Ssw_Sat_t) );
     p->pAig          = NULL;
     p->fPolarFlip    = fPolarFlip;
@@ -84,7 +84,7 @@ void Ssw_SatStop( Ssw_Sat_t * p )
     Vec_IntFree( p->vSatVars );
     Vec_PtrFree( p->vFanins );
     Vec_PtrFree( p->vUsedPis );
-    free( p );
+    ABC_FREE( p );
 }
 
 /**Function*************************************************************
@@ -225,7 +225,7 @@ void Ssw_AddClausesSuper( Ssw_Sat_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 )
@@ -256,7 +256,7 @@ void Ssw_AddClausesSuper( Ssw_Sat_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vSuper )
     }
     RetValue = sat_solver_addclause( p->pSat, pLits, pLits + nLits );
     assert( RetValue );
-    free( pLits );
+    ABC_FREE( pLits );
 }
 
 /**Function*************************************************************
diff --git a/src/aig/ssw/sswCore.c b/src/aig/ssw/sswCore.c
index 38a36022..485a5146 100644
--- a/src/aig/ssw/sswCore.c
+++ b/src/aig/ssw/sswCore.c
@@ -157,7 +157,7 @@ clk = clock();
                     nIter, Ssw_ClassesCand1Num(p->ppClasses), Ssw_ClassesClassNum(p->ppClasses), 
                     p->nSatProof-nSatProof, p->nSatCallsSat-nSatCallsSat, 
                     p->nRecycles-nRecycles, p->nSatFailsReal-nSatFailsReal );
-                PRT( "T", clock() - clk );
+                ABC_PRT( "T", clock() - clk );
             } 
         }
         else
@@ -180,7 +180,7 @@ clk = clock();
                     printf( "R =%4d. ",   p->nRecycles-nRecycles );
                 }
                 printf( "F =%5d. ", p->nSatFailsReal-nSatFailsReal );
-                PRT( "T", clock() - clk );
+                ABC_PRT( "T", clock() - clk );
             } 
 //            if ( p->pPars->fDynamic && p->nSatCallsSat-nSatCallsSat < 100 )
 //                p->pPars->nBTLimit = 10000;
@@ -299,7 +299,7 @@ Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
         Ssw_ClassesSetData( p->ppClasses, NULL, NULL, Ssw_SmlObjIsConstBit, Ssw_SmlObjsAreEqualBit );
     }
     if ( p->pPars->fLocalSim )
-        p->pVisited = CALLOC( int, Ssw_SmlNumFrames( p->pSml ) * Aig_ManObjNumMax(p->pAig) );
+        p->pVisited = ABC_CALLOC( int, Ssw_SmlNumFrames( p->pSml ) * Aig_ManObjNumMax(p->pAig) );
     // perform refinement of classes
     pAigNew = Ssw_SignalCorrespondenceRefine( p );    
     if ( pPars->fUniqueness )
diff --git a/src/aig/ssw/sswInt.h b/src/aig/ssw/sswInt.h
index 930796fc..269bdad7 100644
--- a/src/aig/ssw/sswInt.h
+++ b/src/aig/ssw/sswInt.h
@@ -21,10 +21,6 @@
 #ifndef __SSW_INT_H__
 #define __SSW_INT_H__
 
-#ifdef __cplusplus
-extern "C" {
-#endif
-
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -37,6 +33,10 @@ extern "C" {
 ///                         PARAMETERS                               ///
 ////////////////////////////////////////////////////////////////////////
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                         BASIC TYPES                              ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/ssw/sswIslands.c b/src/aig/ssw/sswIslands.c
index 64515f3e..8913116c 100644
--- a/src/aig/ssw/sswIslands.c
+++ b/src/aig/ssw/sswIslands.c
@@ -491,7 +491,7 @@ int Ssw_SecWithSimilarityPairs( Aig_Man_t * p0, Aig_Man_t * p1, Vec_Int_t * vPai
     else
         printf( "Verification UNDECIDED. The number of remaining regs = %d (total = %d).  ", 
             Aig_ManRegNum(pAigRes), Aig_ManRegNum(p0)+Aig_ManRegNum(p1) );
-    PRT( "Time", clock() - clk );
+    ABC_PRT( "Time", clock() - clk );
     Aig_ManStop( pAigRes );
     return RetValue;
 }
diff --git a/src/aig/ssw/sswMan.c b/src/aig/ssw/sswMan.c
index 7e6e4473..90cc9028 100644
--- a/src/aig/ssw/sswMan.c
+++ b/src/aig/ssw/sswMan.c
@@ -47,17 +47,17 @@ Ssw_Man_t * Ssw_ManCreate( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
     Aig_ManFanoutStart( pAig );
     Aig_ManSetPioNumbers( pAig );
     // create interpolation manager
-    p = ALLOC( Ssw_Man_t, 1 ); 
+    p = ABC_ALLOC( Ssw_Man_t, 1 ); 
     memset( p, 0, sizeof(Ssw_Man_t) );
     p->pPars         = pPars;
     p->pAig          = pAig;
     p->nFrames       = pPars->nFramesK + 1;
-    p->pNodeToFrames = CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) * p->nFrames );
+    p->pNodeToFrames = ABC_CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) * p->nFrames );
     p->vCommon       = Vec_PtrAlloc( 100 );
     p->iOutputLit    = -1;
     // allocate storage for sim pattern
     p->nPatWords     = Aig_BitWordNum( Saig_ManPiNum(pAig) * p->nFrames + Saig_ManRegNum(pAig) );
-    p->pPatWords     = ALLOC( unsigned, p->nPatWords ); 
+    p->pPatWords     = ABC_ALLOC( unsigned, p->nPatWords ); 
     // other
     p->vNewLos       = Vec_PtrAlloc( 100 );
     p->vNewPos       = Vec_IntAlloc( 100 );
@@ -117,16 +117,16 @@ void Ssw_ManPrintStats( Ssw_Man_t * p )
         p->nRegsBeg, p->nRegsEnd, 100.0*(p->nRegsBeg-p->nRegsEnd)/(p->nRegsBeg?p->nRegsBeg:1) );
 
     p->timeOther = p->timeTotal-p->timeBmc-p->timeReduce-p->timeMarkCones-p->timeSimSat-p->timeSat;
-    PRTP( "BMC        ", p->timeBmc,       p->timeTotal );
-    PRTP( "Spec reduce", p->timeReduce,    p->timeTotal );
-    PRTP( "Mark cones ", p->timeMarkCones, p->timeTotal );
-    PRTP( "Sim SAT    ", p->timeSimSat,    p->timeTotal );
-    PRTP( "SAT solving", p->timeSat,       p->timeTotal );
-    PRTP( "  unsat    ", p->timeSatUnsat,  p->timeTotal );
-    PRTP( "  sat      ", p->timeSatSat,    p->timeTotal );
-    PRTP( "  undecided", p->timeSatUndec,  p->timeTotal );
-    PRTP( "Other      ", p->timeOther,     p->timeTotal );
-    PRTP( "TOTAL      ", p->timeTotal,     p->timeTotal );
+    ABC_PRTP( "BMC        ", p->timeBmc,       p->timeTotal );
+    ABC_PRTP( "Spec reduce", p->timeReduce,    p->timeTotal );
+    ABC_PRTP( "Mark cones ", p->timeMarkCones, p->timeTotal );
+    ABC_PRTP( "Sim SAT    ", p->timeSimSat,    p->timeTotal );
+    ABC_PRTP( "SAT solving", p->timeSat,       p->timeTotal );
+    ABC_PRTP( "  unsat    ", p->timeSatUnsat,  p->timeTotal );
+    ABC_PRTP( "  sat      ", p->timeSatSat,    p->timeTotal );
+    ABC_PRTP( "  undecided", p->timeSatUndec,  p->timeTotal );
+    ABC_PRTP( "Other      ", p->timeOther,     p->timeTotal );
+    ABC_PRTP( "TOTAL      ", p->timeTotal,     p->timeTotal );
 }
 
 /**Function*************************************************************
@@ -173,7 +173,7 @@ void Ssw_ManCleanup( Ssw_Man_t * p )
 ***********************************************************************/
 void Ssw_ManStop( Ssw_Man_t * p )
 {
-    FREE( p->pVisited );
+    ABC_FREE( p->pVisited );
     if ( p->pPars->fVerbose )
         Ssw_ManPrintStats( p );
     if ( p->ppClasses )
@@ -187,9 +187,9 @@ void Ssw_ManStop( Ssw_Man_t * p )
     Vec_PtrFree( p->vNewLos );
     Vec_IntFree( p->vNewPos );
     Vec_PtrFree( p->vCommon );
-    FREE( p->pNodeToFrames );
-    FREE( p->pPatWords );
-    free( p );
+    ABC_FREE( p->pNodeToFrames );
+    ABC_FREE( p->pPatWords );
+    ABC_FREE( p );
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/ssw/sswPairs.c b/src/aig/ssw/sswPairs.c
index 1af357f9..3c079922 100644
--- a/src/aig/ssw/sswPairs.c
+++ b/src/aig/ssw/sswPairs.c
@@ -149,8 +149,8 @@ Vec_Int_t ** Ssw_TransformPairsIntoTempClasses( Vec_Int_t * vPairs, int nObjNumM
     int * pReprs;             // mapping nodes into their representatives
     int Entry, idObj, idRepr, idReprObj, idReprRepr, i;
     // allocate data-structures
-    pvClasses = CALLOC( Vec_Int_t *, nObjNumMax );
-    pReprs    = ALLOC( int, nObjNumMax );
+    pvClasses = ABC_CALLOC( Vec_Int_t *, nObjNumMax );
+    pReprs    = ABC_ALLOC( int, nObjNumMax );
     for ( i = 0; i < nObjNumMax; i++ )
         pReprs[i] = -1;
     // consider pairs
@@ -231,7 +231,7 @@ Vec_Int_t ** Ssw_TransformPairsIntoTempClasses( Vec_Int_t * vPairs, int nObjNumM
             }
         }
     }
-    free( pReprs );
+    ABC_FREE( pReprs );
     return pvClasses;
 }
 
@@ -252,7 +252,7 @@ void Ssw_FreeTempClasses( Vec_Int_t ** pvClasses, int nObjNumMax )
     for ( i = 0; i < nObjNumMax; i++ )
         if ( pvClasses[i] ) 
             Vec_IntFree( pvClasses[i] );
-    free( pvClasses );
+    ABC_FREE( pvClasses );
 }
 
 /**Function*************************************************************
@@ -356,7 +356,7 @@ Aig_Man_t * Ssw_SignalCorrespondeceTestPairs( Aig_Man_t * pAig )
     else
         printf( "Verification UNDECIDED. Remaining registers %d (total %d).  ", 
             Aig_ManRegNum(pAigRes), Aig_ManRegNum(pAig) + Aig_ManRegNum(pAigNew) );
-    PRT( "Time", clock() - clk );
+    ABC_PRT( "Time", clock() - clk );
     // cleanup
     Aig_ManStop( pAigNew );
     return pAigRes;
@@ -390,7 +390,7 @@ int Ssw_SecWithPairs( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Vec_Int_t * vIds1, V
     else
         printf( "Verification UNDECIDED. The number of remaining regs = %d (total = %d).  ", 
             Aig_ManRegNum(pAigRes), Aig_ManRegNum(pAig1) + Aig_ManRegNum(pAig2) );
-    PRT( "Time", clock() - clk );
+    ABC_PRT( "Time", clock() - clk );
     // cleanup
     Aig_ManStop( pAigRes );
     return RetValue;
@@ -426,7 +426,7 @@ int Ssw_SecGeneral( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Ssw_Pars_t * pPars )
     else
         printf( "Verification UNDECIDED. The number of remaining regs = %d (total = %d).  ", 
             Aig_ManRegNum(pAigRes), Aig_ManRegNum(pAig1) + Aig_ManRegNum(pAig2) );
-    PRT( "Time", clock() - clk );
+    ABC_PRT( "Time", clock() - clk );
     // cleanup
     Aig_ManStop( pAigRes );
     return RetValue;
@@ -459,7 +459,7 @@ int Ssw_SecGeneralMiter( Aig_Man_t * pMiter, Ssw_Pars_t * pPars )
     else
         printf( "Verification UNDECIDED. The number of remaining regs = %d (total = %d).  ", 
             Aig_ManRegNum(pAigRes), Aig_ManRegNum(pMiter) );
-    PRT( "Time", clock() - clk );
+    ABC_PRT( "Time", clock() - clk );
     // cleanup
     Aig_ManStop( pAigRes );
     return RetValue;
diff --git a/src/aig/ssw/sswPart.c b/src/aig/ssw/sswPart.c
index 9d2ec34e..f481b457 100644
--- a/src/aig/ssw/sswPart.c
+++ b/src/aig/ssw/sswPart.c
@@ -106,7 +106,7 @@ Aig_Man_t * Ssw_SignalCorrespondencePart( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
             Aig_ManStop( pNew );
         }
         Aig_ManStop( pTemp );
-        free( pMapBack );
+        ABC_FREE( pMapBack );
     }
     // remap the AIG
     pNew = Aig_ManDupRepr( pAig, 0 );
@@ -118,7 +118,7 @@ Aig_Man_t * Ssw_SignalCorrespondencePart( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
     pPars->fVerbose = fVerbose;
     if ( fVerbose )
     {
-        PRT( "Total time", clock() - clk );
+        ABC_PRT( "Total time", clock() - clk );
     }
     return pNew;
 }
diff --git a/src/aig/ssw/sswSat.c b/src/aig/ssw/sswSat.c
index 2fd0fba3..21c5c1f1 100644
--- a/src/aig/ssw/sswSat.c
+++ b/src/aig/ssw/sswSat.c
@@ -81,7 +81,7 @@ int Ssw_NodesAreEquiv( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
 
 clk = clock();
     RetValue1 = sat_solver_solve( p->pMSat->pSat, pLits, pLits + nLits, 
-        (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
+        (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
 p->timeSat += clock() - clk;
     if ( RetValue1 == l_False )
     {
@@ -143,7 +143,7 @@ p->timeSatUndec += clock() - clk;
 
 clk = clock();
     RetValue1 = sat_solver_solve( p->pMSat->pSat, pLits, pLits + nLits, 
-        (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
+        (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
 p->timeSat += clock() - clk;
     if ( RetValue1 == l_False )
     {
diff --git a/src/aig/ssw/sswSemi.c b/src/aig/ssw/sswSemi.c
index 572ab076..5f426093 100644
--- a/src/aig/ssw/sswSemi.c
+++ b/src/aig/ssw/sswSemi.c
@@ -64,7 +64,7 @@ Ssw_Sem_t * Ssw_SemManStart( Ssw_Man_t * pMan, int nConfMax, int fVerbose )
     Aig_Obj_t * pObj;
     int i;
     // create interpolation manager
-    p = ALLOC( Ssw_Sem_t, 1 ); 
+    p = ABC_ALLOC( Ssw_Sem_t, 1 ); 
     memset( p, 0, sizeof(Ssw_Sem_t) );
     p->nConfMaxStart  = nConfMax;
     p->nConfMax       = nConfMax;
@@ -85,9 +85,9 @@ Ssw_Sem_t * Ssw_SemManStart( Ssw_Man_t * pMan, int nConfMax, int fVerbose )
     // update arrays of the manager
     assert( 0 );
 /*
-    free( p->pMan->pNodeToFrames );
+    ABC_FREE( p->pMan->pNodeToFrames );
     Vec_IntFree( p->pMan->vSatVars );
-    p->pMan->pNodeToFrames = CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pMan->pAig) * p->nFramesSweep );
+    p->pMan->pNodeToFrames = ABC_CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pMan->pAig) * p->nFramesSweep );
     p->pMan->vSatVars      = Vec_IntStart( Aig_ManObjNumMax(p->pMan->pAig) * (p->nFramesSweep+1) );
 */
     return p;
@@ -109,7 +109,7 @@ void Ssw_SemManStop( Ssw_Sem_t * p )
     Vec_PtrFree( p->vTargets );
     Vec_PtrFree( p->vPatterns );
     Vec_IntFree( p->vHistory );
-    free( p );
+    ABC_FREE( p );
 }
 
 /**Function*************************************************************
@@ -283,7 +283,7 @@ clk = clock();
                 Iter, Ssw_ClassesCand1Num(p->pMan->ppClasses), Ssw_ClassesClassNum(p->pMan->ppClasses), 
                 Aig_ManNodeNum(p->pMan->pFrames), Frames, (int)p->pMan->pMSat->pSat->stats.conflicts, p->nPatterns, 
                 p->pMan->nSatFailsReal? "f" : " " );
-            PRT( "T", clock() - clk );
+            ABC_PRT( "T", clock() - clk );
         } 
         Ssw_ManCleanup( p->pMan );
         if ( fCheckTargets && Ssw_SemCheckTargets( p ) )
diff --git a/src/aig/ssw/sswSim.c b/src/aig/ssw/sswSim.c
index a860199e..7a2f4664 100644
--- a/src/aig/ssw/sswSim.c
+++ b/src/aig/ssw/sswSim.c
@@ -437,7 +437,7 @@ int * Ssw_SmlCheckOutputSavePattern( Ssw_Sml_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->pAig)+1 );
+    pModel = ABC_ALLOC( int, Aig_ManPiNum(p->pAig)+1 );
     Aig_ManForEachPi( p->pAig, pObjPi, i )
     {
         pModel[i] = Aig_InfoHasBit(Ssw_ObjSim(p, pObjPi->Id), BestPat);
@@ -1074,7 +1074,7 @@ p->nSimRounds++;
 Ssw_Sml_t * Ssw_SmlStart( Aig_Man_t * pAig, int nPref, int nFrames, int nWordsFrame )
 {
     Ssw_Sml_t * p;
-    p = (Ssw_Sml_t *)malloc( sizeof(Ssw_Sml_t) + sizeof(unsigned) * Aig_ManObjNumMax(pAig) * (nPref + nFrames) * nWordsFrame );
+    p = (Ssw_Sml_t *)ABC_ALLOC( char, sizeof(Ssw_Sml_t) + sizeof(unsigned) * Aig_ManObjNumMax(pAig) * (nPref + nFrames) * nWordsFrame );
     memset( p, 0, sizeof(Ssw_Sml_t) + sizeof(unsigned) * (nPref + nFrames) * nWordsFrame );
     p->pAig        = pAig;
     p->nPref       = nPref;
@@ -1114,7 +1114,7 @@ void Ssw_SmlClean( Ssw_Sml_t * p )
 ***********************************************************************/
 void Ssw_SmlStop( Ssw_Sml_t * p )
 {
-    free( p );
+    ABC_FREE( p );
 }
 
 
@@ -1244,7 +1244,7 @@ Ssw_Cex_t * Ssw_SmlAllocCounterExample( int nRegs, int nRealPis, int nFrames )
 {
     Ssw_Cex_t * pCex;
     int nWords = Aig_BitWordNum( nRegs + nRealPis * nFrames );
-    pCex = (Ssw_Cex_t *)malloc( sizeof(Ssw_Cex_t) + sizeof(unsigned) * nWords );
+    pCex = (Ssw_Cex_t *)ABC_ALLOC( char, sizeof(Ssw_Cex_t) + sizeof(unsigned) * nWords );
     memset( pCex, 0, sizeof(Ssw_Cex_t) + sizeof(unsigned) * nWords );
     pCex->nRegs  = nRegs;
     pCex->nPis   = nRealPis;
@@ -1265,7 +1265,7 @@ Ssw_Cex_t * Ssw_SmlAllocCounterExample( int nRegs, int nRealPis, int nFrames )
 ***********************************************************************/
 void Ssw_SmlFreeCounterExample( Ssw_Cex_t * pCex )
 {
-    free( pCex );
+    ABC_FREE( pCex );
 }
 
 /**Function*************************************************************