Fixing time primtouts throughout the code.

5 files changed, 18 insertions, 15 deletions

diff --git a/src/proof/dch/dch.h b/src/proof/dch/dch.h
index 731eb776..ff29f0da 100644
--- a/src/proof/dch/dch.h
+++ b/src/proof/dch/dch.h
@@ -54,7 +54,7 @@ struct Dch_Pars_t_
     int              fUseCSat;      // uses circuit-based solver
     int              fLightSynth;   // uses lighter version of synthesis
     int              fVerbose;      // verbose stats
-    int              timeSynth;     // synthesis runtime
+    clock_t          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 bc78682b..bfef8d8c 100644
--- a/src/proof/dch/dchCore.c
+++ b/src/proof/dch/dchCore.c
@@ -89,7 +89,7 @@ Aig_Man_t * Dch_ComputeChoices( Aig_Man_t * pAig, Dch_Pars_t * pPars )
 {
     Dch_Man_t * p;
     Aig_Man_t * pResult;
-    int clk, clkTotal = clock();
+    clock_t clk, clkTotal = clock();
     // reset random numbers
     Aig_ManRandom(1);
     // start the choicing manager
@@ -131,7 +131,7 @@ p->timeTotal = clock() - clkTotal;
 void Dch_ComputeEquivalences( Aig_Man_t * pAig, Dch_Pars_t * pPars )
 {
     Dch_Man_t * p;
-    int clk, clkTotal = clock();
+    clock_t clk, clkTotal = clock();
     // reset random numbers
     Aig_ManRandom(1);
     // start the choicing manager
diff --git a/src/proof/dch/dchInt.h b/src/proof/dch/dchInt.h
index c9f2f4f6..b22834cf 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
-    int              timeSimInit;    // simulation and class computation
-    int              timeSimSat;     // simulation of the counter-examples
-    int              timeSat;        // solving SAT
-    int              timeSatSat;     // sat
-    int              timeSatUnsat;   // unsat
-    int              timeSatUndec;   // undecided
-    int              timeChoice;     // choice computation
-    int              timeOther;      // other runtime
-    int              timeTotal;      // total runtime
+    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
 };
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/proof/dch/dchSat.c b/src/proof/dch/dchSat.c
index f5e346ef..fefd5ce2 100644
--- a/src/proof/dch/dchSat.c
+++ b/src/proof/dch/dchSat.c
@@ -45,7 +45,8 @@ ABC_NAMESPACE_IMPL_START
 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, clk;
+    int pLits[2], RetValue, RetValue1, status;
+    clock_t clk;
     p->nSatCalls++;
 
     // sanity checks
diff --git a/src/proof/dch/dchSimSat.c b/src/proof/dch/dchSimSat.c
index 6f69b47e..26de4643 100644
--- a/src/proof/dch/dchSimSat.c
+++ b/src/proof/dch/dchSimSat.c
@@ -177,7 +177,8 @@ void Dch_ManResimulateOther_rec( Dch_Man_t * p, Aig_Obj_t * pObj )
 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, clk = clock();
+    int i, k, nSize, RetValue1, RetValue2;
+    clock_t clk = clock();
     // get the equivalence classes
     Dch_ManCollectTfoCands( p, pObj, pRepr );
     // resimulate the cone of influence of the solved nodes
@@ -224,7 +225,8 @@ p->timeSimSat += clock() - clk;
 void Dch_ManResimulateCex2( Dch_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr )
 {
     Aig_Obj_t * pRoot;
-    int i, RetValue, clk = clock();
+    int i, RetValue;
+    clock_t clk = clock();
     // get the equivalence class
     if ( Dch_ObjIsConst1Cand(p->pAigTotal, pObj) )
         Dch_ClassesCollectConst1Group( p->ppClasses, pObj, 500, p->vSimRoots );