Fixing time primtouts throughout the code.

44 files changed, 79 insertions, 58 deletions

diff --git a/src/aig/aig/aigCanon.c b/src/aig/aig/aigCanon.c
index d51132c9..f312c996 100644
--- a/src/aig/aig/aigCanon.c
+++ b/src/aig/aig/aigCanon.c
@@ -175,7 +175,8 @@ void Aig_RManTableResize( Aig_RMan_t * p )
 {
     Aig_Tru_t * pEntry, * pNext;
     Aig_Tru_t ** pBinsOld, ** ppPlace;
-    int nBinsOld, Counter, i, clk;
+    int nBinsOld, Counter, i;
+    clock_t clk;
     assert( p->pBins != NULL );
 clk = clock();
     // save the old Bins
diff --git a/src/aig/aig/aigInter.c b/src/aig/aig/aigInter.c
index 6f183925..f4901c79 100644
--- a/src/aig/aig/aigInter.c
+++ b/src/aig/aig/aigInter.c
@@ -54,7 +54,7 @@ void Aig_ManInterFast( Aig_Man_t * pManOn, Aig_Man_t * pManOff, int fVerbose )
     Cnf_Dat_t * pCnfOn, * pCnfOff;
     Aig_Obj_t * pObj, * pObj2;
     int Lits[3], status, i;
-//    int clk = clock();
+//    clock_t clk = clock();
 
     assert( Aig_ManCiNum(pManOn) == Aig_ManCiNum(pManOff) );
     assert( Aig_ManCoNum(pManOn) == Aig_ManCoNum(pManOff) );
diff --git a/src/aig/gia/giaEmbed.c b/src/aig/gia/giaEmbed.c
index f71281cb..79a1acf4 100644
--- a/src/aig/gia/giaEmbed.c
+++ b/src/aig/gia/giaEmbed.c
@@ -1791,7 +1791,8 @@ void Emb_ManDumpGnuplot( Emb_Man_t * p, char * pName, int fDumpLarge, int fShowI
 void Gia_ManSolveProblem( Gia_Man_t * pGia, Emb_Par_t * pPars )
 {
     Emb_Man_t * p;
-    int i, clkSetup;
+    int i;
+    clock_t clkSetup;
     clock_t clk;
 //   Gia_ManTestDistance( pGia );
 
diff --git a/src/aig/gia/giaForce.c b/src/aig/gia/giaForce.c
index a905b220..32edb28f 100644
--- a/src/aig/gia/giaForce.c
+++ b/src/aig/gia/giaForce.c
@@ -714,7 +714,7 @@ Vec_Int_t * Frc_ManCollectCos( Frc_Man_t * p )
 void Frc_ManCrossCutTest( Frc_Man_t * p, Vec_Int_t * vOrderInit )
 {
     Vec_Int_t * vOrder;
-//    int clk = clock();
+//    clock_t clk = clock();
     vOrder = vOrderInit? vOrderInit : Frc_ManCollectCos( p );
     printf( "CrossCut = %6d\n", Frc_ManCrossCut( p, vOrder, 0 ) );
     printf( "CrossCut = %6d\n", Frc_ManCrossCut( p, vOrder, 1 ) );
diff --git a/src/aig/gia/giaSat.c b/src/aig/gia/giaSat.c
index 138eedd5..4f8a6acb 100644
--- a/src/aig/gia/giaSat.c
+++ b/src/aig/gia/giaSat.c
@@ -354,7 +354,8 @@ void Gia_ManSatExperiment( Gia_Man_t * p )
     Gia_Obj_t * pObj;
     int i, nLevels, nLeaves, nNodes, nCount[2*GIA_LIMIT+2] = {0}, nCountAll = 0;
     int Num0 = 0, Num1 = 0;
-    int clk = clock(), nWords = 0, nWords2 = 0;
+    clock_t clk = clock();
+    int nWords = 0, nWords2 = 0;
     pMan = Gia_ManSatStart();
     // mark the nodes to become roots of leaf-DAGs
     Gia_ManSetRefs( p );
diff --git a/src/aig/saig/saigAbsCba.c b/src/aig/saig/saigAbsCba.c
index 0b59274a..5a73a4d0 100644
--- a/src/aig/saig/saigAbsCba.c
+++ b/src/aig/saig/saigAbsCba.c
@@ -787,7 +787,7 @@ Vec_Int_t * Saig_ManCbaFilterInputs( Aig_Man_t * pAig, int iFirstFlopPi, Abc_Cex
 {
     Saig_ManCba_t * p;
     Vec_Int_t * vRes, * vReasons;
-    int clk;
+    clock_t clk;
     if ( Saig_ManPiNum(pAig) != pCex->nPis )
     {
         printf( "Saig_ManCbaFilterInputs(): The PI count of AIG (%d) does not match that of cex (%d).\n", 
diff --git a/src/aig/saig/saigHaig.c b/src/aig/saig/saigHaig.c
index b92b7a9b..d06dc758 100644
--- a/src/aig/saig/saigHaig.c
+++ b/src/aig/saig/saigHaig.c
@@ -198,7 +198,7 @@ int Aig_ManMapHaigNodes( Aig_Man_t * pHaig )
   SeeAlso     []
 
 ***********************************************************************/
-int Aig_ManHaigVerify( Aig_Man_t * p, Aig_Man_t * pAig, Aig_Man_t * pHaig, int nFrames, int clkSynth )
+int Aig_ManHaigVerify( Aig_Man_t * p, Aig_Man_t * pAig, Aig_Man_t * pHaig, int nFrames, clock_t clkSynth )
 {
     int nBTLimit = 0;
     Aig_Man_t * pFrames, * pTemp;
diff --git a/src/aig/saig/saigIso.c b/src/aig/saig/saigIso.c
index ccff1bde..be97aa74 100644
--- a/src/aig/saig/saigIso.c
+++ b/src/aig/saig/saigIso.c
@@ -428,7 +428,7 @@ Aig_Man_t * Iso_ManFilterPos( Aig_Man_t * pAig, Vec_Ptr_t ** pvPosEquivs, int fV
     Vec_Str_t * vStr, * vPrev;
     int i, nPos;
     clock_t clk = clock();
-    int clkDup = 0, clkAig = 0, clkIso = 0, clk2;
+    clock_t clkDup = 0, clkAig = 0, clkIso = 0, clk2;
     *pvPosEquivs = NULL;
 
     // derive AIG for each PO
diff --git a/src/aig/saig/saigIsoFast.c b/src/aig/saig/saigIsoFast.c
index 8b60368f..08718fa8 100644
--- a/src/aig/saig/saigIsoFast.c
+++ b/src/aig/saig/saigIsoFast.c
@@ -181,7 +181,7 @@ Vec_Int_t * Iso_StoCollectInfo( Iso_Sto_t * p, Aig_Obj_t * pPo )
     Aig_Man_t * pAig = p->pAig;
     Aig_Obj_t * pObj;
     int i, Value, Entry, * pPerm;
-//    int clk = clock();
+//    clock_t clk = clock();
 
     assert( Aig_ObjIsCo(pPo) );
 
diff --git a/src/base/abci/abcCut.c b/src/base/abci/abcCut.c
index a2ab9315..918ee2ab 100644
--- a/src/base/abci/abcCut.c
+++ b/src/base/abci/abcCut.c
@@ -291,7 +291,7 @@ Cut_Man_t * Abc_NtkSeqCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams )
     Abc_Obj_t * pObj, * pNode;
     int i, nIters, fStatus;
     Vec_Int_t * vChoices;
-    int clk = clock();
+    clock_t clk = clock();
 
     assert( Abc_NtkIsSeq(pNtk) );
     assert( pParams->fSeq );
diff --git a/src/base/abci/abcFraig.c b/src/base/abci/abcFraig.c
index 5ca34ba1..23004df2 100644
--- a/src/base/abci/abcFraig.c
+++ b/src/base/abci/abcFraig.c
@@ -698,7 +698,7 @@ Abc_Ntk_t * Abc_NtkFraigRestore()
     Vec_Ptr_t * vStore;
     Abc_Ntk_t * pNtk, * pFraig;
     int nWords1, nWords2, nWordsMin;
-//    int clk = clock();
+//    clock_t clk = clock();
 
     // get the stored network
     vStore = Abc_FrameReadStore();
diff --git a/src/base/abci/abcIvy.c b/src/base/abci/abcIvy.c
index 0c422ab5..8df8d150 100644
--- a/src/base/abci/abcIvy.c
+++ b/src/base/abci/abcIvy.c
@@ -543,7 +543,7 @@ int Abc_NtkIvyProve( Abc_Ntk_t ** ppNtk, void * pPars )
     // apply AIG rewriting
     if ( pParams->fUseRewriting && Abc_NtkNodeNum(pNtk) > 500 )
     {
-//        int clk = clock();
+//        clock_t clk = clock();
 //printf( "Before rwsat = %d. ", Abc_NtkNodeNum(pNtk) );
         pParams->fUseRewriting = 0;
         pNtk = Abc_NtkBalance( pNtkTemp = pNtk, 0, 0, 0 );          
diff --git a/src/base/abci/abcProve.c b/src/base/abci/abcProve.c
index f4bd89ef..0322b587 100644
--- a/src/base/abci/abcProve.c
+++ b/src/base/abci/abcProve.c
@@ -35,7 +35,7 @@ extern int  Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMa
 extern Abc_Ntk_t * Abc_NtkFromFraig( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk );
 
 static Abc_Ntk_t * Abc_NtkMiterFraig( Abc_Ntk_t * pNtk, int nBTLimit, ABC_INT64_T nInspLimit, int * pRetValue, int * pNumFails, ABC_INT64_T * pNumConfs, ABC_INT64_T * pNumInspects );
-static void Abc_NtkMiterPrint( Abc_Ntk_t * pNtk, char * pString, int clk, int fVerbose );
+static void Abc_NtkMiterPrint( Abc_Ntk_t * pNtk, char * pString, clock_t clk, int fVerbose );
 
 
 ////////////////////////////////////////////////////////////////////////
@@ -308,7 +308,7 @@ Abc_Ntk_t * Abc_NtkMiterFraig( Abc_Ntk_t * pNtk, int nBTLimit, ABC_INT64_T nInsp
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkMiterPrint( Abc_Ntk_t * pNtk, char * pString, int clk, int fVerbose )
+void Abc_NtkMiterPrint( Abc_Ntk_t * pNtk, char * pString, clock_t clk, int fVerbose )
 {
     if ( !fVerbose )
         return;
diff --git a/src/base/abci/abcRec.c b/src/base/abci/abcRec.c
index 276f29c9..dd4beebd 100644
--- a/src/base/abci/abcRec.c
+++ b/src/base/abci/abcRec.c
@@ -2201,7 +2201,7 @@ int Abc_NtkRecAddCut( If_Man_t * pIfMan, If_Obj_t * pRoot, If_Cut_t * pCut )
     unsigned * pTruth;
     int i, RetValue, nNodes, nNodesBeg, nInputs = s_pMan->nVars, nLeaves = If_CutLeaveNum(pCut);
     unsigned uCanonPhase;
-    int clk, timeInsert, timeBuild;
+    clock_t clk, timeInsert, timeBuild;
     //int begin = clock();
     assert( nInputs <= 16 );
     assert( nInputs == (int)pCut->nLimit );
diff --git a/src/base/abci/abcRefactor.c b/src/base/abci/abcRefactor.c
index 361b91ce..22b88d28 100644
--- a/src/base/abci/abcRefactor.c
+++ b/src/base/abci/abcRefactor.c
@@ -196,7 +196,8 @@ Dec_Graph_t * Abc_NodeRefactor( Abc_ManRef_t * p, Abc_Obj_t * pNode, Vec_Ptr_t *
     Abc_Obj_t * pFanin;
     Dec_Graph_t * pFForm;
     DdNode * bNodeFunc;
-    int nNodesSaved, nNodesAdded, i, clk;
+    int nNodesSaved, nNodesAdded, i;
+    clock_t clk;
     char * pSop;
     int Required;
 
diff --git a/src/base/abci/abcRewrite.c b/src/base/abci/abcRewrite.c
index 091ac647..a1e19405 100644
--- a/src/base/abci/abcRewrite.c
+++ b/src/base/abci/abcRewrite.c
@@ -169,7 +169,7 @@ Rwr_ManAddTimeTotal( pManRwr, clock() - clkStart );
 
     // put the nodes into the DFS order and reassign their IDs
     {
-//        int clk = clock();
+//        clock_t clk = clock();
     Abc_NtkReassignIds( pNtk );
 //        ABC_PRT( "time", clock() - clk );
     }
diff --git a/src/base/abci/fahout_cut.c b/src/base/abci/fahout_cut.c
index 0b4b421f..eff2ec19 100644
--- a/src/base/abci/fahout_cut.c
+++ b/src/base/abci/fahout_cut.c
@@ -285,7 +285,8 @@ Vec_Int_t * Abc_NtkLutMerge( Abc_Ntk_t * pNtk, Nwk_LMPars_t * pPars )
     Vec_Int_t * vResult;
     Vec_Ptr_t * vStart, * vNext, * vCands1, * vCands2;
     Abc_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;
     Abc_NtkForEachNode( pNtk, pLut, i )
diff --git a/src/base/main/mainMC.c b/src/base/main/mainMC.c
index 6d9f4c73..7fec111c 100644
--- a/src/base/main/mainMC.c
+++ b/src/base/main/mainMC.c
@@ -65,7 +65,7 @@ int main( int argc, char * argv[] )
     int fRewrite = 0;
     int fNewAlgo = 1;
     int fVerbose = 0;
-    int clkTotal = clock();
+    clock_t clkTotal = clock();
 
     if ( argc != 2 )
     {
diff --git a/src/bdd/reo/reoTest.c b/src/bdd/reo/reoTest.c
index 1e5fa1e0..58e442f3 100644
--- a/src/bdd/reo/reoTest.c
+++ b/src/bdd/reo/reoTest.c
@@ -182,7 +182,7 @@ int Extra_bddReorderTest( DdManager * dd, DdNode * bF )
     static DdManager * s_ddmin;
     DdNode * bFmin;
     int  nNodes;
-//    int clk1;
+//    clock_t clk1;
 
     if ( s_ddmin == NULL )
         s_ddmin = Cudd_Init( dd->size, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0);
diff --git a/src/bool/dec/decMan.c b/src/bool/dec/decMan.c
index cfca58c5..13bc34e0 100644
--- a/src/bool/dec/decMan.c
+++ b/src/bool/dec/decMan.c
@@ -45,7 +45,7 @@ ABC_NAMESPACE_IMPL_START
 Dec_Man_t * Dec_ManStart()
 {
     Dec_Man_t * p;
-//    int clk = clock();
+//    clock_t clk = clock();
     p = ABC_ALLOC( Dec_Man_t, 1 );
     p->pMvcMem = Mvc_ManagerStart();
     p->vCubes = Vec_IntAlloc( 8 );
diff --git a/src/demo.c b/src/demo.c
index 0656cb1e..80eca766 100644
--- a/src/demo.c
+++ b/src/demo.c
@@ -66,7 +66,7 @@ int main( int argc, char * argv[] )
     void * pAbc;
     char * pFileName;
     char Command[1000];
-    int clkRead, clkResyn, clkVer, clk;
+    clock_t clkRead, clkResyn, clkVer, clk;
 
     //////////////////////////////////////////////////////////////////////////
     // get the input file name
diff --git a/src/map/amap/amapRule.c b/src/map/amap/amapRule.c
index e8cb48c4..78016f4f 100644
--- a/src/map/amap/amapRule.c
+++ b/src/map/amap/amapRule.c
@@ -338,7 +338,7 @@ void Amap_LibCreateRules( Amap_Lib_t * pLib, int fVeryVerbose )
 {
     Amap_Gat_t * pGate;
     int i, nGates = 0;
-//    int clk = clock();
+//    clock_t clk = clock();
     pLib->fVerbose = fVeryVerbose;
     pLib->vRules   = Vec_PtrAlloc( 100 );
     pLib->vRulesX  = Vec_PtrAlloc( 100 );
diff --git a/src/map/fpga/fpgaMatch.c b/src/map/fpga/fpgaMatch.c
index dd04e562..5f233533 100644
--- a/src/map/fpga/fpgaMatch.c
+++ b/src/map/fpga/fpgaMatch.c
@@ -667,7 +667,8 @@ Fpga_Cut_t * Fpga_MappingAreaWithoutNode( Fpga_Man_t * p, Fpga_Node_t * pNode, F
 {
     Fpga_Cut_t * pCut, * pCutBestOld, * pCutRes;
     float aAreaCutBest;
-    int i, clk;
+    int i;
+    clock_t clk;
     // make sure that at least one cut other than the trivial is present
     if ( pNode->pCuts->pNext == NULL )
     {
diff --git a/src/map/if/ifCut.c b/src/map/if/ifCut.c
index c1d770fd..efeacdac 100644
--- a/src/map/if/ifCut.c
+++ b/src/map/if/ifCut.c
@@ -1407,7 +1407,7 @@ int If_CutCountTotalFanins( If_Man_t * p )
     If_Obj_t * pObj;
     Vec_Int_t * vLeaves;
     int i, nFaninsTotal = 0, Counter = 0;
-    int clk = clock();
+    clock_t clk = clock();
     vLeaves = Vec_IntAlloc( 100 );
     If_ManForEachObj( p, pObj, i )
     {
diff --git a/src/map/if/ifMap.c b/src/map/if/ifMap.c
index ea1d5f33..1293521a 100644
--- a/src/map/if/ifMap.c
+++ b/src/map/if/ifMap.c
@@ -203,7 +203,7 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
         pCut->fCompl = 0;
         if ( p->pPars->fTruth )
         {
-//            int clk = clock();
+//            clock_t clk = clock();
             int RetValue = If_CutComputeTruth( p, pCut, pCut0, pCut1, pObj->fCompl0, pObj->fCompl1 );
 //            p->timeTruth += clock() - clk;
             pCut->fUseless = 0;
diff --git a/src/map/mapper/mapperCut.c b/src/map/mapper/mapperCut.c
index 12ee5d92..bec1870a 100644
--- a/src/map/mapper/mapperCut.c
+++ b/src/map/mapper/mapperCut.c
@@ -915,7 +915,7 @@ Map_Cut_t * Map_CutTableConsider( Map_Man_t * pMan, Map_CutTable_t * p, Map_Node
 {
     Map_Cut_t * pCut;
     int Place, i;
-//    int clk;
+//    clock_t clk;
     // check the cut
     Place = Map_CutTableLookup( p, ppNodes, nNodes );
     if ( Place == -1 )
@@ -996,7 +996,7 @@ Map_Cut_t * Map_CutSortCuts( Map_Man_t * pMan, Map_CutTable_t * p, Map_Cut_t * p
 {
     Map_Cut_t * pListNew;
     int nCuts, i;
-//    int clk;
+//    clock_t clk;
     // move the cuts from the list into the array
     nCuts = Map_CutList2Array( p->pCuts1, pList );
     assert( nCuts <= MAP_CUTS_MAX_COMPUTE );
diff --git a/src/opt/cut/abcCut.c b/src/opt/cut/abcCut.c
index 0b57b844..56918f01 100644
--- a/src/opt/cut/abcCut.c
+++ b/src/opt/cut/abcCut.c
@@ -77,7 +77,7 @@ Cut_Man_t * Abc_NtkCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams )
     Vec_Ptr_t * vNodes;
     Vec_Int_t * vChoices;
     int i;
-    int clk = clock();
+    clock_t clk = clock();
 
     extern void Abc_NtkBalanceAttach( Abc_Ntk_t * pNtk );
     extern void Abc_NtkBalanceDetach( Abc_Ntk_t * pNtk );
@@ -163,7 +163,8 @@ void Abc_NtkCutsOracle( Abc_Ntk_t * pNtk, Cut_Oracle_t * p )
 {
     Abc_Obj_t * pObj;
     Vec_Ptr_t * vNodes;
-    int i, clk = clock();
+    int i;
+    clock_t clk = clock();
     int fDrop = Cut_OracleReadDrop(p);
 
     assert( Abc_NtkIsStrash(pNtk) );
@@ -225,7 +226,7 @@ Cut_Man_t * Abc_NtkSeqCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams )
     Abc_Obj_t * pObj, * pNode;
     int i, nIters, fStatus;
     Vec_Int_t * vChoices;
-    int clk = clock();
+    clock_t clk = clock();
 
     assert( Abc_NtkIsSeq(pNtk) );
     assert( pParams->fSeq );
diff --git a/src/opt/dar/darLib.c b/src/opt/dar/darLib.c
index 67a5f59e..acf49b02 100644
--- a/src/opt/dar/darLib.c
+++ b/src/opt/dar/darLib.c
@@ -592,7 +592,7 @@ Dar_Lib_t * Dar_LibRead()
 ***********************************************************************/
 void Dar_LibStart()
 {
-//    int clk = clock();
+//    clock_t clk = clock();
     assert( s_DarLib == NULL );
     s_DarLib = Dar_LibRead();
 //    printf( "The 4-input library started with %d nodes and %d subgraphs. ", s_DarLib->nObjs - 4, s_DarLib->nSubgrTotal );
@@ -1189,7 +1189,7 @@ int Dar2_LibEval( Gia_Man_t * p, Vec_Int_t * vCutLits, unsigned uTruth, int fKee
 //    int fTraining    =  0;
     Dar_LibObj_t * pObj;
     int Out, k, Class, nNodesSaved, nNodesAdded, nNodesGained;
-    clock_t clk = clock();
+//    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/darScript.c b/src/opt/dar/darScript.c
index be67b212..b59626af 100644
--- a/src/opt/dar/darScript.c
+++ b/src/opt/dar/darScript.c
@@ -721,7 +721,8 @@ Aig_Man_t * Dar_ManChoiceNew( Aig_Man_t * pAig, Dch_Pars_t * pPars )
     int fConstruct = 0;
     Aig_Man_t * pMan, * pTemp;
     Vec_Ptr_t * vAigs;
-    int i, clk;
+    int i;
+    clock_t clk;
 
 clk = clock();
 //    vAigs = Dar_ManChoiceSynthesisExt();
diff --git a/src/opt/fsim/fsimSim.c b/src/opt/fsim/fsimSim.c
index 84844407..5a3fffb0 100644
--- a/src/opt/fsim/fsimSim.c
+++ b/src/opt/fsim/fsimSim.c
@@ -384,7 +384,8 @@ static inline void Fsim_ManSimulateRound( Fsim_Man_t * p )
 void Fsim_ManSimulateRoundTest( Fsim_Man_t * p )
 {
     Fsim_Obj_t * pObj;
-    int i, clk = clock();
+    int i;
+    clock_t clk = clock();
     Fsim_ManForEachObj( p, pObj, i )
     {
     }
@@ -471,7 +472,8 @@ int Fsim_ManSimulate( Aig_Man_t * pAig, Fsim_ParSim_t * pPars )
 {
     Fsim_Man_t * p;
     Sec_MtrStatus_t Status;
-    int i, iOut, iPat, clk, clkTotal = clock(), clk2, clk2Total = 0;
+    int i, iOut, iPat;
+    clock_t clk, clkTotal = clock(), clk2, clk2Total = 0;
     assert( Aig_ManRegNum(pAig) > 0 );
     if ( pPars->fCheckMiter )
     {
diff --git a/src/opt/fsim/fsimTsim.c b/src/opt/fsim/fsimTsim.c
index 5ad78b33..78db166f 100644
--- a/src/opt/fsim/fsimTsim.c
+++ b/src/opt/fsim/fsimTsim.c
@@ -341,7 +341,8 @@ Vec_Ptr_t * Fsim_ManTerSimulate( Aig_Man_t * pAig, int fVerbose )
     Fsim_Man_t * p;
     Vec_Ptr_t * vStates;
     unsigned ** pBins, * pState;
-    int i, nWords, nBins, clk, clkTotal = clock();
+    int i, nWords, nBins;
+    clock_t clk, clkTotal = clock();
     assert( Aig_ManRegNum(pAig) > 0 );
     // create manager
     clk = clock();
diff --git a/src/opt/fxu/fxuReduce.c b/src/opt/fxu/fxuReduce.c
index 6d76576a..f9d88f7a 100644
--- a/src/opt/fxu/fxuReduce.c
+++ b/src/opt/fxu/fxuReduce.c
@@ -60,7 +60,7 @@ int Fxu_PreprocessCubePairs( Fxu_Matrix * p, Vec_Ptr_t * vCovers, int nPairsTota
     int nCubes, nBitsMax, nSum;
     int CutOffNum = -1, CutOffQuant = -1; // Suppress "might be used uninitialized"
     int iPair, iQuant, k, c;
-//    int clk = clock();
+//    clock_t clk = clock();
     char * pSopCover;
     int nFanins;
 
diff --git a/src/opt/mfs/mfsCore.c b/src/opt/mfs/mfsCore.c
index 8ca9edcf..8482d7a3 100644
--- a/src/opt/mfs/mfsCore.c
+++ b/src/opt/mfs/mfsCore.c
@@ -86,7 +86,7 @@ int Abc_NtkMfsEdgePower( Mfs_Man_t * p, Abc_Obj_t * pNode )
 
 int Abc_WinNode(Mfs_Man_t * p, Abc_Obj_t *pNode)
 {
-//    int clk;
+//    clock_t clk;
 //    Abc_Obj_t * pFanin;
 //    int i;
 
@@ -119,7 +119,7 @@ int Abc_WinNode(Mfs_Man_t * p, Abc_Obj_t *pNode)
 /*
 int Abc_NtkMfsPowerResubNode( Mfs_Man_t * p, Abc_Obj_t * pNode )
 {
-    int clk;
+    clock_t clk;
     Abc_Obj_t * pFanin;
     int i;
 
diff --git a/src/opt/mfs/mfsCore_.c b/src/opt/mfs/mfsCore_.c
index 69f64ae5..659a82fc 100644
--- a/src/opt/mfs/mfsCore_.c
+++ b/src/opt/mfs/mfsCore_.c
@@ -74,7 +74,7 @@ void Abc_NtkMfsParsDefault( 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 ); 
@@ -140,7 +140,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 );
@@ -213,7 +214,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/mfsGia.c b/src/opt/mfs/mfsGia.c
index 07c258ab..88c0a45e 100644
--- a/src/opt/mfs/mfsGia.c
+++ b/src/opt/mfs/mfsGia.c
@@ -205,7 +205,8 @@ int Abc_NtkMfsTryResubOnceGia( Mfs_Man_t * p, int * pCands, int nCands )
     int fVeryVerbose = 0;
     int fUseGia = 1;
     unsigned * pData;
-    int i, iVar, status, iOut, clk = clock();
+    int i, iVar, status, iOut;
+    clock_t clk = clock();
     p->nSatCalls++;
 //    return -1;
     assert( p->pGia != NULL );
diff --git a/src/opt/mfs/mfsInter.c b/src/opt/mfs/mfsInter.c
index b3de7b96..08713c75 100644
--- a/src/opt/mfs/mfsInter.c
+++ b/src/opt/mfs/mfsInter.c
@@ -337,7 +337,7 @@ Hop_Obj_t * Abc_NtkMfsInterplate( Mfs_Man_t * p, int * pCands, int nCands )
     Hop_Obj_t * pFunc;
     int nFanins, status;
     int c, i, * pGloVars;
-//    int clk = clock();
+//    clock_t clk = clock();
 
 //    p->nDcMints += Abc_NtkMfsInterplateEval( p, pCands, nCands );
 
diff --git a/src/opt/mfs/mfsResub_.c b/src/opt/mfs/mfsResub_.c
index bca1285d..b79ccd9e 100644
--- a/src/opt/mfs/mfsResub_.c
+++ b/src/opt/mfs/mfsResub_.c
@@ -143,7 +143,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;
     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 );
@@ -292,7 +293,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/nwkFlow_depth.c b/src/opt/nwk/nwkFlow_depth.c
index 6c2e7eb9..e4f4406f 100644
--- a/src/opt/nwk/nwkFlow_depth.c
+++ b/src/opt/nwk/nwkFlow_depth.c
@@ -465,7 +465,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;
@@ -550,7 +550,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/proof/cec/cecCorr_updated.c b/src/proof/cec/cecCorr_updated.c
index 3bea8dbf..0d441629 100644
--- a/src/proof/cec/cecCorr_updated.c
+++ b/src/proof/cec/cecCorr_updated.c
@@ -830,9 +830,10 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
     Cec_ManSim_t * pSim;
     Gia_Man_t * pSrm;
     unsigned * pInitState = NULL;
-    int r, RetValue, clkTotal = clock();
-    int clkSat = 0, clkSim = 0, clkSrm = 0;
-    int clk2, clk = clock();
+    int r, RetValue;
+    clock_t clkTotal = clock();
+    clock_t clkSat = 0, clkSim = 0, clkSrm = 0;
+    clock_t clk2, clk = clock();
     ABC_FREE( pAig->pReprs );
     ABC_FREE( pAig->pNexts );
     if ( Gia_ManRegNum(pAig) == 0 )
@@ -917,7 +918,7 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
         int fChanges = 1;
         while ( fChanges )
         {
-            int clkBmc = clock();
+            clock_t clkBmc = clock();
             fChanges = 0;
             pSrm = Gia_ManCorrSpecReduceInit( pAig, pPars->nFrames, pPars->nPrefix, !pPars->fLatchCorr, &vOutputs, pPars->fUseRings );
             if ( Gia_ManPoNum(pSrm) == 0 )
diff --git a/src/proof/fra/fraInd.c b/src/proof/fra/fraInd.c
index 633f8979..0c7134aa 100644
--- a/src/proof/fra/fraInd.c
+++ b/src/proof/fra/fraInd.c
@@ -590,7 +590,8 @@ clk2 = clock();
     // verify implications using simulation
     if ( p->pCla->vImps && Vec_IntSize(p->pCla->vImps) )
     {
-        int Temp, clk = clock();
+        int Temp;
+        clock_t clk = clock();
         if ( Temp = Fra_ImpVerifyUsingSimulation( p ) )
             printf( "Implications failing the simulation test = %d (out of %d).  ", Temp, Vec_IntSize(p->pCla->vImps) );
         else
diff --git a/src/proof/int/intM114p.c b/src/proof/int/intM114p.c
index f143dc39..ad1ff61d 100644
--- a/src/proof/int/intM114p.c
+++ b/src/proof/int/intM114p.c
@@ -394,7 +394,8 @@ int Inter_ManPerformOneStepM114p( Inter_Man_t * p, int fUsePudlak, int fUseOther
 {
     M114p_Solver_t pSat;
     Vec_Int_t * vMapRoots, * vMapVars;
-    int clk, status, RetValue;
+    clock_t clk;
+    int status, RetValue;
     assert( p->pInterNew == NULL );
     // derive the SAT solver
     pSat = Inter_ManDeriveSatSolverM114p( p->pInter, p->pCnfInter, 
diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c
index f143916a..70feaa17 100644
--- a/src/sat/bsat/satSolver.c
+++ b/src/sat/bsat/satSolver.c
@@ -317,7 +317,8 @@ static inline void act_var_rescale(sat_solver* s) {
 static inline void act_clause_rescale(sat_solver* s) {
     static int Total = 0;
     clause** cs = (clause**)vecp_begin(&s->learnts);
-    int i, clk = clock();
+    int i;
+    clock_t clk = clock();
     for (i = 0; i < vecp_size(&s->learnts); i++){
         unsigned a = clause_activity2(cs[i]);
         clause_setactivity2(cs[i], a >> 14);
diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c
index cbe6bc52..573c1d35 100644
--- a/src/sat/bsat/satSolver2.c
+++ b/src/sat/bsat/satSolver2.c
@@ -294,7 +294,8 @@ static inline void act_var_rescale(sat_solver2* s)  {
 static inline void act_clause_rescale(sat_solver2* s) {
     static int Total = 0;
     float * claActs = (float *)veci_begin(&s->claActs);
-    int i, clk = clock();
+    int i;
+    clock_t clk = clock();
     for (i = 0; i < veci_size(&s->claActs); i++)
         claActs[i] *= (float)1e-20;
     s->cla_inc *= (float)1e-20;
diff --git a/src/sat/msat/msatOrderJ.c b/src/sat/msat/msatOrderJ.c
index a9c27bd0..82e12ec6 100644
--- a/src/sat/msat/msatOrderJ.c
+++ b/src/sat/msat/msatOrderJ.c
@@ -264,7 +264,7 @@ int Msat_OrderVarSelect( Msat_Order_t * p )
     Msat_OrderVar_t * pVar, * pNext, * pVarBest;
     double * pdActs = p->pSat->pdActivity;
     double dfActBest;
-//    int clk = clock();
+//    clock_t clk = clock();
 
     pVarBest = NULL;
     dfActBest = -1.0;