5 files changed, 33 insertions, 33 deletions

diff --git a/src/proof/dch/dch.h b/src/proof/dch/dch.h
index e887ba26..5d644643 100644
--- a/src/proof/dch/dch.h
+++ b/src/proof/dch/dch.h
@@ -55,7 +55,7 @@ struct Dch_Pars_t_
     int              fLightSynth;   // uses lighter version of synthesis
     int              fSkipRedSupp;  // skip choices with redundant support vars
     int              fVerbose;      // verbose stats
-    clock_t          timeSynth;     // synthesis runtime
+    abctime          timeSynth;     // synthesis runtime
     int              nNodesAhead;   // the lookahead in terms of nodes
     int              nCallsRecycle; // calls to perform before recycling SAT solver
 };
diff --git a/src/proof/dch/dchCore.c b/src/proof/dch/dchCore.c
index b92de8a6..0da65bee 100644
--- a/src/proof/dch/dchCore.c
+++ b/src/proof/dch/dchCore.c
@@ -90,21 +90,21 @@ Aig_Man_t * Dch_ComputeChoices( Aig_Man_t * pAig, Dch_Pars_t * pPars )
 {
     Dch_Man_t * p;
     Aig_Man_t * pResult;
-    clock_t clk, clkTotal = clock();
+    abctime clk, clkTotal = Abc_Clock();
     // reset random numbers
     Aig_ManRandom(1);
     // start the choicing manager
     p = Dch_ManCreate( pAig, pPars );
     // compute candidate equivalence classes
-clk = clock(); 
+clk = Abc_Clock(); 
     p->ppClasses = Dch_CreateCandEquivClasses( pAig, pPars->nWords, pPars->fVerbose );
-p->timeSimInit = clock() - clk;
+p->timeSimInit = Abc_Clock() - clk;
 //    Dch_ClassesPrint( p->ppClasses, 0 );
     p->nLits = Dch_ClassesLitNum( p->ppClasses );
     // perform SAT sweeping
     Dch_ManSweep( p );
     // free memory ahead of time
-p->timeTotal = clock() - clkTotal;
+p->timeTotal = Abc_Clock() - clkTotal;
     Dch_ManStop( p );
     // create choices
     ABC_FREE( pAig->pTable );
@@ -134,21 +134,21 @@ p->timeTotal = clock() - clkTotal;
 void Dch_ComputeEquivalences( Aig_Man_t * pAig, Dch_Pars_t * pPars )
 {
     Dch_Man_t * p;
-    clock_t clk, clkTotal = clock();
+    abctime clk, clkTotal = Abc_Clock();
     // reset random numbers
     Aig_ManRandom(1);
     // start the choicing manager
     p = Dch_ManCreate( pAig, pPars );
     // compute candidate equivalence classes
-clk = clock(); 
+clk = Abc_Clock(); 
     p->ppClasses = Dch_CreateCandEquivClasses( pAig, pPars->nWords, pPars->fVerbose );
-p->timeSimInit = clock() - clk;
+p->timeSimInit = Abc_Clock() - clk;
 //    Dch_ClassesPrint( p->ppClasses, 0 );
     p->nLits = Dch_ClassesLitNum( p->ppClasses );
     // perform SAT sweeping
     Dch_ManSweep( p );
     // free memory ahead of time
-p->timeTotal = clock() - clkTotal;
+p->timeTotal = Abc_Clock() - clkTotal;
     Dch_ManStop( p );
 }
 
diff --git a/src/proof/dch/dchInt.h b/src/proof/dch/dchInt.h
index d1dd2c51..7edbc0f9 100644
--- a/src/proof/dch/dchInt.h
+++ b/src/proof/dch/dchInt.h
@@ -84,15 +84,15 @@ struct Dch_Man_t_
     int              nEquivs;        // the number of final equivalences
     int              nChoices;       // the number of final choice nodes
     // runtime stats
-    clock_t          timeSimInit;    // simulation and class computation
-    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          timeChoice;     // choice computation
-    clock_t          timeOther;      // other runtime
-    clock_t          timeTotal;      // total runtime
+    abctime          timeSimInit;    // simulation and class computation
+    abctime          timeSimSat;     // simulation of the counter-examples
+    abctime          timeSat;        // solving SAT
+    abctime          timeSatSat;     // sat
+    abctime          timeSatUnsat;   // unsat
+    abctime          timeSatUndec;   // undecided
+    abctime          timeChoice;     // choice computation
+    abctime          timeOther;      // other runtime
+    abctime          timeTotal;      // total runtime
 };
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/proof/dch/dchSat.c b/src/proof/dch/dchSat.c
index fefd5ce2..9da18564 100644
--- a/src/proof/dch/dchSat.c
+++ b/src/proof/dch/dchSat.c
@@ -46,7 +46,7 @@ int Dch_NodesAreEquiv( Dch_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
 {
     int nBTLimit = p->pPars->nBTLimit;
     int pLits[2], RetValue, RetValue1, status;
-    clock_t clk;
+    abctime clk;
     p->nSatCalls++;
 
     // sanity checks
@@ -85,13 +85,13 @@ int Dch_NodesAreEquiv( Dch_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
         if ( pNew->fPhase )  pLits[1] = lit_neg( pLits[1] );
     }
 //Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 );
-clk = clock();
+clk = Abc_Clock();
     RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2, 
         (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
-p->timeSat += clock() - clk;
+p->timeSat += Abc_Clock() - clk;
     if ( RetValue1 == l_False )
     {
-p->timeSatUnsat += clock() - clk;
+p->timeSatUnsat += Abc_Clock() - clk;
         pLits[0] = lit_neg( pLits[0] );
         pLits[1] = lit_neg( pLits[1] );
         RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
@@ -100,13 +100,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;
     }
@@ -127,13 +127,13 @@ p->timeSatUndec += clock() - clk;
         if ( pOld->fPhase )  pLits[0] = lit_neg( pLits[0] );
         if ( pNew->fPhase )  pLits[1] = lit_neg( pLits[1] );
     }
-clk = clock();
+clk = Abc_Clock();
     RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2, 
         (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
-p->timeSat += clock() - clk;
+p->timeSat += Abc_Clock() - clk;
     if ( RetValue1 == l_False )
     {
-p->timeSatUnsat += clock() - clk;
+p->timeSatUnsat += Abc_Clock() - clk;
         pLits[0] = lit_neg( pLits[0] );
         pLits[1] = lit_neg( pLits[1] );
         RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
@@ -142,13 +142,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/dch/dchSimSat.c b/src/proof/dch/dchSimSat.c
index 26de4643..d3dbbe16 100644
--- a/src/proof/dch/dchSimSat.c
+++ b/src/proof/dch/dchSimSat.c
@@ -178,7 +178,7 @@ void Dch_ManResimulateCex( Dch_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr )
 {
     Aig_Obj_t * pRoot, ** ppClass;
     int i, k, nSize, RetValue1, RetValue2;
-    clock_t clk = clock();
+    abctime clk = Abc_Clock();
     // get the equivalence classes
     Dch_ManCollectTfoCands( p, pObj, pRepr );
     // resimulate the cone of influence of the solved nodes
@@ -208,7 +208,7 @@ void Dch_ManResimulateCex( Dch_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr )
         assert( RetValue1 );
     else
         assert( RetValue2 );
-p->timeSimSat += clock() - clk;
+p->timeSimSat += Abc_Clock() - clk;
 }
 
 /**Function*************************************************************
@@ -226,7 +226,7 @@ void Dch_ManResimulateCex2( Dch_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr )
 {
     Aig_Obj_t * pRoot;
     int i, RetValue;
-    clock_t clk = clock();
+    abctime clk = Abc_Clock();
     // get the equivalence class
     if ( Dch_ObjIsConst1Cand(p->pAigTotal, pObj) )
         Dch_ClassesCollectConst1Group( p->ppClasses, pObj, 500, p->vSimRoots );
@@ -248,7 +248,7 @@ void Dch_ManResimulateCex2( Dch_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr )
     else
         RetValue = Dch_ClassesRefineOneClass( p->ppClasses, pRepr, 0 );
     assert( RetValue );
-p->timeSimSat += clock() - clk;
+p->timeSimSat += Abc_Clock() - clk;
 }
 
 ////////////////////////////////////////////////////////////////////////