Adding a wrapper around clock() for more accurate time counting in ABC.

60 files changed, 485 insertions, 485 deletions

diff --git a/src/opt/cgt/cgtCore.c b/src/opt/cgt/cgtCore.c
index a24b180b..a7b3844c 100644
--- a/src/opt/cgt/cgtCore.c
+++ b/src/opt/cgt/cgtCore.c
@@ -201,19 +201,19 @@ void Cgt_ClockGatingRangeCheck( Cgt_Man_t * p, int iStart, int nOutputs )
 int Cgt_ClockGatingRange( Cgt_Man_t * p, int iStart )
 {
     int nOutputs, iStop;
-    clock_t clk, clkTotal = clock();
+    abctime clk, clkTotal = Abc_Clock();
     int nCallsUnsat    = p->nCallsUnsat;
     int nCallsSat      = p->nCallsSat;
     int nCallsUndec    = p->nCallsUndec;
     int nCallsFiltered = p->nCallsFiltered;
-clk = clock();
+clk = Abc_Clock();
     p->pPart = Cgt_ManDupPartition( p->pFrame, p->pPars->nVarsMin, p->pPars->nFlopsMin, iStart, p->pCare, p->vSuppsInv, &nOutputs );
     p->pCnf  = Cnf_DeriveSimple( p->pPart, nOutputs );
     p->pSat  = (sat_solver *)Cnf_DataWriteIntoSolver( p->pCnf, 1, 0 );
     sat_solver_compress( p->pSat );
     p->vPatts = Vec_PtrAllocSimInfo( Aig_ManObjNumMax(p->pPart), p->nPattWords );
     Vec_PtrCleanSimInfo( p->vPatts, 0, p->nPattWords );
-p->timePrepare += clock() - clk;
+p->timePrepare += Abc_Clock() - clk;
     Cgt_ClockGatingRangeCheck( p, iStart, nOutputs );
     iStop = iStart + nOutputs;
     if ( p->pPars->fVeryVerbose )
@@ -224,7 +224,7 @@ p->timePrepare += clock() - clk;
             p->nCallsSat  -nCallsSat, 
             p->nCallsUndec-nCallsUndec,
             p->nCallsFiltered-nCallsFiltered );
-        ABC_PRT( "Time", clock() - clkTotal );
+        ABC_PRT( "Time", Abc_Clock() - clkTotal );
     }
     Cgt_ManClean( p );
     p->nRecycles++;
@@ -249,14 +249,14 @@ Vec_Vec_t * Cgt_ClockGatingCandidates( Aig_Man_t * pAig, Aig_Man_t * pCare, Cgt_
     Cgt_Man_t * p;
     Vec_Vec_t * vGatesAll;
     int iStart;
-    clock_t clk = clock(), clkTotal = clock();
+    abctime clk = Abc_Clock(), clkTotal = Abc_Clock();
     // reset random numbers
     Aig_ManRandom( 1 );
     if ( pPars == NULL )
         Cgt_SetDefaultParams( pPars = &Pars );    
     p = Cgt_ManCreate( pAig, pCare, pPars );
     p->pFrame = Cgt_ManDeriveAigForGating( p );
-p->timeAig += clock() - clk;
+p->timeAig += Abc_Clock() - clk;
     assert( Aig_ManCoNum(p->pFrame) == Saig_ManRegNum(p->pAig) );
     pProgress = Bar_ProgressStart( stdout, Aig_ManCoNum(p->pFrame) );
     for ( iStart = 0; iStart < Aig_ManCoNum(p->pFrame); )
@@ -267,7 +267,7 @@ p->timeAig += clock() - clk;
     Bar_ProgressStop( pProgress );
     vGatesAll = p->vGatesAll;
     p->vGatesAll = NULL;
-p->timeTotal = clock() - clkTotal;
+p->timeTotal = Abc_Clock() - clkTotal;
     Cgt_ManStop( p );
     return vGatesAll;
 }
@@ -288,7 +288,7 @@ Aig_Man_t * Cgt_ClockGating( Aig_Man_t * pAig, Aig_Man_t * pCare, Cgt_Par_t * pP
     Aig_Man_t * pGated;
     Vec_Vec_t * vGatesAll;
     Vec_Vec_t * vGates;
-    int nNodesUsed;//, clk = clock();
+    int nNodesUsed;//, clk = Abc_Clock();
     vGatesAll = Cgt_ClockGatingCandidates( pAig, pCare, pPars );
     if ( pPars->fAreaOnly )
         vGates = Cgt_ManDecideArea( pAig, vGatesAll, pPars->nOdcMax, pPars->fVerbose );
diff --git a/src/opt/cgt/cgtDecide.c b/src/opt/cgt/cgtDecide.c
index 63730f55..033375a7 100644
--- a/src/opt/cgt/cgtDecide.c
+++ b/src/opt/cgt/cgtDecide.c
@@ -193,7 +193,7 @@ Vec_Vec_t * Cgt_ManDecideSimple( Aig_Man_t * pAig, Vec_Vec_t * vGatesAll, int nO
     Vec_Ptr_t * vCands;
     Aig_Obj_t * pObjLi, * pObjLo, * pCand, * pCandBest;
     int i, k, nHitsCur, nHitsMax, Counter = 0;
-    clock_t clk = clock();
+    abctime clk = Abc_Clock();
     int nTransTotal = 0, nTransSaved = 0;
     vGates = Vec_VecStart( Saig_ManRegNum(pAig) );
     pSml = Ssw_SmlSimulateSeq( pAig, 0, nFrames, nWords );
@@ -231,7 +231,7 @@ Vec_Vec_t * Cgt_ManDecideSimple( Aig_Man_t * pAig, Vec_Vec_t * vGatesAll, int nO
 //        printf( "Gated transitions = %5.2f %%. (%5.2f %%.) ", 
 //            100.0*nTransSaved/nTransTotal, Cgt_ManComputeCoverage(pAig, vGates) );
         printf( "Gated transitions = %5.2f %%. ", Cgt_ManComputeCoverage(pAig, vGates) );
-        ABC_PRT( "Time", clock() - clk );
+        ABC_PRT( "Time", Abc_Clock() - clk );
     }
 /*
     {
@@ -261,7 +261,7 @@ Vec_Vec_t * Cgt_ManDecideArea( Aig_Man_t * pAig, Vec_Vec_t * vGatesAll, int nOdc
     Vec_Ptr_t * vCompletes, * vOne;
     Aig_Obj_t * pGate;
     int i, k, Counter = 0;
-    clock_t clk = clock();
+    abctime clk = Abc_Clock();
     // derive and label complete gates
     vCompletes = Cgt_ManCompleteGates( pAig, vGatesAll, nOdcMax, fVerbose );
     // label complete gates
@@ -288,7 +288,7 @@ Vec_Vec_t * Cgt_ManDecideArea( Aig_Man_t * pAig, Vec_Vec_t * vGatesAll, int nOdc
             Vec_VecSizeSize(vGatesAll), Counter, Saig_ManRegNum(pAig) );
         printf( "Complete gates = %6d. Gated transitions = %5.2f %%. ", 
             Vec_PtrSize(vCompletes), Cgt_ManComputeCoverage(pAig, vGates) );
-        ABC_PRT( "Time", clock() - clk );
+        ABC_PRT( "Time", Abc_Clock() - clk );
     }
     Vec_PtrFree( vCompletes );
     return vGates;
diff --git a/src/opt/cgt/cgtInt.h b/src/opt/cgt/cgtInt.h
index b73d60dd..43d38d8d 100644
--- a/src/opt/cgt/cgtInt.h
+++ b/src/opt/cgt/cgtInt.h
@@ -74,15 +74,15 @@ struct Cgt_Man_t_
     int          nCallsUnsat;    // unsatisfiable calls  
     int          nCallsUndec;    // undecided calls
     int          nCallsFiltered; // filtered out calls
-    clock_t      timeAig;        // constructing AIG
-    clock_t      timePrepare;    // partitioning and SAT solving
-    clock_t      timeSat;        // total runtime
-    clock_t      timeSatSat;     // satisfiable runtime 
-    clock_t      timeSatUnsat;   // unsatisfiable runtime 
-    clock_t      timeSatUndec;   // undecided runtime
-    clock_t      timeDecision;   // making decision about what gates to use
-    clock_t      timeOther;      // other runtime
-    clock_t      timeTotal;      // total runtime
+    abctime      timeAig;        // constructing AIG
+    abctime      timePrepare;    // partitioning and SAT solving
+    abctime      timeSat;        // total runtime
+    abctime      timeSatSat;     // satisfiable runtime 
+    abctime      timeSatUnsat;   // unsatisfiable runtime 
+    abctime      timeSatUndec;   // undecided runtime
+    abctime      timeDecision;   // making decision about what gates to use
+    abctime      timeOther;      // other runtime
+    abctime      timeTotal;      // total runtime
 };
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/cgt/cgtSat.c b/src/opt/cgt/cgtSat.c
index b6d3c599..9ff5f69c 100644
--- a/src/opt/cgt/cgtSat.c
+++ b/src/opt/cgt/cgtSat.c
@@ -47,7 +47,7 @@ int Cgt_CheckImplication( Cgt_Man_t * p, Aig_Obj_t * pGate, Aig_Obj_t * pMiter )
 {
     int nBTLimit = p->pPars->nConfMax;
     int pLits[2], RetValue;
-    clock_t clk;
+    abctime clk;
     p->nCalls++;
 
     // sanity checks
@@ -60,12 +60,12 @@ int Cgt_CheckImplication( Cgt_Man_t * p, Aig_Obj_t * pGate, Aig_Obj_t * pMiter )
     pLits[0] = toLitCond( p->pCnf->pVarNums[Aig_Regular(pGate)->Id], Aig_IsComplement(pGate) );
     pLits[1] = toLitCond( p->pCnf->pVarNums[pMiter->Id], 0 );
 
-clk = clock();
+clk = Abc_Clock();
     RetValue = sat_solver_solve( p->pSat, pLits, pLits + 2, (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
-p->timeSat += clock() - clk;
+p->timeSat += Abc_Clock() - clk;
     if ( RetValue == l_False )
     {
-p->timeSatUnsat += clock() - clk;
+p->timeSatUnsat += Abc_Clock() - clk;
         pLits[0] = lit_neg( pLits[0] );
         pLits[1] = lit_neg( pLits[1] );
         RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
@@ -76,13 +76,13 @@ p->timeSatUnsat += clock() - clk;
     }
     else if ( RetValue == l_True )
     {
-p->timeSatSat += clock() - clk;
+p->timeSatSat += Abc_Clock() - clk;
         p->nCallsSat++;
         return 0;
     }
     else // if ( RetValue1 == l_Undef )
     {
-p->timeSatUndec += clock() - clk;
+p->timeSatUndec += Abc_Clock() - clk;
         p->nCallsUndec++;
         return -1;
     }
diff --git a/src/opt/csw/cswCore.c b/src/opt/csw/cswCore.c
index 3702b346..d1b871f9 100644
--- a/src/opt/csw/cswCore.c
+++ b/src/opt/csw/cswCore.c
@@ -48,8 +48,8 @@ Aig_Man_t * Csw_Sweep( Aig_Man_t * pAig, int nCutsMax, int nLeafMax, int fVerbos
     Aig_Man_t * pRes;
     Aig_Obj_t * pObj, * pObjNew, * pObjRes;
     int i;
-    clock_t clk;
-clk = clock();
+    abctime clk;
+clk = Abc_Clock();
     // start the manager
     p = Csw_ManStart( pAig, nCutsMax, nLeafMax, fVerbose );
     // set elementary cuts at the PIs
@@ -83,7 +83,7 @@ clk = clock();
     // remove dangling nodes 
     Aig_ManCleanup( p->pManRes );
     // return the resulting manager
-p->timeTotal = clock() - clk;
+p->timeTotal = Abc_Clock() - clk;
 p->timeOther = p->timeTotal - p->timeCuts - p->timeHash;
     pRes = p->pManRes;
     Csw_ManStop( p );
diff --git a/src/opt/csw/cswCut.c b/src/opt/csw/cswCut.c
index 0b1d9254..0474d8a5 100644
--- a/src/opt/csw/cswCut.c
+++ b/src/opt/csw/cswCut.c
@@ -498,7 +498,7 @@ Aig_Obj_t * Csw_ObjSweep( Csw_Man_t * p, Aig_Obj_t * pObj, int fTriv )
     Aig_Obj_t * pObjNew;
     unsigned * pTruth;
     int i, k, nVars, nFanins, iVar;
-    clock_t clk;
+    abctime clk;
 
     assert( !Aig_IsComplement(pObj) );
     if ( !Aig_ObjIsNode(pObj) )
@@ -523,7 +523,7 @@ Aig_Obj_t * Csw_ObjSweep( Csw_Man_t * p, Aig_Obj_t * pObj, int fTriv )
             continue;
         // get the next cut of this node
         pCut = Csw_CutFindFree( p, pObj );
-clk = clock();
+clk = Abc_Clock();
         // assemble the new cut
         if ( !Csw_CutMerge( p, pCut0, pCut1, pCut ) )
         {
@@ -542,7 +542,7 @@ clk = clock();
         nFanins = pCut->nFanins;
 //        nVars = Csw_CutSupportMinimize( p, pCut ); // leads to quality degradation
         nVars = Kit_TruthSupportSize( pTruth, p->nLeafMax );
-p->timeCuts += clock() - clk;
+p->timeCuts += Abc_Clock() - clk;
 
         // check for trivial truth tables
         if ( nVars == 0 )
@@ -567,9 +567,9 @@ p->timeCuts += clock() - clk;
         }
 
         // check if an equivalent node with the same cut exists
-clk = clock();
+clk = Abc_Clock();
         pObjNew = pCut->nFanins > 2 ? Csw_TableCutLookup( p, pCut ) : NULL;
-p->timeHash += clock() - clk;
+p->timeHash += Abc_Clock() - clk;
         if ( pObjNew )
         {
             p->nNodesCuts++;
@@ -584,7 +584,7 @@ p->timeHash += clock() - clk;
     p->nNodesTried++;
 
     // load the resulting cuts into the table
-clk = clock();
+clk = Abc_Clock();
     Csw_ObjForEachCut( p, pObj, pCut, i )
     {
         if ( pCut->nFanins > 2 )
@@ -593,7 +593,7 @@ clk = clock();
             Csw_TableCutInsert( p, pCut );
         }
     }
-p->timeHash += clock() - clk;
+p->timeHash += Abc_Clock() - clk;
 
     // return the node if could not replace it
     return pObj;
diff --git a/src/opt/csw/cswInt.h b/src/opt/csw/cswInt.h
index 4f8dac39..890a61d2 100644
--- a/src/opt/csw/cswInt.h
+++ b/src/opt/csw/cswInt.h
@@ -93,10 +93,10 @@ struct Csw_Man_t_
     int             nNodesTriv2;     // the number of trivial nodes
     int             nNodesCuts;      // the number of rewritten nodes
     int             nNodesTried;     // the number of nodes tried
-    clock_t         timeCuts;        // time to compute the cut and its truth table
-    clock_t         timeHash;        // time for hashing cuts
-    clock_t         timeOther;       // other time
-    clock_t         timeTotal;       // total time
+    abctime         timeCuts;        // time to compute the cut and its truth table
+    abctime         timeHash;        // time for hashing cuts
+    abctime         timeOther;       // other time
+    abctime         timeTotal;       // total time
 };
 
 static inline int          Csw_CutLeaveNum( Csw_Cut_t * pCut )          { return pCut->nFanins;                                   }
diff --git a/src/opt/cut/cut.h b/src/opt/cut/cut.h
index 64d3108a..9d4e223b 100644
--- a/src/opt/cut/cut.h
+++ b/src/opt/cut/cut.h
@@ -124,7 +124,7 @@ extern int              Cut_CutCountList( Cut_Cut_t * pList );
 extern Cut_Man_t *      Cut_ManStart( Cut_Params_t * pParams );
 extern void             Cut_ManStop( Cut_Man_t * p );
 extern void             Cut_ManPrintStats( Cut_Man_t * p );
-extern void             Cut_ManPrintStatsToFile( Cut_Man_t * p, char * pFileName, clock_t TimeTotal );
+extern void             Cut_ManPrintStatsToFile( Cut_Man_t * p, char * pFileName, abctime TimeTotal );
 extern void             Cut_ManSetFanoutCounts( Cut_Man_t * p, Vec_Int_t * vFanCounts );
 extern void             Cut_ManSetNodeAttrs( Cut_Man_t * p, Vec_Int_t * vFanCounts );
 extern int              Cut_ManReadVarsMax( Cut_Man_t * p );
diff --git a/src/opt/cut/cutInt.h b/src/opt/cut/cutInt.h
index 754779a3..957cf2c2 100644
--- a/src/opt/cut/cutInt.h
+++ b/src/opt/cut/cutInt.h
@@ -92,12 +92,12 @@ struct Cut_ManStruct_t_
     int                nNodesDag;
     int                nNodesNoCuts;
     // runtime
-    clock_t            timeMerge;
-    clock_t            timeUnion;
-    clock_t            timeTruth;
-    clock_t            timeFilter;
-    clock_t            timeHash;
-    clock_t            timeMap;
+    abctime            timeMerge;
+    abctime            timeUnion;
+    abctime            timeTruth;
+    abctime            timeFilter;
+    abctime            timeHash;
+    abctime            timeMap;
 };
 
 // iterator through all the cuts of the list
diff --git a/src/opt/cut/cutMan.c b/src/opt/cut/cutMan.c
index ea3d73bb..2a82d8bb 100644
--- a/src/opt/cut/cutMan.c
+++ b/src/opt/cut/cutMan.c
@@ -201,7 +201,7 @@ void Cut_ManPrintStats( Cut_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Cut_ManPrintStatsToFile( Cut_Man_t * p, char * pFileName, clock_t TimeTotal )
+void Cut_ManPrintStatsToFile( Cut_Man_t * p, char * pFileName, abctime TimeTotal )
 {
     FILE * pTable;
     pTable = fopen( "cut_stats.txt", "a+" );
diff --git a/src/opt/cut/cutNode.c b/src/opt/cut/cutNode.c
index 4f94011a..11810c33 100644
--- a/src/opt/cut/cutNode.c
+++ b/src/opt/cut/cutNode.c
@@ -370,7 +370,7 @@ Cut_Cut_t * Cut_NodeComputeCuts( Cut_Man_t * p, int Node, int Node0, int Node1,
 {
     Cut_List_t Super, * pSuper = &Super;
     Cut_Cut_t * pList, * pCut;
-    clock_t clk;
+    abctime clk;
     // start the number of cuts at the node
     p->nNodes++;
     p->nNodeCuts = 0;
@@ -381,11 +381,11 @@ Cut_Cut_t * Cut_NodeComputeCuts( Cut_Man_t * p, int Node, int Node0, int Node1,
         Cut_CutNumberList( Cut_NodeReadCutsNew(p, Node1) );
     }
     // compute the cuts
-clk = clock();
+clk = Abc_Clock();
     Cut_ListStart( pSuper );
     Cut_NodeDoComputeCuts( p, pSuper, Node, fCompl0, fCompl1, Cut_NodeReadCutsNew(p, Node0), Cut_NodeReadCutsNew(p, Node1), fTriv, TreeCode );
     pList = Cut_ListFinish( pSuper );
-p->timeMerge += clock() - clk;
+p->timeMerge += Abc_Clock() - clk;
     // verify the result of cut computation
 //    Cut_CutListVerify( pList );
     // performing the recording
@@ -414,12 +414,12 @@ p->timeMerge += clock() - clk;
     /////
     Cut_NodeWriteCutsNew( p, Node, pList );
     // filter the cuts
-//clk = clock();
+//clk = Abc_Clock();
 //    if ( p->pParams->fFilter )
 //        Cut_CutFilter( p, pList0 );
-//p->timeFilter += clock() - clk;
+//p->timeFilter += Abc_Clock() - clk;
     // perform mapping of this node with these cuts
-clk = clock();
+clk = Abc_Clock();
     if ( p->pParams->fMap && !p->pParams->fSeq )
     {
 //        int Delay1, Delay2;
@@ -428,7 +428,7 @@ clk = clock();
 //        assert( Delay1 >= Delay2 );
         Cut_NodeMapping( p, pList, Node, Node0, Node1 );
     }
-p->timeMap += clock() - clk;
+p->timeMap += Abc_Clock() - clk;
     return pList;
 }
 
@@ -681,7 +681,7 @@ Cut_Cut_t * Cut_NodeUnionCuts( Cut_Man_t * p, Vec_Int_t * vNodes )
     Cut_Cut_t * pList, * pListStart, * pCut, * pCut2;
     Cut_Cut_t * pTop = NULL; // Suppress "might be used uninitialized"
     int i, k, Node, Root, Limit = p->pParams->nVarsMax;
-    clock_t clk = clock();
+    abctime clk = Abc_Clock();
 
     // start the new list
     Cut_ListStart( pSuper );
@@ -771,12 +771,12 @@ finish :
     assert( Cut_NodeReadCutsNew(p, Root) == NULL );
     pList = Cut_ListFinish( pSuper );
     Cut_NodeWriteCutsNew( p, Root, pList );
-p->timeUnion += clock() - clk;
+p->timeUnion += Abc_Clock() - clk;
     // filter the cuts
-//clk = clock();
+//clk = Abc_Clock();
 //    if ( p->pParams->fFilter )
 //        Cut_CutFilter( p, pList );
-//p->timeFilter += clock() - clk;
+//p->timeFilter += Abc_Clock() - clk;
     p->nNodes -= vNodes->nSize - 1;
     return pList;
 }
@@ -797,7 +797,7 @@ Cut_Cut_t * Cut_NodeUnionCutsSeq( Cut_Man_t * p, Vec_Int_t * vNodes, int CutSetN
     Cut_List_t Super, * pSuper = &Super;
     Cut_Cut_t * pList, * pListStart, * pCut, * pCut2, * pTop;
     int i, k, Node, Root, Limit = p->pParams->nVarsMax;
-    clock_t clk = clock();
+    abctime clk = Abc_Clock();
 
     // start the new list
     Cut_ListStart( pSuper );
@@ -953,12 +953,12 @@ finish :
         Cut_NodeWriteCutsNew( p, Root, pList );
     }
 
-p->timeUnion += clock() - clk;
+p->timeUnion += Abc_Clock() - clk;
     // filter the cuts
-//clk = clock();
+//clk = Abc_Clock();
 //    if ( p->pParams->fFilter )
 //        Cut_CutFilter( p, pList );
-//p->timeFilter += clock() - clk;
+//p->timeFilter += Abc_Clock() - clk;
 //    if ( fFirst )
 //        p->nNodes -= vNodes->nSize - 1;
     return pList;
diff --git a/src/opt/cut/cutOracle.c b/src/opt/cut/cutOracle.c
index 5b740da5..59d823c8 100644
--- a/src/opt/cut/cutOracle.c
+++ b/src/opt/cut/cutOracle.c
@@ -46,7 +46,7 @@ struct Cut_OracleStruct_t_
     int                EntrySize;
     int                nTruthWords;
     // stats
-    clock_t            timeTotal;
+    abctime            timeTotal;
     int                nCuts;
     int                nCutsTriv;
 };
@@ -322,7 +322,7 @@ Cut_Cut_t * Cut_OracleComputeCuts( Cut_Oracle_t * p, int Node, int Node0, int No
     Cut_Cut_t * pList = NULL, ** ppTail = &pList;
     Cut_Cut_t * pCut, * pCut0, * pCut1, * pList0, * pList1;
     int iCutStart, nCuts, i, Entry;
-    clock_t clk = clock();
+    abctime clk = Abc_Clock();
 
     // get the cuts of the children
     pList0 = (Cut_Cut_t *)Vec_PtrEntry( p->vCutsNew, Node0 );
@@ -367,7 +367,7 @@ Cut_Cut_t * Cut_OracleComputeCuts( Cut_Oracle_t * p, int Node, int Node0, int No
     // write the new cut
     assert( Vec_PtrEntry( p->vCutsNew, Node ) == NULL );
     Vec_PtrWriteEntry( p->vCutsNew, Node, pList );
-p->timeTotal += clock() - clk;
+p->timeTotal += Abc_Clock() - clk;
     return pList;
 }
 
diff --git a/src/opt/cut/cutPre22.c b/src/opt/cut/cutPre22.c
index 0eeea66b..ea1ab64f 100644
--- a/src/opt/cut/cutPre22.c
+++ b/src/opt/cut/cutPre22.c
@@ -69,9 +69,9 @@ struct Cut_CMan_t_
     int                nVarCounts[CUT_CELL_MVAR+1];
     int                nSymGroups[CUT_CELL_MVAR+1];
     int                nSymGroupsE[CUT_CELL_MVAR+1];
-    clock_t            timeCanon;
-    clock_t            timeSupp;
-    clock_t            timeTable;
+    abctime            timeCanon;
+    abctime            timeSupp;
+    abctime            timeTable;
     int                nCellFound;
     int                nCellNotFound;
 };
@@ -235,7 +235,7 @@ void Cut_CellPrecompute()
     Cut_CMan_t * p;
     Cut_Cell_t * pCell, * pTemp;
     int i1, i2, i3, i, j, k, c;
-    clock_t clk = clock(); //, clk2 = clock();
+    abctime clk = Abc_Clock(); //, clk2 = Abc_Clock();
 
     p = Cut_CManStart();
 
@@ -402,7 +402,7 @@ void Cut_CellPrecompute()
     }
 
     printf( "BASIC: Total = %d. Good = %d. Entry = %d. ", (int)p->nTotal, (int)p->nGood, (int)sizeof(Cut_Cell_t) );
-    ABC_PRT( "Time", clock() - clk );
+    ABC_PRT( "Time", Abc_Clock() - clk );
     printf( "Cells:  " );
     for ( i = 0; i <= 9; i++ )
         printf( "%d=%d ", i, p->nVarCounts[i] );
@@ -438,16 +438,16 @@ void Cut_CellPrecompute()
             pCell->CrossBarPhase = c;
             Cut_CellCrossBar( pCell );
             // minimize the support
-//clk2 = clock();
+//clk2 = Abc_Clock();
             Cut_CellSuppMin( pCell );
-//p->timeSupp += clock() - clk2;
+//p->timeSupp += Abc_Clock() - clk2;
             // canonicize
-//clk2 = clock();
+//clk2 = Abc_Clock();
             pCell->CanonPhase = Extra_TruthSemiCanonicize( pCell->uTruth, p->puAux, pCell->nVars, pCell->CanonPerm, pCell->Store );
-//p->timeCanon += clock() - clk2;
+//p->timeCanon += Abc_Clock() - clk2;
 
             // add to the table
-//clk2 = clock();
+//clk2 = Abc_Clock();
             p->nTotal++;
             if ( Cut_CellTableLookup( p, pCell ) ) // already exists
                 Extra_MmFixedEntryRecycle( p->pMem, (char *)pCell );
@@ -482,11 +482,11 @@ void Cut_CellPrecompute()
                 }
 */
             }
-//p->timeTable += clock() - clk2;
+//p->timeTable += Abc_Clock() - clk2;
         }
 
         printf( "VAR %d: Total = %d. Good = %d. Entry = %d. ", k, p->nTotal, p->nGood, (int)sizeof(Cut_Cell_t) );
-        ABC_PRT( "Time", clock() - clk );
+        ABC_PRT( "Time", Abc_Clock() - clk );
         printf( "Cells:  " );
         for ( i = 0; i <= 9; i++ )
             printf( "%d=%d ", i, p->nVarCounts[i] );
@@ -841,7 +841,7 @@ void Cut_CellDumpToFile()
     int NumUsed[10][5] = {{0}};
     int BoxUsed[22][5] = {{0}};
     int i, k, Counter;
-    clock_t clk = clock();
+    abctime clk = Abc_Clock();
 
     if ( p == NULL )
     {
@@ -920,7 +920,7 @@ void Cut_CellDumpToFile()
 
     printf( "Library composed of %d functions is written into file \"%s\".  ", Counter, pFileName );
 
-    ABC_PRT( "Time", clock() - clk );
+    ABC_PRT( "Time", Abc_Clock() - clk );
 }
 
 
diff --git a/src/opt/cut/cutSeq.c b/src/opt/cut/cutSeq.c
index e1df2c95..d4f2d85f 100644
--- a/src/opt/cut/cutSeq.c
+++ b/src/opt/cut/cutSeq.c
@@ -73,7 +73,7 @@ void Cut_NodeComputeCutsSeq( Cut_Man_t * p, int Node, int Node0, int Node1, int
 {
     Cut_List_t Super, * pSuper = &Super;
     Cut_Cut_t * pListNew;
-    clock_t clk;
+    abctime clk;
     
     // get the number of cuts at the node
     p->nNodeCuts = Cut_CutCountList( Cut_NodeReadCutsOld(p, Node) );
@@ -110,13 +110,13 @@ void Cut_NodeComputeCutsSeq( Cut_Man_t * p, int Node, int Node0, int Node1, int
     p->pCompareNew = Cut_NodeReadCutsNew( p, Node );
 
     // merge the old and the new
-clk = clock();
+clk = Abc_Clock();
     Cut_ListStart( pSuper );
     Cut_NodeDoComputeCuts( p, pSuper, Node, fCompl0, fCompl1, p->pStore0[0], p->pStore1[1], 0, 0 );
     Cut_NodeDoComputeCuts( p, pSuper, Node, fCompl0, fCompl1, p->pStore0[1], p->pStore1[0], 0, 0 );
     Cut_NodeDoComputeCuts( p, pSuper, Node, fCompl0, fCompl1, p->pStore0[1], p->pStore1[1], fTriv, 0 );
     pListNew = Cut_ListFinish( pSuper );
-p->timeMerge += clock() - clk;
+p->timeMerge += Abc_Clock() - clk;
 
     // shift the cuts by as many latches and recompute signatures
     if ( Node == Node0 || Node == Node1 || Node0 == Node1 )
diff --git a/src/opt/dar/darCore.c b/src/opt/dar/darCore.c
index bbcb385e..17074123 100644
--- a/src/opt/dar/darCore.c
+++ b/src/opt/dar/darCore.c
@@ -83,7 +83,7 @@ int Dar_ManRewrite( Aig_Man_t * pAig, Dar_RwrPar_t * pPars )
     Dar_Cut_t * pCut;
     Aig_Obj_t * pObj, * pObjNew;
     int i, k, nNodesOld, nNodeBefore, nNodeAfter, Required;
-    clock_t clk = 0, clkStart;
+    abctime clk = 0, clkStart;
     int Counter = 0;
     int nMffcSize;//, nMffcGains[MAX_VAL+1][MAX_VAL+1] = {{0}};
     // prepare the library
@@ -102,7 +102,7 @@ int Dar_ManRewrite( Aig_Man_t * pAig, Dar_RwrPar_t * pPars )
     // set elementary cuts for the PIs
 //    Dar_ManCutsStart( p );
     // resynthesize each node once
-    clkStart = clock();
+    clkStart = Abc_Clock();
     p->nNodesInit = Aig_ManNodeNum(pAig);
     nNodesOld = Vec_PtrSize( pAig->vObjs );
 
@@ -133,10 +133,10 @@ int Dar_ManRewrite( Aig_Man_t * pAig, Dar_RwrPar_t * pPars )
 
         // compute cuts for the node
         p->nNodesTried++;
-clk = clock();
+clk = Abc_Clock();
         Dar_ObjSetCuts( pObj, NULL );
         Dar_ObjComputeCuts_rec( p, pObj );
-p->timeCuts += clock() - clk;
+p->timeCuts += Abc_Clock() - clk;
 
         // check if there is a trivial cut
         Dar_ObjForEachCut( pObj, pCut, k )
@@ -210,7 +210,7 @@ p->timeCuts += clock() - clk;
     }
 */
 
-p->timeTotal = clock() - clkStart;
+p->timeTotal = Abc_Clock() - clkStart;
 p->timeOther = p->timeTotal - p->timeCuts - p->timeEval;
 
 //    Bar_ProgressStop( pProgress );
@@ -289,7 +289,7 @@ Aig_MmFixed_t * Dar_ManComputeCuts( Aig_Man_t * pAig, int nCutsMax, int fSkipTtM
     Aig_Obj_t * pObj;
     Aig_MmFixed_t * pMemCuts;
     int i, nNodes;
-    clock_t clk = clock();
+    abctime clk = Abc_Clock();
     // remove dangling nodes
     if ( (nNodes = Aig_ManCleanup( pAig )) )
     {
@@ -319,7 +319,7 @@ Aig_MmFixed_t * Dar_ManComputeCuts( Aig_Man_t * pAig, int nCutsMax, int fSkipTtM
             Aig_ManObjNum(pAig), nCuts, nCutsK );
         printf( "Cut size = %2d. Truth size = %2d. Total mem = %5.2f MB  ",
             (int)sizeof(Dar_Cut_t), (int)4, 1.0*Aig_MmFixedReadMemUsage(p->pMemCuts)/(1<<20) );
-        ABC_PRT( "Runtime", clock() - clk );
+        ABC_PRT( "Runtime", Abc_Clock() - clk );
 /*
         Aig_ManForEachNode( pAig, pObj, i )
             if ( i % 300 == 0 )
diff --git a/src/opt/dar/darInt.h b/src/opt/dar/darInt.h
index 08a905a8..263e66b6 100644
--- a/src/opt/dar/darInt.h
+++ b/src/opt/dar/darInt.h
@@ -96,12 +96,12 @@ struct Dar_Man_t_
     int              nCutsGood;      // good cuts
     int              nCutsSkipped;   // skipped bad cuts
     // timing statistics
-    clock_t          timeCuts;
-    clock_t          timeEval;
-    clock_t          timeOther;
-    clock_t          timeTotal;
-    clock_t          time1;
-    clock_t          time2;
+    abctime          timeCuts;
+    abctime          timeEval;
+    abctime          timeOther;
+    abctime          timeTotal;
+    abctime          time1;
+    abctime          time2;
 };
 
 static inline Dar_Cut_t *  Dar_ObjCuts( Aig_Obj_t * pObj )                         { return (Dar_Cut_t *)pObj->pData;    }
diff --git a/src/opt/dar/darLib.c b/src/opt/dar/darLib.c
index 27408328..ee440872 100644
--- a/src/opt/dar/darLib.c
+++ b/src/opt/dar/darLib.c
@@ -129,7 +129,7 @@ Dar_Lib_t * Dar_LibAlloc( int nObjs )
 {
     unsigned uTruths[4] = { 0xAAAA, 0xCCCC, 0xF0F0, 0xFF00 };
     Dar_Lib_t * p;
-    int i;//, clk = clock();
+    int i;//, clk = Abc_Clock();
     p = ABC_ALLOC( Dar_Lib_t, 1 );
     memset( p, 0, sizeof(Dar_Lib_t) );
     // allocate objects
@@ -146,7 +146,7 @@ Dar_Lib_t * Dar_LibAlloc( int nObjs )
         p->pObjs[i].fTerm = 1;
         p->pObjs[i].Num = uTruths[i];
     }
-//    ABC_PRT( "Library start", clock() - clk );
+//    ABC_PRT( "Library start", Abc_Clock() - clk );
     return p;
 }
 
@@ -592,11 +592,11 @@ Dar_Lib_t * Dar_LibRead()
 ***********************************************************************/
 void Dar_LibStart()
 {
-//    clock_t clk = clock();
+//    abctime clk = Abc_Clock();
     assert( s_DarLib == NULL );
     s_DarLib = Dar_LibRead();
 //    printf( "The 4-input library started with %d nodes and %d subgraphs. ", s_DarLib->nObjs - 4, s_DarLib->nSubgrTotal );
-//    ABC_PRT( "Time", clock() - clk );
+//    ABC_PRT( "Time", Abc_Clock() - clk );
 }
 
 /**Function*************************************************************
@@ -921,7 +921,7 @@ void Dar_LibEval( Dar_Man_t * p, Aig_Obj_t * pRoot, Dar_Cut_t * pCut, int Requir
     float PowerSaved, PowerAdded;
     Dar_LibObj_t * pObj;
     int Out, k, Class, nNodesSaved, nNodesAdded, nNodesGained;
-    clock_t clk = clock();
+    abctime clk = Abc_Clock();
     if ( pCut->nLeaves != 4 )
         return;
     // check if the cut exits and assigns leaves and their levels
@@ -963,7 +963,7 @@ void Dar_LibEval( Dar_Man_t * p, Aig_Obj_t * pRoot, Dar_Cut_t * pCut, int Requir
         assert( p->LevelBest <= Required );
         *pnMffcSize   = nNodesSaved;
     }
-clk = clock() - clk;
+clk = Abc_Clock() - clk;
 p->ClassTimes[Class] += clk;
 p->timeEval += clk;
 }
@@ -1189,7 +1189,7 @@ int Dar2_LibEval( Gia_Man_t * p, Vec_Int_t * vCutLits, unsigned uTruth, int fKee
 //    int fTraining    =  0;
     Dar_LibObj_t * pObj;
     int Out, k, Class, nNodesSaved, nNodesAdded, nNodesGained;
-//    clock_t clk = clock();
+//    abctime clk = Abc_Clock();
     assert( Vec_IntSize(vCutLits) == 4 );
     assert( (uTruth >> 16) == 0 );
     // check if the cut exits and assigns leaves and their levels
@@ -1233,7 +1233,7 @@ int Dar2_LibEval( Gia_Man_t * p, Vec_Int_t * vCutLits, unsigned uTruth, int fKee
         p_ClassBest  = Class;
 //        assert( p_LevelBest <= Required );
     }
-//clk = clock() - clk;
+//clk = Abc_Clock() - clk;
 //p->ClassTimes[Class] += clk;
 //p->timeEval += clk;
     assert( p_OutBest != -1 );
diff --git a/src/opt/dar/darRefact.c b/src/opt/dar/darRefact.c
index 0dcb54e8..45e150c4 100644
--- a/src/opt/dar/darRefact.c
+++ b/src/opt/dar/darRefact.c
@@ -61,10 +61,10 @@ struct Ref_Man_t_
     int              nCutsUsed;      // the number of rewriting steps
     int              nCutsTried;     // the number of cuts tries
     // timing statistics
-    clock_t          timeCuts;
-    clock_t          timeEval;
-    clock_t          timeOther;
-    clock_t          timeTotal;
+    abctime          timeCuts;
+    abctime          timeEval;
+    abctime          timeOther;
+    abctime          timeTotal;
 };
 
 ////////////////////////////////////////////////////////////////////////
@@ -501,7 +501,7 @@ int Dar_ManRefactor( Aig_Man_t * pAig, Dar_RefPar_t * pPars )
     Aig_Obj_t * pObj, * pObjNew;
     int nNodesOld, nNodeBefore, nNodeAfter, nNodesSaved, nNodesSaved2;
     int i, Required, nLevelMin;
-    clock_t clkStart, clk;
+    abctime clkStart, clk;
 
     // start the manager
     p = Dar_ManRefStart( pAig, pPars );
@@ -513,7 +513,7 @@ int Dar_ManRefactor( Aig_Man_t * pAig, Dar_RefPar_t * pPars )
         Aig_ManStartReverseLevels( pAig, 0 );
 
     // resynthesize each node once
-    clkStart = clock();
+    clkStart = Abc_Clock();
     vCut = Vec_VecEntry( p->vCuts, 0 );
     vCut2 = Vec_VecEntry( p->vCuts, 1 );
     p->nNodesInit = Aig_ManNodeNum(pAig);
@@ -530,12 +530,12 @@ int Dar_ManRefactor( Aig_Man_t * pAig, Dar_RefPar_t * pPars )
 
 //printf( "\nConsidering node %d.\n", pObj->Id );
         // get the bounded MFFC size
-clk = clock();
+clk = Abc_Clock();
         nLevelMin = Abc_MaxInt( 0, Aig_ObjLevel(pObj) - 10 );
         nNodesSaved = Aig_NodeMffcSupp( pAig, pObj, nLevelMin, vCut );
         if ( nNodesSaved < p->pPars->nMffcMin ) // too small to consider
         {
-p->timeCuts += clock() - clk;
+p->timeCuts += Abc_Clock() - clk;
             continue; 
         }
         p->nNodesTried++;
@@ -564,13 +564,13 @@ p->timeCuts += clock() - clk;
             else
                 p->nNodesBelow++;
         }
-p->timeCuts += clock() - clk;
+p->timeCuts += Abc_Clock() - clk;
 
         // try the cuts
-clk = clock();
+clk = Abc_Clock();
         Required = pAig->vLevelR? Aig_ObjRequiredLevel(pAig, pObj) : ABC_INFINITY;
         Dar_ManRefactorTryCuts( p, pObj, nNodesSaved, Required );
-p->timeEval += clock() - clk;
+p->timeEval += Abc_Clock() - clk;
 
         // check the best gain
         if ( !(p->GainBest > 0 || (p->GainBest == 0 && p->pPars->fUseZeros)) )
@@ -594,7 +594,7 @@ p->timeEval += clock() - clk;
         p->nCutsUsed++;
 //        break;
     }
-p->timeTotal = clock() - clkStart;
+p->timeTotal = Abc_Clock() - clkStart;
 p->timeOther = p->timeTotal - p->timeCuts - p->timeEval;
 
 //    Bar_ProgressStop( pProgress );
diff --git a/src/opt/dar/darScript.c b/src/opt/dar/darScript.c
index 583ca563..f1a30a82 100644
--- a/src/opt/dar/darScript.c
+++ b/src/opt/dar/darScript.c
@@ -364,9 +364,9 @@ Aig_Man_t * Dar_ManChoice( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int
     Aig_Man_t * pMan, * pTemp;
     Vec_Ptr_t * vAigs;
     int i;
-    clock_t clk;
+    abctime clk;
 
-clk = clock();
+clk = Abc_Clock();
 //    vAigs = Dar_ManChoiceSynthesisExt();
     vAigs = Dar_ManChoiceSynthesis( pAig, fBalance, fUpdateLevel, 0, fVerbose );
 
@@ -382,9 +382,9 @@ clk = clock();
 
 if ( fVerbose )
 {
-ABC_PRT( "Synthesis time", clock() - clk );
+ABC_PRT( "Synthesis time", Abc_Clock() - clk );
 }
-clk = clock();
+clk = Abc_Clock();
     if ( fConstruct )
         pMan = Aig_ManChoiceConstructive( vAigs, fVerbose );
     else
@@ -394,7 +394,7 @@ clk = clock();
     Vec_PtrFree( vAigs );
 if ( fVerbose )
 {
-ABC_PRT( "Choicing time ", clock() - clk );
+ABC_PRT( "Choicing time ", Abc_Clock() - clk );
 }
     return pMan;
 //    return NULL;
@@ -687,9 +687,9 @@ Aig_Man_t * Dar_ManChoiceNew( Aig_Man_t * pAig, Dch_Pars_t * pPars )
     Aig_Man_t * pMan, * pTemp;
     Vec_Ptr_t * vAigs;
     int i;
-    clock_t clk;
+    abctime clk;
 
-clk = clock();
+clk = Abc_Clock();
 //    vAigs = Dar_ManChoiceSynthesisExt();
 //    vAigs = Dar_ManChoiceSynthesis( pAig, 1, 1, pPars->fPower, fVerbose );
     vAigs = Dar_ManChoiceSynthesis( pAig, 1, 1, pPars->fPower, 0 );
@@ -706,11 +706,11 @@ clk = clock();
 
 if ( fVerbose )
 {
-//ABC_PRT( "Synthesis time", clock() - clk );
+//ABC_PRT( "Synthesis time", Abc_Clock() - clk );
 }
-    pPars->timeSynth = clock() - clk;
+    pPars->timeSynth = Abc_Clock() - clk;
 
-clk = clock();
+clk = Abc_Clock();
     // perform choice computation
     if ( pPars->fUseGia )
         pMan = Cec_ComputeChoices( vAigs, pPars );
@@ -741,7 +741,7 @@ clk = clock();
 
 if ( fVerbose )
 {
-//ABC_PRT( "Choicing time ", clock() - clk );
+//ABC_PRT( "Choicing time ", Abc_Clock() - clk );
 }
     return pMan;
 //    return NULL;
@@ -770,11 +770,11 @@ Aig_Man_t * Dar_ManChoiceNewAig( Aig_Man_t * pAig, Dch_Pars_t * pPars )
     void * pManTime;
     char * pName, * pSpec;
     int i;
-    clock_t clk;
+    abctime clk;
 
-clk = clock();
+clk = Abc_Clock();
     vAigs = Dar_ManChoiceSynthesis( pAig, 1, 1, pPars->fPower, fVerbose );
-pPars->timeSynth = clock() - clk;
+pPars->timeSynth = Abc_Clock() - clk;
     // swap the first and last network
     // this should lead to the primary choice being "better" because of synthesis
     // (it is also important when constructing choices)
@@ -841,7 +841,7 @@ Aig_Man_t * Dar_ManChoiceNew( Aig_Man_t * pAig, Dch_Pars_t * pPars )
     Vec_Ptr_t * vPios;
     void * pManTime;
     char * pName, * pSpec;
-    clock_t clk;
+    abctime clk;
 
     // save useful things
     pManTime = pAig->pManTime; pAig->pManTime = NULL;
@@ -849,9 +849,9 @@ Aig_Man_t * Dar_ManChoiceNew( Aig_Man_t * pAig, Dch_Pars_t * pPars )
     pSpec = Abc_UtilStrsav( pAig->pSpec );
 
     // perform synthesis
-clk = clock();
+clk = Abc_Clock();
     pGia = Dar_NewChoiceSynthesis( Aig_ManDupDfs(pAig), 1, 1, pPars->fPower, pPars->fLightSynth, pPars->fVerbose );
-pPars->timeSynth = clock() - clk;
+pPars->timeSynth = Abc_Clock() - clk;
 
     // perform choice computation
     if ( pPars->fUseGia )
diff --git a/src/opt/dau/dauDsd.c b/src/opt/dau/dauDsd.c
index a6597d98..2aeeb958 100644
--- a/src/opt/dau/dauDsd.c
+++ b/src/opt/dau/dauDsd.c
@@ -949,7 +949,7 @@ struct Dau_Dsd_t_
     char     pOutput[DAU_MAX_STR]; // output stream
 };
 
-static clock_t s_Times[3] = {0};
+static abctime s_Times[3] = {0};
 
 /**Function*************************************************************
 
@@ -1155,7 +1155,7 @@ finish:
 }
 int Dau_Dsd6DecomposeSingleVar( Dau_Dsd_t * p, word * pTruth, int * pVars, int nVars )
 {
-    clock_t clk = clock();
+    abctime clk = Abc_Clock();
     assert( nVars > 1 );
     while ( 1 )
     {
@@ -1171,7 +1171,7 @@ int Dau_Dsd6DecomposeSingleVar( Dau_Dsd_t * p, word * pTruth, int * pVars, int n
     }
     if ( nVars == 1 )
         Dau_DsdWriteVar( p, pVars[--nVars], (int)(pTruth[0] & 1) );
-    s_Times[0] += clock() - clk;
+    s_Times[0] += Abc_Clock() - clk;
     return nVars;
 }
 static inline int Dau_Dsd6FindSupportOne( Dau_Dsd_t * p, word tCof0, word tCof1, int * pVars, int nVars, int v, int u )
@@ -1284,7 +1284,7 @@ finish:
 }
 int Dau_Dsd6DecomposeDoubleVars( Dau_Dsd_t * p, word  * pTruth, int * pVars, int nVars )
 {
-    clock_t clk = clock();
+    abctime clk = Abc_Clock();
     while ( 1 )
     {
         int v, u, nVarsOld;
@@ -1298,7 +1298,7 @@ int Dau_Dsd6DecomposeDoubleVars( Dau_Dsd_t * p, word  * pTruth, int * pVars, int
                 nVars = Dau_Dsd6DecomposeDoubleVarsOne( p, pTruth, pVars, nVars, v, u );
                 if ( nVars == 0 )
                 {
-                    s_Times[1] += clock() - clk;
+                    s_Times[1] += Abc_Clock() - clk;
                     return 0;
                 }
                 if ( nVarsOld > nVars )
@@ -1310,7 +1310,7 @@ int Dau_Dsd6DecomposeDoubleVars( Dau_Dsd_t * p, word  * pTruth, int * pVars, int
         if ( v == 0 ) // not found
             break;
     }
-    s_Times[1] += clock() - clk;
+    s_Times[1] += Abc_Clock() - clk;
     return nVars;
 }
 
@@ -1382,7 +1382,7 @@ static inline int Dau_Dsd6DecomposeTripleVarsInner( Dau_Dsd_t * p, word  * pTrut
 }
 int Dau_Dsd6DecomposeTripleVars( Dau_Dsd_t * p, word  * pTruth, int * pVars, int nVars )
 {
-    clock_t clk = clock();
+    abctime clk = Abc_Clock();
     while ( 1 )
     {
         int v;
@@ -1401,13 +1401,13 @@ int Dau_Dsd6DecomposeTripleVars( Dau_Dsd_t * p, word  * pTruth, int * pVars, int
                     continue;
                 if ( nVarsNew == 0 )
                 {
-                    s_Times[2] += clock() - clk;
+                    s_Times[2] += Abc_Clock() - clk;
                     return 0;
                 }
                 nVars = Dau_Dsd6DecomposeDoubleVars( p, pTruth, pVars, nVarsNew );
                 if ( nVars == 0 )
                 {
-                    s_Times[2] += clock() - clk;
+                    s_Times[2] += Abc_Clock() - clk;
                     return 0;
                 }
                 break;
@@ -1415,7 +1415,7 @@ int Dau_Dsd6DecomposeTripleVars( Dau_Dsd_t * p, word  * pTruth, int * pVars, int
         }
         if ( v == -1 )
         {
-            s_Times[2] += clock() - clk;
+            s_Times[2] += Abc_Clock() - clk;
             return nVars;
         }
     }
@@ -1513,7 +1513,7 @@ finish:
 }
 int Dau_DsdDecomposeSingleVar( Dau_Dsd_t * p, word * pTruth, int * pVars, int nVars )
 {
-    clock_t clk = clock();
+    abctime clk = Abc_Clock();
     assert( nVars > 1 );
     while ( 1 )
     {
@@ -1529,7 +1529,7 @@ int Dau_DsdDecomposeSingleVar( Dau_Dsd_t * p, word * pTruth, int * pVars, int nV
     }
     if ( nVars == 1 )
         Dau_DsdWriteVar( p, pVars[--nVars], (int)(pTruth[0] & 1) );
-    s_Times[0] += clock() - clk;
+    s_Times[0] += Abc_Clock() - clk;
     return nVars;
 }
 
@@ -1660,7 +1660,7 @@ finish:
 }
 int Dau_DsdDecomposeDoubleVars( Dau_Dsd_t * p, word  * pTruth, int * pVars, int nVars )
 {
-    clock_t clk = clock();
+    abctime clk = Abc_Clock();
     while ( 1 )
     {
         int v, u, nVarsOld;
@@ -1674,7 +1674,7 @@ int Dau_DsdDecomposeDoubleVars( Dau_Dsd_t * p, word  * pTruth, int * pVars, int
                 nVars = Dau_DsdDecomposeDoubleVarsOne( p, pTruth, pVars, nVars, v, u );
                 if ( nVars == 0 )
                 {
-                    s_Times[1] += clock() - clk;
+                    s_Times[1] += Abc_Clock() - clk;
                     return 0;
                 }
                 if ( nVarsOld > nVars )
@@ -1686,7 +1686,7 @@ int Dau_DsdDecomposeDoubleVars( Dau_Dsd_t * p, word  * pTruth, int * pVars, int
         if ( v == 0 ) // not found
             break;
     }
-    s_Times[1] += clock() - clk;
+    s_Times[1] += Abc_Clock() - clk;
     return nVars;
 }
 
@@ -1775,7 +1775,7 @@ static inline int Dau_DsdDecomposeTripleVarsInner( Dau_Dsd_t * p, word  * pTruth
 }
 int Dau_DsdDecomposeTripleVars( Dau_Dsd_t * p, word  * pTruth, int * pVars, int nVars )
 {
-    clock_t clk = clock();
+    abctime clk = Abc_Clock();
     while ( 1 )
     {
         int v;
@@ -1794,13 +1794,13 @@ int Dau_DsdDecomposeTripleVars( Dau_Dsd_t * p, word  * pTruth, int * pVars, int
                     continue;
                 if ( nVarsNew == 0 )
                 {
-                    s_Times[2] += clock() - clk;
+                    s_Times[2] += Abc_Clock() - clk;
                     return 0;
                 }
                 nVars = Dau_DsdDecomposeDoubleVars( p, pTruth, pVars, nVarsNew );
                 if ( nVars == 0 )
                 {
-                    s_Times[2] += clock() - clk;
+                    s_Times[2] += Abc_Clock() - clk;
                     return 0;
                 }
                 break;
@@ -1808,7 +1808,7 @@ int Dau_DsdDecomposeTripleVars( Dau_Dsd_t * p, word  * pTruth, int * pVars, int
         }
         if ( v == -1 )
         {
-            s_Times[2] += clock() - clk;
+            s_Times[2] += Abc_Clock() - clk;
             return nVars;
         }
     }
@@ -1969,7 +1969,7 @@ void Dau_DsdTest555()
     char pRes[DAU_MAX_STR];
     int nSizeNonDec;
     int i, Counter = 0;
-    clock_t clk = clock(), clkDec = 0, clk2;
+    abctime clk = Abc_Clock(), clkDec = 0, clk2;
 //    return;
 
     while ( fgets( pBuffer, DAU_MAX_STR, pFile ) != NULL )
@@ -1989,9 +1989,9 @@ void Dau_DsdTest555()
             pTruth = Dau_DsdToTruth( pBuffer[0] == '*' ? pBuffer + 1 : pBuffer, nVars );
             Abc_TtCopy( Tru[0], pTruth, nWords, 0 );
             Abc_TtCopy( Tru[1], pTruth, nWords, 0 );
-            clk2 = clock();
+            clk2 = Abc_Clock();
             nSizeNonDec = Dau_DsdDecompose( Tru[1], nVars, 0, 1, pRes );
-            clkDec += clock() - clk2;
+            clkDec += Abc_Clock() - clk2;
             Dau_DsdNormalize( pRes );
 //            pStr2 = Dau_DsdPerform( t ); nSizeNonDec = 0;
             assert( nSizeNonDec == 0 );
@@ -2008,7 +2008,7 @@ void Dau_DsdTest555()
     }
     printf( "Finished trying %d decompositions.  ", Counter );
     Abc_PrintTime( 1, "Time", clkDec );
-    Abc_PrintTime( 1, "Total", clock() - clk );
+    Abc_PrintTime( 1, "Total", Abc_Clock() - clk );
 
     Abc_PrintTime( 1, "Time1", s_Times[0] );
     Abc_PrintTime( 1, "Time2", s_Times[1] );
diff --git a/src/opt/dau/dauMerge.c b/src/opt/dau/dauMerge.c
index 08eaff73..fff2e523 100644
--- a/src/opt/dau/dauMerge.c
+++ b/src/opt/dau/dauMerge.c
@@ -571,7 +571,7 @@ void Dau_DsdRemoveBraces( char * pDsd, int * pMatches )
 }
 
 
-clock_t s_TimeComp[4] = {0};
+abctime s_TimeComp[4] = {0};
 
 /**Function*************************************************************
 
@@ -605,7 +605,7 @@ char * Dau_DsdMerge( char * pDsd0i, int * pPerm0, char * pDsd1i, int * pPerm1, i
     word * pTruth, * pt = NULL, * pt0 = NULL, * pt1 = NULL;
     word pParts[3][DAU_MAX_WORD];
     int Status;
-    clock_t clk = clock();
+    abctime clk = Abc_Clock();
     Counter++;
     // create local copies
     Dau_DsdMergeCopy( pDsd0i, fCompl0, pDsd0 );
@@ -675,10 +675,10 @@ printf( "Normalized:\n" );
 if ( fVerbose )
 printf( "%s\n", pRes );
 
-        s_TimeComp[0] += clock() - clk;
+        s_TimeComp[0] += Abc_Clock() - clk;
         return pRes;
     }
-s_TimeComp[3] += clock() - clk;
+s_TimeComp[3] += Abc_Clock() - clk;
     // create variable mapping
     nVarsTotal = Dau_DsdMergeCreateMaps( pVarPres, nVarsShared, pOld2New, pNew2Old );
     // perform variable replacement
@@ -761,9 +761,9 @@ printf( "%s\n", pRes );
     }
 
     if ( Status == 0 )
-        s_TimeComp[1] += clock() - clk;
+        s_TimeComp[1] += Abc_Clock() - clk;
     else
-        s_TimeComp[2] += clock() - clk;
+        s_TimeComp[2] += Abc_Clock() - clk;
     return pRes;
 }
 
diff --git a/src/opt/dau/dauTree.c b/src/opt/dau/dauTree.c
index dd62642b..e0ce4ac4 100644
--- a/src/opt/dau/dauTree.c
+++ b/src/opt/dau/dauTree.c
@@ -91,10 +91,10 @@ struct Dss_Man_t_
     int            nCacheHits[2];
     int            nCacheMisses[2];
     int            nCacheEntries[2];
-    clock_t        timeBeg;
-    clock_t        timeDec;
-    clock_t        timeLook;
-    clock_t        timeEnd;
+    abctime        timeBeg;
+    abctime        timeDec;
+    abctime        timeLook;
+    abctime        timeEnd;
 };
 
 static inline Dss_Obj_t *  Dss_Regular( Dss_Obj_t * p )                            { return (Dss_Obj_t *)((ABC_PTRUINT_T)(p) & ~01);                                    }
@@ -309,16 +309,16 @@ void Dau_DsdTest_()
 */
 }
 
-clock_t if_dec_time;
+abctime if_dec_time;
 
 void Dau_DsdCheckStructOne( word * pTruth, int nVars, int nLeaves )
 {
     extern Dss_Ntk_t * Dss_NtkCreate( char * pDsd, int nVars, word * pTruth );
     extern void Dss_NtkFree( Dss_Ntk_t * p );
 
-    static clock_t timeTt  = 0;
-    static clock_t timeDsd = 0;
-    clock_t clkTt, clkDsd;
+    static abctime timeTt  = 0;
+    static abctime timeDsd = 0;
+    abctime clkTt, clkDsd;
 
     char pDsd[1000];
     word Truth[1024];
@@ -345,14 +345,14 @@ void Dau_DsdCheckStructOne( word * pTruth, int nVars, int nLeaves )
     pNtk = Dss_NtkCreate( pDsd, 16, NULL );
 
     // measure DSD runtime
-    clkDsd = clock();
+    clkDsd = Abc_Clock();
     Status = Dss_ObjCheck666( pNtk );
-    timeDsd += clock() - clkDsd;
+    timeDsd += Abc_Clock() - clkDsd;
 
     Dss_NtkFree( pNtk );
 
     // measure TT runtime
-    clkTt = clock();
+    clkTt = Abc_Clock();
     {
         #define CLU_VAR_MAX  16
 
@@ -381,7 +381,7 @@ void Dau_DsdCheckStructOne( word * pTruth, int nVars, int nLeaves )
         }
 
     }
-    timeTt += clock() - clkTt;
+    timeTt += Abc_Clock() - clkTt;
 }
 
 #endif
@@ -1087,7 +1087,7 @@ void Dss_ManPrint( char * pFileName, Dss_Man_t * p )
 {
     Dss_Obj_t * pObj;
     int CountNonDsd = 0, CountNonDsdStr = 0;
-    int i, clk = clock();
+    int i, clk = Abc_Clock();
     FILE * pFile;
     pFile = pFileName ? fopen( pFileName, "wb" ) : stdout;
     if ( pFileName && pFile == NULL )
@@ -1110,7 +1110,7 @@ void Dss_ManPrint( char * pFileName, Dss_Man_t * p )
     fprintf( pFile, "Cache hits    = %8d %8d\n", p->nCacheHits[0],    p->nCacheHits[1] );
     fprintf( pFile, "Cache misses  = %8d %8d\n", p->nCacheMisses[0],  p->nCacheMisses[1] );
     fprintf( pFile, "Cache entries = %8d %8d\n", p->nCacheEntries[0], p->nCacheEntries[1] );
-    Abc_PrintTime( 1, "Time", clock() - clk );
+    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
 //    Dss_ManHashProfile( p );
 //    Dss_ManDump( p );
 //    return;
@@ -1547,7 +1547,7 @@ int Dss_ManMerge( Dss_Man_t * p, int * iDsd, int * nFans, int ** pFans, unsigned
     Dss_Ent_t * pEnt, ** ppSpot;
     Dss_Fun_t * pFun;
     int i;
-    clock_t clk;
+    abctime clk;
     Counter++;
     if ( DAU_MAX_VAR < nKLutSize )
     {
@@ -1569,17 +1569,17 @@ Dss_ManPrintOne( stdout, p, iDsd[1], pFans[1] );
     if ( iDsd[1] == 1 ) return iDsd[0];
 
     // no overlap
-clk = clock();
+clk = Abc_Clock();
     assert( nFans[0] == Dss_VecLitSuppSize(p->vObjs, iDsd[0]) );
     assert( nFans[1] == Dss_VecLitSuppSize(p->vObjs, iDsd[1]) );
     assert( nFans[0] + nFans[1] <= nKLutSize + Dss_WordCountOnes(uSharedMask) );
     // create map of shared variables
     pEnt = Dss_ManSharedMap( p, iDsd, nFans, pFans, uSharedMask );
-p->timeBeg += clock() - clk;
+p->timeBeg += Abc_Clock() - clk;
     // check cache
     if ( p->pCache == NULL )
     {
-clk = clock();
+clk = Abc_Clock();
         if ( uSharedMask == 0 )
             pFun = Dss_ManOperationFun( p, iDsd, nFans[0] + nFans[1] );
         else
@@ -1588,14 +1588,14 @@ clk = clock();
             return -1;
         assert( (int)pFun->nFans == Dss_VecLitSuppSize(p->vObjs, pFun->iDsd) );
         assert( (int)pFun->nFans <= nKLutSize );
-p->timeDec += clock() - clk;
+p->timeDec += Abc_Clock() - clk;
     }
     else
     {
-clk = clock();
+clk = Abc_Clock();
         ppSpot = Dss_ManCacheLookup( p, pEnt );
-p->timeLook += clock() - clk;
-clk = clock();
+p->timeLook += Abc_Clock() - clk;
+clk = Abc_Clock();
         if ( *ppSpot == NULL )
         {
             if ( uSharedMask == 0 )
@@ -1610,10 +1610,10 @@ clk = clock();
             *ppSpot = Dss_ManCacheCreate( p, pEnt, pFun );
         }
         pFun = (*ppSpot)->pFunc;
-p->timeDec += clock() - clk;
+p->timeDec += Abc_Clock() - clk;
     }
 
-clk = clock();
+clk = Abc_Clock();
     for ( i = 0; i < (int)pFun->nFans; i++ )
         if ( pFun->pFans[i] < 2 * nFans[0] ) // first dec
             pPermRes[i] = (unsigned char)Dss_Lit2Lit( pFans[0], pFun->pFans[i] );
@@ -1636,7 +1636,7 @@ clk = clock();
 
     for ( i = 0; i < (int)pFun->nFans; i++ )
         pPermResInt[i] = pPermRes[i];
-p->timeEnd += clock() - clk;
+p->timeEnd += Abc_Clock() - clk;
 
 if ( fVerbose )
 {
@@ -1698,7 +1698,7 @@ int Mpm_FuncCompute( Dss_Man_t * p, int iDsd0, int iDsd1, Vec_Str_t * vShared, i
     Dss_Fun_t * pFun;
     int iDsd[2] = { iDsd0, iDsd1 };
     int i;
-    clock_t clk;
+    abctime clk;
 
     assert( iDsd0 <= iDsd1 );
     if ( DAU_MAX_VAR < *pnLeaves )
@@ -1712,12 +1712,12 @@ int Mpm_FuncCompute( Dss_Man_t * p, int iDsd0, int iDsd1, Vec_Str_t * vShared, i
         Dss_ManPrintOne( stdout, p, iDsd1, NULL );
     } 
 
-clk = clock();
+clk = Abc_Clock();
     pEnt = Dss_ManSharedMapDerive( p, iDsd0, iDsd1, vShared );
     ppSpot = Dss_ManCacheLookup( p, pEnt );
-p->timeLook += clock() - clk;
+p->timeLook += Abc_Clock() - clk;
 
-clk = clock();
+clk = Abc_Clock();
     if ( *ppSpot == NULL )
     {
         if ( Vec_StrSize(vShared) == 0 )
@@ -1732,7 +1732,7 @@ clk = clock();
         *ppSpot = Dss_ManCacheCreate( p, pEnt, pFun );
     }
     pFun = (*ppSpot)->pFunc;
-p->timeDec += clock() - clk;
+p->timeDec += Abc_Clock() - clk;
 
     *pnLeaves = (int)pFun->nFans;
     for ( i = 0; i < (int)pFun->nFans; i++ )
diff --git a/src/opt/fxu/fxuReduce.c b/src/opt/fxu/fxuReduce.c
index 1e553d8d..7542a432 100644
--- a/src/opt/fxu/fxuReduce.c
+++ b/src/opt/fxu/fxuReduce.c
@@ -60,7 +60,7 @@ int Fxu_PreprocessCubePairs( Fxu_Matrix * p, Vec_Ptr_t * vCovers, int nPairsTota
     int nCubes, nBitsMax, nSum;
     int CutOffNum = -1, CutOffQuant = -1; // Suppress "might be used uninitialized"
     int iPair, iQuant, k, c;
-//    clock_t clk = clock();
+//    abctime clk = Abc_Clock();
     char * pSopCover;
     int nFanins;
 
@@ -164,7 +164,7 @@ int Fxu_PreprocessCubePairs( Fxu_Matrix * p, Vec_Ptr_t * vCovers, int nPairsTota
         }
     assert( iPair == nPairsTotal );
     ABC_FREE( pnLitsDiff );
-//ABC_PRT( "Preprocess", clock() - clk );
+//ABC_PRT( "Preprocess", Abc_Clock() - clk );
     return 1;
 }
 
diff --git a/src/opt/lpk/lpkAbcDec.c b/src/opt/lpk/lpkAbcDec.c
index 731c37e6..b7d4ccb1 100644
--- a/src/opt/lpk/lpkAbcDec.c
+++ b/src/opt/lpk/lpkAbcDec.c
@@ -148,7 +148,7 @@ int Lpk_Decompose_rec( Lpk_Man_t * pMan, Lpk_Fun_t * p )
 {
     Lpk_Res_t * pResMux, * pResDsd;
     Lpk_Fun_t * p2;
-    clock_t clk;
+    abctime clk;
 
     // is only called for non-trivial blocks
     assert( p->nLutK >= 3 && p->nLutK <= 6 );
@@ -165,15 +165,15 @@ int Lpk_Decompose_rec( Lpk_Man_t * pMan, Lpk_Fun_t * p )
         Lpk_FunComputeCofSupps( p );
 
     // check DSD decomposition
-clk = clock();
+clk = Abc_Clock();
     pResDsd = Lpk_DsdAnalize( pMan, p, pMan->pPars->nVarsShared );
-pMan->timeEvalDsdAn += clock() - clk;
+pMan->timeEvalDsdAn += Abc_Clock() - clk;
     if ( pResDsd && (pResDsd->nBSVars == (int)p->nLutK || pResDsd->nBSVars == (int)p->nLutK - 1) && 
           pResDsd->AreaEst <= (int)p->nAreaLim && pResDsd->DelayEst <= (int)p->nDelayLim )
     {
-clk = clock();
+clk = Abc_Clock();
         p2 = Lpk_DsdSplit( pMan, p, pResDsd->pCofVars, pResDsd->nCofVars, pResDsd->BSVars );
-pMan->timeEvalDsdSp += clock() - clk;
+pMan->timeEvalDsdSp += Abc_Clock() - clk;
         assert( p2->nVars <= (int)p->nLutK );
         if ( p->nVars > p->nLutK && !Lpk_Decompose_rec( pMan, p ) )
             return 0;
@@ -181,9 +181,9 @@ pMan->timeEvalDsdSp += clock() - clk;
     }
 
     // check MUX decomposition
-clk = clock();
+clk = Abc_Clock();
     pResMux = Lpk_MuxAnalize( pMan, p );
-pMan->timeEvalMuxAn += clock() - clk;
+pMan->timeEvalMuxAn += Abc_Clock() - clk;
 //    pResMux = NULL;
     assert( !pResMux || (pResMux->DelayEst <= (int)p->nDelayLim && pResMux->AreaEst <= (int)p->nAreaLim) );
     // accept MUX decomposition if it is "good"
@@ -202,9 +202,9 @@ pMan->timeEvalMuxAn += clock() - clk;
     assert( pResMux == NULL || pResDsd == NULL );
     if ( pResMux )
     {
-clk = clock();
+clk = Abc_Clock();
         p2 = Lpk_MuxSplit( pMan, p, pResMux->Variable, pResMux->Polarity );
-pMan->timeEvalMuxSp += clock() - clk;
+pMan->timeEvalMuxSp += Abc_Clock() - clk;
         if ( p2->nVars > p->nLutK && !Lpk_Decompose_rec( pMan, p2 ) )
             return 0;
         if ( p->nVars > p->nLutK && !Lpk_Decompose_rec( pMan, p ) )
@@ -213,9 +213,9 @@ pMan->timeEvalMuxSp += clock() - clk;
     }
     if ( pResDsd )
     {
-clk = clock();
+clk = Abc_Clock();
         p2 = Lpk_DsdSplit( pMan, p, pResDsd->pCofVars, pResDsd->nCofVars, pResDsd->BSVars );
-pMan->timeEvalDsdSp += clock() - clk;
+pMan->timeEvalDsdSp += Abc_Clock() - clk;
         assert( p2->nVars <= (int)p->nLutK );
         if ( p->nVars > p->nLutK && !Lpk_Decompose_rec( pMan, p ) )
             return 0;
diff --git a/src/opt/lpk/lpkCore.c b/src/opt/lpk/lpkCore.c
index f060db9a..91e7c715 100644
--- a/src/opt/lpk/lpkCore.c
+++ b/src/opt/lpk/lpkCore.c
@@ -134,7 +134,7 @@ int Lpk_ExploreCut( Lpk_Man_t * p, Lpk_Cut_t * pCut, Kit_DsdNtk_t * pNtk )
     If_Obj_t * pDriver, * ppLeaves[16];
     Abc_Obj_t * pLeaf, * pObjNew;
     int nGain, i;
-    clock_t clk;
+    abctime clk;
     int nNodesBef;
 //    int nOldShared;
 
@@ -186,9 +186,9 @@ int Lpk_ExploreCut( Lpk_Man_t * p, Lpk_Cut_t * pCut, Kit_DsdNtk_t * pNtk )
 
     // perform mapping
     p->pIfMan->pPars->fAreaOnly = 1;
-clk = clock();
+clk = Abc_Clock();
     If_ManPerformMappingComb( p->pIfMan );
-p->timeMap += clock() - clk;
+p->timeMap += Abc_Clock() - clk;
 
     // compute the gain in area
     nGain = pCut->nNodes - pCut->nNodesDup - (int)p->pIfMan->AreaGlo;
@@ -244,16 +244,16 @@ int Lpk_ResynthesizeNode( Lpk_Man_t * p )
     Lpk_Cut_t * pCut;
     unsigned * pTruth;
     int i, k, nSuppSize, nCutNodes, RetValue;
-    clock_t clk;
+    abctime clk;
 
     // compute the cuts
-clk = clock();
+clk = Abc_Clock();
     if ( !Lpk_NodeCuts( p ) )
     {
-p->timeCuts += clock() - clk;
+p->timeCuts += Abc_Clock() - clk;
         return 0;
     }
-p->timeCuts += clock() - clk;
+p->timeCuts += Abc_Clock() - clk;
 
 //return 0;
 
@@ -283,10 +283,10 @@ p->timeCuts += clock() - clk;
             continue;
 
         // compute the truth table
-clk = clock();
+clk = Abc_Clock();
         pTruth = Lpk_CutTruth( p, pCut, 0 );
         nSuppSize = Extra_TruthSupportSize(pTruth, pCut->nLeaves);
-p->timeTruth += clock() - clk;
+p->timeTruth += Abc_Clock() - clk;
 
         pDsdNtk = Kit_DsdDecompose( pTruth, pCut->nLeaves ); 
 //        Kit_DsdVerify( pDsdNtk, pTruth, pCut->nLeaves ); 
@@ -319,9 +319,9 @@ p->timeTruth += clock() - clk;
         }
 
         // update the network
-clk = clock();
+clk = Abc_Clock();
         RetValue = Lpk_ExploreCut( p, pCut, pDsdNtk );
-p->timeEval += clock() - clk;
+p->timeEval += Abc_Clock() - clk;
         Kit_DsdNtkFree( pDsdNtk );
         if ( RetValue )
             break;
@@ -374,18 +374,18 @@ int Lpk_ResynthesizeNodeNew( Lpk_Man_t * p )
     unsigned * pTruth;
     int nNodesBef, nNodesAft, nCutNodes;
     int i, k;
-    clock_t clk;
+    abctime clk;
     int Required = Abc_ObjRequiredLevel(p->pObj);
 //    CloudNode * pFun2;//, * pFun1;
 
     // compute the cuts
-clk = clock();
+clk = Abc_Clock();
     if ( !Lpk_NodeCuts( p ) )
     {
-p->timeCuts += clock() - clk;
+p->timeCuts += Abc_Clock() - clk;
         return 0;
     }
-p->timeCuts += clock() - clk;
+p->timeCuts += Abc_Clock() - clk;
 
     if ( p->pPars->fVeryVerbose )
         printf( "Node %5d : Mffc size = %5d. Cuts = %5d.  Level = %2d. Req = %2d.\n", 
@@ -421,21 +421,21 @@ p->timeCuts += clock() - clk;
             Vec_PtrPush( p->vLeaves, Abc_NtkObj(p->pNtk, pCut->pLeaves[k]) );
 
         // compute the truth table
-clk = clock();
+clk = Abc_Clock();
         pTruth = Lpk_CutTruth( p, pCut, 0 );
-p->timeTruth += clock() - clk;
-clk = clock();
+p->timeTruth += Abc_Clock() - clk;
+clk = Abc_Clock();
         Lpk_ComputeSupports( p, pCut, pTruth );        
-p->timeSupps += clock() - clk;
-//clk = clock();
+p->timeSupps += Abc_Clock() - clk;
+//clk = Abc_Clock();
 //        pFun1 = Lpk_CutTruthBdd( p, pCut );
-//p->timeTruth2 += clock() - clk;
+//p->timeTruth2 += Abc_Clock() - clk;
 /*
-clk = clock();
+clk = Abc_Clock();
         Cloud_Restart( p->pDsdMan->dd );
         pFun2 = Kit_TruthToCloud( p->pDsdMan->dd, pTruth, pCut->nLeaves );
         RetValue = Kit_CreateCloud( p->pDsdMan->dd, pFun2, p->vBddNodes );
-p->timeTruth3 += clock() - clk;
+p->timeTruth3 += Abc_Clock() - clk;
 */
 //        if ( pFun1 != pFun2 )
 //            printf( "Truth tables do not agree!\n" );
@@ -458,10 +458,10 @@ p->timeTruth3 += clock() - clk;
 
         // update the network
         nNodesBef = Abc_NtkNodeNum(p->pNtk);
-clk = clock();
+clk = Abc_Clock();
         pObjNew = Lpk_Decompose( p, p->pNtk, p->vLeaves, pTruth, p->puSupps, p->pPars->nLutSize,
             (int)pCut->nNodes - (int)pCut->nNodesDup - 1 + (int)(p->pPars->fZeroCost > 0), Required );
-p->timeEval += clock() - clk;
+p->timeEval += Abc_Clock() - clk;
         nNodesAft = Abc_NtkNodeNum(p->pNtk);
 
         // perform replacement
@@ -511,7 +511,7 @@ int Lpk_Resynthesize( Abc_Ntk_t * pNtk, Lpk_Par_t * pPars )
     double Delta;
 //    int * pnFanouts, nObjMax;
     int i, Iter, nNodes, nNodesPrev;
-    clock_t clk = clock();
+    abctime clk = Abc_Clock();
     assert( Abc_NtkIsLogic(pNtk) );
  
     // sweep dangling nodes as a preprocessing step
@@ -659,7 +659,7 @@ int Lpk_Resynthesize( Abc_Ntk_t * pNtk, Lpk_Par_t * pPars )
                 printf( " %d=%d", i, p->nBlocks[i] );
         printf( "\n" );
 
-        p->timeTotal = clock() - clk;
+        p->timeTotal = Abc_Clock() - clk;
         p->timeEval  = p->timeEval  - p->timeMap;
         p->timeOther = p->timeTotal - p->timeCuts - p->timeTruth - p->timeEval - p->timeMap;
         ABC_PRTP( "Cuts  ", p->timeCuts,  p->timeTotal );
diff --git a/src/opt/lpk/lpkInt.h b/src/opt/lpk/lpkInt.h
index 053cfe96..841572c7 100644
--- a/src/opt/lpk/lpkInt.h
+++ b/src/opt/lpk/lpkInt.h
@@ -121,20 +121,20 @@ struct Lpk_Man_t_
     // counter of non-DSD blocks
     int          nBlocks[17];
     // runtime
-    clock_t      timeCuts;
-    clock_t      timeTruth;
-    clock_t      timeSupps;
-    clock_t      timeTruth2;
-    clock_t      timeTruth3;
-    clock_t      timeEval;
-    clock_t      timeMap;
-    clock_t      timeOther;
-    clock_t      timeTotal;
+    abctime      timeCuts;
+    abctime      timeTruth;
+    abctime      timeSupps;
+    abctime      timeTruth2;
+    abctime      timeTruth3;
+    abctime      timeEval;
+    abctime      timeMap;
+    abctime      timeOther;
+    abctime      timeTotal;
     // runtime of eval
-    clock_t      timeEvalMuxAn;
-    clock_t      timeEvalMuxSp;
-    clock_t      timeEvalDsdAn;
-    clock_t      timeEvalDsdSp;
+    abctime      timeEvalMuxAn;
+    abctime      timeEvalMuxSp;
+    abctime      timeEvalDsdAn;
+    abctime      timeEvalDsdSp;
  
 };
 
diff --git a/src/opt/mfs/mfsCore.c b/src/opt/mfs/mfsCore.c
index bb36b85c..12355132 100644
--- a/src/opt/mfs/mfsCore.c
+++ b/src/opt/mfs/mfsCore.c
@@ -86,7 +86,7 @@ int Abc_NtkMfsEdgePower( Mfs_Man_t * p, Abc_Obj_t * pNode )
 
 int Abc_WinNode(Mfs_Man_t * p, Abc_Obj_t *pNode)
 {
-//    clock_t clk;
+//    abctime clk;
 //    Abc_Obj_t * pFanin;
 //    int i;
 
@@ -119,7 +119,7 @@ int Abc_WinNode(Mfs_Man_t * p, Abc_Obj_t *pNode)
 /*
 int Abc_NtkMfsPowerResubNode( Mfs_Man_t * p, Abc_Obj_t * pNode )
 {
-    clock_t clk;
+    abctime clk;
     Abc_Obj_t * pFanin;
     int i;
 
@@ -235,46 +235,46 @@ void Abc_NtkMfsPowerResub( Mfs_Man_t * p, Mfs_Par_t * pPars)
 ***********************************************************************/
 int Abc_NtkMfsResub( Mfs_Man_t * p, Abc_Obj_t * pNode )
 {
-    clock_t clk;
+    abctime clk;
     p->nNodesTried++;
     // prepare data structure for this node
     Mfs_ManClean( p );
     // compute window roots, window support, and window nodes
-clk = clock();
+clk = Abc_Clock();
     p->vRoots = Abc_MfsComputeRoots( pNode, p->pPars->nWinTfoLevs, p->pPars->nFanoutsMax );
     p->vSupp  = Abc_NtkNodeSupport( p->pNtk, (Abc_Obj_t **)Vec_PtrArray(p->vRoots), Vec_PtrSize(p->vRoots) );
     p->vNodes = Abc_NtkDfsNodes( p->pNtk, (Abc_Obj_t **)Vec_PtrArray(p->vRoots), Vec_PtrSize(p->vRoots) );
-p->timeWin += clock() - clk;
+p->timeWin += Abc_Clock() - clk;
     if ( p->pPars->nWinMax && Vec_PtrSize(p->vNodes) > p->pPars->nWinMax )
     {
         p->nMaxDivs++;
         return 1;
     }
     // compute the divisors of the window
-clk = clock();
+clk = Abc_Clock();
     p->vDivs  = Abc_MfsComputeDivisors( p, pNode, Abc_ObjRequiredLevel(pNode) - 1 );
     p->nTotalDivs += Vec_PtrSize(p->vDivs) - Abc_ObjFaninNum(pNode);
-p->timeDiv += clock() - clk;
+p->timeDiv += Abc_Clock() - clk;
     // construct AIG for the window
-clk = clock();
+clk = Abc_Clock();
     p->pAigWin = Abc_NtkConstructAig( p, pNode );
-p->timeAig += clock() - clk;
+p->timeAig += Abc_Clock() - clk;
     // translate it into CNF
-clk = clock();
+clk = Abc_Clock();
     p->pCnf = Cnf_DeriveSimple( p->pAigWin, 1 + Vec_PtrSize(p->vDivs) );
-p->timeCnf += clock() - clk;
+p->timeCnf += Abc_Clock() - clk;
     // create the SAT problem
-clk = clock();
+clk = Abc_Clock();
     p->pSat = Abc_MfsCreateSolverResub( p, NULL, 0, 0 );
     if ( p->pSat == NULL )
     {
         p->nNodesBad++;
         return 1;
     }
-//clk = clock();
+//clk = Abc_Clock();
 //    if ( p->pPars->fGiaSat )
 //        Abc_NtkMfsConstructGia( p );
-//p->timeGia += clock() - clk;
+//p->timeGia += Abc_Clock() - clk;
     // solve the SAT problem
     if ( p->pPars->fPower )
         Abc_NtkMfsEdgePower( p, pNode );
@@ -286,7 +286,7 @@ clk = clock();
         if ( p->pPars->fMoreEffort )
             Abc_NtkMfsResubNode2( p, pNode );
     }
-p->timeSat += clock() - clk;
+p->timeSat += Abc_Clock() - clk;
 //    if ( p->pPars->fGiaSat )
 //        Abc_NtkMfsDeconstructGia( p );
     return 1;
@@ -311,28 +311,28 @@ int Abc_NtkMfsNode( Mfs_Man_t * p, Abc_Obj_t * pNode )
     extern Hop_Obj_t * Abc_NodeIfNodeResyn( Bdc_Man_t * p, Hop_Man_t * pHop, Hop_Obj_t * pRoot, int nVars, Vec_Int_t * vTruth, unsigned * puCare, float dProb );
 
     int nGain;
-    clock_t clk;
+    abctime clk;
     p->nNodesTried++;
     // prepare data structure for this node
     Mfs_ManClean( p );
     // compute window roots, window support, and window nodes
-clk = clock();
+clk = Abc_Clock();
     p->vRoots = Abc_MfsComputeRoots( pNode, p->pPars->nWinTfoLevs, p->pPars->nFanoutsMax );
     p->vSupp  = Abc_NtkNodeSupport( p->pNtk, (Abc_Obj_t **)Vec_PtrArray(p->vRoots), Vec_PtrSize(p->vRoots) );
     p->vNodes = Abc_NtkDfsNodes( p->pNtk, (Abc_Obj_t **)Vec_PtrArray(p->vRoots), Vec_PtrSize(p->vRoots) );
-p->timeWin += clock() - clk;
+p->timeWin += Abc_Clock() - clk;
     // count the number of patterns
 //    p->dTotalRatios += Abc_NtkConstraintRatio( p, pNode );
     // construct AIG for the window
-clk = clock();
+clk = Abc_Clock();
     p->pAigWin = Abc_NtkConstructAig( p, pNode );
-p->timeAig += clock() - clk;
+p->timeAig += Abc_Clock() - clk;
     // translate it into CNF
-clk = clock();
+clk = Abc_Clock();
     p->pCnf = Cnf_DeriveSimple( p->pAigWin, Abc_ObjFaninNum(pNode) );
-p->timeCnf += clock() - clk;
+p->timeCnf += Abc_Clock() - clk;
     // create the SAT problem
-clk = clock();
+clk = Abc_Clock();
     p->pSat = (sat_solver *)Cnf_DataWriteIntoSolver( p->pCnf, 1, 0 );
     if ( p->pSat && p->pPars->fOneHotness )
         Abc_NtkAddOneHotness( p );
@@ -341,7 +341,7 @@ clk = clock();
     // solve the SAT problem
     RetValue = Abc_NtkMfsSolveSat( p, pNode );
     p->nTotConfLevel += p->pSat->stats.conflicts;
-p->timeSat += clock() - clk;
+p->timeSat += Abc_Clock() - clk;
     if ( RetValue == 0 )
     {
         p->nTimeOutsLevel++;
@@ -385,7 +385,7 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars )
     Vec_Vec_t * vLevels;
     Vec_Ptr_t * vNodes;
     int i, k, nNodes, nFaninMax;
-    clock_t clk = clock(), clk2;
+    abctime clk = Abc_Clock(), clk2;
     int nTotalNodesBeg = Abc_NtkNodeNum(pNtk);
     int nTotalEdgesBeg = Abc_NtkGetTotalFanins(pNtk);
 
@@ -520,7 +520,7 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars )
             p->nNodesGainedLevel = 0;
             p->nTotConfLevel = 0;
             p->nTimeOutsLevel = 0;
-            clk2 = clock();
+            clk2 = Abc_Clock();
             Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )
             {
                 if ( p->pPars->nDepthMax && (int)pObj->Level > p->pPars->nDepthMax )
@@ -541,7 +541,7 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars )
                 1.0*p->nNodesGainedLevel/Vec_PtrSize(vNodes),
                 1.0*p->nTotConfLevel/Vec_PtrSize(vNodes),
                 100.0*p->nTimeOutsLevel/Vec_PtrSize(vNodes) );
-            ABC_PRT( "Time", clock() - clk2 );
+            ABC_PRT( "Time", Abc_Clock() - clk2 );
             */
             }
         }
@@ -582,7 +582,7 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars )
     }
 
     // free the manager
-    p->timeTotal = clock() - clk;
+    p->timeTotal = Abc_Clock() - clk;
     Mfs_ManStop( p );
     return 1;
 }
diff --git a/src/opt/mfs/mfsInt.h b/src/opt/mfs/mfsInt.h
index ddaa323d..68e4b231 100644
--- a/src/opt/mfs/mfsInt.h
+++ b/src/opt/mfs/mfsInt.h
@@ -124,14 +124,14 @@ struct Mfs_Man_t_
     float               TotalSwitchingBeg;
     float               TotalSwitchingEnd;
     // statistics
-    clock_t             timeWin;
-    clock_t             timeDiv;
-    clock_t             timeAig;
-    clock_t             timeGia;
-    clock_t             timeCnf;
-    clock_t             timeSat;
-    clock_t             timeInt;
-    clock_t             timeTotal;
+    abctime             timeWin;
+    abctime             timeDiv;
+    abctime             timeAig;
+    abctime             timeGia;
+    abctime             timeCnf;
+    abctime             timeSat;
+    abctime             timeInt;
+    abctime             timeTotal;
 };
 
 static inline float Abc_MfsObjProb( Mfs_Man_t * p, Abc_Obj_t * pObj ) { return (p->vProbs && pObj->Id < Vec_IntSize(p->vProbs))? Abc_Int2Float(Vec_IntEntry(p->vProbs,pObj->Id)) : 0.0; }
diff --git a/src/opt/mfs/mfsInter.c b/src/opt/mfs/mfsInter.c
index 5e97f0b3..d56365b0 100644
--- a/src/opt/mfs/mfsInter.c
+++ b/src/opt/mfs/mfsInter.c
@@ -338,7 +338,7 @@ Hop_Obj_t * Abc_NtkMfsInterplate( Mfs_Man_t * p, int * pCands, int nCands )
     Hop_Obj_t * pFunc;
     int nFanins, status;
     int c, i, * pGloVars;
-//    clock_t clk = clock();
+//    abctime clk = Abc_Clock();
 //    p->nDcMints += Abc_NtkMfsInterplateEval( p, pCands, nCands );
 
     // derive the SAT solver for interpolation
@@ -362,7 +362,7 @@ Hop_Obj_t * Abc_NtkMfsInterplate( Mfs_Man_t * p, int * pCands, int nCands )
         return NULL;
     }
 //printf( "%d\n", pSat->stats.conflicts );
-//    ABC_PRT( "S", clock() - clk );
+//    ABC_PRT( "S", Abc_Clock() - clk );
     // get the learned clauses
     pCnf = (Sto_Man_t *)sat_solver_store_release( pSat );
     sat_solver_delete( pSat );
diff --git a/src/opt/mfs/mfsResub.c b/src/opt/mfs/mfsResub.c
index 694b366c..dc73cea7 100644
--- a/src/opt/mfs/mfsResub.c
+++ b/src/opt/mfs/mfsResub.c
@@ -102,12 +102,12 @@ int Abc_NtkMfsTryResubOnce( Mfs_Man_t * p, int * pCands, int nCands )
 {
     int fVeryVerbose = 0;
     unsigned * pData;
-    int RetValue, RetValue2 = -1, iVar, i;//, clk = clock();
+    int RetValue, RetValue2 = -1, iVar, i;//, clk = Abc_Clock();
 /*
     if ( p->pPars->fGiaSat )
     {
         RetValue2 = Abc_NtkMfsTryResubOnceGia( p, pCands, nCands );
-p->timeGia += clock() - clk;
+p->timeGia += Abc_Clock() - clk;
         return RetValue2;
     }
 */ 
@@ -168,7 +168,7 @@ int Abc_NtkMfsSolveSatResub( Mfs_Man_t * p, Abc_Obj_t * pNode, int iFanin, int f
     unsigned * pData;
     int pCands[MFS_FANIN_MAX];
     int RetValue, iVar, i, nCands, nWords, w;
-    clock_t clk;
+    abctime clk;
     Abc_Obj_t * pFanin;
     Hop_Obj_t * pFunc;
     assert( iFanin >= 0 );
@@ -208,14 +208,14 @@ int Abc_NtkMfsSolveSatResub( Mfs_Man_t * p, Abc_Obj_t * pNode, int iFanin, int f
         p->nNodesGainedLevel++;
         if ( fSkipUpdate )
             return 1;
-clk = clock();
+clk = Abc_Clock();
         // derive the function
         pFunc = Abc_NtkMfsInterplate( p, pCands, nCands );
         if ( pFunc == NULL )
             return 0;
         // update the network
         Abc_NtkMfsUpdateNetwork( p, pNode, p->vMfsFanins, pFunc );
-p->timeInt += clock() - clk;
+p->timeInt += Abc_Clock() - clk;
         p->nRemoves++;
         return 1;
     }
@@ -285,7 +285,7 @@ p->timeInt += clock() - clk;
             p->nNodesGainedLevel++;
             if ( fSkipUpdate )
                 return 1;
-clk = clock();
+clk = Abc_Clock();
             // derive the function
             pFunc = Abc_NtkMfsInterplate( p, pCands, nCands+1 );
             if ( pFunc == NULL )
@@ -293,7 +293,7 @@ clk = clock();
             // update the network
             Vec_PtrPush( p->vMfsFanins, Vec_PtrEntry(p->vDivs, iVar) );
             Abc_NtkMfsUpdateNetwork( p, pNode, p->vMfsFanins, pFunc );
-p->timeInt += clock() - clk;
+p->timeInt += Abc_Clock() - clk;
             p->nResubs++;
             return 1;
         }
@@ -322,7 +322,7 @@ int Abc_NtkMfsSolveSatResub2( Mfs_Man_t * p, Abc_Obj_t * pNode, int iFanin, int
     unsigned * pData, * pData2;
     int pCands[MFS_FANIN_MAX];
     int RetValue, iVar, iVar2, i, w, nCands, nWords, fBreak;
-    clock_t clk;
+    abctime clk;
     Abc_Obj_t * pFanin;
     Hop_Obj_t * pFunc;
     assert( iFanin >= 0 );
@@ -360,14 +360,14 @@ int Abc_NtkMfsSolveSatResub2( Mfs_Man_t * p, Abc_Obj_t * pNode, int iFanin, int
         printf( "Node %d: Fanins %d/%d can be removed.\n", pNode->Id, iFanin, iFanin2 );
         p->nNodesResub++;
         p->nNodesGainedLevel++;
-clk = clock();
+clk = Abc_Clock();
         // derive the function
         pFunc = Abc_NtkMfsInterplate( p, pCands, nCands );
         if ( pFunc == NULL )
             return 0;
         // update the network
         Abc_NtkMfsUpdateNetwork( p, pNode, p->vMfsFanins, pFunc );
-p->timeInt += clock() - clk;
+p->timeInt += Abc_Clock() - clk;
         return 1;
     }
 
@@ -454,7 +454,7 @@ p->timeInt += clock() - clk;
             printf( "Node %d: Fanins %d/%d can be replaced by divisors %d/%d.\n", pNode->Id, iFanin, iFanin2, iVar, iVar2 );
             p->nNodesResub++;
             p->nNodesGainedLevel++;
-clk = clock();
+clk = Abc_Clock();
             // derive the function
             pFunc = Abc_NtkMfsInterplate( p, pCands, nCands+2 );
             if ( pFunc == NULL )
@@ -464,7 +464,7 @@ clk = clock();
             Vec_PtrPush( p->vMfsFanins, Vec_PtrEntry(p->vDivs, iVar) );
             assert( Vec_PtrSize(p->vMfsFanins) == nCands + 2 );
             Abc_NtkMfsUpdateNetwork( p, pNode, p->vMfsFanins, pFunc );
-p->timeInt += clock() - clk;
+p->timeInt += Abc_Clock() - clk;
             return 1;
         }
         if ( p->nCexes >= p->pPars->nWinMax )
diff --git a/src/opt/nwk/nwkBidec.c b/src/opt/nwk/nwkBidec.c
index 2f1c0366..1d3d2c26 100644
--- a/src/opt/nwk/nwkBidec.c
+++ b/src/opt/nwk/nwkBidec.c
@@ -133,7 +133,7 @@ void Nwk_ManBidecResyn( Nwk_Man_t * pNtk, int fVerbose )
     Nwk_Obj_t * pObj;
     Vec_Int_t * vTruth;
     int i, nGainTotal = 0, nNodes1, nNodes2;
-    clock_t clk = clock();
+    abctime clk = Abc_Clock();
     pPars->nVarsMax = Nwk_ManGetFaninMax( pNtk );
     pPars->fVerbose = fVerbose;
     if ( pPars->nVarsMax < 2 )
@@ -163,7 +163,7 @@ void Nwk_ManBidecResyn( Nwk_Man_t * pNtk, int fVerbose )
     if ( fVerbose )
     {
     printf( "Total gain in AIG nodes = %d.  ", nGainTotal );
-    ABC_PRT( "Total runtime", clock() - clk );
+    ABC_PRT( "Total runtime", Abc_Clock() - clk );
     }
 }
 
diff --git a/src/opt/nwk/nwkFlow.c b/src/opt/nwk/nwkFlow.c
index 50a4787f..8a672c72 100644
--- a/src/opt/nwk/nwkFlow.c
+++ b/src/opt/nwk/nwkFlow.c
@@ -444,7 +444,7 @@ Vec_Ptr_t * Nwk_ManRetimeCutForward( Nwk_Man_t * pMan, int nLatches, int fVerbos
     Vec_Ptr_t * vNodes;
     Nwk_Obj_t * pObj;
     int i, RetValue, Counter = 0, Counter2 = 0;
-    clock_t clk = clock();
+    abctime clk = Abc_Clock();
     // set the sequential parameters
     pMan->nLatches = nLatches;
     pMan->nTruePis = Nwk_ManCiNum(pMan) - nLatches;
@@ -504,7 +504,7 @@ Vec_Ptr_t * Nwk_ManRetimeCutForward( Nwk_Man_t * pMan, int nLatches, int fVerbos
     if ( fVerbose )
     {
     printf( "Min-cut = %4d.  Unmoved = %4d. ", Vec_PtrSize(vNodes), Counter );
-    ABC_PRT( "Time", clock() - clk );
+    ABC_PRT( "Time", Abc_Clock() - clk );
     }
     return vNodes;
 }
@@ -525,7 +525,7 @@ Vec_Ptr_t * Nwk_ManRetimeCutBackward( Nwk_Man_t * pMan, int nLatches, int fVerbo
     Vec_Ptr_t * vNodes;
     Nwk_Obj_t * pObj;
     int i, RetValue, Counter = 0, Counter2 = 0;
-    clock_t clk = clock();
+    abctime clk = Abc_Clock();
     // set the sequential parameters
     pMan->nLatches = nLatches;
     pMan->nTruePis = Nwk_ManCiNum(pMan) - nLatches;
@@ -591,7 +591,7 @@ Vec_Ptr_t * Nwk_ManRetimeCutBackward( Nwk_Man_t * pMan, int nLatches, int fVerbo
     if ( fVerbose )
     {
     printf( "Min-cut = %4d.  Unmoved = %4d. ", Vec_PtrSize(vNodes), Counter );
-    ABC_PRT( "Time", clock() - clk );
+    ABC_PRT( "Time", Abc_Clock() - clk );
     }
     return vNodes;
 }
diff --git a/src/opt/nwk/nwkMap.c b/src/opt/nwk/nwkMap.c
index e8be5a2d..0b54e74e 100644
--- a/src/opt/nwk/nwkMap.c
+++ b/src/opt/nwk/nwkMap.c
@@ -110,7 +110,7 @@ If_Man_t * Nwk_ManToIf( Aig_Man_t * p, If_Par_t * pPars, Vec_Ptr_t * vAigToIf )
     If_Obj_t * pIfObj;
     Aig_Obj_t * pNode, * pFanin, * pPrev;
     int i;
-    clock_t clk = clock();
+    abctime clk = Abc_Clock();
     // set the number of registers (switch activity will be combinational)
     Aig_ManSetRegNum( p, 0 );
     if ( pPars->fPower )
@@ -118,7 +118,7 @@ If_Man_t * Nwk_ManToIf( Aig_Man_t * p, If_Par_t * pPars, Vec_Ptr_t * vAigToIf )
         vSwitching  = Saig_ManComputeSwitchProbs( p, 48, 16, 0 );
         if ( pPars->fVerbose )
         {
-            ABC_PRT( "Computing switching activity", clock() - clk );
+            ABC_PRT( "Computing switching activity", Abc_Clock() - clk );
         }
         pSwitching  = (float *)vSwitching->pArray;
         vSwitching2 = Vec_IntStart( Aig_ManObjNumMax(p) );
diff --git a/src/opt/nwk/nwkMerge.c b/src/opt/nwk/nwkMerge.c
index c913e0d1..3e458a06 100644
--- a/src/opt/nwk/nwkMerge.c
+++ b/src/opt/nwk/nwkMerge.c
@@ -704,14 +704,14 @@ int Nwk_ManLutMergeGraphTest( char * pFileName )
 {
     int nPairs;
     Nwk_Grf_t * p;
-    clock_t clk = clock();
+    abctime clk = Abc_Clock();
     p = Nwk_ManLutMergeReadGraph( pFileName );
-    ABC_PRT( "Reading", clock() - clk );
-    clk = clock();
+    ABC_PRT( "Reading", Abc_Clock() - clk );
+    clk = Abc_Clock();
     Nwk_ManGraphSolve( p );
     printf( "GRAPH: Nodes = %6d. Edges = %6d.  Pairs = %6d.  ", 
         p->nVerts, p->nEdges, Vec_IntSize(p->vPairs)/2 );
-    ABC_PRT( "Solving", clock() - clk );
+    ABC_PRT( "Solving", Abc_Clock() - clk );
     nPairs = Vec_IntSize(p->vPairs)/2;
     Nwk_ManGraphReportMemoryUsage( p );
     Nwk_ManGraphFree( p );
@@ -975,7 +975,7 @@ Vec_Int_t * Nwk_ManLutMerge( Nwk_Man_t * pNtk, void * pParsInit )
     Vec_Ptr_t * vStart, * vNext, * vCands1, * vCands2;
     Nwk_Obj_t * pLut, * pCand;
     int i, k, nVertsMax, nCands;
-    clock_t clk = clock();
+    abctime clk = Abc_Clock();
     // count the number of vertices
     nVertsMax = 0;
     Nwk_ManForEachNode( pNtk, pLut, i )
@@ -1015,16 +1015,16 @@ Vec_Int_t * Nwk_ManLutMerge( Nwk_Man_t * pNtk, void * pParsInit )
     if ( pPars->fVerbose )
     {
         printf( "Mergable LUTs = %6d. Total cands = %6d. ", p->nVertsMax, nCands );
-        ABC_PRT( "Deriving graph", clock() - clk );
+        ABC_PRT( "Deriving graph", Abc_Clock() - clk );
     }
     // solve the graph problem
-    clk = clock();
+    clk = Abc_Clock();
     Nwk_ManGraphSolve( p );
     if ( pPars->fVerbose )
     {
         printf( "GRAPH: Nodes = %6d. Edges = %6d.  Pairs = %6d.  ", 
             p->nVerts, p->nEdges, Vec_IntSize(p->vPairs)/2 );
-        ABC_PRT( "Solving", clock() - clk );
+        ABC_PRT( "Solving", Abc_Clock() - clk );
         Nwk_ManGraphReportMemoryUsage( p );
     }
     vResult = p->vPairs; p->vPairs = NULL;
diff --git a/src/opt/nwk/nwkUtil.c b/src/opt/nwk/nwkUtil.c
index 2771e723..5b42b881 100644
--- a/src/opt/nwk/nwkUtil.c
+++ b/src/opt/nwk/nwkUtil.c
@@ -544,9 +544,9 @@ int Nwk_ManMinimumBaseInt( Nwk_Man_t * pNtk, int fVerbose )
 void Nwk_ManMinimumBaseRec( Nwk_Man_t * pNtk, int fVerbose )
 {
     int i;
-    clock_t clk = clock();
+    abctime clk = Abc_Clock();
     for ( i = 0; Nwk_ManMinimumBaseInt( pNtk, fVerbose ); i++ );
-    ABC_PRT( "Minbase", clock() - clk );
+    ABC_PRT( "Minbase", Abc_Clock() - clk );
 }
 
 /**Function*************************************************************
diff --git a/src/opt/res/resCore.c b/src/opt/res/resCore.c
index d7edf189..d57cdea5 100644
--- a/src/opt/res/resCore.c
+++ b/src/opt/res/resCore.c
@@ -60,23 +60,23 @@ struct Res_Man_t_
     int           nTotalNets2;   // the total number of nets
     int           nTotalNodes2;  // the total number of nodess
     // runtime
-    clock_t       timeWin;       // windowing
-    clock_t       timeDiv;       // divisors
-    clock_t       timeAig;       // strashing
-    clock_t       timeSim;       // simulation
-    clock_t       timeCand;      // resubstitution candidates
-    clock_t       timeSatTotal;  // SAT solving total 
-    clock_t       timeSatSat;    // SAT solving (sat calls)
-    clock_t       timeSatUnsat;  // SAT solving (unsat calls)
-    clock_t       timeSatSim;    // SAT solving (simulation)
-    clock_t       timeInt;       // interpolation 
-    clock_t       timeUpd;       // updating  
-    clock_t       timeTotal;     // total runtime
+    abctime       timeWin;       // windowing
+    abctime       timeDiv;       // divisors
+    abctime       timeAig;       // strashing
+    abctime       timeSim;       // simulation
+    abctime       timeCand;      // resubstitution candidates
+    abctime       timeSatTotal;  // SAT solving total 
+    abctime       timeSatSat;    // SAT solving (sat calls)
+    abctime       timeSatUnsat;  // SAT solving (unsat calls)
+    abctime       timeSatSim;    // SAT solving (simulation)
+    abctime       timeInt;       // interpolation 
+    abctime       timeUpd;       // updating  
+    abctime       timeTotal;     // total runtime
 };
 
 extern Hop_Obj_t * Kit_GraphToHop( Hop_Man_t * pMan, Kit_Graph_t * pGraph );
 
-extern clock_t s_ResynTime;
+extern abctime s_ResynTime;
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -220,7 +220,7 @@ int Abc_NtkResynthesize( Abc_Ntk_t * pNtk, Res_Par_t * pPars )
     Vec_Ptr_t * vFanins;
     unsigned * puTruth;
     int i, k, RetValue, nNodesOld, nFanins, nFaninsMax;
-    clock_t clk, clkTotal = clock();
+    abctime clk, clkTotal = Abc_Clock();
 
     // start the manager
     p = Res_ManAlloc( pPars );
@@ -260,9 +260,9 @@ int Abc_NtkResynthesize( Abc_Ntk_t * pNtk, Res_Par_t * pPars )
             break;
 
         // create the window for this node
-clk = clock();
+clk = Abc_Clock();
         RetValue = Res_WinCompute( pObj, p->pPars->nWindow/10, p->pPars->nWindow%10, p->pWin );
-p->timeWin += clock() - clk;
+p->timeWin += Abc_Clock() - clk;
         if ( !RetValue )
             continue;
         p->nWinsTriv += Res_WinIsTrivial( p->pWin );
@@ -278,9 +278,9 @@ p->timeWin += clock() - clk;
         }
 
         // collect the divisors
-clk = clock();
+clk = Abc_Clock();
         Res_WinDivisors( p->pWin, Abc_ObjRequiredLevel(pObj) - 1 );
-p->timeDiv += clock() - clk;
+p->timeDiv += Abc_Clock() - clk;
 
         p->nWins++;
         p->nWinNodes += Vec_PtrSize(p->pWin->vNodes);
@@ -293,10 +293,10 @@ p->timeDiv += clock() - clk;
         }
 
         // create the AIG for the window
-clk = clock();
+clk = Abc_Clock();
         if ( p->pAig ) Abc_NtkDelete( p->pAig );
         p->pAig = Res_WndStrash( p->pWin );
-p->timeAig += clock() - clk;
+p->timeAig += Abc_Clock() - clk;
 
         if ( p->pPars->fVeryVerbose )
         {
@@ -305,9 +305,9 @@ p->timeAig += clock() - clk;
         }
  
         // prepare simulation info
-clk = clock();
+clk = Abc_Clock();
         RetValue = Res_SimPrepare( p->pSim, p->pAig, Vec_PtrSize(p->pWin->vLeaves), 0 ); //p->pPars->fVerbose );
-p->timeSim += clock() - clk;
+p->timeSim += Abc_Clock() - clk;
         if ( !RetValue )
         {
             p->nSimEmpty++;
@@ -329,12 +329,12 @@ p->timeSim += clock() - clk;
 //        printf( " " );
 
         // find resub candidates for the node
-clk = clock();
+clk = Abc_Clock();
         if ( p->pPars->fArea )
             RetValue = Res_FilterCandidates( p->pWin, p->pAig, p->pSim, p->vResubs, p->vResubsW, nFaninsMax, 1 );
         else
             RetValue = Res_FilterCandidates( p->pWin, p->pAig, p->pSim, p->vResubs, p->vResubsW, nFaninsMax, 0 );
-p->timeCand += clock() - clk;
+p->timeCand += Abc_Clock() - clk;
         p->nCandSets += RetValue;
         if ( RetValue == 0 )
             continue;
@@ -350,17 +350,17 @@ p->timeCand += clock() - clk;
                 break;
 
             // solve the SAT problem and get clauses
-clk = clock();
+clk = Abc_Clock();
             if ( p->pCnf ) Sto_ManFree( p->pCnf );
             p->pCnf = (Sto_Man_t *)Res_SatProveUnsat( p->pAig, vFanins );
             if ( p->pCnf == NULL )
             {
-p->timeSatSat += clock() - clk;
+p->timeSatSat += Abc_Clock() - clk;
 //                printf( " Sat\n" );
 //                printf( "-" );
                 continue;
             }
-p->timeSatUnsat += clock() - clk;
+p->timeSatUnsat += Abc_Clock() - clk;
 //            printf( "+" );
 
             p->nProvedSets++;
@@ -372,9 +372,9 @@ p->timeSatUnsat += clock() - clk;
 //            Sto_ManDumpClauses( p->pCnf, "trace.cnf" );
 
             // interpolate the problem if it was UNSAT
-clk = clock();
+clk = Abc_Clock();
             nFanins = Int_ManInterpolate( p->pMan, p->pCnf, 0, &puTruth );
-p->timeInt += clock() - clk;
+p->timeInt += Abc_Clock() - clk;
             if ( nFanins != Vec_PtrSize(vFanins) - 2 )
                 continue;
             assert( puTruth );
@@ -388,9 +388,9 @@ p->timeInt += clock() - clk;
             Kit_GraphFree( pGraph );
 
             // update the network
-clk = clock();
+clk = Abc_Clock();
             Res_UpdateNetwork( pObj, Vec_VecEntry(p->vResubsW, k), pFunc, p->vLevels );
-p->timeUpd += clock() - clk;
+p->timeUpd += Abc_Clock() - clk;
             break;
         }
 //        printf( "\n" );
@@ -405,10 +405,10 @@ p->timeSatTotal = p->timeSatSat + p->timeSatUnsat + p->timeSatSim;
     p->nTotalNodes2 = Abc_NtkNodeNum(pNtk);
 
     // quit resubstitution manager
-p->timeTotal = clock() - clkTotal;
+p->timeTotal = Abc_Clock() - clkTotal;
     Res_ManFree( p );
 
-s_ResynTime += clock() - clkTotal;
+s_ResynTime += Abc_Clock() - clkTotal;
     // check the resulting network
     if ( !Abc_NtkCheck( pNtk ) )
     {
diff --git a/src/opt/res/resInt.h b/src/opt/res/resInt.h
index f9709bf6..0eb91322 100644
--- a/src/opt/res/resInt.h
+++ b/src/opt/res/resInt.h
@@ -91,7 +91,7 @@ struct Res_Sim_t_
     // resub candidates
     Vec_Vec_t *      vCands;       // resubstitution candidates
     // statistics
-    clock_t          timeSat;
+    abctime          timeSat;
 };
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/res/resSat.c b/src/opt/res/resSat.c
index 6e209ad9..d6fb5f5e 100644
--- a/src/opt/res/resSat.c
+++ b/src/opt/res/resSat.c
@@ -216,7 +216,7 @@ int Res_SatSimulate( Res_Sim_t * p, int nPatsLimit, int fOnSet )
     sat_solver * pSat;
     int RetValue = -1; // Suppress "might be used uninitialized"
     int i, k, value, status, Lit, Var, iPat;
-    clock_t clk = clock();
+    abctime clk = Abc_Clock();
 
 //printf( "Looking for %s:  ", fOnSet? "onset " : "offset" );
 
@@ -319,7 +319,7 @@ int Res_SatSimulate( Res_Sim_t * p, int nPatsLimit, int fOnSet )
 finish:
 
     sat_solver_delete( pSat );
-p->timeSat += clock() - clk;
+p->timeSat += Abc_Clock() - clk;
     return RetValue;
 }
 
diff --git a/src/opt/ret/retCore.c b/src/opt/ret/retCore.c
index 35d5f4d0..f3484d2c 100644
--- a/src/opt/ret/retCore.c
+++ b/src/opt/ret/retCore.c
@@ -27,7 +27,7 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-clock_t timeRetime = 0;
+abctime timeRetime = 0;
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -49,7 +49,7 @@ int Abc_NtkRetime( Abc_Ntk_t * pNtk, int Mode, int nDelayLim, int fForwardOnly,
     int nLatches = Abc_NtkLatchNum(pNtk);
     int nLevels  = Abc_NtkLevel(pNtk);
     int RetValue = 0;
-    clock_t clkTotal = clock();
+    abctime clkTotal = Abc_Clock();
     int nNodesOld, nLatchesOld;
     assert( Mode > 0 && Mode < 7 );
     assert( !fForwardOnly || !fBackwardOnly );
@@ -98,9 +98,9 @@ int Abc_NtkRetime( Abc_Ntk_t * pNtk, int Mode, int nDelayLim, int fForwardOnly,
     {
         printf( "Reduction in area = %3d. Reduction in delay = %3d. ", 
             nLatches - Abc_NtkLatchNum(pNtk), nLevels - Abc_NtkLevel(pNtk) );
-        ABC_PRT( "Total runtime", clock() - clkTotal );
+        ABC_PRT( "Total runtime", Abc_Clock() - clkTotal );
     }
-    timeRetime = clock() - clkTotal;
+    timeRetime = Abc_Clock() - clkTotal;
     return RetValue;
 }
 
diff --git a/src/opt/ret/retFlow.c b/src/opt/ret/retFlow.c
index 9b215dab..3ce0458b 100644
--- a/src/opt/ret/retFlow.c
+++ b/src/opt/ret/retFlow.c
@@ -145,7 +145,7 @@ Vec_Ptr_t * Abc_NtkMaxFlow( Abc_Ntk_t * pNtk, int fForward, int fVerbose )
     Vec_Ptr_t * vMinCut;
     Abc_Obj_t * pLatch;
     int Flow, FlowCur, RetValue, i;
-    clock_t clk = clock();
+    abctime clk = Abc_Clock();
     int fUseDirectedFlow = 1;
 
     // find the max-flow
@@ -231,7 +231,7 @@ Vec_Ptr_t * Abc_NtkMaxFlow( Abc_Ntk_t * pNtk, int fForward, int fVerbose )
     {
     printf( "L = %6d. %s max-flow = %6d.  Min-cut = %6d.  ", 
         Abc_NtkLatchNum(pNtk), fForward? "Forward " : "Backward", Flow, Vec_PtrSize(vMinCut) );
-ABC_PRT( "Time", clock() - clk );
+ABC_PRT( "Time", Abc_Clock() - clk );
     }
 
 //    Abc_NtkMaxFlowPrintCut( pNtk, vMinCut );
diff --git a/src/opt/ret/retInit.c b/src/opt/ret/retInit.c
index b3f6180a..8e09e1b3 100644
--- a/src/opt/ret/retInit.c
+++ b/src/opt/ret/retInit.c
@@ -49,7 +49,7 @@ Vec_Int_t * Abc_NtkRetimeInitialValues( Abc_Ntk_t * pNtkCone, Vec_Int_t * vValue
     Vec_Int_t * vSolution;
     Abc_Ntk_t * pNtkMiter, * pNtkLogic;
     int RetValue;
-    clock_t clk;
+    abctime clk;
     if ( pNtkCone == NULL )
         return Vec_IntDup( vValues );
     // convert the target network to AIG
@@ -60,10 +60,10 @@ Vec_Int_t * Abc_NtkRetimeInitialValues( Abc_Ntk_t * pNtkCone, Vec_Int_t * vValue
     if ( fVerbose )
         printf( "The miter for initial state computation has %d AIG nodes. ", Abc_NtkNodeNum(pNtkMiter) );
     // solve the miter
-    clk = clock();
+    clk = Abc_Clock();
     RetValue = Abc_NtkMiterSat( pNtkMiter, (ABC_INT64_T)500000, (ABC_INT64_T)50000000, 0, NULL, NULL );
     if ( fVerbose ) 
-        { ABC_PRT( "SAT solving time", clock() - clk ); }
+        { ABC_PRT( "SAT solving time", Abc_Clock() - clk ); }
     // analyze the result
     if ( RetValue == 1 )
         printf( "Abc_NtkRetimeInitialValues(): The problem is unsatisfiable. DC latch values are used.\n" );
diff --git a/src/opt/ret/retLvalue.c b/src/opt/ret/retLvalue.c
index 5bcc2583..d48bc6cd 100644
--- a/src/opt/ret/retLvalue.c
+++ b/src/opt/ret/retLvalue.c
@@ -94,7 +94,7 @@ Vec_Int_t * Abc_NtkRetimeGetLags( Abc_Ntk_t * pNtk, int nIterLimit, int fVerbose
     Vec_Ptr_t * vNodes, * vLatches;
     Abc_Obj_t * pNode;
     int i, FiMax, FiBest, RetValue;
-    clock_t clk, clkIter;
+    abctime clk, clkIter;
     char NodeLag;
 
     // get the upper bound on the clock period
@@ -112,9 +112,9 @@ Vec_Int_t * Abc_NtkRetimeGetLags( Abc_Ntk_t * pNtk, int nIterLimit, int fVerbose
     }
  
     // search for the optimal clock period between 0 and nLevelMax
-clk = clock();
+clk = Abc_Clock();
     FiBest = Abc_NtkRetimeSearch_rec( pNtk, vNodes, vLatches, 0, FiMax, nIterLimit, fVerbose );
-clkIter = clock() - clk;
+clkIter = Abc_Clock() - clk;
 
     // recompute the best l-values
     RetValue = Abc_NtkRetimeForPeriod( pNtk, vNodes, vLatches, FiBest, nIterLimit, fVerbose );
diff --git a/src/opt/rwr/rwr.h b/src/opt/rwr/rwr.h
index 74af4caa..b688fc09 100644
--- a/src/opt/rwr/rwr.h
+++ b/src/opt/rwr/rwr.h
@@ -86,13 +86,13 @@ struct Rwr_Man_t_
     int                nCutsBad;
     int                nSubgraphs;
     // runtime statistics
-    clock_t            timeStart;
-    clock_t            timeCut;
-    clock_t            timeRes;
-    clock_t            timeEval;
-    clock_t            timeMffc;
-    clock_t            timeUpdate;
-    clock_t            timeTotal;
+    abctime            timeStart;
+    abctime            timeCut;
+    abctime            timeRes;
+    abctime            timeEval;
+    abctime            timeMffc;
+    abctime            timeUpdate;
+    abctime            timeTotal;
 };
 
 struct Rwr_Node_t_ // 24 bytes
@@ -146,9 +146,9 @@ extern void              Rwr_ManPrintStatsFile( Rwr_Man_t * p );
 extern void *            Rwr_ManReadDecs( Rwr_Man_t * p );
 extern Vec_Ptr_t *       Rwr_ManReadLeaves( Rwr_Man_t * p );
 extern int               Rwr_ManReadCompl( Rwr_Man_t * p );
-extern void              Rwr_ManAddTimeCuts( Rwr_Man_t * p, clock_t Time );
-extern void              Rwr_ManAddTimeUpdate( Rwr_Man_t * p, clock_t Time );
-extern void              Rwr_ManAddTimeTotal( Rwr_Man_t * p, clock_t Time );
+extern void              Rwr_ManAddTimeCuts( Rwr_Man_t * p, abctime Time );
+extern void              Rwr_ManAddTimeUpdate( Rwr_Man_t * p, abctime Time );
+extern void              Rwr_ManAddTimeTotal( Rwr_Man_t * p, abctime Time );
 /*=== rwrPrint.c ========================================================*/
 extern void              Rwr_ManPrint( Rwr_Man_t * p );
 /*=== rwrUtil.c ========================================================*/
diff --git a/src/opt/rwr/rwrEva.c b/src/opt/rwr/rwrEva.c
index de29e153..a4d50fca 100644
--- a/src/opt/rwr/rwrEva.c
+++ b/src/opt/rwr/rwrEva.c
@@ -69,17 +69,17 @@ int Rwr_NodeRewrite( Rwr_Man_t * p, Cut_Man_t * pManCut, Abc_Obj_t * pNode, int
     int Required, nNodesSaved;
     int nNodesSaveCur = -1; // Suppress "might be used uninitialized"
     int i, GainCur, GainBest = -1;
-    clock_t clk, clk2;//, Counter;
+    abctime clk, clk2;//, Counter;
 
     p->nNodesConsidered++;
     // get the required times
     Required = fUpdateLevel? Abc_ObjRequiredLevel(pNode) : ABC_INFINITY;
 
     // get the node's cuts
-clk = clock();
+clk = Abc_Clock();
     pCut = (Cut_Cut_t *)Abc_NodeGetCutsRecursive( pManCut, pNode, 0, 0 );
     assert( pCut != NULL );
-p->timeCut += clock() - clk;
+p->timeCut += Abc_Clock() - clk;
 
 //printf( " %d", Rwr_CutCountNumNodes(pNode, pCut) );
 /*
@@ -89,7 +89,7 @@ p->timeCut += clock() - clk;
     printf( "%d ", Counter );
 */
     // go through the cuts
-clk = clock();
+clk = Abc_Clock();
     for ( pCut = pCut->pNext; pCut; pCut = pCut->pNext )
     {
         // consider only 4-input cuts
@@ -128,7 +128,7 @@ clk = clock();
                 continue;
         }
 
-clk2 = clock();
+clk2 = Abc_Clock();
 /*
         printf( "Considering: (" );
         Vec_PtrForEachEntry( Abc_Obj_t *, p->vFaninsCur, pFanin, i )
@@ -145,12 +145,12 @@ clk2 = clock();
         // unmark the fanin boundary
         Vec_PtrForEachEntry( Abc_Obj_t *, p->vFaninsCur, pFanin, i )
             Abc_ObjRegular(pFanin)->vFanouts.nSize--;
-p->timeMffc += clock() - clk2;
+p->timeMffc += Abc_Clock() - clk2;
 
         // evaluate the cut
-clk2 = clock();
+clk2 = Abc_Clock();
         pGraph = Rwr_CutEvaluate( p, pNode, pCut, p->vFaninsCur, nNodesSaved, Required, &GainCur, fPlaceEnable );
-p->timeEval += clock() - clk2;
+p->timeEval += Abc_Clock() - clk2;
 
         // check if the cut is better than the current best one
         if ( pGraph != NULL && GainBest < GainCur )
@@ -167,7 +167,7 @@ p->timeEval += clock() - clk2;
                 Vec_PtrPush( p->vFanins, pFanin );
         }
     }
-p->timeRes += clock() - clk;
+p->timeRes += Abc_Clock() - clk;
 
     if ( GainBest == -1 )
         return -1;
diff --git a/src/opt/rwr/rwrExp.c b/src/opt/rwr/rwrExp.c
index e760ab8e..9d8455b4 100644
--- a/src/opt/rwr/rwrExp.c
+++ b/src/opt/rwr/rwrExp.c
@@ -226,7 +226,7 @@ void Rwt_Man5ExplorePrint()
     int * pDistrib;
     unsigned * pReprs;
     unsigned uTruth, uTruthC;
-    clock_t clk = clock();
+    abctime clk = Abc_Clock();
     Vec_Int_t * vClassesNN, * vClassesNPN;
 
     // find the max number of occurences
@@ -285,7 +285,7 @@ void Rwt_Man5ExplorePrint()
     printf( "%d classes written into file \"%s\".\n", vClassesNN->nSize, "nnclass_stats5.txt" );
 
 
-clk = clock();
+clk = Abc_Clock();
     // how many NPN classes exist?
     Vec_IntForEachEntry( vClassesNN, uTruth, i )
     {
@@ -300,7 +300,7 @@ clk = clock();
         (*pCounter) += Counter;
     }
     printf( "The numbe of NPN classes = %d.\n", stmm_count(s_pManRwrExp5->tTableNPN) );
-ABC_PRT( "Computing NPN classes", clock() - clk );
+ABC_PRT( "Computing NPN classes", Abc_Clock() - clk );
 
     // put them into an array
     vClassesNPN = Vec_IntAlloc( stmm_count(s_pManRwrExp5->tTableNPN) );
diff --git a/src/opt/rwr/rwrMan.c b/src/opt/rwr/rwrMan.c
index 0f0631bc..2245428f 100644
--- a/src/opt/rwr/rwrMan.c
+++ b/src/opt/rwr/rwrMan.c
@@ -48,8 +48,8 @@ Rwr_Man_t * Rwr_ManStart( int  fPrecompute )
 {
     Dec_Man_t * pManDec;
     Rwr_Man_t * p;
-    clock_t clk = clock();
-clk = clock();
+    abctime clk = Abc_Clock();
+clk = Abc_Clock();
     p = ABC_ALLOC( Rwr_Man_t, 1 );
     memset( p, 0, sizeof(Rwr_Man_t) );
     p->nFuncs = (1<<16);
@@ -91,7 +91,7 @@ clk = clock();
 //        Rwr_ManPrint( p );
         Rwr_ManPreprocess( p );
     }
-p->timeStart = clock() - clk;
+p->timeStart = Abc_Clock() - clk;
     return p;
 }
 
@@ -258,7 +258,7 @@ int Rwr_ManReadCompl( Rwr_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Rwr_ManAddTimeCuts( Rwr_Man_t * p, clock_t Time )
+void Rwr_ManAddTimeCuts( Rwr_Man_t * p, abctime Time )
 {
     p->timeCut += Time;
 }
@@ -274,7 +274,7 @@ void Rwr_ManAddTimeCuts( Rwr_Man_t * p, clock_t Time )
   SeeAlso     []
 
 ***********************************************************************/
-void Rwr_ManAddTimeUpdate( Rwr_Man_t * p, clock_t Time )
+void Rwr_ManAddTimeUpdate( Rwr_Man_t * p, abctime Time )
 {
     p->timeUpdate += Time;
 }
@@ -290,7 +290,7 @@ void Rwr_ManAddTimeUpdate( Rwr_Man_t * p, clock_t Time )
   SeeAlso     []
 
 ***********************************************************************/
-void Rwr_ManAddTimeTotal( Rwr_Man_t * p, clock_t Time )
+void Rwr_ManAddTimeTotal( Rwr_Man_t * p, abctime Time )
 {
     p->timeTotal += Time;
 }
diff --git a/src/opt/rwr/rwrUtil.c b/src/opt/rwr/rwrUtil.c
index 97ddca3c..ee87cf9f 100644
--- a/src/opt/rwr/rwrUtil.c
+++ b/src/opt/rwr/rwrUtil.c
@@ -429,7 +429,7 @@ void Rwr_ManWriteToArray( Rwr_Man_t * p )
     Rwr_Node_t * pNode;
     unsigned Entry0, Entry1;
     int i, nEntries;
-    clock_t clk = clock();
+    abctime clk = Abc_Clock();
     // prepare the buffer
     nEntries = p->vForest->nSize - 5;
     pFile = fopen( "npn4_aig_array.txt", "w" );
@@ -455,7 +455,7 @@ void Rwr_ManWriteToArray( Rwr_Man_t * p )
     Extra_PrintHex( pFile, &Entry0, 4 );
     fprintf( pFile, " \n};\n" );
     fclose( pFile );
-    printf( "The number of nodes saved = %d.   ", nEntries );  ABC_PRT( "Saving", clock() - clk );
+    printf( "The number of nodes saved = %d.   ", nEntries );  ABC_PRT( "Saving", Abc_Clock() - clk );
 }
 
 /**Function*************************************************************
@@ -476,7 +476,7 @@ void Rwr_ManLoadFromArray( Rwr_Man_t * p, int fVerbose )
     unsigned Entry0, Entry1;
     int Level, Volume, nEntries, fExor;
     int i;
-    clock_t clk = clock();
+    abctime clk = Abc_Clock();
 
     // reconstruct the forest
     for ( i = 0; ; i++ )
@@ -505,7 +505,7 @@ void Rwr_ManLoadFromArray( Rwr_Man_t * p, int fVerbose )
     if ( fVerbose )
     {
         printf( "The number of classes = %d. Canonical nodes = %d.\n", p->nClasses, p->nAdded );
-        printf( "The number of nodes loaded = %d.  ", nEntries );  ABC_PRT( "Loading", clock() - clk );
+        printf( "The number of nodes loaded = %d.  ", nEntries );  ABC_PRT( "Loading", Abc_Clock() - clk );
     }
 }
 
@@ -527,7 +527,7 @@ void Rwr_ManWriteToFile( Rwr_Man_t * p, char * pFileName )
     Rwr_Node_t * pNode;
     unsigned * pBuffer;
     int i, nEntries;
-    clock_t clk = clock();
+    abctime clk = Abc_Clock();
     // prepare the buffer
     nEntries = p->vForest->nSize - 5;
     pBuffer = ABC_ALLOC( unsigned, nEntries * 2 );
@@ -545,7 +545,7 @@ void Rwr_ManWriteToFile( Rwr_Man_t * p, char * pFileName )
     fwrite( pBuffer, sizeof(unsigned), nEntries * 2, pFile );
     ABC_FREE( pBuffer );
     fclose( pFile );
-    printf( "The number of nodes saved = %d.   ", nEntries );  ABC_PRT( "Saving", clock() - clk );
+    printf( "The number of nodes saved = %d.   ", nEntries );  ABC_PRT( "Saving", Abc_Clock() - clk );
 }
 
 /**Function*************************************************************
@@ -566,7 +566,7 @@ void Rwr_ManLoadFromFile( Rwr_Man_t * p, char * pFileName )
     unsigned * pBuffer;
     int Level, Volume, nEntries, fExor;
     int i;
-    clock_t clk = clock();
+    abctime clk = Abc_Clock();
     int RetValue;
 
     // load the data
@@ -601,7 +601,7 @@ void Rwr_ManLoadFromFile( Rwr_Man_t * p, char * pFileName )
     }
     ABC_FREE( pBuffer );
     printf( "The number of classes = %d. Canonical nodes = %d.\n", p->nClasses, p->nAdded );
-    printf( "The number of nodes loaded = %d.   ", nEntries );  ABC_PRT( "Loading", clock() - clk );
+    printf( "The number of nodes loaded = %d.   ", nEntries );  ABC_PRT( "Loading", Abc_Clock() - clk );
 }
 
 
diff --git a/src/opt/rwt/rwt.h b/src/opt/rwt/rwt.h
index ff00cf52..2a0f7618 100644
--- a/src/opt/rwt/rwt.h
+++ b/src/opt/rwt/rwt.h
@@ -94,14 +94,14 @@ struct Rwt_Man_t_
     int                nCutsBad;
     int                nSubgraphs;
     // runtime statistics
-    clock_t            timeStart;
-    clock_t            timeTruth;
-    clock_t            timeCut;
-    clock_t            timeRes;
-    clock_t            timeEval;
-    clock_t            timeMffc;
-    clock_t            timeUpdate;
-    clock_t            timeTotal;
+    abctime            timeStart;
+    abctime            timeTruth;
+    abctime            timeCut;
+    abctime            timeRes;
+    abctime            timeEval;
+    abctime            timeMffc;
+    abctime            timeUpdate;
+    abctime            timeTotal;
 };
 
 struct Rwt_Node_t_ // 24 bytes
@@ -142,9 +142,9 @@ extern void              Rwt_ManPrintStatsFile( Rwt_Man_t * p );
 extern void *            Rwt_ManReadDecs( Rwt_Man_t * p );
 extern Vec_Ptr_t *       Rwt_ManReadLeaves( Rwt_Man_t * p );
 extern int               Rwt_ManReadCompl( Rwt_Man_t * p );
-extern void              Rwt_ManAddTimeCuts( Rwt_Man_t * p, clock_t Time );
-extern void              Rwt_ManAddTimeUpdate( Rwt_Man_t * p, clock_t Time );
-extern void              Rwt_ManAddTimeTotal( Rwt_Man_t * p, clock_t Time );
+extern void              Rwt_ManAddTimeCuts( Rwt_Man_t * p, abctime Time );
+extern void              Rwt_ManAddTimeUpdate( Rwt_Man_t * p, abctime Time );
+extern void              Rwt_ManAddTimeTotal( Rwt_Man_t * p, abctime Time );
 /*=== rwrUtil.c ========================================================*/
 extern void              Rwt_ManLoadFromArray( Rwt_Man_t * p, int fVerbose );
 extern char *            Rwt_ManGetPractical( Rwt_Man_t * p );
diff --git a/src/opt/rwt/rwtMan.c b/src/opt/rwt/rwtMan.c
index 18998ac8..d7597e08 100644
--- a/src/opt/rwt/rwtMan.c
+++ b/src/opt/rwt/rwtMan.c
@@ -87,8 +87,8 @@ void Rwt_ManGlobalStop()
 Rwt_Man_t * Rwt_ManStart( int fPrecompute )
 {
     Rwt_Man_t * p;
-    clock_t clk = clock();
-clk = clock();
+    abctime clk = Abc_Clock();
+clk = Abc_Clock();
     p = ABC_ALLOC( Rwt_Man_t, 1 );
     memset( p, 0, sizeof(Rwt_Man_t) );
     p->nFuncs = (1<<16);
@@ -131,7 +131,7 @@ clk = clock();
 //        Rwt_ManPrint( p );
         Rwt_ManPreprocess( p );
     }
-p->timeStart = clock() - clk;
+p->timeStart = Abc_Clock() - clk;
     return p;
 }
 
@@ -298,7 +298,7 @@ int Rwt_ManReadCompl( Rwt_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Rwt_ManAddTimeCuts( Rwt_Man_t * p, clock_t Time )
+void Rwt_ManAddTimeCuts( Rwt_Man_t * p, abctime Time )
 {
     p->timeCut += Time;
 }
@@ -314,7 +314,7 @@ void Rwt_ManAddTimeCuts( Rwt_Man_t * p, clock_t Time )
   SeeAlso     []
 
 ***********************************************************************/
-void Rwt_ManAddTimeUpdate( Rwt_Man_t * p, clock_t Time )
+void Rwt_ManAddTimeUpdate( Rwt_Man_t * p, abctime Time )
 {
     p->timeUpdate += Time;
 }
@@ -330,7 +330,7 @@ void Rwt_ManAddTimeUpdate( Rwt_Man_t * p, clock_t Time )
   SeeAlso     []
 
 ***********************************************************************/
-void Rwt_ManAddTimeTotal( Rwt_Man_t * p, clock_t Time )
+void Rwt_ManAddTimeTotal( Rwt_Man_t * p, abctime Time )
 {
     p->timeTotal += Time;
 }
diff --git a/src/opt/rwt/rwtUtil.c b/src/opt/rwt/rwtUtil.c
index d6011b20..c6bf63ed 100644
--- a/src/opt/rwt/rwtUtil.c
+++ b/src/opt/rwt/rwtUtil.c
@@ -593,7 +593,7 @@ void Rwt_ManLoadFromArray( Rwt_Man_t * p, int fVerbose )
     unsigned Entry0, Entry1;
     int Level, Volume, nEntries, fExor;
     int i;
-    clock_t clk = clock();
+    abctime clk = Abc_Clock();
 
     // reconstruct the forest
     for ( i = 0; ; i++ )
@@ -622,7 +622,7 @@ void Rwt_ManLoadFromArray( Rwt_Man_t * p, int fVerbose )
     if ( fVerbose )
     {
         printf( "The number of classes = %d. Canonical nodes = %d.\n", p->nClasses, p->nAdded );
-        printf( "The number of nodes loaded = %d.  ", nEntries );  ABC_PRT( "Loading", clock() - clk );
+        printf( "The number of nodes loaded = %d.  ", nEntries );  ABC_PRT( "Loading", Abc_Clock() - clk );
     }
 }
 
diff --git a/src/opt/sfm/sfmCore.c b/src/opt/sfm/sfmCore.c
index 7032c7dd..865db096 100644
--- a/src/opt/sfm/sfmCore.c
+++ b/src/opt/sfm/sfmCore.c
@@ -111,7 +111,7 @@ int Sfm_NodeResubSolve( Sfm_Ntk_t * p, int iNode, int f, int fRemoveOnly )
     int fVeryVerbose = 0;//p->pPars->fVeryVerbose && Vec_IntSize(p->vDivs) < 200;// || pNode->Id == 556;
     int i, iFanin, iVar = -1;
     word uTruth, uSign, uMask;
-    clock_t clk;
+    abctime clk;
     assert( Sfm_ObjIsNode(p, iNode) );
     assert( f >= 0 && f < Sfm_ObjFaninNum(p, iNode) );
     p->nTryRemoves++;
@@ -128,9 +128,9 @@ int Sfm_NodeResubSolve( Sfm_Ntk_t * p, int iNode, int f, int fRemoveOnly )
     Sfm_ObjForEachFanin( p, iNode, iFanin, i )
         if ( i != f )
             Vec_IntPush( p->vDivIds, Sfm_ObjSatVar(p, iFanin) );
-clk = clock();
+clk = Abc_Clock();
     uTruth = Sfm_ComputeInterpolant( p );
-p->timeSat += clock() - clk;
+p->timeSat += Abc_Clock() - clk;
     // analyze outcomes
     if ( uTruth == SFM_SAT_UNDEC )
     {
@@ -169,9 +169,9 @@ p->timeSat += clock() - clk;
             return 0;
         // try replacing the critical fanin
         Vec_IntPush( p->vDivIds, Sfm_ObjSatVar(p, Vec_IntEntry(p->vDivs, iVar)) );
-clk = clock();
+clk = Abc_Clock();
         uTruth = Sfm_ComputeInterpolant( p );
-p->timeSat += clock() - clk;
+p->timeSat += Abc_Clock() - clk;
         // analyze outcomes
         if ( uTruth == SFM_SAT_UNDEC )
         {
@@ -254,7 +254,7 @@ int Sfm_NodeResub( Sfm_Ntk_t * p, int iNode )
 int Sfm_NtkPerform( Sfm_Ntk_t * p, Sfm_Par_t * pPars )
 {
     int i, k, Counter = 0;
-    p->timeTotal = clock();
+    p->timeTotal = Abc_Clock();
     if ( pPars->fVerbose )
         printf( "Performing MFS with %d fixed objects.\n", Vec_StrSum(p->vFixed) );
     p->pPars = pPars;
@@ -280,7 +280,7 @@ int Sfm_NtkPerform( Sfm_Ntk_t * p, Sfm_Par_t * pPars )
     }
     p->nTotalNodesEnd = Vec_WecSizeUsed(&p->vFanins) - Sfm_NtkPoNum(p);
     p->nTotalEdgesEnd = Vec_WecSizeSize(&p->vFanins) - Sfm_NtkPoNum(p);
-    p->timeTotal = clock() - p->timeTotal;
+    p->timeTotal = Abc_Clock() - p->timeTotal;
     if ( pPars->fVerbose )
         Sfm_NtkPrintStats( p );
     return Counter;
diff --git a/src/opt/sfm/sfmInt.h b/src/opt/sfm/sfmInt.h
index 8b0072f1..d918077c 100644
--- a/src/opt/sfm/sfmInt.h
+++ b/src/opt/sfm/sfmInt.h
@@ -112,13 +112,13 @@ struct Sfm_Ntk_t_
     int               nTimeOuts;
     int               nMaxDivs;
     // runtime
-    clock_t           timeWin;
-    clock_t           timeDiv;
-    clock_t           timeCnf;
-    clock_t           timeSat;
-    clock_t           timeOther;
-    clock_t           timeTotal;
-//    clock_t           time1;
+    abctime           timeWin;
+    abctime           timeDiv;
+    abctime           timeCnf;
+    abctime           timeSat;
+    abctime           timeOther;
+    abctime           timeTotal;
+//    abctime           time1;
 };
 
 static inline int  Sfm_NtkPiNum( Sfm_Ntk_t * p )                        { return p->nPis;                                   }
diff --git a/src/opt/sfm/sfmSat.c b/src/opt/sfm/sfmSat.c
index 01b9d4cf..f96e2078 100644
--- a/src/opt/sfm/sfmSat.c
+++ b/src/opt/sfm/sfmSat.c
@@ -55,7 +55,7 @@ void Sfm_NtkWindowToSolver( Sfm_Ntk_t * p )
 {
     Vec_Int_t * vClause;
     int RetValue, iNode = -1, iFanin, i, k;
-    clock_t clk = clock();
+    abctime clk = Abc_Clock();
 //    if ( p->pSat )
 //        printf( "%d  ", p->pSat->stats.learnts );
     sat_solver_restart( p->pSat );
@@ -93,7 +93,7 @@ void Sfm_NtkWindowToSolver( Sfm_Ntk_t * p )
     // finalize
     RetValue = sat_solver_simplify( p->pSat );
     assert( RetValue );
-    p->timeCnf += clock() - clk;
+    p->timeCnf += Abc_Clock() - clk;
 } 
 
 /**Function*************************************************************
diff --git a/src/opt/sfm/sfmWin.c b/src/opt/sfm/sfmWin.c
index 9efe30d3..9f3617d1 100644
--- a/src/opt/sfm/sfmWin.c
+++ b/src/opt/sfm/sfmWin.c
@@ -264,7 +264,7 @@ int Sfm_NtkCollectTfi_rec( Sfm_Ntk_t * p, int iNode, int nWinSizeMax )
 int Sfm_NtkCreateWindow( Sfm_Ntk_t * p, int iNode, int fVerbose )
 {
     int i, k, iTemp, nDivStart;
-    clock_t clk = clock();
+    abctime clk = Abc_Clock();
     assert( Sfm_ObjIsNode( p, iNode ) );
     Vec_IntClear( p->vLeaves ); // leaves 
     Vec_IntClear( p->vNodes );  // internal
@@ -276,7 +276,7 @@ int Sfm_NtkCreateWindow( Sfm_Ntk_t * p, int iNode, int fVerbose )
     if ( Sfm_NtkCollectTfi_rec( p, iNode, p->pPars->nWinSizeMax ) )
     {
         p->nMaxDivs++;
-        p->timeWin += clock() - clk;
+        p->timeWin += Abc_Clock() - clk;
         return 0;
     }
     // collect TFO (currently use only one level of TFO)
@@ -293,8 +293,8 @@ int Sfm_NtkCreateWindow( Sfm_Ntk_t * p, int iNode, int fVerbose )
     }
     else
         Vec_IntPush( p->vRoots, iNode );
-    p->timeWin += clock() - clk;
-    clk = clock();
+    p->timeWin += Abc_Clock() - clk;
+    clk = Abc_Clock();
     // create divisors
     Vec_IntClear( p->vDivs );
     Vec_IntForEachEntry( p->vLeaves, iTemp, i )
@@ -338,7 +338,7 @@ int Sfm_NtkCreateWindow( Sfm_Ntk_t * p, int iNode, int fVerbose )
     assert( Vec_IntSize(p->vDivs) <= p->pPars->nWinSizeMax );
     // statistics
     p->nTotalDivs += Vec_IntSize(p->vDivs);
-    p->timeDiv += clock() - clk;
+    p->timeDiv += Abc_Clock() - clk;
     if ( !fVerbose )
         return 1;
 
diff --git a/src/opt/sim/sim.h b/src/opt/sim/sim.h
index 93553a84..bb26dc1a 100644
--- a/src/opt/sim/sim.h
+++ b/src/opt/sim/sim.h
@@ -88,13 +88,13 @@ struct Sym_Man_t_
     int               nPairsRem;
     int               nPairsTotal;
     // runtime statistics
-    clock_t           timeStruct;
-    clock_t           timeCount;
-    clock_t           timeMatr;
-    clock_t           timeSim;
-    clock_t           timeFraig;
-    clock_t           timeSat;
-    clock_t           timeTotal;
+    abctime           timeStruct;
+    abctime           timeCount;
+    abctime           timeMatr;
+    abctime           timeSim;
+    abctime           timeFraig;
+    abctime           timeSat;
+    abctime           timeTotal;
 };
 
 typedef struct Sim_Man_t_ Sim_Man_t;
@@ -126,11 +126,11 @@ struct Sim_Man_t_
     int               nSatRunsSat;
     int               nSatRunsUnsat;
     // runtime statistics
-    clock_t           timeSim;
-    clock_t           timeTrav;
-    clock_t           timeFraig;
-    clock_t           timeSat;
-    clock_t           timeTotal;
+    abctime           timeSim;
+    abctime           timeTrav;
+    abctime           timeFraig;
+    abctime           timeSat;
+    abctime           timeTotal;
 };
 
 typedef struct Sim_Pat_t_ Sim_Pat_t;
diff --git a/src/opt/sim/simSupp.c b/src/opt/sim/simSupp.c
index 1cf13fa8..e8093aaa 100644
--- a/src/opt/sim/simSupp.c
+++ b/src/opt/sim/simSupp.c
@@ -105,7 +105,7 @@ Vec_Ptr_t * Sim_ComputeFunSupp( Abc_Ntk_t * pNtk, int fVerbose )
     Sim_Man_t * p;
     Vec_Ptr_t * vResult;
     int nSolved, i;
-    clock_t clk = clock();
+    abctime clk = Abc_Clock();
 
     srand( 0xABC );
 
@@ -151,7 +151,7 @@ if ( fVerbose )
     }
 
 exit:
-p->timeTotal = clock() - clk;
+p->timeTotal = Abc_Clock() - clk;
     vResult = p->vSuppFun;  
     //  p->vSuppFun = NULL;
     Sim_ManStop( p );
@@ -173,11 +173,11 @@ int Sim_ComputeSuppRound( Sim_Man_t * p, int  fUseTargets )
 {
     Vec_Int_t * vTargets;
     int i, Counter = 0;
-    clock_t clk;
+    abctime clk;
     // perform one round of random simulation
-clk = clock();
+clk = Abc_Clock();
     Sim_UtilSimulate( p, 0 );
-p->timeSim += clock() - clk;
+p->timeSim += Abc_Clock() - clk;
     // iterate through the CIs and detect COs that depend on them
     for ( i = p->iInput; i < p->nInputs; i++ )
     {
@@ -210,14 +210,14 @@ int Sim_ComputeSuppRoundNode( Sim_Man_t * p, int iNumCi, int  fUseTargets )
     int i, k, v, Output, LuckyPat, fType0, fType1;
     int Counter = 0;
     int fFirst = 1;
-    clock_t clk;
+    abctime clk;
     // collect nodes by level in the TFO of the CI 
     // this proceduredoes not collect the CIs and COs
     // but it increments TravId of the collected nodes and CIs/COs
-clk = clock();
+clk = Abc_Clock();
     pNodeCi       = Abc_NtkCi( p->pNtk, iNumCi );
     vNodesByLevel = Abc_DfsLevelized( pNodeCi, 0 );
-p->timeTrav += clock() - clk;
+p->timeTrav += Abc_Clock() - clk;
     // complement the simulation info of the selected CI
     Sim_UtilInfoFlip( p, pNodeCi );
     // simulate the levelized structure of nodes
@@ -225,9 +225,9 @@ p->timeTrav += clock() - clk;
     {
         fType0 = Abc_NodeIsTravIdCurrent( Abc_ObjFanin0(pNode) );
         fType1 = Abc_NodeIsTravIdCurrent( Abc_ObjFanin1(pNode) );
-clk = clock();
+clk = Abc_Clock();
         Sim_UtilSimulateNode( p, pNode, 1, fType0, fType1 );
-p->timeSim += clock() - clk;
+p->timeSim += Abc_Clock() - clk;
     }
     // set the simulation info of the affected COs
     if ( fUseTargets )
@@ -457,7 +457,7 @@ void Sim_SolveTargetsUsingSat( Sim_Man_t * p, int Limit )
     int * pModel;
     int RetValue, Output, Input, k, v;
     int Counter = 0;
-    clock_t clk;
+    abctime clk;
 
     p->nSatRuns = 0;
     // put targets into one array
@@ -473,12 +473,12 @@ void Sim_SolveTargetsUsingSat( Sim_Man_t * p, int Limit )
         Fraig_ParamsSetDefault( &Params );
         Params.nSeconds = ABC_INFINITY;
         Params.fInternal = 1;
-clk = clock();
+clk = Abc_Clock();
         pMan = (Fraig_Man_t *)Abc_NtkToFraig( pMiter, &Params, 0, 0 ); 
-p->timeFraig += clock() - clk;
-clk = clock();
+p->timeFraig += Abc_Clock() - clk;
+clk = Abc_Clock();
         Fraig_ManProveMiter( pMan );
-p->timeSat += clock() - clk;
+p->timeSat += Abc_Clock() - clk;
 
         // analyze the result
         RetValue = Fraig_ManCheckMiter( pMan );
diff --git a/src/opt/sim/simSym.c b/src/opt/sim/simSym.c
index 8f99dc54..591adc59 100644
--- a/src/opt/sim/simSym.c
+++ b/src/opt/sim/simSym.c
@@ -49,7 +49,7 @@ int Sim_ComputeTwoVarSymms( Abc_Ntk_t * pNtk, int fVerbose )
     Vec_Ptr_t * vResult;
     int Result;
     int i;
-    clock_t clk, clkTotal = clock();
+    abctime clk, clkTotal = Abc_Clock();
 
     srand( 0xABC );
 
@@ -61,9 +61,9 @@ int Sim_ComputeTwoVarSymms( Abc_Ntk_t * pNtk, int fVerbose )
                p->nPairsTotal, p->nPairsSymm, p->nPairsNonSymm, p->nPairsRem );
 
     // detect symmetries using circuit structure
-clk = clock();
+clk = Abc_Clock();
     Sim_SymmsStructCompute( pNtk, p->vMatrSymms, p->vSuppFun );
-p->timeStruct = clock() - clk;
+p->timeStruct = Abc_Clock() - clk;
 
     Sim_UtilCountPairsAll( p );
     p->nPairsSymmStr = p->nPairsSymm;
@@ -133,7 +133,7 @@ p->timeStruct = clock() - clk;
 
     Result = p->nPairsSymm;
     vResult = p->vMatrSymms;  
-p->timeTotal = clock() - clkTotal;
+p->timeTotal = Abc_Clock() - clkTotal;
     //  p->vMatrSymms = NULL;
     Sym_ManStop( p );
     return Result;
diff --git a/src/opt/sim/simSymSat.c b/src/opt/sim/simSymSat.c
index 14ec6806..125f7cc6 100644
--- a/src/opt/sim/simSymSat.c
+++ b/src/opt/sim/simSymSat.c
@@ -138,7 +138,7 @@ int Sim_SymmsSatProveOne( Sym_Man_t * p, int Out, int Var1, int Var2, unsigned *
     Fraig_Man_t * pMan;
     Abc_Ntk_t * pMiter;
     int RetValue, i;
-    clock_t clk;
+    abctime clk;
     int * pModel;
 
     // get the miter for this problem
@@ -150,12 +150,12 @@ int Sim_SymmsSatProveOne( Sym_Man_t * p, int Out, int Var1, int Var2, unsigned *
     Params.nPatsDyna = 512;
     Params.nSeconds = ABC_INFINITY;
 
-clk = clock();
+clk = Abc_Clock();
     pMan = (Fraig_Man_t *)Abc_NtkToFraig( pMiter, &Params, 0, 0 ); 
-p->timeFraig += clock() - clk;
-clk = clock();
+p->timeFraig += Abc_Clock() - clk;
+clk = Abc_Clock();
     Fraig_ManProveMiter( pMan );
-p->timeSat += clock() - clk;
+p->timeSat += Abc_Clock() - clk;
 
     // analyze the result
     RetValue = Fraig_ManCheckMiter( pMan );
diff --git a/src/opt/sim/simSymSim.c b/src/opt/sim/simSymSim.c
index 811397a5..fb0d60a7 100644
--- a/src/opt/sim/simSymSim.c
+++ b/src/opt/sim/simSymSim.c
@@ -50,21 +50,21 @@ void Sim_SymmsSimulate( Sym_Man_t * p, unsigned * pPat, Vec_Ptr_t * vMatrsNonSym
 {
     Abc_Obj_t * pNode;
     int i, nPairsTotal, nPairsSym, nPairsNonSym;
-    clock_t clk;
+    abctime clk;
 
     // create the simulation matrix
     Sim_SymmsCreateSquare( p, pPat );
     // simulate each node in the DFS order
-clk = clock();
+clk = Abc_Clock();
     Vec_PtrForEachEntry( Abc_Obj_t *, p->vNodes, pNode, i )
     {
 //        if ( Abc_NodeIsConst(pNode) )
 //            continue;
         Sim_UtilSimulateNodeOne( pNode, p->vSim, p->nSimWords, 0 );
     }
-p->timeSim += clock() - clk;
+p->timeSim += Abc_Clock() - clk;
     // collect info into the CO matrices
-clk = clock();
+clk = Abc_Clock();
     Abc_NtkForEachCo( p->pNtk, pNode, i )
     {
         pNode = Abc_ObjFanin0(pNode);
@@ -78,7 +78,7 @@ clk = clock();
             continue;
         Sim_SymmsDeriveInfo( p, pPat, pNode, vMatrsNonSym, i );
     }
-p->timeMatr += clock() - clk;
+p->timeMatr += Abc_Clock() - clk;
 }
 
 /**Function*************************************************************
diff --git a/src/opt/sim/simUtils.c b/src/opt/sim/simUtils.c
index 975c57a6..dc05df0f 100644
--- a/src/opt/sim/simUtils.c
+++ b/src/opt/sim/simUtils.c
@@ -634,15 +634,15 @@ int Sim_UtilCountPairsOnePrint( Extra_BitMat_t * pMat, Vec_Int_t * vSupport )
 void Sim_UtilCountPairsAllPrint( Sym_Man_t * p )
 {
     int i;
-    clock_t clk;
-clk = clock();
+    abctime clk;
+clk = Abc_Clock();
     for ( i = 0; i < p->nOutputs; i++ )
     {
         printf( "Output %2d :", i );
         Sim_UtilCountPairsOnePrint( (Extra_BitMat_t *)Vec_PtrEntry(p->vMatrSymms, i), Vec_VecEntryInt(p->vSupports, i) );
         printf( "\n" );
     }
-p->timeCount += clock() - clk;
+p->timeCount += Abc_Clock() - clk;
 }
 
 /**Function*************************************************************
@@ -659,8 +659,8 @@ p->timeCount += clock() - clk;
 void Sim_UtilCountPairsAll( Sym_Man_t * p )
 {
     int nPairsTotal, nPairsSym, nPairsNonSym, i;
-    clock_t clk;
-clk = clock();
+    abctime clk;
+clk = Abc_Clock();
     p->nPairsSymm    = 0;
     p->nPairsNonSymm = 0;
     for ( i = 0; i < p->nOutputs; i++ )
@@ -686,7 +686,7 @@ clk = clock();
     }
 //printf( "\n" );
     p->nPairsRem = p->nPairsTotal-p->nPairsSymm-p->nPairsNonSymm;
-p->timeCount += clock() - clk;
+p->timeCount += Abc_Clock() - clk;
 }
 
 /**Function*************************************************************