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

7 files changed, 76 insertions, 76 deletions

diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h
index b5f07151..6e1fd62a 100644
--- a/src/sat/bmc/bmc.h
+++ b/src/sat/bmc/bmc.h
@@ -64,7 +64,7 @@ struct Saig_ParBmc_t_
     int         iFrame;         // explored up to this frame
     int         nFailOuts;      // the number of failed outputs
     int         nDropOuts;      // the number of dropped outputs
-    clock_t     timeLastSolved; // the time when the last output was solved
+    abctime     timeLastSolved; // the time when the last output was solved
     int(*pFuncOnFail)(int,Abc_Cex_t*); // called for a failed output in MO mode
 };
 
diff --git a/src/sat/bmc/bmcBmc.c b/src/sat/bmc/bmcBmc.c
index 7a7c8940..bcad9013 100644
--- a/src/sat/bmc/bmcBmc.c
+++ b/src/sat/bmc/bmcBmc.c
@@ -191,10 +191,10 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim
     Aig_Man_t * pFrames, * pAigTemp;
     Aig_Obj_t * pObj;
     int status, Lit, i, RetValue = -1;
-    clock_t clk;
+    abctime clk;
 
     // derive the timeframes
-    clk = clock();
+    clk = Abc_Clock();
     if ( nCofFanLit )
     {
         pFrames = Gia_ManCofactorAig( pAig, nFrames, nCofFanLit );
@@ -218,13 +218,13 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim
         printf( "Time-frames (%d):  PI/PO = %d/%d.  Node = %6d. Lev = %5d.  ", 
             nFrames, Aig_ManCiNum(pFrames), Aig_ManCoNum(pFrames), 
             Aig_ManNodeNum(pFrames), Aig_ManLevelNum(pFrames) );
-        ABC_PRT( "Time", clock() - clk );
+        ABC_PRT( "Time", Abc_Clock() - clk );
         fflush( stdout );
     }
     // rewrite the timeframes
     if ( fRewrite )
     {
-        clk = clock();
+        clk = Abc_Clock();
 //        pFrames = Dar_ManBalance( pAigTemp = pFrames, 0 );
         pFrames = Dar_ManRwsat( pAigTemp = pFrames, 1, 0 );
         Aig_ManStop( pAigTemp );
@@ -232,12 +232,12 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim
         {
             printf( "Time-frames after rewriting:  Node = %6d. Lev = %5d.  ", 
                 Aig_ManNodeNum(pFrames), Aig_ManLevelNum(pFrames) );
-            ABC_PRT( "Time", clock() - clk );
+            ABC_PRT( "Time", Abc_Clock() - clk );
             fflush( stdout );
         }
     }
     // create the SAT solver
-    clk = clock();
+    clk = Abc_Clock();
     pCnf = Cnf_Derive( pFrames, Aig_ManCoNum(pFrames) );  
 //if ( s_fInterrupt )
 //return -1;
@@ -251,7 +251,7 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim
     if ( fVerbose )
     {
         printf( "CNF: Variables = %6d. Clauses = %7d. Literals = %8d. ", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals );
-        ABC_PRT( "Time", clock() - clk );
+        ABC_PRT( "Time", Abc_Clock() - clk );
         fflush( stdout );
     }
     status = sat_solver_simplify(pSat);
@@ -265,7 +265,7 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim
     }
     else
     {
-        clock_t clkPart = clock();
+        abctime clkPart = Abc_Clock();
         Aig_ManForEachCo( pFrames, pObj, i )
         {
 //if ( s_fInterrupt )
@@ -276,15 +276,15 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim
                 printf( "Solving output %2d of frame %3d ... \r", 
                     i % Saig_ManPoNum(pAig), i / Saig_ManPoNum(pAig) );
             }
-            clk = clock();
+            clk = Abc_Clock();
             status = sat_solver_solve( pSat, &Lit, &Lit + 1, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
             if ( fVerbose && (i % Saig_ManPoNum(pAig) == Saig_ManPoNum(pAig) - 1) )
             {
                 printf( "Solved %2d outputs of frame %3d.  ", 
                     Saig_ManPoNum(pAig), i / Saig_ManPoNum(pAig) );
                 printf( "Conf =%8.0f. Imp =%11.0f. ", (double)pSat->stats.conflicts, (double)pSat->stats.propagations );
-                ABC_PRT( "T", clock() - clkPart );
-                clkPart = clock();
+                ABC_PRT( "T", Abc_Clock() - clkPart );
+                clkPart = Abc_Clock();
                 fflush( stdout );
             }
             if ( status == l_False )
diff --git a/src/sat/bmc/bmcBmc2.c b/src/sat/bmc/bmcBmc2.c
index 658010c0..47bfc008 100644
--- a/src/sat/bmc/bmcBmc2.c
+++ b/src/sat/bmc/bmcBmc2.c
@@ -202,7 +202,7 @@ Vec_Ptr_t * Abs_ManTernarySimulate( Aig_Man_t * p, int nFramesMax, int fVerbose
     Vec_Ptr_t * vSimInfo;
     Aig_Obj_t * pObj;
     int i, f, nFramesLimit, nFrameWords;
-    clock_t clk = clock();
+    abctime clk = Abc_Clock();
     assert( Aig_ManRegNum(p) > 0 );
     // the maximum number of frames will be determined to use at most 200Mb of RAM
     nFramesLimit = 1 + (200000000 * 4)/Aig_ManObjNum(p);
@@ -231,7 +231,7 @@ Vec_Ptr_t * Abs_ManTernarySimulate( Aig_Man_t * p, int nFramesMax, int fVerbose
                 {
                     printf( "Ternary sim found non-zero output in frame %d.  Used %5.2f MB.  ", 
                         f, 0.25 * (f+1) * Aig_ManObjNum(p) / (1<<20) );
-                    ABC_PRT( "Time", clock() - clk );
+                    ABC_PRT( "Time", Abc_Clock() - clk );
                 }
                 return vSimInfo;
             }
@@ -240,7 +240,7 @@ Vec_Ptr_t * Abs_ManTernarySimulate( Aig_Man_t * p, int nFramesMax, int fVerbose
     {
         printf( "Ternary sim proved all outputs in the first %d frames.  Used %5.2f MB.  ", 
             nFramesLimit, 0.25 * nFramesLimit * Aig_ManObjNum(p) / (1<<20) );
-        ABC_PRT( "Time", clock() - clk );
+        ABC_PRT( "Time", Abc_Clock() - clk );
     }
     return vSimInfo;
 }
@@ -765,8 +765,8 @@ int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax
     Cnf_Dat_t * pCnf;
     int nOutsSolved = 0;
     int Iter, RetValue = -1;
-    clock_t nTimeToStop = nTimeOut ? nTimeOut * CLOCKS_PER_SEC + clock(): 0;
-    clock_t clk = clock(), clk2, clkTotal = clock();
+    abctime nTimeToStop = nTimeOut ? nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0;
+    abctime clk = Abc_Clock(), clk2, clkTotal = Abc_Clock();
     int Status = -1;
 /*
     Vec_Ptr_t * vSimInfo;
@@ -788,7 +788,7 @@ int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax
         sat_solver_set_runtime_limit( p->pSat, nTimeToStop );
     for ( Iter = 0; ; Iter++ )
     {
-        clk2 = clock();
+        clk2 = Abc_Clock();
         // add new logic interval to frames
         Saig_BmcInterval( p );
 //        Saig_BmcAddTargetsAsPos( p );
@@ -812,14 +812,14 @@ int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax
             printf( "%4d : F =%5d. O =%4d.  And =%8d. Var =%8d. Conf =%7d. ", 
                 Iter, p->iFrameLast, p->iOutputLast, Aig_ManNodeNum(p->pFrm), p->nSatVars, (int)p->pSat->stats.conflicts );   
             printf( "%4.0f MB",     4.0*(p->iFrameLast+1)*p->nObjs/(1<<20) );
-            printf( "%9.2f sec", (float)(clock() - clkTotal)/(float)(CLOCKS_PER_SEC) );
+            printf( "%9.2f sec", (float)(Abc_Clock() - clkTotal)/(float)(CLOCKS_PER_SEC) );
             printf( "\n" );
             fflush( stdout );
         }
         if ( RetValue != l_False )
             break;
         // check the timeout
-        if ( nTimeOut && clock() > nTimeToStop )
+        if ( nTimeOut && Abc_Clock() > nTimeToStop )
         {
             if ( !fSilent )
                 printf( "Reached timeout (%d seconds).\n",  nTimeOut );
@@ -855,11 +855,11 @@ int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax
     {
         if ( fVerbOverwrite )
         {
-            ABC_PRTr( "Time", clock() - clk );
+            ABC_PRTr( "Time", Abc_Clock() - clk );
         }
         else
         {
-            ABC_PRT( "Time", clock() - clk );
+            ABC_PRT( "Time", Abc_Clock() - clk );
         }
         if ( RetValue != l_True )
         {
@@ -867,7 +867,7 @@ int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax
                 printf( "Reached limit on the number of timeframes (%d).\n", p->nFramesMax );
             else if ( p->nConfMaxAll && p->pSat->stats.conflicts > p->nConfMaxAll )
                 printf( "Reached global conflict limit (%d).\n", p->nConfMaxAll );
-            else if ( nTimeOut && clock() > nTimeToStop )
+            else if ( nTimeOut && Abc_Clock() > nTimeToStop )
                 printf( "Reached timeout (%d seconds).\n", nTimeOut );
             else
                 printf( "Reached local conflict limit (%d).\n", p->nConfMaxOne );
diff --git a/src/sat/bmc/bmcBmc3.c b/src/sat/bmc/bmcBmc3.c
index 87edbb5f..9d399a20 100644
--- a/src/sat/bmc/bmcBmc3.c
+++ b/src/sat/bmc/bmcBmc3.c
@@ -44,7 +44,7 @@ struct Gia_ManBmc_t_
     Vec_Int_t *       vId2Num;     // number of each node 
     Vec_Ptr_t *       vTerInfo;    // ternary information
     Vec_Ptr_t *       vId2Var;     // SAT vars for each object
-    clock_t *         pTime4Outs;  // timeout per output
+    abctime *         pTime4Outs;  // timeout per output
     // hash table
     Vec_Int_t *       vData;       // storage for cuts
     Hsh_IntMan_t *    vHash;       // hash table
@@ -742,7 +742,7 @@ Gia_ManBmc_t * Saig_Bmc3ManStart( Aig_Man_t * pAig, int nTimeOutOne )
     // time spent on each outputs
     if ( nTimeOutOne )
     {
-        p->pTime4Outs = ABC_ALLOC( clock_t, Saig_ManPoNum(pAig) );
+        p->pTime4Outs = ABC_ALLOC( abctime, Saig_ManPoNum(pAig) );
         for ( i = 0; i < Saig_ManPoNum(pAig); i++ )
             p->pTime4Outs[i] = nTimeOutOne * CLOCKS_PER_SEC / 1000 + 1;
     }
@@ -1243,10 +1243,10 @@ void Saig_ParBmcSetDefaultParams( Saig_ParBmc_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-clock_t Saig_ManBmcTimeToStop( Saig_ParBmc_t * pPars, clock_t nTimeToStopNG )
+abctime Saig_ManBmcTimeToStop( Saig_ParBmc_t * pPars, abctime nTimeToStopNG )
 {
-    clock_t nTimeToStopGap = pPars->nTimeOutGap ? pPars->nTimeOutGap * CLOCKS_PER_SEC + clock(): 0;
-    clock_t nTimeToStop = 0;
+    abctime nTimeToStopGap = pPars->nTimeOutGap ? pPars->nTimeOutGap * CLOCKS_PER_SEC + Abc_Clock(): 0;
+    abctime nTimeToStop = 0;
     if ( nTimeToStopNG && nTimeToStopGap )
         nTimeToStop = Abc_MinInt( nTimeToStopNG, nTimeToStopGap );
     else if ( nTimeToStopNG )
@@ -1302,14 +1302,14 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
     int RetValue = -1, fFirst = 1, nJumpFrame = 0, fUnfinished = 0;
     int nOutDigits = Abc_Base10Log( Saig_ManPoNum(pAig) );
     int i, f, k, Lit, status;
-    clock_t clk, clk2, clkOther = 0, clkTotal = clock();
-    clock_t nTimeUnsat = 0, nTimeSat = 0, nTimeUndec = 0, clkOne = 0;
-    clock_t nTimeToStopNG, nTimeToStop;
+    abctime clk, clk2, clkOther = 0, clkTotal = Abc_Clock();
+    abctime nTimeUnsat = 0, nTimeSat = 0, nTimeUndec = 0, clkOne = 0;
+    abctime nTimeToStopNG, nTimeToStop;
     if ( pPars->nTimeOutOne )
         pPars->nTimeOut = pPars->nTimeOutOne * Saig_ManPoNum(pAig) / 1000 + 1;
     if ( pPars->nTimeOutOne && !pPars->fSolveAll )
         pPars->nTimeOutOne = 0;
-    nTimeToStopNG = pPars->nTimeOut ? pPars->nTimeOut * CLOCKS_PER_SEC + clock(): 0;
+    nTimeToStopNG = pPars->nTimeOut ? pPars->nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0;
     nTimeToStop   = Saig_ManBmcTimeToStop( pPars, nTimeToStopNG );
     // create BMC manager
     p = Saig_Bmc3ManStart( pAig, pPars->nTimeOutOne );
@@ -1332,7 +1332,7 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
         sat_solver_set_runtime_limit( p->pSat, nTimeToStop );
     // perform frames
     Aig_ManRandom( 1 );
-    pPars->timeLastSolved = clock();
+    pPars->timeLastSolved = Abc_Clock();
     for ( f = 0; f < pPars->nFramesMax; f++ )
     {
         // stop BMC after exploring all reachable states
@@ -1379,18 +1379,18 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
         if ( (pPars->nStart && f < pPars->nStart) || (nJumpFrame && f < nJumpFrame) )
             continue;
         // solve SAT
-        clk = clock(); 
+        clk = Abc_Clock(); 
         Saig_ManForEachPo( pAig, pObj, i )
         {
             if ( i >= Saig_ManPoNum(pAig) )
                 break;
             // check for timeout
-            if ( pPars->nTimeOutGap && pPars->timeLastSolved && clock() > pPars->timeLastSolved + pPars->nTimeOutGap * CLOCKS_PER_SEC )
+            if ( pPars->nTimeOutGap && pPars->timeLastSolved && Abc_Clock() > pPars->timeLastSolved + pPars->nTimeOutGap * CLOCKS_PER_SEC )
             {
                 printf( "Reached gap timeout (%d seconds).\n",  pPars->nTimeOutGap );
                 goto finish;
             }
-            if ( nTimeToStop && clock() > nTimeToStop )
+            if ( nTimeToStop && Abc_Clock() > nTimeToStop )
             {
                 printf( "Reached timeout (%d seconds).\n",  pPars->nTimeOut );
                 goto finish;
@@ -1402,9 +1402,9 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
             if ( p->pTime4Outs && p->pTime4Outs[i] == 0 )
                 continue;
             // add constraints for this output
-clk2 = clock();
+clk2 = Abc_Clock();
             Lit = Saig_ManBmcCreateCnf( p, pObj, f );
-clkOther += clock() - clk2;
+clkOther += Abc_Clock() - clk2;
             if ( Lit == 0 )
                 continue;
             if ( Lit == 1 )
@@ -1431,7 +1431,7 @@ clkOther += clock() - clk2;
                     goto finish;
                 }
                 // reset the timeout
-                pPars->timeLastSolved = clock();
+                pPars->timeLastSolved = Abc_Clock();
                 nTimeToStop = Saig_ManBmcTimeToStop( pPars, nTimeToStopNG );
                 if ( nTimeToStop )
                     sat_solver_set_runtime_limit( p->pSat, nTimeToStop );
@@ -1440,17 +1440,17 @@ clkOther += clock() - clk2;
             // solve this output
             fUnfinished = 0;
             sat_solver_compress( p->pSat );
-clk2 = clock();
+clk2 = Abc_Clock();
             if ( p->pTime4Outs )
             {
                 assert( p->pTime4Outs[i] > 0 );
-                clkOne = clock();
-                sat_solver_set_runtime_limit( p->pSat, p->pTime4Outs[i] + clock() );
+                clkOne = Abc_Clock();
+                sat_solver_set_runtime_limit( p->pSat, p->pTime4Outs[i] + Abc_Clock() );
             }
             status = sat_solver_solve( p->pSat, &Lit, &Lit + 1, (ABC_INT64_T)pPars->nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
             if ( p->pTime4Outs )
             {
-                clock_t timeSince = clock() - clkOne;
+                abctime timeSince = Abc_Clock() - clkOne;
                 assert( p->pTime4Outs[i] > 0 );
                 p->pTime4Outs[i] = (p->pTime4Outs[i] > timeSince) ? p->pTime4Outs[i] - timeSince : 0;
                 if ( p->pTime4Outs[i] == 0 && status != l_True )
@@ -1458,7 +1458,7 @@ clk2 = clock();
             }
             if ( status == l_False )
             {
-nTimeUnsat += clock() - clk2;
+nTimeUnsat += Abc_Clock() - clk2;
                 if ( 1 )
                 {
                     // add final unit clause
@@ -1479,7 +1479,7 @@ nTimeUnsat += clock() - clk2;
             }
             else if ( status == l_True )
             {
-nTimeSat += clock() - clk2;
+nTimeSat += Abc_Clock() - clk2;
                 RetValue = 0;
                 fFirst = 0;
                 if ( !pPars->fSolveAll )
@@ -1492,10 +1492,10 @@ nTimeSat += clock() - clk2;
                         printf( "Conf =%7.0f. ", (double)p->pSat->stats.conflicts );
 //                        printf( "Imp =%10.0f. ", (double)p->pSat->stats.propagations );
                         printf( "Uni =%7.0f. ",(double)sat_solver_count_assigned(p->pSat) );
-//                        ABC_PRT( "Time", clock() - clk );
+//                        ABC_PRT( "Time", Abc_Clock() - clk );
                         printf( "%4.0f MB",      4.25*(f+1)*p->nObjNums /(1<<20) );
                         printf( "%4.0f MB",      1.0*sat_solver_memory(p->pSat)/(1<<20) );
-                        printf( "%9.2f sec  ",   (float)(clock() - clkTotal)/(float)(CLOCKS_PER_SEC) );
+                        printf( "%9.2f sec  ",   (float)(Abc_Clock() - clkTotal)/(float)(CLOCKS_PER_SEC) );
 //                        printf( "\n" );
 //                        ABC_PRMn( "Id2Var", (f+1)*p->nObjNums*4 );
 //                        ABC_PRMn( "SAT", 42 * p->pSat->size + 16 * (int)p->pSat->stats.clauses + 4 * (int)p->pSat->stats.clauses_literals );
@@ -1521,14 +1521,14 @@ nTimeSat += clock() - clk2;
                     goto finish;
                 }
                 // reset the timeout
-                pPars->timeLastSolved = clock();
+                pPars->timeLastSolved = Abc_Clock();
                 nTimeToStop = Saig_ManBmcTimeToStop( pPars, nTimeToStopNG );
                 if ( nTimeToStop )
                     sat_solver_set_runtime_limit( p->pSat, nTimeToStop );
             }
             else 
             {
-nTimeUndec += clock() - clk2;
+nTimeUndec += Abc_Clock() - clk2;
                 assert( status == l_Undef );
                 if ( pPars->nFramesJump )
                 {
@@ -1559,12 +1559,12 @@ nTimeUndec += clock() - clk2;
                 printf( "CEX =%5d. ", pPars->nFailOuts );
             if ( pPars->nTimeOutOne )
                 printf( "T/O =%4d. ", pPars->nDropOuts );
-//            ABC_PRT( "Time", clock() - clk );
+//            ABC_PRT( "Time", Abc_Clock() - clk );
 //            printf( "%4.0f MB",     4.0*Vec_IntSize(p->vVisited) /(1<<20) );
             printf( "%4.0f MB",     4.0*(f+1)*p->nObjNums /(1<<20) );
             printf( "%4.0f MB",     1.0*sat_solver_memory(p->pSat)/(1<<20) );
 //            printf( " %6d %6d ",   p->nLitUsed, p->nLitUseless );
-            printf( "%9.2f sec ",  1.0*(clock() - clkTotal)/CLOCKS_PER_SEC );
+            printf( "%9.2f sec ",  1.0*(Abc_Clock() - clkTotal)/CLOCKS_PER_SEC );
 //            printf( "\n" );
 //            ABC_PRMn( "Id2Var", (f+1)*p->nObjNums*4 );
 //            ABC_PRMn( "SAT", 42 * p->pSat->size + 16 * (int)p->pSat->stats.clauses + 4 * (int)p->pSat->stats.clauses_literals );
@@ -1584,10 +1584,10 @@ finish:
     if ( pPars->fVerbose )
     {
         printf( "Runtime:  " );
-        printf( "CNF = %.1f sec (%.1f %%)  ",   1.0*clkOther/CLOCKS_PER_SEC,   100.0*clkOther/(clock() - clkTotal)   );
-        printf( "UNSAT = %.1f sec (%.1f %%)  ", 1.0*nTimeUnsat/CLOCKS_PER_SEC, 100.0*nTimeUnsat/(clock() - clkTotal) );
-        printf( "SAT = %.1f sec (%.1f %%)  ",   1.0*nTimeSat/CLOCKS_PER_SEC,   100.0*nTimeSat/(clock() - clkTotal)   );
-        printf( "UNDEC = %.1f sec (%.1f %%)",   1.0*nTimeUndec/CLOCKS_PER_SEC, 100.0*nTimeUndec/(clock() - clkTotal) );
+        printf( "CNF = %.1f sec (%.1f %%)  ",   1.0*clkOther/CLOCKS_PER_SEC,   100.0*clkOther/(Abc_Clock() - clkTotal)   );
+        printf( "UNSAT = %.1f sec (%.1f %%)  ", 1.0*nTimeUnsat/CLOCKS_PER_SEC, 100.0*nTimeUnsat/(Abc_Clock() - clkTotal) );
+        printf( "SAT = %.1f sec (%.1f %%)  ",   1.0*nTimeSat/CLOCKS_PER_SEC,   100.0*nTimeSat/(Abc_Clock() - clkTotal)   );
+        printf( "UNDEC = %.1f sec (%.1f %%)",   1.0*nTimeUndec/CLOCKS_PER_SEC, 100.0*nTimeUndec/(Abc_Clock() - clkTotal) );
         printf( "\n" );
     }
     Saig_Bmc3ManStop( p );
diff --git a/src/sat/bmc/bmcCexDepth.c b/src/sat/bmc/bmcCexDepth.c
index b28a7ba7..7bdfd0ad 100644
--- a/src/sat/bmc/bmcCexDepth.c
+++ b/src/sat/bmc/bmcCexDepth.c
@@ -343,7 +343,7 @@ Gia_Man_t * Bmc_CexBuildNetwork2Test( Gia_Man_t * p, Abc_Cex_t * pCex, int nFram
 {
     Gia_Man_t * pNew, * pTemp;
     Vec_Ptr_t * vCones;
-    clock_t clk = clock();
+    abctime clk = Abc_Clock();
     int i;
     nFramesMax = Abc_MinInt( nFramesMax, pCex->iFrame );
     printf( "Processing CEX in frame %d (max frames %d).\n", pCex->iFrame, nFramesMax );
@@ -357,13 +357,13 @@ Gia_Man_t * Bmc_CexBuildNetwork2Test( Gia_Man_t * p, Abc_Cex_t * pCex, int nFram
     }
     pNew = Gia_ManDupAppendCones( p, (Gia_Man_t **)Vec_PtrArray(vCones), Vec_PtrSize(vCones), 1 );
     Gia_AigerWrite( pNew, "miter2.aig", 0, 0 );
-//Bmc_CexDumpAogStats( pNew, clock() - clk );
+//Bmc_CexDumpAogStats( pNew, Abc_Clock() - clk );
     Vec_PtrForEachEntry( Gia_Man_t *, vCones, pTemp, i )
         Gia_ManStop( pTemp );
     Vec_PtrFree( vCones );
     printf( "GIA with additional properties is written into \"miter2.aig\".\n" );
 //    printf( "CE-induced network is written into file \"unate.aig\".\n" );
-    Abc_PrintTime( 1, "Time", clock() - clk );
+    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
 //    Gia_ManStop( pNew );
     return pNew;
 }
@@ -383,7 +383,7 @@ Gia_Man_t * Bmc_CexBuildNetwork2Test( Gia_Man_t * p, Abc_Cex_t * pCex, int nFram
 Gia_Man_t * Bmc_CexDepthTest( Gia_Man_t * p, Abc_Cex_t * pCex, int nFrames, int fVerbose )
 {
     Gia_Man_t * pNew;
-    clock_t clk = clock();
+    abctime clk = Abc_Clock();
     Abc_Cex_t * pCexImpl   = NULL;
     Abc_Cex_t * pCexStates = Bmc_CexInnerStates( p, pCex, &pCexImpl, fVerbose );
     Abc_Cex_t * pCexCare   = Bmc_CexCareBits( p, pCexStates, pCexImpl, NULL, 1, fVerbose );
@@ -398,9 +398,9 @@ Gia_Man_t * Bmc_CexDepthTest( Gia_Man_t * p, Abc_Cex_t * pCex, int nFrames, int
 //    if ( !Bmc_CexVerify( p, pCex, pCexMin ) )
 //        printf( "Counter-example min-set verification has failed.\n" );
 
-//    Bmc_CexDumpStats( p, pCex, pCexCare, pCexEss, pCexMin, clock() - clk );
+//    Bmc_CexDumpStats( p, pCex, pCexCare, pCexEss, pCexMin, Abc_Clock() - clk );
 
-    Abc_PrintTime( 1, "Time", clock() - clk );
+    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
     pNew = Bmc_CexBuildNetwork2Test( p, pCexStates, nFrames );
 //    Bmc_CexPerformUnrollingTest( p, pCex );
 
diff --git a/src/sat/bmc/bmcCexTools.c b/src/sat/bmc/bmcCexTools.c
index bbf7d1ad..0260b537 100644
--- a/src/sat/bmc/bmcCexTools.c
+++ b/src/sat/bmc/bmcCexTools.c
@@ -75,7 +75,7 @@ int Bmc_CexBitCount( Abc_Cex_t * p, int nInputs )
   SeeAlso     []
 
 ***********************************************************************/
-void Bmc_CexDumpStats( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexCare, Abc_Cex_t * pCexEss, Abc_Cex_t * pCexMin, clock_t clk )
+void Bmc_CexDumpStats( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexCare, Abc_Cex_t * pCexEss, Abc_Cex_t * pCexMin, abctime clk )
 {
     int nInputs    = Gia_ManPiNum(p);
     int nBitsTotal = (pCex->iFrame + 1) * nInputs;
@@ -112,7 +112,7 @@ void Bmc_CexDumpStats( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexCare, Ab
   SeeAlso     []
 
 ***********************************************************************/
-void Bmc_CexDumpAogStats( Gia_Man_t * p, clock_t clk )
+void Bmc_CexDumpAogStats( Gia_Man_t * p, abctime clk )
 {
     FILE * pTable  = fopen( "cex/aig_stats.txt", "a+" );
     fprintf( pTable, "%s ", p->pName );
@@ -170,14 +170,14 @@ Gia_Man_t * Bmc_CexPerformUnrolling( Gia_Man_t * p, Abc_Cex_t * pCex )
 void Bmc_CexPerformUnrollingTest( Gia_Man_t * p, Abc_Cex_t * pCex )
 {
     Gia_Man_t * pNew;
-    clock_t clk = clock();
+    abctime clk = Abc_Clock();
     pNew = Bmc_CexPerformUnrolling( p, pCex );
     Gia_ManPrintStats( pNew, 0, 0, 0 );
     Gia_AigerWrite( pNew, "unroll.aig", 0, 0 );
-//Bmc_CexDumpAogStats( pNew, clock() - clk );
+//Bmc_CexDumpAogStats( pNew, Abc_Clock() - clk );
     Gia_ManStop( pNew );
     printf( "CE-induced network is written into file \"unroll.aig\".\n" );
-    Abc_PrintTime( 1, "Time", clock() - clk );
+    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
 }
 
 
@@ -282,14 +282,14 @@ Gia_Man_t * Bmc_CexBuildNetwork( Gia_Man_t * p, Abc_Cex_t * pCex )
 void Bmc_CexBuildNetworkTest( Gia_Man_t * p, Abc_Cex_t * pCex )
 {
     Gia_Man_t * pNew;
-    clock_t clk = clock();
+    abctime clk = Abc_Clock();
     pNew = Bmc_CexBuildNetwork( p, pCex );
     Gia_ManPrintStats( pNew, 0, 0, 0 );
     Gia_AigerWrite( pNew, "unate.aig", 0, 0 );
-//Bmc_CexDumpAogStats( pNew, clock() - clk );
+//Bmc_CexDumpAogStats( pNew, Abc_Clock() - clk );
     Gia_ManStop( pNew );
     printf( "CE-induced network is written into file \"unate.aig\".\n" );
-    Abc_PrintTime( 1, "Time", clock() - clk );
+    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
 }
 
 
@@ -756,7 +756,7 @@ Abc_Cex_t * Bmc_CexEssentialBits( Gia_Man_t * p, Abc_Cex_t * pCexState, Abc_Cex_
 {
     Abc_Cex_t * pNew, * pTemp, * pPrev = NULL;
     int b, fEqual = 0, fPrevStatus = 0;
-//    clock_t clk = clock();
+//    abctime clk = Abc_Clock();
     assert( pCexState->nBits == pCexCare->nBits );
     // start the counter-example
     pNew = Abc_CexAlloc( 0, Gia_ManCiNum(p), pCexState->iFrame + 1 );
@@ -795,7 +795,7 @@ Abc_Cex_t * Bmc_CexEssentialBits( Gia_Man_t * p, Abc_Cex_t * pCexState, Abc_Cex_
             Abc_InfoSetBit( pNew->pData, b );
     }
     Abc_CexFreeP( &pPrev );
-//    Abc_PrintTime( 1, "Time", clock() - clk );
+//    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
     printf( "Essentials:   " );
     Bmc_CexPrint( pNew, Gia_ManPiNum(p), fVerbose );
     return pNew;
@@ -815,7 +815,7 @@ Abc_Cex_t * Bmc_CexEssentialBits( Gia_Man_t * p, Abc_Cex_t * pCexState, Abc_Cex_
 ***********************************************************************/
 void Bmc_CexTest( Gia_Man_t * p, Abc_Cex_t * pCex, int fVerbose )
 {
-    clock_t clk = clock();
+    abctime clk = Abc_Clock();
     Abc_Cex_t * pCexImpl   = NULL;
     Abc_Cex_t * pCexStates = Bmc_CexInnerStates( p, pCex, &pCexImpl, fVerbose );
     Abc_Cex_t * pCexCare   = Bmc_CexCareBits( p, pCexStates, pCexImpl, NULL, 1, fVerbose );
@@ -830,7 +830,7 @@ void Bmc_CexTest( Gia_Man_t * p, Abc_Cex_t * pCex, int fVerbose )
     if ( !Bmc_CexVerify( p, pCex, pCexMin ) )
         printf( "Counter-example min-set verification has failed.\n" );
 
-//    Bmc_CexDumpStats( p, pCex, pCexCare, pCexEss, pCexMin, clock() - clk );
+//    Bmc_CexDumpStats( p, pCex, pCexCare, pCexEss, pCexMin, Abc_Clock() - clk );
 
     Abc_CexFreeP( &pCexStates );
     Abc_CexFreeP( &pCexImpl );
@@ -838,7 +838,7 @@ void Bmc_CexTest( Gia_Man_t * p, Abc_Cex_t * pCex, int fVerbose )
     Abc_CexFreeP( &pCexEss );
     Abc_CexFreeP( &pCexMin );
 
-    Abc_PrintTime( 1, "Time", clock() - clk );
+    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
 //    Bmc_CexBuildNetworkTest( p, pCex );
 //    Bmc_CexPerformUnrollingTest( p, pCex );
 }
diff --git a/src/sat/bmc/bmcUnroll.c b/src/sat/bmc/bmcUnroll.c
index 83848c49..dd1abde6 100644
--- a/src/sat/bmc/bmcUnroll.c
+++ b/src/sat/bmc/bmcUnroll.c
@@ -177,7 +177,7 @@ void Unr_ManSetup( Unr_Man_t * p )
     Gia_Obj_t * pObj, * pObjRi;
     Unr_Obj_t * pUnrObj;
     int i, k, t, iObj, nInts, * pInts;
-    clock_t clk = clock();
+    abctime clk = Abc_Clock();
     vRoots  = Vec_IntAlloc( 100 );
     vRoots2 = Vec_IntAlloc( 100 );
     // create zero rank
@@ -268,7 +268,7 @@ Unr_ManProfileRanks( p->vRanks );
     Vec_IntFreeP( &vMap );
 
     printf( "Memory usage = %6.2f MB\n", 4.0 * nInts / (1<<20) );
-    Abc_PrintTime( 1, "Time", clock() - clk );
+    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
 }