Fixing time primtouts throughout the code.

51 files changed, 211 insertions, 177 deletions

diff --git a/src/opt/cgt/cgtCore.c b/src/opt/cgt/cgtCore.c
index 73195413..82f4e105 100644
--- a/src/opt/cgt/cgtCore.c
+++ b/src/opt/cgt/cgtCore.c
@@ -200,7 +200,8 @@ void Cgt_ClockGatingRangeCheck( Cgt_Man_t * p, int iStart, int nOutputs )
 ***********************************************************************/
 int Cgt_ClockGatingRange( Cgt_Man_t * p, int iStart )
 {
-    int nOutputs, iStop, clk, clkTotal = clock();
+    int nOutputs, iStop;
+    clock_t clk, clkTotal = clock();
     int nCallsUnsat    = p->nCallsUnsat;
     int nCallsSat      = p->nCallsSat;
     int nCallsUndec    = p->nCallsUndec;
@@ -247,7 +248,8 @@ Vec_Vec_t * Cgt_ClockGatingCandidates( Aig_Man_t * pAig, Aig_Man_t * pCare, Cgt_
     Cgt_Par_t Pars; 
     Cgt_Man_t * p;
     Vec_Vec_t * vGatesAll;
-    int iStart, clk = clock(), clkTotal = clock();
+    int iStart;
+    clock_t clk = clock(), clkTotal = clock();
     // reset random numbers
     Aig_ManRandom( 1 );
     if ( pPars == NULL )
diff --git a/src/opt/cgt/cgtDecide.c b/src/opt/cgt/cgtDecide.c
index c5b49bbc..4e4a57b1 100644
--- a/src/opt/cgt/cgtDecide.c
+++ b/src/opt/cgt/cgtDecide.c
@@ -192,7 +192,8 @@ Vec_Vec_t * Cgt_ManDecideSimple( Aig_Man_t * pAig, Vec_Vec_t * vGatesAll, int nO
     Vec_Vec_t * vGates;
     Vec_Ptr_t * vCands;
     Aig_Obj_t * pObjLi, * pObjLo, * pCand, * pCandBest;
-    int i, k, nHitsCur, nHitsMax, Counter = 0, clk = clock();
+    int i, k, nHitsCur, nHitsMax, Counter = 0;
+    clock_t clk = clock();
     int nTransTotal = 0, nTransSaved = 0;
     vGates = Vec_VecStart( Saig_ManRegNum(pAig) );
     pSml = Ssw_SmlSimulateSeq( pAig, 0, nFrames, nWords );
@@ -259,7 +260,8 @@ Vec_Vec_t * Cgt_ManDecideArea( Aig_Man_t * pAig, Vec_Vec_t * vGatesAll, int nOdc
     Vec_Vec_t * vGates;
     Vec_Ptr_t * vCompletes, * vOne;
     Aig_Obj_t * pGate;
-    int i, k, Counter = 0, clk = clock();
+    int i, k, Counter = 0;
+    clock_t clk = clock();
     // derive and label complete gates
     vCompletes = Cgt_ManCompleteGates( pAig, vGatesAll, nOdcMax, fVerbose );
     // label complete gates
diff --git a/src/opt/cgt/cgtInt.h b/src/opt/cgt/cgtInt.h
index 1fdbf35f..78c27224 100644
--- a/src/opt/cgt/cgtInt.h
+++ b/src/opt/cgt/cgtInt.h
@@ -74,15 +74,15 @@ struct Cgt_Man_t_
     int          nCallsUnsat;    // unsatisfiable calls  
     int          nCallsUndec;    // undecided calls
     int          nCallsFiltered; // filtered out calls
-    int          timeAig;        // constructing AIG
-    int          timePrepare;    // partitioning and SAT solving
-    int          timeSat;        // total runtime
-    int          timeSatSat;     // satisfiable runtime 
-    int          timeSatUnsat;   // unsatisfiable runtime 
-    int          timeSatUndec;   // undecided runtime
-    int          timeDecision;   // making decision about what gates to use
-    int          timeOther;      // other runtime
-    int          timeTotal;      // total runtime
+    clock_t      timeAig;        // constructing AIG
+    clock_t      timePrepare;    // partitioning and SAT solving
+    clock_t      timeSat;        // total runtime
+    clock_t      timeSatSat;     // satisfiable runtime 
+    clock_t      timeSatUnsat;   // unsatisfiable runtime 
+    clock_t      timeSatUndec;   // undecided runtime
+    clock_t      timeDecision;   // making decision about what gates to use
+    clock_t      timeOther;      // other runtime
+    clock_t      timeTotal;      // total runtime
 };
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/cgt/cgtSat.c b/src/opt/cgt/cgtSat.c
index 0a2a1daa..b6d3c599 100644
--- a/src/opt/cgt/cgtSat.c
+++ b/src/opt/cgt/cgtSat.c
@@ -46,7 +46,8 @@ ABC_NAMESPACE_IMPL_START
 int Cgt_CheckImplication( Cgt_Man_t * p, Aig_Obj_t * pGate, Aig_Obj_t * pMiter )
 {
     int nBTLimit = p->pPars->nConfMax;
-    int pLits[2], RetValue, clk;
+    int pLits[2], RetValue;
+    clock_t clk;
     p->nCalls++;
 
     // sanity checks
diff --git a/src/opt/csw/cswCore.c b/src/opt/csw/cswCore.c
index f1c2d934..3702b346 100644
--- a/src/opt/csw/cswCore.c
+++ b/src/opt/csw/cswCore.c
@@ -47,7 +47,8 @@ Aig_Man_t * Csw_Sweep( Aig_Man_t * pAig, int nCutsMax, int nLeafMax, int fVerbos
     Csw_Man_t * p;
     Aig_Man_t * pRes;
     Aig_Obj_t * pObj, * pObjNew, * pObjRes;
-    int i, clk;
+    int i;
+    clock_t clk;
 clk = clock();
     // start the manager
     p = Csw_ManStart( pAig, nCutsMax, nLeafMax, fVerbose );
diff --git a/src/opt/csw/cswCut.c b/src/opt/csw/cswCut.c
index bb6677c2..0b1d9254 100644
--- a/src/opt/csw/cswCut.c
+++ b/src/opt/csw/cswCut.c
@@ -497,7 +497,8 @@ Aig_Obj_t * Csw_ObjSweep( Csw_Man_t * p, Aig_Obj_t * pObj, int fTriv )
     Aig_Obj_t * pFanin1 = Aig_ObjFanin1(pObj);
     Aig_Obj_t * pObjNew;
     unsigned * pTruth;
-    int i, k, nVars, nFanins, iVar, clk;
+    int i, k, nVars, nFanins, iVar;
+    clock_t clk;
 
     assert( !Aig_IsComplement(pObj) );
     if ( !Aig_ObjIsNode(pObj) )
diff --git a/src/opt/csw/cswInt.h b/src/opt/csw/cswInt.h
index e6c10b36..65228fcd 100644
--- a/src/opt/csw/cswInt.h
+++ b/src/opt/csw/cswInt.h
@@ -30,7 +30,6 @@
 #include <stdlib.h>
 #include <string.h>
 #include <assert.h>
-#include <time.h>
 
 #include "src/aig/aig/aig.h"
 #include "src/opt/dar/dar.h"
@@ -94,10 +93,10 @@ struct Csw_Man_t_
     int             nNodesTriv2;     // the number of trivial nodes
     int             nNodesCuts;      // the number of rewritten nodes
     int             nNodesTried;     // the number of nodes tried
-    int             timeCuts;        // time to compute the cut and its truth table
-    int             timeHash;        // time for hashing cuts
-    int             timeOther;       // other time
-    int             timeTotal;       // total time
+    clock_t         timeCuts;        // time to compute the cut and its truth table
+    clock_t         timeHash;        // time for hashing cuts
+    clock_t         timeOther;       // other time
+    clock_t         timeTotal;       // total time
 };
 
 static inline int          Csw_CutLeaveNum( Csw_Cut_t * pCut )          { return pCut->nFanins;                                   }
diff --git a/src/opt/cut/cut.h b/src/opt/cut/cut.h
index cd87e5a0..64d3108a 100644
--- a/src/opt/cut/cut.h
+++ b/src/opt/cut/cut.h
@@ -124,7 +124,7 @@ extern int              Cut_CutCountList( Cut_Cut_t * pList );
 extern Cut_Man_t *      Cut_ManStart( Cut_Params_t * pParams );
 extern void             Cut_ManStop( Cut_Man_t * p );
 extern void             Cut_ManPrintStats( Cut_Man_t * p );
-extern void             Cut_ManPrintStatsToFile( Cut_Man_t * p, char * pFileName, int TimeTotal );
+extern void             Cut_ManPrintStatsToFile( Cut_Man_t * p, char * pFileName, clock_t TimeTotal );
 extern void             Cut_ManSetFanoutCounts( Cut_Man_t * p, Vec_Int_t * vFanCounts );
 extern void             Cut_ManSetNodeAttrs( Cut_Man_t * p, Vec_Int_t * vFanCounts );
 extern int              Cut_ManReadVarsMax( Cut_Man_t * p );
diff --git a/src/opt/cut/cutInt.h b/src/opt/cut/cutInt.h
index 39606b00..a66a5786 100644
--- a/src/opt/cut/cutInt.h
+++ b/src/opt/cut/cutInt.h
@@ -92,12 +92,12 @@ struct Cut_ManStruct_t_
     int                nNodesDag;
     int                nNodesNoCuts;
     // runtime
-    int                timeMerge;
-    int                timeUnion;
-    int                timeTruth;
-    int                timeFilter;
-    int                timeHash;
-    int                timeMap;
+    clock_t            timeMerge;
+    clock_t            timeUnion;
+    clock_t            timeTruth;
+    clock_t            timeFilter;
+    clock_t            timeHash;
+    clock_t            timeMap;
 };
 
 // iterator through all the cuts of the list
diff --git a/src/opt/cut/cutMan.c b/src/opt/cut/cutMan.c
index 4a9f8f4b..12c65935 100644
--- a/src/opt/cut/cutMan.c
+++ b/src/opt/cut/cutMan.c
@@ -201,7 +201,7 @@ void Cut_ManPrintStats( Cut_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Cut_ManPrintStatsToFile( Cut_Man_t * p, char * pFileName, int TimeTotal )
+void Cut_ManPrintStatsToFile( Cut_Man_t * p, char * pFileName, clock_t TimeTotal )
 {
     FILE * pTable;
     pTable = fopen( "cut_stats.txt", "a+" );
diff --git a/src/opt/cut/cutNode.c b/src/opt/cut/cutNode.c
index 010e1e00..4f94011a 100644
--- a/src/opt/cut/cutNode.c
+++ b/src/opt/cut/cutNode.c
@@ -370,7 +370,7 @@ Cut_Cut_t * Cut_NodeComputeCuts( Cut_Man_t * p, int Node, int Node0, int Node1,
 {
     Cut_List_t Super, * pSuper = &Super;
     Cut_Cut_t * pList, * pCut;
-    int clk;
+    clock_t clk;
     // start the number of cuts at the node
     p->nNodes++;
     p->nNodeCuts = 0;
@@ -681,7 +681,7 @@ Cut_Cut_t * Cut_NodeUnionCuts( Cut_Man_t * p, Vec_Int_t * vNodes )
     Cut_Cut_t * pList, * pListStart, * pCut, * pCut2;
     Cut_Cut_t * pTop = NULL; // Suppress "might be used uninitialized"
     int i, k, Node, Root, Limit = p->pParams->nVarsMax;
-    int clk = clock();
+    clock_t clk = clock();
 
     // start the new list
     Cut_ListStart( pSuper );
@@ -797,7 +797,7 @@ Cut_Cut_t * Cut_NodeUnionCutsSeq( Cut_Man_t * p, Vec_Int_t * vNodes, int CutSetN
     Cut_List_t Super, * pSuper = &Super;
     Cut_Cut_t * pList, * pListStart, * pCut, * pCut2, * pTop;
     int i, k, Node, Root, Limit = p->pParams->nVarsMax;
-    int clk = clock();
+    clock_t clk = clock();
 
     // start the new list
     Cut_ListStart( pSuper );
diff --git a/src/opt/cut/cutOracle.c b/src/opt/cut/cutOracle.c
index b26e7d5e..5b740da5 100644
--- a/src/opt/cut/cutOracle.c
+++ b/src/opt/cut/cutOracle.c
@@ -46,7 +46,7 @@ struct Cut_OracleStruct_t_
     int                EntrySize;
     int                nTruthWords;
     // stats
-    int                timeTotal;
+    clock_t            timeTotal;
     int                nCuts;
     int                nCutsTriv;
 };
@@ -322,7 +322,7 @@ Cut_Cut_t * Cut_OracleComputeCuts( Cut_Oracle_t * p, int Node, int Node0, int No
     Cut_Cut_t * pList = NULL, ** ppTail = &pList;
     Cut_Cut_t * pCut, * pCut0, * pCut1, * pList0, * pList1;
     int iCutStart, nCuts, i, Entry;
-    int clk = clock();
+    clock_t clk = clock();
 
     // get the cuts of the children
     pList0 = (Cut_Cut_t *)Vec_PtrEntry( p->vCutsNew, Node0 );
diff --git a/src/opt/cut/cutPre22.c b/src/opt/cut/cutPre22.c
index d51d9056..4e507fba 100644
--- a/src/opt/cut/cutPre22.c
+++ b/src/opt/cut/cutPre22.c
@@ -69,9 +69,9 @@ struct Cut_CMan_t_
     int                nVarCounts[CUT_CELL_MVAR+1];
     int                nSymGroups[CUT_CELL_MVAR+1];
     int                nSymGroupsE[CUT_CELL_MVAR+1];
-    int                timeCanon;
-    int                timeSupp;
-    int                timeTable;
+    clock_t            timeCanon;
+    clock_t            timeSupp;
+    clock_t            timeTable;
     int                nCellFound;
     int                nCellNotFound;
 };
@@ -234,7 +234,8 @@ void Cut_CellPrecompute()
 {
     Cut_CMan_t * p;
     Cut_Cell_t * pCell, * pTemp;
-    int i1, i2, i3, i, j, k, c, clk = clock(); //, clk2 = clock();
+    int i1, i2, i3, i, j, k, c;
+    clock_t clk = clock(); //, clk2 = clock();
 
     p = Cut_CManStart();
 
@@ -840,7 +841,7 @@ void Cut_CellDumpToFile()
     int NumUsed[10][5] = {{0}};
     int BoxUsed[22][5] = {{0}};
     int i, k, Counter;
-    int clk = clock();
+    clock_t clk = clock();
 
     if ( p == NULL )
     {
diff --git a/src/opt/cut/cutSeq.c b/src/opt/cut/cutSeq.c
index 3f671d24..e1df2c95 100644
--- a/src/opt/cut/cutSeq.c
+++ b/src/opt/cut/cutSeq.c
@@ -73,7 +73,7 @@ void Cut_NodeComputeCutsSeq( Cut_Man_t * p, int Node, int Node0, int Node1, int
 {
     Cut_List_t Super, * pSuper = &Super;
     Cut_Cut_t * pListNew;
-    int clk;
+    clock_t clk;
     
     // get the number of cuts at the node
     p->nNodeCuts = Cut_CutCountList( Cut_NodeReadCutsOld(p, Node) );
diff --git a/src/opt/dar/darCore.c b/src/opt/dar/darCore.c
index 958ab70a..ba945f77 100644
--- a/src/opt/dar/darCore.c
+++ b/src/opt/dar/darCore.c
@@ -83,7 +83,8 @@ int Dar_ManRewrite( Aig_Man_t * pAig, Dar_RwrPar_t * pPars )
     Dar_Cut_t * pCut;
     Aig_Obj_t * pObj, * pObjNew;
     int i, k, nNodesOld, nNodeBefore, nNodeAfter, Required;
-    int clk = 0, clkStart, Counter = 0;
+    clock_t clk = 0, clkStart;
+    int Counter = 0;
     int nMffcSize;//, nMffcGains[MAX_VAL+1][MAX_VAL+1] = {{0}};
     // prepare the library
     Dar_LibPrepare( pPars->nSubgMax ); 
@@ -287,7 +288,8 @@ Aig_MmFixed_t * Dar_ManComputeCuts( Aig_Man_t * pAig, int nCutsMax, int fSkipTtM
     Dar_RwrPar_t Pars, * pPars = &Pars; 
     Aig_Obj_t * pObj;
     Aig_MmFixed_t * pMemCuts;
-    int i, nNodes, clk = clock();
+    int i, nNodes;
+    clock_t clk = clock();
     // remove dangling nodes
     if ( (nNodes = Aig_ManCleanup( pAig )) )
     {
diff --git a/src/opt/dar/darInt.h b/src/opt/dar/darInt.h
index caea213c..6bf347e1 100644
--- a/src/opt/dar/darInt.h
+++ b/src/opt/dar/darInt.h
@@ -30,9 +30,7 @@
 #include <stdlib.h>
 #include <string.h>
 #include <assert.h>
-#include <time.h>
 
-//#include "bar.h"
 #include "src/misc/vec/vec.h"
 #include "src/aig/aig/aig.h"
 #include "dar.h"
@@ -98,12 +96,12 @@ struct Dar_Man_t_
     int              nCutsGood;      // good cuts
     int              nCutsSkipped;   // skipped bad cuts
     // timing statistics
-    int              timeCuts;
-    int              timeEval;
-    int              timeOther;
-    int              timeTotal;
-    int              time1;
-    int              time2;
+    clock_t          timeCuts;
+    clock_t          timeEval;
+    clock_t          timeOther;
+    clock_t          timeTotal;
+    clock_t          time1;
+    clock_t          time2;
 };
 
 static inline Dar_Cut_t *  Dar_ObjCuts( Aig_Obj_t * pObj )                         { return (Dar_Cut_t *)pObj->pData;    }
diff --git a/src/opt/dar/darLib.c b/src/opt/dar/darLib.c
index 41794d18..67a5f59e 100644
--- a/src/opt/dar/darLib.c
+++ b/src/opt/dar/darLib.c
@@ -920,8 +920,8 @@ void Dar_LibEval( Dar_Man_t * p, Aig_Obj_t * pRoot, Dar_Cut_t * pCut, int Requir
     int fTraining = 0;
     float PowerSaved, PowerAdded;
     Dar_LibObj_t * pObj;
-    int Out, k, Class, nNodesSaved, nNodesAdded, nNodesGained, clk;
-    clk = clock();
+    int Out, k, Class, nNodesSaved, nNodesAdded, nNodesGained;
+    clock_t clk = clock();
     if ( pCut->nLeaves != 4 )
         return;
     // check if the cut exits and assigns leaves and their levels
@@ -1188,8 +1188,8 @@ int Dar2_LibEval( Gia_Man_t * p, Vec_Int_t * vCutLits, unsigned uTruth, int fKee
     int p_ClassBest  = -1;
 //    int fTraining    =  0;
     Dar_LibObj_t * pObj;
-    int Out, k, Class, nNodesSaved, nNodesAdded, nNodesGained, clk;
-    clk = clock();
+    int Out, k, Class, nNodesSaved, nNodesAdded, nNodesGained;
+    clock_t clk = clock();
     assert( Vec_IntSize(vCutLits) == 4 );
     assert( (uTruth >> 16) == 0 );
     // check if the cut exits and assigns leaves and their levels
diff --git a/src/opt/dar/darRefact.c b/src/opt/dar/darRefact.c
index 0ff7c44f..dcfbeac7 100644
--- a/src/opt/dar/darRefact.c
+++ b/src/opt/dar/darRefact.c
@@ -61,10 +61,10 @@ struct Ref_Man_t_
     int              nCutsUsed;      // the number of rewriting steps
     int              nCutsTried;     // the number of cuts tries
     // timing statistics
-    int              timeCuts;
-    int              timeEval;
-    int              timeOther;
-    int              timeTotal;
+    clock_t          timeCuts;
+    clock_t          timeEval;
+    clock_t          timeOther;
+    clock_t          timeTotal;
 };
 
 ////////////////////////////////////////////////////////////////////////
@@ -500,7 +500,8 @@ int Dar_ManRefactor( Aig_Man_t * pAig, Dar_RefPar_t * pPars )
     Vec_Ptr_t * vCut, * vCut2;
     Aig_Obj_t * pObj, * pObjNew;
     int nNodesOld, nNodeBefore, nNodeAfter, nNodesSaved, nNodesSaved2;
-    int i, Required, nLevelMin, clkStart, clk;
+    int i, Required, nLevelMin;
+    clock_t clkStart, clk;
 
     // start the manager
     p = Dar_ManRefStart( pAig, pPars );
diff --git a/src/opt/dar/darScript.c b/src/opt/dar/darScript.c
index 5561908d..be67b212 100644
--- a/src/opt/dar/darScript.c
+++ b/src/opt/dar/darScript.c
@@ -398,7 +398,8 @@ Aig_Man_t * Dar_ManChoice( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int
 {
     Aig_Man_t * pMan, * pTemp;
     Vec_Ptr_t * vAigs;
-    int i, clk;
+    int i;
+    clock_t clk;
 
 clk = clock();
 //    vAigs = Dar_ManChoiceSynthesisExt();
@@ -802,7 +803,8 @@ Aig_Man_t * Dar_ManChoiceNewAig( Aig_Man_t * pAig, Dch_Pars_t * pPars )
     Vec_Ptr_t * vPios;
     void * pManTime;
     char * pName, * pSpec;
-    int i, clk;
+    int i;
+    clock_t clk;
 
 clk = clock();
     vAigs = Dar_ManChoiceSynthesis( pAig, 1, 1, pPars->fPower, fVerbose );
@@ -873,7 +875,7 @@ Aig_Man_t * Dar_ManChoiceNew( Aig_Man_t * pAig, Dch_Pars_t * pPars )
     Vec_Ptr_t * vPios;
     void * pManTime;
     char * pName, * pSpec;
-    int clk;
+    clock_t clk;
 
     // save useful things
     pManTime = pAig->pManTime; pAig->pManTime = NULL;
diff --git a/src/opt/lpk/lpkAbcDec.c b/src/opt/lpk/lpkAbcDec.c
index de5b66cc..731c37e6 100644
--- a/src/opt/lpk/lpkAbcDec.c
+++ b/src/opt/lpk/lpkAbcDec.c
@@ -148,7 +148,7 @@ int Lpk_Decompose_rec( Lpk_Man_t * pMan, Lpk_Fun_t * p )
 {
     Lpk_Res_t * pResMux, * pResDsd;
     Lpk_Fun_t * p2;
-    int clk;
+    clock_t clk;
 
     // is only called for non-trivial blocks
     assert( p->nLutK >= 3 && p->nLutK <= 6 );
diff --git a/src/opt/lpk/lpkCore.c b/src/opt/lpk/lpkCore.c
index 5019ba83..6ab13bda 100644
--- a/src/opt/lpk/lpkCore.c
+++ b/src/opt/lpk/lpkCore.c
@@ -133,7 +133,8 @@ int Lpk_ExploreCut( Lpk_Man_t * p, Lpk_Cut_t * pCut, Kit_DsdNtk_t * pNtk )
     Kit_DsdObj_t * pRoot;
     If_Obj_t * pDriver, * ppLeaves[16];
     Abc_Obj_t * pLeaf, * pObjNew;
-    int nGain, i, clk;
+    int nGain, i;
+    clock_t clk;
     int nNodesBef;
 //    int nOldShared;
 
@@ -242,7 +243,8 @@ int Lpk_ResynthesizeNode( Lpk_Man_t * p )
     Kit_DsdNtk_t * pDsdNtk;
     Lpk_Cut_t * pCut;
     unsigned * pTruth;
-    int i, k, nSuppSize, nCutNodes, RetValue, clk;
+    int i, k, nSuppSize, nCutNodes, RetValue;
+    clock_t clk;
 
     // compute the cuts
 clk = clock();
@@ -371,7 +373,8 @@ int Lpk_ResynthesizeNodeNew( Lpk_Man_t * p )
     Lpk_Cut_t * pCut;
     unsigned * pTruth;
     int nNodesBef, nNodesAft, nCutNodes;
-    int i, k, clk;
+    int i, k;
+    clock_t clk;
     int Required = Abc_ObjRequiredLevel(p->pObj);
 //    CloudNode * pFun2;//, * pFun1;
 
@@ -507,7 +510,8 @@ int Lpk_Resynthesize( Abc_Ntk_t * pNtk, Lpk_Par_t * pPars )
     Abc_Obj_t * pObj;
     double Delta;
 //    int * pnFanouts, nObjMax;
-    int i, Iter, nNodes, nNodesPrev, clk = clock();
+    int i, Iter, nNodes, nNodesPrev;
+    clock_t clk = clock();
     assert( Abc_NtkIsLogic(pNtk) );
  
     // sweep dangling nodes as a preprocessing step
diff --git a/src/opt/lpk/lpkInt.h b/src/opt/lpk/lpkInt.h
index 61fa1624..2ff47dc4 100644
--- a/src/opt/lpk/lpkInt.h
+++ b/src/opt/lpk/lpkInt.h
@@ -121,20 +121,20 @@ struct Lpk_Man_t_
     // counter of non-DSD blocks
     int          nBlocks[17];
     // runtime
-    int          timeCuts;
-    int          timeTruth;
-    int          timeSupps;
-    int          timeTruth2;
-    int          timeTruth3;
-    int          timeEval;
-    int          timeMap;
-    int          timeOther;
-    int          timeTotal;
+    clock_t      timeCuts;
+    clock_t      timeTruth;
+    clock_t      timeSupps;
+    clock_t      timeTruth2;
+    clock_t      timeTruth3;
+    clock_t      timeEval;
+    clock_t      timeMap;
+    clock_t      timeOther;
+    clock_t      timeTotal;
     // runtime of eval
-    int          timeEvalMuxAn;
-    int          timeEvalMuxSp;
-    int          timeEvalDsdAn;
-    int          timeEvalDsdSp;
+    clock_t      timeEvalMuxAn;
+    clock_t      timeEvalMuxSp;
+    clock_t      timeEvalDsdAn;
+    clock_t      timeEvalDsdSp;
  
 };
 
diff --git a/src/opt/mfs/mfsCore.c b/src/opt/mfs/mfsCore.c
index 5214e833..8ca9edcf 100644
--- a/src/opt/mfs/mfsCore.c
+++ b/src/opt/mfs/mfsCore.c
@@ -235,7 +235,7 @@ void Abc_NtkMfsPowerResub( Mfs_Man_t * p, Mfs_Par_t * pPars)
 ***********************************************************************/
 int Abc_NtkMfsResub( Mfs_Man_t * p, Abc_Obj_t * pNode )
 {
-    int clk;
+    clock_t clk;
     p->nNodesTried++;
     // prepare data structure for this node
     Mfs_ManClean( p );
@@ -307,7 +307,8 @@ int Abc_NtkMfsNode( Mfs_Man_t * p, Abc_Obj_t * pNode )
     float dProb;
     extern Hop_Obj_t * Abc_NodeIfNodeResyn( Bdc_Man_t * p, Hop_Man_t * pHop, Hop_Obj_t * pRoot, int nVars, Vec_Int_t * vTruth, unsigned * puCare, float dProb );
 
-    int nGain, clk;
+    int nGain;
+    clock_t clk;
     p->nNodesTried++;
     // prepare data structure for this node
     Mfs_ManClean( p );
@@ -380,7 +381,8 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars )
     Abc_Obj_t * pObj;
     Vec_Vec_t * vLevels;
     Vec_Ptr_t * vNodes;
-    int i, k, nNodes, nFaninMax, clk = clock(), clk2;
+    int i, k, nNodes, nFaninMax;
+    clock_t clk = clock(), clk2;
     int nTotalNodesBeg = Abc_NtkNodeNum(pNtk);
     int nTotalEdgesBeg = Abc_NtkGetTotalFanins(pNtk);
 
diff --git a/src/opt/mfs/mfsInt.h b/src/opt/mfs/mfsInt.h
index fe154093..8b28fe61 100644
--- a/src/opt/mfs/mfsInt.h
+++ b/src/opt/mfs/mfsInt.h
@@ -119,14 +119,14 @@ struct Mfs_Man_t_
     float               TotalSwitchingBeg;
     float               TotalSwitchingEnd;
     // statistics
-    int                 timeWin;
-    int                 timeDiv;
-    int                 timeAig;
-    int                 timeGia;
-    int                 timeCnf;
-    int                 timeSat;
-    int                 timeInt;
-    int                 timeTotal;
+    clock_t             timeWin;
+    clock_t             timeDiv;
+    clock_t             timeAig;
+    clock_t             timeGia;
+    clock_t             timeCnf;
+    clock_t             timeSat;
+    clock_t             timeInt;
+    clock_t             timeTotal;
 };
 
 static inline float Abc_MfsObjProb( Mfs_Man_t * p, Abc_Obj_t * pObj ) { return (p->vProbs && pObj->Id < Vec_IntSize(p->vProbs))? Abc_Int2Float(Vec_IntEntry(p->vProbs,pObj->Id)) : 0.0; }
diff --git a/src/opt/mfs/mfsResub.c b/src/opt/mfs/mfsResub.c
index e908a56c..54f40721 100644
--- a/src/opt/mfs/mfsResub.c
+++ b/src/opt/mfs/mfsResub.c
@@ -167,7 +167,8 @@ int Abc_NtkMfsSolveSatResub( Mfs_Man_t * p, Abc_Obj_t * pNode, int iFanin, int f
     int fVeryVerbose = p->pPars->fVeryVerbose && Vec_PtrSize(p->vDivs) < 80;// || pNode->Id == 556;
     unsigned * pData;
     int pCands[MFS_FANIN_MAX];
-    int RetValue, iVar, i, nCands, nWords, w, clk;
+    int RetValue, iVar, i, nCands, nWords, w;
+    clock_t clk;
     Abc_Obj_t * pFanin;
     Hop_Obj_t * pFunc;
     assert( iFanin >= 0 );
@@ -314,7 +315,8 @@ int Abc_NtkMfsSolveSatResub2( Mfs_Man_t * p, Abc_Obj_t * pNode, int iFanin, int
     int fVeryVerbose = p->pPars->fVeryVerbose && Vec_PtrSize(p->vDivs) < 80;
     unsigned * pData, * pData2;
     int pCands[MFS_FANIN_MAX];
-    int RetValue, iVar, iVar2, i, w, nCands, clk, nWords, fBreak;
+    int RetValue, iVar, iVar2, i, w, nCands, nWords, fBreak;
+    clock_t clk;
     Abc_Obj_t * pFanin;
     Hop_Obj_t * pFunc;
     assert( iFanin >= 0 );
diff --git a/src/opt/nwk/nwkBidec.c b/src/opt/nwk/nwkBidec.c
index 1b6439d2..2f1c0366 100644
--- a/src/opt/nwk/nwkBidec.c
+++ b/src/opt/nwk/nwkBidec.c
@@ -133,7 +133,7 @@ void Nwk_ManBidecResyn( Nwk_Man_t * pNtk, int fVerbose )
     Nwk_Obj_t * pObj;
     Vec_Int_t * vTruth;
     int i, nGainTotal = 0, nNodes1, nNodes2;
-    int clk = clock();
+    clock_t clk = clock();
     pPars->nVarsMax = Nwk_ManGetFaninMax( pNtk );
     pPars->fVerbose = fVerbose;
     if ( pPars->nVarsMax < 2 )
diff --git a/src/opt/nwk/nwkFlow.c b/src/opt/nwk/nwkFlow.c
index 3961e5c2..50a4787f 100644
--- a/src/opt/nwk/nwkFlow.c
+++ b/src/opt/nwk/nwkFlow.c
@@ -444,7 +444,7 @@ Vec_Ptr_t * Nwk_ManRetimeCutForward( Nwk_Man_t * pMan, int nLatches, int fVerbos
     Vec_Ptr_t * vNodes;
     Nwk_Obj_t * pObj;
     int i, RetValue, Counter = 0, Counter2 = 0;
-    int clk = clock();
+    clock_t clk = clock();
     // set the sequential parameters
     pMan->nLatches = nLatches;
     pMan->nTruePis = Nwk_ManCiNum(pMan) - nLatches;
@@ -525,7 +525,7 @@ Vec_Ptr_t * Nwk_ManRetimeCutBackward( Nwk_Man_t * pMan, int nLatches, int fVerbo
     Vec_Ptr_t * vNodes;
     Nwk_Obj_t * pObj;
     int i, RetValue, Counter = 0, Counter2 = 0;
-    int clk = clock();
+    clock_t clk = clock();
     // set the sequential parameters
     pMan->nLatches = nLatches;
     pMan->nTruePis = Nwk_ManCiNum(pMan) - nLatches;
diff --git a/src/opt/nwk/nwkMap.c b/src/opt/nwk/nwkMap.c
index 5f08e179..3de55c43 100644
--- a/src/opt/nwk/nwkMap.c
+++ b/src/opt/nwk/nwkMap.c
@@ -109,7 +109,8 @@ If_Man_t * Nwk_ManToIf( Aig_Man_t * p, If_Par_t * pPars, Vec_Ptr_t * vAigToIf )
     If_Man_t * pIfMan;
     If_Obj_t * pIfObj;
     Aig_Obj_t * pNode, * pFanin, * pPrev;
-    int i, clk = clock();
+    int i;
+    clock_t clk = clock();
     // set the number of registers (switch activity will be combinational)
     Aig_ManSetRegNum( p, 0 );
     if ( pPars->fPower )
diff --git a/src/opt/nwk/nwkMerge.c b/src/opt/nwk/nwkMerge.c
index 2a43bc16..b733e2a3 100644
--- a/src/opt/nwk/nwkMerge.c
+++ b/src/opt/nwk/nwkMerge.c
@@ -704,7 +704,7 @@ int Nwk_ManLutMergeGraphTest( char * pFileName )
 {
     int nPairs;
     Nwk_Grf_t * p;
-    int clk = clock();
+    clock_t clk = clock();
     p = Nwk_ManLutMergeReadGraph( pFileName );
     ABC_PRT( "Reading", clock() - clk );
     clk = clock();
@@ -974,7 +974,8 @@ Vec_Int_t * Nwk_ManLutMerge( Nwk_Man_t * pNtk, void * pParsInit )
     Vec_Int_t * vResult;
     Vec_Ptr_t * vStart, * vNext, * vCands1, * vCands2;
     Nwk_Obj_t * pLut, * pCand;
-    int i, k, nVertsMax, nCands, clk = clock();
+    int i, k, nVertsMax, nCands;
+    clock_t clk = clock();
     // count the number of vertices
     nVertsMax = 0;
     Nwk_ManForEachNode( pNtk, pLut, i )
diff --git a/src/opt/nwk/nwkUtil.c b/src/opt/nwk/nwkUtil.c
index 9d23c869..cf3e5bf3 100644
--- a/src/opt/nwk/nwkUtil.c
+++ b/src/opt/nwk/nwkUtil.c
@@ -543,7 +543,8 @@ int Nwk_ManMinimumBaseInt( Nwk_Man_t * pNtk, int fVerbose )
 ***********************************************************************/
 void Nwk_ManMinimumBaseRec( Nwk_Man_t * pNtk, int fVerbose )
 {
-    int i, clk = clock();
+    int i;
+    clock_t clk = clock();
     for ( i = 0; Nwk_ManMinimumBaseInt( pNtk, fVerbose ); i++ );
     ABC_PRT( "Minbase", clock() - clk );
 }
diff --git a/src/opt/res/resCore.c b/src/opt/res/resCore.c
index effc7e65..acb8542c 100644
--- a/src/opt/res/resCore.c
+++ b/src/opt/res/resCore.c
@@ -60,18 +60,18 @@ struct Res_Man_t_
     int           nTotalNets2;   // the total number of nets
     int           nTotalNodes2;  // the total number of nodess
     // runtime
-    int           timeWin;       // windowing
-    int           timeDiv;       // divisors
-    int           timeAig;       // strashing
-    int           timeSim;       // simulation
-    int           timeCand;      // resubstitution candidates
-    int           timeSatTotal;  // SAT solving total 
-    int           timeSatSat;    // SAT solving (sat calls)
-    int           timeSatUnsat;  // SAT solving (unsat calls)
-    int           timeSatSim;    // SAT solving (simulation)
-    int           timeInt;       // interpolation 
-    int           timeUpd;       // updating  
-    int           timeTotal;     // total runtime
+    clock_t       timeWin;       // windowing
+    clock_t       timeDiv;       // divisors
+    clock_t       timeAig;       // strashing
+    clock_t       timeSim;       // simulation
+    clock_t       timeCand;      // resubstitution candidates
+    clock_t       timeSatTotal;  // SAT solving total 
+    clock_t       timeSatSat;    // SAT solving (sat calls)
+    clock_t       timeSatUnsat;  // SAT solving (unsat calls)
+    clock_t       timeSatSim;    // SAT solving (simulation)
+    clock_t       timeInt;       // interpolation 
+    clock_t       timeUpd;       // updating  
+    clock_t       timeTotal;     // total runtime
 };
 
 extern Hop_Obj_t * Kit_GraphToHop( Hop_Man_t * pMan, Kit_Graph_t * pGraph );
@@ -220,7 +220,7 @@ int Abc_NtkResynthesize( Abc_Ntk_t * pNtk, Res_Par_t * pPars )
     Vec_Ptr_t * vFanins;
     unsigned * puTruth;
     int i, k, RetValue, nNodesOld, nFanins, nFaninsMax;
-    int clk, clkTotal = clock();
+    clock_t clk, clkTotal = clock();
 
     // start the manager
     p = Res_ManAlloc( pPars );
diff --git a/src/opt/res/resInt.h b/src/opt/res/resInt.h
index cd0cf84b..f9709bf6 100644
--- a/src/opt/res/resInt.h
+++ b/src/opt/res/resInt.h
@@ -91,7 +91,7 @@ struct Res_Sim_t_
     // resub candidates
     Vec_Vec_t *      vCands;       // resubstitution candidates
     // statistics
-    int              timeSat;
+    clock_t          timeSat;
 };
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/res/resSat.c b/src/opt/res/resSat.c
index 111442b4..eec4012a 100644
--- a/src/opt/res/resSat.c
+++ b/src/opt/res/resSat.c
@@ -216,7 +216,7 @@ int Res_SatSimulate( Res_Sim_t * p, int nPatsLimit, int fOnSet )
     sat_solver * pSat;
     int RetValue = -1; // Suppress "might be used uninitialized"
     int i, k, value, status, Lit, Var, iPat;
-    int clk = clock();
+    clock_t clk = clock();
 
 //printf( "Looking for %s:  ", fOnSet? "onset " : "offset" );
 
diff --git a/src/opt/ret/retCore.c b/src/opt/ret/retCore.c
index 1b574001..35d5f4d0 100644
--- a/src/opt/ret/retCore.c
+++ b/src/opt/ret/retCore.c
@@ -27,7 +27,7 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-int timeRetime = 0;
+clock_t timeRetime = 0;
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -48,7 +48,8 @@ int Abc_NtkRetime( Abc_Ntk_t * pNtk, int Mode, int nDelayLim, int fForwardOnly,
 {
     int nLatches = Abc_NtkLatchNum(pNtk);
     int nLevels  = Abc_NtkLevel(pNtk);
-    int RetValue = 0, clkTotal = clock();
+    int RetValue = 0;
+    clock_t clkTotal = clock();
     int nNodesOld, nLatchesOld;
     assert( Mode > 0 && Mode < 7 );
     assert( !fForwardOnly || !fBackwardOnly );
diff --git a/src/opt/ret/retFlow.c b/src/opt/ret/retFlow.c
index f684939c..9b215dab 100644
--- a/src/opt/ret/retFlow.c
+++ b/src/opt/ret/retFlow.c
@@ -145,7 +145,7 @@ Vec_Ptr_t * Abc_NtkMaxFlow( Abc_Ntk_t * pNtk, int fForward, int fVerbose )
     Vec_Ptr_t * vMinCut;
     Abc_Obj_t * pLatch;
     int Flow, FlowCur, RetValue, i;
-    int clk = clock();
+    clock_t clk = clock();
     int fUseDirectedFlow = 1;
 
     // find the max-flow
diff --git a/src/opt/ret/retInit.c b/src/opt/ret/retInit.c
index 44331e72..b3f6180a 100644
--- a/src/opt/ret/retInit.c
+++ b/src/opt/ret/retInit.c
@@ -48,7 +48,8 @@ Vec_Int_t * Abc_NtkRetimeInitialValues( Abc_Ntk_t * pNtkCone, Vec_Int_t * vValue
 {
     Vec_Int_t * vSolution;
     Abc_Ntk_t * pNtkMiter, * pNtkLogic;
-    int RetValue, clk;
+    int RetValue;
+    clock_t clk;
     if ( pNtkCone == NULL )
         return Vec_IntDup( vValues );
     // convert the target network to AIG
diff --git a/src/opt/ret/retLvalue.c b/src/opt/ret/retLvalue.c
index 95569867..5bcc2583 100644
--- a/src/opt/ret/retLvalue.c
+++ b/src/opt/ret/retLvalue.c
@@ -93,7 +93,8 @@ Vec_Int_t * Abc_NtkRetimeGetLags( Abc_Ntk_t * pNtk, int nIterLimit, int fVerbose
     Vec_Int_t * vLags;
     Vec_Ptr_t * vNodes, * vLatches;
     Abc_Obj_t * pNode;
-    int i, FiMax, FiBest, RetValue, clk, clkIter;
+    int i, FiMax, FiBest, RetValue;
+    clock_t clk, clkIter;
     char NodeLag;
 
     // get the upper bound on the clock period
diff --git a/src/opt/rwr/rwr.h b/src/opt/rwr/rwr.h
index 50ea7998..d6c57329 100644
--- a/src/opt/rwr/rwr.h
+++ b/src/opt/rwr/rwr.h
@@ -86,13 +86,13 @@ struct Rwr_Man_t_
     int                nCutsBad;
     int                nSubgraphs;
     // runtime statistics
-    int                timeStart;
-    int                timeCut;
-    int                timeRes;
-    int                timeEval;
-    int                timeMffc;
-    int                timeUpdate;
-    int                timeTotal;
+    clock_t            timeStart;
+    clock_t            timeCut;
+    clock_t            timeRes;
+    clock_t            timeEval;
+    clock_t            timeMffc;
+    clock_t            timeUpdate;
+    clock_t            timeTotal;
 };
 
 struct Rwr_Node_t_ // 24 bytes
@@ -146,9 +146,9 @@ extern void              Rwr_ManPrintStatsFile( Rwr_Man_t * p );
 extern void *            Rwr_ManReadDecs( Rwr_Man_t * p );
 extern Vec_Ptr_t *       Rwr_ManReadLeaves( Rwr_Man_t * p );
 extern int               Rwr_ManReadCompl( Rwr_Man_t * p );
-extern void              Rwr_ManAddTimeCuts( Rwr_Man_t * p, int Time );
-extern void              Rwr_ManAddTimeUpdate( Rwr_Man_t * p, int Time );
-extern void              Rwr_ManAddTimeTotal( Rwr_Man_t * p, int Time );
+extern void              Rwr_ManAddTimeCuts( Rwr_Man_t * p, clock_t Time );
+extern void              Rwr_ManAddTimeUpdate( Rwr_Man_t * p, clock_t Time );
+extern void              Rwr_ManAddTimeTotal( Rwr_Man_t * p, clock_t Time );
 /*=== rwrPrint.c ========================================================*/
 extern void              Rwr_ManPrint( Rwr_Man_t * p );
 /*=== rwrUtil.c ========================================================*/
diff --git a/src/opt/rwr/rwrEva.c b/src/opt/rwr/rwrEva.c
index 83eb8d7b..d3d5143c 100644
--- a/src/opt/rwr/rwrEva.c
+++ b/src/opt/rwr/rwrEva.c
@@ -69,7 +69,7 @@ int Rwr_NodeRewrite( Rwr_Man_t * p, Cut_Man_t * pManCut, Abc_Obj_t * pNode, int
     int Required, nNodesSaved;
     int nNodesSaveCur = -1; // Suppress "might be used uninitialized"
     int i, GainCur, GainBest = -1;
-    int clk, clk2;//, Counter;
+    clock_t clk, clk2;//, Counter;
 
     p->nNodesConsidered++;
     // get the required times
diff --git a/src/opt/rwr/rwrExp.c b/src/opt/rwr/rwrExp.c
index c4664fbf..2e5bc536 100644
--- a/src/opt/rwr/rwrExp.c
+++ b/src/opt/rwr/rwrExp.c
@@ -226,7 +226,7 @@ void Rwt_Man5ExplorePrint()
     int * pDistrib;
     unsigned * pReprs;
     unsigned uTruth, uTruthC;
-    int clk = clock();
+    clock_t clk = clock();
     Vec_Int_t * vClassesNN, * vClassesNPN;
 
     // find the max number of occurences
diff --git a/src/opt/rwr/rwrMan.c b/src/opt/rwr/rwrMan.c
index 00273b38..78ee2067 100644
--- a/src/opt/rwr/rwrMan.c
+++ b/src/opt/rwr/rwrMan.c
@@ -48,7 +48,7 @@ Rwr_Man_t * Rwr_ManStart( int  fPrecompute )
 {
     Dec_Man_t * pManDec;
     Rwr_Man_t * p;
-    int clk = clock();
+    clock_t clk = clock();
 clk = clock();
     p = ABC_ALLOC( Rwr_Man_t, 1 );
     memset( p, 0, sizeof(Rwr_Man_t) );
@@ -258,7 +258,7 @@ int Rwr_ManReadCompl( Rwr_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Rwr_ManAddTimeCuts( Rwr_Man_t * p, int Time )
+void Rwr_ManAddTimeCuts( Rwr_Man_t * p, clock_t Time )
 {
     p->timeCut += Time;
 }
@@ -274,7 +274,7 @@ void Rwr_ManAddTimeCuts( Rwr_Man_t * p, int Time )
   SeeAlso     []
 
 ***********************************************************************/
-void Rwr_ManAddTimeUpdate( Rwr_Man_t * p, int Time )
+void Rwr_ManAddTimeUpdate( Rwr_Man_t * p, clock_t Time )
 {
     p->timeUpdate += Time;
 }
@@ -290,7 +290,7 @@ void Rwr_ManAddTimeUpdate( Rwr_Man_t * p, int Time )
   SeeAlso     []
 
 ***********************************************************************/
-void Rwr_ManAddTimeTotal( Rwr_Man_t * p, int Time )
+void Rwr_ManAddTimeTotal( Rwr_Man_t * p, clock_t Time )
 {
     p->timeTotal += Time;
 }
diff --git a/src/opt/rwr/rwrUtil.c b/src/opt/rwr/rwrUtil.c
index ac723588..97ddca3c 100644
--- a/src/opt/rwr/rwrUtil.c
+++ b/src/opt/rwr/rwrUtil.c
@@ -428,7 +428,8 @@ void Rwr_ManWriteToArray( Rwr_Man_t * p )
     FILE * pFile;
     Rwr_Node_t * pNode;
     unsigned Entry0, Entry1;
-    int i, nEntries, clk = clock();
+    int i, nEntries;
+    clock_t clk = clock();
     // prepare the buffer
     nEntries = p->vForest->nSize - 5;
     pFile = fopen( "npn4_aig_array.txt", "w" );
@@ -474,7 +475,8 @@ void Rwr_ManLoadFromArray( Rwr_Man_t * p, int fVerbose )
     Rwr_Node_t * p0, * p1;
     unsigned Entry0, Entry1;
     int Level, Volume, nEntries, fExor;
-    int i, clk = clock();
+    int i;
+    clock_t clk = clock();
 
     // reconstruct the forest
     for ( i = 0; ; i++ )
@@ -524,7 +526,8 @@ void Rwr_ManWriteToFile( Rwr_Man_t * p, char * pFileName )
     FILE * pFile;
     Rwr_Node_t * pNode;
     unsigned * pBuffer;
-    int i, nEntries, clk = clock();
+    int i, nEntries;
+    clock_t clk = clock();
     // prepare the buffer
     nEntries = p->vForest->nSize - 5;
     pBuffer = ABC_ALLOC( unsigned, nEntries * 2 );
@@ -562,7 +565,8 @@ void Rwr_ManLoadFromFile( Rwr_Man_t * p, char * pFileName )
     Rwr_Node_t * p0, * p1;
     unsigned * pBuffer;
     int Level, Volume, nEntries, fExor;
-    int i, clk = clock();
+    int i;
+    clock_t clk = clock();
     int RetValue;
 
     // load the data
diff --git a/src/opt/rwt/rwt.h b/src/opt/rwt/rwt.h
index a528a307..2e6de2cd 100644
--- a/src/opt/rwt/rwt.h
+++ b/src/opt/rwt/rwt.h
@@ -94,14 +94,14 @@ struct Rwt_Man_t_
     int                nCutsBad;
     int                nSubgraphs;
     // runtime statistics
-    int                timeStart;
-    int                timeTruth;
-    int                timeCut;
-    int                timeRes;
-    int                timeEval;
-    int                timeMffc;
-    int                timeUpdate;
-    int                timeTotal;
+    clock_t            timeStart;
+    clock_t            timeTruth;
+    clock_t            timeCut;
+    clock_t            timeRes;
+    clock_t            timeEval;
+    clock_t            timeMffc;
+    clock_t            timeUpdate;
+    clock_t            timeTotal;
 };
 
 struct Rwt_Node_t_ // 24 bytes
@@ -142,9 +142,9 @@ extern void              Rwt_ManPrintStatsFile( Rwt_Man_t * p );
 extern void *            Rwt_ManReadDecs( Rwt_Man_t * p );
 extern Vec_Ptr_t *       Rwt_ManReadLeaves( Rwt_Man_t * p );
 extern int               Rwt_ManReadCompl( Rwt_Man_t * p );
-extern void              Rwt_ManAddTimeCuts( Rwt_Man_t * p, int Time );
-extern void              Rwt_ManAddTimeUpdate( Rwt_Man_t * p, int Time );
-extern void              Rwt_ManAddTimeTotal( Rwt_Man_t * p, int Time );
+extern void              Rwt_ManAddTimeCuts( Rwt_Man_t * p, clock_t Time );
+extern void              Rwt_ManAddTimeUpdate( Rwt_Man_t * p, clock_t Time );
+extern void              Rwt_ManAddTimeTotal( Rwt_Man_t * p, clock_t Time );
 /*=== rwrUtil.c ========================================================*/
 extern void              Rwt_ManLoadFromArray( Rwt_Man_t * p, int fVerbose );
 extern char *            Rwt_ManGetPractical( Rwt_Man_t * p );
diff --git a/src/opt/rwt/rwtMan.c b/src/opt/rwt/rwtMan.c
index 775d3a88..17799407 100644
--- a/src/opt/rwt/rwtMan.c
+++ b/src/opt/rwt/rwtMan.c
@@ -87,7 +87,7 @@ void Rwt_ManGlobalStop()
 Rwt_Man_t * Rwt_ManStart( int fPrecompute )
 {
     Rwt_Man_t * p;
-    int clk = clock();
+    clock_t clk = clock();
 clk = clock();
     p = ABC_ALLOC( Rwt_Man_t, 1 );
     memset( p, 0, sizeof(Rwt_Man_t) );
@@ -298,7 +298,7 @@ int Rwt_ManReadCompl( Rwt_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Rwt_ManAddTimeCuts( Rwt_Man_t * p, int Time )
+void Rwt_ManAddTimeCuts( Rwt_Man_t * p, clock_t Time )
 {
     p->timeCut += Time;
 }
@@ -314,7 +314,7 @@ void Rwt_ManAddTimeCuts( Rwt_Man_t * p, int Time )
   SeeAlso     []
 
 ***********************************************************************/
-void Rwt_ManAddTimeUpdate( Rwt_Man_t * p, int Time )
+void Rwt_ManAddTimeUpdate( Rwt_Man_t * p, clock_t Time )
 {
     p->timeUpdate += Time;
 }
@@ -330,7 +330,7 @@ void Rwt_ManAddTimeUpdate( Rwt_Man_t * p, int Time )
   SeeAlso     []
 
 ***********************************************************************/
-void Rwt_ManAddTimeTotal( Rwt_Man_t * p, int Time )
+void Rwt_ManAddTimeTotal( Rwt_Man_t * p, clock_t Time )
 {
     p->timeTotal += Time;
 }
diff --git a/src/opt/rwt/rwtUtil.c b/src/opt/rwt/rwtUtil.c
index 6cdaf657..d6011b20 100644
--- a/src/opt/rwt/rwtUtil.c
+++ b/src/opt/rwt/rwtUtil.c
@@ -592,7 +592,8 @@ void Rwt_ManLoadFromArray( Rwt_Man_t * p, int fVerbose )
     Rwt_Node_t * p0, * p1;
     unsigned Entry0, Entry1;
     int Level, Volume, nEntries, fExor;
-    int i, clk = clock();
+    int i;
+    clock_t clk = clock();
 
     // reconstruct the forest
     for ( i = 0; ; i++ )
diff --git a/src/opt/sim/sim.h b/src/opt/sim/sim.h
index 84b2ed51..93553a84 100644
--- a/src/opt/sim/sim.h
+++ b/src/opt/sim/sim.h
@@ -88,13 +88,13 @@ struct Sym_Man_t_
     int               nPairsRem;
     int               nPairsTotal;
     // runtime statistics
-    int               timeStruct;
-    int               timeCount;
-    int               timeMatr;
-    int               timeSim;
-    int               timeFraig;
-    int               timeSat;
-    int               timeTotal;
+    clock_t           timeStruct;
+    clock_t           timeCount;
+    clock_t           timeMatr;
+    clock_t           timeSim;
+    clock_t           timeFraig;
+    clock_t           timeSat;
+    clock_t           timeTotal;
 };
 
 typedef struct Sim_Man_t_ Sim_Man_t;
@@ -126,11 +126,11 @@ struct Sim_Man_t_
     int               nSatRunsSat;
     int               nSatRunsUnsat;
     // runtime statistics
-    int               timeSim;
-    int               timeTrav;
-    int               timeFraig;
-    int               timeSat;
-    int               timeTotal;
+    clock_t           timeSim;
+    clock_t           timeTrav;
+    clock_t           timeFraig;
+    clock_t           timeSat;
+    clock_t           timeTotal;
 };
 
 typedef struct Sim_Pat_t_ Sim_Pat_t;
diff --git a/src/opt/sim/simSupp.c b/src/opt/sim/simSupp.c
index a7ceaee7..b383376e 100644
--- a/src/opt/sim/simSupp.c
+++ b/src/opt/sim/simSupp.c
@@ -104,7 +104,8 @@ Vec_Ptr_t * Sim_ComputeFunSupp( Abc_Ntk_t * pNtk, int fVerbose )
 {
     Sim_Man_t * p;
     Vec_Ptr_t * vResult;
-    int nSolved, i, clk = clock();
+    int nSolved, i;
+    clock_t clk = clock();
 
     srand( 0xABC );
 
@@ -172,7 +173,7 @@ int Sim_ComputeSuppRound( Sim_Man_t * p, int  fUseTargets )
 {
     Vec_Int_t * vTargets;
     int i, Counter = 0;
-    int clk;
+    clock_t clk;
     // perform one round of random simulation
 clk = clock();
     Sim_UtilSimulate( p, 0 );
@@ -209,7 +210,7 @@ int Sim_ComputeSuppRoundNode( Sim_Man_t * p, int iNumCi, int  fUseTargets )
     int i, k, v, Output, LuckyPat, fType0, fType1;
     int Counter = 0;
     int fFirst = 1;
-    int clk;
+    clock_t clk;
     // collect nodes by level in the TFO of the CI 
     // this proceduredoes not collect the CIs and COs
     // but it increments TravId of the collected nodes and CIs/COs
@@ -456,7 +457,7 @@ void Sim_SolveTargetsUsingSat( Sim_Man_t * p, int Limit )
     int * pModel;
     int RetValue, Output, Input, k, v;
     int Counter = 0;
-    int clk;
+    clock_t clk;
 
     p->nSatRuns = 0;
     // put targets into one array
diff --git a/src/opt/sim/simSym.c b/src/opt/sim/simSym.c
index 801d4218..0367c2af 100644
--- a/src/opt/sim/simSym.c
+++ b/src/opt/sim/simSym.c
@@ -48,7 +48,8 @@ int Sim_ComputeTwoVarSymms( Abc_Ntk_t * pNtk, int fVerbose )
     Sym_Man_t * p;
     Vec_Ptr_t * vResult;
     int Result;
-    int i, clk, clkTotal = clock();
+    int i;
+    clock_t clk, clkTotal = clock();
 
     srand( 0xABC );
 
diff --git a/src/opt/sim/simSymSat.c b/src/opt/sim/simSymSat.c
index 2043e2d7..e252e0f4 100644
--- a/src/opt/sim/simSymSat.c
+++ b/src/opt/sim/simSymSat.c
@@ -137,7 +137,8 @@ int Sim_SymmsSatProveOne( Sym_Man_t * p, int Out, int Var1, int Var2, unsigned *
     Fraig_Params_t Params;
     Fraig_Man_t * pMan;
     Abc_Ntk_t * pMiter;
-    int RetValue, i, clk;
+    int RetValue, i;
+    clock_t clk;
     int * pModel;
 
     // get the miter for this problem
diff --git a/src/opt/sim/simSymSim.c b/src/opt/sim/simSymSim.c
index fddf602e..2c2a8a9e 100644
--- a/src/opt/sim/simSymSim.c
+++ b/src/opt/sim/simSymSim.c
@@ -50,7 +50,7 @@ void Sim_SymmsSimulate( Sym_Man_t * p, unsigned * pPat, Vec_Ptr_t * vMatrsNonSym
 {
     Abc_Obj_t * pNode;
     int i, nPairsTotal, nPairsSym, nPairsNonSym;
-    int clk;
+    clock_t clk;
 
     // create the simulation matrix
     Sim_SymmsCreateSquare( p, pPat );
diff --git a/src/opt/sim/simUtils.c b/src/opt/sim/simUtils.c
index 77597e83..586fab42 100644
--- a/src/opt/sim/simUtils.c
+++ b/src/opt/sim/simUtils.c
@@ -633,7 +633,8 @@ int Sim_UtilCountPairsOnePrint( Extra_BitMat_t * pMat, Vec_Int_t * vSupport )
 ***********************************************************************/
 void Sim_UtilCountPairsAllPrint( Sym_Man_t * p )
 {
-    int i, clk;
+    int i;
+    clock_t clk;
 clk = clock();
     for ( i = 0; i < p->nOutputs; i++ )
     {
@@ -657,7 +658,8 @@ p->timeCount += clock() - clk;
 ***********************************************************************/
 void Sim_UtilCountPairsAll( Sym_Man_t * p )
 {
-    int nPairsTotal, nPairsSym, nPairsNonSym, i, clk;
+    int nPairsTotal, nPairsSym, nPairsNonSym, i;
+    clock_t clk;
 clk = clock();
     p->nPairsSymm    = 0;
     p->nPairsNonSymm = 0;