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

10 files changed, 155 insertions, 155 deletions

diff --git a/src/aig/ivy/ivy.h b/src/aig/ivy/ivy.h
index 1cce1217..c2bbd5ab 100644
--- a/src/aig/ivy/ivy.h
+++ b/src/aig/ivy/ivy.h
@@ -125,8 +125,8 @@ struct Ivy_Man_t_
     Vec_Ptr_t *      vPages;         // memory pages used by nodes
     Ivy_Obj_t *      pListFree;      // the list of free nodes 
     // timing statistics
-    clock_t          time1;
-    clock_t          time2;
+    abctime          time1;
+    abctime          time2;
 };
 
 struct Ivy_FraigParams_t_
diff --git a/src/aig/ivy/ivyCut.c b/src/aig/ivy/ivyCut.c
index 19d37bb2..5b5957ed 100644
--- a/src/aig/ivy/ivyCut.c
+++ b/src/aig/ivy/ivyCut.c
@@ -969,7 +969,7 @@ void Ivy_ManTestCutsAll( Ivy_Man_t * p )
 {
     Ivy_Obj_t * pObj;
     int i, nCutsCut, nCutsTotal, nNodeTotal, nNodeOver;
-    clock_t clk = clock();
+    abctime clk = Abc_Clock();
     nNodeTotal = nNodeOver = 0;
     nCutsTotal = -Ivy_ManNodeNum(p);
     Ivy_ManForEachObj( p, pObj, i )
@@ -983,7 +983,7 @@ void Ivy_ManTestCutsAll( Ivy_Man_t * p )
     }
     printf( "Total cuts = %6d. Trivial = %6d.   Nodes = %6d. Satur = %6d.  ", 
         nCutsTotal, Ivy_ManPiNum(p) + Ivy_ManNodeNum(p), nNodeTotal, nNodeOver );
-    ABC_PRT( "Time", clock() - clk );
+    ABC_PRT( "Time", Abc_Clock() - clk );
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/ivy/ivyCutTrav.c b/src/aig/ivy/ivyCutTrav.c
index 5834a6fc..75acd260 100644
--- a/src/aig/ivy/ivyCutTrav.c
+++ b/src/aig/ivy/ivyCutTrav.c
@@ -439,7 +439,7 @@ void Ivy_ManTestCutsTravAll( Ivy_Man_t * p )
     Vec_Int_t * vStore;
     Vec_Vec_t * vBitCuts;
     int i, nCutsCut, nCutsTotal, nNodeTotal, nNodeOver;
-    clock_t clk = clock();
+    abctime clk = Abc_Clock();
 
     vNodes = Vec_PtrAlloc( 100 );
     vFront = Vec_PtrAlloc( 100 );
@@ -460,7 +460,7 @@ void Ivy_ManTestCutsTravAll( Ivy_Man_t * p )
     }
     printf( "Total cuts = %6d. Trivial = %6d.   Nodes = %6d. Satur = %6d.  ", 
         nCutsTotal, Ivy_ManPiNum(p) + Ivy_ManNodeNum(p), nNodeTotal, nNodeOver );
-    ABC_PRT( "Time", clock() - clk );
+    ABC_PRT( "Time", Abc_Clock() - clk );
 
     Vec_PtrFree( vNodes );
     Vec_PtrFree( vFront );
diff --git a/src/aig/ivy/ivyFastMap.c b/src/aig/ivy/ivyFastMap.c
index 34d2796e..b8322b3f 100644
--- a/src/aig/ivy/ivyFastMap.c
+++ b/src/aig/ivy/ivyFastMap.c
@@ -67,7 +67,7 @@ static inline Ivy_Supp_t * Ivy_ObjSuppStart( Ivy_Man_t * pAig, Ivy_Obj_t * pObj
     return pSupp;
 }
 
-static void Ivy_FastMapPrint( Ivy_Man_t * pAig, int Delay, int Area, clock_t Time, char * pStr );
+static void Ivy_FastMapPrint( Ivy_Man_t * pAig, int Delay, int Area, abctime Time, char * pStr );
 static int  Ivy_FastMapDelay( Ivy_Man_t * pAig );
 static int  Ivy_FastMapArea( Ivy_Man_t * pAig );
 static void Ivy_FastMapNode( Ivy_Man_t * pAig, Ivy_Obj_t * pObj, int nLimit );
@@ -83,7 +83,7 @@ static int  Ivy_FastMapNodeRef( Ivy_Man_t * pAig, Ivy_Obj_t * pObj );
 static int  Ivy_FastMapNodeDeref( Ivy_Man_t * pAig, Ivy_Obj_t * pObj );
 
 
-extern clock_t s_MappingTime;
+extern abctime s_MappingTime;
 extern int s_MappingMem;
 
 
@@ -107,7 +107,7 @@ void Ivy_FastMapPerform( Ivy_Man_t * pAig, int nLimit, int fRecovery, int fVerbo
     Ivy_SuppMan_t * pMan;
     Ivy_Obj_t * pObj;
     int i, Delay, Area;
-    clock_t clk, clkTotal = clock();
+    abctime clk, clkTotal = Abc_Clock();
     // start the memory for supports
     pMan = ABC_ALLOC( Ivy_SuppMan_t, 1 );
     memset( pMan, 0, sizeof(Ivy_SuppMan_t) );
@@ -118,7 +118,7 @@ void Ivy_FastMapPerform( Ivy_Man_t * pAig, int nLimit, int fRecovery, int fVerbo
     memset( pMan->pMem, 0, pMan->nObjs * pMan->nSize );
     pMan->vLuts  = Vec_VecAlloc( 100 );
     pAig->pData  = pMan;
-clk = clock();
+clk = Abc_Clock();
     // set the PI mapping
     Ivy_ObjSuppStart( pAig, Ivy_ManConst1(pAig) );
     Ivy_ManForEachPi( pAig, pObj, i )
@@ -130,22 +130,22 @@ clk = clock();
     Delay = Ivy_FastMapDelay( pAig );
     Area = Ivy_FastMapArea(pAig);
     if ( fVerbose )
-        Ivy_FastMapPrint( pAig, Delay, Area, clock() - clk, "Delay oriented mapping: " );
+        Ivy_FastMapPrint( pAig, Delay, Area, Abc_Clock() - clk, "Delay oriented mapping: " );
 
 // 2-1-2 (doing 2-1-2-1-2 improves 0.5%)
 
     if ( fRecovery )
     {
-clk = clock();
+clk = Abc_Clock();
     Ivy_FastMapRequired( pAig, Delay, 0 );
     // remap the nodes
     Ivy_FastMapRecover( pAig, nLimit );
     Delay = Ivy_FastMapDelay( pAig );
     Area = Ivy_FastMapArea(pAig);
     if ( fVerbose )
-        Ivy_FastMapPrint( pAig, Delay, Area, clock() - clk, "Area recovery 2       : " );
+        Ivy_FastMapPrint( pAig, Delay, Area, Abc_Clock() - clk, "Area recovery 2       : " );
 
-clk = clock();
+clk = Abc_Clock();
     Ivy_FastMapRequired( pAig, Delay, 0 );
     // iterate through all nodes in the topological order
     Ivy_ManForEachNode( pAig, pObj, i )
@@ -153,20 +153,20 @@ clk = clock();
     Delay = Ivy_FastMapDelay( pAig );
     Area = Ivy_FastMapArea(pAig);
     if ( fVerbose )
-        Ivy_FastMapPrint( pAig, Delay, Area, clock() - clk, "Area recovery 1       : " );
+        Ivy_FastMapPrint( pAig, Delay, Area, Abc_Clock() - clk, "Area recovery 1       : " );
 
-clk = clock();
+clk = Abc_Clock();
     Ivy_FastMapRequired( pAig, Delay, 0 );
     // remap the nodes
     Ivy_FastMapRecover( pAig, nLimit );
     Delay = Ivy_FastMapDelay( pAig );
     Area = Ivy_FastMapArea(pAig);
     if ( fVerbose )
-        Ivy_FastMapPrint( pAig, Delay, Area, clock() - clk, "Area recovery 2       : " );
+        Ivy_FastMapPrint( pAig, Delay, Area, Abc_Clock() - clk, "Area recovery 2       : " );
     }
 
 
-    s_MappingTime = clock() - clkTotal;
+    s_MappingTime = Abc_Clock() - clkTotal;
     s_MappingMem = pMan->nObjs * pMan->nSize;
 /*
     {
@@ -211,7 +211,7 @@ void Ivy_FastMapStop( Ivy_Man_t * pAig )
   SeeAlso     []
 
 ***********************************************************************/
-void Ivy_FastMapPrint( Ivy_Man_t * pAig, int Delay, int Area, clock_t Time, char * pStr )
+void Ivy_FastMapPrint( Ivy_Man_t * pAig, int Delay, int Area, abctime Time, char * pStr )
 {
     printf( "%s : Delay = %3d. Area = %6d. ", pStr, Delay, Area );
     ABC_PRT( "Time", Time );
diff --git a/src/aig/ivy/ivyFraig.c b/src/aig/ivy/ivyFraig.c
index 776a41b3..4a1487e7 100644
--- a/src/aig/ivy/ivyFraig.c
+++ b/src/aig/ivy/ivyFraig.c
@@ -93,16 +93,16 @@ struct Ivy_FraigMan_t_
     int                 nSatFails;
     int                 nSatFailsReal;
     // runtime
-    clock_t             timeSim;
-    clock_t             timeTrav;
-    clock_t             timeSat;
-    clock_t             timeSatUnsat;
-    clock_t             timeSatSat;
-    clock_t             timeSatFail;
-    clock_t             timeRef;
-    clock_t             timeTotal;
-    clock_t             time1;
-    clock_t             time2;
+    abctime             timeSim;
+    abctime             timeTrav;
+    abctime             timeSat;
+    abctime             timeSatUnsat;
+    abctime             timeSatSat;
+    abctime             timeSatFail;
+    abctime             timeRef;
+    abctime             timeTotal;
+    abctime             time1;
+    abctime             time2;
 };
 
 typedef struct Prove_ParamsStruct_t_      Prove_Params_t;
@@ -198,7 +198,7 @@ static int           Ivy_FraigSetActivityFactors( Ivy_FraigMan_t * p, Ivy_Obj_t
 static void          Ivy_FraigAddToPatScores( Ivy_FraigMan_t * p, Ivy_Obj_t * pClass, Ivy_Obj_t * pClassNew );
 static int           Ivy_FraigMiterStatus( Ivy_Man_t * pMan );
 static void          Ivy_FraigMiterProve( Ivy_FraigMan_t * p );
-static void          Ivy_FraigMiterPrint( Ivy_Man_t * pNtk, char * pString, clock_t clk, int fVerbose );
+static void          Ivy_FraigMiterPrint( Ivy_Man_t * pNtk, char * pString, abctime clk, int fVerbose );
 static int *         Ivy_FraigCreateModel( Ivy_FraigMan_t * p );
 
 static int Ivy_FraigNodesAreEquivBdd( Ivy_Obj_t * pObj1, Ivy_Obj_t * pObj2 );
@@ -258,7 +258,7 @@ int Ivy_FraigProve( Ivy_Man_t ** ppManAig, void * pPars )
     Ivy_FraigParams_t Params, * pIvyParams = &Params; 
     Ivy_Man_t * pManAig, * pManTemp;
     int RetValue, nIter;
-    clock_t clk;//, Counter;
+    abctime clk;//, Counter;
     ABC_INT64_T nSatConfs = 0, nSatInspects = 0;
 
     // start the network and parameters
@@ -280,7 +280,7 @@ int Ivy_FraigProve( Ivy_Man_t ** ppManAig, void * pPars )
     // if SAT only, solve without iteration
     if ( !pParams->fUseRewriting && !pParams->fUseFraiging )
     {
-        clk = clock();
+        clk = Abc_Clock();
         pIvyParams->nBTLimitMiter = pParams->nMiteringLimitLast / Ivy_ManPoNum(pManAig);
         pManAig = Ivy_FraigMiter( pManTemp = pManAig, pIvyParams );  Ivy_ManStop( pManTemp );
         RetValue = Ivy_FraigMiterStatus( pManAig );
@@ -292,7 +292,7 @@ int Ivy_FraigProve( Ivy_Man_t ** ppManAig, void * pPars )
     if ( Ivy_ManNodeNum(pManAig) < 500 )
     {
         // run the first mitering
-        clk = clock();
+        clk = Abc_Clock();
         pIvyParams->nBTLimitMiter = pParams->nMiteringLimitStart / Ivy_ManPoNum(pManAig);
         pManAig = Ivy_FraigMiter( pManTemp = pManAig, pIvyParams );  Ivy_ManStop( pManTemp );
         RetValue = Ivy_FraigMiterStatus( pManAig );
@@ -320,7 +320,7 @@ int Ivy_FraigProve( Ivy_Man_t ** ppManAig, void * pPars )
         if ( pParams->fUseRewriting )
         { // bug in Ivy_NodeFindCutsAll() when leaves are identical!
 /*
-            clk = clock();
+            clk = Abc_Clock();
             Counter = (int)(pParams->nRewritingLimitStart * pow(pParams->nRewritingLimitMulti,nIter));
             pManAig = Ivy_ManRwsat( pManAig, 0 );  
             RetValue = Ivy_FraigMiterStatus( pManAig );
@@ -338,7 +338,7 @@ int Ivy_FraigProve( Ivy_Man_t ** ppManAig, void * pPars )
         // try fraiging followed by mitering
         if ( pParams->fUseFraiging )
         {
-            clk = clock();
+            clk = Abc_Clock();
             pIvyParams->nBTLimitNode  = (int)(pParams->nFraigingLimitStart * pow(pParams->nFraigingLimitMulti,nIter));
             pIvyParams->nBTLimitMiter = 1 + (int)(pParams->nMiteringLimitStart * pow(pParams->nMiteringLimitMulti,nIter)) / Ivy_ManPoNum(pManAig);
             pManAig = Ivy_FraigPerform_int( pManTemp = pManAig, pIvyParams, pParams->nTotalBacktrackLimit, pParams->nTotalInspectLimit, &nSatConfs, &nSatInspects );  Ivy_ManStop( pManTemp );
@@ -368,7 +368,7 @@ int Ivy_FraigProve( Ivy_Man_t ** ppManAig, void * pPars )
             printf( "Attempting SAT with conflict limit %d ...\n", pParams->nMiteringLimitLast );
             fflush( stdout );
         }
-        clk = clock();
+        clk = Abc_Clock();
         pIvyParams->nBTLimitMiter = pParams->nMiteringLimitLast / Ivy_ManPoNum(pManAig);
         if ( pParams->nTotalBacktrackLimit )
             s_nBTLimitGlobal  = pParams->nTotalBacktrackLimit - pParams->nTotalBacktracksMade;
@@ -415,10 +415,10 @@ Ivy_Man_t * Ivy_FraigPerform_int( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pPara
 { 
     Ivy_FraigMan_t * p;
     Ivy_Man_t * pManAigNew;
-    clock_t clk;
+    abctime clk;
     if ( Ivy_ManNodeNum(pManAig) == 0 )
         return Ivy_ManDup(pManAig);
-clk = clock();
+clk = Abc_Clock();
     assert( Ivy_ManLatchNum(pManAig) == 0 );
     p = Ivy_FraigStart( pManAig, pParams );
     // set global limits
@@ -428,7 +428,7 @@ clk = clock();
     Ivy_FraigSimulate( p );
     Ivy_FraigSweep( p );
     pManAigNew = p->pManFraig;
-p->timeTotal = clock() - clk;
+p->timeTotal = Abc_Clock() - clk;
     if ( pnSatConfs )
         *pnSatConfs = p->pSat? p->pSat->stats.conflicts : 0;
     if ( pnSatInspects )
@@ -452,16 +452,16 @@ Ivy_Man_t * Ivy_FraigPerform( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams )
 {
     Ivy_FraigMan_t * p;
     Ivy_Man_t * pManAigNew;
-    clock_t clk;
+    abctime clk;
     if ( Ivy_ManNodeNum(pManAig) == 0 )
         return Ivy_ManDup(pManAig);
-clk = clock();
+clk = Abc_Clock();
     assert( Ivy_ManLatchNum(pManAig) == 0 );
     p = Ivy_FraigStart( pManAig, pParams );
     Ivy_FraigSimulate( p );
     Ivy_FraigSweep( p );
     pManAigNew = p->pManFraig;
-p->timeTotal = clock() - clk;
+p->timeTotal = Abc_Clock() - clk;
     Ivy_FraigStop( p );
     return pManAigNew;
 }
@@ -483,8 +483,8 @@ Ivy_Man_t * Ivy_FraigMiter( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams )
     Ivy_Man_t * pManAigNew;
     Ivy_Obj_t * pObj;
     int i;
-    clock_t clk;
-clk = clock();
+    abctime clk;
+clk = Abc_Clock();
     assert( Ivy_ManLatchNum(pManAig) == 0 );
     p = Ivy_FraigStartSimple( pManAig, pParams );
     // set global limits
@@ -508,7 +508,7 @@ clk = clock();
     // remove dangling nodes 
     Ivy_ManCleanup( p->pManFraig );
     pManAigNew = p->pManFraig;
-p->timeTotal = clock() - clk;
+p->timeTotal = Abc_Clock() - clk;
 
 //printf( "Final nodes = %6d. ", Ivy_ManNodeNum(pManAigNew) );
 //ABC_PRT( "Time", p->timeTotal );
@@ -991,8 +991,8 @@ void Ivy_FraigSimulateOne( Ivy_FraigMan_t * p )
 {
     Ivy_Obj_t * pObj;
     int i;
-    clock_t clk;
-clk = clock();
+    abctime clk;
+clk = Abc_Clock();
     Ivy_ManForEachNode( p->pManAig, pObj, i )
     {
         Ivy_NodeSimulate( p, pObj );
@@ -1005,7 +1005,7 @@ clk = clock();
         printf( "\n" );
 */
     }
-p->timeSim += clock() - clk;
+p->timeSim += Abc_Clock() - clk;
 p->nSimRounds++;
 }
 
@@ -1023,11 +1023,11 @@ p->nSimRounds++;
 void Ivy_FraigSimulateOneSim( Ivy_FraigMan_t * p )
 {
     Ivy_FraigSim_t * pSims;
-    clock_t clk;
-clk = clock();
+    abctime clk;
+clk = Abc_Clock();
     for ( pSims = p->pSimStart; pSims; pSims = pSims->pNext )
         Ivy_NodeSimulateSim( p, pSims );
-p->timeSim += clock() - clk;
+p->timeSim += Abc_Clock() - clk;
 p->nSimRounds++;
 }
 
@@ -1388,7 +1388,7 @@ int Ivy_FraigRefineClasses( Ivy_FraigMan_t * p )
 {
     Ivy_Obj_t * pClass, * pClass2;
     int RetValue, Counter = 0;
-    clock_t clk;
+    abctime clk;
     // check if some outputs already became non-constant
     // this is a special case when computation can be stopped!!!
     if ( p->pParams->fProve )
@@ -1396,7 +1396,7 @@ int Ivy_FraigRefineClasses( Ivy_FraigMan_t * p )
     if ( p->pManFraig->pData )
         return 0;
     // refine the classed
-clk = clock();
+clk = Abc_Clock();
     Ivy_FraigForEachEquivClassSafe( p->lClasses.pHead, pClass, pClass2 )
     {
         if ( pClass->fMarkA )
@@ -1406,9 +1406,9 @@ clk = clock();
 //if ( Ivy_ObjIsConst1(pClass) )
 //printf( "%d ", RetValue );
 //if ( Ivy_ObjIsConst1(pClass) )
-//    p->time1 += clock() - clk;
+//    p->time1 += Abc_Clock() - clk;
     }
-p->timeRef += clock() - clk;
+p->timeRef += Abc_Clock() - clk;
     return Counter;
 }
 
@@ -1793,12 +1793,12 @@ void Ivy_FraigResimulate( Ivy_FraigMan_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Ivy_FraigMiterPrint( Ivy_Man_t * pNtk, char * pString, clock_t clk, int fVerbose )
+void Ivy_FraigMiterPrint( Ivy_Man_t * pNtk, char * pString, abctime clk, int fVerbose )
 {
     if ( !fVerbose )
         return;
     printf( "Nodes = %7d.  Levels = %4d.  ", Ivy_ManNodeNum(pNtk), Ivy_ManLevels(pNtk) );
-    ABC_PRT( pString, clock() - clk );
+    ABC_PRT( pString, Abc_Clock() - clk );
 }
 
 /**Function*************************************************************
@@ -1881,13 +1881,13 @@ void Ivy_FraigMiterProve( Ivy_FraigMan_t * p )
 {
     Ivy_Obj_t * pObj, * pObjNew;
     int i, RetValue;
-    clock_t clk = clock();
+    abctime clk = Abc_Clock();
     int fVerbose = 0;
     Ivy_ManForEachPo( p->pManAig, pObj, i )
     {
         if ( i && fVerbose )
         {
-            ABC_PRT( "Time", clock() -clk );
+            ABC_PRT( "Time", Abc_Clock() -clk );
         }
         pObjNew = Ivy_ObjChild0Equiv(pObj);
         // check if the output is constant 1
@@ -1950,7 +1950,7 @@ void Ivy_FraigMiterProve( Ivy_FraigMan_t * p )
     }
     if ( fVerbose )
     {
-        ABC_PRT( "Time", clock() -clk );
+        ABC_PRT( "Time", Abc_Clock() -clk );
     }
 }
 
@@ -2099,7 +2099,7 @@ void Ivy_FraigPrintActivity( Ivy_FraigMan_t * p )
 int Ivy_FraigNodesAreEquiv( Ivy_FraigMan_t * p, Ivy_Obj_t * pOld, Ivy_Obj_t * pNew )
 {
     int pLits[4], RetValue, RetValue1, nBTLimit;
-    clock_t clk; //, clk2 = clock();
+    abctime clk; //, clk2 = Abc_Clock();
 
     // make sure the nodes are not complemented
     assert( !Ivy_IsComplement(pNew) );
@@ -2141,17 +2141,17 @@ int Ivy_FraigNodesAreEquiv( Ivy_FraigMan_t * p, Ivy_Obj_t * pOld, Ivy_Obj_t * pN
 
     // solve under assumptions
     // A = 1; B = 0     OR     A = 1; B = 1 
-clk = clock();
+clk = Abc_Clock();
     pLits[0] = toLitCond( Ivy_ObjSatNum(pOld), 0 );
     pLits[1] = toLitCond( Ivy_ObjSatNum(pNew), pOld->fPhase == pNew->fPhase );
 //Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 );
     RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2, 
         (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, 
         p->nBTLimitGlobal, p->nInsLimitGlobal );
-p->timeSat += clock() - clk;
+p->timeSat += Abc_Clock() - clk;
     if ( RetValue1 == 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 );
@@ -2161,14 +2161,14 @@ p->timeSatUnsat += clock() - clk;
     }
     else if ( RetValue1 == l_True )
     {
-p->timeSatSat += clock() - clk;
+p->timeSatSat += Abc_Clock() - clk;
         Ivy_FraigSavePattern( p );
         p->nSatCallsSat++;
         return 0;
     }
     else // if ( RetValue1 == l_Undef )
     {
-p->timeSatFail += clock() - clk;
+p->timeSatFail += Abc_Clock() - clk;
 /*
         if ( nBTLimit > 1000 )
         {
@@ -2194,16 +2194,16 @@ p->timeSatFail += clock() - clk;
 
     // solve under assumptions
     // A = 0; B = 1     OR     A = 0; B = 0 
-clk = clock();
+clk = Abc_Clock();
     pLits[0] = toLitCond( Ivy_ObjSatNum(pOld), 1 );
     pLits[1] = toLitCond( Ivy_ObjSatNum(pNew), pOld->fPhase ^ pNew->fPhase );
     RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2, 
         (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, 
         p->nBTLimitGlobal, p->nInsLimitGlobal );
-p->timeSat += clock() - clk;
+p->timeSat += Abc_Clock() - clk;
     if ( RetValue1 == 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 );
@@ -2212,14 +2212,14 @@ p->timeSatUnsat += clock() - clk;
     }
     else if ( RetValue1 == l_True )
     {
-p->timeSatSat += clock() - clk;
+p->timeSatSat += Abc_Clock() - clk;
         Ivy_FraigSavePattern( p );
         p->nSatCallsSat++;
         return 0;
     }
     else // if ( RetValue1 == l_Undef )
     {
-p->timeSatFail += clock() - clk;
+p->timeSatFail += Abc_Clock() - clk;
 /*
         if ( nBTLimit > 1000 )
         {
@@ -2238,12 +2238,12 @@ p->timeSatFail += clock() - clk;
     // check BDD proof
     {
         int RetVal;
-        ABC_PRT( "Sat", clock() - clk2 );
-        clk2 = clock();
+        ABC_PRT( "Sat", Abc_Clock() - clk2 );
+        clk2 = Abc_Clock();
         RetVal = Ivy_FraigNodesAreEquivBdd( pOld, pNew );
 //        printf( "%d ", RetVal );
         assert( RetVal );
-        ABC_PRT( "Bdd", clock() - clk2 );
+        ABC_PRT( "Bdd", Abc_Clock() - clk2 );
         printf( "\n" );
     }
 */
@@ -2266,7 +2266,7 @@ p->timeSatFail += clock() - clk;
 int Ivy_FraigNodeIsConst( Ivy_FraigMan_t * p, Ivy_Obj_t * pNew )
 {
     int pLits[2], RetValue1;
-    clock_t clk;
+    abctime clk;
     int RetValue;
 
     // make sure the nodes are not complemented
@@ -2293,15 +2293,15 @@ int Ivy_FraigNodeIsConst( Ivy_FraigMan_t * p, Ivy_Obj_t * pNew )
     Ivy_FraigSetActivityFactors( p, NULL, pNew ); 
 
     // solve under assumptions
-clk = clock();
+clk = Abc_Clock();
     pLits[0] = toLitCond( Ivy_ObjSatNum(pNew), pNew->fPhase );
     RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 1, 
         (ABC_INT64_T)p->pParams->nBTLimitMiter, (ABC_INT64_T)0, 
         p->nBTLimitGlobal, p->nInsLimitGlobal );
-p->timeSat += clock() - clk;
+p->timeSat += Abc_Clock() - clk;
     if ( RetValue1 == l_False )
     {
-p->timeSatUnsat += clock() - clk;
+p->timeSatUnsat += Abc_Clock() - clk;
         pLits[0] = lit_neg( pLits[0] );
         RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 1 );
         assert( RetValue );
@@ -2310,7 +2310,7 @@ p->timeSatUnsat += clock() - clk;
     }
     else if ( RetValue1 == l_True )
     {
-p->timeSatSat += clock() - clk;
+p->timeSatSat += Abc_Clock() - clk;
         if ( p->pPatWords )
             Ivy_FraigSavePattern( p );
         p->nSatCallsSat++;
@@ -2318,7 +2318,7 @@ p->timeSatSat += clock() - clk;
     }
     else // if ( RetValue1 == l_Undef )
     {
-p->timeSatFail += clock() - clk;
+p->timeSatFail += Abc_Clock() - clk;
 /*
         if ( p->pParams->nBTLimitMiter > 1000 )
         {
@@ -2636,9 +2636,9 @@ int Ivy_FraigSetActivityFactors_rec( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj, int L
 int Ivy_FraigSetActivityFactors( Ivy_FraigMan_t * p, Ivy_Obj_t * pOld, Ivy_Obj_t * pNew )
 {
     int LevelMin, LevelMax;
-    clock_t clk;
+    abctime clk;
     assert( pOld || pNew );
-clk = clock(); 
+clk = Abc_Clock(); 
     // reset the active variables
     veci_resize(&p->pSat->act_vars, 0);
     // prepare for traversal
@@ -2653,7 +2653,7 @@ clk = clock();
     if ( pNew && !Ivy_ObjIsConst1(pNew) )
         Ivy_FraigSetActivityFactors_rec( p, pNew, LevelMin, LevelMax );
 //Ivy_FraigPrintActivity( p );
-p->timeTrav += clock() - clk;
+p->timeTrav += Abc_Clock() - clk;
     return 1;
 }
 
diff --git a/src/aig/ivy/ivyObj.c b/src/aig/ivy/ivyObj.c
index becf69d1..2829fd38 100644
--- a/src/aig/ivy/ivyObj.c
+++ b/src/aig/ivy/ivyObj.c
@@ -354,7 +354,7 @@ void Ivy_ObjReplace( Ivy_Man_t * p, Ivy_Obj_t * pObjOld, Ivy_Obj_t * pObjNew, in
     assert( !Ivy_IsComplement(pObjNew) );
     if ( fUpdateLevel )
     {
-//clk = clock();
+//clk = Abc_Clock();
         // if the new node's arrival time is different, recursively update arrival time of the fanouts
         if ( p->fFanout && !Ivy_ObjIsBuf(pObjNew) && pObjOld->Level != pObjNew->Level )
         {
@@ -362,9 +362,9 @@ void Ivy_ObjReplace( Ivy_Man_t * p, Ivy_Obj_t * pObjOld, Ivy_Obj_t * pObjNew, in
             pObjOld->Level = pObjNew->Level;
             Ivy_ObjUpdateLevel_rec( p, pObjOld );
         }
-//p->time1 += clock() - clk;
+//p->time1 += Abc_Clock() - clk;
         // if the new node's required time has changed, recursively update required time of the fanins
-//clk = clock();
+//clk = Abc_Clock();
         if ( p->vRequired )
         {
             int ReqNew = Vec_IntEntry(p->vRequired, pObjOld->Id);
@@ -374,7 +374,7 @@ void Ivy_ObjReplace( Ivy_Man_t * p, Ivy_Obj_t * pObjOld, Ivy_Obj_t * pObjNew, in
                 Ivy_ObjUpdateLevelR_rec( p, pObjNew, ReqNew );
             }
         }
-//p->time2 += clock() - clk;
+//p->time2 += Abc_Clock() - clk;
     }
     // delete the old object
     if ( fDeleteOld )
diff --git a/src/aig/ivy/ivyResyn.c b/src/aig/ivy/ivyResyn.c
index dc483bf6..1eacbe5e 100644
--- a/src/aig/ivy/ivyResyn.c
+++ b/src/aig/ivy/ivyResyn.c
@@ -44,30 +44,30 @@ ABC_NAMESPACE_IMPL_START
 ***********************************************************************/
 Ivy_Man_t * Ivy_ManResyn0( Ivy_Man_t * pMan, int fUpdateLevel, int fVerbose )
 {
-    clock_t clk;
+    abctime clk;
     Ivy_Man_t * pTemp;
 
 if ( fVerbose ) { printf( "Original:\n" ); }
 if ( fVerbose ) Ivy_ManPrintStats( pMan );
 
-clk = clock();
+clk = Abc_Clock();
     pMan = Ivy_ManBalance( pMan, fUpdateLevel );
 if ( fVerbose ) { printf( "\n" ); }
-if ( fVerbose ) { ABC_PRT( "Balance", clock() - clk ); }
+if ( fVerbose ) { ABC_PRT( "Balance", Abc_Clock() - clk ); }
 if ( fVerbose ) Ivy_ManPrintStats( pMan );
 
 //    Ivy_ManRewriteAlg( pMan, fUpdateLevel, 0 );
-clk = clock();
+clk = Abc_Clock();
     Ivy_ManRewritePre( pMan, fUpdateLevel, 0, 0 );
 if ( fVerbose ) { printf( "\n" ); }
-if ( fVerbose ) { ABC_PRT( "Rewrite", clock() - clk ); }
+if ( fVerbose ) { ABC_PRT( "Rewrite", Abc_Clock() - clk ); }
 if ( fVerbose ) Ivy_ManPrintStats( pMan );
 
-clk = clock();
+clk = Abc_Clock();
     pMan = Ivy_ManBalance( pTemp = pMan, fUpdateLevel );
     Ivy_ManStop( pTemp );
 if ( fVerbose ) { printf( "\n" ); }
-if ( fVerbose ) { ABC_PRT( "Balance", clock() - clk ); }
+if ( fVerbose ) { ABC_PRT( "Balance", Abc_Clock() - clk ); }
 if ( fVerbose ) Ivy_ManPrintStats( pMan );
     return pMan;
 }
@@ -85,58 +85,58 @@ if ( fVerbose ) Ivy_ManPrintStats( pMan );
 ***********************************************************************/
 Ivy_Man_t * Ivy_ManResyn( Ivy_Man_t * pMan, int fUpdateLevel, int fVerbose )
 {
-    clock_t clk;
+    abctime clk;
     Ivy_Man_t * pTemp;
 
 if ( fVerbose ) { printf( "Original:\n" ); }
 if ( fVerbose ) Ivy_ManPrintStats( pMan );
 
-clk = clock();
+clk = Abc_Clock();
     pMan = Ivy_ManBalance( pMan, fUpdateLevel );
 if ( fVerbose ) { printf( "\n" ); }
-if ( fVerbose ) { ABC_PRT( "Balance", clock() - clk ); }
+if ( fVerbose ) { ABC_PRT( "Balance", Abc_Clock() - clk ); }
 if ( fVerbose ) Ivy_ManPrintStats( pMan );
 
 //    Ivy_ManRewriteAlg( pMan, fUpdateLevel, 0 );
-clk = clock();
+clk = Abc_Clock();
     Ivy_ManRewritePre( pMan, fUpdateLevel, 0, 0 );
 if ( fVerbose ) { printf( "\n" ); }
-if ( fVerbose ) { ABC_PRT( "Rewrite", clock() - clk ); }
+if ( fVerbose ) { ABC_PRT( "Rewrite", Abc_Clock() - clk ); }
 if ( fVerbose ) Ivy_ManPrintStats( pMan );
 
-clk = clock();
+clk = Abc_Clock();
     pMan = Ivy_ManBalance( pTemp = pMan, fUpdateLevel );
     Ivy_ManStop( pTemp );
 if ( fVerbose ) { printf( "\n" ); }
-if ( fVerbose ) { ABC_PRT( "Balance", clock() - clk ); }
+if ( fVerbose ) { ABC_PRT( "Balance", Abc_Clock() - clk ); }
 if ( fVerbose ) Ivy_ManPrintStats( pMan );
 
 //    Ivy_ManRewriteAlg( pMan, fUpdateLevel, 1 );
-clk = clock();
+clk = Abc_Clock();
     Ivy_ManRewritePre( pMan, fUpdateLevel, 1, 0 );
 if ( fVerbose ) { printf( "\n" ); }
-if ( fVerbose ) { ABC_PRT( "Rewrite", clock() - clk ); }
+if ( fVerbose ) { ABC_PRT( "Rewrite", Abc_Clock() - clk ); }
 if ( fVerbose ) Ivy_ManPrintStats( pMan );
 
-clk = clock();
+clk = Abc_Clock();
     pMan = Ivy_ManBalance( pTemp = pMan, fUpdateLevel );
     Ivy_ManStop( pTemp );
 if ( fVerbose ) { printf( "\n" ); }
-if ( fVerbose ) { ABC_PRT( "Balance", clock() - clk ); }
+if ( fVerbose ) { ABC_PRT( "Balance", Abc_Clock() - clk ); }
 if ( fVerbose ) Ivy_ManPrintStats( pMan );
 
 //    Ivy_ManRewriteAlg( pMan, fUpdateLevel, 1 );
-clk = clock();
+clk = Abc_Clock();
     Ivy_ManRewritePre( pMan, fUpdateLevel, 1, 0 );
 if ( fVerbose ) { printf( "\n" ); }
-if ( fVerbose ) { ABC_PRT( "Rewrite", clock() - clk ); }
+if ( fVerbose ) { ABC_PRT( "Rewrite", Abc_Clock() - clk ); }
 if ( fVerbose ) Ivy_ManPrintStats( pMan );
 
-clk = clock();
+clk = Abc_Clock();
     pMan = Ivy_ManBalance( pTemp = pMan, fUpdateLevel );
     Ivy_ManStop( pTemp );
 if ( fVerbose ) { printf( "\n" ); }
-if ( fVerbose ) { ABC_PRT( "Balance", clock() - clk ); }
+if ( fVerbose ) { ABC_PRT( "Balance", Abc_Clock() - clk ); }
 if ( fVerbose ) Ivy_ManPrintStats( pMan );
     return pMan;
 }
@@ -154,38 +154,38 @@ if ( fVerbose ) Ivy_ManPrintStats( pMan );
 ***********************************************************************/
 Ivy_Man_t * Ivy_ManRwsat( Ivy_Man_t * pMan, int fVerbose )
 {
-    clock_t clk;
+    abctime clk;
     Ivy_Man_t * pTemp;
 
 if ( fVerbose ) { printf( "Original:\n" ); }
 if ( fVerbose ) Ivy_ManPrintStats( pMan );
 
-clk = clock();
+clk = Abc_Clock();
     Ivy_ManRewritePre( pMan, 0, 0, 0 );
 if ( fVerbose ) { printf( "\n" ); }
-if ( fVerbose ) { ABC_PRT( "Rewrite", clock() - clk ); }
+if ( fVerbose ) { ABC_PRT( "Rewrite", Abc_Clock() - clk ); }
 if ( fVerbose ) Ivy_ManPrintStats( pMan );
 
-clk = clock();
+clk = Abc_Clock();
     pMan = Ivy_ManBalance( pTemp = pMan, 0 );
 //    pMan = Ivy_ManDup( pTemp = pMan );
     Ivy_ManStop( pTemp );
 if ( fVerbose ) { printf( "\n" ); }
-if ( fVerbose ) { ABC_PRT( "Balance", clock() - clk ); }
+if ( fVerbose ) { ABC_PRT( "Balance", Abc_Clock() - clk ); }
 if ( fVerbose ) Ivy_ManPrintStats( pMan );
 
 /*
-clk = clock();
+clk = Abc_Clock();
     Ivy_ManRewritePre( pMan, 0, 0, 0 );
 if ( fVerbose ) { printf( "\n" ); }
-if ( fVerbose ) { ABC_PRT( "Rewrite", clock() - clk ); }
+if ( fVerbose ) { ABC_PRT( "Rewrite", Abc_Clock() - clk ); }
 if ( fVerbose ) Ivy_ManPrintStats( pMan );
 
-clk = clock();
+clk = Abc_Clock();
     pMan = Ivy_ManBalance( pTemp = pMan, 0 );
     Ivy_ManStop( pTemp );
 if ( fVerbose ) { printf( "\n" ); }
-if ( fVerbose ) { ABC_PRT( "Balance", clock() - clk ); }
+if ( fVerbose ) { ABC_PRT( "Balance", Abc_Clock() - clk ); }
 if ( fVerbose ) Ivy_ManPrintStats( pMan );
 */
     return pMan;
diff --git a/src/aig/ivy/ivyRwr.c b/src/aig/ivy/ivyRwr.c
index 2e3689c1..a4bfe54b 100644
--- a/src/aig/ivy/ivyRwr.c
+++ b/src/aig/ivy/ivyRwr.c
@@ -57,7 +57,7 @@ int Ivy_ManRewritePre( Ivy_Man_t * p, int fUpdateLevel, int fUseZeroCost, int fV
     Rwt_Man_t * pManRwt;
     Ivy_Obj_t * pNode;
     int i, nNodes, nGain;
-    clock_t clk, clkStart = clock();
+    abctime clk, clkStart = Abc_Clock();
     // start the rewriting manager
     pManRwt = Rwt_ManStart( 0 );
     p->pData = pManRwt;
@@ -105,14 +105,14 @@ int Ivy_ManRewritePre( Ivy_Man_t * p, int fUpdateLevel, int fUseZeroCost, int fV
             }
 */
             // complement the FF if needed
-clk = clock();
+clk = Abc_Clock();
             if ( fCompl ) Dec_GraphComplement( pGraph );
             Ivy_GraphUpdateNetwork( p, pNode, pGraph, fUpdateLevel, nGain );
             if ( fCompl ) Dec_GraphComplement( pGraph );
-Rwt_ManAddTimeUpdate( pManRwt, clock() - clk );
+Rwt_ManAddTimeUpdate( pManRwt, Abc_Clock() - clk );
         }
     }
-Rwt_ManAddTimeTotal( pManRwt, clock() - clkStart );
+Rwt_ManAddTimeTotal( pManRwt, Abc_Clock() - clkStart );
     // print stats
     if ( fVerbose )
         Rwt_ManPrintStats( pManRwt );
@@ -164,18 +164,18 @@ int Ivy_NodeRewrite( Ivy_Man_t * pMan, Rwt_Man_t * p, Ivy_Obj_t * pNode, int fUp
     int Required, nNodesSaved;
     int nNodesSaveCur = -1; // Suppress "might be used uninitialized"
     int i, c, GainCur, GainBest = -1;
-    clock_t clk, clk2;
+    abctime clk, clk2;
 
     p->nNodesConsidered++;
     // get the required times
     Required = fUpdateLevel? Vec_IntEntry( pMan->vRequired, pNode->Id ) : 1000000;
     // get the node's cuts
-clk = clock();
+clk = Abc_Clock();
     pStore = Ivy_NodeFindCutsAll( pMan, pNode, 5 );
-p->timeCut += clock() - clk;
+p->timeCut += Abc_Clock() - clk;
 
     // go through the cuts
-clk = clock();
+clk = Abc_Clock();
     for ( c = 1; c < pStore->nCuts; c++ )
     {
         pCut = pStore->pCuts + c;
@@ -193,9 +193,9 @@ clk = clock();
         }
         p->nCutsGood++;
         // get the fanin permutation
-clk2 = clock();
+clk2 = Abc_Clock();
         uTruth = 0xFFFF & Ivy_NodeGetTruth( pNode, pCut->pArray, pCut->nSize );  // truth table
-p->timeTruth += clock() - clk2;
+p->timeTruth += Abc_Clock() - clk2;
         pPerm = p->pPerms4[ (int) p->pPerms[uTruth] ];
         uPhase = p->pPhases[uTruth];
         // collect fanins with the corresponding permutation/phase
@@ -208,7 +208,7 @@ p->timeTruth += clock() - clk2;
             pFanin = Ivy_NotCond(pFanin, ((uPhase & (1<<i)) > 0) );
             Vec_PtrWriteEntry( p->vFaninsCur, i, pFanin );
         }
-clk2 = clock();
+clk2 = Abc_Clock();
 /*
         printf( "Considering: (" );
         Vec_PtrForEachEntry( Ivy_Obj_t *, p->vFaninsCur, pFanin, i )
@@ -224,12 +224,12 @@ clk2 = clock();
         // unmark the fanin boundary
         Vec_PtrForEachEntry( Ivy_Obj_t *, p->vFaninsCur, pFanin, i )
             Ivy_ObjRefsDec( Ivy_Regular(pFanin) );
-p->timeMffc += clock() - clk2;
+p->timeMffc += Abc_Clock() - clk2;
 
         // evaluate the cut
-clk2 = clock();
+clk2 = Abc_Clock();
         pGraph = Rwt_CutEvaluate( pMan, p, pNode, p->vFaninsCur, nNodesSaved, Required, &GainCur, uTruth );
-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 )
@@ -246,7 +246,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/aig/ivy/ivySeq.c b/src/aig/ivy/ivySeq.c
index c905fa62..c231dea6 100644
--- a/src/aig/ivy/ivySeq.c
+++ b/src/aig/ivy/ivySeq.c
@@ -65,7 +65,7 @@ int Ivy_ManRewriteSeq( Ivy_Man_t * p, int fUseZeroCost, int fVerbose )
     Rwt_Man_t * pManRwt;
     Ivy_Obj_t * pNode;
     int i, nNodes, nGain;
-    clock_t clk, clkStart = clock();
+    abctime clk, clkStart = Abc_Clock();
 
     // set the DC latch values
     Ivy_ManForEachLatch( p, pNode, i )
@@ -99,14 +99,14 @@ int Ivy_ManRewriteSeq( Ivy_Man_t * p, int fUseZeroCost, int fVerbose )
             Dec_Graph_t * pGraph = (Dec_Graph_t *)Rwt_ManReadDecs(pManRwt);
             int fCompl           = Rwt_ManReadCompl(pManRwt);
             // complement the FF if needed
-clk = clock();
+clk = Abc_Clock();
             if ( fCompl ) Dec_GraphComplement( pGraph );
             Ivy_GraphUpdateNetworkSeq( p, pNode, pGraph, nGain );
             if ( fCompl ) Dec_GraphComplement( pGraph );
-Rwt_ManAddTimeUpdate( pManRwt, clock() - clk );
+Rwt_ManAddTimeUpdate( pManRwt, Abc_Clock() - clk );
         }
     }
-Rwt_ManAddTimeTotal( pManRwt, clock() - clkStart );
+Rwt_ManAddTimeTotal( pManRwt, Abc_Clock() - clkStart );
     // print stats
     if ( fVerbose )
         Rwt_ManPrintStats( pManRwt );
@@ -157,16 +157,16 @@ int Ivy_NodeRewriteSeq( Ivy_Man_t * pMan, Rwt_Man_t * p, Ivy_Obj_t * pNode, int
     int nNodesSaved;
     int nNodesSaveCur = -1; // Suppress "might be used uninitialized"
     int i, c, GainCur, GainBest = -1;
-    clock_t clk, clk2;//, clk3;
+    abctime clk, clk2;//, clk3;
 
     p->nNodesConsidered++;
     // get the node's cuts
-clk = clock();
+clk = Abc_Clock();
     pStore = Ivy_CutComputeForNode( pMan, pNode, 5 );
-p->timeCut += clock() - clk;
+p->timeCut += Abc_Clock() - clk;
 
     // go through the cuts
-clk = clock();
+clk = Abc_Clock();
     vFanout = Vec_PtrAlloc( 100 );
     for ( c = 1; c < pStore->nCuts; c++ )
     {
@@ -185,9 +185,9 @@ clk = clock();
         }
         p->nCutsGood++;
         // get the fanin permutation
-clk2 = clock();
+clk2 = Abc_Clock();
         uTruth = 0xFFFF & Ivy_CutGetTruth( pMan, pNode, pCut->pArray, pCut->nSize );  // truth table
-p->timeTruth += clock() - clk2;
+p->timeTruth += Abc_Clock() - clk2;
         pPerm = p->pPerms4[ (int)p->pPerms[uTruth] ];
         uPhase = p->pPhases[uTruth];
         // collect fanins with the corresponding permutation/phase
@@ -200,7 +200,7 @@ p->timeTruth += clock() - clk2;
             pFanin = Ivy_NotCond(pFanin, ((uPhase & (1<<i)) > 0) );
             Vec_PtrWriteEntry( p->vFaninsCur, i, pFanin );
         }
-clk2 = clock();
+clk2 = Abc_Clock();
         // mark the fanin boundary 
         Vec_PtrForEachEntry( Ivy_Obj_t *, p->vFaninsCur, pFanin, i )
             Ivy_ObjRefsInc( Ivy_Regular(pFanin) );
@@ -213,12 +213,12 @@ clk2 = clock();
         // unmark the fanin boundary
         Vec_PtrForEachEntry( Ivy_Obj_t *, p->vFaninsCur, pFanin, i )
             Ivy_ObjRefsDec( Ivy_Regular(pFanin) );
-p->timeMffc += clock() - clk2;
+p->timeMffc += Abc_Clock() - clk2;
 
         // evaluate the cut
-clk2 = clock();
+clk2 = Abc_Clock();
         pGraph = Rwt_CutEvaluateSeq( pMan, p, pNode, pCut, pPerm, p->vFaninsCur, nNodesSaved, &GainCur, uTruth );
-p->timeEval += clock() - clk2;
+p->timeEval += Abc_Clock() - clk2;
 
 
         // check if the cut is better than the current best one
@@ -239,7 +239,7 @@ p->timeEval += clock() - clk2;
         }
     }
     Vec_PtrFree( vFanout );
-p->timeRes += clock() - clk;
+p->timeRes += Abc_Clock() - clk;
 
     if ( GainBest == -1 )
         return -1;
@@ -253,9 +253,9 @@ p->timeRes += clock() - clk;
     }
 */
 
-//clk3 = clock();
+//clk3 = Abc_Clock();
 //nNewClauses = Ivy_CutTruthPrint( pMan, p->pCut, uTruth );
-//timeInv += clock() - clk;
+//timeInv += Abc_Clock() - clk;
 
 //    nClauses += nNewClauses;
 //    nMoves++;
@@ -1110,7 +1110,7 @@ void Ivy_CutComputeAll( Ivy_Man_t * p, int nInputs )
     Ivy_Store_t * pStore;
     Ivy_Obj_t * pObj;
     int i, nCutsTotal, nCutsTotalM, nNodeTotal, nNodeOver;
-    clock_t clk = clock();
+    abctime clk = Abc_Clock();
     if ( nInputs > IVY_CUT_INPUT )
     {
         printf( "Cannot compute cuts for more than %d inputs.\n", IVY_CUT_INPUT );
@@ -1130,7 +1130,7 @@ void Ivy_CutComputeAll( Ivy_Man_t * p, int nInputs )
     }
     printf( "All = %6d. Minus = %6d. Triv = %6d.   Node = %6d. Satur = %6d.  ", 
         nCutsTotal, nCutsTotalM, Ivy_ManPiNum(p) + Ivy_ManNodeNum(p), nNodeTotal, nNodeOver );
-    ABC_PRT( "Time", clock() - clk );
+    ABC_PRT( "Time", Abc_Clock() - clk );
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/ivy/ivyTable.c b/src/aig/ivy/ivyTable.c
index d2753aa8..7d8590d8 100644
--- a/src/aig/ivy/ivyTable.c
+++ b/src/aig/ivy/ivyTable.c
@@ -207,8 +207,8 @@ void Ivy_TableResize( Ivy_Man_t * p )
 {
     int * pTableOld, * pPlace;
     int nTableSizeOld, Counter, nEntries, e;
-    clock_t clk;
-clk = clock();
+    abctime clk;
+clk = Abc_Clock();
     // save the old table
     pTableOld = p->pTable;
     nTableSizeOld = p->nTableSize;
@@ -231,7 +231,7 @@ clk = clock();
     nEntries = Ivy_ManHashObjNum(p);
 //    assert( Counter == nEntries );
 //    printf( "Increasing the structural table size from %6d to %6d. ", nTableSizeOld, p->nTableSize );
-//    ABC_PRT( "Time", clock() - clk );
+//    ABC_PRT( "Time", Abc_Clock() - clk );
     // replace the table and the parameters
     ABC_FREE( pTableOld );
 }