Version abc90215

13 files changed, 223 insertions, 237 deletions

diff --git a/src/sat/bsat/satInter.c b/src/sat/bsat/satInter.c
index fe2ed113..849ceb71 100644
--- a/src/sat/bsat/satInter.c
+++ b/src/sat/bsat/satInter.c
@@ -55,7 +55,7 @@ struct Int_Man_t_
     Sto_Cls_t **    pWatches;     // watched clauses for each literal (size 2*nVars)          
     // interpolation data
     int             nVarsAB;      // the number of global variables
-    char *          pVarTypes;    // variable type (size nVars) [1=A, 0=B, <0=AB]
+    int *           pVarTypes;    // variable type (size nVars) [1=A, 0=B, <0=AB]
     unsigned *      pInters;      // storage for interpolants as truth tables (size nClauses)
     int             nIntersAlloc; // the allocated size of truth table array
     int             nWords;       // the number of words in the truth table
@@ -105,11 +105,11 @@ Int_Man_t * Int_ManAlloc()
 {
     Int_Man_t * p;
     // allocate the manager
-    p = (Int_Man_t *)malloc( sizeof(Int_Man_t) );
+    p = (Int_Man_t *)ABC_ALLOC( char, sizeof(Int_Man_t) );
     memset( p, 0, sizeof(Int_Man_t) );
     // verification
     p->nResLitsAlloc = (1<<16);
-    p->pResLits = malloc( sizeof(lit) * p->nResLitsAlloc );
+    p->pResLits = ABC_ALLOC( lit, p->nResLitsAlloc );
     // parameters
     p->fProofWrite = 0;
     p->fProofVerif = 1;
@@ -214,18 +214,18 @@ void Int_ManResize( Int_Man_t * p )
         while ( p->nVarsAlloc < p->pCnf->nVars ) 
             p->nVarsAlloc *= 2;
         // resize the arrays
-        p->pTrail    = (lit *)       realloc( p->pTrail,    sizeof(lit) * p->nVarsAlloc );
-        p->pAssigns  = (lit *)       realloc( p->pAssigns,  sizeof(lit) * p->nVarsAlloc );
-        p->pSeens    = (char *)      realloc( p->pSeens,    sizeof(char) * p->nVarsAlloc );
-        p->pVarTypes = (char *)      realloc( p->pVarTypes, sizeof(char) * p->nVarsAlloc );
-        p->pReasons  = (Sto_Cls_t **)realloc( p->pReasons,  sizeof(Sto_Cls_t *) * p->nVarsAlloc );
-        p->pWatches  = (Sto_Cls_t **)realloc( p->pWatches,  sizeof(Sto_Cls_t *) * p->nVarsAlloc*2 );
+        p->pTrail    = ABC_REALLOC(lit,         p->pTrail,    p->nVarsAlloc );
+        p->pAssigns  = ABC_REALLOC(lit,         p->pAssigns,  p->nVarsAlloc );
+        p->pSeens    = ABC_REALLOC(char,        p->pSeens,    p->nVarsAlloc );
+        p->pVarTypes = ABC_REALLOC(int,         p->pVarTypes, p->nVarsAlloc );
+        p->pReasons  = ABC_REALLOC(Sto_Cls_t *, p->pReasons,  p->nVarsAlloc );
+        p->pWatches  = ABC_REALLOC(Sto_Cls_t *, p->pWatches,  p->nVarsAlloc*2 );
     }
 
-    // clean the free space
+    // clean the ABC_FREE space
     memset( p->pAssigns , 0xff, sizeof(lit) * p->pCnf->nVars );
     memset( p->pSeens   , 0,    sizeof(char) * p->pCnf->nVars );
-    memset( p->pVarTypes, 0,    sizeof(char) * p->pCnf->nVars );
+    memset( p->pVarTypes, 0,    sizeof(int) * p->pCnf->nVars );
     memset( p->pReasons , 0,    sizeof(Sto_Cls_t *) * p->pCnf->nVars );
     memset( p->pWatches , 0,    sizeof(Sto_Cls_t *) * p->pCnf->nVars*2 );
 
@@ -243,7 +243,7 @@ void Int_ManResize( Int_Man_t * p )
         while ( p->nClosAlloc < p->pCnf->nClauses ) 
             p->nClosAlloc *= 2;
         // resize the arrays
-        p->pProofNums = (int *) realloc( p->pProofNums,  sizeof(int) * p->nClosAlloc );
+        p->pProofNums = ABC_REALLOC(int, p->pProofNums,  p->nClosAlloc );
     }
     memset( p->pProofNums, 0, sizeof(int) * p->pCnf->nClauses );
 
@@ -251,7 +251,7 @@ void Int_ManResize( Int_Man_t * p )
     if ( p->nIntersAlloc < p->nWords * p->pCnf->nClauses )
     {
         p->nIntersAlloc = p->nWords * p->pCnf->nClauses;
-        p->pInters = (unsigned *) realloc( p->pInters, sizeof(unsigned) * p->nIntersAlloc );
+        p->pInters = ABC_REALLOC(unsigned, p->pInters, p->nIntersAlloc );
     }
 //    memset( p->pInters, 0, sizeof(unsigned) * p->nWords * p->pCnf->nClauses );
 }
@@ -271,20 +271,20 @@ void Int_ManFree( Int_Man_t * p )
 {
 /*
     printf( "Runtime stats:\n" );
-PRT( "BCP     ", p->timeBcp   );
-PRT( "Trace   ", p->timeTrace );
-PRT( "TOTAL   ", p->timeTotal );
+ABC_PRT( "BCP     ", p->timeBcp   );
+ABC_PRT( "Trace   ", p->timeTrace );
+ABC_PRT( "TOTAL   ", p->timeTotal );
 */
-    free( p->pInters );
-    free( p->pProofNums );
-    free( p->pTrail );
-    free( p->pAssigns );
-    free( p->pSeens );
-    free( p->pVarTypes );
-    free( p->pReasons );
-    free( p->pWatches );
-    free( p->pResLits );
-    free( p );
+    ABC_FREE( p->pInters );
+    ABC_FREE( p->pProofNums );
+    ABC_FREE( p->pTrail );
+    ABC_FREE( p->pAssigns );
+    ABC_FREE( p->pSeens );
+    ABC_FREE( p->pVarTypes );
+    ABC_FREE( p->pReasons );
+    ABC_FREE( p->pWatches );
+    ABC_FREE( p->pResLits );
+    ABC_FREE( p );
 }
 
 
diff --git a/src/sat/bsat/satInterA.c b/src/sat/bsat/satInterA.c
index 5edc5b67..5dcc7f0b 100644
--- a/src/sat/bsat/satInterA.c
+++ b/src/sat/bsat/satInterA.c
@@ -106,11 +106,11 @@ Inta_Man_t * Inta_ManAlloc()
 {
     Inta_Man_t * p;
     // allocate the manager
-    p = (Inta_Man_t *)malloc( sizeof(Inta_Man_t) );
+    p = (Inta_Man_t *)ABC_ALLOC( char, sizeof(Inta_Man_t) );
     memset( p, 0, sizeof(Inta_Man_t) );
     // verification
     p->nResLitsAlloc = (1<<16);
-    p->pResLits = malloc( sizeof(lit) * p->nResLitsAlloc );
+    p->pResLits = ABC_ALLOC( lit, p->nResLitsAlloc );
     // parameters
     p->fProofWrite = 0;
     p->fProofVerif = 1;
@@ -195,15 +195,15 @@ void Inta_ManResize( Inta_Man_t * p )
         while ( p->nVarsAlloc < p->pCnf->nVars ) 
             p->nVarsAlloc *= 2;
         // resize the arrays
-        p->pTrail    = (lit *)       realloc( p->pTrail,    sizeof(lit) * p->nVarsAlloc );
-        p->pAssigns  = (lit *)       realloc( p->pAssigns,  sizeof(lit) * p->nVarsAlloc );
-        p->pSeens    = (char *)      realloc( p->pSeens,    sizeof(char) * p->nVarsAlloc );
-        p->pVarTypes = (int *)       realloc( p->pVarTypes, sizeof(int) * p->nVarsAlloc );
-        p->pReasons  = (Sto_Cls_t **)realloc( p->pReasons,  sizeof(Sto_Cls_t *) * p->nVarsAlloc );
-        p->pWatches  = (Sto_Cls_t **)realloc( p->pWatches,  sizeof(Sto_Cls_t *) * p->nVarsAlloc*2 );
+        p->pTrail    = ABC_REALLOC(lit,         p->pTrail,    p->nVarsAlloc );
+        p->pAssigns  = ABC_REALLOC(lit,         p->pAssigns,  p->nVarsAlloc );
+        p->pSeens    = ABC_REALLOC(char,        p->pSeens,    p->nVarsAlloc );
+        p->pVarTypes = ABC_REALLOC(int,         p->pVarTypes, p->nVarsAlloc );
+        p->pReasons  = ABC_REALLOC(Sto_Cls_t *, p->pReasons,  p->nVarsAlloc );
+        p->pWatches  = ABC_REALLOC(Sto_Cls_t *, p->pWatches,  p->nVarsAlloc*2 );
     }
 
-    // clean the free space
+    // clean the ABC_FREE space
     memset( p->pAssigns , 0xff, sizeof(lit) * p->pCnf->nVars );
     memset( p->pSeens   , 0,    sizeof(char) * p->pCnf->nVars );
     memset( p->pVarTypes, 0,    sizeof(int) * p->pCnf->nVars );
@@ -222,7 +222,7 @@ void Inta_ManResize( Inta_Man_t * p )
         while ( p->nClosAlloc < p->pCnf->nClauses ) 
             p->nClosAlloc *= 2;
         // resize the arrays
-        p->pProofNums = (int *) realloc( p->pProofNums,  sizeof(int) * p->nClosAlloc );
+        p->pProofNums = ABC_REALLOC( int, p->pProofNums,  p->nClosAlloc );
     }
     memset( p->pProofNums, 0, sizeof(int) * p->pCnf->nClauses );
 
@@ -230,7 +230,7 @@ void Inta_ManResize( Inta_Man_t * p )
     if ( p->nIntersAlloc < p->pCnf->nClauses )
     {
         p->nIntersAlloc = p->pCnf->nClauses;
-        p->pInters = (Aig_Obj_t **) realloc( p->pInters, sizeof(Aig_Obj_t *) * p->nIntersAlloc );
+        p->pInters = ABC_REALLOC( Aig_Obj_t *, p->pInters, p->nIntersAlloc );
     }
     memset( p->pInters, 0, sizeof(Aig_Obj_t *) * p->pCnf->nClauses );
 }
@@ -250,20 +250,20 @@ void Inta_ManFree( Inta_Man_t * p )
 {
 /*
     printf( "Runtime stats:\n" );
-PRT( "BCP     ", p->timeBcp   );
-PRT( "Trace   ", p->timeTrace );
-PRT( "TOTAL   ", p->timeTotal );
+ABC_PRT( "BCP     ", p->timeBcp   );
+ABC_PRT( "Trace   ", p->timeTrace );
+ABC_PRT( "TOTAL   ", p->timeTotal );
 */
-    free( p->pInters );
-    free( p->pProofNums );
-    free( p->pTrail );
-    free( p->pAssigns );
-    free( p->pSeens );
-    free( p->pVarTypes );
-    free( p->pReasons );
-    free( p->pWatches );
-    free( p->pResLits );
-    free( p );
+    ABC_FREE( p->pInters );
+    ABC_FREE( p->pProofNums );
+    ABC_FREE( p->pTrail );
+    ABC_FREE( p->pAssigns );
+    ABC_FREE( p->pSeens );
+    ABC_FREE( p->pVarTypes );
+    ABC_FREE( p->pReasons );
+    ABC_FREE( p->pWatches );
+    ABC_FREE( p->pResLits );
+    ABC_FREE( p );
 }
 
 
@@ -1004,7 +1004,7 @@ void * Inta_ManInterpolate( Inta_Man_t * p, Sto_Man_t * pCnf, void * vVarsAB, in
 
     if ( fVerbose )
     {
-//        PRT( "Interpo", clock() - clkTotal );
+//        ABC_PRT( "Interpo", clock() - clkTotal );
     printf( "Vars = %d. Roots = %d. Learned = %d. Resol steps = %d.  Ave = %.2f.  Mem = %.2f Mb\n", 
         p->pCnf->nVars, p->pCnf->nRoots, p->pCnf->nClauses-p->pCnf->nRoots, p->Counter,  
         1.0*(p->Counter-p->pCnf->nRoots)/(p->pCnf->nClauses-p->pCnf->nRoots), 
diff --git a/src/sat/bsat/satInterB.c b/src/sat/bsat/satInterB.c
index e0f4328d..cb7f7828 100644
--- a/src/sat/bsat/satInterB.c
+++ b/src/sat/bsat/satInterB.c
@@ -108,11 +108,11 @@ Intb_Man_t * Intb_ManAlloc()
 {
     Intb_Man_t * p;
     // allocate the manager
-    p = (Intb_Man_t *)malloc( sizeof(Intb_Man_t) );
+    p = (Intb_Man_t *)ABC_ALLOC( char, sizeof(Intb_Man_t) );
     memset( p, 0, sizeof(Intb_Man_t) );
     // verification
     p->nResLitsAlloc = (1<<16);
-    p->pResLits = malloc( sizeof(lit) * p->nResLitsAlloc );
+    p->pResLits = ABC_ALLOC( lit, p->nResLitsAlloc );
     // parameters
     p->fProofWrite = 0;
     p->fProofVerif = 1;
@@ -197,15 +197,15 @@ void Intb_ManResize( Intb_Man_t * p )
         while ( p->nVarsAlloc < p->pCnf->nVars ) 
             p->nVarsAlloc *= 2;
         // resize the arrays
-        p->pTrail    = (lit *)       realloc( p->pTrail,    sizeof(lit) * p->nVarsAlloc );
-        p->pAssigns  = (lit *)       realloc( p->pAssigns,  sizeof(lit) * p->nVarsAlloc );
-        p->pSeens    = (char *)      realloc( p->pSeens,    sizeof(char) * p->nVarsAlloc );
-        p->pVarTypes = (int *)       realloc( p->pVarTypes, sizeof(int) * p->nVarsAlloc );
-        p->pReasons  = (Sto_Cls_t **)realloc( p->pReasons,  sizeof(Sto_Cls_t *) * p->nVarsAlloc );
-        p->pWatches  = (Sto_Cls_t **)realloc( p->pWatches,  sizeof(Sto_Cls_t *) * p->nVarsAlloc*2 );
+        p->pTrail    = ABC_REALLOC(lit,         p->pTrail,    p->nVarsAlloc );
+        p->pAssigns  = ABC_REALLOC(lit,         p->pAssigns,  p->nVarsAlloc );
+        p->pSeens    = ABC_REALLOC(char,        p->pSeens,    p->nVarsAlloc );
+        p->pVarTypes = ABC_REALLOC(int,         p->pVarTypes, p->nVarsAlloc );
+        p->pReasons  = ABC_REALLOC(Sto_Cls_t *, p->pReasons,  p->nVarsAlloc );
+        p->pWatches  = ABC_REALLOC(Sto_Cls_t *, p->pWatches,  p->nVarsAlloc*2 );
     }
 
-    // clean the free space
+    // clean the ABC_FREE space
     memset( p->pAssigns , 0xff, sizeof(lit) * p->pCnf->nVars );
     memset( p->pSeens   , 0,    sizeof(char) * p->pCnf->nVars );
     memset( p->pVarTypes, 0,    sizeof(int) * p->pCnf->nVars );
@@ -224,7 +224,7 @@ void Intb_ManResize( Intb_Man_t * p )
         while ( p->nClosAlloc < p->pCnf->nClauses ) 
             p->nClosAlloc *= 2;
         // resize the arrays
-        p->pProofNums = (int *) realloc( p->pProofNums,  sizeof(int) * p->nClosAlloc );
+        p->pProofNums = ABC_REALLOC( int, p->pProofNums,  p->nClosAlloc );
     }
     memset( p->pProofNums, 0, sizeof(int) * p->pCnf->nClauses );
 
@@ -232,7 +232,7 @@ void Intb_ManResize( Intb_Man_t * p )
     if ( p->nIntersAlloc < p->pCnf->nClauses )
     {
         p->nIntersAlloc = p->pCnf->nClauses;
-        p->pInters = (Aig_Obj_t **) realloc( p->pInters, sizeof(Aig_Obj_t *) * p->nIntersAlloc );
+        p->pInters = ABC_REALLOC(Aig_Obj_t *, p->pInters, p->nIntersAlloc );
     }
     memset( p->pInters, 0, sizeof(Aig_Obj_t *) * p->pCnf->nClauses );
 }
@@ -252,20 +252,20 @@ void Intb_ManFree( Intb_Man_t * p )
 {
 /*
     printf( "Runtime stats:\n" );
-PRT( "BCP     ", p->timeBcp   );
-PRT( "Trace   ", p->timeTrace );
-PRT( "TOTAL   ", p->timeTotal );
+ABC_PRT( "BCP     ", p->timeBcp   );
+ABC_PRT( "Trace   ", p->timeTrace );
+ABC_PRT( "TOTAL   ", p->timeTotal );
 */
-    free( p->pInters );
-    free( p->pProofNums );
-    free( p->pTrail );
-    free( p->pAssigns );
-    free( p->pSeens );
-    free( p->pVarTypes );
-    free( p->pReasons );
-    free( p->pWatches );
-    free( p->pResLits );
-    free( p );
+    ABC_FREE( p->pInters );
+    ABC_FREE( p->pProofNums );
+    ABC_FREE( p->pTrail );
+    ABC_FREE( p->pAssigns );
+    ABC_FREE( p->pSeens );
+    ABC_FREE( p->pVarTypes );
+    ABC_FREE( p->pReasons );
+    ABC_FREE( p->pWatches );
+    ABC_FREE( p->pResLits );
+    ABC_FREE( p );
 }
 
 
@@ -987,7 +987,7 @@ void * Intb_ManInterpolate( Intb_Man_t * p, Sto_Man_t * pCnf, void * vVarsAB, in
 
     if ( fVerbose )
     {
-//        PRT( "Interpo", clock() - clkTotal );
+//        ABC_PRT( "Interpo", clock() - clkTotal );
     printf( "Vars = %d. Roots = %d. Learned = %d. Resol steps = %d.  Ave = %.2f.  Mem = %.2f Mb\n", 
         p->pCnf->nVars, p->pCnf->nRoots, p->pCnf->nClauses-p->pCnf->nRoots, p->Counter,  
         1.0*(p->Counter-p->pCnf->nRoots)/(p->pCnf->nClauses-p->pCnf->nRoots), 
diff --git a/src/sat/bsat/satInterP.c b/src/sat/bsat/satInterP.c
index c944c36d..57fb79d2 100644
--- a/src/sat/bsat/satInterP.c
+++ b/src/sat/bsat/satInterP.c
@@ -23,6 +23,7 @@
 #include <string.h>
 #include <assert.h>
 #include <time.h>
+
 #include "satStore.h"
 #include "vec.h"
 
@@ -92,11 +93,11 @@ Intp_Man_t * Intp_ManAlloc()
 {
     Intp_Man_t * p;
     // allocate the manager
-    p = (Intp_Man_t *)malloc( sizeof(Intp_Man_t) );
+    p = (Intp_Man_t *)ABC_ALLOC( char, sizeof(Intp_Man_t) );
     memset( p, 0, sizeof(Intp_Man_t) );
     // verification
     p->nResLitsAlloc = (1<<16);
-    p->pResLits = malloc( sizeof(lit) * p->nResLitsAlloc );
+    p->pResLits = ABC_ALLOC( lit, p->nResLitsAlloc );
     // proof recording
     p->vAnties = Vec_IntAlloc( 1000 );
     p->vBreaks = Vec_IntAlloc( 1000 );
@@ -128,15 +129,15 @@ void Intp_ManResize( Intp_Man_t * p )
         while ( p->nVarsAlloc < p->pCnf->nVars ) 
             p->nVarsAlloc *= 2;
         // resize the arrays
-        p->pTrail    = (lit *)       realloc( p->pTrail,    sizeof(lit) * p->nVarsAlloc );
-        p->pAssigns  = (lit *)       realloc( p->pAssigns,  sizeof(lit) * p->nVarsAlloc );
-        p->pSeens    = (char *)      realloc( p->pSeens,    sizeof(char) * p->nVarsAlloc );
-//        p->pVarTypes = (int *)       realloc( p->pVarTypes, sizeof(int) * p->nVarsAlloc );
-        p->pReasons  = (Sto_Cls_t **)realloc( p->pReasons,  sizeof(Sto_Cls_t *) * p->nVarsAlloc );
-        p->pWatches  = (Sto_Cls_t **)realloc( p->pWatches,  sizeof(Sto_Cls_t *) * p->nVarsAlloc*2 );
+        p->pTrail    = ABC_REALLOC(lit,         p->pTrail,    p->nVarsAlloc );
+        p->pAssigns  = ABC_REALLOC(lit,         p->pAssigns,  p->nVarsAlloc );
+        p->pSeens    = ABC_REALLOC(char,        p->pSeens,    p->nVarsAlloc );
+//        p->pVarTypes = ABC_REALLOC(int,         p->pVarTypes, p->nVarsAlloc );
+        p->pReasons  = ABC_REALLOC(Sto_Cls_t *, p->pReasons,  p->nVarsAlloc );
+        p->pWatches  = ABC_REALLOC(Sto_Cls_t *, p->pWatches,  p->nVarsAlloc*2 );
     }
 
-    // clean the free space
+    // clean the ABC_FREE space
     memset( p->pAssigns , 0xff, sizeof(lit) * p->pCnf->nVars );
     memset( p->pSeens   , 0,    sizeof(char) * p->pCnf->nVars );
 //    memset( p->pVarTypes, 0,    sizeof(int) * p->pCnf->nVars );
@@ -152,7 +153,7 @@ void Intp_ManResize( Intp_Man_t * p )
         while ( p->nClosAlloc < p->pCnf->nClauses ) 
             p->nClosAlloc *= 2;
         // resize the arrays
-        p->pProofNums = (int *) realloc( p->pProofNums,  sizeof(int) * p->nClosAlloc );
+        p->pProofNums = ABC_REALLOC( int, p->pProofNums,  p->nClosAlloc );
     }
     memset( p->pProofNums, 0, sizeof(int) * p->pCnf->nClauses );
 }
@@ -172,22 +173,22 @@ void Intp_ManFree( Intp_Man_t * p )
 {
 /*
     printf( "Runtime stats:\n" );
-PRT( "BCP     ", p->timeBcp   );
-PRT( "Trace   ", p->timeTrace );
-PRT( "TOTAL   ", p->timeTotal );
+ABC_PRT( "BCP     ", p->timeBcp   );
+ABC_PRT( "Trace   ", p->timeTrace );
+ABC_PRT( "TOTAL   ", p->timeTotal );
 */
     Vec_IntFree( p->vAnties );
     Vec_IntFree( p->vBreaks );
-//    free( p->pInters );
-    free( p->pProofNums );
-    free( p->pTrail );
-    free( p->pAssigns );
-    free( p->pSeens );
-//    free( p->pVarTypes );
-    free( p->pReasons );
-    free( p->pWatches );
-    free( p->pResLits );
-    free( p );
+//    ABC_FREE( p->pInters );
+    ABC_FREE( p->pProofNums );
+    ABC_FREE( p->pTrail );
+    ABC_FREE( p->pAssigns );
+    ABC_FREE( p->pSeens );
+//    ABC_FREE( p->pVarTypes );
+    ABC_FREE( p->pReasons );
+    ABC_FREE( p->pWatches );
+    ABC_FREE( p->pResLits );
+    ABC_FREE( p );
 }
 
 
@@ -864,7 +865,7 @@ void Intp_ManUnsatCoreVerify( Sto_Man_t * pCnf, Vec_Int_t * vCore )
     }
     Vec_PtrFree( vClauses );
     // solve the problem
-    RetValue = sat_solver_solve( pSat, NULL, NULL, (sint64)nConfMax, (sint64)0, (sint64)0, (sint64)0 );
+    RetValue = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)nConfMax, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
     sat_solver_delete( pSat );
     if ( fVerbose )
     {
@@ -874,7 +875,7 @@ void Intp_ManUnsatCoreVerify( Sto_Man_t * pCnf, Vec_Int_t * vCore )
             printf( "UNSAT core verification FAILED.  " );
         else
             printf( "UNSAT core verification succeeded.  " );
-        PRT( "Time", clock() - clk );
+        ABC_PRT( "Time", clock() - clk );
     }
     else
     {
@@ -989,7 +990,7 @@ void * Intp_ManUnsatCore( Intp_Man_t * p, Sto_Man_t * pCnf, int fVerbose )
 
     if ( fVerbose )
     {
-        PRT( "Core", clock() - clkTotal );
+        ABC_PRT( "Core", clock() - clkTotal );
     printf( "Vars = %d. Roots = %d. Learned = %d. Resol steps = %d.  Ave = %.2f.  Mem = %.2f Mb\n", 
         p->pCnf->nVars, p->pCnf->nRoots, p->pCnf->nClauses-p->pCnf->nRoots, p->Counter,  
         1.0*(p->Counter-p->pCnf->nRoots)/(p->pCnf->nClauses-p->pCnf->nRoots), 
diff --git a/src/sat/bsat/satMem.c b/src/sat/bsat/satMem.c
index 1dacb854..f789f927 100644
--- a/src/sat/bsat/satMem.c
+++ b/src/sat/bsat/satMem.c
@@ -16,8 +16,13 @@
 
 ***********************************************************************/
 
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+#include <assert.h>
+
+#include "abc_global.h"
 #include "satMem.h"
-#include "vec.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -30,7 +35,7 @@ struct Sat_MmFixed_t_
     int           nEntriesAlloc; // the total number of entries allocated
     int           nEntriesUsed;  // the number of entries in use
     int           nEntriesMax;   // the max number of entries in use
-    char *        pEntriesFree;  // the linked list of free entries
+    char *        pEntriesFree;  // the linked list of ABC_FREE entries
 
     // this is where the memory is stored
     int           nChunkSize;    // the size of one chunk
@@ -47,8 +52,8 @@ struct Sat_MmFlex_t_
 {
     // information about individual entries
     int           nEntriesUsed;  // the number of entries allocated
-    char *        pCurrent;      // the current pointer to free memory
-    char *        pEnd;          // the first entry outside the free memory
+    char *        pCurrent;      // the current pointer to ABC_FREE memory
+    char *        pEnd;          // the first entry outside the ABC_FREE memory
 
     // this is where the memory is stored
     int           nChunkSize;    // the size of one chunk
@@ -93,7 +98,7 @@ Sat_MmFixed_t * Sat_MmFixedStart( int nEntrySize )
 {
     Sat_MmFixed_t * p;
 
-    p = ALLOC( Sat_MmFixed_t, 1 );
+    p = ABC_ALLOC( Sat_MmFixed_t, 1 );
     memset( p, 0, sizeof(Sat_MmFixed_t) );
 
     p->nEntrySize    = nEntrySize;
@@ -110,7 +115,7 @@ Sat_MmFixed_t * Sat_MmFixedStart( int nEntrySize )
 
     p->nChunksAlloc  = 64;
     p->nChunks       = 0;
-    p->pChunks       = ALLOC( char *, p->nChunksAlloc );
+    p->pChunks       = ABC_ALLOC( char *, p->nChunksAlloc );
 
     p->nMemoryUsed   = 0;
     p->nMemoryAlloc  = 0;
@@ -141,9 +146,9 @@ void Sat_MmFixedStop( Sat_MmFixed_t * p, int fVerbose )
             p->nEntriesUsed, p->nEntriesMax, p->nEntrySize * p->nEntriesUsed, p->nMemoryAlloc );
     }
     for ( i = 0; i < p->nChunks; i++ )
-        free( p->pChunks[i] );
-    free( p->pChunks );
-    free( p );
+        ABC_FREE( p->pChunks[i] );
+    ABC_FREE( p->pChunks );
+    ABC_FREE( p );
 }
 
 /**Function*************************************************************
@@ -162,16 +167,16 @@ char * Sat_MmFixedEntryFetch( Sat_MmFixed_t * p )
     char * pTemp;
     int i;
 
-    // check if there are still free entries
+    // check if there are still ABC_FREE entries
     if ( p->nEntriesUsed == p->nEntriesAlloc )
     { // need to allocate more entries
         assert( p->pEntriesFree == NULL );
         if ( p->nChunks == p->nChunksAlloc )
         {
             p->nChunksAlloc *= 2;
-            p->pChunks = REALLOC( char *, p->pChunks, p->nChunksAlloc ); 
+            p->pChunks = ABC_REALLOC( char *, p->pChunks, p->nChunksAlloc ); 
         }
-        p->pEntriesFree = ALLOC( char, p->nEntrySize * p->nChunkSize );
+        p->pEntriesFree = ABC_ALLOC( char, p->nEntrySize * p->nChunkSize );
         p->nMemoryAlloc += p->nEntrySize * p->nChunkSize;
         // transform these entries into a linked list
         pTemp = p->pEntriesFree;
@@ -191,7 +196,7 @@ char * Sat_MmFixedEntryFetch( Sat_MmFixed_t * p )
     p->nEntriesUsed++;
     if ( p->nEntriesMax < p->nEntriesUsed )
         p->nEntriesMax = p->nEntriesUsed;
-    // return the first entry in the free entry list
+    // return the first entry in the ABC_FREE entry list
     pTemp = p->pEntriesFree;
     p->pEntriesFree = *((char **)pTemp);
     return pTemp;
@@ -212,7 +217,7 @@ void Sat_MmFixedEntryRecycle( Sat_MmFixed_t * p, char * pEntry )
 {
     // decrement the counter of used entries
     p->nEntriesUsed--;
-    // add the entry to the linked list of free entries
+    // add the entry to the linked list of ABC_FREE entries
     *((char **)pEntry) = p->pEntriesFree;
     p->pEntriesFree = pEntry;
 }
@@ -235,7 +240,7 @@ void Sat_MmFixedRestart( Sat_MmFixed_t * p )
 
     // deallocate all chunks except the first one
     for ( i = 1; i < p->nChunks; i++ )
-        free( p->pChunks[i] );
+        ABC_FREE( p->pChunks[i] );
     p->nChunks = 1;
     // transform these entries into a linked list
     pTemp = p->pChunks[0];
@@ -246,7 +251,7 @@ void Sat_MmFixedRestart( Sat_MmFixed_t * p )
     }
     // set the last link
     *((char **)pTemp) = NULL;
-    // set the free entry list
+    // set the ABC_FREE entry list
     p->pEntriesFree  = p->pChunks[0];
     // set the correct statistics
     p->nMemoryAlloc  = p->nEntrySize * p->nChunkSize;
@@ -288,7 +293,7 @@ Sat_MmFlex_t * Sat_MmFlexStart()
 {
     Sat_MmFlex_t * p;
 
-    p = ALLOC( Sat_MmFlex_t, 1 );
+    p = ABC_ALLOC( Sat_MmFlex_t, 1 );
     memset( p, 0, sizeof(Sat_MmFlex_t) );
 
     p->nEntriesUsed  = 0;
@@ -298,7 +303,7 @@ Sat_MmFlex_t * Sat_MmFlexStart()
     p->nChunkSize    = (1 << 16);
     p->nChunksAlloc  = 64;
     p->nChunks       = 0;
-    p->pChunks       = ALLOC( char *, p->nChunksAlloc );
+    p->pChunks       = ABC_ALLOC( char *, p->nChunksAlloc );
 
     p->nMemoryUsed   = 0;
     p->nMemoryAlloc  = 0;
@@ -329,9 +334,9 @@ void Sat_MmFlexStop( Sat_MmFlex_t * p, int fVerbose )
             p->nEntriesUsed, p->nMemoryUsed, p->nMemoryAlloc );
     }
     for ( i = 0; i < p->nChunks; i++ )
-        free( p->pChunks[i] );
-    free( p->pChunks );
-    free( p );
+        ABC_FREE( p->pChunks[i] );
+    ABC_FREE( p->pChunks );
+    ABC_FREE( p );
 }
 
 /**Function*************************************************************
@@ -348,13 +353,13 @@ void Sat_MmFlexStop( Sat_MmFlex_t * p, int fVerbose )
 char * Sat_MmFlexEntryFetch( Sat_MmFlex_t * p, int nBytes )
 {
     char * pTemp;
-    // check if there are still free entries
+    // check if there are still ABC_FREE entries
     if ( p->pCurrent == NULL || p->pCurrent + nBytes > p->pEnd )
     { // need to allocate more entries
         if ( p->nChunks == p->nChunksAlloc )
         {
             p->nChunksAlloc *= 2;
-            p->pChunks = REALLOC( char *, p->pChunks, p->nChunksAlloc ); 
+            p->pChunks = ABC_REALLOC( char *, p->pChunks, p->nChunksAlloc ); 
         }
         if ( nBytes > p->nChunkSize )
         {
@@ -362,7 +367,7 @@ char * Sat_MmFlexEntryFetch( Sat_MmFlex_t * p, int nBytes )
             // (ideally, this should never happen)
             p->nChunkSize = 2 * nBytes;
         }
-        p->pCurrent = ALLOC( char, p->nChunkSize );
+        p->pCurrent = ABC_ALLOC( char, p->nChunkSize );
         p->pEnd     = p->pCurrent + p->nChunkSize;
         p->nMemoryAlloc += p->nChunkSize;
         // add the chunk to the chunk storage
@@ -412,7 +417,7 @@ int Sat_MmFlexReadMemUsage( Sat_MmFlex_t * p )
   are employed internally. Calling this procedure with nSteps equal
   to 10 results in 10 hierarchically arranged internal memory managers, 
   which can allocate up to 4096 (1Kb) entries. Requests for larger 
-  entries are handed over to malloc() and then free()ed.]
+  entries are handed over to malloc() and then ABC_FREE()ed.]
                
   SideEffects []
 
@@ -423,15 +428,15 @@ Sat_MmStep_t * Sat_MmStepStart( int nSteps )
 {
     Sat_MmStep_t * p;
     int i, k;
-    p = ALLOC( Sat_MmStep_t, 1 );
+    p = ABC_ALLOC( Sat_MmStep_t, 1 );
     p->nMems = nSteps;
     // start the fixed memory managers
-    p->pMems = ALLOC( Sat_MmFixed_t *, p->nMems );
+    p->pMems = ABC_ALLOC( Sat_MmFixed_t *, p->nMems );
     for ( i = 0; i < p->nMems; i++ )
         p->pMems[i] = Sat_MmFixedStart( (8<<i) );
     // set up the mapping of the required memory size into the corresponding manager
     p->nMapSize = (4<<p->nMems);
-    p->pMap = ALLOC( Sat_MmFixed_t *, p->nMapSize+1 );
+    p->pMap = ABC_ALLOC( Sat_MmFixed_t *, p->nMapSize+1 );
     p->pMap[0] = NULL;
     for ( k = 1; k <= 4; k++ )
         p->pMap[k] = p->pMems[0];
@@ -442,7 +447,7 @@ Sat_MmStep_t * Sat_MmStepStart( int nSteps )
 //printf( "%10d: size = %10d\n", i, p->pMap[i]->nEntrySize );
     p->nChunksAlloc  = 64;
     p->nChunks       = 0;
-    p->pChunks       = ALLOC( char *, p->nChunksAlloc );
+    p->pChunks       = ABC_ALLOC( char *, p->nChunksAlloc );
     return p;
 }
 
@@ -463,14 +468,14 @@ void Sat_MmStepStop( Sat_MmStep_t * p, int fVerbose )
     if ( p->nChunksAlloc )
     {
         for ( i = 0; i < p->nChunks; i++ )
-            free( p->pChunks[i] );
-        free( p->pChunks );
+            ABC_FREE( p->pChunks[i] );
+        ABC_FREE( p->pChunks );
     }
     for ( i = 0; i < p->nMems; i++ )
         Sat_MmFixedStop( p->pMems[i], fVerbose );
-    free( p->pMems );
-    free( p->pMap );
-    free( p );
+    ABC_FREE( p->pMems );
+    ABC_FREE( p->pMap );
+    ABC_FREE( p );
 }
 
 /**Function*************************************************************
@@ -493,9 +498,9 @@ char * Sat_MmStepEntryFetch( Sat_MmStep_t * p, int nBytes )
         if ( p->nChunks == p->nChunksAlloc )
         {
             p->nChunksAlloc *= 2;
-            p->pChunks = REALLOC( char *, p->pChunks, p->nChunksAlloc ); 
+            p->pChunks = ABC_REALLOC( char *, p->pChunks, p->nChunksAlloc ); 
         }
-        p->pChunks[ p->nChunks++ ] = ALLOC( char, nBytes );
+        p->pChunks[ p->nChunks++ ] = ABC_ALLOC( char, nBytes );
         return p->pChunks[p->nChunks-1];
     }
     return Sat_MmFixedEntryFetch( p->pMap[nBytes] );
@@ -519,7 +524,7 @@ void Sat_MmStepEntryRecycle( Sat_MmStep_t * p, char * pEntry, int nBytes )
         return;
     if ( nBytes > p->nMapSize )
     {
-//        free( pEntry );
+//        ABC_FREE( pEntry );
         return;
     }
     Sat_MmFixedEntryRecycle( p->pMap[nBytes], pEntry );
diff --git a/src/sat/bsat/satMem.h b/src/sat/bsat/satMem.h
index f60d7fdd..b6d93807 100644
--- a/src/sat/bsat/satMem.h
+++ b/src/sat/bsat/satMem.h
@@ -23,11 +23,6 @@
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
 
-#include <stdio.h>
-#include <stdlib.h>
-#include <string.h>
-#include <assert.h>
-
 ////////////////////////////////////////////////////////////////////////
 ///                         PARAMETERS                               ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c
index 833ea394..d2ebf552 100644
--- a/src/sat/bsat/satSolver.c
+++ b/src/sat/bsat/satSolver.c
@@ -2,7 +2,7 @@
 MiniSat -- Copyright (c) 2005, Niklas Sorensson
 http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/
 
-Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
+Permission is hereby granted, ABC_FREE of charge, to any person obtaining a copy of this software and
 associated documentation files (the "Software"), to deal in the Software without restriction,
 including without limitation the rights to use, copy, modify, merge, publish, distribute,
 sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
@@ -25,7 +25,6 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include <math.h>
 
 #include "satSolver.h"
-#include "port_type.h"
 
 //#define SAT_USE_SYSTEM_MEMORY_MANAGEMENT
 
@@ -91,9 +90,9 @@ static inline void  clause_setactivity(clause* c, float a) { *((float*)&c->lits[
 //=================================================================================================
 // Encode literals in clause pointers:
 
-static inline clause* clause_from_lit (lit l)     { return (clause*)((PORT_PTRUINT_T)l + (PORT_PTRUINT_T)l + 1); }
-static inline bool    clause_is_lit   (clause* c) { return ((PORT_PTRUINT_T)c & 1);                              }
-static inline lit     clause_read_lit (clause* c) { return (lit)((PORT_PTRUINT_T)c >> 1);                        }
+static inline clause* clause_from_lit (lit l)     { return (clause*)((ABC_PTRUINT_T)l + (ABC_PTRUINT_T)l + 1); }
+static inline bool    clause_is_lit   (clause* c) { return ((ABC_PTRUINT_T)c & 1);                              }
+static inline lit     clause_read_lit (clause* c) { return (lit)((ABC_PTRUINT_T)c >> 1);                        }
 
 //=================================================================================================
 // Simple helpers:
@@ -288,15 +287,15 @@ static clause* clause_new(sat_solver* s, lit* begin, lit* end, int learnt)
     assert(end - begin > 1);
     assert(learnt >= 0 && learnt < 2);
     size           = end - begin;
-//    c              = (clause*)malloc(sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float));
+//    c              = (clause*)ABC_ALLOC( char, sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float));
 #ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT
-    c = (clause*)malloc(sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float));
+    c = (clause*)ABC_ALLOC( char, sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float));
 #else
     c = (clause*)Sat_MmStepEntryFetch( s->pMem, sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float) );
 #endif
 
     c->size_learnt = (size << 1) | learnt;
-    assert(((PORT_PTRUINT_T)c & 1) == 0);
+    assert(((ABC_PTRUINT_T)c & 1) == 0);
 
     for (i = 0; i < size; i++)
         c->lits[i] = begin[i];
@@ -344,7 +343,7 @@ static void clause_remove(sat_solver* s, clause* c)
     }
 
 #ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT
-    free(c);
+    ABC_FREE(c);
 #else
     Sat_MmStepEntryRecycle( s->pMem, (char *)c, sizeof(clause) + sizeof(lit) * clause_size(c) + clause_learnt(c) * sizeof(float) );
 #endif
@@ -378,15 +377,15 @@ void sat_solver_setnvars(sat_solver* s,int n)
 
         while (s->cap < n) s->cap = s->cap*2+1;
 
-        s->wlists    = (vecp*)   realloc(s->wlists,   sizeof(vecp)*s->cap*2);
-        s->activity  = (double*) realloc(s->activity, sizeof(double)*s->cap);
-        s->factors   = (double*) realloc(s->factors,  sizeof(double)*s->cap);
-        s->assigns   = (lbool*)  realloc(s->assigns,  sizeof(lbool)*s->cap);
-        s->orderpos  = (int*)    realloc(s->orderpos, sizeof(int)*s->cap);
-        s->reasons   = (clause**)realloc(s->reasons,  sizeof(clause*)*s->cap);
-        s->levels    = (int*)    realloc(s->levels,   sizeof(int)*s->cap);
-        s->tags      = (lbool*)  realloc(s->tags,     sizeof(lbool)*s->cap);
-        s->trail     = (lit*)    realloc(s->trail,    sizeof(lit)*s->cap);
+        s->wlists    = ABC_REALLOC(vecp,   s->wlists,   s->cap*2);
+        s->activity  = ABC_REALLOC(double, s->activity, s->cap);
+        s->factors   = ABC_REALLOC(double, s->factors,  s->cap);
+        s->assigns   = ABC_REALLOC(lbool,  s->assigns,  s->cap);
+        s->orderpos  = ABC_REALLOC(int,    s->orderpos, s->cap);
+        s->reasons   = ABC_REALLOC(clause*,s->reasons,  s->cap);
+        s->levels    = ABC_REALLOC(int,    s->levels,   s->cap);
+        s->tags      = ABC_REALLOC(lbool,  s->tags,     s->cap);
+        s->trail     = ABC_REALLOC(lit,    s->trail,    s->cap);
     }
 
     for (var = s->size; var < n; var++){
@@ -830,14 +829,14 @@ void sat_solver_reducedb(sat_solver* s)
     vecp_resize(&s->learnts,j);
 }
 
-static lbool sat_solver_search(sat_solver* s, sint64 nof_conflicts, sint64 nof_learnts)
+static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts, ABC_INT64_T nof_learnts)
 {
     int*    levels          = s->levels;
     double  var_decay       = 0.95;
     double  clause_decay    = 0.999;
     double  random_var_freq = 0.02;
 
-    sint64  conflictC       = 0;
+    ABC_INT64_T  conflictC       = 0;
     veci    learnt_clause;
     int     i;
 
@@ -950,7 +949,7 @@ static lbool sat_solver_search(sat_solver* s, sint64 nof_conflicts, sint64 nof_l
 
 sat_solver* sat_solver_new(void)
 {
-    sat_solver* s = (sat_solver*)malloc(sizeof(sat_solver));
+    sat_solver* s = (sat_solver*)ABC_ALLOC( char, sizeof(sat_solver));
     memset( s, 0, sizeof(sat_solver) );
 
     // initialize vectors
@@ -990,7 +989,7 @@ sat_solver* sat_solver_new(void)
     s->simpdb_props           = 0;
     s->random_seed            = 91648253;
     s->progress_estimate      = 0;
-    s->binary                 = (clause*)malloc(sizeof(clause) + sizeof(lit)*2);
+    s->binary                 = (clause*)ABC_ALLOC( char, sizeof(clause) + sizeof(lit)*2);
     s->binary->size_learnt    = (2 << 1);
     s->verbosity              = 0;
 
@@ -1021,9 +1020,9 @@ void sat_solver_delete(sat_solver* s)
 #ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT
     int i;
     for (i = 0; i < vecp_size(&s->clauses); i++)
-        free(vecp_begin(&s->clauses)[i]);
+        ABC_FREE(vecp_begin(&s->clauses)[i]);
     for (i = 0; i < vecp_size(&s->learnts); i++)
-        free(vecp_begin(&s->learnts)[i]);
+        ABC_FREE(vecp_begin(&s->learnts)[i]);
 #else
     Sat_MmStepStop( s->pMem, 0 );
 #endif
@@ -1038,7 +1037,7 @@ void sat_solver_delete(sat_solver* s)
     veci_delete(&s->model);
     veci_delete(&s->act_vars);
     veci_delete(&s->temp_clause);
-    free(s->binary);
+    ABC_FREE(s->binary);
 
     // delete arrays
     if (s->wlists != 0){
@@ -1047,19 +1046,19 @@ void sat_solver_delete(sat_solver* s)
             vecp_delete(&s->wlists[i]);
 
         // if one is different from null, all are
-        free(s->wlists   );
-        free(s->activity );
-        free(s->factors  );
-        free(s->assigns  );
-        free(s->orderpos );
-        free(s->reasons  );
-        free(s->levels   );
-        free(s->trail    );
-        free(s->tags     );
+        ABC_FREE(s->wlists   );
+        ABC_FREE(s->activity );
+        ABC_FREE(s->factors  );
+        ABC_FREE(s->assigns  );
+        ABC_FREE(s->orderpos );
+        ABC_FREE(s->reasons  );
+        ABC_FREE(s->levels   );
+        ABC_FREE(s->trail    );
+        ABC_FREE(s->tags     );
     }
 
     sat_solver_store_free(s);
-    free(s);
+    ABC_FREE(s);
 }
 
 
@@ -1172,10 +1171,10 @@ bool sat_solver_simplify(sat_solver* s)
 }
 
 
-int sat_solver_solve(sat_solver* s, lit* begin, lit* end, sint64 nConfLimit, sint64 nInsLimit, sint64 nConfLimitGlobal, sint64 nInsLimitGlobal)
+int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal)
 {
-    sint64  nof_conflicts = 100;
-    sint64  nof_learnts   = sat_solver_nclauses(s) / 3;
+    ABC_INT64_T  nof_conflicts = 100;
+    ABC_INT64_T  nof_learnts   = sat_solver_nclauses(s) / 3;
     lbool   status        = l_Undef;
     lbool*  values        = s->assigns;
     lit*    i;
@@ -1398,6 +1397,9 @@ static void sortrnd(void** array, int size, int(*comp)(const void *, const void
 
 void sat_solver_sort(void** array, int size, int(*comp)(const void *, const void *))
 {
+//    int i;
     double seed = 91648253;
     sortrnd(array,size,comp,&seed);
+//    for ( i = 1; i < size; i++ )
+//        assert(comp(array[i-1], array[i])<0);
 }
diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h
index 7bb4bd6c..f37c1738 100644
--- a/src/sat/bsat/satSolver.h
+++ b/src/sat/bsat/satSolver.h
@@ -2,7 +2,7 @@
 MiniSat -- Copyright (c) 2005, Niklas Sorensson
 http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/
 
-Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
+Permission is hereby granted, ABC_FREE of charge, to any person obtaining a copy of this software and
 associated documentation files (the "Software"), to deal in the Software without restriction,
 including without limitation the rights to use, copy, modify, merge, publish, distribute,
 sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
@@ -22,10 +22,12 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #ifndef satSolver_h
 #define satSolver_h
 
-#ifdef _WIN32
-#define inline __inline // compatible with MS VS 6.0
-#endif
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+#include <assert.h>
 
+#include "abc_global.h"
 #include "satVec.h"
 #include "satMem.h"
 
@@ -46,17 +48,6 @@ static const bool  false     = 0;
 typedef int                lit;
 typedef char               lbool;
 
-#ifndef SINT64
-#define SINT64
-
-#ifdef _WIN32
-typedef signed __int64     sint64;   // compatible with MS VS 6.0
-#else
-typedef long long          sint64;
-#endif
-
-#endif
-
 static const int   var_Undef = -1;
 static const lit   lit_Undef = -2;
 
@@ -85,7 +76,7 @@ extern void        sat_solver_delete(sat_solver* s);
 
 extern bool        sat_solver_addclause(sat_solver* s, lit* begin, lit* end);
 extern bool        sat_solver_simplify(sat_solver* s);
-extern int         sat_solver_solve(sat_solver* s, lit* begin, lit* end, sint64 nConfLimit, sint64 nInsLimit, sint64 nConfLimitGlobal, sint64 nInsLimitGlobal);
+extern int         sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal);
 
 extern int         sat_solver_nvars(sat_solver* s);
 extern int         sat_solver_nclauses(sat_solver* s);
@@ -95,8 +86,8 @@ extern void        sat_solver_setnvars(sat_solver* s,int n);
 
 struct stats_t
 {
-    sint64   starts, decisions, propagations, inspects, conflicts;
-    sint64   clauses, clauses_literals, learnts, learnts_literals, max_literals, tot_literals;
+    ABC_INT64_T   starts, decisions, propagations, inspects, conflicts;
+    ABC_INT64_T   clauses, clauses_literals, learnts, learnts_literals, max_literals, tot_literals;
 };
 typedef struct stats_t stats;
 
@@ -167,8 +158,8 @@ struct sat_solver_t
 
     stats    stats;
 
-    sint64   nConfLimit;    // external limit on the number of conflicts
-    sint64   nInsLimit;     // external limit on the number of implications
+    ABC_INT64_T   nConfLimit;    // external limit on the number of conflicts
+    ABC_INT64_T   nInsLimit;     // external limit on the number of implications
 
     veci     act_vars;      // variables whose activity has changed
     double*  factors;       // the activity factors
diff --git a/src/sat/bsat/satStore.c b/src/sat/bsat/satStore.c
index 31fe92ca..fff8a836 100644
--- a/src/sat/bsat/satStore.c
+++ b/src/sat/bsat/satStore.c
@@ -23,6 +23,7 @@
 #include <string.h>
 #include <assert.h>
 #include <time.h>
+
 #include "satStore.h"
 
 ////////////////////////////////////////////////////////////////////////
@@ -49,7 +50,7 @@ char * Sto_ManMemoryFetch( Sto_Man_t * p, int nBytes )
     char * pMem;
     if ( p->pChunkLast == NULL || nBytes > p->nChunkSize - p->nChunkUsed )
     {
-        pMem = (char *)malloc( p->nChunkSize );
+        pMem = (char *)ABC_ALLOC( char, p->nChunkSize );
         *(char **)pMem = p->pChunkLast;
         p->pChunkLast = pMem;
         p->nChunkUsed = sizeof(char *);
@@ -76,8 +77,8 @@ void Sto_ManMemoryStop( Sto_Man_t * p )
     if ( p->pChunkLast == NULL )
         return;
     for ( pMem = p->pChunkLast; (pNext = *(char **)pMem); pMem = pNext )
-        free( pMem );
-    free( pMem );
+        ABC_FREE( pMem );
+    ABC_FREE( pMem );
 }
 
 /**Function*************************************************************
@@ -119,7 +120,7 @@ Sto_Man_t * Sto_ManAlloc()
 {
     Sto_Man_t * p;
     // allocate the manager
-    p = (Sto_Man_t *)malloc( sizeof(Sto_Man_t) );
+    p = (Sto_Man_t *)ABC_ALLOC( char, sizeof(Sto_Man_t) );
     memset( p, 0, sizeof(Sto_Man_t) );
     // memory management
     p->nChunkSize = (1<<16); // use 64K chunks
@@ -140,7 +141,7 @@ Sto_Man_t * Sto_ManAlloc()
 void Sto_ManFree( Sto_Man_t * p )
 {
     Sto_ManMemoryStop( p );
-    free( p );
+    ABC_FREE( p );
 }
 
 /**Function*************************************************************
@@ -398,7 +399,7 @@ Sto_Man_t * Sto_ManLoadClauses( char * pFileName )
 
     // alloc the array of literals
     nLitsAlloc = 1024;
-    pLits = (lit *)malloc( sizeof(lit) * nLitsAlloc );
+    pLits = (lit *)ABC_ALLOC( char, sizeof(lit) * nLitsAlloc );
 
     // read file header
     p->nVars = p->nClauses = p->nRoots = p->nClausesA = 0;
@@ -429,7 +430,7 @@ Sto_Man_t * Sto_ManLoadClauses( char * pFileName )
         if ( nLits == nLitsAlloc )
         {
             nLitsAlloc *= 2;
-            pLits = (lit *)realloc( pLits, sizeof(lit) * nLitsAlloc );
+            pLits = ABC_REALLOC( lit, pLits, nLitsAlloc );
         }
         pLits[ nLits++ ] = lit_read(Number);
     }
@@ -449,7 +450,7 @@ Sto_Man_t * Sto_ManLoadClauses( char * pFileName )
         return NULL;
     }
 
-    free( pLits );
+    ABC_FREE( pLits );
     fclose( pFile );
     return p;
 }
diff --git a/src/sat/bsat/satStore.h b/src/sat/bsat/satStore.h
index f63703d3..ea11f46a 100644
--- a/src/sat/bsat/satStore.h
+++ b/src/sat/bsat/satStore.h
@@ -21,8 +21,6 @@
 #ifndef __SAT_STORE_H__
 #define __SAT_STORE_H__
 
-#include "satSolver.h"
-
 /*
     The trace of SAT solving contains the original clauses of the problem
     along with the learned clauses derived during SAT solving.
@@ -30,6 +28,16 @@
     c <num_vars> <num_all_clauses> <num_root_clauses>
 */
 
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+#include "satSolver.h"
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
 #ifdef __cplusplus
 extern "C" {
 #endif
@@ -38,21 +46,9 @@ extern "C" {
 #define inline __inline // compatible with MS VS 6.0
 #endif
 
-#ifndef PRT
-#define PRT(a,t)  printf("%s = ", (a)); printf("%6.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC))
-#endif
-
 #define STO_MAX(a,b)  ((a) > (b) ? (a) : (b))
 
 ////////////////////////////////////////////////////////////////////////
-///                          INCLUDES                                ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                         PARAMETERS                               ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
 ///                         BASIC TYPES                              ///
 ////////////////////////////////////////////////////////////////////////
 
diff --git a/src/sat/bsat/satTrace.c b/src/sat/bsat/satTrace.c
index 111e8dfb..08cfadf6 100644
--- a/src/sat/bsat/satTrace.c
+++ b/src/sat/bsat/satTrace.c
@@ -18,8 +18,6 @@
 
 ***********************************************************************/
 
-#include <stdio.h>
-#include <assert.h>
 #include "satSolver.h"
 
 /*
diff --git a/src/sat/bsat/satUtil.c b/src/sat/bsat/satUtil.c
index ff8f9fd6..5f8008bb 100644
--- a/src/sat/bsat/satUtil.c
+++ b/src/sat/bsat/satUtil.c
@@ -21,7 +21,6 @@
 #include <stdio.h>
 #include <assert.h>
 #include "satSolver.h"
-#include "vec.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -170,7 +169,7 @@ int * Sat_SolverGetModel( sat_solver * p, int * pVars, int nVars )
 {
     int * pModel;
     int i;
-    pModel = ALLOC( int, nVars+1 );
+    pModel = ABC_ALLOC( int, nVars+1 );
     for ( i = 0; i < nVars; i++ )
     {
         assert( pVars[i] >= 0 && pVars[i] < p->size );
diff --git a/src/sat/bsat/satVec.h b/src/sat/bsat/satVec.h
index d7fce5c0..f017c90b 100644
--- a/src/sat/bsat/satVec.h
+++ b/src/sat/bsat/satVec.h
@@ -2,7 +2,7 @@
 MiniSat -- Copyright (c) 2005, Niklas Sorensson
 http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/
 
-Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
+Permission is hereby granted, ABC_FREE of charge, to any person obtaining a copy of this software and
 associated documentation files (the "Software"), to deal in the Software without restriction,
 including without limitation the rights to use, copy, modify, merge, publish, distribute,
 sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
@@ -22,8 +22,6 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #ifndef satVec_h
 #define satVec_h
 
-#include <stdlib.h>
-
 // vector of 32-bit intergers (added for 64-bit portability)
 struct veci_t {
     int    size;
@@ -35,10 +33,10 @@ typedef struct veci_t veci;
 static inline void veci_new (veci* v) {
     v->size = 0;
     v->cap  = 4;
-    v->ptr  = (int*)malloc(sizeof(int)*v->cap);
+    v->ptr  = (int*)ABC_ALLOC( char, sizeof(int)*v->cap);
 }
 
-static inline void   veci_delete (veci* v)          { free(v->ptr);   }
+static inline void   veci_delete (veci* v)          { ABC_FREE(v->ptr);   }
 static inline int*   veci_begin  (veci* v)          { return v->ptr;  }
 static inline int    veci_size   (veci* v)          { return v->size; }
 static inline void   veci_resize (veci* v, int k)   { v->size = k;    } // only safe to shrink !!
@@ -46,7 +44,7 @@ static inline void   veci_push   (veci* v, int e)
 {
     if (v->size == v->cap) {
         int newsize = v->cap * 2;//+1;
-        v->ptr = (int*)realloc(v->ptr,sizeof(int)*newsize);
+        v->ptr = ABC_REALLOC( int, v->ptr, newsize );
         v->cap = newsize; }
     v->ptr[v->size++] = e;
 }
@@ -63,10 +61,10 @@ typedef struct vecp_t vecp;
 static inline void vecp_new (vecp* v) {
     v->size = 0;
     v->cap  = 4;
-    v->ptr  = (void**)malloc(sizeof(void*)*v->cap);
+    v->ptr  = (void**)ABC_ALLOC( char, sizeof(void*)*v->cap);
 }
 
-static inline void   vecp_delete (vecp* v)          { free(v->ptr);   }
+static inline void   vecp_delete (vecp* v)          { ABC_FREE(v->ptr);   }
 static inline void** vecp_begin  (vecp* v)          { return v->ptr;  }
 static inline int    vecp_size   (vecp* v)          { return v->size; }
 static inline void   vecp_resize (vecp* v, int   k) { v->size = k;    } // only safe to shrink !!
@@ -74,7 +72,7 @@ static inline void   vecp_push   (vecp* v, void* e)
 {
     if (v->size == v->cap) {
         int newsize = v->cap * 2;//+1;
-        v->ptr = (void**)realloc(v->ptr,sizeof(void*)*newsize);
+        v->ptr = ABC_REALLOC( void*, v->ptr, newsize );
         v->cap = newsize; }
     v->ptr[v->size++] = e;
 }