Version abc90215

52 files changed, 2239 insertions, 483 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 7aad2eb2..b6a21b5f 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -1,5 +1,5 @@
 /**CFile****************************************************************
-
+ 
   FileName    [abc.c]
 
   SystemName  [ABC: Logic synthesis and verification system.]
@@ -39,6 +39,7 @@
 #include "ssw.h"
 #include "cgt.h"
 #include "amap.h"
+#include "gia.h"
 #include "cec.h"
 
 ////////////////////////////////////////////////////////////////////////
@@ -63,6 +64,7 @@ static int Abc_CommandPrintSharing   ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandPrintXCut      ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandPrintDsd       ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandPrintCone      ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandPrintMiter     ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Abc_CommandShow           ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandShowBdd        ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -149,12 +151,13 @@ static int Abc_CommandIResyn         ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandISat           ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandIFraig         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandDFraig         ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandNFraig         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandCSweep         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandDProve         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbSec          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandSimSec         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandMatch          ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandHaig           ( Abc_Frame_t * pAbc, int argc, char ** argv );
+//static int Abc_CommandHaig           ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandMini           ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandQbf            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
@@ -170,11 +173,11 @@ static int Abc_CommandFraigDress     ( Abc_Frame_t * pAbc, int argc, char ** arg
 //static int Abc_CommandHaigStop       ( Abc_Frame_t * pAbc, int argc, char ** argv );
 //static int Abc_CommandHaigUse        ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
-static int Abc_CommandRecStart       ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandRecStop        ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandRecAdd         ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandRecPs          ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandRecUse         ( Abc_Frame_t * pAbc, int argc, char ** argv );
+//static int Abc_CommandRecStart       ( Abc_Frame_t * pAbc, int argc, char ** argv );
+//static int Abc_CommandRecStop        ( Abc_Frame_t * pAbc, int argc, char ** argv );
+//static int Abc_CommandRecAdd         ( Abc_Frame_t * pAbc, int argc, char ** argv );
+//static int Abc_CommandRecPs          ( Abc_Frame_t * pAbc, int argc, char ** argv );
+//static int Abc_CommandRecUse         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Abc_CommandMap            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAmap           ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -270,6 +273,27 @@ static int Abc_CommandAbc8Zero       ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandAbc8Cec        ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc8DSec       ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
+static int Abc_CommandAbc9Get        ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Put        ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Read       ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Write      ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Ps         ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9PFan       ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Status     ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Show       ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Hash       ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Topand     ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Cof        ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Trim       ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Dfs        ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Sim        ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Times      ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Frames     ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Scl        ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Sat        ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Fraig      ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Test       ( Abc_Frame_t * pAbc, int argc, char ** argv );
+
 static int Abc_CommandAbcTestNew     ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 ////////////////////////////////////////////////////////////////////////
@@ -347,6 +371,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Printing",     "print_xcut",    Abc_CommandPrintXCut,        0 );
     Cmd_CommandAdd( pAbc, "Printing",     "print_dsd",     Abc_CommandPrintDsd,         0 );
     Cmd_CommandAdd( pAbc, "Printing",     "print_cone",    Abc_CommandPrintCone,        0 );
+    Cmd_CommandAdd( pAbc, "Printing",     "print_miter",   Abc_CommandPrintMiter,       0 );
 
     Cmd_CommandAdd( pAbc, "Printing",     "show",          Abc_CommandShow,             0 );
     Cmd_CommandAdd( pAbc, "Printing",     "show_bdd",      Abc_CommandShowBdd,          0 );
@@ -433,8 +458,9 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "New AIG",      "isat",          Abc_CommandISat,             1 );
     Cmd_CommandAdd( pAbc, "New AIG",      "ifraig",        Abc_CommandIFraig,           1 );
     Cmd_CommandAdd( pAbc, "New AIG",      "dfraig",        Abc_CommandDFraig,           1 );
+    Cmd_CommandAdd( pAbc, "New AIG",      "nfraig",        Abc_CommandNFraig,           1 );
     Cmd_CommandAdd( pAbc, "New AIG",      "csweep",        Abc_CommandCSweep,           1 );
-    Cmd_CommandAdd( pAbc, "New AIG",      "haig",          Abc_CommandHaig,             1 );
+//    Cmd_CommandAdd( pAbc, "New AIG",      "haig",          Abc_CommandHaig,             1 );
     Cmd_CommandAdd( pAbc, "New AIG",      "mini",          Abc_CommandMini,             1 );
     Cmd_CommandAdd( pAbc, "New AIG",      "qbf",           Abc_CommandQbf,              0 );
 
@@ -450,11 +476,11 @@ void Abc_Init( Abc_Frame_t * pAbc )
 //    Cmd_CommandAdd( pAbc, "Choicing",     "haig_stop",     Abc_CommandHaigStop,         0 );
 //    Cmd_CommandAdd( pAbc, "Choicing",     "haig_use",      Abc_CommandHaigUse,          1 );
 
-    Cmd_CommandAdd( pAbc, "Choicing",     "rec_start",     Abc_CommandRecStart,         0 );
-    Cmd_CommandAdd( pAbc, "Choicing",     "rec_stop",      Abc_CommandRecStop,          0 );
-    Cmd_CommandAdd( pAbc, "Choicing",     "rec_add",       Abc_CommandRecAdd,           0 );
-    Cmd_CommandAdd( pAbc, "Choicing",     "rec_ps",        Abc_CommandRecPs,            0 );
-    Cmd_CommandAdd( pAbc, "Choicing",     "rec_use",       Abc_CommandRecUse,           1 );
+//    Cmd_CommandAdd( pAbc, "Choicing",     "rec_start",     Abc_CommandRecStart,         0 );
+//    Cmd_CommandAdd( pAbc, "Choicing",     "rec_stop",      Abc_CommandRecStop,          0 );
+//    Cmd_CommandAdd( pAbc, "Choicing",     "rec_add",       Abc_CommandRecAdd,           0 );
+//    Cmd_CommandAdd( pAbc, "Choicing",     "rec_ps",        Abc_CommandRecPs,            0 );
+//    Cmd_CommandAdd( pAbc, "Choicing",     "rec_use",       Abc_CommandRecUse,           1 );
 
     Cmd_CommandAdd( pAbc, "SC mapping",   "map",           Abc_CommandMap,              1 );
     Cmd_CommandAdd( pAbc, "SC mapping",   "amap",          Abc_CommandAmap,             1 );
@@ -547,7 +573,28 @@ void Abc_Init( Abc_Frame_t * pAbc )
 
     Cmd_CommandAdd( pAbc, "ABC8",         "*cec",          Abc_CommandAbc8Cec,          0 );
     Cmd_CommandAdd( pAbc, "ABC8",         "*dsec",         Abc_CommandAbc8DSec,         0 );
- 
+
+    Cmd_CommandAdd( pAbc, "AIG",          "&get",          Abc_CommandAbc9Get,          0 );
+    Cmd_CommandAdd( pAbc, "AIG",          "&put",          Abc_CommandAbc9Put,          0 );
+    Cmd_CommandAdd( pAbc, "AIG",          "&r",            Abc_CommandAbc9Read,         0 );
+    Cmd_CommandAdd( pAbc, "AIG",          "&w",            Abc_CommandAbc9Write,        0 );
+    Cmd_CommandAdd( pAbc, "AIG",          "&ps",           Abc_CommandAbc9Ps,           0 );
+    Cmd_CommandAdd( pAbc, "AIG",          "&pfan",         Abc_CommandAbc9PFan,         0 );
+    Cmd_CommandAdd( pAbc, "AIG",          "&status",       Abc_CommandAbc9Status,       0 );
+    Cmd_CommandAdd( pAbc, "AIG",          "&show",         Abc_CommandAbc9Show,         0 );
+    Cmd_CommandAdd( pAbc, "AIG",          "&hash",         Abc_CommandAbc9Hash,         0 );
+    Cmd_CommandAdd( pAbc, "AIG",          "&topand",       Abc_CommandAbc9Topand,       0 );
+    Cmd_CommandAdd( pAbc, "AIG",          "&cof",          Abc_CommandAbc9Cof,          0 );
+    Cmd_CommandAdd( pAbc, "AIG",          "&trim",         Abc_CommandAbc9Trim,         0 );
+    Cmd_CommandAdd( pAbc, "AIG",          "&dfs",          Abc_CommandAbc9Dfs,          0 );
+    Cmd_CommandAdd( pAbc, "AIG",          "&sim",          Abc_CommandAbc9Sim,          0 );
+    Cmd_CommandAdd( pAbc, "AIG",          "&times",        Abc_CommandAbc9Times,        0 );
+    Cmd_CommandAdd( pAbc, "AIG",          "&frames",       Abc_CommandAbc9Frames,       0 );
+    Cmd_CommandAdd( pAbc, "AIG",          "&scl",          Abc_CommandAbc9Scl,          0 );
+    Cmd_CommandAdd( pAbc, "AIG",          "&sat",          Abc_CommandAbc9Sat,          0 );
+    Cmd_CommandAdd( pAbc, "AIG",          "&fraig",        Abc_CommandAbc9Fraig,        0 );
+    Cmd_CommandAdd( pAbc, "AIG",          "&test",         Abc_CommandAbc9Test,         0 );
+
     Cmd_CommandAdd( pAbc, "Various",      "testnew",         Abc_CommandAbcTestNew,     0 );
 
 //    Cmd_CommandAdd( pAbc, "Verification", "trace_start",   Abc_CommandTraceStart,       0 );
@@ -574,10 +621,14 @@ void Abc_Init( Abc_Frame_t * pAbc )
 //        extern void Aig_ManRandomTest1();
 //        Aig_ManRandomTest1();
     }
-//    malloc(1001);
     {
         extern void Extra_MemTest();
-//        Extra_MemTest();
+//       Extra_MemTest();
+    }
+
+    {
+        extern void Gia_SortTest();
+//        Gia_SortTest();
     }
 
 } 
@@ -624,6 +675,8 @@ void Abc_End()
     Abc_NtkFraigStoreClean();
 //    Rwt_Man4ExplorePrint();
 
+    if ( Abc_FrameGetGlobalFrame()->pAig )
+        Gia_ManStop( Abc_FrameGetGlobalFrame()->pAig );
 }
 
 /**Function*************************************************************
@@ -648,6 +701,7 @@ int Abc_CommandPrintStats( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fPrintTime;
     int fPrintMuxes;
     int fPower;
+    int fGlitch;
     int c;
 
     pNtk = Abc_FrameReadNtk(pAbc);
@@ -662,8 +716,9 @@ int Abc_CommandPrintStats( Abc_Frame_t * pAbc, int argc, char ** argv )
     fPrintTime = 0;
     fPrintMuxes = 0;
     fPower = 0;
+    fGlitch = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "fbdltmph" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "fbdltmpgh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -688,6 +743,9 @@ int Abc_CommandPrintStats( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'p':
             fPower ^= 1;
             break;
+        case 'g':
+            fGlitch ^= 1;
+            break;
         case 'h':
             goto usage;
         default:
@@ -705,7 +763,7 @@ int Abc_CommandPrintStats( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( Abc_FrameReadErr(pAbc), "Cannot print LUT delay for a non-logic network.\n" );
         return 1;
     }
-    Abc_NtkPrintStats( pOut, pNtk, fFactor, fSaveBest, fDumpResult, fUseLutLib, fPrintMuxes, fPower );
+    Abc_NtkPrintStats( pOut, pNtk, fFactor, fSaveBest, fDumpResult, fUseLutLib, fPrintMuxes, fPower, fGlitch );
     if ( fPrintTime )
     {
         pAbc->TimeTotal += pAbc->TimeCommand;
@@ -716,7 +774,7 @@ int Abc_CommandPrintStats( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: print_stats [-fbdltmph]\n" );
+    fprintf( pErr, "usage: print_stats [-fbdltmpgh]\n" );
     fprintf( pErr, "\t        prints the network statistics\n" );
     fprintf( pErr, "\t-f    : toggles printing the literal count in the factored forms [default = %s]\n", fFactor? "yes": "no" );
     fprintf( pErr, "\t-b    : toggles saving the best logic network in \"best.blif\" [default = %s]\n", fSaveBest? "yes": "no" );
@@ -725,6 +783,7 @@ usage:
     fprintf( pErr, "\t-t    : toggles printing runtime statistics [default = %s]\n", fPrintTime? "yes": "no" );
     fprintf( pErr, "\t-m    : toggles printing MUX statistics [default = %s]\n", fPrintMuxes? "yes": "no" );
     fprintf( pErr, "\t-p    : toggles printing power dissipation due to switching [default = %s]\n", fPower? "yes": "no" );
+    fprintf( pErr, "\t-q    : toggles printing percentage of increased power due to glitching [default = %s]\n", fGlitch? "yes": "no" );
     fprintf( pErr, "\t-h    : print the command usage\n");
     return 1;
 }
@@ -810,7 +869,7 @@ int Abc_CommandPrintExdc( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     else
         printf( "EXDC network statistics: \n" );
-    Abc_NtkPrintStats( pOut, pNtk->pExdc, 0, 0, 0, 0, 0, 0 );
+    Abc_NtkPrintStats( pOut, pNtk->pExdc, 0, 0, 0, 0, 0, 0, 0 );
     return 0;
 
 usage:
@@ -1303,7 +1362,7 @@ int Abc_CommandPrintSupport( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
     vSuppFun = Sim_ComputeFunSupp( pNtk, fVerbose );
-    free( vSuppFun->pArray[0] );
+    ABC_FREE( vSuppFun->pArray[0] );
     Vec_PtrFree( vSuppFun );
     return 0;
 
@@ -1998,6 +2057,66 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandPrintMiter( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk;
+    int c;
+    int fUseLibrary;
+
+    extern void Abc_NtkPrintMiter( Abc_Ntk_t * pNtk );
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    fUseLibrary = 1;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "lh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'l':
+            fUseLibrary ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        fprintf( pErr, "The network is should be structurally hashed.\n" );
+        return 1;
+    }
+    Abc_NtkPrintMiter( pNtk );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: print_miter [-h]\n" );
+    fprintf( pErr, "\t        prints the status of the miter\n" );
+    fprintf( pErr, "\t-h    : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandShow( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
@@ -3080,7 +3199,7 @@ int Abc_CommandFastExtract( Abc_Frame_t * pAbc, int argc, char ** argv )
     pErr = Abc_FrameReadErr(pAbc);
 
     // allocate the structure
-    p = ALLOC( Fxu_Data_t, 1 );
+    p = ABC_ALLOC( Fxu_Data_t, 1 );
     memset( p, 0, sizeof(Fxu_Data_t) );
     // set the defaults
     p->nSingleMax = 20000;
@@ -8039,6 +8158,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
 //    extern void Aig_ProcedureTest();
     extern void Abc_NtkDarTest( Abc_Ntk_t * pNtk );
     extern Abc_Ntk_t * Abc_NtkDarTestNtk( Abc_Ntk_t * pNtk );
+    extern void Amap_LibertyTest( char * pFileName );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -8251,7 +8371,9 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
 */
 
-    Abc_NtkDarTest( pNtk );
+//Amap_LibertyTest( "bwrc.lib" );
+
+//    Abc_NtkDarTest( pNtk );
 
     return 0;
 usage:
@@ -8883,7 +9005,7 @@ int Abc_CommandDRewrite( Abc_Frame_t * pAbc, int argc, char ** argv )
     // set defaults
     Dar_ManDefaultRwrParams( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "CNflzvwh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "CNflzrvwh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -8918,6 +9040,9 @@ int Abc_CommandDRewrite( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'z':
             pPars->fUseZeros ^= 1;
             break;
+        case 'r':
+            pPars->fRecycle ^= 1;
+            break;
         case 'v':
             pPars->fVerbose ^= 1;
             break;
@@ -8951,13 +9076,14 @@ int Abc_CommandDRewrite( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: drw [-C num] [-N num] [-lfzvwh]\n" );
+    fprintf( pErr, "usage: drw [-C num] [-N num] [-lfzrvwh]\n" );
     fprintf( pErr, "\t         performs combinational AIG rewriting\n" );
     fprintf( pErr, "\t-C num : the max number of cuts at a node [default = %d]\n", pPars->nCutsMax );
     fprintf( pErr, "\t-N num : the max number of subgraphs tried [default = %d]\n", pPars->nSubgMax );
     fprintf( pErr, "\t-l     : toggle preserving the number of levels [default = %s]\n", pPars->fUpdateLevel? "yes": "no" );
     fprintf( pErr, "\t-f     : toggle representing fanouts [default = %s]\n", pPars->fFanout? "yes": "no" );
     fprintf( pErr, "\t-z     : toggle using zero-cost replacements [default = %s]\n", pPars->fUseZeros? "yes": "no" );
+    fprintf( pErr, "\t-r     : toggle using cut recycling [default = %s]\n", pPars->fRecycle? "yes": "no" );
     fprintf( pErr, "\t-v     : toggle verbose printout [default = %s]\n", pPars->fVerbose? "yes": "no" );
     fprintf( pErr, "\t-w     : toggle very verbose printout [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
     fprintf( pErr, "\t-h     : print the command usage\n");
@@ -9946,6 +10072,152 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandNFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    Cec_ParCsw_t Pars, * p = &Pars; 
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk, * pNtkRes;
+    int c;
+    extern Abc_Ntk_t * Abc_NtkDarSatSweep( Abc_Ntk_t * pNtk, Cec_ParCsw_t * pPars );
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    Cec_ManCswSetDefaultParams( p );
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "WRCNZLrfvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'W':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-W\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            p->nWords = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( p->nWords < 0 ) 
+                goto usage;
+            break;
+        case 'R':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-R\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            p->nRounds = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( p->nRounds < 0 ) 
+                goto usage;
+            break;
+        case 'C':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            p->nBTLimit = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( p->nBTLimit < 0 ) 
+                goto usage;
+            break;
+        case 'N':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-N\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            p->nSatVarMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( p->nSatVarMax < 0 ) 
+                goto usage;
+            break;
+        case 'Z':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-Z\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            p->nCallsRecycle = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( p->nCallsRecycle < 0 ) 
+                goto usage;
+            break;
+        case 'L':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-L\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            p->nLevelMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( p->nLevelMax < 0 ) 
+                goto usage;
+            break;
+        case 'r':
+            p->fRewriting ^= 1;
+            break;
+        case 'f':
+            p->fFirstStop ^= 1;
+            break;
+        case 'v':
+            p->fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        fprintf( pErr, "This command works only for strashed networks.\n" );
+        return 1;
+    }
+    pNtkRes = Abc_NtkDarSatSweep( pNtk, p );
+    if ( pNtkRes == NULL )
+    {
+        fprintf( pErr, "Command has failed.\n" );
+        return 0;
+    }
+    // replace the current network
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+    return 0;
+usage:
+    fprintf( pErr, "usage: nfraig [-WRCNZL num] [-rfvh]\n" );
+    fprintf( pErr, "\t         performs fraiging using a new method\n" );
+    fprintf( pErr, "\t-W num : lthe number of simulation words [default = %d]\n", p->nWords );
+    fprintf( pErr, "\t-R num : the number of simulation rounds [default = %d]\n", p->nRounds );
+    fprintf( pErr, "\t-C num : limit on conflicts at a node [default = %d]\n", p->nBTLimit );
+    fprintf( pErr, "\t-N num : the min number of SAT vars before recycling [default = %d]\n", p->nSatVarMax );
+    fprintf( pErr, "\t-Z num : the min number of SAT calls before recycling [default = %d]\n", p->nCallsRecycle );
+    fprintf( pErr, "\t-L num : the maximum level of the nodes to be swept [default = %d]\n", p->nLevelMax );
+    fprintf( pErr, "\t-r     : toggle the use of AIG rewriting [default = %s]\n", p->fRewriting? "yes": "no" );
+    fprintf( pErr, "\t-f     : stop after one output is disproved [default = %s]\n", p->fFirstStop? "yes": "no" );
+    fprintf( pErr, "\t-v     : enable verbose printout [default = %s]\n", p->fVerbose? "yes": "no" );
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandCSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
@@ -10121,7 +10393,7 @@ int Abc_CommandIProve( Abc_Frame_t * pAbc, int argc, char ** argv )
             }
         if ( i == Abc_NtkCoNum(pNtk) )
             printf( "ERROR in Abc_NtkMiterProve(): Generated counter-example is invalid.\n" );
-        free( pSimInfo );
+        ABC_FREE( pSimInfo );
     }
  
     if ( RetValue == -1 ) 
@@ -10132,7 +10404,7 @@ int Abc_CommandIProve( Abc_Frame_t * pAbc, int argc, char ** argv )
         printf( "UNSATISFIABLE  " );
     //printf( "\n" );
 
-    PRT( "Time", clock() - clk );
+    ABC_PRT( "Time", clock() - clk );
     // replace the current network
     Abc_FrameReplaceCurrentNetwork( pAbc, pNtkTemp );
     return 0;
@@ -10157,6 +10429,7 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+/*
 int Abc_CommandHaig( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
@@ -10264,6 +10537,7 @@ usage:
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
 }
+*/
 
 /**Function*************************************************************
 
@@ -11001,6 +11275,7 @@ usage:
     return 1;
 }
 
+#if 0
 
 /**Function*************************************************************
 
@@ -11448,7 +11723,7 @@ usage:
     return 1;
 }
 
-
+#endif
 
 /**Function*************************************************************
 
@@ -11741,7 +12016,7 @@ usage:
     fprintf( pErr, "\t-E float : sets epsilon used for tie-breaking [default = %f]\n", pPars->fEpsilon );  
     fprintf( pErr, "\t-m       : toggles using MUX matching [default = %s]\n", pPars->fUseMuxes? "yes": "no" );
     fprintf( pErr, "\t-x       : toggles using XOR matching [default = %s]\n", pPars->fUseXors? "yes": "no" );
-    fprintf( pErr, "\t-i       : toggles assuming inverters are free [default = %s]\n", pPars->fFreeInvs? "yes": "no" );
+    fprintf( pErr, "\t-i       : toggles assuming inverters are ABC_FREE [default = %s]\n", pPars->fFreeInvs? "yes": "no" );
     fprintf( pErr, "\t-s       : toggles sweep after mapping [default = %s]\n", fSweep? "yes": "no" );
     fprintf( pErr, "\t-v       : toggles verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" );
     fprintf( pErr, "\t-h       : print the command usage\n");
@@ -12454,6 +12729,7 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
             globalUtilOptind++;
             if ( pPars->DelayTarget <= 0.0 ) 
                 goto usage;
+            break;
         case 'E':
             if ( globalUtilOptind >= argc )
             {
@@ -12888,7 +13164,7 @@ int Abc_CommandUndc( Abc_Frame_t * pAbc, int argc, char ** argv )
 
 usage:
     fprintf( pErr, "usage: undc [-h]\n" );
-    fprintf( pErr, "\t        converts latches with DC init values into free PIs\n" );
+    fprintf( pErr, "\t        converts latches with DC init values into ABC_FREE PIs\n" );
     fprintf( pErr, "\t-h    : print the command usage\n");
     return 1;
 }
@@ -14897,13 +15173,13 @@ int Abc_CommandSim( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "Only works for strashed networks.\n" );
         return 1;
     }
-    FREE( pNtk->pSeqModel );
+    ABC_FREE( pNtk->pSeqModel );
     Abc_NtkDarSeqSim( pNtk, nFrames, nWords, TimeOut, fNew, fComb, fMiter, fVerbose );        
     return 0;
 
 usage:
     fprintf( pErr, "usage: sim [-FWT num] [-ncmvh]\n" );
-    fprintf( pErr, "\t         performs random simulation of the sequentail miter\n" );
+    fprintf( pErr, "\t         performs random simulation of the sequential miter\n" );
     fprintf( pErr, "\t-F num : the number of frames to simulate [default = %d]\n", nFrames );
     fprintf( pErr, "\t-W num : the number of words to simulate [default = %d]\n", nWords );
     fprintf( pErr, "\t-T num : approximate runtime limit in seconds [default = %d]\n", TimeOut );
@@ -15698,7 +15974,7 @@ int Abc_CommandDCec( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fPartition;
     int fMiter;
 
-    extern int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fAlignPol, int fAndOuts, int fVerbose );
+    extern int Abc_NtkDSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fAlignPol, int fAndOuts, int fVerbose );
     extern int Abc_NtkDarCec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int fPartition, int fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
@@ -16843,13 +17119,13 @@ int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv )
     clk = clock();
     if ( Abc_NtkIsStrash(pNtk) )
     {
-        RetValue = Abc_NtkMiterSat( pNtk, (sint64)nConfLimit, (sint64)nInsLimit, fVerbose, NULL, NULL );
+        RetValue = Abc_NtkMiterSat( pNtk, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)nInsLimit, fVerbose, NULL, NULL );
     }
     else
     {
         assert( Abc_NtkIsLogic(pNtk) );
         Abc_NtkToBdd( pNtk );
-        RetValue = Abc_NtkMiterSat( pNtk, (sint64)nConfLimit, (sint64)nInsLimit, fVerbose, NULL, NULL );
+        RetValue = Abc_NtkMiterSat( pNtk, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)nInsLimit, fVerbose, NULL, NULL );
     }
 
     // verify that the pattern is correct
@@ -16860,7 +17136,7 @@ int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv )
         int * pSimInfo = Abc_NtkVerifySimulatePattern( pNtk, pNtk->pModel );
         if ( pSimInfo[0] != 1 )
             printf( "ERROR in Abc_NtkMiterSat(): Generated counter example is invalid.\n" );
-        free( pSimInfo );
+        ABC_FREE( pSimInfo );
         /*
         // print model
         Abc_NtkForEachPi( pNtk, pObj, i )
@@ -16880,7 +17156,7 @@ int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv )
     else
         printf( "UNSATISFIABLE  " );
     //printf( "\n" );
-    PRT( "Time", clock() - clk );
+    ABC_PRT( "Time", clock() - clk );
     return 0;
 
 usage:
@@ -16919,7 +17195,7 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv )
     int nInsLimit;
     int clk;
 
-    extern int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fAlignPol, int fAndOuts, int fVerbose );
+    extern int Abc_NtkDSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fAlignPol, int fAndOuts, int fVerbose );
 
 
     pNtk = Abc_FrameReadNtk(pAbc);
@@ -16999,7 +17275,7 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     clk = clock();
-    RetValue = Abc_NtkDSat( pNtk, (sint64)nConfLimit, (sint64)nInsLimit, fAlignPol, fAndOuts, fVerbose );
+    RetValue = Abc_NtkDSat( pNtk, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)nInsLimit, fAlignPol, fAndOuts, fVerbose );
     // verify that the pattern is correct
     if ( RetValue == 0 && Abc_NtkPoNum(pNtk) == 1 )
     {
@@ -17008,7 +17284,7 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv )
         int * pSimInfo = Abc_NtkVerifySimulatePattern( pNtk, pNtk->pModel );
         if ( pSimInfo[0] != 1 )
             printf( "ERROR in Abc_NtkMiterSat(): Generated counter example is invalid.\n" );
-        free( pSimInfo );
+        ABC_FREE( pSimInfo );
         /*
         // print model
         Abc_NtkForEachPi( pNtk, pObj, i )
@@ -17028,7 +17304,7 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv )
     else
         printf( "UNSATISFIABLE  " );
     //printf( "\n" );
-    PRT( "Time", clock() - clk );
+    ABC_PRT( "Time", clock() - clk );
     return 0;
 
 usage:
@@ -17163,7 +17439,7 @@ int Abc_CommandPSat( Abc_Frame_t * pAbc, int argc, char ** argv )
         int * pSimInfo = Abc_NtkVerifySimulatePattern( pNtk, pNtk->pModel );
         if ( pSimInfo[0] != 1 )
             printf( "ERROR in Abc_NtkMiterSat(): Generated counter example is invalid.\n" );
-        free( pSimInfo );
+        ABC_FREE( pSimInfo );
         /*
         // print model
         Abc_NtkForEachPi( pNtk, pObj, i )
@@ -17183,7 +17459,7 @@ int Abc_CommandPSat( Abc_Frame_t * pAbc, int argc, char ** argv )
     else
         printf( "UNSATISFIABLE  " );
     //printf( "\n" );
-    PRT( "Time", clock() - clk );
+    ABC_PRT( "Time", clock() - clk );
     return 0;
 
 usage:
@@ -17341,7 +17617,7 @@ int Abc_CommandProve( Abc_Frame_t * pAbc, int argc, char ** argv )
         int * pSimInfo = Abc_NtkVerifySimulatePattern( pNtk, pNtkTemp->pModel );
         if ( pSimInfo[0] != 1 )
             printf( "ERROR in Abc_NtkMiterProve(): Generated counter-example is invalid.\n" );
-        free( pSimInfo );
+        ABC_FREE( pSimInfo );
     }
  
     if ( RetValue == -1 ) 
@@ -17352,7 +17628,7 @@ int Abc_CommandProve( Abc_Frame_t * pAbc, int argc, char ** argv )
         printf( "UNSATISFIABLE  " );
     //printf( "\n" );
 
-    PRT( "Time", clock() - clk );
+    ABC_PRT( "Time", clock() - clk );
     // replace the current network
     Abc_FrameReplaceCurrentNetwork( pAbc, pNtkTemp );
     return 0;
@@ -18581,7 +18857,7 @@ int Abc_CommandAbc8Read( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     else
     {
-        extern void * Nal_ManRead( char * pFileName );
+//        extern void * Nal_ManRead( char * pFileName );
         pAbc->pAbc8Ntl = NULL;
 //        pAbc->pAbc8Ntl = Nal_ManRead( pFileName );
 //        Ioa_WriteBlif( pAbc->pAbc8Ntl, "test_boxes.blif" );
@@ -19380,7 +19656,7 @@ int Abc_CommandAbc8If( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // enable truth table computation if choices are selected
-    if ( (c = Aig_ManCountChoices( pAbc->pAbc8Aig )) )
+    if ( (c = Aig_ManChoiceNum( pAbc->pAbc8Aig )) )
     {
         printf( "Performing LUT mapping with %d choices.\n", c );
         pPars->fExpRed = 0;
@@ -21519,6 +21795,1213 @@ usage:
 }
 
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandAbc9Read( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    Gia_Man_t * pAig;
+    FILE * pFile;
+    char ** pArgvNew;
+    char * FileName, * pTemp;
+    int nArgcNew;
+    int c, fVerbose = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        default:
+            goto usage;
+        }
+    }
+    pArgvNew = argv + globalUtilOptind;
+    nArgcNew = argc - globalUtilOptind;
+    if ( nArgcNew != 1 )
+    {
+        printf( "There is no file name.\n" );
+        return 1;
+    }
+
+    // get the input file name
+    FileName = pArgvNew[0];
+    // fix the wrong symbol
+    for ( pTemp = FileName; *pTemp; pTemp++ )
+        if ( *pTemp == '>' )
+            *pTemp = '\\';
+    if ( (pFile = fopen( FileName, "r" )) == NULL )
+    {
+        fprintf( pAbc->Err, "Cannot open input file \"%s\". ", FileName );
+        if ( (FileName = Extra_FileGetSimilarName( FileName, ".aig", ".blif", ".pla", ".eqn", ".bench" )) )
+            fprintf( pAbc->Err, "Did you mean \"%s\"?", FileName );
+        fprintf( pAbc->Err, "\n" );
+        return 1;
+    }
+    fclose( pFile );
+
+    pAig = Gia_ReadAiger( FileName, 0 );
+    if ( pAig == NULL )
+    {
+        printf( "Reading AIGER has failed.\n" );
+        return 0;
+    }
+    if ( pAbc->pAig )
+        Gia_ManStop( pAbc->pAig );
+    pAbc->pAig = pAig;
+    return 0;
+
+usage:
+    fprintf( stdout, "usage: &r [-vh] <file>\n" );
+    fprintf( stdout, "\t         reads the current AIG from the AIGER file\n" );
+    fprintf( stdout, "\t-v     : toggles additional verbose output [default = %s]\n", fVerbose? "yes": "no" );
+    fprintf( stdout, "\t-h     : print the command usage\n");
+    fprintf( stdout, "\t<file> : the file name\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandAbc9Get( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
+    Gia_Man_t * pAig;
+    Aig_Man_t * pMan;
+    int c, fVerbose = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pNtkCur == NULL )
+    {
+        printf( "There is no current network\n" );
+        return 1;
+    }
+    if ( !Abc_NtkIsStrash( pAbc->pNtkCur ) )
+    {
+        printf( "The current network should be strashed.\n" );
+        return 1;
+    }
+    if ( Abc_NtkGetChoiceNum(pAbc->pNtkCur) )
+    {
+        printf( "Removing %d choices from the AIG.\n", Abc_NtkGetChoiceNum(pAbc->pNtkCur) );
+        Abc_AigCleanup(pAbc->pNtkCur->pManFunc);
+    }
+    pMan = Abc_NtkToDar( pAbc->pNtkCur, 0, 1 );
+    pAig = Gia_ManFromAig( pMan );
+    Aig_ManStop( pMan );
+    if ( pAig == NULL )
+    {
+        printf( "Transferring AIG has failed.\n" );
+        return 0;
+    }
+    if ( pAbc->pAig )
+        Gia_ManStop( pAbc->pAig );
+    pAbc->pAig = pAig;
+    return 0;
+
+usage:
+    fprintf( stdout, "usage: &get [-vh] <file>\n" );
+    fprintf( stdout, "\t         transfer the current network from the old ABC\n" );
+    fprintf( stdout, "\t-v     : toggles additional verbose output [default = %s]\n", fVerbose? "yes": "no" );
+    fprintf( stdout, "\t-h     : print the command usage\n");
+    fprintf( stdout, "\t<file> : the file name\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandAbc9Put( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan );
+    Aig_Man_t * pMan;
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk;
+    int c;
+    int fVerbose;
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    fVerbose    = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pAig == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+    pMan = Gia_ManToAig( pAbc->pAig );
+    pNtk = Abc_NtkFromAigPhase( pMan );
+    Aig_ManStop( pMan );
+    // replace the current network
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: &put [-vh]\n" );
+    fprintf( pErr, "\t         transfer the current network into the old ABC\n" );
+    fprintf( pErr, "\t-v     : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandAbc9Write( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    char * pFileName;
+    char ** pArgvNew;
+    int c, nArgcNew;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    pArgvNew = argv + globalUtilOptind;
+    nArgcNew = argc - globalUtilOptind;
+    if ( nArgcNew != 1 )
+    {
+        printf( "There is no file name.\n" );
+        return 1;
+    }
+    if ( pAbc->pAig == NULL )
+    {
+        printf( "Abc_CommandAbc9Write(): There is no AIG to write.\n" );
+        return 1;
+    } 
+    // create the design to write
+    pFileName = argv[globalUtilOptind];
+    Gia_WriteAiger( pAbc->pAig, pFileName, 0, 0 );
+    return 0;
+
+usage:
+    fprintf( stdout, "usage: &w [-h] <file>\n" );
+    fprintf( stdout, "\t        writes the current AIG into the AIGER file\n" );
+    fprintf( stdout, "\t-h    : print the command usage\n");
+    fprintf( stdout, "\t<file> : the file name\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandAbc9Ps( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    int c;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pAig == NULL )
+    {
+        printf( "Abc_CommandAbc9Ps(): There is no AIG.\n" );
+        return 1;
+    } 
+    Gia_ManPrintStats( pAbc->pAig );
+    return 0;
+
+usage:
+    fprintf( stdout, "usage: &ps [-h]\n" );
+    fprintf( stdout, "\t        prints stats of the current AIG\n" );
+    fprintf( stdout, "\t-h    : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandAbc9PFan( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    int c;
+    int nNodes = 40;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Nh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'N':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( stdout, "Command line switch \"-N\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nNodes = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nNodes < 0 ) 
+                goto usage;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pAig == NULL )
+    {
+        printf( "Abc_CommandAbc9PFan(): There is no AIG.\n" );
+        return 1;
+    } 
+    Gia_ManPrintFanio( pAbc->pAig, nNodes );
+    return 0;
+
+usage:
+    fprintf( stdout, "usage: &pfan [-N num] [-h]\n" );
+    fprintf( stdout, "\t         prints fanin/fanout statistics\n" );
+    fprintf( stdout, "\t-N num : the number of high-fanout nodes to explore [default = %d]\n", nNodes );
+    fprintf( stdout, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandAbc9Status( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    int c;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pAig == NULL )
+    {
+        printf( "Abc_CommandAbc9Status(): There is no AIG.\n" );
+        return 1;
+    } 
+    Gia_ManPrintMiterStatus( pAbc->pAig );
+    return 0;
+
+usage:
+    fprintf( stdout, "usage: &status [-h]\n" );
+    fprintf( stdout, "\t         prints status of the miter\n" );
+    fprintf( stdout, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandAbc9Show( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    Aig_Man_t * pMan;
+    int c;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pAig == NULL )
+    {
+        printf( "Abc_CommandAbc9Show(): There is no AIG.\n" );
+        return 1;
+    } 
+    pMan = Gia_ManToAig( pAbc->pAig );
+    Aig_ManShow( pMan, 0, NULL );
+    Aig_ManStop( pMan );
+    return 0;
+
+usage:
+    fprintf( stdout, "usage: &show [-h]\n" );
+    fprintf( stdout, "\t        shows the current AIG using GSView\n" );
+    fprintf( stdout, "\t-h    : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandAbc9Hash( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    Gia_Man_t * pTemp;
+    int c;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pAig == NULL )
+    {
+        printf( "Abc_CommandAbc9Hash(): There is no AIG.\n" );
+        return 1;
+    } 
+    pAbc->pAig = Gia_ManRehash( pTemp = pAbc->pAig );
+    Gia_ManStop( pTemp );
+    return 0;
+
+usage:
+    fprintf( stdout, "usage: &hash [-h]\n" );
+    fprintf( stdout, "\t        performs structural hashing\n" );
+    fprintf( stdout, "\t-h    : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandAbc9Topand( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    Gia_Man_t * pTemp;
+    int c, fVerbose = 1;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pAig == NULL )
+    {
+        printf( "Abc_CommandAbc9Hash(): There is no AIG.\n" );
+        return 1;
+    } 
+    if ( Gia_ManRegNum(pAbc->pAig) > 0 )
+    {
+        printf( "Abc_CommandAbc9Topand(): Can only be applied to a combinational miter.\n" );
+        return 1;
+    } 
+    pAbc->pAig = Gia_ManDupTopAnd( pTemp = pAbc->pAig, fVerbose );
+    Gia_ManStop( pTemp );
+    return 0;
+
+usage:
+    fprintf( stdout, "usage: &topand [-vh]\n" );
+    fprintf( stdout, "\t        performs AND decomposition for combinational miter\n" );
+    fprintf( stdout, "\t-v    : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+    fprintf( stdout, "\t-h    : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandAbc9Cof( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    Gia_Man_t * pTemp;
+    int c, iVar = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Vh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'V':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( stdout, "Command line switch \"-V\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            iVar = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( iVar < 0 ) 
+                goto usage;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pAig == NULL )
+    {
+        printf( "Abc_CommandAbc9Cof(): There is no AIG.\n" );
+        return 1;
+    } 
+    pAbc->pAig = Gia_ManDupCofactored( pTemp = pAbc->pAig, iVar );
+    Gia_ManStop( pTemp );
+    return 0;
+
+usage:
+    fprintf( stdout, "usage: &cof [-V num] [-h]\n" );
+    fprintf( stdout, "\t         performs cofactoring w.r.t. a variable\n" );
+    fprintf( stdout, "\t-V num : the zero-based ID of the variable to cofactor [default = %d]\n", iVar );
+    fprintf( stdout, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandAbc9Trim( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    Gia_Man_t * pTemp;
+    int c;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pAig == NULL )
+    {
+        printf( "Abc_CommandAbc9Trim(): There is no AIG.\n" );
+        return 1;
+    } 
+    pAbc->pAig = Gia_ManDupTrimmed( pTemp = pAbc->pAig );
+    Gia_ManStop( pTemp );
+    return 0;
+
+usage:
+    fprintf( stdout, "usage: &trim [-h]\n" );
+    fprintf( stdout, "\t         removes PIs without fanout and PO driven by constants\n" );
+    fprintf( stdout, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandAbc9Dfs( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    Gia_Man_t * pTemp;
+    int c;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pAig == NULL )
+    {
+        printf( "Abc_CommandAbc9Dfs(): There is no AIG.\n" );
+        return 1;
+    } 
+    pAbc->pAig = Gia_ManDupDfs( pTemp = pAbc->pAig );
+    Gia_ManStop( pTemp );
+    return 0;
+
+usage:
+    fprintf( stdout, "usage: &dfs [-h]\n" );
+    fprintf( stdout, "\t        orders objects in the DFS order\n" );
+    fprintf( stdout, "\t-h    : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandAbc9Sim( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    Gia_ParSim_t Pars, * pPars = &Pars;
+    int c;
+    Gia_ManSimSetDefaultParams( pPars );
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "WFTmvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'W':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( stdout, "Command line switch \"-W\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nWords = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nWords < 0 ) 
+                goto usage;
+            break;
+        case 'F':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( stdout, "Command line switch \"-F\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nIters = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nIters < 0 ) 
+                goto usage;
+            break;
+        case 'T':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( stdout, "Command line switch \"-T\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->TimeLimit = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->TimeLimit < 0 ) 
+                goto usage;
+            break;
+        case 'm':
+            pPars->fCheckMiter ^= 1;
+            break;
+        case 'v':
+            pPars->fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pAig == NULL )
+    {
+        printf( "Abc_CommandAbc9Sim(): There is no AIG.\n" );
+        return 1;
+    } 
+    Gia_ManSimSimulate( pAbc->pAig, pPars );
+    return 0;
+
+usage:
+    fprintf( stdout, "usage: &sim [-WFT <num>] [-mvh]\n" );
+    fprintf( stdout, "\t         performs random simulation of the sequential miter\n" );
+    fprintf( stdout, "\t-W num : the number of words to simulate [default = %d]\n", pPars->nWords );
+    fprintf( stdout, "\t-F num : the number of frames to simulate [default = %d]\n", pPars->nIters );
+    fprintf( stdout, "\t-T num : approximate runtime limit in seconds [default = %d]\n", pPars->TimeLimit );
+    fprintf( stdout, "\t-m     : toggle miter vs. any circuit [default = %s]\n", pPars->fCheckMiter? "miter": "not miter" );
+    fprintf( stdout, "\t-v     : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
+    fprintf( stdout, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandAbc9Times( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    Gia_Man_t * pTemp;
+    int c, nTimes = 2, fVerbose = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Nvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'N':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( stdout, "Command line switch \"-T\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nTimes = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nTimes < 0 ) 
+                goto usage;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pAig == NULL )
+    {
+        printf( "Abc_CommandAbc9Times(): There is no AIG.\n" );
+        return 1;
+    } 
+    pAbc->pAig = Gia_ManDupTimes( pTemp = pAbc->pAig, nTimes );
+    Gia_ManStop( pTemp );
+    return 0;
+
+usage:
+    fprintf( stdout, "usage: &times [-N <num>] [-vh]\n" );
+    fprintf( stdout, "\t         creates several \"parallel\" copies of the design\n" );
+    fprintf( stdout, "\t-N num : number of copies to create [default = %d]\n", nTimes );
+    fprintf( stdout, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+    fprintf( stdout, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandAbc9Frames( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    Gia_Man_t * pTemp;
+    Gia_ParFra_t Pars, * pPars = &Pars;
+    int c;
+    Gia_ManFraSetDefaultParams( pPars );
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Fivh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'F':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( stdout, "Command line switch \"-F\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nFrames = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nFrames < 0 ) 
+                goto usage;
+            break;
+        case 'i':
+            pPars->fInit ^= 1;
+            break;
+        case 'v':
+            pPars->fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pAig == NULL )
+    {
+        printf( "Abc_CommandAbc9Times(): There is no AIG.\n" );
+        return 1;
+    } 
+    pAbc->pAig = Gia_ManFrames( pTemp = pAbc->pAig, pPars );
+    Gia_ManStop( pTemp );
+    return 0;
+
+usage:
+    fprintf( stdout, "usage: &frames [-F <num>] [-ivh]\n" );
+    fprintf( stdout, "\t         unrolls the design for several timeframes\n" );
+    fprintf( stdout, "\t-F num : the number of frames to unroll [default = %d]\n", pPars->nFrames );
+    fprintf( stdout, "\t-i     : toggle initializing registers [default = %s]\n", pPars->fInit? "yes": "no" );
+    fprintf( stdout, "\t-v     : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
+    fprintf( stdout, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandAbc9Scl( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    Gia_Man_t * pTemp;
+    int c, fConst = 1, fEquiv = 1, fVerbose = 1;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "cevh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'c':
+            fConst ^= 1;
+            break;
+        case 'e':
+            fEquiv ^= 1;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pAig == NULL )
+    {
+        printf( "Abc_CommandAbc9Scl(): There is no AIG.\n" );
+        return 1;
+    } 
+    printf( "Implementation of this command is not finished.\n" );
+    return 0;
+
+    pAbc->pAig = Gia_ManSeqStructSweep( pTemp = pAbc->pAig, fConst, fEquiv, fVerbose );
+    Gia_ManStop( pTemp );
+    return 0;
+
+usage:
+    fprintf( stdout, "usage: &scl [-cevh]\n" );
+    fprintf( stdout, "\t         performs structural sequential cleanup\n" );
+    fprintf( stdout, "\t-c     : toggle removing stuck-at constant registers [default = %s]\n", fConst? "yes": "no" );
+    fprintf( stdout, "\t-e     : toggle removing equivalent-driver registers [default = %s]\n", fEquiv? "yes": "no" );
+    fprintf( stdout, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+    fprintf( stdout, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandAbc9Sat( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    Cec_ParSat_t ParsSat, * pPars = &ParsSat;
+    Gia_Man_t * pTemp;
+    int c;
+    Cec_ManSatSetDefaultParams( pPars );
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "CSNfvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'C':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( stdout, "Command line switch \"-C\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nBTLimit = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nBTLimit < 0 ) 
+                goto usage;
+            break;
+        case 'S':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( stdout, "Command line switch \"-S\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nSatVarMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nSatVarMax < 0 ) 
+                goto usage;
+            break;
+        case 'N':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( stdout, "Command line switch \"-N\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nCallsRecycle = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nCallsRecycle < 0 ) 
+                goto usage;
+            break;
+        case 'f':
+            pPars->fFirstStop ^= 1;
+            break;
+        case 'v':
+            pPars->fVerbose ^= 1;
+            break;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pAig == NULL )
+    {
+        printf( "Abc_CommandAbc9Sat(): There is no AIG.\n" );
+        return 1;
+    } 
+    pAbc->pAig = Cec_ManSatSolving( pTemp = pAbc->pAig, pPars );
+    Gia_ManStop( pTemp );
+    return 0;
+
+usage:
+    fprintf( stdout, "usage: &sat [-CSN <num>] [-fvh]\n" );
+    fprintf( stdout, "\t         performs SAT solving for the combinational outputs\n" );
+    fprintf( stdout, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
+    fprintf( stdout, "\t-S num : the min number of variables to recycle the solver [default = %d]\n", pPars->nSatVarMax );
+    fprintf( stdout, "\t-N num : the max number of calls to recycle the solver [default = %d]\n", pPars->nCallsRecycle );
+    fprintf( stdout, "\t-f     : toggle stopping when an output is satisfiable [default = %s]\n", pPars->fFirstStop? "yes": "no" );
+    fprintf( stdout, "\t-v     : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
+    fprintf( stdout, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    Cec_ParCsw_t ParsCsw, * pPars = &ParsCsw;
+    Gia_Man_t * pTemp;
+    int c;
+    Cec_ManCswSetDefaultParams( pPars );
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "WRILDCSNrmwvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'W':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( stdout, "Command line switch \"-W\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nWords = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nWords < 0 ) 
+                goto usage;
+            break;
+        case 'R':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( stdout, "Command line switch \"-R\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nRounds = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nRounds < 0 ) 
+                goto usage;
+            break;
+        case 'I':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( stdout, "Command line switch \"-I\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nItersMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nItersMax < 0 ) 
+                goto usage;
+            break;
+        case 'L':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( stdout, "Command line switch \"-L\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nLevelMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nLevelMax < 0 ) 
+                goto usage;
+            break;
+        case 'D':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( stdout, "Command line switch \"-D\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nDepthMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nDepthMax < 0 ) 
+                goto usage;
+            break;
+        case 'C':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( stdout, "Command line switch \"-C\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nBTLimit = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nBTLimit < 0 ) 
+                goto usage;
+            break;
+        case 'S':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( stdout, "Command line switch \"-S\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nSatVarMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nSatVarMax < 0 ) 
+                goto usage;
+            break;
+        case 'N':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( stdout, "Command line switch \"-N\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nCallsRecycle = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nCallsRecycle < 0 ) 
+                goto usage;
+            break;
+        case 'r':
+            pPars->fRewriting ^= 1;
+            break;
+        case 'm':
+            pPars->fFirstStop ^= 1;
+            break;
+        case 'w':
+            pPars->fVeryVerbose ^= 1;
+            break;
+        case 'v':
+            pPars->fVerbose ^= 1;
+            break;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pAig == NULL )
+    {
+        printf( "Abc_CommandAbc9Fraig(): There is no AIG.\n" );
+        return 1;
+    } 
+    pAbc->pAig = Cec_ManSatSweeping( pTemp = pAbc->pAig, pPars );
+    Gia_ManStop( pTemp );
+    return 0;
+
+usage:
+    fprintf( stdout, "usage: &fraig [-WRILDCSN <num>] [-rmwvh]\n" );
+    fprintf( stdout, "\t         performs combinational SAT sweeping\n" );
+    fprintf( stdout, "\t-W num : the number of simulation words [default = %d]\n", pPars->nWords );
+    fprintf( stdout, "\t-R num : the number of simulation rounds [default = %d]\n", pPars->nRounds );
+    fprintf( stdout, "\t-I num : the number of sweeping iterations [default = %d]\n", pPars->nItersMax );
+    fprintf( stdout, "\t-L num : the max number of levels of nodes to consider [default = %d]\n", pPars->nLevelMax );
+    fprintf( stdout, "\t-D num : the max number of steps of speculative reduction [default = %d]\n", pPars->nDepthMax );
+    fprintf( stdout, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
+    fprintf( stdout, "\t-S num : the min number of variables to recycle the solver [default = %d]\n", pPars->nSatVarMax );
+    fprintf( stdout, "\t-N num : the max number of calls to recycle the solver [default = %d]\n", pPars->nCallsRecycle );
+    fprintf( stdout, "\t-r     : toggle the use of AIG rewriting [default = %s]\n", pPars->fRewriting? "yes": "no" );
+    fprintf( stdout, "\t-m     : toggle stopping when an output is satisfiable [default = %s]\n", pPars->fFirstStop? "yes": "no" );
+    fprintf( stdout, "\t-w     : toggle printing even more verbose information [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
+    fprintf( stdout, "\t-v     : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
+    fprintf( stdout, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    int c;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pAig == NULL )
+    {
+        printf( "Abc_CommandAbc9Test(): There is no AIG.\n" );
+        return 1;
+    } 
+//    Gia_ManFrontTest( pAbc->pAig );
+//    Gia_ManReduceConst( pAbc->pAig, 1 );
+//    Sat_ManTest( pAbc->pAig, Gia_ManCo(pAbc->pAig, 0), 0 );
+    Gia_ManTestDistance( pAbc->pAig );
+    return 0;
+
+usage:
+    fprintf( stdout, "usage: &test [-h]\n" );
+    fprintf( stdout, "\t        testing various procedures\n" );
+    fprintf( stdout, "\t-h    : print the command usage\n");
+    return 1;
+}
+
 
 /**Function*************************************************************
 
diff --git a/src/base/abci/abcAbc8.c b/src/base/abci/abcAbc8.c
index be25d9c2..a306a8e4 100644
--- a/src/base/abci/abcAbc8.c
+++ b/src/base/abci/abcAbc8.c
@@ -161,12 +161,12 @@ Abc_Ntk_t * Abc_NtkNtkTest2( Abc_Ntk_t * pNtk )
 
 clk = clock();
     Abc_NtkSupportSum( pNtk );
-PRT( "Time", clock() - clk );
+ABC_PRT( "Time", clock() - clk );
 
     pMan = Abc_NtkToNtkNew( pNtk );
 clk = clock();
     Nwk_ManSupportSum( pMan );
-PRT( "Time", clock() - clk );
+ABC_PRT( "Time", clock() - clk );
 
     pNtkNew = Abc_NtkFromNtkNew( pNtk, pMan );
     Nwk_ManFree( pMan );
@@ -195,13 +195,13 @@ Abc_Ntk_t * Abc_NtkNtkTest3( Abc_Ntk_t * pNtk )
 
 clk = clock();
     printf( "%6.2f\n", Abc_NtkDelayTraceLut( pNtk, 1 ) );
-PRT( "Time", clock() - clk );
+ABC_PRT( "Time", clock() - clk );
 
     pMan = Abc_NtkToNtkNew( pNtk );
     pMan->pLutLib = Abc_FrameReadLibLut();
 clk = clock();
     printf( "%6.2f\n", Nwk_ManDelayTraceLut( pMan ) );
-PRT( "Time", clock() - clk );
+ABC_PRT( "Time", clock() - clk );
 
     pNtkNew = Abc_NtkFromNtkNew( pNtk, pMan );
     Nwk_ManFree( pMan );
diff --git a/src/base/abci/abcAttach.c b/src/base/abci/abcAttach.c
index d5d2aa16..e35cfdf6 100644
--- a/src/base/abci/abcAttach.c
+++ b/src/base/abci/abcAttach.c
@@ -80,8 +80,8 @@ int Abc_NtkAttach( Abc_Ntk_t * pNtk )
     ppGates = Mio_CollectRoots( pGenlib, 6, (float)1.0e+20, 1, &nGates );
 
     // derive the gate truth tables
-    puTruthGates    = ALLOC( unsigned *, nGates );
-    puTruthGates[0] = ALLOC( unsigned, 2 * nGates );
+    puTruthGates    = ABC_ALLOC( unsigned *, nGates );
+    puTruthGates[0] = ABC_ALLOC( unsigned, 2 * nGates );
     for ( i = 1; i < nGates; i++ )
         puTruthGates[i] = puTruthGates[i-1] + 2;
     for ( i = 0; i < nGates; i++ )
@@ -109,24 +109,24 @@ int Abc_NtkAttach( Abc_Ntk_t * pNtk )
         else if ( nFanins > 6 )
         {
             printf( "Cannot attach gate with more than 6 inputs to node %s.\n", Abc_ObjName(pNode) );
-            free( puTruthGates[0] );
-            free( puTruthGates );
-            free( ppGates );
+            ABC_FREE( puTruthGates[0] );
+            ABC_FREE( puTruthGates );
+            ABC_FREE( ppGates );
             return 0;
         }
         else if ( !Abc_NodeAttach( pNode, ppGates, puTruthGates, nGates, uTruths ) )
         {
             printf( "Could not attach the library gate to node %s.\n", Abc_ObjName(pNode) );
-            free( puTruthGates[0] );
-            free( puTruthGates );
-            free( ppGates );
+            ABC_FREE( puTruthGates[0] );
+            ABC_FREE( puTruthGates );
+            ABC_FREE( ppGates );
             return 0;
         }
     }
-    free( puTruthGates[0] );
-    free( puTruthGates );
-    free( ppGates );
-    FREE( s_pPerms );
+    ABC_FREE( puTruthGates[0] );
+    ABC_FREE( puTruthGates );
+    ABC_FREE( ppGates );
+    ABC_FREE( s_pPerms );
 
     // perform the final transformation
     Abc_NtkForEachNode( pNtk, pNode, i )
diff --git a/src/base/abci/abcAuto.c b/src/base/abci/abcAuto.c
index 40212c17..13be6eea 100644
--- a/src/base/abci/abcAuto.c
+++ b/src/base/abci/abcAuto.c
@@ -96,8 +96,8 @@ void Abc_NtkAutoPrint( Abc_Ntk_t * pNtk, int Output, int fNaive, int fVerbose )
 //    Extra_StopManager( pNtk->pManGlob );
 //    pNtk->pManGlob = NULL;
     Abc_NtkFreeGlobalBdds( pNtk, 1 );
-    free( pInputNames );
-    free( pOutputNames );
+    ABC_FREE( pInputNames );
+    ABC_FREE( pOutputNames );
     Vec_PtrFree( vFuncsGlob );
 }
 
@@ -161,8 +161,8 @@ void Abc_NtkAutoPrintAll( DdManager * dd, int nInputs, DdNode * pbOutputs[], int
             nSuppSizeMax = nSupp;
 
 
-//PRB( dd, bCanVars );
-//PRB( dd, bReduced );
+//ABC_PRB( dd, bCanVars );
+//ABC_PRB( dd, bReduced );
 //Cudd_PrintMinterm( dd, bReduced );
 //printf( "The equations are:\n" );
 //Cudd_zddPrintCover( dd, zEquations );
@@ -170,8 +170,8 @@ void Abc_NtkAutoPrintAll( DdManager * dd, int nInputs, DdNode * pbOutputs[], int
 //fflush( stdout );
 
         bSpace2 = Extra_bddSpaceFromMatrixPos( dd, zEquations );   Cudd_Ref( bSpace2 );
-//PRB( dd, bSpace1 );
-//PRB( dd, bSpace2 );
+//ABC_PRB( dd, bSpace1 );
+//ABC_PRB( dd, bSpace2 );
         if ( bSpace1 != bSpace2 )
             printf( "Spaces are NOT EQUAL!\n" );
 //        else
diff --git a/src/base/abci/abcBalance.c b/src/base/abci/abcBalance.c
index 26b6db99..134a175a 100644
--- a/src/base/abci/abcBalance.c
+++ b/src/base/abci/abcBalance.c
@@ -49,7 +49,7 @@ static Vec_Ptr_t * Abc_NodeBalanceConeExor( Abc_Obj_t * pNode );
 ***********************************************************************/
 Abc_Ntk_t * Abc_NtkBalance( Abc_Ntk_t * pNtk, bool fDuplicate, bool fSelective, bool fUpdateLevel )
 {
-    extern void Abc_NtkHaigTranfer( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtkNew );
+//    extern void Abc_NtkHaigTranfer( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtkNew );
     Abc_Ntk_t * pNtkAig;
     assert( Abc_NtkIsStrash(pNtk) );
     // compute the required times
@@ -61,7 +61,7 @@ Abc_Ntk_t * Abc_NtkBalance( Abc_Ntk_t * pNtk, bool fDuplicate, bool fSelective,
     // perform balancing
     pNtkAig = Abc_NtkStartFrom( pNtk, ABC_NTK_STRASH, ABC_FUNC_AIG );
     // transfer HAIG
-    Abc_NtkHaigTranfer( pNtk, pNtkAig );
+//    Abc_NtkHaigTranfer( pNtk, pNtkAig );
     // perform balancing
     Abc_NtkBalancePerform( pNtk, pNtkAig, fDuplicate, fSelective, fUpdateLevel );
     Abc_NtkFinalize( pNtk, pNtkAig );
@@ -271,8 +271,8 @@ Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld, Vec_
 //        printf( "Constant node\n" );
 //    assert( pNodeOld->Level >= Abc_ObjRegular(pNodeOld->pCopy)->Level );
     // update HAIG
-    if ( Abc_ObjRegular(pNodeOld->pCopy)->pNtk->pHaig )
-        Hop_ObjCreateChoice( pNodeOld->pEquiv, Abc_ObjRegular(pNodeOld->pCopy)->pEquiv );
+//    if ( Abc_ObjRegular(pNodeOld->pCopy)->pNtk->pHaig )
+//        Hop_ObjCreateChoice( pNodeOld->pEquiv, Abc_ObjRegular(pNodeOld->pCopy)->pEquiv );
     return pNodeOld->pCopy;
 }
 
diff --git a/src/base/abci/abcBidec.c b/src/base/abci/abcBidec.c
index 01146014..0b6165fb 100644
--- a/src/base/abci/abcBidec.c
+++ b/src/base/abci/abcBidec.c
@@ -138,7 +138,7 @@ void Abc_NtkBidecResyn( Abc_Ntk_t * pNtk, int fVerbose )
     if ( fVerbose )
     {
     printf( "Total gain in AIG nodes = %d.  ", nGainTotal );
-    PRT( "Total runtime", clock() - clk );
+    ABC_PRT( "Total runtime", clock() - clk );
     }
 }
 
diff --git a/src/base/abci/abcBmc.c b/src/base/abci/abcBmc.c
index 1512c76f..d2c5a12c 100644
--- a/src/base/abci/abcBmc.c
+++ b/src/base/abci/abcBmc.c
@@ -64,7 +64,7 @@ printf( "Fraig has %6d nodes.\n", Ivy_ManNodeNum(pFraig) );
     // report the classes
 //    if ( fVerbose )
 //        Abc_NtkBmcReport( pMan, pFrames, pFraig, vMapping, nFrames );
-    // free stuff
+    // ABC_FREE stuff
     Vec_PtrFree( vMapping );
     Ivy_ManStop( pFraig );
     Ivy_ManStop( pFrames );
diff --git a/src/base/abci/abcCas.c b/src/base/abci/abcCas.c
index 4ed7a774..ff0d761e 100644
--- a/src/base/abci/abcCas.c
+++ b/src/base/abci/abcCas.c
@@ -68,12 +68,12 @@ Abc_Ntk_t * Abc_NtkCascade( Abc_Ntk_t * pNtk, int nLutSize, int fCheck, int fVer
     {
         DdManager * dd = Abc_NtkGlobalBddMan( pNtk );
         printf( "Shared BDD size = %6d nodes.  ", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
-        PRT( "BDD construction time", clock() - clk );
+        ABC_PRT( "BDD construction time", clock() - clk );
     }
 
     // collect global BDDs
     dd = Abc_NtkGlobalBddMan( pNtk );
-    ppOutputs = ALLOC( DdNode *, Abc_NtkCoNum(pNtk) );
+    ppOutputs = ABC_ALLOC( DdNode *, Abc_NtkCoNum(pNtk) );
     Abc_NtkForEachCo( pNtk, pNode, i )
         ppOutputs[i] = Abc_ObjGlobalBdd(pNode);
 
@@ -89,8 +89,8 @@ Abc_Ntk_t * Abc_NtkCascade( Abc_Ntk_t * pNtk, int nLutSize, int fCheck, int fVer
 
     // cleanup
     Abc_NtkFreeGlobalBdds( pNtk, 1 );
-    free( ppOutputs );
-    free( pFileGeneric );
+    ABC_FREE( ppOutputs );
+    ABC_FREE( pFileGeneric );
 
 //    if ( pNtk->pExdc )
 //        pNtkNew->pExdc = Abc_NtkDup( pNtk->pExdc );
diff --git a/src/base/abci/abcClpBdd.c b/src/base/abci/abcClpBdd.c
index a6b3a770..27cba249 100644
--- a/src/base/abci/abcClpBdd.c
+++ b/src/base/abci/abcClpBdd.c
@@ -56,7 +56,7 @@ Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, i
     {
         DdManager * dd = Abc_NtkGlobalBddMan( pNtk );
         printf( "Shared BDD size = %6d nodes.  ", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
-        PRT( "BDD construction time", clock() - clk );
+        ABC_PRT( "BDD construction time", clock() - clk );
     }
 
     // create the new network
@@ -142,8 +142,8 @@ Abc_Ntk_t * Abc_NtkFromGlobalBdds( Abc_Ntk_t * pNtk )
     Extra_ProgressBarStop( pProgress );
 
 //    Extra_ReorderQuit( pReo );
-//PRT( "Reo ", runtime1 );
-//PRT( "Cudd", runtime2 );
+//ABC_PRT( "Reo ", runtime1 );
+//ABC_PRT( "Cudd", runtime2 );
 
     return pNtkNew;
 }
diff --git a/src/base/abci/abcCut.c b/src/base/abci/abcCut.c
index 1c7459eb..48c2f8e0 100644
--- a/src/base/abci/abcCut.c
+++ b/src/base/abci/abcCut.c
@@ -189,7 +189,7 @@ Cut_Man_t * Abc_NtkCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams )
     Vec_PtrFree( vNodes );
     Vec_IntFree( vChoices );
     Cut_ManPrintStats( p );
-PRT( "TOTAL", clock() - clk );
+ABC_PRT( "TOTAL", clock() - clk );
     printf( "Area = %d.\n", Abc_NtkComputeArea( pNtk, p ) );
 //Abc_NtkPrintCuts( p, pNtk, 0 );
 //    Cut_ManPrintStatsToFile( p, pNtk->pSpec, clock() - clk );
@@ -256,7 +256,7 @@ void Abc_NtkCutsOracle( Abc_Ntk_t * pNtk, Cut_Oracle_t * p )
         }
     }
     Vec_PtrFree( vNodes );
-//PRT( "Total", clock() - clk );
+//ABC_PRT( "Total", clock() - clk );
 //Abc_NtkPrintCuts_( p, pNtk, 0 );
 }
 
@@ -356,7 +356,7 @@ Cut_Man_t * Abc_NtkSeqCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams )
 if ( pParams->fVerbose )
 {
     Cut_ManPrintStats( p );
-PRT( "TOTAL ", clock() - clk );
+ABC_PRT( "TOTAL ", clock() - clk );
 printf( "Converged after %d iterations.\n", nIters );
 }
 //Abc_NtkPrintCuts( p, pNtk, 1 );
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 9dc10d84..dbd461c4 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -29,8 +29,9 @@
 #include "dch.h"
 #include "ssw.h"
 #include "cgt.h"
+//#include "fsim.h"
+#include "gia.h"
 #include "cec.h"
-#include "fsim.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -174,7 +175,7 @@ Aig_Man_t * Abc_NtkToDarChoices( Abc_Ntk_t * pNtk )
     pMan->pName = Extra_UtilStrsav( pNtk->pName );
     if ( Abc_NtkGetChoiceNum(pNtk) )
     {
-        pMan->pEquivs = ALLOC( Aig_Obj_t *, Abc_NtkObjNum(pNtk) );
+        pMan->pEquivs = ABC_ALLOC( Aig_Obj_t *, Abc_NtkObjNum(pNtk) );
         memset( pMan->pEquivs, 0, sizeof(Aig_Obj_t *) * Abc_NtkObjNum(pNtk) );
     }
     // transfer the pointers to the basic nodes
@@ -701,6 +702,35 @@ Abc_Ntk_t * Abc_NtkDarFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fDoSparse, in
   SeeAlso     []
 
 ***********************************************************************/
+Abc_Ntk_t * Abc_NtkDarSatSweep( Abc_Ntk_t * pNtk, Cec_ParCsw_t * pPars )
+{
+/*
+    extern Aig_Man_t * Cec_ManSatSweep( Aig_Man_t * pAig, Cec_ParCsw_t * pPars );
+    Abc_Ntk_t * pNtkAig;
+    Aig_Man_t * pMan, * pTemp;
+    pMan = Abc_NtkToDar( pNtk, 0, 0 );
+    if ( pMan == NULL )
+        return NULL;
+    pMan = Cec_ManSatSweep( pTemp = pMan, pPars );
+    Aig_ManStop( pTemp );
+    pNtkAig = Abc_NtkFromDar( pNtk, pMan );
+    Aig_ManStop( pMan );
+    return pNtkAig;
+    */
+    return NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Gives the current ABC network to AIG manager for processing.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 Abc_Ntk_t * Abc_NtkDarFraigPart( Abc_Ntk_t * pNtk, int nPartSize, int nConfLimit, int nLevelMax, int fVerbose )
 {
     Abc_Ntk_t * pNtkAig;
@@ -777,7 +807,7 @@ Abc_Ntk_t * Abc_NtkDRewrite( Abc_Ntk_t * pNtk, Dar_RwrPar_t * pPars )
 clk = clock();
     pMan = Aig_ManDupDfs( pTemp = pMan ); 
     Aig_ManStop( pTemp );
-//PRT( "time", clock() - clk );
+//ABC_PRT( "time", clock() - clk );
 
 //    Aig_ManPrintStats( pMan );
     pNtkAig = Abc_NtkFromDar( pNtk, pMan );
@@ -814,7 +844,7 @@ Abc_Ntk_t * Abc_NtkDRefactor( Abc_Ntk_t * pNtk, Dar_RefPar_t * pPars )
 clk = clock();
     pMan = Aig_ManDupDfs( pTemp = pMan ); 
     Aig_ManStop( pTemp );
-//PRT( "time", clock() - clk );
+//ABC_PRT( "time", clock() - clk );
 
 //    Aig_ManPrintStats( pMan );
     pNtkAig = Abc_NtkFromDar( pNtk, pMan );
@@ -847,7 +877,7 @@ Abc_Ntk_t * Abc_NtkDC2( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, int fF
 clk = clock();
     pMan = Dar_ManCompress2( pTemp = pMan, fBalance, fUpdateLevel, fFanout, fPower, fVerbose ); 
     Aig_ManStop( pTemp );
-//PRT( "time", clock() - clk );
+//ABC_PRT( "time", clock() - clk );
 
 //    Aig_ManPrintStats( pMan );
     pNtkAig = Abc_NtkFromDar( pNtk, pMan );
@@ -953,7 +983,7 @@ Abc_Ntk_t * Abc_NtkDrwsat( Abc_Ntk_t * pNtk, int fBalance, int fVerbose )
 clk = clock();
     pMan = Dar_ManRwsat( pTemp = pMan, fBalance, fVerbose ); 
     Aig_ManStop( pTemp );
-//PRT( "time", clock() - clk );
+//ABC_PRT( "time", clock() - clk );
 
 //    Aig_ManPrintStats( pMan );
     pNtkAig = Abc_NtkFromDar( pNtk, pMan );
@@ -1032,7 +1062,7 @@ Abc_Ntk_t * Abc_NtkConstructFromCnf( Abc_Ntk_t * pNtk, Cnf_Man_t * p, Vec_Ptr_t
         fprintf( stdout, "Abc_NtkConstructFromCnf(): Network check has failed.\n" );
     return pNtkNew;
 }
-
+ 
 /**Function*************************************************************
 
   Synopsis    [Gives the current ABC network to AIG manager for processing.]
@@ -1069,6 +1099,8 @@ Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName )
     // derive CNF
     pCnf = Cnf_Derive( pMan, 0 );
     Cnf_DataTranformPolarity( pCnf, 0 );
+    printf( "Vars = %6d. Clauses = %7d. Literals = %8d.\n", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals );
+
 /*
     // write the network for verification
     pManCnf = Cnf_ManRead();
@@ -1097,7 +1129,7 @@ Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName )
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fAlignPol, int fAndOuts, int fVerbose )
+int Abc_NtkDSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fAlignPol, int fAndOuts, int fVerbose )
 {
     Aig_Man_t * pMan;
     int RetValue;//, clk = clock();
@@ -1195,7 +1227,7 @@ int Abc_NtkDarCec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int fPa
             pNtk1->pModel = Abc_NtkVerifyGetCleanModel( pNtk1, 1 );
 //        pMiter->pModel = Abc_NtkVerifyGetCleanModel( pMiter, nFrames );
 //        Abc_NtkVerifyReportErrorSeq( pNtk1, pNtk2, pMiter->pModel, nFrames );
-//        FREE( pMiter->pModel );
+//        ABC_FREE( pMiter->pModel );
         Abc_NtkDelete( pMiter );
         return 0;
     }
@@ -1226,17 +1258,17 @@ finish:
     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;
@@ -1290,7 +1322,8 @@ int Abc_NtkDarCec2( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Cec_ParCec_t * pPars )
         }
     }
     // perform verification
-    RetValue = Cec_Solve( pMan1, pMan2, pPars );
+//    RetValue = Cec_Solve( pMan1, pMan2, pPars );
+    RetValue = -1;
     // transfer model if given
     pNtk1->pModel = pMan1->pData, pMan1->pData = NULL;
     Aig_ManStop( pMan1 );
@@ -1301,17 +1334,17 @@ int Abc_NtkDarCec2( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Cec_ParCec_t * pPars )
     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;
@@ -1345,7 +1378,7 @@ Abc_Ntk_t * Abc_NtkDarSeqSweep( Abc_Ntk_t * pNtk, Fra_Ssw_t * pPars )
         pNtkFraig = Abc_NtkFraig( pNtk, &Params, 0, 0 );
 if ( pPars->fVerbose ) 
 {
-PRT( "Initial fraiging time", clock() - clk );
+ABC_PRT( "Initial fraiging time", clock() - clk );
 }
     }
     else
@@ -1391,8 +1424,8 @@ void Abc_NtkPrintLatchEquivClasses( Abc_Ntk_t * pNtk, Aig_Man_t * pAig )
 {
     bool header_dumped = false;
     int num_orig_latches = Abc_NtkLatchNum(pNtk);
-    char **pNames = ALLOC( char *, num_orig_latches );
-    bool *p_irrelevant = ALLOC( bool, num_orig_latches );
+    char **pNames = ABC_ALLOC( char *, num_orig_latches );
+    bool *p_irrelevant = ABC_ALLOC( bool, num_orig_latches );
     char * pFlopName, * pReprName;
     Aig_Obj_t * pFlop, * pRepr;
     Abc_Obj_t * pNtkFlop; 
@@ -1402,7 +1435,7 @@ void Abc_NtkPrintLatchEquivClasses( Abc_Ntk_t * pNtk, Aig_Man_t * pAig )
     Abc_NtkForEachLatch( pNtk, pNtkFlop, i )
     {
         char *temp_name = Abc_ObjName( Abc_ObjFanout0(pNtkFlop) );
-        pNames[i] = ALLOC( char , strlen(temp_name)+1);
+        pNames[i] = ABC_ALLOC( char , strlen(temp_name)+1);
         strcpy(pNames[i], temp_name);
     }
     i = 0;
@@ -1457,13 +1490,13 @@ void Abc_NtkPrintLatchEquivClasses( Abc_Ntk_t * pNtk, Aig_Man_t * pAig )
             printf("%s ", pNames[i]);
         }
         
-        FREE(pNames[i]);
+        ABC_FREE(pNames[i]);
     }
     if (header_dumped)
         printf("\n");
     
-    FREE(pNames);
-    FREE(p_irrelevant);
+    ABC_FREE(pNames);
+    ABC_FREE(p_irrelevant);
 }
 
 /**Function*************************************************************
@@ -1617,8 +1650,8 @@ int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nSizeMax, int nNodeDelta,
     {
         int iFrame;
         RetValue = Saig_ManBmcSimple( pMan, nFrames, nSizeMax, nBTLimit, fRewrite, fVerbose, &iFrame );
-        FREE( pNtk->pModel );
-        FREE( pNtk->pSeqModel );
+        ABC_FREE( pNtk->pModel );
+        ABC_FREE( pNtk->pSeqModel );
         pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
         if ( RetValue == 1 )
             printf( "No output was asserted in %d frames. ", iFrame );
@@ -1634,8 +1667,8 @@ int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nSizeMax, int nNodeDelta,
     {
 /*
         Fra_BmcPerformSimple( pMan, nFrames, nBTLimit, fRewrite, fVerbose );
-        FREE( pNtk->pModel );
-        FREE( pNtk->pSeqModel );
+        ABC_FREE( pNtk->pModel );
+        ABC_FREE( pNtk->pSeqModel );
         pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
         if ( pNtk->pSeqModel )
         {
@@ -1652,8 +1685,8 @@ int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nSizeMax, int nNodeDelta,
 /*
         int iFrame;
         RetValue = Ssw_BmcDynamic( pMan, nFrames, nBTLimit, fVerbose, &iFrame );
-        FREE( pNtk->pModel );
-        FREE( pNtk->pSeqModel );
+        ABC_FREE( pNtk->pModel );
+        ABC_FREE( pNtk->pSeqModel );
         pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
         if ( RetValue == 1 )
             printf( "No output was asserted in %d frames. ", iFrame );
@@ -1666,11 +1699,11 @@ int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nSizeMax, int nNodeDelta,
         }
 */
         Saig_BmcPerform( pMan, nFrames, nNodeDelta, nBTLimit, nBTLimitAll, fVerbose );
-        FREE( pNtk->pModel );
-        FREE( pNtk->pSeqModel );
+        ABC_FREE( pNtk->pModel );
+        ABC_FREE( pNtk->pSeqModel );
         pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
     }
-PRT( "Time", clock() - clk );
+ABC_PRT( "Time", clock() - clk );
     // verify counter-example
     if ( pNtk->pSeqModel ) 
     {
@@ -1711,15 +1744,15 @@ int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, Inter_ManParams_t * pPars )
     else if ( RetValue == 0 )
     {
         printf( "Property DISPROVED in frame %d (use \"write_counter\" to dump a witness).  ", iFrame );
-        FREE( pNtk->pModel );
-        FREE( pNtk->pSeqModel );
+        ABC_FREE( pNtk->pModel );
+        ABC_FREE( pNtk->pSeqModel );
         pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
     }
     else if ( RetValue == -1 )
         printf( "Property UNDECIDED.  " );
     else
         assert( 0 );
-PRT( "Time", clock() - clk );
+ABC_PRT( "Time", clock() - clk );
     Aig_ManStop( pMan );
     return 1;
 }
@@ -1801,11 +1834,11 @@ int Abc_NtkDarProve( Abc_Ntk_t * pNtk, Fra_Sec_t * pSecPar )
         if ( RetValue == 1 )
         {
             printf( "Networks are equivalent after CEC.   " );
-            PRT( "Time", clock() - clk );
+            ABC_PRT( "Time", clock() - clk );
             if ( pSecPar->fReportSolution )
             {
             printf( "SOLUTION: PASS       " );
-            PRT( "Time", clock() - clkTotal );
+            ABC_PRT( "Time", clock() - clkTotal );
             }
             return RetValue;
         }
@@ -1819,7 +1852,7 @@ int Abc_NtkDarProve( Abc_Ntk_t * pNtk, Fra_Sec_t * pSecPar )
             if ( pSecPar->fReportSolution )
             {
             printf( "SOLUTION: FAIL       " );
-            PRT( "Time", clock() - clkTotal );
+            ABC_PRT( "Time", clock() - clkTotal );
             }
             return RetValue;
         }
@@ -1840,8 +1873,8 @@ int Abc_NtkDarProve( Abc_Ntk_t * pNtk, Fra_Sec_t * pSecPar )
     else
     {
         RetValue = Fra_FraigSec( pMan, pSecPar, NULL );
-        FREE( pNtk->pModel );
-        FREE( pNtk->pSeqModel );
+        ABC_FREE( pNtk->pModel );
+        ABC_FREE( pNtk->pSeqModel );
         pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
         if ( pNtk->pSeqModel )
         {
@@ -1888,7 +1921,7 @@ int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Fra_Sec_t * pSecPar )
         // report the error
         pMiter->pModel = Abc_NtkVerifyGetCleanModel( pMiter, pSecPar->nFramesMax );
         Abc_NtkVerifyReportErrorSeq( pNtk1, pNtk2, pMiter->pModel, pSecPar->nFramesMax );
-        FREE( pMiter->pModel );
+        ABC_FREE( pMiter->pModel );
         Abc_NtkDelete( pMiter );
         return 0;
     }
@@ -1916,7 +1949,7 @@ int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Fra_Sec_t * pSecPar )
         // report the error
         pMiter->pModel = Abc_NtkVerifyGetCleanModel( pMiter, nFrames );
         Abc_NtkVerifyReportErrorSeq( pNtk1, pNtk2, pMiter->pModel, nFrames );
-        FREE( pMiter->pModel );
+        ABC_FREE( pMiter->pModel );
         Abc_NtkDelete( pMiter );
         return 0;
     }
@@ -2297,6 +2330,7 @@ Abc_Ntk_t * Abc_NtkDarRetimeStep( Abc_Ntk_t * pNtk, int fVerbose )
   SeeAlso     []
 
 ***********************************************************************/
+/*
 Abc_Ntk_t * Abc_NtkDarHaigRecord( Abc_Ntk_t * pNtk, int nIters, int nSteps, int fRetimingOnly, int fAddBugs, int fUseCnf, int fVerbose )
 {
     Abc_Ntk_t * pNtkAig;
@@ -2315,6 +2349,7 @@ Abc_Ntk_t * Abc_NtkDarHaigRecord( Abc_Ntk_t * pNtk, int nIters, int nSteps, int
     Aig_ManStop( pMan );
     return pNtkAig;
 }
+*/
 
 /**Function*************************************************************
 
@@ -2334,9 +2369,15 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, in
     Aig_Man_t * pMan;
     Fra_Cex_t * pCex;
     int status, RetValue, clk = clock();
+    if ( Abc_NtkGetChoiceNum(pNtk) )
+    {
+        printf( "Removing %d choices from the AIG.\n", Abc_NtkGetChoiceNum(pNtk) );
+        Abc_AigCleanup(pNtk->pManFunc);
+    }
     pMan = Abc_NtkToDar( pNtk, 0, 1 );
     if ( fComb || Abc_NtkLatchNum(pNtk) == 0 )
     {
+/*
         if ( Cec_ManSimulate( pMan, nWords, nFrames, TimeOut, fMiter, fVerbose ) )
         {
             pCex = pMan->pSeqModel;
@@ -2348,8 +2389,8 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, in
             if ( status == 0 )
                 printf( "Abc_NtkDarSeqSim(): Counter-example verification has FAILED.\n" );
             }
-            FREE( pNtk->pModel );
-            FREE( pNtk->pSeqModel );
+            ABC_FREE( pNtk->pModel );
+            ABC_FREE( pNtk->pSeqModel );
             pNtk->pSeqModel = pCex;
             RetValue = 1;
         }
@@ -2359,6 +2400,8 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, in
             printf( "Simulation iterated %d times with %d words did not assert the outputs. ", 
                 nFrames, nWords );
         }
+*/
+        printf( "Comb simulation is temporarily disabled.\n" );
     }
     else if ( fNew )
     {
@@ -2373,8 +2416,8 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, in
                 if ( status == 0 )
                     printf( "Abc_NtkDarSeqSim(): Counter-example verification has FAILED.\n" );
             }
-            FREE( pNtk->pModel );
-            FREE( pNtk->pSeqModel );
+            ABC_FREE( pNtk->pModel );
+            ABC_FREE( pNtk->pSeqModel );
             pNtk->pSeqModel = pCex; pMan->pSeqModel = NULL;
             RetValue = 1;
         }
@@ -2385,6 +2428,7 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, in
                 nFrames, nWords );
         }
 */
+/*
         Fsim_ParSim_t Pars, * pPars = &Pars;
         Fsim_ManSetDefaultParamsSim( pPars );
         pPars->nWords = nWords;
@@ -2393,7 +2437,38 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, in
         pPars->fCheckMiter = fMiter;
         pPars->fVerbose = fVerbose;
         if ( Fsim_ManSimulate( pMan, pPars ) )
+        { 
+            if ( (pCex = pMan->pSeqModel) )
+            {
+                printf( "Simulation of %d frames with %d words asserted output %d in frame %d. ", 
+                    nFrames, nWords, pCex->iPo, pCex->iFrame );
+                status = Ssw_SmlRunCounterExample( pMan, (Ssw_Cex_t *)pCex );
+                if ( status == 0 )
+                    printf( "Abc_NtkDarSeqSim(): Counter-example verification has FAILED.\n" );
+            }
+            ABC_FREE( pNtk->pModel );
+            ABC_FREE( pNtk->pSeqModel );
+            pNtk->pSeqModel = pCex; pMan->pSeqModel = NULL;
+            RetValue = 1;
+        }
+        else
         {
+            RetValue = 0;
+            printf( "Simulation of %d frames with %d words did not assert the outputs. ", 
+                nFrames, nWords );
+        }
+*/ 
+        Gia_Man_t * pGia;
+        Gia_ParSim_t Pars, * pPars = &Pars;
+        Gia_ManSimSetDefaultParams( pPars );
+        pPars->nWords = nWords;
+        pPars->nIters = nFrames;
+        pPars->TimeLimit = TimeOut;
+        pPars->fCheckMiter = fMiter;
+        pPars->fVerbose = fVerbose;
+        pGia = Gia_ManFromAig( pMan );
+        if ( Gia_ManSimSimulate( pGia, pPars ) )
+        { 
             if ( (pCex = pMan->pSeqModel) )
             {
                 printf( "Simulation of %d frames with %d words asserted output %d in frame %d. ", 
@@ -2402,8 +2477,8 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, in
                 if ( status == 0 )
                     printf( "Abc_NtkDarSeqSim(): Counter-example verification has FAILED.\n" );
             }
-            FREE( pNtk->pModel );
-            FREE( pNtk->pSeqModel );
+            ABC_FREE( pNtk->pModel );
+            ABC_FREE( pNtk->pSeqModel );
             pNtk->pSeqModel = pCex; pMan->pSeqModel = NULL;
             RetValue = 1;
         }
@@ -2413,20 +2488,20 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, in
             printf( "Simulation of %d frames with %d words did not assert the outputs. ", 
                 nFrames, nWords );
         }
+        Gia_ManStop( pGia );
     }
     else
     {
-/*
         Fra_Sml_t * pSml;
-        pSml = Fra_SmlSimulateSeq( pMan, 0, nFrames, nWords );
+        pSml = Fra_SmlSimulateSeq( pMan, 0, nFrames, nWords, fMiter );
         if ( pSml->fNonConstOut )
         {
             pCex = Fra_SmlGetCounterExample( pSml );
             if ( pCex )
                 printf( "Simulation of %d frames with %d words asserted output %d in frame %d. ", 
                     nFrames, nWords, pCex->iPo, pCex->iFrame );
-            FREE( pNtk->pModel );
-            FREE( pNtk->pSeqModel );
+            ABC_FREE( pNtk->pModel );
+            ABC_FREE( pNtk->pSeqModel );
             pNtk->pSeqModel = pCex;
             RetValue = 1;
         }
@@ -2437,7 +2512,7 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, in
                 nFrames, nWords );
         }
         Fra_SmlStop( pSml );
-*/
+/*
         if ( Raig_ManSimulate( pMan, nWords, nFrames, TimeOut, fMiter, fVerbose ) )
         {
             if ( (pCex = pMan->pSeqModel) )
@@ -2448,8 +2523,8 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, in
                 if ( status == 0 )
                     printf( "Abc_NtkDarSeqSim(): Counter-example verification has FAILED.\n" );
             }
-            FREE( pNtk->pModel );
-            FREE( pNtk->pSeqModel );
+            ABC_FREE( pNtk->pModel );
+            ABC_FREE( pNtk->pSeqModel );
             pNtk->pSeqModel = pCex; pMan->pSeqModel = NULL;
             RetValue = 1;
         }
@@ -2459,8 +2534,9 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, in
             printf( "Simulation of %d frames with %d words did not assert the outputs. ", 
                 nFrames, nWords );
         }
+*/
     }
-    PRT( "Time", clock() - clk );
+    ABC_PRT( "Time", clock() - clk );
     Aig_ManStop( pMan );
     return RetValue;
 }
@@ -2549,17 +2625,17 @@ void Abc_NtkDarInduction( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fV
     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 );
     }
 }
 
@@ -2588,8 +2664,8 @@ Abc_Ntk_t * Abc_NtkDarPBAbstraction( Abc_Ntk_t * pNtk, int nFramesMax, int nConf
     pMan = Saig_ManProofAbstraction( pTemp = pMan, nFramesMax, nConfMax, fDynamic, fExtend, 0, fVerbose );
     if ( pTemp->pSeqModel )
     {
-        FREE( pNtk->pModel );
-        FREE( pNtk->pSeqModel );
+        ABC_FREE( pNtk->pModel );
+        ABC_FREE( pNtk->pSeqModel );
         pNtk->pSeqModel = pTemp->pSeqModel; pTemp->pSeqModel = NULL;
     }
     Aig_ManStop( pTemp );
@@ -2753,10 +2829,10 @@ timeInt = 0;
         Abc_NtkDelete( pNtkOn1 );
         Abc_NtkDelete( pNtkOff1 );
     }
-//    PRT( "CNF", timeCnf );
-//    PRT( "SAT", timeSat );
-//    PRT( "Int", timeInt );
-//    PRT( "Slow interpolation time", clock() - clk );
+//    ABC_PRT( "CNF", timeCnf );
+//    ABC_PRT( "SAT", timeSat );
+//    ABC_PRT( "Int", timeInt );
+//    ABC_PRT( "Slow interpolation time", clock() - clk );
 
     // return the network
     if ( !Abc_NtkCheck( pNtkInter ) )
@@ -3188,8 +3264,8 @@ void Abc_NtkDarReach( Abc_Ntk_t * pNtk, int nBddMax, int nIterMax, int fPartitio
     if ( pMan == NULL )
         return;
     Aig_ManVerifyUsingBdds( pMan, nBddMax, nIterMax, fPartition, fReorder, fVerbose, 0 );
-    FREE( pNtk->pModel );
-    FREE( pNtk->pSeqModel );
+    ABC_FREE( pNtk->pModel );
+    ABC_FREE( pNtk->pSeqModel );
     pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
     Aig_ManStop( pMan );
 }
@@ -3270,6 +3346,7 @@ Abc_Ntk_t * Amap_ManProduceNetwork( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMapping )
 ***********************************************************************/
 Abc_Ntk_t * Abc_NtkDarAmap( Abc_Ntk_t * pNtk, Amap_Par_t * pPars )
 {
+    extern Vec_Ptr_t * Amap_ManTest( Aig_Man_t * pAig, Amap_Par_t * pPars );
     Vec_Ptr_t * vMapping;
     Abc_Ntk_t * pNtkAig = NULL;
     Aig_Man_t * pMan;
@@ -3314,7 +3391,7 @@ Abc_Ntk_t * Abc_NtkDarAmap( Abc_Ntk_t * pNtk, Amap_Par_t * pPars )
 ***********************************************************************/
 void Abc_NtkDarTest( Abc_Ntk_t * pNtk )
 {
-    extern void Fsim_ManTest( Aig_Man_t * pAig );
+//    extern void Fsim_ManTest( Aig_Man_t * pAig );
     extern Vec_Int_t * Saig_StrSimPerformMatching( Aig_Man_t * p0, Aig_Man_t * p1, int nDist, int fVerbose, Aig_Man_t ** ppMiter );
 //    Vec_Int_t * vPairs;
     Aig_Man_t * pMan;//, * pMan2;//, * pTemp;
@@ -3347,7 +3424,7 @@ Aig_ManPrintStats( pMan );
 
 //    Saig_MvManSimulate( pMan, 1 );
 
-    Fsim_ManTest( pMan );
+//    Fsim_ManTest( pMan );
     Aig_ManStop( pMan );
 
 }
@@ -3365,7 +3442,7 @@ Aig_ManPrintStats( pMan );
 ***********************************************************************/
 Abc_Ntk_t * Abc_NtkDarTestNtk( Abc_Ntk_t * pNtk )
 {
-    extern Aig_Man_t * Saig_ManDualRail( Aig_Man_t * p, int fMiter );
+//    extern Aig_Man_t * Saig_ManDualRail( Aig_Man_t * p, int fMiter );
 
 /*
     extern Aig_Man_t * Ssw_SignalCorrespondeceTestPairs( Aig_Man_t * pAig );
@@ -3390,7 +3467,7 @@ Abc_Ntk_t * Abc_NtkDarTestNtk( Abc_Ntk_t * pNtk )
     return pNtkAig;
 */
     Abc_Ntk_t * pNtkAig;
-    Aig_Man_t * pMan, * pTemp;
+    Aig_Man_t * pMan;//, * pTemp;
     assert( Abc_NtkIsStrash(pNtk) );
     pMan = Abc_NtkToDar( pNtk, 0, 1 );
     if ( pMan == NULL )
@@ -3402,7 +3479,7 @@ Abc_Ntk_t * Abc_NtkDarTestNtk( Abc_Ntk_t * pNtk )
     if ( pMan == NULL )
         return NULL;
 */
-
+/*
     Aig_ManSetRegNum( pMan, pMan->nRegs );
     pMan = Saig_ManDualRail( pTemp = pMan, 1 );
     Aig_ManStop( pTemp );
@@ -3413,6 +3490,12 @@ Abc_Ntk_t * Abc_NtkDarTestNtk( Abc_Ntk_t * pNtk )
     pNtkAig->pName = Extra_UtilStrsav(pNtk->pName);
     pNtkAig->pSpec = Extra_UtilStrsav(pNtk->pSpec);
     Aig_ManStop( pMan );
+*/
+
+
+    pNtkAig = Abc_NtkFromDar( pNtk, pMan );
+    Aig_ManStop( pMan );
+
     return pNtkAig;
 
 }
diff --git a/src/base/abci/abcDebug.c b/src/base/abci/abcDebug.c
index 95b95d89..6d8d9bfa 100644
--- a/src/base/abci/abcDebug.c
+++ b/src/base/abci/abcDebug.c
@@ -88,14 +88,14 @@ void Abc_NtkAutoDebug( Abc_Ntk_t * pNtk, int (*pFuncError) (Abc_Ntk_t *) )
         }
         printf( "Iter %6d : Latches = %6d. Nodes = %6d. Steps = %6d. Error step = %3d.  ", 
             nIter, Abc_NtkLatchNum(pNtk), Abc_NtkNodeNum(pNtk), nSteps, i );
-        PRT( "Time", clock() - clk );
+        ABC_PRT( "Time", clock() - clk );
         if ( i == nSteps ) // could not modify it while preserving the bug
             break;
     }
     // write out the final network
     Io_WriteBlifLogic( pNtk, pFileName, 1 );
     printf( "Final network written into file \"%s\". ", pFileName );
-    PRT( "Total time", clock() - clkTotal );
+    ABC_PRT( "Total time", clock() - clkTotal );
     Abc_NtkDelete( pNtk );
 }
 
diff --git a/src/base/abci/abcDelay.c b/src/base/abci/abcDelay.c
index 847c7f1b..203b076f 100644
--- a/src/base/abci/abcDelay.c
+++ b/src/base/abci/abcDelay.c
@@ -117,8 +117,8 @@ float Abc_NtkDelayTraceLut( Abc_Ntk_t * pNtk, int fUseLutLib )
     }
 
     // initialize the arrival times
-    FREE( pNtk->pLutTimes );
-    pNtk->pLutTimes = ALLOC( float, 3 * Abc_NtkObjNumMax(pNtk) );
+    ABC_FREE( pNtk->pLutTimes );
+    pNtk->pLutTimes = ABC_ALLOC( float, 3 * Abc_NtkObjNumMax(pNtk) );
     for ( i = 0; i < Abc_NtkObjNumMax(pNtk); i++ )
     {
         pNtk->pLutTimes[3*i+0] = pNtk->pLutTimes[3*i+2] = 0;
@@ -255,7 +255,7 @@ void Abc_NtkDelayTracePrint( Abc_Ntk_t * pNtk, int fUseLutLib, int fVerbose )
     }
     // decide how many steps
     nSteps = fUseLutLib ? 20 : Abc_NtkLevel(pNtk);
-    pCounters = ALLOC( int, nSteps + 1 );
+    pCounters = ABC_ALLOC( int, nSteps + 1 );
     memset( pCounters, 0, sizeof(int)*(nSteps + 1) );
     // perform delay trace
     tArrival = Abc_NtkDelayTraceLut( pNtk, fUseLutLib );
@@ -278,7 +278,7 @@ void Abc_NtkDelayTracePrint( Abc_Ntk_t * pNtk, int fUseLutLib, int fVerbose )
         printf( "%3d %s : %5d  (%6.2f %%)\n", fUseLutLib? 5*(i+1) : i+1, 
             fUseLutLib? "%":"lev", Nodes, 100.0*Nodes/Abc_NtkNodeNum(pNtk) );
     }
-    free( pCounters );
+    ABC_FREE( pCounters );
 }
 
 /**Function*************************************************************
@@ -527,7 +527,7 @@ Abc_Ntk_t * Abc_NtkSpeedup( Abc_Ntk_t * pNtk, int fUseLutLib, int Percentage, in
         printf( "\n" );
     }
     // mark the timing critical nodes and edges
-    puTCEdges = ALLOC( unsigned, Abc_NtkObjNumMax(pNtk) );
+    puTCEdges = ABC_ALLOC( unsigned, Abc_NtkObjNumMax(pNtk) );
     memset( puTCEdges, 0, sizeof(unsigned) * Abc_NtkObjNumMax(pNtk) );
     Abc_NtkForEachNode( pNtk, pNode, i )
     {
@@ -636,7 +636,7 @@ Abc_Ntk_t * Abc_NtkSpeedup( Abc_Ntk_t * pNtk, int fUseLutLib, int Percentage, in
     }
     Vec_PtrFree( vTimeCries );
     Vec_PtrFree( vTimeFanins );
-    free( puTCEdges );
+    ABC_FREE( puTCEdges );
     if ( fVerbose )
         printf( "Nodes: Total = %7d. 0-slack = %7d. Workable = %7d. Ratio = %4.2f\n", 
             Abc_NtkNodeNum(pNtk), Counter, CounterRes, 1.0*CounterRes/Counter ); 
@@ -691,7 +691,7 @@ Vec_Int_t * Abc_NtkPowerEstimate( Abc_Ntk_t * pNtk, int fProbOne )
     pSwitching = (float *)vSwitching->pArray;
     Abc_NtkForEachObj( pNtk, pObjAbc, i )
     {
-        if ( (pObjAbc2 = Abc_ObjRegular(pObjAbc->pTemp)) && (pObjAig = pObjAbc2->pTemp) )
+        if ( (pObjAbc2 = Abc_ObjRegular(pObjAbc->pTemp)) && (pObjAig = Aig_Regular(pObjAbc2->pTemp)) )
             pProbability[pObjAbc->Id] = pSwitching[pObjAig->Id];
     }
     Vec_IntFree( vSwitching );
@@ -714,8 +714,8 @@ Vec_Int_t * Abc_NtkPowerEstimate( Abc_Ntk_t * pNtk, int fProbOne )
 void Abc_NtkPowerPrint( Abc_Ntk_t * pNtk, Vec_Int_t * vProbs )
 {
     Abc_Obj_t * pObj;
-    float * pProb, TotalProb = 0.0, ProbThis, Probs[5] = {0.0};
-    int i, nNodes = 0, nEdges = 0, Counter[5] = {0};
+    float * pProb, TotalProb = 0.0, ProbThis, Probs[6] = {0.0};
+    int i, nNodes = 0, nEdges = 0, Counter[6] = {0};
     pProb = (float *)vProbs->pArray;
     assert( Vec_IntSize(vProbs) >= Abc_NtkObjNumMax(pNtk) );
     Abc_NtkForEachObj( pNtk, pObj, i )
@@ -726,8 +726,13 @@ void Abc_NtkPowerPrint( Abc_Ntk_t * pNtk, Vec_Int_t * vProbs )
         nEdges += Abc_ObjFanoutNum(pObj);
         ProbThis = pProb[i] * Abc_ObjFanoutNum(pObj);
         TotalProb += ProbThis;
-        assert( pProb[i] >= 0.0 && pProb[i] <= 0.5 );
-        if ( pProb[i] >= 0.4 )
+        assert( pProb[i] >= 0.0 && pProb[i] <= 1.0 );
+        if ( pProb[i] >= 0.5 )
+        {
+            Counter[5]++;
+            Probs[5] += ProbThis;
+        }
+        else if ( pProb[i] >= 0.4 )
         {
             Counter[4]++;
             Probs[4] += ProbThis;
@@ -754,11 +759,11 @@ void Abc_NtkPowerPrint( Abc_Ntk_t * pNtk, Vec_Int_t * vProbs )
         }
     }
     printf( "Node  distribution: " );
-    for ( i = 0; i < 5; i++ )
+    for ( i = 0; i < 6; i++ )
         printf( "n%d%d = %6.2f%%  ", i, i+1, 100.0 * Counter[i]/nNodes );
     printf( "\n" );
     printf( "Power distribution: " );
-    for ( i = 0; i < 5; i++ )
+    for ( i = 0; i < 6; i++ )
         printf( "p%d%d = %6.2f%%  ", i, i+1, 100.0 * Probs[i]/TotalProb );
     printf( "\n" );
     printf( "Total probs = %7.2f. ", TotalProb );
@@ -819,7 +824,7 @@ Abc_Ntk_t * Abc_NtkPowerdown( Abc_Ntk_t * pNtk, int fUseLutLib, int Percentage,
     if ( fVerbose )
         Abc_NtkPowerPrint( pNtk, vProbs );
     // mark the power critical nodes and edges
-    puPCEdges = ALLOC( unsigned, Abc_NtkObjNumMax(pNtk) );
+    puPCEdges = ABC_ALLOC( unsigned, Abc_NtkObjNumMax(pNtk) );
     memset( puPCEdges, 0, sizeof(unsigned) * Abc_NtkObjNumMax(pNtk) );
     Abc_NtkForEachNode( pNtk, pNode, i )
     {
@@ -931,7 +936,7 @@ Abc_Ntk_t * Abc_NtkPowerdown( Abc_Ntk_t * pNtk, int fUseLutLib, int Percentage,
     }
     Vec_PtrFree( vTimeCries );
     Vec_PtrFree( vTimeFanins );
-    free( puPCEdges );
+    ABC_FREE( puPCEdges );
     if ( fVerbose )
         printf( "Nodes: Total = %7d. Power-critical = %7d. Workable = %7d. Ratio = %4.2f\n", 
             Abc_NtkNodeNum(pNtk), Counter, CounterRes, 1.0*CounterRes/Counter ); 
diff --git a/src/base/abci/abcDsd.c b/src/base/abci/abcDsd.c
index ab6279b6..7f3d2071 100644
--- a/src/base/abci/abcDsd.c
+++ b/src/base/abci/abcDsd.c
@@ -133,8 +133,8 @@ Abc_Ntk_t * Abc_NtkDsdInternal( Abc_Ntk_t * pNtk, bool fVerbose, bool fPrint, bo
         ppNamesCi = Abc_NtkCollectCioNames( pNtk, 0 );
         ppNamesCo = Abc_NtkCollectCioNames( pNtk, 1 );
         Dsd_TreePrint( stdout, pManDsd, ppNamesCi, ppNamesCo, fShort, -1 );
-        free( ppNamesCi );
-        free( ppNamesCo );
+        ABC_FREE( ppNamesCi );
+        ABC_FREE( ppNamesCo );
     }
 
     // stop the DSD manager
@@ -161,18 +161,18 @@ void Abc_NtkDsdConstruct( Dsd_Manager_t * pManDsd, Abc_Ntk_t * pNtk, Abc_Ntk_t *
     int i, nNodesDsd;
 
     // save the CI nodes in the DSD nodes
-    Dsd_NodeSetMark( Dsd_ManagerReadConst1(pManDsd), (int)(PORT_PTRINT_T)Abc_NtkCreateNodeConst1(pNtkNew) );
+    Dsd_NodeSetMark( Dsd_ManagerReadConst1(pManDsd), (int)(ABC_PTRINT_T)Abc_NtkCreateNodeConst1(pNtkNew) );
     Abc_NtkForEachCi( pNtk, pNode, i )
     {
         pNodeDsd = Dsd_ManagerReadInput( pManDsd, i );
-        Dsd_NodeSetMark( pNodeDsd, (int)(PORT_PTRINT_T)pNode->pCopy );
+        Dsd_NodeSetMark( pNodeDsd, (int)(ABC_PTRINT_T)pNode->pCopy );
     }
 
     // collect DSD nodes in DFS order (leaves and const1 are not collected)
     ppNodesDsd = Dsd_TreeCollectNodesDfs( pManDsd, &nNodesDsd );
     for ( i = 0; i < nNodesDsd; i++ )
         Abc_NtkDsdConstructNode( pManDsd, ppNodesDsd[i], pNtkNew, NULL );
-    free( ppNodesDsd );
+    ABC_FREE( ppNodesDsd );
 
     // set the pointers to the CO drivers
     Abc_NtkForEachCo( pNtk, pNode, i )
@@ -183,7 +183,7 @@ void Abc_NtkDsdConstruct( Dsd_Manager_t * pManDsd, Abc_Ntk_t * pNtk, Abc_Ntk_t *
         if ( !Abc_AigNodeIsAnd(pDriver) )
             continue;
         pNodeDsd = Dsd_ManagerReadRoot( pManDsd, i );
-        pNodeNew = (Abc_Obj_t *)(PORT_PTRINT_T)Dsd_NodeReadMark( Dsd_Regular(pNodeDsd) );
+        pNodeNew = (Abc_Obj_t *)(ABC_PTRINT_T)Dsd_NodeReadMark( Dsd_Regular(pNodeDsd) );
         assert( !Abc_ObjIsComplement(pNodeNew) );
         pDriver->pCopy = Abc_ObjNotCond( pNodeNew, Dsd_IsComplement(pNodeDsd) );
     }
@@ -219,7 +219,7 @@ Abc_Obj_t * Abc_NtkDsdConstructNode( Dsd_Manager_t * pManDsd, Dsd_Node_t * pNode
     for ( i = 0; i < nDecs; i++ )
     {
         pFaninDsd  = Dsd_NodeReadDec( pNodeDsd, i );
-        pFanin     = (Abc_Obj_t *)(PORT_PTRINT_T)Dsd_NodeReadMark(Dsd_Regular(pFaninDsd));
+        pFanin     = (Abc_Obj_t *)(ABC_PTRINT_T)Dsd_NodeReadMark(Dsd_Regular(pFaninDsd));
         Abc_ObjAddFanin( pNodeNew, pFanin );
         assert( Type == DSD_NODE_OR || !Dsd_IsComplement(pFaninDsd) );
     }
@@ -284,7 +284,7 @@ printf( "\n" );
         }
     }
     pNodeNew->pData = bLocal;
-    Dsd_NodeSetMark( pNodeDsd, (int)(PORT_PTRINT_T)pNodeNew );
+    Dsd_NodeSetMark( pNodeDsd, (int)(ABC_PTRINT_T)pNodeNew );
     return pNodeNew;
 }
 
@@ -400,7 +400,7 @@ void Abc_NodeDecompDsdAndMux( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes, Dsd_Manager
         Abc_ObjForEachFanin( pNode, pFanin, i )
         {
             pFaninDsd = Dsd_ManagerReadInput( pManDsd, i );
-            Dsd_NodeSetMark( pFaninDsd, (int)(PORT_PTRINT_T)pFanin );
+            Dsd_NodeSetMark( pFaninDsd, (int)(ABC_PTRINT_T)pFanin );
         }
 
         // construct the intermediate nodes
@@ -411,7 +411,7 @@ void Abc_NodeDecompDsdAndMux( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes, Dsd_Manager
             if ( Abc_NodeIsForDsd(pRoot) && fRecursive )
                 Vec_PtrPush( vNodes, pRoot );
         }
-        free( ppNodesDsd );
+        ABC_FREE( ppNodesDsd );
         assert(pRoot);
 
         // remove the current fanins
diff --git a/src/base/abci/abcFraig.c b/src/base/abci/abcFraig.c
index d3cbaccb..1db939b2 100644
--- a/src/base/abci/abcFraig.c
+++ b/src/base/abci/abcFraig.c
@@ -185,7 +185,7 @@ Fraig_Node_t * Abc_NtkToFraigExdc( Fraig_Man_t * pMan, Abc_Ntk_t * pNtkMain, Abc
             }
         assert( pObj->pCopy != NULL );
     }
-    free( ppNames );
+    ABC_FREE( ppNames );
     // build FRAIG for each node
     Abc_AigForEachAnd( pNtkStrash, pObj, i )
         pObj->pCopy = (Abc_Obj_t *)Fraig_NodeAnd( pMan, 
@@ -742,7 +742,7 @@ Abc_Ntk_t * Abc_NtkFraigRestore()
     // perform partitioned computation of structural choices
     pFraig = Abc_NtkFraigPartitioned( vStore, &Params );
     Abc_NtkFraigStoreClean();
-//PRT( "Total choicing time", clock() - clk );
+//ABC_PRT( "Total choicing time", clock() - clk );
     return pFraig;
 }
 
diff --git a/src/base/abci/abcFxu.c b/src/base/abci/abcFxu.c
index 45515dd1..850a6e24 100644
--- a/src/base/abci/abcFxu.c
+++ b/src/base/abci/abcFxu.c
@@ -54,9 +54,9 @@ bool Abc_NtkFastExtract( Abc_Ntk_t * pNtk, Fxu_Data_t * p )
 {
     assert( Abc_NtkIsLogic(pNtk) );
     // if the network is already in the SOP form, it may come from BLIF file
-    // and it may not be SCC-free, in which case FXU will not work correctly
+    // and it may not be SCC-ABC_FREE, in which case FXU will not work correctly
     if ( Abc_NtkIsSopLogic(pNtk) )
-    { // to make sure the SOPs are SCC-free
+    { // to make sure the SOPs are SCC-ABC_FREE
 //        Abc_NtkSopToBdd(pNtk);
 //        Abc_NtkBddToSop(pNtk);
     }
@@ -177,17 +177,17 @@ void Abc_NtkFxuCollectInfo( Abc_Ntk_t * pNtk, Fxu_Data_t * p )
 void Abc_NtkFxuFreeInfo( Fxu_Data_t * p )
 {
     int i;
-    // free the arrays of new fanins
+    // ABC_FREE the arrays of new fanins
     if ( p->vFaninsNew )
         for ( i = 0; i < p->vFaninsNew->nSize; i++ )
             if ( p->vFaninsNew->pArray[i] )
                 Vec_IntFree( p->vFaninsNew->pArray[i] );
-    // free the arrays
+    // ABC_FREE the arrays
     if ( p->vSops      ) Vec_PtrFree( p->vSops      );
     if ( p->vSopsNew   ) Vec_PtrFree( p->vSopsNew   );
     if ( p->vFanins    ) Vec_PtrFree( p->vFanins    );
     if ( p->vFaninsNew ) Vec_PtrFree( p->vFaninsNew );
-    FREE( p );
+    ABC_FREE( p );
 }
 
 /**Function*************************************************************
diff --git a/src/base/abci/abcHaig.c b/src/base/abci/abcHaig.c
index d3513bbe..569275f2 100644
--- a/src/base/abci/abcHaig.c
+++ b/src/base/abci/abcHaig.c
@@ -28,6 +28,8 @@
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
+#if 0
+
 /**Function*************************************************************
 
   Synopsis    [Start history AIG.]
@@ -148,6 +150,7 @@ void Abc_NtkHaigTranfer( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtkNew )
 }
 
 
+#endif
 
 /**Function*************************************************************
 
@@ -636,6 +639,8 @@ int Abc_NtkHaigResetReprs( Hop_Man_t * p )
     return nFanouts;
 }
 
+#if 0
+
 /**Function*************************************************************
 
   Synopsis    [Stops history AIG.]
@@ -686,10 +691,12 @@ Abc_Ntk_t * Abc_NtkHaigUse( Abc_Ntk_t * pNtk )
     pNtkAig = Abc_NtkHaigRecreateAig( pNtk, pMan );
     Hop_ManStop( pMan );
 
-    // free HAIG
+    // ABC_FREE HAIG
     return pNtkAig;
 }
 
+#endif
+
 /**Function*************************************************************
 
   Synopsis    [Transform HOP manager into the one without loops.]
diff --git a/src/base/abci/abcIf.c b/src/base/abci/abcIf.c
index c5d9ada7..facf06bc 100644
--- a/src/base/abci/abcIf.c
+++ b/src/base/abci/abcIf.c
@@ -89,7 +89,7 @@ void Abc_NtkIfComputeSwitching( Abc_Ntk_t * pNtk, If_Man_t * pIfMan )
             pSwitching[i] = pObjAbc->dTemp;
 if ( pIfMan->pPars->fVerbose )
 {
-    PRT( "Computing switching activity", clock() - clk );
+    ABC_PRT( "Computing switching activity", clock() - clk );
 }
 }
 
@@ -509,8 +509,8 @@ Hop_Obj_t * Abc_NodeIfToHop( Hop_Man_t * pHopMan, If_Man_t * pIfMan, If_Obj_t *
 ***********************************************************************/
 int Abc_ObjCompareFlow( Abc_Obj_t ** ppNode0, Abc_Obj_t ** ppNode1 )
 {
-    float Flow0 = Abc_Int2Float((int)(PORT_PTRINT_T)(*ppNode0)->pCopy);
-    float Flow1 = Abc_Int2Float((int)(PORT_PTRINT_T)(*ppNode1)->pCopy);
+    float Flow0 = Abc_Int2Float((int)(ABC_PTRINT_T)(*ppNode0)->pCopy);
+    float Flow1 = Abc_Int2Float((int)(ABC_PTRINT_T)(*ppNode1)->pCopy);
     if ( Flow0 > Flow1 )
         return -1;
     if ( Flow0 < Flow1 )
@@ -573,9 +573,9 @@ Vec_Ptr_t * Abc_NtkFindGoodOrder( Abc_Ntk_t * pNtk )
     {
         pFanin0 = Abc_ObjFanin0(pNode);
         pFanin1 = Abc_ObjFanin1(pNode);
-        Flow0 = Abc_Int2Float((int)(PORT_PTRINT_T)pFanin0->pCopy)/Abc_ObjFanoutNum(pFanin0);
-        Flow1 = Abc_Int2Float((int)(PORT_PTRINT_T)pFanin1->pCopy)/Abc_ObjFanoutNum(pFanin1);
-        pNode->pCopy = (Abc_Obj_t *)(PORT_PTRINT_T)Abc_Float2Int(Flow0 + Flow1+(float)1.0);
+        Flow0 = Abc_Int2Float((int)(ABC_PTRINT_T)pFanin0->pCopy)/Abc_ObjFanoutNum(pFanin0);
+        Flow1 = Abc_Int2Float((int)(ABC_PTRINT_T)pFanin1->pCopy)/Abc_ObjFanoutNum(pFanin1);
+        pNode->pCopy = (Abc_Obj_t *)(ABC_PTRINT_T)Abc_Float2Int(Flow0 + Flow1+(float)1.0);
     }
     // find the flow of the COs
     vCos = Vec_PtrAlloc( Abc_NtkCoNum(pNtk) );
@@ -592,7 +592,7 @@ Vec_Ptr_t * Abc_NtkFindGoodOrder( Abc_Ntk_t * pNtk )
     // verify sorting
     pFanin0 = Vec_PtrEntry(vCos, 0);
     pFanin1 = Vec_PtrEntryLast(vCos);
-    assert( Abc_Int2Float((int)(PORT_PTRINT_T)pFanin0->pCopy) >= Abc_Int2Float((int)(PORT_PTRINT_T)pFanin1->pCopy) );
+    assert( Abc_Int2Float((int)(ABC_PTRINT_T)pFanin0->pCopy) >= Abc_Int2Float((int)(ABC_PTRINT_T)pFanin1->pCopy) );
 
     // collect the nodes in the topological order from the new array
     Abc_NtkIncrementTravId( pNtk );
diff --git a/src/base/abci/abcIvy.c b/src/base/abci/abcIvy.c
index 96d8196e..c7fa5a1e 100644
--- a/src/base/abci/abcIvy.c
+++ b/src/base/abci/abcIvy.c
@@ -216,13 +216,13 @@ clk = clock();
     Ivy_ManRewriteSeq( pMan, 1, 0 );
 //printf( "%d ", Ivy_ManNodeNum(pMan) );
 //printf( "%d ", Ivy_ManNodeNum(pMan->pHaig) );
-//PRT( " ", clock() - clk );
+//ABC_PRT( " ", clock() - clk );
 //printf( "\n" );
 /*
     printf( "Moves = %d.  ", nMoves );
     printf( "MovesS = %d.  ", nMovesS );
     printf( "Clauses = %d.  ", nClauses );
-    PRT( "Time", timeInv );
+    ABC_PRT( "Time", timeInv );
 */
 //    Ivy_ManRewriteSeq( pMan, 1, 0 );
 //printf( "Haig size = %d.\n", Ivy_ManNodeNum(pMan->pHaig) );
@@ -510,13 +510,13 @@ int Abc_NtkIvyProve( Abc_Ntk_t ** ppNtk, void * pPars )
     pFanin = Abc_ObjFanin0(pObj);
     if ( Abc_ObjFanin0(pObj)->fPhase != (unsigned)Abc_ObjFaninC0(pObj) )
     {
-        pNtk->pModel = ALLOC( int, Abc_NtkPiNum(pNtk) );
+        pNtk->pModel = ABC_ALLOC( int, Abc_NtkPiNum(pNtk) );
         memset( pNtk->pModel, 0, sizeof(int) * Abc_NtkPiNum(pNtk) );
         return 0;
     }
 
     // if SAT only, solve without iteration
-    RetValue = Abc_NtkMiterSat( pNtk, 2*(sint64)pParams->nMiteringLimitStart, (sint64)0, 0, NULL, NULL );
+    RetValue = Abc_NtkMiterSat( pNtk, 2*(ABC_INT64_T)pParams->nMiteringLimitStart, (ABC_INT64_T)0, 0, NULL, NULL );
     if ( RetValue >= 0 )
         return RetValue;
 
@@ -534,7 +534,7 @@ int Abc_NtkIvyProve( Abc_Ntk_t ** ppNtk, void * pPars )
         Abc_NtkRewrite( pNtk, 0, 0, 0, 0, 0 );
         Abc_NtkRefactor( pNtk, 10, 16, 0, 0, 0, 0 );
 //printf( "After rwsat = %d. ", Abc_NtkNodeNum(pNtk) );
-//PRT( "Time", clock() - clk );
+//ABC_PRT( "Time", clock() - clk );
     }
 
     // convert ABC network into IVY network
@@ -672,13 +672,13 @@ Abc_Ntk_t * Abc_NtkIvy( Abc_Ntk_t * pNtk )
     // make sure everything is okay
     if ( !Abc_NtkCheck( pNtkAig ) )
     {
-        FREE( pInit );
+        ABC_FREE( pInit );
         printf( "Abc_NtkStrash: The network check has failed.\n" );
         Abc_NtkDelete( pNtkAig );
         return NULL;
     }
 
-    FREE( pInit );
+    ABC_FREE( pInit );
     return pNtkAig;
 */
 }
diff --git a/src/base/abci/abcLut.c b/src/base/abci/abcLut.c
index 4203a425..bb45f6c4 100644
--- a/src/base/abci/abcLut.c
+++ b/src/base/abci/abcLut.c
@@ -286,7 +286,7 @@ Abc_ManScl_t * Abc_ManSclStart( int nLutSize, int nCutSizeMax, int nNodesMax )
     Abc_ManScl_t * p;
     int i, k;
     assert( sizeof(unsigned) == 4 );
-    p = ALLOC( Abc_ManScl_t, 1 );
+    p = ABC_ALLOC( Abc_ManScl_t, 1 );
     memset( p, 0, sizeof(Abc_ManScl_t) );
     p->nLutSize    = nLutSize;
     p->nCutSizeMax = nCutSizeMax;
@@ -321,10 +321,10 @@ Abc_ManScl_t * Abc_ManSclStart( int nLutSize, int nCutSizeMax, int nNodesMax )
 void Abc_ManSclStop( Abc_ManScl_t * p )
 {
 //    Vec_IntFree( p->vBound );
-    free( p->uVars );
-    free( p->uSims );
-    free( p->uCofs );
-    free( p );
+    ABC_FREE( p->uVars );
+    ABC_FREE( p->uSims );
+    ABC_FREE( p->uCofs );
+    ABC_FREE( p );
 }
 
 
diff --git a/src/base/abci/abcMap.c b/src/base/abci/abcMap.c
index 3a454fc0..c4a68cc7 100644
--- a/src/base/abci/abcMap.c
+++ b/src/base/abci/abcMap.c
@@ -117,7 +117,7 @@ clk = clock();
         pNtkNew->pExdc = Abc_NtkDup( pNtk->pExdc );
 if ( fVerbose )
 {
-PRT( "Total runtime", clock() - clkTotal );
+ABC_PRT( "Total runtime", clock() - clkTotal );
 }
 
     // make sure that everything is okay
diff --git a/src/base/abci/abcMeasure.c b/src/base/abci/abcMeasure.c
index 6604a0c4..00d5d971 100644
--- a/src/base/abci/abcMeasure.c
+++ b/src/base/abci/abcMeasure.c
@@ -244,8 +244,8 @@ void Abc_Ntk4VarTable( Abc_Ntk_t * pNtk )
 //        Counters[ puMap[uTruth & 0xFFFF] ]++;
         Vec_PtrFree( vNodes );
     }
-    free( puCanons );
-    free( puMap );
+    ABC_FREE( puCanons );
+    ABC_FREE( puMap );
 
     Count = 0;
     for ( k = 0; k < 222; k++ )
diff --git a/src/base/abci/abcMerge.c b/src/base/abci/abcMerge.c
index 25a4f02e..4997af48 100644
--- a/src/base/abci/abcMerge.c
+++ b/src/base/abci/abcMerge.c
@@ -322,7 +322,7 @@ Vec_Int_t * Abc_NtkLutMerge( Abc_Ntk_t * pNtk, Nwk_LMPars_t * pPars )
     if ( pPars->fVerbose )
     {
         printf( "Mergable LUTs = %6d. Total cands = %6d. ", p->nVertsMax, nCands );
-        PRT( "Deriving graph", clock() - clk );
+        ABC_PRT( "Deriving graph", clock() - clk );
     }
     // solve the graph problem
     clk = clock();
@@ -331,7 +331,7 @@ Vec_Int_t * Abc_NtkLutMerge( Abc_Ntk_t * pNtk, Nwk_LMPars_t * pPars )
     {
         printf( "GRAPH: Nodes = %6d. Edges = %6d.  Pairs = %6d.  ", 
             p->nVerts, p->nEdges, Vec_IntSize(p->vPairs)/2 );
-        PRT( "Solving", clock() - clk );
+        ABC_PRT( "Solving", clock() - clk );
         Nwk_ManGraphReportMemoryUsage( p );
     }
     vResult = p->vPairs; p->vPairs = NULL;
diff --git a/src/base/abci/abcMiter.c b/src/base/abci/abcMiter.c
index 4e1022b8..34270fab 100644
--- a/src/base/abci/abcMiter.c
+++ b/src/base/abci/abcMiter.c
@@ -805,7 +805,7 @@ Abc_Ntk_t * Abc_NtkFrames( Abc_Ntk_t * pNtk, int nFrames, int fInitial, int fVer
                 pLatchOut->pCopy = Abc_ObjNotCond( Abc_AigConst1(pNtkFrames), Abc_LatchIsInit0(pLatch) );
         }
         if ( Counter )
-            printf( "Warning: %d uninitialized latches are replaced by free PI variables.\n", Counter );
+            printf( "Warning: %d uninitialized latches are replaced by ABC_FREE PI variables.\n", Counter );
     }
     
     // create the timeframes
@@ -939,7 +939,7 @@ Abc_Ntk_t * Abc_NtkFrames2( Abc_Ntk_t * pNtk, int nFrames, int fInitial, AddFram
             if (addFrameMapping) addFrameMapping(pLatch->pCopy, pLatch, 0, arg);
         }
         if ( Counter )
-            printf( "Warning: %d uninitialized latches are replaced by free PI variables.\n", Counter );
+            printf( "Warning: %d uninitialized latches are replaced by ABC_FREE PI variables.\n", Counter );
     }
     
     // create the timeframes
diff --git a/src/base/abci/abcMv.c b/src/base/abci/abcMv.c
index 2858b8a7..dacd16b2 100644
--- a/src/base/abci/abcMv.c
+++ b/src/base/abci/abcMv.c
@@ -60,7 +60,7 @@ void Abc_MvExperiment()
 {
     Mv_Man_t * p;
     // get the functions
-    p = ALLOC( Mv_Man_t, 1 );
+    p = ABC_ALLOC( Mv_Man_t, 1 );
     memset( p, 0, sizeof(Mv_Man_t) );
     p->dd = Cudd_Init( 32, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
     p->nFuncs  = 15;
@@ -76,7 +76,7 @@ void Abc_MvExperiment()
     // remove the manager
     Abc_MvDeref( p );
     Extra_StopManager( p->dd );
-    free( p );
+    ABC_FREE( p );
 }
 
 /**Function*************************************************************
@@ -349,7 +349,7 @@ void Abc_MvDecompose( Mv_Man_t * p )
             printf( "%d ", Vec_PtrSize(vCofs) );
             Vec_PtrFree( vCofs );
 
-            // free the cofactors
+            // ABC_FREE the cofactors
             for ( v1 = 0; v1 < 4; v1++ )
             for ( v2 = 0; v2 < 4; v2++ )
                 Cudd_RecursiveDeref( p->dd, bCofs[v1 * 4 + v2] );
diff --git a/src/base/abci/abcNtbdd.c b/src/base/abci/abcNtbdd.c
index ed02f589..62256997 100644
--- a/src/base/abci/abcNtbdd.c
+++ b/src/base/abci/abcNtbdd.c
@@ -582,7 +582,7 @@ clk = clock();
     printf( "The BDD before = %d.\n", Cudd_DagSize(bSum) );
     Cudd_ReduceHeap( dd, CUDD_REORDER_SIFT, 1 );
     printf( "The BDD after  = %d.\n", Cudd_DagSize(bSum) );
-PRT( "Time", clock() - clk );
+ABC_PRT( "Time", clock() - clk );
     Cudd_RecursiveDeref( dd, bSum );
     Cudd_Quit( dd );
 }
diff --git a/src/base/abci/abcOdc.c b/src/base/abci/abcOdc.c
index 989d551f..67b243b9 100644
--- a/src/base/abci/abcOdc.c
+++ b/src/base/abci/abcOdc.c
@@ -168,7 +168,7 @@ Odc_Man_t * Abc_NtkDontCareAlloc( int nVarsMax, int nLevels, int fVerbose, int f
     Odc_Man_t * p;
     unsigned * pData;
     int i, k;
-    p = ALLOC( Odc_Man_t, 1 );
+    p = ABC_ALLOC( Odc_Man_t, 1 );
     memset( p, 0, sizeof(Odc_Man_t) );
     assert( nVarsMax > 4 && nVarsMax < 16 );
     assert( nLevels > 0 && nLevels < 10 );
@@ -189,7 +189,7 @@ Odc_Man_t * Abc_NtkDontCareAlloc( int nVarsMax, int nLevels, int fVerbose, int f
     // internal AIG package
     // allocate room for objects
     p->nObjsAlloc = ABC_DC_MAX_NODES; 
-    p->pObjs = ALLOC( Odc_Obj_t, p->nObjsAlloc * sizeof(Odc_Obj_t) );
+    p->pObjs = ABC_ALLOC( Odc_Obj_t, p->nObjsAlloc * sizeof(Odc_Obj_t) );
     p->nPis  = nVarsMax + 32;
     p->nObjs = 1 + p->nPis;
     memset( p->pObjs, 0, p->nObjs * sizeof(Odc_Obj_t) );
@@ -198,7 +198,7 @@ Odc_Man_t * Abc_NtkDontCareAlloc( int nVarsMax, int nLevels, int fVerbose, int f
         p->pObjs[1 + p->nVarsMax + i].uMask = (1 << i);
     // allocate hash table
     p->nTableSize = p->nObjsAlloc/3 + 1;
-    p->pTable = ALLOC( Odc_Lit_t, p->nTableSize * sizeof(Odc_Lit_t) );
+    p->pTable = ABC_ALLOC( Odc_Lit_t, p->nTableSize * sizeof(Odc_Lit_t) );
     memset( p->pTable, 0, p->nTableSize * sizeof(Odc_Lit_t) );
     p->vUsedSpots = Vec_IntAlloc( 1000 );
 
@@ -284,23 +284,23 @@ void Abc_NtkDontCareFree( Odc_Man_t * p )
         printf( "Ave DCs per window = %6.2f %%. Ave DCs per finished window = %6.2f %%.\n", 
             1.0*p->nTotalDcs/p->nWins, 1.0*p->nTotalDcs/p->nWinsFinish );
         printf( "Runtime stats of the ODC manager:\n" );
-        PRT( "Cleaning    ", p->timeClean );
-        PRT( "Windowing   ", p->timeWin   );
-        PRT( "Miter       ", p->timeMiter );
-        PRT( "Simulation  ", p->timeSim   );
-        PRT( "Quantifying ", p->timeQuant );
-        PRT( "Truth table ", p->timeTruth );
-        PRT( "TOTAL       ", p->timeTotal );
-        PRT( "Aborted     ", p->timeAbort );
+        ABC_PRT( "Cleaning    ", p->timeClean );
+        ABC_PRT( "Windowing   ", p->timeWin   );
+        ABC_PRT( "Miter       ", p->timeMiter );
+        ABC_PRT( "Simulation  ", p->timeSim   );
+        ABC_PRT( "Quantifying ", p->timeQuant );
+        ABC_PRT( "Truth table ", p->timeTruth );
+        ABC_PRT( "TOTAL       ", p->timeTotal );
+        ABC_PRT( "Aborted     ", p->timeAbort );
     }
     Vec_PtrFree( p->vRoots );
     Vec_PtrFree( p->vBranches );
     Vec_PtrFree( p->vTruths );
     Vec_PtrFree( p->vTruthsElem );
     Vec_IntFree( p->vUsedSpots );
-    free( p->pObjs );
-    free( p->pTable );
-    free( p );
+    ABC_FREE( p->pObjs );
+    ABC_FREE( p->pTable );
+    ABC_FREE( p );
 }
 
 
@@ -662,10 +662,10 @@ void * Abc_NtkDontCareTransfer_rec( Odc_Man_t * p, Abc_Obj_t * pNode, Abc_Obj_t
     assert( Abc_ObjIsNode(pNode) );
     // consider the case when the node is the pivot
     if ( pNode == pPivot )
-        return pNode->pCopy = (void *)(PORT_PTRUINT_T)((Odc_Const1() << 16) | Odc_Const0());
+        return pNode->pCopy = (void *)(ABC_PTRUINT_T)((Odc_Const1() << 16) | Odc_Const0());
     // compute the cofactors
-    uData0 = (unsigned)(PORT_PTRUINT_T)Abc_NtkDontCareTransfer_rec( p, Abc_ObjFanin0(pNode), pPivot );
-    uData1 = (unsigned)(PORT_PTRUINT_T)Abc_NtkDontCareTransfer_rec( p, Abc_ObjFanin1(pNode), pPivot );
+    uData0 = (unsigned)(ABC_PTRUINT_T)Abc_NtkDontCareTransfer_rec( p, Abc_ObjFanin0(pNode), pPivot );
+    uData1 = (unsigned)(ABC_PTRUINT_T)Abc_NtkDontCareTransfer_rec( p, Abc_ObjFanin1(pNode), pPivot );
     // find the 0-cofactor
     uLit0 = Odc_NotCond( (Odc_Lit_t)(uData0 & 0xffff), Abc_ObjFaninC0(pNode) );
     uLit1 = Odc_NotCond( (Odc_Lit_t)(uData1 & 0xffff), Abc_ObjFaninC1(pNode) );
@@ -675,7 +675,7 @@ void * Abc_NtkDontCareTransfer_rec( Odc_Man_t * p, Abc_Obj_t * pNode, Abc_Obj_t
     uLit1 = Odc_NotCond( (Odc_Lit_t)(uData1 >> 16), Abc_ObjFaninC1(pNode) );
     uRes1 = Odc_And( p, uLit0, uLit1 );
     // find the result
-    return pNode->pCopy = (void *)(PORT_PTRUINT_T)((uRes1 << 16) | uRes0);
+    return pNode->pCopy = (void *)(ABC_PTRUINT_T)((uRes1 << 16) | uRes0);
 }
 
 /**Function*************************************************************
@@ -701,21 +701,21 @@ int Abc_NtkDontCareTransfer( Odc_Man_t * p )
     Vec_PtrForEachEntry( p->vLeaves, pObj, i )
     {
         uLit = Odc_Var( p, i );
-        pObj->pCopy = (void *)(PORT_PTRUINT_T)((uLit << 16) | uLit);
+        pObj->pCopy = (void *)(ABC_PTRUINT_T)((uLit << 16) | uLit);
         Abc_NodeSetTravIdCurrent(pObj);
     }
     // set elementary variables at the branched 
     Vec_PtrForEachEntry( p->vBranches, pObj, i )
     {
         uLit = Odc_Var( p, i+p->nVarsMax );
-        pObj->pCopy = (void *)(PORT_PTRUINT_T)((uLit << 16) | uLit);
+        pObj->pCopy = (void *)(ABC_PTRUINT_T)((uLit << 16) | uLit);
         Abc_NodeSetTravIdCurrent(pObj);
     }
     // compute the AIG for the window
     p->iRoot = Odc_Const0();
     Vec_PtrForEachEntry( p->vRoots, pObj, i )
     {
-        uData = (unsigned)(PORT_PTRUINT_T)Abc_NtkDontCareTransfer_rec( p, pObj, p->pNode );
+        uData = (unsigned)(ABC_PTRUINT_T)Abc_NtkDontCareTransfer_rec( p, pObj, p->pNode );
         // get the cofactors
         uRes0 = uData & 0xffff;
         uRes1 = uData >> 16;
diff --git a/src/base/abci/abcPart.c b/src/base/abci/abcPart.c
index a482e5c9..4c348b16 100644
--- a/src/base/abci/abcPart.c
+++ b/src/base/abci/abcPart.c
@@ -29,10 +29,10 @@ struct Supp_Man_t_
 {
     int              nChunkSize;    // the size of one chunk of memory (~1 Mb)
     int              nStepSize;     // the step size in saving memory (~64 bytes)
-    char *           pFreeBuf;      // the pointer to free memory
-    int              nFreeSize;     // the size of remaining free memory
+    char *           pFreeBuf;      // the pointer to ABC_FREE memory
+    int              nFreeSize;     // the size of remaining ABC_FREE memory
     Vec_Ptr_t *      vMemory;       // the memory allocated
-    Vec_Ptr_t *      vFree;         // the vector of free pieces of memory
+    Vec_Ptr_t *      vFree;         // the vector of ABC_FREE pieces of memory
 };
 
 typedef struct Supp_One_t_     Supp_One_t;
@@ -66,7 +66,7 @@ static inline void   Supp_OneSetNext( char * pPart, char * pNext ) { *((char **)
 Supp_Man_t * Supp_ManStart( int nChunkSize, int nStepSize )
 {
     Supp_Man_t * p;
-    p = ALLOC( Supp_Man_t, 1 );
+    p = ABC_ALLOC( Supp_Man_t, 1 );
     memset( p, 0, sizeof(Supp_Man_t) );
     p->nChunkSize = nChunkSize;
     p->nStepSize  = nStepSize;
@@ -91,10 +91,10 @@ void Supp_ManStop( Supp_Man_t * p )
     void * pMemory;
     int i;
     Vec_PtrForEachEntry( p->vMemory, pMemory, i )
-        free( pMemory );
+        ABC_FREE( pMemory );
     Vec_PtrFree( p->vMemory );
     Vec_PtrFree( p->vFree );
-    free( p );
+    ABC_FREE( p );
 }
 
 /**Function*************************************************************
@@ -123,7 +123,7 @@ char * Supp_ManFetch( Supp_Man_t * p, int nSize )
     nSizeReal = p->nStepSize * Type;
     if ( p->nFreeSize < nSizeReal )
     {
-        p->pFreeBuf = ALLOC( char, p->nChunkSize );
+        p->pFreeBuf = ABC_ALLOC( char, p->nChunkSize );
         p->nFreeSize = p->nChunkSize;
         Vec_PtrPush( p->vMemory, p->pFreeBuf );
     }
@@ -321,9 +321,9 @@ Vec_Ptr_t * Abc_NtkComputeSupportsSmart( Abc_Ntk_t * pNtk )
     int i;
     // set the number of PIs/POs
     Abc_NtkForEachCi( pNtk, pObj, i )
-        pObj->pNext = (Abc_Obj_t *)(PORT_PTRINT_T)i;
+        pObj->pNext = (Abc_Obj_t *)(ABC_PTRINT_T)i;
     Abc_NtkForEachCo( pNtk, pObj, i )
-        pObj->pNext = (Abc_Obj_t *)(PORT_PTRINT_T)i;
+        pObj->pNext = (Abc_Obj_t *)(ABC_PTRINT_T)i;
     // start the support computation manager
     p = Supp_ManStart( 1 << 20, 1 << 6 );
     // consider objects in the topological order
@@ -353,7 +353,7 @@ Vec_Ptr_t * Abc_NtkComputeSupportsSmart( Abc_Ntk_t * pNtk )
             if ( Abc_ObjIsNode(Abc_ObjFanin0(pObj)) )
             {
                 vSupp = Supp_ManTransferEntry(pPart0);
-                Vec_IntPush( vSupp, (int)(PORT_PTRINT_T)pObj->pNext );
+                Vec_IntPush( vSupp, (int)(ABC_PTRINT_T)pObj->pNext );
                 Vec_PtrPush( vSupports, vSupp );
             }
             assert( pPart0->nRefs > 0 );
@@ -366,7 +366,7 @@ Vec_Ptr_t * Abc_NtkComputeSupportsSmart( Abc_Ntk_t * pNtk )
             if ( Abc_ObjFanoutNum(pObj) )
             {
                 pPart0 = (Supp_One_t *)Supp_ManFetchEntry( p, 1, Abc_ObjFanoutNum(pObj) );
-                pPart0->pOuts[ pPart0->nOuts++ ] = (int)(PORT_PTRINT_T)pObj->pNext;
+                pPart0->pOuts[ pPart0->nOuts++ ] = (int)(ABC_PTRINT_T)pObj->pNext;
                 pObj->pCopy = (Abc_Obj_t *)pPart0;
             }
             continue;
@@ -417,7 +417,7 @@ Vec_Ptr_t * Abc_NtkComputeSupportsNaive( Abc_Ntk_t * pNtk )
     int i, k;
     // set the PI numbers
     Abc_NtkForEachCi( pNtk, pObj, i )
-        pObj->pNext = (void *)(PORT_PTRINT_T)i;
+        pObj->pNext = (void *)(ABC_PTRINT_T)i;
     // save the CI numbers
     vSupports = Vec_PtrAlloc( Abc_NtkCoNum(pNtk) );
     Abc_NtkForEachCo( pNtk, pObj, i )
@@ -427,7 +427,7 @@ Vec_Ptr_t * Abc_NtkComputeSupportsNaive( Abc_Ntk_t * pNtk )
         vSupp = Abc_NtkNodeSupport( pNtk, &pObj, 1 );
         vSuppI = (Vec_Int_t *)vSupp;
         Vec_PtrForEachEntry( vSupp, pTemp, k )
-            Vec_IntWriteEntry( vSuppI, k, (int)(PORT_PTRINT_T)pTemp->pNext );
+            Vec_IntWriteEntry( vSuppI, k, (int)(ABC_PTRINT_T)pTemp->pNext );
         Vec_IntSort( vSuppI, 0 );
         // append the number of this output
         Vec_IntPush( vSuppI, i );
@@ -463,7 +463,7 @@ unsigned * Abc_NtkSuppCharStart( Vec_Int_t * vOne, int nPis )
     unsigned * pBuffer;
     int i, Entry;
     int nWords = Abc_BitWordNum(nPis);
-    pBuffer = ALLOC( unsigned, nWords );
+    pBuffer = ABC_ALLOC( unsigned, nWords );
     memset( pBuffer, 0, sizeof(unsigned) * nWords );
     Vec_IntForEachEntry( vOne, Entry, i )
     {
@@ -728,7 +728,7 @@ clk = clock();
     vSupps = Abc_NtkComputeSupportsSmart( pNtk );
 if ( fVerbose )
 {
-PRT( "Supps", clock() - clk );
+ABC_PRT( "Supps", clock() - clk );
 }
     // start char-based support representation
     vPartSuppsChar = Vec_PtrAlloc( 1000 );
@@ -782,14 +782,14 @@ timeFind += clock() - clk2;
 
     // stop char-based support representation
     Vec_PtrForEachEntry( vPartSuppsChar, vTemp, i )
-        free( vTemp );
+        ABC_FREE( vTemp );
     Vec_PtrFree( vPartSuppsChar );
 
 //printf( "\n" );
 if ( fVerbose )
 {
-PRT( "Parts", clock() - clk );
-//PRT( "Find ", timeFind );
+ABC_PRT( "Parts", clock() - clk );
+//ABC_PRT( "Find ", timeFind );
 }
 
 clk = clock();
@@ -811,7 +811,7 @@ clk = clock();
 
 if ( fVerbose )
 {
-PRT( "Comps", clock() - clk );
+ABC_PRT( "Comps", clock() - clk );
 }
     if ( fVerbose )
     printf( "Created %d partitions.\n", Vec_PtrSize(vPartsAll) );
@@ -1195,7 +1195,7 @@ void Abc_NtkFraigPartitionedTime( Abc_Ntk_t * pNtk, void * pParams )
         Abc_NtkDelete( pNtkAig );
     Vec_PtrFree( vFraigs );
     Vec_PtrFree( vOnePtr );
-    PRT( "Partitioned fraiging time", clock() - clk );
+    ABC_PRT( "Partitioned fraiging time", clock() - clk );
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c
index 0b1d8fc1..50b0c749 100644
--- a/src/base/abci/abcPrint.c
+++ b/src/base/abci/abcPrint.c
@@ -64,10 +64,10 @@ int Abc_NtkCompareAndSaveBest( Abc_Ntk_t * pNtk )
         int    nPis;   // the number of primary inputs
         int    nPos;   // the number of primary outputs
     } ParsNew, ParsBest = { 0 };
-    // free storage for the name
+    // ABC_FREE storage for the name
     if ( pNtk == NULL )
     {
-        FREE( ParsBest.pName );
+        ABC_FREE( ParsBest.pName );
         return 0;
     }
     // quit if not a logic network
@@ -86,7 +86,7 @@ int Abc_NtkCompareAndSaveBest( Abc_Ntk_t * pNtk )
          (ParsBest.Depth == ParsNew.Depth && ParsBest.Flops >  ParsNew.Flops) ||
          (ParsBest.Depth == ParsNew.Depth && ParsBest.Flops == ParsNew.Flops && ParsBest.Nodes >  ParsNew.Nodes) )
     {
-        FREE( ParsBest.pName );
+        ABC_FREE( ParsBest.pName );
         ParsBest.pName = Extra_UtilStrsav( pNtk->pName );
         ParsBest.Depth = ParsNew.Depth; 
         ParsBest.Flops = ParsNew.Flops; 
@@ -134,8 +134,9 @@ float Abc_NtkMfsTotalSwitching( Abc_Ntk_t * pNtk )
     pSwitching = (float *)vSwitching->pArray;
     Abc_NtkForEachObj( pNtk, pObjAbc, i )
     {
-        if ( (pObjAbc2 = Abc_ObjRegular(pObjAbc->pTemp)) && (pObjAig = pObjAbc2->pTemp) )
+        if ( (pObjAbc2 = Abc_ObjRegular(pObjAbc->pTemp)) && (pObjAig = Aig_Regular(pObjAbc2->pTemp)) )
             Result += Abc_ObjFanoutNum(pObjAbc) * pSwitching[pObjAig->Id];
+//            Result += pSwitching[pObjAig->Id];
     }
     Vec_IntFree( vSwitching );
     Aig_ManStop( pAig );
@@ -154,7 +155,7 @@ float Abc_NtkMfsTotalSwitching( Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored, int fSaveBest, int fDumpResult, int fUseLutLib, int fPrintMuxes, int fPower )
+void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored, int fSaveBest, int fDumpResult, int fUseLutLib, int fPrintMuxes, int fPower, int fGlitch )
 {
     int Num;
     if ( fSaveBest )
@@ -165,7 +166,7 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored, int fSave
         char * pNameGen = pNtk->pSpec? Extra_FileNameGeneric( pNtk->pSpec ) : "nameless_";
         sprintf( Buffer, "%s_dump.blif", pNameGen );
         Io_Write( pNtk, Buffer, IO_FILE_BLIF );
-        if ( pNtk->pSpec ) free( pNameGen );
+        if ( pNtk->pSpec ) ABC_FREE( pNameGen );
     }
 
 //    if ( Abc_NtkIsStrash(pNtk) )
@@ -230,15 +231,33 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored, int fSave
     }
 
     if ( Abc_NtkIsStrash(pNtk) )
+    {
+        extern int Abc_NtkGetMultiRefNum( Abc_Ntk_t * pNtk );
         fprintf( pFile, "  lev = %3d", Abc_AigLevel(pNtk) );
+//        fprintf( pFile, "  ff = %5d", Abc_NtkNodeNum(pNtk) + 2 * (Abc_NtkCoNum(pNtk)+Abc_NtkGetMultiRefNum(pNtk)) );
+//        fprintf( pFile, "  var = %5d", Abc_NtkCiNum(pNtk) + Abc_NtkCoNum(pNtk)+Abc_NtkGetMultiRefNum(pNtk) );
+    }
     else 
         fprintf( pFile, "  lev = %3d", Abc_NtkLevel(pNtk) );
     if ( fUseLutLib && Abc_FrameReadLibLut() )
         fprintf( pFile, "  delay = %5.2f", Abc_NtkDelayTraceLut(pNtk, 1) );
     if ( fPower )
         fprintf( pFile, "  power = %7.2f", Abc_NtkMfsTotalSwitching(pNtk) );
+    if ( fGlitch )
+    {
+        extern float Abc_NtkMfsTotalGlitching( Abc_Ntk_t * pNtk );
+        if ( Abc_NtkIsLogic(pNtk) && Abc_NtkGetFaninMax(pNtk) <= 6 )
+            fprintf( pFile, "  glitch = %7.2f %%", Abc_NtkMfsTotalGlitching(pNtk) );
+        else
+            printf( "\nCurrently computes glitching only for K-LUT networks with K <= 6." ); 
+    }
     fprintf( pFile, "\n" );
 
+    {
+        extern int Abc_NtkPrintSubraphSizes( Abc_Ntk_t * pNtk );
+//        Abc_NtkPrintSubraphSizes( pNtk );
+    }
+
 //    Abc_NtkCrossCut( pNtk );
 
     // print the statistic into a file
@@ -627,6 +646,13 @@ void Abc_NtkPrintFanioNew( FILE * pFile, Abc_Ntk_t * pNtk )
     fprintf( pFile, "Fanins: Max = %d. Ave = %.2f.  Fanouts: Max = %d. Ave =  %.2f.\n", 
         nFaninsMax,  1.0*nFaninsAll/Abc_NtkNodeNum(pNtk), 
         nFanoutsMax, 1.0*nFanoutsAll/Abc_NtkNodeNum(pNtk)  );
+/*
+    Abc_NtkForEachCi( pNtk, pNode, i )
+    {
+        printf( "%d ", Abc_ObjFanoutNum(pNode) );
+    }
+    printf( "\n" );
+*/
 }
 
 /**Function*************************************************************
@@ -786,7 +812,7 @@ void Abc_NtkPrintLevel( FILE * pFile, Abc_Ntk_t * pNtk, int fProfile, int fListN
         DelayMax   = Abc_NtkDelayTrace( pNtk );
         DelayDelta = DelayMax/nIntervals;
         // collect outputs by delay
-        pLevelCounts = ALLOC( int, nIntervals );
+        pLevelCounts = ABC_ALLOC( int, nIntervals );
         memset( pLevelCounts, 0, sizeof(int) * nIntervals );
         Abc_NtkForEachCo( pNtk, pNode, i )
         {
@@ -805,7 +831,7 @@ void Abc_NtkPrintLevel( FILE * pFile, Abc_Ntk_t * pNtk, int fProfile, int fListN
             printf( "[%8.2f - %8.2f] :   COs = %4d.   %5.1f %%\n", 
                 DelayDelta * i, DelayDelta * (i+1), pLevelCounts[i], 100.0 * nOutsSum/nOutsTotal );
         }
-        free( pLevelCounts );
+        ABC_FREE( pLevelCounts );
         return;
     }
     else if ( fProfile )
@@ -820,7 +846,7 @@ void Abc_NtkPrintLevel( FILE * pFile, Abc_Ntk_t * pNtk, int fProfile, int fListN
         Abc_NtkForEachCo( pNtk, pNode, i )
             if ( LevelMax < (int)Abc_ObjFanin0(pNode)->Level )
                 LevelMax = Abc_ObjFanin0(pNode)->Level;
-        pLevelCounts = ALLOC( int, LevelMax + 1 );
+        pLevelCounts = ABC_ALLOC( int, LevelMax + 1 );
         memset( pLevelCounts, 0, sizeof(int) * (LevelMax + 1) );
         Abc_NtkForEachCo( pNtk, pNode, i )
             pLevelCounts[Abc_ObjFanin0(pNode)->Level]++;
@@ -833,7 +859,7 @@ void Abc_NtkPrintLevel( FILE * pFile, Abc_Ntk_t * pNtk, int fProfile, int fListN
                 nOutsSum += pLevelCounts[i];
                 printf( "Level = %4d.  COs = %4d.   %5.1f %%\n", i, pLevelCounts[i], 100.0 * nOutsSum/nOutsTotal );
             }
-        free( pLevelCounts );
+        ABC_FREE( pLevelCounts );
         return;
     }
     assert( Abc_NtkIsStrash(pNtk) );
@@ -1188,6 +1214,152 @@ void Abc_ObjPrint( FILE * pFile, Abc_Obj_t * pObj )
 }
 
 
+/**Function*************************************************************
+
+  Synopsis    [Checks the status of the miter.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkPrintMiter( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pObj, * pChild, * pConst1 = Abc_AigConst1(pNtk);
+    int i, iOut = -1, Time = clock();
+    int nUnsat = 0;
+    int nSat   = 0;
+    int nUndec = 0;
+    int nPis   = 0;
+    Abc_NtkForEachPi( pNtk, pObj, i )
+        nPis += (int)( Abc_ObjFanoutNum(pObj) > 0 );
+    Abc_NtkForEachPo( pNtk, pObj, i )
+    {
+        pChild = Abc_ObjChild0(pObj);
+        // check if the output is constant 0
+        if ( pChild == Abc_ObjNot(pConst1) )
+            nUnsat++;
+        // check if the output is constant 1
+        else if ( pChild == pConst1 )
+        {
+            nSat++;
+            if ( iOut == -1 )
+                iOut = i;
+        }
+        // check if the output is a primary input
+        else if ( Abc_ObjIsPi(Abc_ObjRegular(pChild)) )
+        {
+            nSat++;
+            if ( iOut == -1 )
+                iOut = i;
+        }
+    // check if the output is 1 for the 0000 pattern
+        else if ( Abc_ObjRegular(pChild)->fPhase != (unsigned)Abc_ObjIsComplement(pChild) )
+        {
+            nSat++;
+            if ( iOut == -1 )
+                iOut = i;
+        }
+        else
+            nUndec++;
+    }
+    printf( "Miter:  I =%6d", nPis );
+    printf( "  N =%7d", Abc_NtkNodeNum(pNtk) );
+    printf( "  ? =%7d", nUndec );
+    printf( "  U =%6d", nUnsat );
+    printf( "  S =%6d", nSat );
+    Time = clock() - Time;
+    printf(" %7.2f sec\n", (float)(Time)/(float)(CLOCKS_PER_SEC));
+    if ( iOut >= 0 )
+        printf( "The first satisfiable output is number %d (%d).\n", iOut, Abc_ObjName( Abc_NtkPo(pNtk, iOut) ) );
+}
+
+
+
+
+typedef struct Gli_Man_t_ Gli_Man_t;
+
+extern Gli_Man_t * Gli_ManAlloc( int nObjs, int nRegs, int nFanioPairs );
+extern void        Gli_ManStop( Gli_Man_t * p );
+extern int         Gli_ManCreateCi( Gli_Man_t * p, int nFanouts );
+extern int         Gli_ManCreateCo( Gli_Man_t * p, int iFanin );
+extern int         Gli_ManCreateNode( Gli_Man_t * p, Vec_Int_t * vFanins, int nFanouts, unsigned * puTruth );
+
+extern void        Gli_ManSwitchesAndGlitches( Gli_Man_t * p, int nPatterns, float PiTransProb, int fVerbose );
+extern int         Gli_ObjNumSwitches( Gli_Man_t * p, int iNode );
+extern int         Gli_ObjNumGlitches( Gli_Man_t * p, int iNode );
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the percentable of increased power due to glitching.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+float Abc_NtkMfsTotalGlitching( Abc_Ntk_t * pNtk )
+{
+    int nSwitches, nGlitches;
+    Gli_Man_t * p;
+    Vec_Ptr_t * vNodes;
+    Vec_Int_t * vFanins, * vTruth;
+    Abc_Obj_t * pObj, * pFanin;
+    unsigned * puTruth;
+    int i, k;
+    assert( Abc_NtkIsLogic(pNtk) );
+    assert( Abc_NtkGetFaninMax(pNtk) <= 6 );
+    if ( Abc_NtkGetFaninMax(pNtk) > 6 )
+    {
+        printf( "Abc_NtkMfsTotalGlitching() This procedure works only for mapped networks with LUTs size up to 6 inputs.\n" );
+        return -1.0;
+    }
+    Abc_NtkToAig( pNtk );
+    vNodes = Abc_NtkDfs( pNtk, 0 );
+    vFanins = Vec_IntAlloc( 6 );
+    vTruth = Vec_IntAlloc( 1 << 12 );
+
+    // derive network for glitch computation
+    p = Gli_ManAlloc( Vec_PtrSize(vNodes) + Abc_NtkCiNum(pNtk) + Abc_NtkCoNum(pNtk), 
+        Abc_NtkLatchNum(pNtk), Abc_NtkGetTotalFanins(pNtk) + Abc_NtkCoNum(pNtk) );
+    Abc_NtkForEachObj( pNtk, pObj, i )
+        pObj->iTemp = -1;
+    Abc_NtkForEachCi( pNtk, pObj, i )
+        pObj->iTemp = Gli_ManCreateCi( p, Abc_ObjFanoutNum(pObj) );
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+    {
+        Vec_IntClear( vFanins );
+        Abc_ObjForEachFanin( pObj, pFanin, k )
+            Vec_IntPush( vFanins, pFanin->iTemp );
+        puTruth = Hop_ManConvertAigToTruth( pNtk->pManFunc, pObj->pData, Abc_ObjFaninNum(pObj), vTruth, 0 );
+        pObj->iTemp = Gli_ManCreateNode( p, vFanins, Abc_ObjFanoutNum(pObj), puTruth );
+    }
+    Abc_NtkForEachCo( pNtk, pObj, i )
+        Gli_ManCreateCo( p, Abc_ObjFanin0(pObj)->iTemp );
+
+    // compute glitching
+    Gli_ManSwitchesAndGlitches( p, 4000, 1.0/8.0, 0 );
+
+    // compute the ratio
+    nSwitches = nGlitches = 0;
+    Abc_NtkForEachObj( pNtk, pObj, i )
+        if ( pObj->iTemp >= 0 )
+        {
+            nSwitches += Abc_ObjFanoutNum(pObj) * Gli_ObjNumSwitches(p, pObj->iTemp);
+            nGlitches += Abc_ObjFanoutNum(pObj) * Gli_ObjNumGlitches(p, pObj->iTemp);
+        }
+
+    Gli_ManStop( p );
+    Vec_PtrFree( vNodes );
+    Vec_IntFree( vTruth );
+    Vec_IntFree( vFanins );
+    return nSwitches ? 100.0*(nGlitches-nSwitches)/nSwitches : 0.0;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abcProve.c b/src/base/abci/abcProve.c
index 6a695fc4..5a546ab1 100644
--- a/src/base/abci/abcProve.c
+++ b/src/base/abci/abcProve.c
@@ -29,7 +29,7 @@
 extern int  Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, bool fUpdateLevel, bool fUseZeros, bool fUseDcs, bool fVerbose );
 extern Abc_Ntk_t * Abc_NtkFromFraig( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk );
 
-static Abc_Ntk_t * Abc_NtkMiterFraig( Abc_Ntk_t * pNtk, int nBTLimit, sint64 nInspLimit, int * pRetValue, int * pNumFails, sint64 * pNumConfs, sint64 * pNumInspects );
+static Abc_Ntk_t * Abc_NtkMiterFraig( Abc_Ntk_t * pNtk, int nBTLimit, ABC_INT64_T nInspLimit, int * pRetValue, int * pNumFails, ABC_INT64_T * pNumConfs, ABC_INT64_T * pNumInspects );
 static void Abc_NtkMiterPrint( Abc_Ntk_t * pNtk, char * pString, int clk, int fVerbose );
 
 
@@ -56,7 +56,7 @@ int Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, void * pPars )
     Prove_Params_t * pParams = pPars;
     Abc_Ntk_t * pNtk, * pNtkTemp;
     int RetValue = -1, nIter, nSatFails, Counter, clk; //, timeStart = clock();
-    sint64 nSatConfs, nSatInspects, nInspectLimit;
+    ABC_INT64_T nSatConfs, nSatInspects, nInspectLimit;
 
     // get the starting network
     pNtk = *ppNtk;
@@ -77,7 +77,7 @@ int Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, void * pPars )
     if ( !pParams->fUseRewriting && !pParams->fUseFraiging )
     {
         clk = clock();
-        RetValue = Abc_NtkMiterSat( pNtk, (sint64)pParams->nMiteringLimitLast, (sint64)0, 0, NULL, NULL );
+        RetValue = Abc_NtkMiterSat( pNtk, (ABC_INT64_T)pParams->nMiteringLimitLast, (ABC_INT64_T)0, 0, NULL, NULL );
         Abc_NtkMiterPrint( pNtk, "SAT solving", clk, pParams->fVerbose );
         *ppNtk = pNtk;
         return RetValue;
@@ -97,7 +97,7 @@ int Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, void * pPars )
         // try brute-force SAT
         clk = clock();
         nInspectLimit = pParams->nTotalInspectLimit? pParams->nTotalInspectLimit - pParams->nTotalInspectsMade : 0;
-        RetValue = Abc_NtkMiterSat( pNtk, (sint64)(pParams->nMiteringLimitStart * pow(pParams->nMiteringLimitMulti,nIter)), (sint64)nInspectLimit, 0, &nSatConfs, &nSatInspects );
+        RetValue = Abc_NtkMiterSat( pNtk, (ABC_INT64_T)(pParams->nMiteringLimitStart * pow(pParams->nMiteringLimitMulti,nIter)), (ABC_INT64_T)nInspectLimit, 0, &nSatConfs, &nSatInspects );
         Abc_NtkMiterPrint( pNtk, "SAT solving", clk, pParams->fVerbose );
         if ( RetValue >= 0 )
             break;
@@ -211,14 +211,14 @@ int Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, void * pPars )
         }
         clk = clock();
         nInspectLimit = pParams->nTotalInspectLimit? pParams->nTotalInspectLimit - pParams->nTotalInspectsMade : 0;
-        RetValue = Abc_NtkMiterSat( pNtk, (sint64)pParams->nMiteringLimitLast, (sint64)nInspectLimit, 0, NULL, NULL );
+        RetValue = Abc_NtkMiterSat( pNtk, (ABC_INT64_T)pParams->nMiteringLimitLast, (ABC_INT64_T)nInspectLimit, 0, NULL, NULL );
         Abc_NtkMiterPrint( pNtk, "SAT solving", clk, pParams->fVerbose );
     }
 
     // assign the model if it was proved by rewriting (const 1 miter)
     if ( RetValue == 0 && pNtk->pModel == NULL )
     {
-        pNtk->pModel = ALLOC( int, Abc_NtkCiNum(pNtk) );
+        pNtk->pModel = ABC_ALLOC( int, Abc_NtkCiNum(pNtk) );
         memset( pNtk->pModel, 0, sizeof(int) * Abc_NtkCiNum(pNtk) );
     }
     *ppNtk = pNtk;
@@ -236,7 +236,7 @@ int Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, void * pPars )
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkMiterFraig( Abc_Ntk_t * pNtk, int nBTLimit, sint64 nInspLimit, int * pRetValue, int * pNumFails, sint64 * pNumConfs, sint64 * pNumInspects )
+Abc_Ntk_t * Abc_NtkMiterFraig( Abc_Ntk_t * pNtk, int nBTLimit, ABC_INT64_T nInspLimit, int * pRetValue, int * pNumFails, ABC_INT64_T * pNumConfs, ABC_INT64_T * pNumInspects )
 {
     Abc_Ntk_t * pNtkNew;
     Fraig_Params_t Params, * pParams = &Params;
@@ -275,8 +275,8 @@ Abc_Ntk_t * Abc_NtkMiterFraig( Abc_Ntk_t * pNtk, int nBTLimit, sint64 nInspLimit
     if ( RetValue == 0 )
     {
         pModel = Fraig_ManReadModel( pMan );
-        FREE( pNtkNew->pModel );
-        pNtkNew->pModel = ALLOC( int, Abc_NtkCiNum(pNtkNew) );
+        ABC_FREE( pNtkNew->pModel );
+        pNtkNew->pModel = ABC_ALLOC( int, Abc_NtkCiNum(pNtkNew) );
         memcpy( pNtkNew->pModel, pModel, sizeof(int) * Abc_NtkCiNum(pNtkNew) );
     }
 
@@ -308,7 +308,7 @@ void Abc_NtkMiterPrint( Abc_Ntk_t * pNtk, char * pString, int clk, int fVerbose
         return;
     printf( "Nodes = %7d.  Levels = %4d.  ", Abc_NtkNodeNum(pNtk), 
         Abc_NtkIsStrash(pNtk)? Abc_AigLevel(pNtk) : Abc_NtkLevel(pNtk) );
-    PRT( pString, clock() - clk );
+    ABC_PRT( pString, clock() - clk );
 }
 
   
diff --git a/src/base/abci/abcQbf.c b/src/base/abci/abcQbf.c
index b839f812..fe6ef895 100644
--- a/src/base/abci/abcQbf.c
+++ b/src/base/abci/abcQbf.c
@@ -140,8 +140,8 @@ clkV = clock() - clkV;
             printf( "AIG = %6d  ", Abc_NtkNodeNum(pNtkSyn) );
             Abc_NtkVectorPrintVars( pNtk, vPiValues, nPars );
             printf( "  " );
-//            PRTn( "Syn", clkS );
-            PRT( "Ver", clkV );
+//            ABC_PRTn( "Syn", clkS );
+            ABC_PRT( "Ver", clkV );
         }
     }
     Abc_NtkDelete( pNtkSyn );
@@ -157,7 +157,7 @@ clkV = clock() - clkV;
         printf( "Unsolved after %d interations.  ", nIters );
     else 
         printf( "Implementation does not exist.  " );
-    PRT( "Total runtime", clock() - clkTotal );
+    ABC_PRT( "Total runtime", clock() - clkTotal );
     Vec_IntFree( vPiValues );
 }
 
diff --git a/src/base/abci/abcQuant.c b/src/base/abci/abcQuant.c
index 24981d1c..6d973a85 100644
--- a/src/base/abci/abcQuant.c
+++ b/src/base/abci/abcQuant.c
@@ -41,6 +41,8 @@
 ***********************************************************************/
 void Abc_NtkSynthesize( Abc_Ntk_t ** ppNtk, int fMoreEffort )
 {
+    extern Abc_Ntk_t * Abc_NtkIvyFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fDoSparse, int fProve, int fTransfer, int fVerbose );
+
     Abc_Ntk_t * pNtk, * pNtkTemp;
 
     pNtk = *ppNtk;
@@ -56,6 +58,9 @@ void Abc_NtkSynthesize( Abc_Ntk_t ** ppNtk, int fMoreEffort )
         Abc_NtkRefactor( pNtk, 10, 16, 0, 0, 0, 0 );
         pNtk = Abc_NtkBalance( pNtkTemp = pNtk, 0, 0, 0 );          
         Abc_NtkDelete( pNtkTemp );
+
+        pNtk = Abc_NtkIvyFraig( pNtkTemp = pNtk, 100, 1, 0, 0, 0 );
+        Abc_NtkDelete( pNtkTemp );
     }
 
     *ppNtk = pNtk;
@@ -384,7 +389,7 @@ Abc_Ntk_t * Abc_NtkReachability( Abc_Ntk_t * pNtkRel, int nIters, int fVerbose )
         {
             printf( "I = %3d : Reach = %6d  Fr = %6d  FrM = %6d  %7.2f %%   ", 
                 i + 1, Abc_NtkNodeNum(pNtkReached), nNodesOld, nNodesNew, 100.0*(nNodesNew-nNodesPrev)/nNodesPrev );
-            PRT( "T", clock() - clk );
+            ABC_PRT( "T", clock() - clk );
         }
         nNodesPrev = Abc_NtkNodeNum(pNtkFront);
     }
diff --git a/src/base/abci/abcReach.c b/src/base/abci/abcReach.c
index 815e452a..3834c00d 100644
--- a/src/base/abci/abcReach.c
+++ b/src/base/abci/abcReach.c
@@ -47,8 +47,8 @@ DdNode * Abc_NtkInitStateVarMap( DdManager * dd, Abc_Ntk_t * pNtk, int fVerbose
     int i;
 
     // set the variable mapping for Cudd_bddVarMap()
-    pbVarsX = ALLOC( DdNode *, dd->size );
-    pbVarsY = ALLOC( DdNode *, dd->size );
+    pbVarsX = ABC_ALLOC( DdNode *, dd->size );
+    pbVarsY = ABC_ALLOC( DdNode *, dd->size );
     bProd = b1;         Cudd_Ref( bProd );
     Abc_NtkForEachLatch( pNtk, pLatch, i )
     {
@@ -60,8 +60,8 @@ DdNode * Abc_NtkInitStateVarMap( DdManager * dd, Abc_Ntk_t * pNtk, int fVerbose
         Cudd_RecursiveDeref( dd, bTemp ); 
     }
     Cudd_SetVarMap( dd, pbVarsX, pbVarsY, Abc_NtkLatchNum(pNtk) );
-    FREE( pbVarsX );
-    FREE( pbVarsY );
+    ABC_FREE( pbVarsX );
+    ABC_FREE( pbVarsY );
 
     Cudd_Deref( bProd );
     return bProd;
@@ -96,13 +96,13 @@ DdNode ** Abc_NtkCreatePartitions( DdManager * dd, Abc_Ntk_t * pNtk, int fReorde
         Cudd_AutodynDisable( dd );
 
     // compute the transition relation
-    pbParts = ALLOC( DdNode *, Abc_NtkLatchNum(pNtk) );
+    pbParts = ABC_ALLOC( DdNode *, Abc_NtkLatchNum(pNtk) );
     Abc_NtkForEachLatch( pNtk, pNode, i )
     {
         bVar  = Cudd_bddIthVar( dd, Abc_NtkCiNum(pNtk) + i );
         pbParts[i] = Cudd_bddXnor( dd, bVar, Abc_ObjGlobalBdd(Abc_ObjFanin0(pNode)) );  Cudd_Ref( pbParts[i] );
     }
-    // free the global BDDs
+    // ABC_FREE the global BDDs
     Abc_NtkFreeGlobalBdds( pNtk, 0 );
 
     // reorder and disable reordering
@@ -143,7 +143,7 @@ DdNode * Abc_NtkComputeReachable( DdManager * dd, Abc_Ntk_t * pNtk, DdNode ** pb
 
     // collect the NS variables
     // set the variable mapping for Cudd_bddVarMap()
-    pbVarsY = ALLOC( DdNode *, dd->size );
+    pbVarsY = ABC_ALLOC( DdNode *, dd->size );
     Abc_NtkForEachLatch( pNtk, pLatch, i )
         pbVarsY[i] = dd->vars[ Abc_NtkCiNum(pNtk) + i ];
 
@@ -153,7 +153,7 @@ DdNode * Abc_NtkComputeReachable( DdManager * dd, Abc_Ntk_t * pNtk, DdNode ** pb
         pTree = Extra_bddImageStart( dd, bCubeCs, Abc_NtkLatchNum(pNtk), pbParts, Abc_NtkLatchNum(pNtk), pbVarsY, fVerbose );
     else
         pTree2 = Extra_bddImageStart2( dd, bCubeCs, Abc_NtkLatchNum(pNtk), pbParts, Abc_NtkLatchNum(pNtk), pbVarsY, fVerbose );
-    free( pbVarsY );
+    ABC_FREE( pbVarsY );
     Cudd_RecursiveDeref( dd, bCubeCs );
 
     // perform reachability analisys
@@ -230,7 +230,7 @@ DdNode * Abc_NtkComputeReachable( DdManager * dd, Abc_Ntk_t * pNtk, DdNode ** pb
         fprintf( stdout, "Reachable states = %.0f. (Ratio = %.4f %%)\n", nMints, 100.0*nMints/pow(2.0, Abc_NtkLatchNum(pNtk)) );
         fflush( stdout );
     }
-//PRB( dd, bReached );
+//ABC_PRB( dd, bReached );
     Cudd_Deref( bReached );
     if ( nIters > nIterMax || Cudd_DagSize(bReached) > nBddMax )
          printf( "Verified ONLY FOR STATES REACHED in %d iterations. \n", nIters );
@@ -298,11 +298,11 @@ void Abc_NtkVerifyUsingBdds( Abc_Ntk_t * pNtk, int nBddMax, int nIterMax, int fP
     Cudd_RecursiveDeref( dd, bInitial );
     for ( i = 0; i < Abc_NtkLatchNum(pNtk); i++ )
         Cudd_RecursiveDeref( dd, pbParts[i] );
-    free( pbParts );
+    ABC_FREE( pbParts );
     Extra_StopManager( dd );
 
     // report the runtime
-    PRT( "Time", clock() - clk );
+    ABC_PRT( "Time", clock() - clk );
     fflush( stdout );
 }
 
diff --git a/src/base/abci/abcRec.c b/src/base/abci/abcRec.c
index 2983efc2..d8884147 100644
--- a/src/base/abci/abcRec.c
+++ b/src/base/abci/abcRec.c
@@ -184,7 +184,7 @@ void Abc_NtkRecStart( Abc_Ntk_t * pNtk, int nVars, int nCuts )
     Abc_NtkCleanEquiv( pNtk );
 
     // start the manager
-    p = ALLOC( Abc_ManRec_t, 1 );
+    p = ABC_ALLOC( Abc_ManRec_t, 1 );
     memset( p, 0, sizeof(Abc_ManRec_t) );
     p->pNtk = pNtk;
     p->nVars = Abc_NtkPiNum(pNtk);
@@ -206,7 +206,7 @@ void Abc_NtkRecStart( Abc_Ntk_t * pNtk, int nVars, int nCuts )
 
     // create hash table
     p->nBins = 50011;
-    p->pBins = ALLOC( Abc_Obj_t *, p->nBins );
+    p->pBins = ABC_ALLOC( Abc_Obj_t *, p->nBins );
     memset( p->pBins, 0, sizeof(Abc_Obj_t *) * p->nBins );
 
     // set elementary tables
@@ -251,10 +251,10 @@ p->timeTruth += clock() - clk;
     }
 
     // temporaries
-    p->pBytes = ALLOC( int, 4*p->nWords );
-    p->pMints = ALLOC( int, 2*p->nVars );
-    p->pTemp1 = ALLOC( unsigned, p->nWords );
-    p->pTemp2 = ALLOC( unsigned, p->nWords );
+    p->pBytes = ABC_ALLOC( int, 4*p->nWords );
+    p->pMints = ABC_ALLOC( int, 2*p->nVars );
+    p->pTemp1 = ABC_ALLOC( unsigned, p->nWords );
+    p->pTemp2 = ABC_ALLOC( unsigned, p->nWords );
     p->vNodes = Vec_PtrAlloc( 100 );
     p->vTtTemps = Vec_PtrAllocSimInfo( 64, p->nWords );
     p->vMemory = Vec_IntAlloc( Abc_TruthWordNum(p->nVars) * 1000 );
@@ -282,13 +282,13 @@ void Abc_NtkRecStop()
         Abc_NtkDelete( s_pMan->pNtk );
     Vec_PtrFree( s_pMan->vTtNodes );
     Vec_PtrFree( s_pMan->vTtElems );
-    free( s_pMan->pBins );
+    ABC_FREE( s_pMan->pBins );
 
     // temporaries
-    free( s_pMan->pBytes );
-    free( s_pMan->pMints );
-    free( s_pMan->pTemp1 );
-    free( s_pMan->pTemp2 );
+    ABC_FREE( s_pMan->pBytes );
+    ABC_FREE( s_pMan->pMints );
+    ABC_FREE( s_pMan->pTemp1 );
+    ABC_FREE( s_pMan->pTemp2 );
     Vec_PtrFree( s_pMan->vNodes );
     Vec_PtrFree( s_pMan->vTtTemps );
     if ( s_pMan->vLabels )
@@ -297,7 +297,7 @@ void Abc_NtkRecStop()
         Vec_StrFree( s_pMan->vCosts );
     Vec_IntFree( s_pMan->vMemory );
 
-    free( s_pMan );
+    ABC_FREE( s_pMan );
     s_pMan = NULL;
 }
 
@@ -396,11 +396,11 @@ void Abc_NtkRecPs()
     printf( "Functions added                             = %8d. (%6.2f %%)\n", p->nAddedFuncs,   !p->nTried? 0 : 100.0*p->nAddedFuncs/p->nTried );
 
     p->timeOther = p->timeTotal - p->timeCollect - p->timeTruth - p->timeCanon;
-    PRTP( "Collecting nodes ", p->timeCollect, p->timeTotal );
-    PRTP( "Computing truth  ", p->timeTruth, p->timeTotal );
-    PRTP( "Canonicizing     ", p->timeCanon, p->timeTotal );
-    PRTP( "Other            ", p->timeOther, p->timeTotal );
-    PRTP( "TOTAL            ", p->timeTotal, p->timeTotal );
+    ABC_PRTP( "Collecting nodes ", p->timeCollect, p->timeTotal );
+    ABC_PRTP( "Computing truth  ", p->timeTruth, p->timeTotal );
+    ABC_PRTP( "Canonicizing     ", p->timeCanon, p->timeTotal );
+    ABC_PRTP( "Other            ", p->timeOther, p->timeTotal );
+    ABC_PRTP( "TOTAL            ", p->timeTotal, p->timeTotal );
     if ( p->nFunsFound )
     printf( "During rewriting found = %d and not found = %d functions.\n", p->nFunsFound, p->nFunsNotFound );
 }
diff --git a/src/base/abci/abcReconv.c b/src/base/abci/abcReconv.c
index 078aee9d..1c086fb0 100644
--- a/src/base/abci/abcReconv.c
+++ b/src/base/abci/abcReconv.c
@@ -584,7 +584,7 @@ DdNode * Abc_NodeConeDcs( DdManager * dd, DdNode ** pbVarsX, DdNode ** pbVarsY,
 Abc_ManCut_t * Abc_NtkManCutStart( int nNodeSizeMax, int nConeSizeMax, int nNodeFanStop, int nConeFanStop )
 {
     Abc_ManCut_t * p;
-    p = ALLOC( Abc_ManCut_t, 1 );
+    p = ABC_ALLOC( Abc_ManCut_t, 1 );
     memset( p, 0, sizeof(Abc_ManCut_t) );
     p->vNodeLeaves  = Vec_PtrAlloc( 100 );
     p->vConeLeaves  = Vec_PtrAlloc( 100 );
@@ -616,7 +616,7 @@ void Abc_NtkManCutStop( Abc_ManCut_t * p )
     Vec_PtrFree( p->vVisited    );
     Vec_VecFree( p->vLevels );
     Vec_PtrFree( p->vNodesTfo );
-    free( p );
+    ABC_FREE( p );
 }
 
 /**Function*************************************************************
diff --git a/src/base/abci/abcRefactor.c b/src/base/abci/abcRefactor.c
index 821bd66b..5245bd23 100644
--- a/src/base/abci/abcRefactor.c
+++ b/src/base/abci/abcRefactor.c
@@ -245,7 +245,7 @@ p->timeSop += clock() - clk;
     // get the factored form
 clk = clock();
     pFForm = Dec_Factor( pSop );
-    free( pSop );
+    ABC_FREE( pSop );
 p->timeFact += clock() - clk;
 
     // mark the fanin boundary 
@@ -310,7 +310,7 @@ p->timeEval += clock() - clk;
 Abc_ManRef_t * Abc_NtkManRefStart( int nNodeSizeMax, int nConeSizeMax, bool fUseDcs, bool fVerbose )
 {
     Abc_ManRef_t * p;
-    p = ALLOC( Abc_ManRef_t, 1 );
+    p = ABC_ALLOC( Abc_ManRef_t, 1 );
     memset( p, 0, sizeof(Abc_ManRef_t) );
     p->vCube        = Vec_StrAlloc( 100 );
     p->vVisited     = Vec_PtrAlloc( 100 );
@@ -342,7 +342,7 @@ void Abc_NtkManRefStop( Abc_ManRef_t * p )
     Extra_StopManager( p->dd );
     Vec_PtrFree( p->vVisited );
     Vec_StrFree( p->vCube    );
-    free( p );
+    ABC_FREE( p );
 }
 
 /**Function*************************************************************
@@ -362,15 +362,15 @@ void Abc_NtkManRefPrintStats( Abc_ManRef_t * p )
     printf( "Nodes considered  = %8d.\n", p->nNodesConsidered );
     printf( "Nodes refactored  = %8d.\n", p->nNodesRefactored );
     printf( "Gain              = %8d. (%6.2f %%).\n", p->nNodesBeg-p->nNodesEnd, 100.0*(p->nNodesBeg-p->nNodesEnd)/p->nNodesBeg );
-    PRT( "Cuts       ", p->timeCut );
-    PRT( "Resynthesis", p->timeRes );
-    PRT( "    BDD    ", p->timeBdd );
-    PRT( "    DCs    ", p->timeDcs );
-    PRT( "    SOP    ", p->timeSop );
-    PRT( "    FF     ", p->timeFact );
-    PRT( "    Eval   ", p->timeEval );
-    PRT( "AIG update ", p->timeNtk );
-    PRT( "TOTAL      ", p->timeTotal );
+    ABC_PRT( "Cuts       ", p->timeCut );
+    ABC_PRT( "Resynthesis", p->timeRes );
+    ABC_PRT( "    BDD    ", p->timeBdd );
+    ABC_PRT( "    DCs    ", p->timeDcs );
+    ABC_PRT( "    SOP    ", p->timeSop );
+    ABC_PRT( "    FF     ", p->timeFact );
+    ABC_PRT( "    Eval   ", p->timeEval );
+    ABC_PRT( "AIG update ", p->timeNtk );
+    ABC_PRT( "TOTAL      ", p->timeTotal );
 }
 
 
diff --git a/src/base/abci/abcReorder.c b/src/base/abci/abcReorder.c
index 182780cd..340e3d17 100644
--- a/src/base/abci/abcReorder.c
+++ b/src/base/abci/abcReorder.c
@@ -46,7 +46,7 @@ void Abc_NodeBddReorder( reo_man * p, Abc_Obj_t * pNode )
     DdNode * bFunc;
     int * pOrder, i;
     // create the temporary array for the variable order
-    pOrder = ALLOC( int, Abc_ObjFaninNum(pNode) );
+    pOrder = ABC_ALLOC( int, Abc_ObjFaninNum(pNode) );
     for ( i = 0; i < Abc_ObjFaninNum(pNode); i++ )
         pOrder[i] = -1;
     // reorder the BDD
@@ -58,7 +58,7 @@ void Abc_NodeBddReorder( reo_man * p, Abc_Obj_t * pNode )
         pOrder[i] = pNode->vFanins.pArray[ pOrder[i] ];
     Abc_ObjForEachFanin( pNode, pFanin, i )
         pNode->vFanins.pArray[i] = pOrder[i];
-    free( pOrder );
+    ABC_FREE( pOrder );
 }
 
 /**Function*************************************************************
diff --git a/src/base/abci/abcRestruct.c b/src/base/abci/abcRestruct.c
index 2550e02c..26774620 100644
--- a/src/base/abci/abcRestruct.c
+++ b/src/base/abci/abcRestruct.c
@@ -990,7 +990,7 @@ Cut_Man_t * Abc_NtkStartCutManForRestruct( Abc_Ntk_t * pNtk, int nCutMax, int fD
 Abc_ManRst_t * Abc_NtkManRstStart( int nCutMax, bool fUpdateLevel, bool fUseZeros, bool fVerbose )
 {
     Abc_ManRst_t * p;
-    p = ALLOC( Abc_ManRst_t, 1 );
+    p = ABC_ALLOC( Abc_ManRst_t, 1 );
     memset( p, 0, sizeof(Abc_ManRst_t) );
     // set the parameters
     p->nCutMax      = nCutMax;
@@ -1045,7 +1045,7 @@ void Abc_NtkManRstStop( Abc_ManRst_t * p )
     Vec_IntFree( p->vBinate );
     Vec_IntFree( p->vTwos );
     Vec_IntFree( p->vRands );
-    free( p );
+    ABC_FREE( p );
 }
 
 /**Function*************************************************************
@@ -1067,13 +1067,13 @@ void Abc_NtkManRstPrintStats( Abc_ManRst_t * p )
     printf( "Cuts explored      = %8d.\n", p->nCutsExplored      );
     printf( "Nodes restructured = %8d.\n", p->nNodesRestructured );
     printf( "Calculated gain    = %8d.\n", p->nNodesGained       );
-    PRT( "Cuts       ", p->timeCut );
-    PRT( "Resynthesis", p->timeRes );
-    PRT( "    BDD    ", p->timeBdd );
-    PRT( "    DSD    ", p->timeDsd );
-    PRT( "    Eval   ", p->timeEval );
-    PRT( "AIG update ", p->timeNtk );
-    PRT( "TOTAL      ", p->timeTotal );
+    ABC_PRT( "Cuts       ", p->timeCut );
+    ABC_PRT( "Resynthesis", p->timeRes );
+    ABC_PRT( "    BDD    ", p->timeBdd );
+    ABC_PRT( "    DSD    ", p->timeDsd );
+    ABC_PRT( "    Eval   ", p->timeEval );
+    ABC_PRT( "AIG update ", p->timeNtk );
+    ABC_PRT( "TOTAL      ", p->timeTotal );
 }
 
 
@@ -1201,16 +1201,16 @@ void Abc_NodeMffcSimulate( Vec_Ptr_t * vDecs, int nLeaves, Vec_Int_t * vRands, V
     Vec_PtrForEachEntryStop( vDecs, pObj, i, nLeaves )
     {
         uData = (unsigned)Vec_IntEntry( vRands, i );
-        pObj->pData = (void *)(PORT_PTRUINT_T)uData;
+        pObj->pData = (void *)(ABC_PTRUINT_T)uData;
         Vec_IntPush( vSims, uData );
     }
     // simulate
     Vec_PtrForEachEntryStart( vDecs, pObj, i, nLeaves )
     {
-        uData0 = (unsigned)(PORT_PTRUINT_T)Abc_ObjFanin0(pObj)->pData;
-        uData1 = (unsigned)(PORT_PTRUINT_T)Abc_ObjFanin1(pObj)->pData;
+        uData0 = (unsigned)(ABC_PTRUINT_T)Abc_ObjFanin0(pObj)->pData;
+        uData1 = (unsigned)(ABC_PTRUINT_T)Abc_ObjFanin1(pObj)->pData;
         uData = (Abc_ObjFaninC0(pObj)? ~uData0 : uData0) & (Abc_ObjFaninC1(pObj)? ~uData1 : uData1);
-        pObj->pData = (void *)(PORT_PTRUINT_T)uData;
+        pObj->pData = (void *)(ABC_PTRUINT_T)uData;
         Vec_IntPush( vSims, uData );
     }
 }
diff --git a/src/base/abci/abcResub.c b/src/base/abci/abcResub.c
index 80532b14..861a5e66 100644
--- a/src/base/abci/abcResub.c
+++ b/src/base/abci/abcResub.c
@@ -293,7 +293,7 @@ Abc_ManRes_t * Abc_ManResubStart( int nLeavesMax, int nDivsMax )
     unsigned * pData;
     int i, k;
     assert( sizeof(unsigned) == 4 );
-    p = ALLOC( Abc_ManRes_t, 1 );
+    p = ABC_ALLOC( Abc_ManRes_t, 1 );
     memset( p, 0, sizeof(Abc_ManRes_t) );
     p->nLeavesMax = nLeavesMax;
     p->nDivsMax   = nDivsMax;
@@ -301,7 +301,7 @@ Abc_ManRes_t * Abc_ManResubStart( int nLeavesMax, int nDivsMax )
     // allocate simulation info
     p->nBits      = (1 << p->nLeavesMax);
     p->nWords     = (p->nBits <= 32)? 1 : (p->nBits / 32);
-    p->pInfo      = ALLOC( unsigned, p->nWords * (p->nDivsMax + 1) );
+    p->pInfo      = ABC_ALLOC( unsigned, p->nWords * (p->nDivsMax + 1) );
     memset( p->pInfo, 0, sizeof(unsigned) * p->nWords * p->nLeavesMax );
     p->vSims      = Vec_PtrAlloc( p->nDivsMax );
     for ( i = 0; i < p->nDivsMax; i++ )
@@ -352,8 +352,8 @@ void Abc_ManResubStop( Abc_ManRes_t * p )
     Vec_PtrFree( p->vDivs2UN0 );
     Vec_PtrFree( p->vDivs2UN1 );
     Vec_PtrFree( p->vTemp );
-    free( p->pInfo );
-    free( p );
+    ABC_FREE( p->pInfo );
+    ABC_FREE( p );
 }
 
 /**Function*************************************************************
@@ -369,16 +369,16 @@ void Abc_ManResubStop( Abc_ManRes_t * p )
 ***********************************************************************/
 void Abc_ManResubPrint( Abc_ManRes_t * p )
 {
-    printf( "Used constants    = %6d.             ", p->nUsedNodeC );          PRT( "Cuts  ", p->timeCut );
-    printf( "Used replacements = %6d.             ", p->nUsedNode0 );          PRT( "Resub ", p->timeRes );
-    printf( "Used single ORs   = %6d.             ", p->nUsedNode1Or );        PRT( " Div  ", p->timeDiv );
-    printf( "Used single ANDs  = %6d.             ", p->nUsedNode1And );       PRT( " Mffc ", p->timeMffc );
-    printf( "Used double ORs   = %6d.             ", p->nUsedNode2Or );        PRT( " Sim  ", p->timeSim );
-    printf( "Used double ANDs  = %6d.             ", p->nUsedNode2And );       PRT( " 1    ", p->timeRes1 );
-    printf( "Used OR-AND       = %6d.             ", p->nUsedNode2OrAnd );     PRT( " D    ", p->timeResD );
-    printf( "Used AND-OR       = %6d.             ", p->nUsedNode2AndOr );     PRT( " 2    ", p->timeRes2 );
-    printf( "Used OR-2ANDs     = %6d.             ", p->nUsedNode3OrAnd );     PRT( "Truth ", p->timeTruth ); //PRT( " 3    ", p->timeRes3 );
-    printf( "Used AND-2ORs     = %6d.             ", p->nUsedNode3AndOr );     PRT( "AIG   ", p->timeNtk );
+    printf( "Used constants    = %6d.             ", p->nUsedNodeC );          ABC_PRT( "Cuts  ", p->timeCut );
+    printf( "Used replacements = %6d.             ", p->nUsedNode0 );          ABC_PRT( "Resub ", p->timeRes );
+    printf( "Used single ORs   = %6d.             ", p->nUsedNode1Or );        ABC_PRT( " Div  ", p->timeDiv );
+    printf( "Used single ANDs  = %6d.             ", p->nUsedNode1And );       ABC_PRT( " Mffc ", p->timeMffc );
+    printf( "Used double ORs   = %6d.             ", p->nUsedNode2Or );        ABC_PRT( " Sim  ", p->timeSim );
+    printf( "Used double ANDs  = %6d.             ", p->nUsedNode2And );       ABC_PRT( " 1    ", p->timeRes1 );
+    printf( "Used OR-AND       = %6d.             ", p->nUsedNode2OrAnd );     ABC_PRT( " D    ", p->timeResD );
+    printf( "Used AND-OR       = %6d.             ", p->nUsedNode2AndOr );     ABC_PRT( " 2    ", p->timeRes2 );
+    printf( "Used OR-2ANDs     = %6d.             ", p->nUsedNode3OrAnd );     ABC_PRT( "Truth ", p->timeTruth ); //ABC_PRT( " 3    ", p->timeRes3 );
+    printf( "Used AND-2ORs     = %6d.             ", p->nUsedNode3AndOr );     ABC_PRT( "AIG   ", p->timeNtk );
     printf( "TOTAL             = %6d.             ", p->nUsedNodeC +
                                                      p->nUsedNode0 +
                                                      p->nUsedNode1Or +
@@ -389,7 +389,7 @@ void Abc_ManResubPrint( Abc_ManRes_t * p )
                                                      p->nUsedNode2AndOr +
                                                      p->nUsedNode3OrAnd +
                                                      p->nUsedNode3AndOr
-                                                   );                          PRT( "TOTAL ", p->timeTotal );
+                                                   );                          ABC_PRT( "TOTAL ", p->timeTotal );
     printf( "Total leaves   = %8d.\n", p->nTotalLeaves );
     printf( "Total divisors = %8d.\n", p->nTotalDivs );
 //    printf( "Total gain     = %8d.\n", p->nTotalGain );
diff --git a/src/base/abci/abcRewrite.c b/src/base/abci/abcRewrite.c
index ff1e1f8b..a119ccd2 100644
--- a/src/base/abci/abcRewrite.c
+++ b/src/base/abci/abcRewrite.c
@@ -168,7 +168,7 @@ Rwr_ManAddTimeTotal( pManRwr, clock() - clkStart );
     {
 //        int clk = clock();
     Abc_NtkReassignIds( pNtk );
-//        PRT( "time", clock() - clk );
+//        ABC_PRT( "time", clock() - clk );
     }
 //    Abc_AigCheckFaninOrder( pNtk->pManFunc );
     // fix the levels
diff --git a/src/base/abci/abcRr.c b/src/base/abci/abcRr.c
index 888850e1..9fbad080 100644
--- a/src/base/abci/abcRr.c
+++ b/src/base/abci/abcRr.c
@@ -244,14 +244,14 @@ int Abc_NtkRR( Abc_Ntk_t * pNtk, int nFaninLevels, int nFanoutLevels, int fUseFa
 Abc_RRMan_t * Abc_RRManStart()
 {
     Abc_RRMan_t * p;
-    p = ALLOC( Abc_RRMan_t, 1 );
+    p = ABC_ALLOC( Abc_RRMan_t, 1 );
     memset( p, 0, sizeof(Abc_RRMan_t) );
     p->vFaninLeaves  = Vec_PtrAlloc( 100 );  // the leaves of the fanin cone
     p->vFanoutRoots  = Vec_PtrAlloc( 100 );  // the roots of the fanout cone
     p->vLeaves       = Vec_PtrAlloc( 100 );  // the leaves of the window
     p->vCone         = Vec_PtrAlloc( 100 );  // the internal nodes of the window
     p->vRoots        = Vec_PtrAlloc( 100 );  // the roots of the window
-    p->pParams       = ALLOC( Prove_Params_t, 1 );
+    p->pParams       = ABC_ALLOC( Prove_Params_t, 1 );
     memset( p->pParams, 0, sizeof(Prove_Params_t) );
     Prove_ParamsSetDefault( p->pParams );
     return p;
@@ -276,8 +276,8 @@ void Abc_RRManStop( Abc_RRMan_t * p )
     Vec_PtrFree( p->vLeaves );  
     Vec_PtrFree( p->vCone );  
     Vec_PtrFree( p->vRoots );  
-    free( p->pParams );
-    free( p );
+    ABC_FREE( p->pParams );
+    ABC_FREE( p );
 }
 
 /**Function*************************************************************
@@ -299,12 +299,12 @@ void Abc_RRManPrintStats( Abc_RRMan_t * p )
     printf( "Edges removed   = %6d. (%5.2f %%)\n", p->nEdgesRemoved, 100.0*p->nEdgesRemoved/p->nEdgesTried );
     printf( "Node gain       = %6d. (%5.2f %%)\n", p->nNodesOld  - Abc_NtkNodeNum(p->pNtk), Ratio );
     printf( "Level gain      = %6d.\n", p->nLevelsOld - Abc_AigLevel(p->pNtk) );
-    PRT( "Windowing      ", p->timeWindow );
-    PRT( "Miter          ", p->timeMiter );
-    PRT( "    Construct  ", p->timeMiter - p->timeProve );
-    PRT( "    Prove      ", p->timeProve );
-    PRT( "Update         ", p->timeUpdate );
-    PRT( "TOTAL          ", p->timeTotal );
+    ABC_PRT( "Windowing      ", p->timeWindow );
+    ABC_PRT( "Miter          ", p->timeMiter );
+    ABC_PRT( "    Construct  ", p->timeMiter - p->timeProve );
+    ABC_PRT( "    Prove      ", p->timeProve );
+    ABC_PRT( "Update         ", p->timeUpdate );
+    ABC_PRT( "TOTAL          ", p->timeTotal );
 }
 
 /**Function*************************************************************
@@ -729,16 +729,16 @@ void Abc_NtkRRSimulateStart( Abc_Ntk_t * pNtk )
     int i;
     Abc_AigConst1(pNtk)->pData = (void *)~((unsigned)0);
     Abc_NtkForEachCi( pNtk, pObj, i )
-        pObj->pData = (void *)(PORT_PTRUINT_T)SIM_RANDOM_UNSIGNED;
+        pObj->pData = (void *)(ABC_PTRUINT_T)SIM_RANDOM_UNSIGNED;
     Abc_NtkForEachNode( pNtk, pObj, i )
     {
         if ( i == 0 ) continue;
-        uData0 = (unsigned)(PORT_PTRUINT_T)Abc_ObjFanin0(pObj)->pData;
-        uData1 = (unsigned)(PORT_PTRUINT_T)Abc_ObjFanin1(pObj)->pData;
+        uData0 = (unsigned)(ABC_PTRUINT_T)Abc_ObjFanin0(pObj)->pData;
+        uData1 = (unsigned)(ABC_PTRUINT_T)Abc_ObjFanin1(pObj)->pData;
         uData  = Abc_ObjFaninC0(pObj)? ~uData0 : uData0;
         uData &= Abc_ObjFaninC1(pObj)? ~uData1 : uData1;
         assert( pObj->pData == NULL );
-        pObj->pData = (void *)(PORT_PTRUINT_T)uData;
+        pObj->pData = (void *)(ABC_PTRUINT_T)uData;
     }
 }
 
@@ -802,24 +802,24 @@ Vec_Str_t * Abc_NtkRRSimulate( Abc_Ntk_t * pNtk )
     // simulate patters and store them in copy
     Abc_AigConst1(pNtk)->pCopy = (Abc_Obj_t *)~((unsigned)0);
     Abc_NtkForEachCi( pNtk, pObj, i )
-        pObj->pCopy = (Abc_Obj_t *)(PORT_PTRUINT_T)SIM_RANDOM_UNSIGNED;
+        pObj->pCopy = (Abc_Obj_t *)(ABC_PTRUINT_T)SIM_RANDOM_UNSIGNED;
     Abc_NtkForEachNode( pNtk, pObj, i )
     {
         if ( i == 0 ) continue;
-        uData0 = (unsigned)(PORT_PTRUINT_T)Abc_ObjFanin0(pObj)->pData;
-        uData1 = (unsigned)(PORT_PTRUINT_T)Abc_ObjFanin1(pObj)->pData;
+        uData0 = (unsigned)(ABC_PTRUINT_T)Abc_ObjFanin0(pObj)->pData;
+        uData1 = (unsigned)(ABC_PTRUINT_T)Abc_ObjFanin1(pObj)->pData;
         uData  = Abc_ObjFaninC0(pObj)? ~uData0 : uData0;
         uData &= Abc_ObjFaninC1(pObj)? ~uData1 : uData1;
-        pObj->pCopy = (Abc_Obj_t *)(PORT_PTRUINT_T)uData;
+        pObj->pCopy = (Abc_Obj_t *)(ABC_PTRUINT_T)uData;
     }
     // store the result in data
     Abc_NtkForEachCo( pNtk, pObj, i )
     {
-        uData0 = (unsigned)(PORT_PTRUINT_T)Abc_ObjFanin0(pObj)->pData;
+        uData0 = (unsigned)(ABC_PTRUINT_T)Abc_ObjFanin0(pObj)->pData;
         if ( Abc_ObjFaninC0(pObj) )
-            pObj->pData = (void *)(PORT_PTRUINT_T)~uData0;
+            pObj->pData = (void *)(ABC_PTRUINT_T)~uData0;
         else
-            pObj->pData = (void *)(PORT_PTRUINT_T)uData0;
+            pObj->pData = (void *)(ABC_PTRUINT_T)uData0;
     }
 
     // refine the candidates
@@ -904,7 +904,7 @@ void Sim_CollectNodes_rec( Abc_Obj_t * pRoot, Vec_Ptr_t * vField )
     Abc_ObjForEachFanin( pRoot, pFanin, i )
         Sim_CollectNodes_rec( pFanin, vField );
     if ( !Abc_ObjIsCo(pRoot) )
-        pRoot->pData = (void *)(PORT_PTRUINT_T)Vec_PtrSize(vField);
+        pRoot->pData = (void *)(ABC_PTRUINT_T)Vec_PtrSize(vField);
     Vec_PtrPush( vField, pRoot );
 }
 
@@ -934,13 +934,13 @@ void Sim_SimulateCollected( Vec_Str_t * vTargets, Vec_Ptr_t * vNodes, Vec_Ptr_t
         {
             pUnsigned = Vec_PtrEntry( vSims, i );
             for ( k = 0; k < Vec_PtrSize(vNodes); k++ )
-                pUnsigned[k] = (unsigned)(PORT_PTRUINT_T)pObj->pCopy;
+                pUnsigned[k] = (unsigned)(ABC_PTRUINT_T)pObj->pCopy;
             continue;
         }
         if ( Abc_ObjIsCo(pObj) )
         {
             pUnsigned  = Vec_PtrEntry( vSims, i );
-            pUnsignedF = Vec_PtrEntry( vSims, (int)(PORT_PTRUINT_T)Abc_ObjFanin0(pObj)->pData );
+            pUnsignedF = Vec_PtrEntry( vSims, (int)(ABC_PTRUINT_T)Abc_ObjFanin0(pObj)->pData );
             if ( Abc_ObjFaninC0(pObj) )
                 for ( k = 0; k < Vec_PtrSize(vNodes); k++ )
                     pUnsigned[k] = ~pUnsignedF[k];
@@ -950,7 +950,7 @@ void Sim_SimulateCollected( Vec_Str_t * vTargets, Vec_Ptr_t * vNodes, Vec_Ptr_t
             // update targets
             for ( k = 0; k < Vec_PtrSize(vNodes); k++ )
             {
-                if ( pUnsigned[k] == (unsigned)(PORT_PTRUINT_T)pObj->pData )
+                if ( pUnsigned[k] == (unsigned)(ABC_PTRUINT_T)pObj->pData )
                     continue;
                 pDisproved = Vec_PtrEntry( vNodes, k );
                 fCompl = Abc_ObjIsComplement(pDisproved);
diff --git a/src/base/abci/abcSat.c b/src/base/abci/abcSat.c
index 025652fe..3cee19ca 100644
--- a/src/base/abci/abcSat.c
+++ b/src/base/abci/abcSat.c
@@ -44,7 +44,7 @@ static int nMuxes;
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fVerbose, sint64 * pNumConfs, sint64 * pNumInspects )
+int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fVerbose, ABC_INT64_T * pNumConfs, ABC_INT64_T * pNumInspects )
 {
     sat_solver * pSat;
     lbool   status;
@@ -70,13 +70,13 @@ int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int
 //return 1;
 
 //    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 )
     {
         sat_solver_delete( pSat );
@@ -88,7 +88,7 @@ int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int
     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" );
@@ -106,7 +106,7 @@ int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int
     }
     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
@@ -117,7 +117,7 @@ int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int
         pNtk->pModel = Sat_SolverGetModel( pSat, vCiIds->pArray, vCiIds->nSize );
         Vec_IntFree( vCiIds );
     }
-    // free the sat_solver
+    // ABC_FREE the sat_solver
     if ( fVerbose )
         Sat_SolverPrintStats( stdout, pSat );
 
@@ -151,7 +151,7 @@ Vec_Int_t * Abc_NtkGetCiSatVarNums( Abc_Ntk_t * pNtk )
     int i;
     vCiIds = Vec_IntAlloc( Abc_NtkCiNum(pNtk) );
     Abc_NtkForEachCi( pNtk, pObj, i )
-        Vec_IntPush( vCiIds, (int)(PORT_PTRINT_T)pObj->pCopy );
+        Vec_IntPush( vCiIds, (int)(ABC_PTRINT_T)pObj->pCopy );
     return vCiIds;
 }
 
@@ -172,7 +172,7 @@ int Abc_NtkClauseTriv( sat_solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars )
 {
 //printf( "Adding triv %d.         %d\n", Abc_ObjRegular(pNode)->Id, (int)pSat->sat_solver_stats.clauses );
     vVars->nSize = 0;
-    Vec_IntPush( vVars, toLitCond( (int)(PORT_PTRINT_T)Abc_ObjRegular(pNode)->pCopy, Abc_ObjIsComplement(pNode) ) );
+    Vec_IntPush( vVars, toLitCond( (int)(ABC_PTRINT_T)Abc_ObjRegular(pNode)->pCopy, Abc_ObjIsComplement(pNode) ) );
 //    Vec_IntPush( vVars, toLitCond( (int)Abc_ObjRegular(pNode)->Id, Abc_ObjIsComplement(pNode) ) );
     return sat_solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
 }
@@ -195,7 +195,7 @@ int Abc_NtkClauseTop( sat_solver * pSat, Vec_Ptr_t * vNodes, Vec_Int_t * vVars )
 //printf( "Adding triv %d.         %d\n", Abc_ObjRegular(pNode)->Id, (int)pSat->sat_solver_stats.clauses );
     vVars->nSize = 0;
     Vec_PtrForEachEntry( vNodes, pNode, i )
-        Vec_IntPush( vVars, toLitCond( (int)(PORT_PTRINT_T)Abc_ObjRegular(pNode)->pCopy, Abc_ObjIsComplement(pNode) ) );
+        Vec_IntPush( vVars, toLitCond( (int)(ABC_PTRINT_T)Abc_ObjRegular(pNode)->pCopy, Abc_ObjIsComplement(pNode) ) );
 //    Vec_IntPush( vVars, toLitCond( (int)Abc_ObjRegular(pNode)->Id, Abc_ObjIsComplement(pNode) ) );
     return sat_solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
 }
@@ -220,7 +220,7 @@ int Abc_NtkClauseAnd( sat_solver * pSat, Abc_Obj_t * pNode, Vec_Ptr_t * vSuper,
     assert( Abc_ObjIsNode( pNode ) );
 
 //    nVars = sat_solver_nvars(pSat);
-    Var = (int)(PORT_PTRINT_T)pNode->pCopy;
+    Var = (int)(ABC_PTRINT_T)pNode->pCopy;
 //    Var = pNode->Id;
 
 //    assert( Var  < nVars ); 
@@ -230,7 +230,7 @@ int Abc_NtkClauseAnd( sat_solver * pSat, Abc_Obj_t * pNode, Vec_Ptr_t * vSuper,
         // get the complemented attributes of the nodes
         fComp1 = Abc_ObjIsComplement(vSuper->pArray[i]);
         // determine the variable numbers
-        Var1 = (int)(PORT_PTRINT_T)Abc_ObjRegular(vSuper->pArray[i])->pCopy;
+        Var1 = (int)(ABC_PTRINT_T)Abc_ObjRegular(vSuper->pArray[i])->pCopy;
 //        Var1 = (int)Abc_ObjRegular(vSuper->pArray[i])->Id;
 
         // check that the variables are in the SAT manager
@@ -255,7 +255,7 @@ int Abc_NtkClauseAnd( sat_solver * pSat, Abc_Obj_t * pNode, Vec_Ptr_t * vSuper,
         // get the complemented attributes of the nodes
         fComp1 = Abc_ObjIsComplement(vSuper->pArray[i]);
         // determine the variable numbers
-        Var1 = (int)(PORT_PTRINT_T)Abc_ObjRegular(vSuper->pArray[i])->pCopy;
+        Var1 = (int)(ABC_PTRINT_T)Abc_ObjRegular(vSuper->pArray[i])->pCopy;
 //        Var1 = (int)Abc_ObjRegular(vSuper->pArray[i])->Id;
         // add this variable to the array
         Vec_IntPush( vVars, toLitCond(Var1, !fComp1) );
@@ -283,10 +283,10 @@ int Abc_NtkClauseMux( sat_solver * pSat, Abc_Obj_t * pNode, Abc_Obj_t * pNodeC,
     assert( !Abc_ObjIsComplement( pNode ) );
     assert( Abc_NodeIsMuxType( pNode ) );
     // get the variable numbers
-    VarF = (int)(PORT_PTRINT_T)pNode->pCopy;
-    VarI = (int)(PORT_PTRINT_T)pNodeC->pCopy;
-    VarT = (int)(PORT_PTRINT_T)Abc_ObjRegular(pNodeT)->pCopy;
-    VarE = (int)(PORT_PTRINT_T)Abc_ObjRegular(pNodeE)->pCopy;
+    VarF = (int)(ABC_PTRINT_T)pNode->pCopy;
+    VarI = (int)(ABC_PTRINT_T)pNodeC->pCopy;
+    VarT = (int)(ABC_PTRINT_T)Abc_ObjRegular(pNodeT)->pCopy;
+    VarE = (int)(ABC_PTRINT_T)Abc_ObjRegular(pNodeE)->pCopy;
 //    VarF = (int)pNode->Id;
 //    VarI = (int)pNodeC->Id;
 //    VarT = (int)Abc_ObjRegular(pNodeT)->Id;
@@ -479,7 +479,7 @@ int Abc_NtkMiterSatCreateInt( sat_solver * pSat, Abc_Ntk_t * pNtk )
     // add the clause for the constant node
     pNode = Abc_AigConst1(pNtk);
     pNode->fMarkA = 1;
-    pNode->pCopy = (Abc_Obj_t *)(PORT_PTRINT_T)vNodes->nSize;
+    pNode->pCopy = (Abc_Obj_t *)(ABC_PTRINT_T)vNodes->nSize;
     Vec_PtrPush( vNodes, pNode );
     Abc_NtkClauseTriv( pSat, pNode, vVars );
 /*
@@ -501,7 +501,7 @@ int Abc_NtkMiterSatCreateInt( sat_solver * pSat, Abc_Ntk_t * pNtk )
         if ( pFanin->fMarkA == 0 )
         {
             pFanin->fMarkA = 1;
-            pFanin->pCopy = (Abc_Obj_t *)(PORT_PTRINT_T)vNodes->nSize;
+            pFanin->pCopy = (Abc_Obj_t *)(ABC_PTRINT_T)vNodes->nSize;
             Vec_PtrPush( vNodes, pFanin );
         }
         // add the trivial clause
@@ -536,7 +536,7 @@ int Abc_NtkMiterSatCreateInt( sat_solver * pSat, Abc_Ntk_t * pNtk )
                 if ( pFanin->fMarkA == 0 )
                 {
                     pFanin->fMarkA = 1;
-                    pFanin->pCopy = (Abc_Obj_t *)(PORT_PTRINT_T)vNodes->nSize;
+                    pFanin->pCopy = (Abc_Obj_t *)(ABC_PTRINT_T)vNodes->nSize;
                     Vec_PtrPush( vNodes, pFanin );
                 }
             }
@@ -555,7 +555,7 @@ int Abc_NtkMiterSatCreateInt( sat_solver * pSat, Abc_Ntk_t * pNtk )
                 if ( pFanin->fMarkA == 0 )
                 {
                     pFanin->fMarkA = 1;
-                    pFanin->pCopy = (Abc_Obj_t *)(PORT_PTRINT_T)vNodes->nSize;
+                    pFanin->pCopy = (Abc_Obj_t *)(ABC_PTRINT_T)vNodes->nSize;
                     Vec_PtrPush( vNodes, pFanin );
                 }
             }
@@ -577,7 +577,7 @@ int Abc_NtkMiterSatCreateInt( sat_solver * pSat, Abc_Ntk_t * pNtk )
     // set preferred variables
     if ( fOrderCiVarsFirst )
     {
-        int * pPrefVars = ALLOC( int, Abc_NtkCiNum(pNtk) );
+        int * pPrefVars = ABC_ALLOC( int, Abc_NtkCiNum(pNtk) );
         int nVars = 0;
         Abc_NtkForEachCi( pNtk, pNode, i )
         {
@@ -644,7 +644,7 @@ sat_solver_store_mark_roots( pSat );
         return NULL;
     }
 //    printf( "Ands = %6d.  Muxes = %6d (%5.2f %%).  ", Abc_NtkNodeNum(pNtk), nMuxes, 300.0*nMuxes/Abc_NtkNodeNum(pNtk) );
-//    PRT( "Creating sat_solver", clock() - clk );
+//    ABC_PRT( "Creating sat_solver", clock() - clk );
     return pSat;
 }
 
@@ -840,7 +840,7 @@ sat_solver * Abc_NtkMiterSatCreateLogic( Abc_Ntk_t * pNtk, int fAllPrimes )
 
     // transfer the IDs to the copy field
     Abc_NtkForEachPi( pNtk, pNode, i )
-        pNode->pCopy = (void *)(PORT_PTRINT_T)pNode->Id;
+        pNode->pCopy = (void *)(ABC_PTRINT_T)pNode->Id;
 
     // start the data structures
     pSat    = sat_solver_new();
@@ -945,9 +945,9 @@ void Abc_NtkWriteSorterCnf( char * pFileName, int nVars, int nQueens )
     Abc_NtkForEachObj( pNtk, pObj, i )
         pObj->pCopy = (void *)~0;
     Abc_NtkForEachPi( pNtk, pObj, i )
-        pObj->pCopy = (void *)(PORT_PTRINT_T)Counter++;
+        pObj->pCopy = (void *)(ABC_PTRINT_T)Counter++;
     Vec_PtrForEachEntry( vNodes, pObj, i )
-        pObj->pCopy = (void *)(PORT_PTRINT_T)Counter++;
+        pObj->pCopy = (void *)(ABC_PTRINT_T)Counter++;
 
 /*
         OutVar   = pCnf->pVarNums[ pObj->Id ];
@@ -975,14 +975,14 @@ void Abc_NtkWriteSorterCnf( char * pFileName, int nVars, int nQueens )
     Vec_PtrForEachEntry( vNodes, pObj, i )
     {
         // positive phase
-        fprintf( pFile, "%d %s%d %s%d 0\n", 1+(int)(PORT_PTRINT_T)pObj->pCopy,
-            Abc_ObjFaninC0(pObj)? "" : "-", 1+(int)(PORT_PTRINT_T)Abc_ObjFanin0(pObj)->pCopy,
-            Abc_ObjFaninC1(pObj)? "" : "-", 1+(int)(PORT_PTRINT_T)Abc_ObjFanin1(pObj)->pCopy );
+        fprintf( pFile, "%d %s%d %s%d 0\n", 1+(int)(ABC_PTRINT_T)pObj->pCopy,
+            Abc_ObjFaninC0(pObj)? "" : "-", 1+(int)(ABC_PTRINT_T)Abc_ObjFanin0(pObj)->pCopy,
+            Abc_ObjFaninC1(pObj)? "" : "-", 1+(int)(ABC_PTRINT_T)Abc_ObjFanin1(pObj)->pCopy );
         // negative phase
-        fprintf( pFile, "-%d %s%d 0\n",     1+(int)(PORT_PTRINT_T)pObj->pCopy,
-            Abc_ObjFaninC0(pObj)? "-" : "", 1+(int)(PORT_PTRINT_T)Abc_ObjFanin0(pObj)->pCopy );
-        fprintf( pFile, "-%d %s%d 0\n",     1+(int)(PORT_PTRINT_T)pObj->pCopy,
-            Abc_ObjFaninC1(pObj)? "-" : "", 1+(int)(PORT_PTRINT_T)Abc_ObjFanin1(pObj)->pCopy );
+        fprintf( pFile, "-%d %s%d 0\n",     1+(int)(ABC_PTRINT_T)pObj->pCopy,
+            Abc_ObjFaninC0(pObj)? "-" : "", 1+(int)(ABC_PTRINT_T)Abc_ObjFanin0(pObj)->pCopy );
+        fprintf( pFile, "-%d %s%d 0\n",     1+(int)(ABC_PTRINT_T)pObj->pCopy,
+            Abc_ObjFaninC1(pObj)? "-" : "", 1+(int)(ABC_PTRINT_T)Abc_ObjFanin1(pObj)->pCopy );
     }
     Vec_PtrFree( vNodes );
 
@@ -992,10 +992,10 @@ void Abc_NtkWriteSorterCnf( char * pFileName, int nVars, int nQueens )
 */
     // assert the first literal to zero
     fprintf( pFile, "%s%d 0\n", 
-        Abc_ObjFaninC0(ppNodes[0])? "" : "-", 1+(int)(PORT_PTRINT_T)Abc_ObjFanin0(ppNodes[0])->pCopy );
+        Abc_ObjFaninC0(ppNodes[0])? "" : "-", 1+(int)(ABC_PTRINT_T)Abc_ObjFanin0(ppNodes[0])->pCopy );
     // assert the second literal to one
     fprintf( pFile, "%s%d 0\n", 
-        Abc_ObjFaninC0(ppNodes[1])? "-" : "", 1+(int)(PORT_PTRINT_T)Abc_ObjFanin0(ppNodes[1])->pCopy );
+        Abc_ObjFaninC0(ppNodes[1])? "-" : "", 1+(int)(ABC_PTRINT_T)Abc_ObjFanin0(ppNodes[1])->pCopy );
     fclose( pFile );
 }
 
diff --git a/src/base/abci/abcSense.c b/src/base/abci/abcSense.c
index a1e5b98a..3e68f0fd 100644
--- a/src/base/abci/abcSense.c
+++ b/src/base/abci/abcSense.c
@@ -184,7 +184,7 @@ Vec_Int_t * Abc_NtkSensitivity( Abc_Ntk_t * pNtk, int nConfLim, int fVerbose )
                 printf( "ERROR in Abc_NtkMiterProve(): Generated counter-example is invalid.\n" );
 //            else
 //                printf( "Networks are NOT EQUIVALENT.\n" );
-            free( pSimInfo );
+            ABC_FREE( pSimInfo );
             Vec_IntPush( vResult, i );
         }
         Abc_NtkDelete( pMiter );
diff --git a/src/base/abci/abcStrash.c b/src/base/abci/abcStrash.c
index a7c9f609..114288ba 100644
--- a/src/base/abci/abcStrash.c
+++ b/src/base/abci/abcStrash.c
@@ -325,7 +325,7 @@ void Abc_NtkStrashPerform( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtkNew, int fAllNod
 //    vNodes = Abc_NtkDfs( pNtkOld, fAllNodes );
     vNodes = Abc_NtkDfsIter( pNtkOld, fAllNodes );
 //printf( "Nodes = %d. ", Vec_PtrSize(vNodes) );
-//PRT( "Time", clock() - clk );
+//ABC_PRT( "Time", clock() - clk );
 //    pProgress = Extra_ProgressBarStart( stdout, vNodes->nSize );
     Vec_PtrForEachEntry( vNodes, pNodeOld, i )
     {
@@ -385,6 +385,7 @@ Abc_Obj_t * Abc_NodeStrash( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld, int fReco
     if ( Abc_NodeIsConst(pNodeOld) || Hop_Regular(pRoot) == Hop_ManConst1(pMan) )
         return Abc_ObjNotCond( Abc_AigConst1(pNtkNew), Hop_IsComplement(pRoot) );
     // perform special case-strashing using the record of AIG subgraphs
+/*
     if ( fRecord && Abc_NtkRecIsRunning() && Abc_ObjFaninNum(pNodeOld) > 2 && Abc_ObjFaninNum(pNodeOld) <= Abc_NtkRecVarNum() )
     {
         extern Vec_Int_t * Abc_NtkRecMemory();
@@ -398,6 +399,7 @@ Abc_Obj_t * Abc_NodeStrash( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld, int fReco
         if ( Abc_NtkRecStrashNode( pNtkNew, pNodeOld, pTruth, nVars ) )
             return pNodeOld->pCopy;
     }
+*/
     // set elementary variables
     Abc_ObjForEachFanin( pNodeOld, pFanin, i )
         Hop_IthVar(pMan, i)->pData = pFanin->pCopy;
diff --git a/src/base/abci/abcSweep.c b/src/base/abci/abcSweep.c
index 2b78ceae..d1f4d4f7 100644
--- a/src/base/abci/abcSweep.c
+++ b/src/base/abci/abcSweep.c
@@ -111,7 +111,7 @@ bool Abc_NtkFraigSweep( Abc_Ntk_t * pNtk, int fUseInv, int fExdc, int fVerbose,
     Abc_NtkFraigTransform( pNtk, tEquiv, fUseInv, fVerbose );
     stmm_free_table( tEquiv );
 
-    // free the manager
+    // ABC_FREE the manager
     Fraig_ManFree( pMan );
     Abc_NtkDelete( pNtkAig );
 
@@ -835,7 +835,7 @@ int Abc_NtkLatchSweep( Abc_Ntk_t * pNtk )
 
 /**Function*************************************************************
 
-  Synopsis    [Replaces autonumnous logic by free inputs.]
+  Synopsis    [Replaces autonumnous logic by ABC_FREE inputs.]
 
   Description [Assumes that non-autonomous logic is marked with
   the current ID.]
diff --git a/src/base/abci/abcSymm.c b/src/base/abci/abcSymm.c
index 0f76065c..73f238f9 100644
--- a/src/base/abci/abcSymm.c
+++ b/src/base/abci/abcSymm.c
@@ -105,9 +105,9 @@ clkSym = clock() - clk;
 printf( "Statistics of BDD-based symmetry detection:\n" );
 printf( "Algorithm = %s. Reordering = %s. Garbage collection = %s.\n", 
        fNaive? "naive" : "fast", fReorder? "yes" : "no", fGarbCollect? "yes" : "no" );
-PRT( "Constructing BDDs", clkBdd );
-PRT( "Computing symms  ", clkSym );
-PRT( "TOTAL            ", clkBdd + clkSym );
+ABC_PRT( "Constructing BDDs", clkBdd );
+ABC_PRT( "Computing symms  ", clkSym );
+ABC_PRT( "TOTAL            ", clkBdd + clkSym );
 }
 
 /**Function*************************************************************
@@ -177,7 +177,7 @@ void Ntk_NetworkSymmsPrint( Abc_Ntk_t * pNtk, Extra_SymmInfo_t * pSymms )
     pInputNames = Abc_NtkCollectCioNames( pNtk, 0 );
 
     // alloc the array of marks
-    pVarTaken = ALLOC( int, nVars );
+    pVarTaken = ABC_ALLOC( int, nVars );
     memset( pVarTaken, 0, sizeof(int) * nVars );
 
     // print the groups
@@ -217,8 +217,8 @@ void Ntk_NetworkSymmsPrint( Abc_Ntk_t * pNtk, Extra_SymmInfo_t * pSymms )
     }   
     printf( "\n" );
 
-    free( pInputNames );
-    free( pVarTaken );
+    ABC_FREE( pInputNames );
+    ABC_FREE( pVarTaken );
 }
 
 
diff --git a/src/base/abci/abcTiming.c b/src/base/abci/abcTiming.c
index be16da95..36e56e7b 100644
--- a/src/base/abci/abcTiming.c
+++ b/src/base/abci/abcTiming.c
@@ -320,7 +320,7 @@ void Abc_NtkTimePrepare( Abc_Ntk_t * pNtk )
 Abc_ManTime_t * Abc_ManTimeStart()
 {
     Abc_ManTime_t * p;
-    p = ALLOC( Abc_ManTime_t, 1 );
+    p = ABC_ALLOC( Abc_ManTime_t, 1 );
     memset( p, 0, sizeof(Abc_ManTime_t) );
     p->vArrs = Vec_PtrAlloc( 0 );
     p->vReqs = Vec_PtrAlloc( 0 );
@@ -342,15 +342,15 @@ void Abc_ManTimeStop( Abc_ManTime_t * p )
 {
     if ( p->vArrs->nSize > 0 )
     {
-        free( p->vArrs->pArray[0] );
+        ABC_FREE( p->vArrs->pArray[0] );
         Vec_PtrFree( p->vArrs );
     }
     if ( p->vReqs->nSize > 0 )
     {
-        free( p->vReqs->pArray[0] );
+        ABC_FREE( p->vReqs->pArray[0] );
         Vec_PtrFree( p->vReqs );
     }
-    free( p );
+    ABC_FREE( p );
 }
 
 /**Function*************************************************************
@@ -420,7 +420,7 @@ void Abc_ManTimeExpand( Abc_ManTime_t * p, int nSize, int fProgressive )
     Vec_PtrGrow( vTimes, nSizeNew );
     vTimes->nSize = nSizeNew;
     ppTimesOld = ( nSizeOld == 0 )? NULL : vTimes->pArray[0];
-    ppTimes = REALLOC( Abc_Time_t, ppTimesOld, nSizeNew );
+    ppTimes = ABC_REALLOC( Abc_Time_t, ppTimesOld, nSizeNew );
     for ( i = 0; i < nSizeNew; i++ )
         vTimes->pArray[i] = ppTimes + i;
     for ( i = nSizeOld; i < nSizeNew; i++ )
@@ -435,7 +435,7 @@ void Abc_ManTimeExpand( Abc_ManTime_t * p, int nSize, int fProgressive )
     Vec_PtrGrow( vTimes, nSizeNew );
     vTimes->nSize = nSizeNew;
     ppTimesOld = ( nSizeOld == 0 )? NULL : vTimes->pArray[0];
-    ppTimes = REALLOC( Abc_Time_t, ppTimesOld, nSizeNew );
+    ppTimes = ABC_REALLOC( Abc_Time_t, ppTimesOld, nSizeNew );
     for ( i = 0; i < nSizeNew; i++ )
         vTimes->pArray[i] = ppTimes + i;
     for ( i = nSizeOld; i < nSizeNew; i++ )
@@ -496,7 +496,7 @@ Abc_Time_t * Abc_NtkGetCiArrivalTimes( Abc_Ntk_t * pNtk )
     Abc_Time_t * p;
     Abc_Obj_t * pNode;
     int i;
-    p = ALLOC( Abc_Time_t, Abc_NtkCiNum(pNtk) );
+    p = ABC_ALLOC( Abc_Time_t, Abc_NtkCiNum(pNtk) );
     memset( p, 0, sizeof(Abc_Time_t) * Abc_NtkCiNum(pNtk) );
     if ( pNtk->pManTime == NULL )
         return p;
@@ -523,7 +523,7 @@ float * Abc_NtkGetCiArrivalFloats( Abc_Ntk_t * pNtk )
     float * p;
     Abc_Obj_t * pNode;
     int i;
-    p = ALLOC( float, Abc_NtkCiNum(pNtk) );
+    p = ABC_ALLOC( float, Abc_NtkCiNum(pNtk) );
     memset( p, 0, sizeof(float) * Abc_NtkCiNum(pNtk) );
     if ( pNtk->pManTime == NULL )
         return p;
diff --git a/src/base/abci/abcUnate.c b/src/base/abci/abcUnate.c
index 20804d19..f6ee57ca 100644
--- a/src/base/abci/abcUnate.c
+++ b/src/base/abci/abcUnate.c
@@ -121,9 +121,9 @@ clkUnate = clock() - clk - clkBdd;
     // print stats
     printf( "Ins/Outs = %4d/%4d.  Total supp = %5d.  Total unate = %5d.\n",
         Abc_NtkCiNum(pNtk), Abc_NtkCoNum(pNtk), TotalSupps, TotalUnate );
-    PRT( "Glob BDDs", clkBdd );
-    PRT( "Unateness", clkUnate );
-    PRT( "Total    ", clock() - clk );
+    ABC_PRT( "Glob BDDs", clkBdd );
+    ABC_PRT( "Unateness", clkUnate );
+    ABC_PRT( "Total    ", clock() - clk );
 
     // deref the PO functions
 //    Abc_NtkFreeGlobalBdds( pNtk );
diff --git a/src/base/abci/abcUnreach.c b/src/base/abci/abcUnreach.c
index ea0a4cd2..196ff643 100644
--- a/src/base/abci/abcUnreach.c
+++ b/src/base/abci/abcUnreach.c
@@ -143,7 +143,7 @@ DdNode * Abc_NtkTransitionRelation( DdManager * dd, Abc_Ntk_t * pNtk, int fVerbo
         Cudd_RecursiveDeref( dd, bTemp ); 
         Cudd_RecursiveDeref( dd, bProd ); 
     }
-    // free the global BDDs
+    // ABC_FREE the global BDDs
 //    Abc_NtkFreeGlobalBdds( pNtk );
     Abc_NtkFreeGlobalBdds( pNtk, 0 );
 
@@ -186,8 +186,8 @@ DdNode * Abc_NtkInitStateAndVarMap( DdManager * dd, Abc_Ntk_t * pNtk, int fVerbo
     int i;
 
     // set the variable mapping for Cudd_bddVarMap()
-    pbVarsX = ALLOC( DdNode *, dd->size );
-    pbVarsY = ALLOC( DdNode *, dd->size );
+    pbVarsX = ABC_ALLOC( DdNode *, dd->size );
+    pbVarsY = ABC_ALLOC( DdNode *, dd->size );
     bProd = b1;         Cudd_Ref( bProd );
     Abc_NtkForEachLatch( pNtk, pLatch, i )
     {
@@ -199,8 +199,8 @@ DdNode * Abc_NtkInitStateAndVarMap( DdManager * dd, Abc_Ntk_t * pNtk, int fVerbo
         Cudd_RecursiveDeref( dd, bTemp ); 
     }
     Cudd_SetVarMap( dd, pbVarsX, pbVarsY, Abc_NtkLatchNum(pNtk) );
-    FREE( pbVarsX );
-    FREE( pbVarsY );
+    ABC_FREE( pbVarsX );
+    ABC_FREE( pbVarsY );
 
     Cudd_Deref( bProd );
     return bProd;
@@ -262,7 +262,7 @@ DdNode * Abc_NtkComputeUnreachable( DdManager * dd, Abc_Ntk_t * pNtk, DdNode * b
         fprintf( stdout, "Reachability analysis completed in %d iterations.\n", nIters );
         fprintf( stdout, "The number of minterms in the reachable state set = %d. (%6.2f %%)\n", nMints, 100.0*nMints/(1<<Abc_NtkLatchNum(pNtk)) );
     }
-//PRB( dd, bReached );
+//ABC_PRB( dd, bReached );
     Cudd_Deref( bReached );
     return Cudd_Not( bReached );
 }
@@ -302,14 +302,14 @@ Abc_Ntk_t * Abc_NtkConstructExdc( DdManager * dd, Abc_Ntk_t * pNtk, DdNode * bUn
         Abc_ObjAddFanin( pNodeNew, pNode->pCopy );
 
     // create the logic function
-    pPermute = ALLOC( int, dd->size );
+    pPermute = ABC_ALLOC( int, dd->size );
     for ( i = 0; i < dd->size; i++ )
         pPermute[i] = -1;
     Abc_NtkForEachLatch( pNtk, pNode, i )
         pPermute[Abc_NtkPiNum(pNtk) + i] = i;
     // remap the functions
     pNodeNew->pData = Extra_TransferPermute( dd, pNtkNew->pManFunc, bUnreach, pPermute );   Cudd_Ref( pNodeNew->pData );
-    free( pPermute );
+    ABC_FREE( pPermute );
     Abc_NodeMinimumBase( pNodeNew );
 
     // for each CO, create PO (skip POs equal to CIs because of name conflict)
diff --git a/src/base/abci/abcVerify.c b/src/base/abci/abcVerify.c
index 1131f119..60197d29 100644
--- a/src/base/abci/abcVerify.c
+++ b/src/base/abci/abcVerify.c
@@ -65,7 +65,7 @@ void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nI
         // report the error
         pMiter->pModel = Abc_NtkVerifyGetCleanModel( pMiter, 1 );
         Abc_NtkVerifyReportError( pNtk1, pNtk2, pMiter->pModel );
-        FREE( pMiter->pModel );
+        ABC_FREE( pMiter->pModel );
         Abc_NtkDelete( pMiter );
         return;
     }
@@ -86,7 +86,7 @@ void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nI
     }
 
     // solve the CNF using the SAT solver
-    RetValue = Abc_NtkMiterSat( pCnf, (sint64)nConfLimit, (sint64)nInsLimit, 0, NULL, NULL );
+    RetValue = Abc_NtkMiterSat( pCnf, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)nInsLimit, 0, NULL, NULL );
     if ( RetValue == -1 )
         printf( "Networks are undecided (SAT solver timed out).\n" );
     else if ( RetValue == 0 )
@@ -95,7 +95,7 @@ void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nI
         printf( "Networks are equivalent after SAT.\n" );
     if ( pCnf->pModel )
         Abc_NtkVerifyReportError( pNtk1, pNtk2, pCnf->pModel );
-    FREE( pCnf->pModel );
+    ABC_FREE( pCnf->pModel );
     Abc_NtkDelete( pCnf );
 }
 
@@ -133,7 +133,7 @@ void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fV
         // report the error
         pMiter->pModel = Abc_NtkVerifyGetCleanModel( pMiter, 1 );
         Abc_NtkVerifyReportError( pNtk1, pNtk2, pMiter->pModel );
-        FREE( pMiter->pModel );
+        ABC_FREE( pMiter->pModel );
         Abc_NtkDelete( pMiter );
         return;
     }
@@ -187,7 +187,7 @@ void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fV
             printf( "ERROR in Abc_NtkMiterProve(): Generated counter-example is invalid.\n" );
         else
             printf( "Networks are NOT EQUIVALENT.\n" );
-        free( pSimInfo );
+        ABC_FREE( pSimInfo );
     }
     else
         printf( "Networks are equivalent.\n" );
@@ -238,7 +238,7 @@ void Abc_NtkCecFraigPart( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, in
         // report the error
         pMiter->pModel = Abc_NtkVerifyGetCleanModel( pMiter, 1 );
         Abc_NtkVerifyReportError( pNtk1, pNtk2, pMiter->pModel );
-        FREE( pMiter->pModel );
+        ABC_FREE( pMiter->pModel );
         Abc_NtkDelete( pMiter );
         return;
     }
@@ -287,7 +287,7 @@ void Abc_NtkCecFraigPart( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, in
                 printf( "ERROR in Abc_NtkMiterProve(): Generated counter-example is invalid.\n" );
             else
                 printf( "Networks are NOT EQUIVALENT.                 \n" );
-            free( pSimInfo );
+            ABC_FREE( pSimInfo );
             Status = 0;
             break;
         }
@@ -355,7 +355,7 @@ void Abc_NtkCecFraigPartAuto( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds
         // report the error
         pMiter->pModel = Abc_NtkVerifyGetCleanModel( pMiter, 1 );
         Abc_NtkVerifyReportError( pNtk1, pNtk2, pMiter->pModel );
-        FREE( pMiter->pModel );
+        ABC_FREE( pMiter->pModel );
         Abc_NtkDelete( pMiter );
         return;
     }
@@ -412,7 +412,7 @@ void Abc_NtkCecFraigPartAuto( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds
                 printf( "ERROR in Abc_NtkMiterProve(): Generated counter-example is invalid.\n" );
             else
                 printf( "Networks are NOT EQUIVALENT.                 \n" );
-            free( pSimInfo );
+            ABC_FREE( pSimInfo );
             Status = 0;
             Abc_NtkDelete( pMiterPart );
             break;
@@ -509,7 +509,7 @@ void Abc_NtkSecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nI
     }
 
     // solve the CNF using the SAT solver
-    RetValue = Abc_NtkMiterSat( pCnf, (sint64)nConfLimit, (sint64)nInsLimit, 0, NULL, NULL );
+    RetValue = Abc_NtkMiterSat( pCnf, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)nInsLimit, 0, NULL, NULL );
     if ( RetValue == -1 )
         printf( "Networks are undecided (SAT solver timed out).\n" );
     else if ( RetValue == 0 )
@@ -552,7 +552,7 @@ int Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nFr
         // report the error
         pMiter->pModel = Abc_NtkVerifyGetCleanModel( pMiter, nFrames );
         Abc_NtkVerifyReportErrorSeq( pNtk1, pNtk2, pMiter->pModel, nFrames );
-        FREE( pMiter->pModel );
+        ABC_FREE( pMiter->pModel );
         Abc_NtkDelete( pMiter );
         return 0;
     }
@@ -578,7 +578,7 @@ int Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nFr
         // report the error
         pFrames->pModel = Abc_NtkVerifyGetCleanModel( pFrames, 1 );
 //        Abc_NtkVerifyReportErrorSeq( pNtk1, pNtk2, pFrames->pModel, nFrames );
-        FREE( pFrames->pModel );
+        ABC_FREE( pFrames->pModel );
         Abc_NtkDelete( pFrames );
         return 0;
     }
@@ -632,7 +632,7 @@ int Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nFr
 ***********************************************************************/
 int * Abc_NtkVerifyGetCleanModel( Abc_Ntk_t * pNtk, int nFrames )
 {
-    int * pModel = ALLOC( int, Abc_NtkCiNum(pNtk) * nFrames );
+    int * pModel = ABC_ALLOC( int, Abc_NtkCiNum(pNtk) * nFrames );
     memset( pModel, 0, sizeof(int) * Abc_NtkCiNum(pNtk) * nFrames );
     return pModel;
 }
@@ -669,18 +669,18 @@ int * Abc_NtkVerifySimulatePattern( Abc_Ntk_t * pNtk, int * pModel )
     // set the CI values
     Abc_AigConst1(pNtk)->pCopy = (void *)1;
     Abc_NtkForEachCi( pNtk, pNode, i )
-        pNode->pCopy = (void *)(PORT_PTRINT_T)pModel[i];
+        pNode->pCopy = (void *)(ABC_PTRINT_T)pModel[i];
     // simulate in the topological order
     Abc_NtkForEachNode( pNtk, pNode, i )
     {
-        Value0 = ((int)(PORT_PTRINT_T)Abc_ObjFanin0(pNode)->pCopy) ^ Abc_ObjFaninC0(pNode);
-        Value1 = ((int)(PORT_PTRINT_T)Abc_ObjFanin1(pNode)->pCopy) ^ Abc_ObjFaninC1(pNode);
-        pNode->pCopy = (void *)(PORT_PTRINT_T)(Value0 & Value1);
+        Value0 = ((int)(ABC_PTRINT_T)Abc_ObjFanin0(pNode)->pCopy) ^ Abc_ObjFaninC0(pNode);
+        Value1 = ((int)(ABC_PTRINT_T)Abc_ObjFanin1(pNode)->pCopy) ^ Abc_ObjFaninC1(pNode);
+        pNode->pCopy = (void *)(ABC_PTRINT_T)(Value0 & Value1);
     }
     // fill the output values
-    pValues = ALLOC( int, Abc_NtkCoNum(pNtk) );
+    pValues = ABC_ALLOC( int, Abc_NtkCoNum(pNtk) );
     Abc_NtkForEachCo( pNtk, pNode, i )
-        pValues[i] = ((int)(PORT_PTRINT_T)Abc_ObjFanin0(pNode)->pCopy) ^ Abc_ObjFaninC0(pNode);
+        pValues[i] = ((int)(ABC_PTRINT_T)Abc_ObjFanin0(pNode)->pCopy) ^ Abc_ObjFaninC0(pNode);
     if ( fStrashed )
         Abc_NtkDelete( pNtk );
     return pValues;
@@ -740,7 +740,7 @@ void Abc_NtkVerifyReportError( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pMode
         vNodes = Abc_NtkNodeSupport( pNtk1, &pNode, 1 );
         // set the PI numbers
         Abc_NtkForEachCi( pNtk1, pNode, i )
-            pNode->pCopy = (void*)(PORT_PTRINT_T)i;
+            pNode->pCopy = (void*)(ABC_PTRINT_T)i;
         // print the model
         pNode = Vec_PtrEntry( vNodes, 0 );
         if ( Abc_ObjIsCi(pNode) )
@@ -748,14 +748,14 @@ void Abc_NtkVerifyReportError( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pMode
             Vec_PtrForEachEntry( vNodes, pNode, i )
             {
                 assert( Abc_ObjIsCi(pNode) );
-                printf( " %s=%d", Abc_ObjName(pNode), pModel[(int)(PORT_PTRINT_T)pNode->pCopy] );
+                printf( " %s=%d", Abc_ObjName(pNode), pModel[(int)(ABC_PTRINT_T)pNode->pCopy] );
             }
         }
         printf( "\n" );
         Vec_PtrFree( vNodes );
     }
-    free( pValues1 );
-    free( pValues2 );
+    ABC_FREE( pValues1 );
+    ABC_FREE( pValues2 );
 }
 
 
@@ -799,7 +799,7 @@ void Abc_NtkGetSeqPoSupp( Abc_Ntk_t * pNtk, int iFrame, int iNumPo )
         for ( k = 0; k <= iFrame; k++ )
             if ( Abc_NtkPi(pFrames, k*Abc_NtkPiNum(pNtk) + i)->pCopy )
                 pObj->pCopy = (void *)1;
-    // free stuff
+    // ABC_FREE stuff
     Vec_PtrFree( vSupp );
     Abc_NtkDelete( pFrames );
 }
@@ -987,16 +987,16 @@ void Abc_NtkSimulteBuggyMiter( Abc_Ntk_t * pNtk )
     assert( strlen(vPiValues1) == (unsigned)Abc_NtkPiNum(pNtk) );
     assert( 1 == Abc_NtkPoNum(pNtk) );
 
-    pModel1 = ALLOC( int, Abc_NtkCiNum(pNtk) );
+    pModel1 = ABC_ALLOC( int, Abc_NtkCiNum(pNtk) );
     Abc_NtkForEachPi( pNtk, pObj, i )
         pModel1[i] = vPiValues1[i] - '0';
     Abc_NtkForEachLatch( pNtk, pObj, i )
-        pModel1[Abc_NtkPiNum(pNtk)+i] = ((int)(PORT_PTRINT_T)pObj->pData) - 1;
+        pModel1[Abc_NtkPiNum(pNtk)+i] = ((int)(ABC_PTRINT_T)pObj->pData) - 1;
 
     pResult1 = Abc_NtkVerifySimulatePattern( pNtk, pModel1 );
     printf( "Value = %d\n", pResult1[0] );
 
-    pModel2 = ALLOC( int, Abc_NtkCiNum(pNtk) );
+    pModel2 = ABC_ALLOC( int, Abc_NtkCiNum(pNtk) );
     Abc_NtkForEachPi( pNtk, pObj, i )
         pModel2[i] = vPiValues2[i] - '0';
     Abc_NtkForEachLatch( pNtk, pObj, i )
@@ -1005,10 +1005,10 @@ void Abc_NtkSimulteBuggyMiter( Abc_Ntk_t * pNtk )
     pResult2 = Abc_NtkVerifySimulatePattern( pNtk, pModel2 );
     printf( "Value = %d\n", pResult2[0] );
 
-    free( pModel1 );
-    free( pModel2 );
-    free( pResult1 );
-    free( pResult2 );
+    ABC_FREE( pModel1 );
+    ABC_FREE( pModel2 );
+    ABC_FREE( pResult1 );
+    ABC_FREE( pResult2 );
 }
 
 
diff --git a/src/base/abci/abcXsim.c b/src/base/abci/abcXsim.c
index 87739572..e63b296a 100644
--- a/src/base/abci/abcXsim.c
+++ b/src/base/abci/abcXsim.c
@@ -28,8 +28,8 @@
 #define XVS1   ABC_INIT_ONE
 #define XVSX   ABC_INIT_DC
 
-static inline void Abc_ObjSetXsim( Abc_Obj_t * pObj, int Value )  { pObj->pCopy = (void *)(PORT_PTRINT_T)Value;  }
-static inline int  Abc_ObjGetXsim( Abc_Obj_t * pObj )             { return (int)(PORT_PTRINT_T)pObj->pCopy;      }
+static inline void Abc_ObjSetXsim( Abc_Obj_t * pObj, int Value )  { pObj->pCopy = (void *)(ABC_PTRINT_T)Value;  }
+static inline int  Abc_ObjGetXsim( Abc_Obj_t * pObj )             { return (int)(ABC_PTRINT_T)pObj->pCopy;      }
 static inline int  Abc_XsimInv( int Value )   
 { 
     if ( Value == XVS0 )
@@ -214,7 +214,7 @@ void Abc_NtkCycleInitState( Abc_Ntk_t * pNtk, int nFrames, int fVerbose )
     }
     // set the final values
     Abc_NtkForEachLatch( pNtk, pObj, i )
-        pObj->pData = (void *)(PORT_PTRINT_T)Abc_ObjGetXsim(Abc_ObjFanout0(pObj));
+        pObj->pData = (void *)(ABC_PTRINT_T)Abc_ObjGetXsim(Abc_ObjFanout0(pObj));
 }
 
 ///////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/module.make b/src/base/abci/module.make
index c872d62e..e520dcce 100644
--- a/src/base/abci/module.make
+++ b/src/base/abci/module.make
@@ -37,7 +37,6 @@ SRC +=    src/base/abci/abc.c \
     src/base/abci/abcProve.c \
     src/base/abci/abcQbf.c \
     src/base/abci/abcQuant.c \
-    src/base/abci/abcRec.c \
     src/base/abci/abcReconv.c \
     src/base/abci/abcReach.c \
     src/base/abci/abcRefactor.c \