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

18 files changed, 136 insertions, 136 deletions

diff --git a/src/proof/ssw/sswBmc.c b/src/proof/ssw/sswBmc.c
index c88b2dcc..61c1c2a7 100644
--- a/src/proof/ssw/sswBmc.c
+++ b/src/proof/ssw/sswBmc.c
@@ -129,7 +129,7 @@ int Ssw_BmcDynamic( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int fVerbo
     Ssw_Sat_t * pSat;
     Aig_Obj_t * pObj, * pObjFrame;
     int status, Lit, i, f, RetValue;
-    clock_t clkPart;
+    abctime clkPart;
 
     // start managers
     assert( Saig_ManRegNum(pAig) > 0 );
@@ -149,7 +149,7 @@ int Ssw_BmcDynamic( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int fVerbo
     RetValue = -1;
     for ( f = 0; f < nFramesMax; f++ )
     {
-        clkPart = clock();
+        clkPart = Abc_Clock();
         Saig_ManForEachPo( pAig, pObj, i )
         {
             // unroll the circuit for this output
@@ -203,8 +203,8 @@ int Ssw_BmcDynamic( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int fVerbo
             Abc_Print( 1, "Conf =%8.0f. Var =%8d. AIG=%9d. ",
                 (double)pSat->pSat->stats.conflicts,
                 pSat->nSatVars, Aig_ManNodeNum(pFrm->pFrames) );
-            ABC_PRT( "T", clock() - clkPart );
-            clkPart = clock();
+            ABC_PRT( "T", Abc_Clock() - clkPart );
+            clkPart = Abc_Clock();
             fflush( stdout );
         }
         if ( RetValue != 1 )
diff --git a/src/proof/ssw/sswClass.c b/src/proof/ssw/sswClass.c
index 9cf8871b..0613302e 100644
--- a/src/proof/ssw/sswClass.c
+++ b/src/proof/ssw/sswClass.c
@@ -611,25 +611,25 @@ Ssw_Cla_t * Ssw_ClassesPrepare( Aig_Man_t * pAig, int nFramesK, int fLatchCorr,
     Vec_Ptr_t * vCands;
     Aig_Obj_t * pObj;
     int i, k, RetValue;
-    clock_t clk;
+    abctime clk;
 
     // start the classes
     p = Ssw_ClassesStart( pAig );
     p->fConstCorr = fConstCorr;
 
     // perform sequential simulation
-clk = clock();
+clk = Abc_Clock();
     pSml = Ssw_SmlSimulateSeq( pAig, 0, nFrames, nWords );
 if ( fVerbose )
 {
     Abc_Print( 1, "Allocated %.2f MB to store simulation information.\n",
         1.0*(sizeof(unsigned) * Aig_ManObjNumMax(pAig) * nFrames * nWords)/(1<<20) );
     Abc_Print( 1, "Initial simulation of %d frames with %d words.     ", nFrames, nWords );
-    ABC_PRT( "Time", clock() - clk );
+    ABC_PRT( "Time", Abc_Clock() - clk );
 }
 
     // set comparison procedures
-clk = clock();
+clk = Abc_Clock();
     Ssw_ClassesSetData( p, pSml, (unsigned(*)(void *,Aig_Obj_t *))Ssw_SmlObjHashWord, (int(*)(void *,Aig_Obj_t *))Ssw_SmlObjIsConstWord, (int(*)(void *,Aig_Obj_t *,Aig_Obj_t *))Ssw_SmlObjsAreEqualWord );
 
     // collect nodes to be considered as candidates
@@ -677,10 +677,10 @@ clk = clock();
 if ( fVerbose )
 {
     Abc_Print( 1, "Collecting candidate equivalence classes.        " );
-ABC_PRT( "Time", clock() - clk );
+ABC_PRT( "Time", Abc_Clock() - clk );
 }
 
-clk = clock();
+clk = Abc_Clock();
     // perform iterative refinement using simulation
     for ( i = 1; i < nIters; i++ )
     {
@@ -703,7 +703,7 @@ if ( fVerbose )
 {
     Abc_Print( 1, "Simulation of %d frames with %d words (%2d rounds). ",
         nFrames, nWords, i-1 );
-    ABC_PRT( "Time", clock() - clk );
+    ABC_PRT( "Time", Abc_Clock() - clk );
 }
     Ssw_ClassesCheck( p );
 //    Ssw_ClassesPrint( p, 0 );
diff --git a/src/proof/ssw/sswConstr.c b/src/proof/ssw/sswConstr.c
index 3dcf0a34..a9ed17fc 100644
--- a/src/proof/ssw/sswConstr.c
+++ b/src/proof/ssw/sswConstr.c
@@ -409,8 +409,8 @@ int Ssw_ManSweepBmcConstr_old( Ssw_Man_t * p )
     Bar_Progress_t * pProgress = NULL;
     Aig_Obj_t * pObj, * pObjNew, * pObjLi, * pObjLo;
     int i, f, iLits;
-    clock_t clk;
-clk = clock();
+    abctime clk;
+clk = Abc_Clock();
 
     // start initialized timeframes
     p->pFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * p->pPars->nFramesK );
@@ -480,7 +480,7 @@ clk = clock();
 
     // cleanup
 //    Ssw_ClassesCheck( p->ppClasses );
-p->timeBmc += clock() - clk;
+p->timeBmc += Abc_Clock() - clk;
     return p->fRefined;
 }
 
@@ -499,8 +499,8 @@ int Ssw_ManSweepBmcConstr( Ssw_Man_t * p )
 {
     Aig_Obj_t * pObj, * pObjNew, * pObjLi, * pObjLo;
     int i, f, iLits;
-    clock_t clk;
-clk = clock();
+    abctime clk;
+clk = Abc_Clock();
 
     // start initialized timeframes
     p->pFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * p->pPars->nFramesK );
@@ -560,7 +560,7 @@ clk = clock();
 
     // cleanup
 //    Ssw_ClassesCheck( p->ppClasses );
-p->timeBmc += clock() - clk;
+p->timeBmc += Abc_Clock() - clk;
     return p->fRefined;
 }
 
@@ -621,11 +621,11 @@ int Ssw_ManSweepConstr( Ssw_Man_t * p )
     Bar_Progress_t * pProgress = NULL;
     Aig_Obj_t * pObj, * pObj2, * pObjNew;
     int nConstrPairs, i, f, iLits;
-    clock_t clk;
+    abctime clk;
 //Ssw_ManPrintPolarity( p->pAig );
 
     // perform speculative reduction
-clk = clock();
+clk = Abc_Clock();
     // create timeframes
     p->pFrames = Ssw_FramesWithClasses( p );
     // add constants
@@ -656,7 +656,7 @@ clk = clock();
         Ssw_ObjSetFrame( p, pObj, f, pObjNew );
     }
     assert( Vec_IntSize(p->vInits) == iLits );
-p->timeReduce += clock() - clk;
+p->timeReduce += Abc_Clock() - clk;
 
     // add constraints to all timeframes
     for ( f = 0; f <= p->pPars->nFramesK; f++ )
diff --git a/src/proof/ssw/sswCore.c b/src/proof/ssw/sswCore.c
index 7a9d4b9f..f944eddc 100644
--- a/src/proof/ssw/sswCore.c
+++ b/src/proof/ssw/sswCore.c
@@ -236,7 +236,7 @@ Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p )
     int nSatProof, nSatCallsSat, nRecycles, nSatFailsReal, nUniques;
     Aig_Man_t * pAigNew;
     int RetValue, nIter = -1;
-    clock_t clk, clkTotal = clock();
+    abctime clk, clkTotal = Abc_Clock();
     // get the starting stats
     p->nLitsBeg  = Ssw_ClassesLitNum( p->ppClasses );
     p->nNodesBeg = Aig_ManNodeNum(p->pAig);
@@ -306,7 +306,7 @@ Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p )
             break;
         }
 
-clk = clock();
+clk = Abc_Clock();
         p->pMSat = Ssw_SatStart( 0 );
         if ( p->pPars->fLatchCorrOpt )
         {
@@ -317,7 +317,7 @@ clk = clock();
                     nIter, Ssw_ClassesCand1Num(p->ppClasses), Ssw_ClassesClassNum(p->ppClasses),
                     p->nSatProof-nSatProof, p->nSatCallsSat-nSatCallsSat,
                     p->nRecycles-nRecycles, p->nSatFailsReal-nSatFailsReal );
-                ABC_PRT( "T", clock() - clk );
+                ABC_PRT( "T", Abc_Clock() - clk );
             }
         }
         else
@@ -342,7 +342,7 @@ clk = clock();
                 }
                 Abc_Print( 1, "F =%5d. %s ", p->nSatFailsReal-nSatFailsReal,
                     (Saig_ManPoNum(p->pAig)==1 && Ssw_ObjIsConst1Cand(p->pAig,Aig_ObjFanin0(Aig_ManCo(p->pAig,0))))? "+" : "-" );
-                ABC_PRT( "T", clock() - clk );
+                ABC_PRT( "T", Abc_Clock() - clk );
             }
 //            if ( p->pPars->fDynamic && p->nSatCallsSat-nSatCallsSat < 100 )
 //                p->pPars->nBTLimit = 10000;
@@ -384,7 +384,7 @@ clk = clock();
 
 finalize:
     p->pPars->nIters = nIter + 1;
-p->timeTotal = clock() - clkTotal;
+p->timeTotal = Abc_Clock() - clkTotal;
 
     Ssw_ManUpdateEquivs( p, p->pAig, p->pPars->fVerbose );
     pAigNew = Aig_ManDupRepr( p->pAig, 0 );
diff --git a/src/proof/ssw/sswDyn.c b/src/proof/ssw/sswDyn.c
index 5fc22fdf..316b2e4d 100644
--- a/src/proof/ssw/sswDyn.c
+++ b/src/proof/ssw/sswDyn.c
@@ -263,7 +263,7 @@ void Ssw_ManSweepTransferDyn( Ssw_Man_t * p )
 int Ssw_ManSweepResimulateDyn( Ssw_Man_t * p, int f )
 {
     int RetValue1, RetValue2;
-    clock_t clk = clock();
+    abctime clk = Abc_Clock();
     // transfer PI simulation information from storage
 //    Ssw_SmlAssignDist1Plus( p->pSml, p->pPatWords );
     Ssw_ManSweepTransferDyn( p );
@@ -277,7 +277,7 @@ int Ssw_ManSweepResimulateDyn( Ssw_Man_t * p, int f )
     Vec_PtrCleanSimInfo( p->vSimInfo, 0, 1 );
     p->nPatterns = 0;
     p->nSimRounds++;
-p->timeSimSat += clock() - clk;
+p->timeSimSat += Abc_Clock() - clk;
     return RetValue1 > 0 || RetValue2 > 0;
 }
 
@@ -296,7 +296,7 @@ int Ssw_ManSweepResimulateDynLocal( Ssw_Man_t * p, int f )
 {
     Aig_Obj_t * pObj, * pRepr, ** ppClass;
     int i, k, nSize, RetValue1, RetValue2;
-    clock_t clk = clock();
+    abctime clk = Abc_Clock();
     p->nSimRounds++;
     // transfer PI simulation information from storage
 //    Ssw_SmlAssignDist1Plus( p->pSml, p->pPatWords );
@@ -355,7 +355,7 @@ int Ssw_ManSweepResimulateDynLocal( Ssw_Man_t * p, int f )
     Vec_PtrCleanSimInfo( p->vSimInfo, 0, 1 );
     p->nPatterns = 0;
     p->nSimRounds++;
-p->timeSimSat += clock() - clk;
+p->timeSimSat += Abc_Clock() - clk;
     return RetValue1 > 0 || RetValue2 > 0;
 }
 
@@ -375,10 +375,10 @@ int Ssw_ManSweepDyn( Ssw_Man_t * p )
     Bar_Progress_t * pProgress = NULL;
     Aig_Obj_t * pObj, * pObjNew;
     int i, f;
-    clock_t clk;
+    abctime clk;
 
     // perform speculative reduction
-clk = clock();
+clk = Abc_Clock();
     // create timeframes
     p->pFrames = Ssw_FramesWithClasses( p );
     Aig_ManFanoutStart( p->pFrames );
@@ -392,7 +392,7 @@ clk = clock();
     Aig_ManSetCioIds( p->pFrames );
     // label nodes corresponding to primary inputs
     Ssw_ManLabelPiNodes( p );
-p->timeReduce += clock() - clk;
+p->timeReduce += Abc_Clock() - clk;
 
     // prepare simulation info
     assert( p->vSimInfo == NULL );
diff --git a/src/proof/ssw/sswFilter.c b/src/proof/ssw/sswFilter.c
index 534fc275..9027d773 100644
--- a/src/proof/ssw/sswFilter.c
+++ b/src/proof/ssw/sswFilter.c
@@ -279,7 +279,7 @@ int Ssw_ManSweepBmcFilter( Ssw_Man_t * p, int TimeLimit )
 {
     Aig_Obj_t * pObj, * pObjNew, * pObjLi, * pObjLo;
     int f, f1, i;
-    clock_t clkTotal = clock();
+    abctime clkTotal = Abc_Clock();
     // start initialized timeframes
     p->pFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * p->pPars->nFramesK );
     Saig_ManForEachLo( p->pAig, pObj, i )
@@ -349,7 +349,7 @@ int Ssw_ManSweepBmcFilter( Ssw_Man_t * p, int TimeLimit )
             break;
         }
         // check timeout
-        if ( TimeLimit && ((float)TimeLimit <= (float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)) )
+        if ( TimeLimit && ((float)TimeLimit <= (float)(Abc_Clock()-clkTotal)/(float)(CLOCKS_PER_SEC)) )
             break;
         // transfer latch input to the latch outputs 
         Aig_ManForEachCo( p->pAig, pObj, i )
@@ -383,8 +383,8 @@ void Ssw_SignalFilter( Aig_Man_t * pAig, int nFramesMax, int nConfMax, int nRoun
 {
     Ssw_Pars_t Pars, * pPars = &Pars;
     Ssw_Man_t * p;
-    int r, TimeLimitPart;//, clkTotal = clock();
-    clock_t nTimeToStop = TimeLimit ? TimeLimit * CLOCKS_PER_SEC + clock(): 0;
+    int r, TimeLimitPart;//, clkTotal = Abc_Clock();
+    abctime nTimeToStop = TimeLimit ? TimeLimit * CLOCKS_PER_SEC + Abc_Clock(): 0;
     assert( Aig_ManRegNum(pAig) > 0 );
     assert( Aig_ManConstrNum(pAig) == 0 );
     // consider the case of empty AIG
@@ -430,7 +430,7 @@ void Ssw_SignalFilter( Aig_Man_t * pAig, int nFramesMax, int nConfMax, int nRoun
             Ssw_ClassesPrint( p->ppClasses, 0 );
         }
         p->pMSat = Ssw_SatStart( 0 );
-        TimeLimitPart = TimeLimit ? (nTimeToStop - clock()) / CLOCKS_PER_SEC : 0;
+        TimeLimitPart = TimeLimit ? (nTimeToStop - Abc_Clock()) / CLOCKS_PER_SEC : 0;
         if ( TimeLimit2 )
         {
             if ( TimeLimitPart )
@@ -445,7 +445,7 @@ void Ssw_SignalFilter( Aig_Man_t * pAig, int nFramesMax, int nConfMax, int nRoun
         // simulate pattern forward
         Ssw_ManRollForward( p, p->pPars->nFramesK );
         // check timeout
-        if ( TimeLimit && clock() > nTimeToStop )
+        if ( TimeLimit && Abc_Clock() > nTimeToStop )
         {
             Abc_Print( 1, "Reached timeout (%d seconds).\n",  TimeLimit );
             break;
diff --git a/src/proof/ssw/sswInt.h b/src/proof/ssw/sswInt.h
index 1edf2087..00681923 100644
--- a/src/proof/ssw/sswInt.h
+++ b/src/proof/ssw/sswInt.h
@@ -127,16 +127,16 @@ struct Ssw_Man_t_
     int              nRegsBegC;
     int              nRegsEndC;
     // runtime stats
-    clock_t          timeBmc;        // bounded model checking
-    clock_t          timeReduce;     // speculative reduction
-    clock_t          timeMarkCones;  // marking the cones not to be refined
-    clock_t          timeSimSat;     // simulation of the counter-examples
-    clock_t          timeSat;        // solving SAT
-    clock_t          timeSatSat;     // sat
-    clock_t          timeSatUnsat;   // unsat
-    clock_t          timeSatUndec;   // undecided
-    clock_t          timeOther;      // other runtime
-    clock_t          timeTotal;      // total runtime
+    abctime          timeBmc;        // bounded model checking
+    abctime          timeReduce;     // speculative reduction
+    abctime          timeMarkCones;  // marking the cones not to be refined
+    abctime          timeSimSat;     // simulation of the counter-examples
+    abctime          timeSat;        // solving SAT
+    abctime          timeSatSat;     // sat
+    abctime          timeSatUnsat;   // unsat
+    abctime          timeSatUndec;   // undecided
+    abctime          timeOther;      // other runtime
+    abctime          timeTotal;      // total runtime
 };
 
 // internal SAT manager
diff --git a/src/proof/ssw/sswIslands.c b/src/proof/ssw/sswIslands.c
index d1758b75..87df4ebf 100644
--- a/src/proof/ssw/sswIslands.c
+++ b/src/proof/ssw/sswIslands.c
@@ -480,7 +480,7 @@ int Ssw_SecWithSimilarityPairs( Aig_Man_t * p0, Aig_Man_t * p1, Vec_Int_t * vPai
     Ssw_Pars_t Pars;
     Aig_Man_t * pAigRes;
     int RetValue;
-    clock_t clk = clock();
+    abctime clk = Abc_Clock();
     // derive parameters if not given
     if ( pPars == NULL )
         Ssw_ManSetDefaultParams( pPars = &Pars );
@@ -495,7 +495,7 @@ int Ssw_SecWithSimilarityPairs( Aig_Man_t * p0, Aig_Man_t * p1, Vec_Int_t * vPai
     else
         Abc_Print( 1, "Verification UNDECIDED. The number of remaining regs = %d (total = %d).  ",
             Aig_ManRegNum(pAigRes), Aig_ManRegNum(p0)+Aig_ManRegNum(p1) );
-    ABC_PRT( "Time", clock() - clk );
+    ABC_PRT( "Time", Abc_Clock() - clk );
     Aig_ManStop( pAigRes );
     return RetValue;
 }
diff --git a/src/proof/ssw/sswLcorr.c b/src/proof/ssw/sswLcorr.c
index cd212e0b..d020ef00 100644
--- a/src/proof/ssw/sswLcorr.c
+++ b/src/proof/ssw/sswLcorr.c
@@ -78,7 +78,7 @@ void Ssw_ManSweepTransfer( Ssw_Man_t * p )
 int Ssw_ManSweepResimulate( Ssw_Man_t * p )
 {
     int RetValue1, RetValue2;
-    clock_t clk = clock();
+    abctime clk = Abc_Clock();
     // transfer PI simulation information from storage
     Ssw_ManSweepTransfer( p );
     // simulate internal nodes
@@ -90,7 +90,7 @@ int Ssw_ManSweepResimulate( Ssw_Man_t * p )
     Vec_PtrCleanSimInfo( p->vSimInfo, 0, 1 );
     p->nPatterns = 0;
     p->nSimRounds++;
-p->timeSimSat += clock() - clk;
+p->timeSimSat += Abc_Clock() - clk;
     return RetValue1 > 0 || RetValue2 > 0;
 }
 
@@ -161,7 +161,7 @@ void Ssw_ManSweepLatchOne( Ssw_Man_t * p, Aig_Obj_t * pObjRepr, Aig_Obj_t * pObj
 {
     Aig_Obj_t * pObjFraig, * pObjReprFraig, * pObjLi;
     int RetValue;
-    clock_t clk;
+    abctime clk;
     assert( Aig_ObjIsCi(pObj) );
     assert( Aig_ObjIsCi(pObjRepr) || Aig_ObjIsConst1(pObjRepr) );
     // check if it makes sense to skip some calls
@@ -171,7 +171,7 @@ void Ssw_ManSweepLatchOne( Ssw_Man_t * p, Aig_Obj_t * pObjRepr, Aig_Obj_t * pObj
             return;
     }
     p->nCallsDelta = 0;
-clk = clock();
+clk = Abc_Clock();
     // get the fraiged node
     pObjLi = Saig_ObjLoToLi( p->pAig, pObj );
     Ssw_ManBuildCone_rec( p, Aig_ObjFanin0(pObjLi) );
@@ -185,7 +185,7 @@ clk = clock();
     }
     else
         pObjReprFraig = Ssw_ObjFrame( p, pObjRepr, 0 );
-p->timeReduce += clock() - clk;
+p->timeReduce += Abc_Clock() - clk;
     // if the fraiged nodes are the same, return
     if ( Aig_Regular(pObjFraig) == Aig_Regular(pObjReprFraig) )
         return;
diff --git a/src/proof/ssw/sswPairs.c b/src/proof/ssw/sswPairs.c
index 3068adc4..fe389191 100644
--- a/src/proof/ssw/sswPairs.c
+++ b/src/proof/ssw/sswPairs.c
@@ -321,7 +321,7 @@ Aig_Man_t * Ssw_SignalCorrespondeceTestPairs( Aig_Man_t * pAig )
     Vec_Int_t * vIds1, * vIds2;
     Aig_Obj_t * pObj, * pRepr;
     int RetValue, i;
-    clock_t clk = clock();
+    abctime clk = Abc_Clock();
     Ssw_ManSetDefaultParams( pPars );
     pPars->fVerbose = 1;
     pAigNew = Ssw_SignalCorrespondence( pAig, pPars );
@@ -360,7 +360,7 @@ Aig_Man_t * Ssw_SignalCorrespondeceTestPairs( Aig_Man_t * pAig )
     else
         Abc_Print( 1, "Verification UNDECIDED. Remaining registers %d (total %d).  ",
             Aig_ManRegNum(pAigRes), Aig_ManRegNum(pAig) + Aig_ManRegNum(pAigNew) );
-    ABC_PRT( "Time", clock() - clk );
+    ABC_PRT( "Time", Abc_Clock() - clk );
     // cleanup
     Aig_ManStop( pAigNew );
     return pAigRes;
@@ -381,7 +381,7 @@ int Ssw_SecWithPairs( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Vec_Int_t * vIds1, V
 {
     Aig_Man_t * pAigRes;
     int RetValue;
-    clock_t clk = clock();
+    abctime clk = Abc_Clock();
     assert( vIds1 != NULL && vIds2 != NULL );
     // try the new AIGs
     Abc_Print( 1, "Performing specialized verification with node pairs.\n" );
@@ -395,7 +395,7 @@ int Ssw_SecWithPairs( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Vec_Int_t * vIds1, V
     else
         Abc_Print( 1, "Verification UNDECIDED. The number of remaining regs = %d (total = %d).  ",
             Aig_ManRegNum(pAigRes), Aig_ManRegNum(pAig1) + Aig_ManRegNum(pAig2) );
-    ABC_PRT( "Time", clock() - clk );
+    ABC_PRT( "Time", Abc_Clock() - clk );
     // cleanup
     Aig_ManStop( pAigRes );
     return RetValue;
@@ -416,7 +416,7 @@ int Ssw_SecGeneral( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Ssw_Pars_t * pPars )
 {
     Aig_Man_t * pAigRes, * pMiter;
     int RetValue;
-    clock_t clk = clock();
+    abctime clk = Abc_Clock();
     // try the new AIGs
     Abc_Print( 1, "Performing general verification without node pairs.\n" );
     pMiter = Saig_ManCreateMiter( pAig1, pAig2, 0 );
@@ -432,7 +432,7 @@ int Ssw_SecGeneral( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Ssw_Pars_t * pPars )
     else
         Abc_Print( 1, "Verification UNDECIDED. The number of remaining regs = %d (total = %d).  ",
             Aig_ManRegNum(pAigRes), Aig_ManRegNum(pAig1) + Aig_ManRegNum(pAig2) );
-    ABC_PRT( "Time", clock() - clk );
+    ABC_PRT( "Time", Abc_Clock() - clk );
     // cleanup
     Aig_ManStop( pAigRes );
     return RetValue;
@@ -453,7 +453,7 @@ int Ssw_SecGeneralMiter( Aig_Man_t * pMiter, Ssw_Pars_t * pPars )
 {
     Aig_Man_t * pAigRes;
     int RetValue;
-    clock_t clk = clock();
+    abctime clk = Abc_Clock();
     // try the new AIGs
 //    Abc_Print( 1, "Performing general verification without node pairs.\n" );
     pAigRes = Ssw_SignalCorrespondence( pMiter, pPars );
@@ -466,7 +466,7 @@ int Ssw_SecGeneralMiter( Aig_Man_t * pMiter, Ssw_Pars_t * pPars )
     else
         Abc_Print( 1, "Verification UNDECIDED. The number of remaining regs = %d (total = %d).  ",
             Aig_ManRegNum(pAigRes), Aig_ManRegNum(pMiter) );
-    ABC_PRT( "Time", clock() - clk );
+    ABC_PRT( "Time", Abc_Clock() - clk );
     // cleanup
     Aig_ManStop( pAigRes );
     return RetValue;
diff --git a/src/proof/ssw/sswPart.c b/src/proof/ssw/sswPart.c
index dbe8a877..30afddca 100644
--- a/src/proof/ssw/sswPart.c
+++ b/src/proof/ssw/sswPart.c
@@ -53,7 +53,7 @@ Aig_Man_t * Ssw_SignalCorrespondencePart( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
     int * pMapBack;
     int i, nCountPis, nCountRegs;
     int nClasses, nPartSize, fVerbose;
-    clock_t clk = clock();
+    abctime clk = Abc_Clock();
     if ( pPars->fConstrs )
     {
         Abc_Print( 1, "Cannot use partitioned computation with constraints.\n" );
@@ -126,7 +126,7 @@ Aig_Man_t * Ssw_SignalCorrespondencePart( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
     pPars->fVerbose = fVerbose;
     if ( fVerbose )
     {
-        ABC_PRT( "Total time", clock() - clk );
+        ABC_PRT( "Total time", Abc_Clock() - clk );
     }
     return pNew;
 }
diff --git a/src/proof/ssw/sswRarity.c b/src/proof/ssw/sswRarity.c
index d780b915..10e19b5a 100644
--- a/src/proof/ssw/sswRarity.c
+++ b/src/proof/ssw/sswRarity.c
@@ -314,7 +314,7 @@ void TransposeTest()
 {
     word M[64], N[64];
     int i;
-    clock_t clk;
+    abctime clk;
     Aig_ManRandom64( 1 );
 //    for ( i = 0; i < 64; i++ )
 //        M[i] = Aig_ManRandom64( 0 );
@@ -323,15 +323,15 @@ void TransposeTest()
 //    for ( i = 0; i < 64; i++ )
 //        Extra_PrintBinary( stdout, (unsigned *)&M[i], 64 ), Abc_Print( 1, "\n" );
 
-    clk = clock();
+    clk = Abc_Clock();
     for ( i = 0; i < 100001; i++ )
         transpose64Simple( M, N );
-    Abc_PrintTime( 1, "Time", clock() - clk );
+    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
 
-    clk = clock();
+    clk = Abc_Clock();
     for ( i = 0; i < 100001; i++ )
         transpose64( M );
-    Abc_PrintTime( 1, "Time", clock() - clk );
+    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
 
     for ( i = 0; i < 64; i++ )
         if ( M[i] != N[i] )
@@ -594,7 +594,7 @@ int Ssw_RarManObjWhichOne( Ssw_RarMan_t * p, Aig_Obj_t * pObj )
   SeeAlso     []
 
 ***********************************************************************/
-int Ssw_RarManCheckNonConstOutputs( Ssw_RarMan_t * p, int iFrame, clock_t Time )
+int Ssw_RarManCheckNonConstOutputs( Ssw_RarMan_t * p, int iFrame, abctime Time )
 {
     Aig_Obj_t * pObj;
     int i;
@@ -976,9 +976,9 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, Ssw_RarPars_t * pPars )
     int fMiter = 1;
     Ssw_RarMan_t * p;
     int r, f = -1;
-    clock_t clk, clkTotal = clock();
-    clock_t nTimeToStop = pPars->TimeOut ? pPars->TimeOut * CLOCKS_PER_SEC + clock(): 0;
-    clock_t timeLastSolved = 0;
+    abctime clk, clkTotal = Abc_Clock();
+    abctime nTimeToStop = pPars->TimeOut ? pPars->TimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0;
+    abctime timeLastSolved = 0;
     int nNumRestart = 0;
     int nSavedSeed = pPars->nRandSeed;
     int RetValue = -1;
@@ -1004,10 +1004,10 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, Ssw_RarPars_t * pPars )
 
     // perform simulation rounds
     pPars->nSolved = 0;
-    timeLastSolved = clock();
+    timeLastSolved = Abc_Clock();
     for ( r = 0; !pPars->nRounds || (nNumRestart * pPars->nRestart + r < pPars->nRounds); r++ )
     {
-        clk = clock();
+        clk = Abc_Clock();
         if ( fTryBmc )
         {
             Aig_Man_t * pNewAig = Saig_ManDupWithPhase( pAig, p->vInits );
@@ -1022,7 +1022,7 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, Ssw_RarPars_t * pPars )
             Ssw_RarManSimulate( p, f ? NULL : p->vInits, 0, 0 );
             if ( fMiter )
             {
-                int Status = Ssw_RarManCheckNonConstOutputs(p, r * p->pPars->nFrames + f, clock() - clkTotal);
+                int Status = Ssw_RarManCheckNonConstOutputs(p, r * p->pPars->nFrames + f, Abc_Clock() - clkTotal);
                 if ( Status == 2 )
                 {
                     Abc_Print( 1, "Quitting due to callback on fail.\n" );
@@ -1041,22 +1041,22 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, Ssw_RarPars_t * pPars )
                         pAig->pSeqModel = Ssw_RarDeriveCex( p, r * p->pPars->nFrames + f, p->iFailPo, p->iFailPat, pPars->fVerbose );
                         // print final report
                         Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d.  ", pAig->pSeqModel->iPo, pAig->pName, pAig->pSeqModel->iFrame );
-                        Abc_PrintTime( 1, "Time", clock() - clkTotal );
+                        Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
                         goto finish;
                     }
-                    timeLastSolved = clock();
+                    timeLastSolved = Abc_Clock();
                 }
                 // else - did not find a counter example
             }
             // check timeout
-            if ( pPars->TimeOut && clock() > nTimeToStop )
+            if ( pPars->TimeOut && Abc_Clock() > nTimeToStop )
             {
                 if ( pPars->fVerbose && !pPars->fSolveAll ) Abc_Print( 1, "\n" );
                 Abc_Print( 1, "Simulated %d frames for %d rounds with %d restarts.  ", pPars->nFrames, nNumRestart * pPars->nRestart + r, nNumRestart );
                 Abc_Print( 1, "Reached timeout (%d sec).\n",  pPars->TimeOut );
                 goto finish;
             }
-            if ( pPars->TimeOutGap && timeLastSolved && clock() > timeLastSolved + pPars->TimeOutGap * CLOCKS_PER_SEC )
+            if ( pPars->TimeOutGap && timeLastSolved && Abc_Clock() > timeLastSolved + pPars->TimeOutGap * CLOCKS_PER_SEC )
             {
                 if ( pPars->fVerbose && !pPars->fSolveAll ) Abc_Print( 1, "\n" );
                 Abc_Print( 1, "Simulated %d frames for %d rounds with %d restarts.  ", pPars->nFrames, nNumRestart * pPars->nRestart + r, nNumRestart );
@@ -1090,7 +1090,7 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, Ssw_RarPars_t * pPars )
                 Abc_Print( 1, "Rounds =%6d   ",  nNumRestart * pPars->nRestart + ((r==-1)?0:r) );
                 Abc_Print( 1, "Frames =%6d   ", (nNumRestart * pPars->nRestart + r) * pPars->nFrames );
                 Abc_Print( 1, "CEX =%6d (%6.2f %%)   ", pPars->nSolved, 100.0*pPars->nSolved/Saig_ManPoNum(p->pAig) );
-                Abc_PrintTime( 1, "Time", clock() - clkTotal );
+                Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
             }
             else
                 Abc_Print( 1, "." );
@@ -1108,13 +1108,13 @@ finish:
     {
         if ( pPars->fVerbose && !pPars->fSolveAll ) Abc_Print( 1, "\n" );
         Abc_Print( 1, "Simulation of %d frames for %d rounds with %d restarts asserted %d (out of %d) POs.    ", pPars->nFrames, nNumRestart * pPars->nRestart + r, nNumRestart, pPars->nSolved, Saig_ManPoNum(p->pAig) );
-        Abc_PrintTime( 1, "Time", clock() - clkTotal );
+        Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
     }
     else if ( r == pPars->nRounds && f == pPars->nFrames )
     {
         if ( pPars->fVerbose ) Abc_Print( 1, "\n" );
         Abc_Print( 1, "Simulation of %d frames for %d rounds with %d restarts did not assert POs.    ", pPars->nFrames, nNumRestart * pPars->nRestart + r, nNumRestart );
-        Abc_PrintTime( 1, "Time", clock() - clkTotal );
+        Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
     }
     // cleanup
     Ssw_RarManStop( p );
@@ -1161,8 +1161,8 @@ int Ssw_RarSignalFilter( Aig_Man_t * pAig, Ssw_RarPars_t * pPars )
 {
     Ssw_RarMan_t * p;
     int r, f = -1, i, k;
-    clock_t clkTotal = clock();
-    clock_t nTimeToStop = pPars->TimeOut ? pPars->TimeOut * CLOCKS_PER_SEC + clock(): 0;
+    abctime clkTotal = Abc_Clock();
+    abctime nTimeToStop = pPars->TimeOut ? pPars->TimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0;
     int nNumRestart = 0;
     int nSavedSeed = pPars->nRandSeed;
     int RetValue = -1;
@@ -1234,12 +1234,12 @@ int Ssw_RarSignalFilter( Aig_Man_t * pAig, Ssw_RarPars_t * pPars )
                 pAig->pSeqModel = Ssw_RarDeriveCex( p, r * p->pPars->nFrames + f, p->iFailPo, p->iFailPat, 1 );
                 // print final report
                 Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d.  ", pAig->pSeqModel->iPo, pAig->pName, pAig->pSeqModel->iFrame );
-                Abc_PrintTime( 1, "Time", clock() - clkTotal );
+                Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
                 RetValue = 0;
                 goto finish;
             }
             // check timeout
-            if ( pPars->TimeOut && clock() > nTimeToStop )
+            if ( pPars->TimeOut && Abc_Clock() > nTimeToStop )
             {
                 if ( pPars->fVerbose ) Abc_Print( 1, "\n" );
                 Abc_Print( 1, "Simulated %d frames for %d rounds with %d restarts.  ", pPars->nFrames, nNumRestart * pPars->nRestart + r, nNumRestart );
@@ -1279,7 +1279,7 @@ finish:
         if ( !pPars->fVerbose )
             Abc_Print( 1, "%s", Abc_FrameIsBatchMode() ? "\n" : "\r" );
         Abc_Print( 1, "Simulation of %d frames for %d rounds with %d restarts did not assert POs.    ", pPars->nFrames, nNumRestart * pPars->nRestart + r, nNumRestart );
-        Abc_PrintTime( 1, "Time", clock() - clkTotal );
+        Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
     }
     // cleanup
     Ssw_RarManStop( p );
diff --git a/src/proof/ssw/sswRarity2.c b/src/proof/ssw/sswRarity2.c
index f6b2c319..01f288c1 100644
--- a/src/proof/ssw/sswRarity2.c
+++ b/src/proof/ssw/sswRarity2.c
@@ -309,8 +309,8 @@ int Ssw_RarSimulate2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, i
     int fMiter = 1;
     Ssw_RarMan_t * p;
     int r;
-    clock_t clk, clkTotal = clock();
-    clock_t nTimeToStop = TimeOut ? TimeOut * CLOCKS_PER_SEC + clock(): 0;
+    abctime clk, clkTotal = Abc_Clock();
+    abctime nTimeToStop = TimeOut ? TimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0;
     int RetValue = -1;
     assert( Aig_ManRegNum(pAig) > 0 );
     assert( Aig_ManConstrNum(pAig) == 0 );
@@ -331,7 +331,7 @@ int Ssw_RarSimulate2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, i
     // perform simulation rounds
     for ( r = 0; r < nRounds; r++ )
     {
-        clk = clock();
+        clk = Abc_Clock();
         // simulate
         Ssw_SmlSimulateOne( p->pSml );
         if ( fMiter && Ssw_SmlCheckNonConstOutputs(p->pSml) )
@@ -349,11 +349,11 @@ int Ssw_RarSimulate2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, i
         if ( fVerbose )
         {
 //            Abc_Print( 1, "Round %3d:  ", r );
-//            Abc_PrintTime( 1, "Time", clock() - clk );
+//            Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
             Abc_Print( 1, "." );
         }
         // check timeout
-        if ( TimeOut && clock() > nTimeToStop )
+        if ( TimeOut && Abc_Clock() > nTimeToStop )
         {
             if ( fVerbose ) Abc_Print( 1, "\n" );
             Abc_Print( 1, "Reached timeout (%d seconds).\n",  TimeOut );
@@ -364,7 +364,7 @@ int Ssw_RarSimulate2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, i
     {
         if ( fVerbose ) Abc_Print( 1, "\n" );
         Abc_Print( 1, "Simulation did not assert POs in the first %d frames.  ", nRounds * nFrames );
-        Abc_PrintTime( 1, "Time", clock() - clkTotal );
+        Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
     }
     // cleanup
     Ssw_RarManStop( p );
@@ -388,8 +388,8 @@ int Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSiz
     int fMiter = 0;
     Ssw_RarMan_t * p;
     int r, i, k;
-    clock_t clkTotal = clock();
-    clock_t nTimeToStop = TimeOut ? TimeOut * CLOCKS_PER_SEC + clock(): 0;
+    abctime clkTotal = Abc_Clock();
+    abctime nTimeToStop = TimeOut ? TimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0;
     int RetValue = -1;
     assert( Aig_ManRegNum(pAig) > 0 );
     assert( Aig_ManConstrNum(pAig) == 0 );
@@ -462,7 +462,7 @@ int Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSiz
         Ssw_RarTransferPatterns( p, p->vInits );
         Ssw_SmlInitializeSpecial( p->pSml, p->vInits );
         // check timeout
-        if ( TimeOut && clock() > nTimeToStop )
+        if ( TimeOut && Abc_Clock() > nTimeToStop )
         {
             if ( fVerbose ) Abc_Print( 1, "\n" );
             Abc_Print( 1, "Reached timeout (%d seconds).\n",  TimeOut );
@@ -472,7 +472,7 @@ int Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSiz
     if ( r == nRounds )
     {
         Abc_Print( 1, "Simulation did not assert POs in the first %d frames.  ", nRounds * nFrames );
-        Abc_PrintTime( 1, "Time", clock() - clkTotal );
+        Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
     }
     // cleanup
     Ssw_RarManStop( p );
diff --git a/src/proof/ssw/sswSat.c b/src/proof/ssw/sswSat.c
index e5971a64..59ed6945 100644
--- a/src/proof/ssw/sswSat.c
+++ b/src/proof/ssw/sswSat.c
@@ -46,7 +46,7 @@ int Ssw_NodesAreEquiv( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
 {
     int nBTLimit = p->pPars->nBTLimit;
     int pLits[3], nLits, RetValue, RetValue1;
-    clock_t clk;//, status;
+    abctime clk;//, status;
     p->nSatCalls++;
     p->pMSat->nSolverCalls++;
 
@@ -80,13 +80,13 @@ int Ssw_NodesAreEquiv( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
         assert( RetValue != 0 );
     }
 
-clk = clock();
+clk = Abc_Clock();
     RetValue1 = sat_solver_solve( p->pMSat->pSat, pLits, pLits + nLits, 
         (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
-p->timeSat += clock() - clk;
+p->timeSat += Abc_Clock() - clk;
     if ( RetValue1 == l_False )
     {
-p->timeSatUnsat += clock() - clk;
+p->timeSatUnsat += Abc_Clock() - clk;
         if ( nLits == 2 )
         {
             pLits[0] = lit_neg( pLits[0] );
@@ -105,13 +105,13 @@ p->timeSatUnsat += clock() - clk;
     }
     else if ( RetValue1 == l_True )
     {
-p->timeSatSat += clock() - clk;
+p->timeSatSat += Abc_Clock() - clk;
         p->nSatCallsSat++;
         return 0;
     }
     else // if ( RetValue1 == l_Undef )
     {
-p->timeSatUndec += clock() - clk;
+p->timeSatUndec += Abc_Clock() - clk;
         p->nSatFailsReal++;
         return -1;
     }
@@ -142,13 +142,13 @@ p->timeSatUndec += clock() - clk;
         assert( RetValue != 0 );
     }
 
-clk = clock();
+clk = Abc_Clock();
     RetValue1 = sat_solver_solve( p->pMSat->pSat, pLits, pLits + nLits, 
         (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
-p->timeSat += clock() - clk;
+p->timeSat += Abc_Clock() - clk;
     if ( RetValue1 == l_False )
     {
-p->timeSatUnsat += clock() - clk;
+p->timeSatUnsat += Abc_Clock() - clk;
         if ( nLits == 2 )
         {
             pLits[0] = lit_neg( pLits[0] );
@@ -167,13 +167,13 @@ p->timeSatUnsat += clock() - clk;
     }
     else if ( RetValue1 == l_True )
     {
-p->timeSatSat += clock() - clk;
+p->timeSatSat += Abc_Clock() - clk;
         p->nSatCallsSat++;
         return 0;
     }
     else // if ( RetValue1 == l_Undef )
     {
-p->timeSatUndec += clock() - clk;
+p->timeSatUndec += Abc_Clock() - clk;
         p->nSatFailsReal++;
         return -1;
     }
diff --git a/src/proof/ssw/sswSemi.c b/src/proof/ssw/sswSemi.c
index 822f63f5..d5af1394 100644
--- a/src/proof/ssw/sswSemi.c
+++ b/src/proof/ssw/sswSemi.c
@@ -180,8 +180,8 @@ int Ssw_ManFilterBmc( Ssw_Sem_t * pBmc, int iPat, int fCheckTargets )
     Aig_Obj_t * pObj, * pObjNew, * pObjLi, * pObjLo;
     unsigned * pInfo;
     int i, f, RetValue, fFirst = 0;
-    clock_t clk;
-clk = clock();
+    abctime clk;
+clk = Abc_Clock();
 
     // start initialized timeframes
     p->pFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * 3 );
@@ -243,7 +243,7 @@ clk = clock();
 
     // cleanup
     Ssw_ClassesCheck( p->ppClasses );
-p->timeBmc += clock() - clk;
+p->timeBmc += Abc_Clock() - clk;
     return RetValue;
 }
 
@@ -262,7 +262,7 @@ int Ssw_FilterUsingSemi( Ssw_Man_t * pMan, int fCheckTargets, int nConfMax, int
 {
     Ssw_Sem_t * p;
     int RetValue, Frames, Iter;
-    clock_t clk = clock();
+    abctime clk = Abc_Clock();
     p = Ssw_SemManStart( pMan, nConfMax, fVerbose );
     if ( fCheckTargets && Ssw_SemCheckTargets( p ) )
     {
@@ -279,7 +279,7 @@ int Ssw_FilterUsingSemi( Ssw_Man_t * pMan, int fCheckTargets, int nConfMax, int
     RetValue = 0;
     for ( Iter = 0; Iter < p->nPatterns; Iter++ )
     {
-clk = clock();
+clk = Abc_Clock();
         pMan->pMSat = Ssw_SatStart( 0 );
         Frames = Ssw_ManFilterBmc( p, Iter, fCheckTargets );
         if ( fVerbose )
@@ -288,7 +288,7 @@ clk = clock();
                 Iter, Ssw_ClassesCand1Num(p->pMan->ppClasses), Ssw_ClassesClassNum(p->pMan->ppClasses),
                 Aig_ManNodeNum(p->pMan->pFrames), Frames, (int)p->pMan->pMSat->pSat->stats.conflicts, p->nPatterns,
                 p->pMan->nSatFailsReal? "f" : " " );
-            ABC_PRT( "T", clock() - clk );
+            ABC_PRT( "T", Abc_Clock() - clk );
         }
         Ssw_ManCleanup( p->pMan );
         if ( fCheckTargets && Ssw_SemCheckTargets( p ) )
diff --git a/src/proof/ssw/sswSim.c b/src/proof/ssw/sswSim.c
index 469af654..c458855d 100644
--- a/src/proof/ssw/sswSim.c
+++ b/src/proof/ssw/sswSim.c
@@ -38,7 +38,7 @@ struct Ssw_Sml_t_
     int              nWordsPref;        // the number of word in the prefix
     int              fNonConstOut;      // have seen a non-const-0 output during simulation
     int              nSimRounds;        // statistics
-    clock_t          timeSim;           // statistics
+    abctime          timeSim;           // statistics
     unsigned         pData[0];          // simulation data for the nodes
 };
 
@@ -1006,8 +1006,8 @@ void Ssw_SmlSimulateOne( Ssw_Sml_t * p )
 {
     Aig_Obj_t * pObj, * pObjLi, * pObjLo;
     int f, i;
-    clock_t clk;
-clk = clock();
+    abctime clk;
+clk = Abc_Clock();
     for ( f = 0; f < p->nFrames; f++ )
     {
         // simulate the nodes
@@ -1026,7 +1026,7 @@ clk = clock();
         Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
             Ssw_SmlNodeTransferNext( p, pObjLi, pObjLo, f );
     }
-p->timeSim += clock() - clk;
+p->timeSim += Abc_Clock() - clk;
 p->nSimRounds++;
 }
 
@@ -1118,8 +1118,8 @@ void Ssw_SmlSimulateOneFrame( Ssw_Sml_t * p )
 {
     Aig_Obj_t * pObj, * pObjLi, * pObjLo;
     int i;
-    clock_t clk;
-clk = clock();
+    abctime clk;
+clk = Abc_Clock();
     // simulate the nodes
     Aig_ManForEachNode( p->pAig, pObj, i )
         Ssw_SmlNodeSimulate( p, pObj, 0 );
@@ -1129,7 +1129,7 @@ clk = clock();
     // copy simulation info into the inputs
     Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
         Ssw_SmlNodeTransferNext( p, pObjLi, pObjLo, 0 );
-p->timeSim += clock() - clk;
+p->timeSim += Abc_Clock() - clk;
 p->nSimRounds++;
 }
 
diff --git a/src/proof/ssw/sswSimSat.c b/src/proof/ssw/sswSimSat.c
index 6e5944d1..74c65c00 100644
--- a/src/proof/ssw/sswSimSat.c
+++ b/src/proof/ssw/sswSimSat.c
@@ -46,7 +46,7 @@ void Ssw_ManResimulateBit( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pRepr )
 {
     Aig_Obj_t * pObj;
     int i, RetValue1, RetValue2;
-    clock_t clk = clock();
+    abctime clk = Abc_Clock();
     // set the PI simulation information
     Aig_ManConst1(p->pAig)->fMarkB = 1;
     Aig_ManForEachCi( p->pAig, pObj, i )
@@ -75,7 +75,7 @@ void Ssw_ManResimulateBit( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pRepr )
                 Abc_Print( 1, "\nSsw_ManResimulateBit() Error: RetValue2 does not hold.\n" );
         }
     }
-p->timeSimSat += clock() - clk;
+p->timeSimSat += Abc_Clock() - clk;
 }
 
 /**Function*************************************************************
@@ -92,7 +92,7 @@ p->timeSimSat += clock() - clk;
 void Ssw_ManResimulateWord( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pRepr, int f )
 {
     int RetValue1, RetValue2;
-    clock_t clk = clock();
+    abctime clk = Abc_Clock();
     // set the PI simulation information
     Ssw_SmlAssignDist1Plus( p->pSml, p->pPatWords );
     // simulate internal nodes
@@ -113,7 +113,7 @@ void Ssw_ManResimulateWord( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pRepr,
         if ( RetValue2 == 0 )
             Abc_Print( 1, "\nSsw_ManResimulateWord() Error: RetValue2 does not hold.\n" );
     }
-p->timeSimSat += clock() - clk;
+p->timeSimSat += Abc_Clock() - clk;
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/proof/ssw/sswSweep.c b/src/proof/ssw/sswSweep.c
index bccc6aa4..6db673cc 100644
--- a/src/proof/ssw/sswSweep.c
+++ b/src/proof/ssw/sswSweep.c
@@ -188,7 +188,7 @@ int Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc, Vec_Int_
 {
     Aig_Obj_t * pObjRepr, * pObjFraig, * pObjFraig2, * pObjReprFraig;
     int RetValue;
-    clock_t clk;
+    abctime clk;
     // get representative of this class
     pObjRepr = Aig_ObjRepr( p->pAig, pObj );
     if ( pObjRepr == NULL )
@@ -206,10 +206,10 @@ int Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc, Vec_Int_
     // add constraints on demand
     if ( !fBmc && p->pPars->fDynamic )
     {
-clk = clock();
+clk = Abc_Clock();
         Ssw_ManLoadSolver( p, pObjRepr, pObj );
         p->nRecycleCalls++;
-p->timeMarkCones += clock() - clk;
+p->timeMarkCones += Abc_Clock() - clk;
     }
     // call equivalence checking
     if ( Aig_Regular(pObjFraig) != Aig_ManConst1(p->pFrames) )
@@ -269,8 +269,8 @@ int Ssw_ManSweepBmc( Ssw_Man_t * p )
     Bar_Progress_t * pProgress = NULL;
     Aig_Obj_t * pObj, * pObjNew, * pObjLi, * pObjLo;
     int i, f;
-    clock_t clk;
-clk = clock();
+    abctime clk;
+clk = Abc_Clock();
 
     // start initialized timeframes
     p->pFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * p->pPars->nFramesK );
@@ -315,7 +315,7 @@ clk = clock();
 
     // cleanup
 //    Ssw_ClassesCheck( p->ppClasses );
-p->timeBmc += clock() - clk;
+p->timeBmc += Abc_Clock() - clk;
     return p->fRefined;
 }
 
@@ -368,11 +368,11 @@ int Ssw_ManSweep( Ssw_Man_t * p )
     Bar_Progress_t * pProgress = NULL;
     Aig_Obj_t * pObj, * pObj2, * pObjNew;
     int nConstrPairs, i, f;
-    clock_t clk;
+    abctime clk;
     Vec_Int_t * vDisproved;
 
     // perform speculative reduction
-clk = clock();
+clk = Abc_Clock();
     // create timeframes
     p->pFrames = Ssw_FramesWithClasses( p );
     // add constants
@@ -397,7 +397,7 @@ clk = clock();
     Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) );
     Saig_ManForEachPi( p->pAig, pObj, i )
         Ssw_ObjSetFrame( p, pObj, f, Aig_ObjCreateCi(p->pFrames) );
-p->timeReduce += clock() - clk;
+p->timeReduce += Abc_Clock() - clk;
 
     // sweep internal nodes
     p->fRefined = 0;