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

10 files changed, 127 insertions, 127 deletions

diff --git a/src/proof/cec/cecCec.c b/src/proof/cec/cecCec.c
index 37df4d8d..aa6d753a 100644
--- a/src/proof/cec/cecCec.c
+++ b/src/proof/cec/cecCec.c
@@ -73,7 +73,7 @@ int Cec_ManVerifyOld( Gia_Man_t * pMiter, int fVerbose, int * piOutFail )
     Gia_Man_t * pTemp = Gia_ManTransformMiter( pMiter );
     Aig_Man_t * pMiterCec = Gia_ManToAig( pTemp, 0 );
     int RetValue, iOut, nOuts;
-    clock_t clkTotal = clock();
+    abctime clkTotal = Abc_Clock();
     if ( piOutFail )
         *piOutFail = -1;
     Gia_ManStop( pTemp );
@@ -83,12 +83,12 @@ int Cec_ManVerifyOld( Gia_Man_t * pMiter, int fVerbose, int * piOutFail )
     if ( RetValue == 1 )
     {
         Abc_Print( 1, "Networks are equivalent.   " );
-Abc_PrintTime( 1, "Time", clock() - clkTotal );
+Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
     }
     else if ( RetValue == 0 )
     {
         Abc_Print( 1, "Networks are NOT EQUIVALENT.   " );
-Abc_PrintTime( 1, "Time", clock() - clkTotal );
+Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
         if ( pMiterCec->pData == NULL )
             Abc_Print( 1, "Counter-example is not available.\n" );
         else
@@ -113,7 +113,7 @@ Abc_PrintTime( 1, "Time", clock() - clkTotal );
     else
     {
         Abc_Print( 1, "Networks are UNDECIDED.   " );
-Abc_PrintTime( 1, "Time", clock() - clkTotal );
+Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
     }
     fflush( stdout );
     Aig_ManStop( pMiterCec );
@@ -136,7 +136,7 @@ int Cec_ManHandleSpecialCases( Gia_Man_t * p, Cec_ParCec_t * pPars )
     Gia_Obj_t * pObj1, * pObj2;
     Gia_Obj_t * pDri1, * pDri2;
     int i;
-    clock_t clk = clock();
+    abctime clk = Abc_Clock();
     Gia_ManSetPhase( p );
     Gia_ManForEachPo( p, pObj1, i )
     {
@@ -146,7 +146,7 @@ int Cec_ManHandleSpecialCases( Gia_Man_t * p, Cec_ParCec_t * pPars )
         if ( Gia_ObjPhase(pObj1) != Gia_ObjPhase(pObj2) )
         {
             Abc_Print( 1, "Networks are NOT EQUIVALENT. Outputs %d trivially differ (different phase).  ", i/2 );
-            Abc_PrintTime( 1, "Time", clock() - clk );
+            Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
             pPars->iOutFail = i/2;
             Cec_ManTransformPattern( p, i/2, NULL );
             return 0;
@@ -158,7 +158,7 @@ int Cec_ManHandleSpecialCases( Gia_Man_t * p, Cec_ParCec_t * pPars )
         if ( Gia_ObjIsPi(p, pDri1) && Gia_ObjIsPi(p, pDri2) && pDri1 != pDri2 )
         {
             Abc_Print( 1, "Networks are NOT EQUIVALENT. Outputs %d trivially differ (different PIs).  ", i/2 );
-            Abc_PrintTime( 1, "Time", clock() - clk );
+            Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
             pPars->iOutFail = i/2;
             Cec_ManTransformPattern( p, i/2, NULL );
             // if their compl attributes are the same - one should be complemented
@@ -171,7 +171,7 @@ int Cec_ManHandleSpecialCases( Gia_Man_t * p, Cec_ParCec_t * pPars )
              (Gia_ObjIsPi(p, pDri2) && Gia_ObjIsConst0(pDri1)) )
         {
             Abc_Print( 1, "Networks are NOT EQUIVALENT. Outputs %d trivially differ (PI vs. constant).  ", i/2 );
-            Abc_PrintTime( 1, "Time", clock() - clk );
+            Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
             pPars->iOutFail = i/2;
             Cec_ManTransformPattern( p, i/2, NULL );
             // the compl attributes are the same - the PI should be complemented
@@ -186,7 +186,7 @@ int Cec_ManHandleSpecialCases( Gia_Man_t * p, Cec_ParCec_t * pPars )
     if ( Gia_ManAndNum(p) == 0 )
     {
         Abc_Print( 1, "Networks are equivalent.  " );
-        Abc_PrintTime( 1, "Time", clock() - clk );
+        Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
         return 1;
     }
     return -1;
@@ -209,8 +209,8 @@ int Cec_ManVerify( Gia_Man_t * pInit, Cec_ParCec_t * pPars )
     Cec_ParFra_t ParsFra, * pParsFra = &ParsFra;
     Gia_Man_t * p, * pNew;
     int RetValue;
-    clock_t clk = clock();
-    clock_t clkTotal = clock();
+    abctime clk = Abc_Clock();
+    abctime clkTotal = Abc_Clock();
     // consider special cases:
     // 1) (SAT) a pair of POs have different value under all-0 pattern
     // 2) (SAT) a pair of POs has different PI/Const drivers
@@ -245,7 +245,7 @@ int Cec_ManVerify( Gia_Man_t * pInit, Cec_ParCec_t * pPars )
             if ( p->pCexComb && !Gia_ManVerifyCex( p, p->pCexComb, 1 ) )
                 Abc_Print( 1, "Counter-example simulation has failed.\n" );
             Abc_Print( 1, "Networks are NOT EQUIVALENT.  " );
-            Abc_PrintTime( 1, "Time", clock() - clk );
+            Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
             return 0;
         }
         p = Gia_ManDup( pInit );
@@ -257,7 +257,7 @@ int Cec_ManVerify( Gia_Man_t * pInit, Cec_ParCec_t * pPars )
     if ( pPars->fVerbose )
     {
         Abc_Print( 1, "Networks are UNDECIDED after the new CEC engine.  " );
-        Abc_PrintTime( 1, "Time", clock() - clk );
+        Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
     }
     if ( fDumpUndecided )
     {
@@ -266,7 +266,7 @@ int Cec_ManVerify( Gia_Man_t * pInit, Cec_ParCec_t * pPars )
         Gia_AigerWrite( pNew, "gia_cec_undecided.aig", 0, 0 );
         Abc_Print( 1, "The result is written into file \"%s\".\n", "gia_cec_undecided.aig" );
     }
-    if ( pPars->TimeLimit && (clock() - clkTotal)/CLOCKS_PER_SEC >= pPars->TimeLimit )
+    if ( pPars->TimeLimit && (Abc_Clock() - clkTotal)/CLOCKS_PER_SEC >= pPars->TimeLimit )
     {
         Gia_ManStop( pNew );
         return -1;
diff --git a/src/proof/cec/cecChoice.c b/src/proof/cec/cecChoice.c
index c07b9112..01b5adec 100644
--- a/src/proof/cec/cecChoice.c
+++ b/src/proof/cec/cecChoice.c
@@ -209,8 +209,8 @@ int Cec_ManChoiceComputation_int( Gia_Man_t * pAig, Cec_ParChc_t * pPars )
     Cec_ManSim_t * pSim;
     Gia_Man_t * pSrm;
     int r, RetValue;
-    clock_t clkSat = 0, clkSim = 0, clkSrm = 0, clkTotal = clock();
-    clock_t clk2, clk = clock();
+    abctime clkSat = 0, clkSim = 0, clkSrm = 0, clkTotal = Abc_Clock();
+    abctime clk2, clk = Abc_Clock();
     ABC_FREE( pAig->pReprs );
     ABC_FREE( pAig->pNexts );
     Gia_ManRandom( 1 );
@@ -233,51 +233,51 @@ int Cec_ManChoiceComputation_int( Gia_Man_t * pAig, Cec_ParChc_t * pPars )
     {
         Abc_Print( 1, "Obj = %7d. And = %7d. Conf = %5d. Ring = %d. CSat = %d.\n",
             Gia_ManObjNum(pAig), Gia_ManAndNum(pAig), pPars->nBTLimit, pPars->fUseRings, pPars->fUseCSat );
-        Cec_ManRefinedClassPrintStats( pAig, NULL, 0, clock() - clk );
+        Cec_ManRefinedClassPrintStats( pAig, NULL, 0, Abc_Clock() - clk );
     }
     // perform refinement of equivalence classes
     for ( r = 0; r < nItersMax; r++ )
     { 
-        clk = clock();
+        clk = Abc_Clock();
         // perform speculative reduction
-        clk2 = clock();
+        clk2 = Abc_Clock();
         pSrm = Cec_ManCombSpecReduce( pAig, &vOutputs, pPars->fUseRings );
         assert( Gia_ManRegNum(pSrm) == 0 && Gia_ManCiNum(pSrm) == Gia_ManCiNum(pAig) );
-        clkSrm += clock() - clk2;
+        clkSrm += Abc_Clock() - clk2;
         if ( Gia_ManCoNum(pSrm) == 0 )
         {
             if ( pPars->fVerbose )
-                Cec_ManRefinedClassPrintStats( pAig, NULL, r+1, clock() - clk );
+                Cec_ManRefinedClassPrintStats( pAig, NULL, r+1, Abc_Clock() - clk );
             Vec_IntFree( vOutputs );
             Gia_ManStop( pSrm );            
             break;
         }
 //Gia_DumpAiger( pSrm, "choicesrm", r, 2 );
         // found counter-examples to speculation
-        clk2 = clock();
+        clk2 = Abc_Clock();
         if ( pPars->fUseCSat )
             vCexStore = Cbs_ManSolveMiterNc( pSrm, pPars->nBTLimit, &vStatus, 0 );
         else
             vCexStore = Cec_ManSatSolveMiter( pSrm, pParsSat, &vStatus );
         Gia_ManStop( pSrm );
-        clkSat += clock() - clk2;
+        clkSat += Abc_Clock() - clk2;
         if ( Vec_IntSize(vCexStore) == 0 )
         {
             if ( pPars->fVerbose )
-                Cec_ManRefinedClassPrintStats( pAig, vStatus, r+1, clock() - clk );
+                Cec_ManRefinedClassPrintStats( pAig, vStatus, r+1, Abc_Clock() - clk );
             Vec_IntFree( vCexStore );
             Vec_StrFree( vStatus );
             Vec_IntFree( vOutputs );
             break;
         }
         // refine classes with these counter-examples
-        clk2 = clock();
+        clk2 = Abc_Clock();
         RetValue = Cec_ManResimulateCounterExamplesComb( pSim, vCexStore );
         Vec_IntFree( vCexStore );
-        clkSim += clock() - clk2;
+        clkSim += Abc_Clock() - clk2;
         Gia_ManCheckRefinements( pAig, vStatus, vOutputs, pSim, pPars->fUseRings );
         if ( pPars->fVerbose )
-            Cec_ManRefinedClassPrintStats( pAig, vStatus, r+1, clock() - clk );
+            Cec_ManRefinedClassPrintStats( pAig, vStatus, r+1, Abc_Clock() - clk );
         Vec_StrFree( vStatus );
         Vec_IntFree( vOutputs );
 //Gia_ManEquivPrintClasses( pAig, 1, 0 );
@@ -286,7 +286,7 @@ int Cec_ManChoiceComputation_int( Gia_Man_t * pAig, Cec_ParChc_t * pPars )
     if ( r == nItersMax )
         Abc_Print( 1, "The refinement was not finished. The result may be incorrect.\n" );
     Cec_ManSimStop( pSim );
-    clkTotal = clock() - clkTotal;
+    clkTotal = Abc_Clock() - clkTotal;
     // report the results
     if ( pPars->fVerbose )
     {
diff --git a/src/proof/cec/cecCore.c b/src/proof/cec/cecCore.c
index 40d5fba6..051a5126 100644
--- a/src/proof/cec/cecCore.c
+++ b/src/proof/cec/cecCore.c
@@ -258,14 +258,14 @@ int Cec_ManSimulationOne( Gia_Man_t * pAig, Cec_ParSim_t * pPars )
 {
     Cec_ManSim_t * pSim;
     int RetValue = 0;
-    clock_t clkTotal = clock();
+    abctime clkTotal = Abc_Clock();
     pSim = Cec_ManSimStart( pAig, pPars );
     if ( (pAig->pReprs == NULL && (RetValue = Cec_ManSimClassesPrepare( pSim, -1 ))) ||
          (RetValue == 0 &&        (RetValue = Cec_ManSimClassesRefine( pSim ))) )
         Abc_Print( 1, "The number of failed outputs of the miter = %6d. (Words = %4d. Frames = %4d.)\n", 
             pSim->nOuts, pPars->nWords, pPars->nFrames );
     if ( pPars->fVerbose )
-        Abc_PrintTime( 1, "Time", clock() - clkTotal );
+        Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
     Cec_ManSimStop( pSim );
     return RetValue;
 }
@@ -344,7 +344,7 @@ Gia_Man_t * Cec_ManSatSweeping( Gia_Man_t * pAig, Cec_ParFra_t * pPars )
     Cec_ManSim_t * pSim;
     Cec_ManPat_t * pPat;
     int i, fTimeOut = 0, nMatches = 0;
-    clock_t clk, clk2, clkTotal = clock();
+    abctime clk, clk2, clkTotal = Abc_Clock();
 
     // duplicate AIG and transfer equivalence classes
     Gia_ManRandom( 1 );
@@ -374,7 +374,7 @@ Gia_Man_t * Cec_ManSatSweeping( Gia_Man_t * pAig, Cec_ParFra_t * pPars )
     pPat->fVerbose = pPars->fVeryVerbose;
 
     // start equivalence classes
-clk = clock();
+clk = Abc_Clock();
     if ( p->pAig->pReprs == NULL )
     {
         if ( Cec_ManSimClassesPrepare(pSim, -1) || Cec_ManSimClassesRefine(pSim) )
@@ -384,11 +384,11 @@ clk = clock();
             goto finalize;
         }
     }
-p->timeSim += clock() - clk;
+p->timeSim += Abc_Clock() - clk;
     // perform solving
     for ( i = 1; i <= pPars->nItersMax; i++ )
     {
-        clk2 = clock();
+        clk2 = Abc_Clock();
         nMatches = 0;
         if ( pPars->fDualOut )
         {
@@ -425,9 +425,9 @@ p->timeSim += clock() - clk;
             }
             break;
         }
-clk = clock();
+clk = Abc_Clock();
         Cec_ManSatSolve( pPat, pSrm, pParsSat ); 
-p->timeSat += clock() - clk;
+p->timeSat += Abc_Clock() - clk;
         if ( Cec_ManFraClassesUpdate( p, pSim, pPat, pSrm ) )
         {
             Gia_ManStop( pSrm );
@@ -449,7 +449,7 @@ p->timeSat += clock() - clk;
         {
             Abc_Print( 1, "%3d : P =%7d. D =%7d. F =%6d. M = %7d. And =%8d. ", 
                 i, p->nAllProved, p->nAllDisproved, p->nAllFailed, nMatches, Gia_ManAndNum(p->pAig) );
-            Abc_PrintTime( 1, "Time", clock() - clk2 );
+            Abc_PrintTime( 1, "Time", Abc_Clock() - clk2 );
         }
         if ( Gia_ManAndNum(p->pAig) == 0 )
         {
@@ -458,7 +458,7 @@ p->timeSat += clock() - clk;
             break;
         }
         // check resource limits
-        if ( p->pPars->TimeLimit && (clock() - clkTotal)/CLOCKS_PER_SEC >= p->pPars->TimeLimit )
+        if ( p->pPars->TimeLimit && (Abc_Clock() - clkTotal)/CLOCKS_PER_SEC >= p->pPars->TimeLimit )
         {
             fTimeOut = 1;
             break;
@@ -509,10 +509,10 @@ finalize:
             100.0*(Gia_ManAndNum(pAig)-Gia_ManAndNum(p->pAig))/(Gia_ManAndNum(pAig)?Gia_ManAndNum(pAig):1), 
             Gia_ManRegNum(pAig), Gia_ManRegNum(p->pAig), 
             100.0*(Gia_ManRegNum(pAig)-Gia_ManRegNum(p->pAig))/(Gia_ManRegNum(pAig)?Gia_ManRegNum(pAig):1) );
-        Abc_PrintTimeP( 1, "Sim ", p->timeSim, clock() - (int)clkTotal );
-        Abc_PrintTimeP( 1, "Sat ", p->timeSat-pPat->timeTotalSave, clock() - (int)clkTotal );
-        Abc_PrintTimeP( 1, "Pat ", p->timePat+pPat->timeTotalSave, clock() - (int)clkTotal );
-        Abc_PrintTime( 1, "Time", (int)(clock() - clkTotal) );
+        Abc_PrintTimeP( 1, "Sim ", p->timeSim, Abc_Clock() - (int)clkTotal );
+        Abc_PrintTimeP( 1, "Sat ", p->timeSat-pPat->timeTotalSave, Abc_Clock() - (int)clkTotal );
+        Abc_PrintTimeP( 1, "Pat ", p->timePat+pPat->timeTotalSave, Abc_Clock() - (int)clkTotal );
+        Abc_PrintTime( 1, "Time", (int)(Abc_Clock() - clkTotal) );
     }
 
     pTemp = p->pAig; p->pAig = NULL;
@@ -524,7 +524,7 @@ finalize:
     else if ( pSim->pCexes )
         Abc_Print( 1, "Disproved %d outputs of the miter.\n", pSim->nOuts );
     if ( fTimeOut )
-        Abc_Print( 1, "Timed out after %d seconds.\n", (int)((double)clock() - clkTotal)/CLOCKS_PER_SEC );
+        Abc_Print( 1, "Timed out after %d seconds.\n", (int)((double)Abc_Clock() - clkTotal)/CLOCKS_PER_SEC );
 
     pAig->pCexComb = pSim->pCexComb; pSim->pCexComb = NULL;
     Cec_ManSimStop( pSim );
diff --git a/src/proof/cec/cecCorr.c b/src/proof/cec/cecCorr.c
index 4ea79935..fac30004 100644
--- a/src/proof/cec/cecCorr.c
+++ b/src/proof/cec/cecCorr.c
@@ -722,7 +722,7 @@ Gia_Man_t * Gia_ManCorrReduce( Gia_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Cec_ManRefinedClassPrintStats( Gia_Man_t * p, Vec_Str_t * vStatus, int iIter, clock_t Time )
+void Cec_ManRefinedClassPrintStats( Gia_Man_t * p, Vec_Str_t * vStatus, int iIter, abctime Time )
 { 
     int nLits, CounterX = 0, Counter0 = 0, Counter = 0;
     int i, Entry, nProve = 0, nDispr = 0, nFail = 0;
@@ -793,7 +793,7 @@ void Cec_ManLSCorrespondenceBmc( Gia_Man_t * pAig, Cec_ParCor_t * pPars, int nPr
     fChanges = 1;
     while ( fChanges )
     {
-        clock_t clkBmc = clock();
+        abctime clkBmc = Abc_Clock();
         fChanges = 0;
         pSrm = Gia_ManCorrSpecReduceInit( pAig, pPars->nFrames, nPrefs, !pPars->fLatchCorr, &vOutputs, pPars->fUseRings );
         if ( Gia_ManPoNum(pSrm) == 0 )
@@ -815,7 +815,7 @@ void Cec_ManLSCorrespondenceBmc( Gia_Man_t * pAig, Cec_ParCor_t * pPars, int nPr
             fChanges = 1;
         }
         if ( pPars->fVerbose )
-            Cec_ManRefinedClassPrintStats( pAig, vStatus, -1, clock() - clkBmc );
+            Cec_ManRefinedClassPrintStats( pAig, vStatus, -1, Abc_Clock() - clkBmc );
         // recycle
         Vec_IntFree( vCexStore );
         Vec_StrFree( vStatus );
@@ -919,9 +919,9 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
     Cec_ManSim_t * pSim;
     Gia_Man_t * pSrm;
     int r, RetValue;
-    clock_t clkTotal = clock();
-    clock_t clkSat = 0, clkSim = 0, clkSrm = 0;
-    clock_t clk2, clk = clock();
+    abctime clkTotal = Abc_Clock();
+    abctime clkSat = 0, clkSim = 0, clkSrm = 0;
+    abctime clk2, clk = Abc_Clock();
     if ( Gia_ManRegNum(pAig) == 0 )
     {
         Abc_Print( 1, "Cec_ManLatchCorrespondence(): Not a sequential AIG.\n" );
@@ -955,7 +955,7 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
         Abc_Print( 1, "Obj = %7d. And = %7d. Conf = %5d. Fr = %d. Lcorr = %d. Ring = %d. CSat = %d.\n",
             Gia_ManObjNum(pAig), Gia_ManAndNum(pAig), 
             pPars->nBTLimit, pPars->nFrames, pPars->fLatchCorr, pPars->fUseRings, pPars->fUseCSat );
-        Cec_ManRefinedClassPrintStats( pAig, NULL, 0, clock() - clk );
+        Cec_ManRefinedClassPrintStats( pAig, NULL, 0, Abc_Clock() - clk );
     }
     // check the base case
     if ( fRunBmcFirst && (!pPars->fLatchCorr || pPars->nFrames > 1) )
@@ -980,12 +980,12 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
             Abc_Print( 1, "Stopped signal correspondence after %d refiment iterations.\n", r );
             return 1;
         }
-        clk = clock();
+        clk = Abc_Clock();
         // perform speculative reduction
-        clk2 = clock();
+        clk2 = Abc_Clock();
         pSrm = Gia_ManCorrSpecReduce( pAig, pPars->nFrames, !pPars->fLatchCorr, &vOutputs, pPars->fUseRings );
         assert( Gia_ManRegNum(pSrm) == 0 && Gia_ManPiNum(pSrm) == Gia_ManRegNum(pAig)+(pPars->nFrames+!pPars->fLatchCorr)*Gia_ManPiNum(pAig) );
-        clkSrm += clock() - clk2;
+        clkSrm += Abc_Clock() - clk2;
         if ( Gia_ManCoNum(pSrm) == 0 )
         {
             Vec_IntFree( vOutputs );
@@ -994,13 +994,13 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
         }
 //Gia_DumpAiger( pSrm, "corrsrm", r, 2 );
         // found counter-examples to speculation
-        clk2 = clock();
+        clk2 = Abc_Clock();
         if ( pPars->fUseCSat )
             vCexStore = Cbs_ManSolveMiterNc( pSrm, pPars->nBTLimit, &vStatus, 0 );
         else
             vCexStore = Cec_ManSatSolveMiter( pSrm, pParsSat, &vStatus );
         Gia_ManStop( pSrm );
-        clkSat += clock() - clk2;
+        clkSat += Abc_Clock() - clk2;
         if ( Vec_IntSize(vCexStore) == 0 )
         {
             Vec_IntFree( vCexStore );
@@ -1011,13 +1011,13 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
 //        Cec_ManLSCorrAnalyzeDependence( pAig, vOutputs, vStatus );        
 
         // refine classes with these counter-examples
-        clk2 = clock();
+        clk2 = Abc_Clock();
         RetValue = Cec_ManResimulateCounterExamples( pSim, vCexStore, pPars->nFrames + 1 + nAddFrames );
         Vec_IntFree( vCexStore );
-        clkSim += clock() - clk2;
+        clkSim += Abc_Clock() - clk2;
         Gia_ManCheckRefinements( pAig, vStatus, vOutputs, pSim, pPars->fUseRings );
         if ( pPars->fVerbose )
-            Cec_ManRefinedClassPrintStats( pAig, vStatus, r+1, clock() - clk );
+            Cec_ManRefinedClassPrintStats( pAig, vStatus, r+1, Abc_Clock() - clk );
         Vec_StrFree( vStatus );
         Vec_IntFree( vOutputs );
 //Gia_ManEquivPrintClasses( pAig, 1, 0 );
@@ -1033,7 +1033,7 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
         }
     }
     if ( pPars->fVerbose )
-        Cec_ManRefinedClassPrintStats( pAig, NULL, r+1, clock() - clk );
+        Cec_ManRefinedClassPrintStats( pAig, NULL, r+1, Abc_Clock() - clk );
     // check the overflow
     if ( r == nIterMax )
         Abc_Print( 1, "The refinement was not finished. The result may be incorrect.\n" );
@@ -1041,7 +1041,7 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
     // check the base case
     if ( !fRunBmcFirst && (!pPars->fLatchCorr || pPars->nFrames > 1) )
         Cec_ManLSCorrespondenceBmc( pAig, pPars, 0 );
-    clkTotal = clock() - clkTotal;
+    clkTotal = Abc_Clock() - clkTotal;
     // report the results
     if ( pPars->fVerbose )
     {
diff --git a/src/proof/cec/cecInt.h b/src/proof/cec/cecInt.h
index 36ff3483..dd6dc618 100644
--- a/src/proof/cec/cecInt.h
+++ b/src/proof/cec/cecInt.h
@@ -61,13 +61,13 @@ struct Cec_ManPat_t_
     int              nSeries;        // simulation series
     int              fVerbose;       // verbose stats
     // runtime statistics
-    clock_t          timeFind;       // detecting the pattern  
-    clock_t          timeShrink;     // minimizing the pattern
-    clock_t          timeVerify;     // verifying the result of minimisation
-    clock_t          timeSort;       // sorting literals 
-    clock_t          timePack;       // packing into sim info structures 
-    clock_t          timeTotal;      // total runtime  
-    clock_t          timeTotalSave;  // total runtime for saving  
+    abctime          timeFind;       // detecting the pattern  
+    abctime          timeShrink;     // minimizing the pattern
+    abctime          timeVerify;     // verifying the result of minimisation
+    abctime          timeSort;       // sorting literals 
+    abctime          timePack;       // packing into sim info structures 
+    abctime          timeTotal;      // total runtime  
+    abctime          timeTotalSave;  // total runtime for saving  
 };
 
 // SAT solving manager
@@ -154,10 +154,10 @@ struct Cec_ManFra_t_
     int              nAllDisproved;  // total number of disproved nodes
     int              nAllFailed;     // total number of failed nodes
     // runtime stats
-    clock_t          timeSim;        // unsat
-    clock_t          timePat;        // unsat
-    clock_t          timeSat;        // sat
-    clock_t          timeTotal;      // total runtime
+    abctime          timeSim;        // unsat
+    abctime          timePat;        // unsat
+    abctime          timeSat;        // sat
+    abctime          timeTotal;      // total runtime
 };
 
 ////////////////////////////////////////////////////////////////////////
@@ -169,7 +169,7 @@ struct Cec_ManFra_t_
 ////////////////////////////////////////////////////////////////////////
 
 /*=== cecCorr.c ============================================================*/
-extern void                 Cec_ManRefinedClassPrintStats( Gia_Man_t * p, Vec_Str_t * vStatus, int iIter, clock_t Time );
+extern void                 Cec_ManRefinedClassPrintStats( Gia_Man_t * p, Vec_Str_t * vStatus, int iIter, abctime Time );
 /*=== cecClass.c ============================================================*/
 extern int                  Cec_ManSimClassRemoveOne( Cec_ManSim_t * p, int i );
 extern int                  Cec_ManSimClassesPrepare( Cec_ManSim_t * p, int LevelMax );
diff --git a/src/proof/cec/cecPat.c b/src/proof/cec/cecPat.c
index f372f3bb..c175eaa7 100644
--- a/src/proof/cec/cecPat.c
+++ b/src/proof/cec/cecPat.c
@@ -360,20 +360,20 @@ void Cec_ManPatSavePattern( Cec_ManPat_t * pMan, Cec_ManSat_t *  p, Gia_Obj_t *
 {
     Vec_Int_t * vPat;
     int nPatLits;
-    clock_t clk, clkTotal = clock();
+    abctime clk, clkTotal = Abc_Clock();
     assert( Gia_ObjIsCo(pObj) );
     pMan->nPats++;
     pMan->nPatsAll++;
     // compute values in the cone of influence
-clk = clock();
+clk = Abc_Clock();
     Gia_ManIncrementTravId( p->pAig );
     nPatLits = Cec_ManPatComputePattern_rec( p, p->pAig, Gia_ObjFanin0(pObj) );
     assert( (Gia_ObjFanin0(pObj)->fMark1 ^ Gia_ObjFaninC0(pObj)) == 1 );
     pMan->nPatLits += nPatLits;
     pMan->nPatLitsAll += nPatLits;
-pMan->timeFind += clock() - clk;
+pMan->timeFind += Abc_Clock() - clk;
     // compute sensitizing path
-clk = clock();
+clk = Abc_Clock();
     Vec_IntClear( pMan->vPattern1 );
     Gia_ManIncrementTravId( p->pAig );
     Cec_ManPatComputePattern1_rec( p->pAig, Gia_ObjFanin0(pObj), pMan->vPattern1 );
@@ -385,18 +385,18 @@ clk = clock();
     vPat = Vec_IntSize(pMan->vPattern1) < Vec_IntSize(pMan->vPattern2) ? pMan->vPattern1 : pMan->vPattern2;
     pMan->nPatLitsMin += Vec_IntSize(vPat);
     pMan->nPatLitsMinAll += Vec_IntSize(vPat);
-pMan->timeShrink += clock() - clk;
+pMan->timeShrink += Abc_Clock() - clk;
     // verify pattern using ternary simulation
-clk = clock();
+clk = Abc_Clock();
     Cec_ManPatVerifyPattern( p->pAig, pObj, vPat );
-pMan->timeVerify += clock() - clk;
+pMan->timeVerify += Abc_Clock() - clk;
     // sort pattern
-clk = clock();
+clk = Abc_Clock();
     Vec_IntSort( vPat, 0 );
-pMan->timeSort += clock() - clk;
+pMan->timeSort += Abc_Clock() - clk;
     // save pattern
     Cec_ManPatStore( pMan, vPat );
-    pMan->timeTotal += clock() - clkTotal;
+    pMan->timeTotal += Abc_Clock() - clkTotal;
 }
 
 /**Function*************************************************************
@@ -452,7 +452,7 @@ Vec_Ptr_t * Cec_ManPatCollectPatterns( Cec_ManPat_t *  pMan, int nInputs, int nW
     int iStartOld = pMan->iStart;
     int nWords = nWordsInit;
     int nBits = 32 * nWords;
-    clock_t clk = clock();
+    abctime clk = Abc_Clock();
     vInfo = Vec_PtrAllocSimInfo( nInputs, nWords );
     Gia_ManRandomInfo( vInfo, 0, 0, nWords );
     vPres = Vec_PtrAllocSimInfo( nInputs, nWords );
@@ -477,14 +477,14 @@ Vec_Ptr_t * Cec_ManPatCollectPatterns( Cec_ManPat_t *  pMan, int nInputs, int nW
     }
     Vec_PtrFree( vPres );
     pMan->nSeries = Vec_PtrReadWordsSimInfo(vInfo) / nWordsInit;
-    pMan->timePack += clock() - clk;
-    pMan->timeTotal += clock() - clk;
+    pMan->timePack += Abc_Clock() - clk;
+    pMan->timeTotal += Abc_Clock() - clk;
     pMan->iStart = iStartOld;
     if ( pMan->fVerbose )
     {
         Abc_Print( 1, "Total = %5d. Max used = %5d. Full = %5d. Series = %d. ", 
             nPatterns, kMax, nWordsInit*32, pMan->nSeries );
-        ABC_PRT( "Time", clock() - clk );
+        ABC_PRT( "Time", Abc_Clock() - clk );
         Cec_ManPatPrintStats( pMan );
     }
     return vInfo;
diff --git a/src/proof/cec/cecSeq.c b/src/proof/cec/cecSeq.c
index 43bfa99c..f39fb2a4 100644
--- a/src/proof/cec/cecSeq.c
+++ b/src/proof/cec/cecSeq.c
@@ -185,7 +185,7 @@ int Cec_ManSeqResimulateInfo( Gia_Man_t * pAig, Vec_Ptr_t * vSimInfo, Abc_Cex_t
 {
     Cec_ParSim_t ParsSim, * pParsSim = &ParsSim;
     Cec_ManSim_t * pSim;
-    int RetValue;//, clkTotal = clock();
+    int RetValue;//, clkTotal = Abc_Clock();
     assert( (Vec_PtrSize(vSimInfo) - Gia_ManRegNum(pAig)) % Gia_ManPiNum(pAig) == 0 );
     Cec_ManSimSetDefaultParams( pParsSim );
     pParsSim->nFrames = (Vec_PtrSize(vSimInfo) - Gia_ManRegNum(pAig)) / Gia_ManPiNum(pAig);
@@ -216,7 +216,7 @@ int Cec_ManSeqResimulateCounter( Gia_Man_t * pAig, Cec_ParSim_t * pPars, Abc_Cex
 {
     Vec_Ptr_t * vSimInfo;
     int RetValue;
-    clock_t clkTotal = clock();
+    abctime clkTotal = Abc_Clock();
     if ( pCex == NULL )
     {
         Abc_Print( 1, "Cec_ManSeqResimulateCounter(): Counter-example is not available.\n" );
@@ -251,7 +251,7 @@ int Cec_ManSeqResimulateCounter( Gia_Man_t * pAig, Cec_ParSim_t * pPars, Abc_Cex
         Gia_ManEquivPrintClasses( pAig, 0, 0 );
     Vec_PtrFree( vSimInfo );
     if ( pPars->fVerbose )
-        ABC_PRT( "Time", clock() - clkTotal );
+        ABC_PRT( "Time", Abc_Clock() - clkTotal );
 //    if ( RetValue && pPars->fCheckMiter )
 //        Abc_Print( 1, "Cec_ManSeqResimulateCounter(): An output of the miter is asserted!\n" );
     return RetValue;
diff --git a/src/proof/cec/cecSolve.c b/src/proof/cec/cecSolve.c
index d560c37a..c799d17d 100644
--- a/src/proof/cec/cecSolve.c
+++ b/src/proof/cec/cecSolve.c
@@ -472,7 +472,7 @@ int Cec_ManSatCheckNode( Cec_ManSat_t * p, Gia_Obj_t * pObj )
     Gia_Obj_t * pObjR = Gia_Regular(pObj);
     int nBTLimit = p->pPars->nBTLimit;
     int Lit, RetValue, status, nConflicts;
-    clock_t clk, clk2;
+    abctime clk, clk2;
 
     if ( pObj == Gia_ManConst0(p->pAig) )
         return 1;
@@ -493,14 +493,14 @@ int Cec_ManSatCheckNode( Cec_ManSat_t * p, Gia_Obj_t * pObj )
         Cec_ManSatSolverRecycle( p );
 
     // if the nodes do not have SAT variables, allocate them
-clk2 = clock();
+clk2 = Abc_Clock();
     Cec_CnfNodeAddToSolver( p, pObjR );
-//ABC_PRT( "cnf", clock() - clk2 );
+//ABC_PRT( "cnf", Abc_Clock() - clk2 );
 //Abc_Print( 1, "%d \n", p->pSat->size );
 
-clk2 = clock();
+clk2 = Abc_Clock();
 //    Cec_SetActivityFactors( p, pObjR ); 
-//ABC_PRT( "act", clock() - clk2 );
+//ABC_PRT( "act", Abc_Clock() - clk2 );
 
     // propage unit clauses
     if ( p->pSat->qtail != p->pSat->qhead )
@@ -518,17 +518,17 @@ clk2 = clock();
         if ( pObjR->fPhase )  Lit = lit_neg( Lit );
     }
 //Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 );
-clk = clock();
+clk = Abc_Clock();
     nConflicts = p->pSat->stats.conflicts;
 
-clk2 = clock();
+clk2 = Abc_Clock();
     RetValue = sat_solver_solve( p->pSat, &Lit, &Lit + 1, 
         (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
-//ABC_PRT( "sat", clock() - clk2 );
+//ABC_PRT( "sat", Abc_Clock() - clk2 );
 
     if ( RetValue == l_False )
     {
-p->timeSatUnsat += clock() - clk;
+p->timeSatUnsat += Abc_Clock() - clk;
         Lit = lit_neg( Lit );
         RetValue = sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
         assert( RetValue );
@@ -539,7 +539,7 @@ p->timeSatUnsat += clock() - clk;
     }
     else if ( RetValue == l_True )
     {
-p->timeSatSat += clock() - clk;
+p->timeSatSat += Abc_Clock() - clk;
         p->nSatSat++;
         p->nConfSat += p->pSat->stats.conflicts - nConflicts;
 //Abc_Print( 1, "SAT after %d conflicts\n", p->pSat->stats.conflicts - nConflicts );
@@ -547,7 +547,7 @@ p->timeSatSat += clock() - clk;
     }
     else // if ( RetValue == l_Undef )
     {
-p->timeSatUndec += clock() - clk;
+p->timeSatUndec += Abc_Clock() - clk;
         p->nSatUndec++;
         p->nConfUndec += p->pSat->stats.conflicts - nConflicts;
 //Abc_Print( 1, "UNDEC after %d conflicts\n", p->pSat->stats.conflicts - nConflicts );
@@ -572,7 +572,7 @@ int Cec_ManSatCheckNodeTwo( Cec_ManSat_t * p, Gia_Obj_t * pObj1, Gia_Obj_t * pOb
     Gia_Obj_t * pObjR2 = Gia_Regular(pObj2);
     int nBTLimit = p->pPars->nBTLimit;
     int Lits[2], RetValue, status, nConflicts;
-    clock_t clk, clk2;
+    abctime clk, clk2;
 
     if ( pObj1 == Gia_ManConst0(p->pAig) || pObj2 == Gia_ManConst0(p->pAig) || pObj1 == Gia_Not(pObj2) )
         return 1;
@@ -593,16 +593,16 @@ int Cec_ManSatCheckNodeTwo( Cec_ManSat_t * p, Gia_Obj_t * pObj1, Gia_Obj_t * pOb
         Cec_ManSatSolverRecycle( p );
 
     // if the nodes do not have SAT variables, allocate them
-clk2 = clock();
+clk2 = Abc_Clock();
     Cec_CnfNodeAddToSolver( p, pObjR1 );
     Cec_CnfNodeAddToSolver( p, pObjR2 );
-//ABC_PRT( "cnf", clock() - clk2 );
+//ABC_PRT( "cnf", Abc_Clock() - clk2 );
 //Abc_Print( 1, "%d \n", p->pSat->size );
 
-clk2 = clock();
+clk2 = Abc_Clock();
 //    Cec_SetActivityFactors( p, pObjR1 ); 
 //    Cec_SetActivityFactors( p, pObjR2 ); 
-//ABC_PRT( "act", clock() - clk2 );
+//ABC_PRT( "act", Abc_Clock() - clk2 );
 
     // propage unit clauses
     if ( p->pSat->qtail != p->pSat->qhead )
@@ -622,17 +622,17 @@ clk2 = clock();
         if ( pObjR2->fPhase )  Lits[1] = lit_neg( Lits[1] );
     }
 //Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 );
-clk = clock();
+clk = Abc_Clock();
     nConflicts = p->pSat->stats.conflicts;
 
-clk2 = clock();
+clk2 = Abc_Clock();
     RetValue = sat_solver_solve( p->pSat, Lits, Lits + 2, 
         (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
-//ABC_PRT( "sat", clock() - clk2 );
+//ABC_PRT( "sat", Abc_Clock() - clk2 );
 
     if ( RetValue == l_False )
     {
-p->timeSatUnsat += clock() - clk;
+p->timeSatUnsat += Abc_Clock() - clk;
         Lits[0] = lit_neg( Lits[0] );
         Lits[1] = lit_neg( Lits[1] );
         RetValue = sat_solver_addclause( p->pSat, Lits, Lits + 2 );
@@ -644,7 +644,7 @@ p->timeSatUnsat += clock() - clk;
     }
     else if ( RetValue == l_True )
     {
-p->timeSatSat += clock() - clk;
+p->timeSatSat += Abc_Clock() - clk;
         p->nSatSat++;
         p->nConfSat += p->pSat->stats.conflicts - nConflicts;
 //Abc_Print( 1, "SAT after %d conflicts\n", p->pSat->stats.conflicts - nConflicts );
@@ -652,7 +652,7 @@ p->timeSatSat += clock() - clk;
     }
     else // if ( RetValue == l_Undef )
     {
-p->timeSatUndec += clock() - clk;
+p->timeSatUndec += Abc_Clock() - clk;
         p->nSatUndec++;
         p->nConfUndec += p->pSat->stats.conflicts - nConflicts;
 //Abc_Print( 1, "UNDEC after %d conflicts\n", p->pSat->stats.conflicts - nConflicts );
@@ -679,7 +679,7 @@ void Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPar
     Cec_ManSat_t * p;
     Gia_Obj_t * pObj;
     int i, status;
-    clock_t clk = clock(), clk2;
+    abctime clk = Abc_Clock(), clk2;
     // reset the manager
     if ( pPat )
     {
@@ -702,7 +702,7 @@ void Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPar
             continue;
         }
         Bar_ProgressUpdate( pProgress, i, "SAT..." );
-clk2 = clock();
+clk2 = Abc_Clock();
         status = Cec_ManSatCheckNode( p, Gia_ObjChild0(pObj) );
         pObj->fMark0 = (status == 0);
         pObj->fMark1 = (status == 1);
@@ -720,15 +720,15 @@ clk2 = clock();
         // save the pattern
         if ( pPat )
         {
-            clock_t clk3 = clock();
+            abctime clk3 = Abc_Clock();
             Cec_ManPatSavePattern( pPat, p, pObj );
-            pPat->timeTotalSave += clock() - clk3;
+            pPat->timeTotalSave += Abc_Clock() - clk3;
         }
         // quit if one of them is solved
         if ( pPars->fCheckMiter )
             break;
     }
-    p->timeTotal = clock() - clk;
+    p->timeTotal = Abc_Clock() - clk;
     Bar_ProgressStop( pProgress );
     if ( pPars->fVerbose )
         Cec_ManSatPrintStats( p );
@@ -803,7 +803,7 @@ Vec_Str_t * Cec_ManSatSolveSeq( Vec_Ptr_t * vPatts, Gia_Man_t * pAig, Cec_ParSat
     Gia_Obj_t * pObj;
     int iPat = 0, nPatsInit, nPats;
     int i, status;
-    clock_t clk = clock();
+    abctime clk = Abc_Clock();
     nPatsInit = nPats = 32 * Vec_PtrReadWordsSimInfo(vPatts);
     Gia_ManSetPhase( pAig );
     Gia_ManLevelNum( pAig );
@@ -857,7 +857,7 @@ Vec_Str_t * Cec_ManSatSolveSeq( Vec_Ptr_t * vPatts, Gia_Man_t * pAig, Cec_ParSat
 //        if ( iPat == 32 * 15 * 16 - 1 )
 //            break;
     }
-    p->timeTotal = clock() - clk;
+    p->timeTotal = Abc_Clock() - clk;
     Bar_ProgressStop( pProgress );
     if ( pPars->fVerbose )
         Cec_ManSatPrintStats( p );
@@ -962,7 +962,7 @@ Vec_Int_t * Cec_ManSatSolveMiter( Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_St
     Cec_ManSat_t * p;
     Gia_Obj_t * pObj;
     int i, status;
-    clock_t clk = clock();
+    abctime clk = Abc_Clock();
     // prepare AIG
     Gia_ManSetPhase( pAig );
     Gia_ManLevelNum( pAig );
@@ -1009,7 +1009,7 @@ Vec_Int_t * Cec_ManSatSolveMiter( Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_St
 //        Gia_SatVerifyPattern( pAig, pObj, p->vCex, p->vVisits );
         Cec_ManSatAddToStore( vCexStore, p->vCex, i );
     }
-    p->timeTotal = clock() - clk;
+    p->timeTotal = Abc_Clock() - clk;
     Bar_ProgressStop( pProgress );
 //    if ( pPars->fVerbose )
 //        Cec_ManSatPrintStats( p );
diff --git a/src/proof/cec/cecSweep.c b/src/proof/cec/cecSweep.c
index 9ba2e07e..977ff3a8 100644
--- a/src/proof/cec/cecSweep.c
+++ b/src/proof/cec/cecSweep.c
@@ -190,11 +190,11 @@ int Cec_ManFraClassesUpdate( Cec_ManFra_t * p, Cec_ManSim_t * pSim, Cec_ManPat_t
     Vec_Ptr_t * vInfo;
     Gia_Obj_t * pObj, * pObjOld, * pReprOld;
     int i, k, iRepr, iNode;
-    clock_t clk;
-clk = clock();
+    abctime clk;
+clk = Abc_Clock();
     vInfo = Cec_ManPatCollectPatterns( pPat, Gia_ManCiNum(p->pAig), pSim->nWords );
-p->timePat += clock() - clk;
-clk = clock();
+p->timePat += Abc_Clock() - clk;
+clk = Abc_Clock();
     if ( vInfo != NULL )
     {
         Gia_ManCreateValueRefs( p->pAig );
@@ -209,7 +209,7 @@ clk = clock();
         }
         Vec_PtrFree( vInfo );
     }
-p->timeSim += clock() - clk;
+p->timeSim += Abc_Clock() - clk;
     assert( Vec_IntSize(p->vXorNodes) == 2*Gia_ManCoNum(pNew) );
     // mark the transitive fanout of failed nodes
     if ( p->pPars->nDepthMax != 1 )
diff --git a/src/proof/cec/cecSynth.c b/src/proof/cec/cecSynth.c
index 6ab88cbe..c00723bc 100644
--- a/src/proof/cec/cecSynth.c
+++ b/src/proof/cec/cecSynth.c
@@ -298,7 +298,7 @@ int Cec_SequentialSynthesisPart( Gia_Man_t * p, Cec_ParSeq_t * pPars )
     int * pMapBack, * pReprs;
     int i, nCountPis, nCountRegs;
     int nClasses;
-    clock_t clk = clock();
+    abctime clk = Abc_Clock();
 
     // save parameters
     if ( fPrintParts )
@@ -367,7 +367,7 @@ int Cec_SequentialSynthesisPart( Gia_Man_t * p, Cec_ParSeq_t * pPars )
     ABC_FREE( pReprs );
     if ( pPars->fVerbose )
     {
-        Abc_PrintTime( 1, "Total time", clock() - clk );
+        Abc_PrintTime( 1, "Total time", Abc_Clock() - clk );
     }
     return 1;
 }