Fixing time primtouts throughout the code.

43 files changed, 175 insertions, 144 deletions

diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index 56f1df85..cbebf318 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -30,7 +30,6 @@
 #include <stdlib.h>
 #include <string.h>
 #include <assert.h>
-#include <time.h>
 
 #include "src/misc/vec/vec.h"
 #include "src/aig/hop/hop.h"
diff --git a/src/base/abc/abcAig.c b/src/base/abc/abcAig.c
index d594846b..4e725a01 100644
--- a/src/base/abc/abcAig.c
+++ b/src/base/abc/abcAig.c
@@ -589,7 +589,8 @@ void Abc_AigResize( Abc_Aig_t * pMan )
 {
     Abc_Obj_t ** pBinsNew;
     Abc_Obj_t * pEnt, * pEnt2;
-    int nBinsNew, Counter, i, clk;
+    int nBinsNew, Counter, i;
+    clock_t clk;
     unsigned Key;
 
 clk = clock();
diff --git a/src/base/abc/abcDfs.c b/src/base/abc/abcDfs.c
index 6d67785b..a96263c1 100644
--- a/src/base/abc/abcDfs.c
+++ b/src/base/abc/abcDfs.c
@@ -835,7 +835,8 @@ int Abc_ObjSuppSize( Abc_Obj_t * pObj )
 int Abc_NtkSuppSizeTest( Abc_Ntk_t * p )
 {
     Abc_Obj_t * pObj;
-    int i, Counter = 0, clk = clock();
+    int i, Counter = 0;
+    clock_t clk = clock();
     Abc_NtkForEachObj( p, pObj, i )
         if ( Abc_ObjIsNode(pObj) )
             Counter += (Abc_ObjSuppSize(pObj) <= 16);
diff --git a/src/base/abc/abcHieCec.c b/src/base/abc/abcHieCec.c
index b3a3718f..83a332c2 100644
--- a/src/base/abc/abcHieCec.c
+++ b/src/base/abc/abcHieCec.c
@@ -667,7 +667,8 @@ Gia_Man_t * Abc_NtkHieCecTest( char * pFileName, int fVerbose )
     Vec_Ptr_t * vMods, * vOrder;
     Abc_Ntk_t * pNtk, * pModel;
     Gia_Man_t * pGia;
-    int i, clk = clock();
+    int i;
+    clock_t clk = clock();
 
     // read hierarchical netlist
     pNtk = Io_ReadBlifMv( pFileName, 0, fCheck );
diff --git a/src/base/abc/abcHieNew.c b/src/base/abc/abcHieNew.c
index d4598ac1..fe1496d9 100644
--- a/src/base/abc/abcHieNew.c
+++ b/src/base/abc/abcHieNew.c
@@ -22,7 +22,6 @@
 #include <stdlib.h>
 #include <string.h>
 #include <assert.h>
-#include <time.h>
 
 #include "src/misc/vec/vec.h"
 #include "src/misc/util/utilNam.h"
@@ -1491,8 +1490,8 @@ Gia_Man_t * Au_ManDeriveTest( Abc_Ntk_t * pRoot )
     Abc_Ntk_t * pMod;
     Au_Man_t * pMan;
     Au_Ntk_t * pNtk = NULL;
-    int i, clk1, clk2 = 0, clk3 = 0, clk = clock();
-//    int clk4 = 0;
+    clock_t clk1, clk2 = 0, clk3 = 0, clk = clock();
+    int i;
 
     clk1 = clock();
     pMan = Au_ManAlloc( pRoot->pDesign ? pRoot->pDesign->pName : pRoot->pName );
@@ -1570,7 +1569,7 @@ Gia_Man_t * Abc_NtkHieCecTest2( char * pFileName, char * pModelName, int fVerbos
     int fSimulation = 0;
     Gia_Man_t * pGia = NULL;
     Au_Ntk_t * pNtk, * pNtkClp = NULL;
-    int clk1 = 0, clk = clock();
+    clock_t clk1 = 0, clk = clock();
 
     // read hierarchical netlist
     pNtk = Au_NtkParseCBlif( pFileName );
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 590e5875..03eb8d21 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -10986,7 +10986,8 @@ int Abc_CommandIProve( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Prove_Params_t Params, * pParams = &Params;
     Abc_Ntk_t * pNtk, * pNtkTemp;
-    int c, clk, RetValue, iOut = -1;
+    int c, RetValue, iOut = -1;
+    clock_t clk;
 
     extern int Abc_NtkIvyProve( Abc_Ntk_t ** ppNtk, void * pPars );
 
@@ -18797,7 +18798,7 @@ int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fVerbose;
     int nConfLimit;
     int nInsLimit;
-    int clk;
+    clock_t clk;
     // set defaults
     fVerbose   = 0;
     nConfLimit = 0;   
@@ -18927,7 +18928,7 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fVerbose;
     int nConfLimit;
     int nInsLimit;
-    int clk;
+    clock_t clk;
 
     extern int Abc_NtkDSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fAlignPol, int fAndOuts, int fNewSolver, int fVerbose );
     // set defaults
@@ -19057,7 +19058,7 @@ int Abc_CommandPSat( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
     int RetValue;
-    int c, clk;
+    int c;
     int nAlgo;
     int nPartSize;
     int nConfPart;
@@ -19065,6 +19066,7 @@ int Abc_CommandPSat( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fAlignPol;
     int fSynthesize;
     int fVerbose;
+    clock_t clk;
 
     extern int Abc_NtkPartitionedSat( Abc_Ntk_t * pNtk, int nAlgo, int nPartSize, int nConfPart, int nConfTotal, int fAlignPol, int fSynthesize, int fVerbose );
     // set defaults
@@ -19215,7 +19217,8 @@ int Abc_CommandProve( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Abc_Ntk_t * pNtk, * pNtkTemp;
     Prove_Params_t Params, * pParams = &Params;
-    int c, clk, RetValue;
+    int c, RetValue;
+    clock_t clk;
 
     pNtk = Abc_FrameReadNtk(pAbc);
     // set defaults
diff --git a/src/base/abci/abcAuto.c b/src/base/abci/abcAuto.c
index e1e479e3..7b4d7694 100644
--- a/src/base/abci/abcAuto.c
+++ b/src/base/abci/abcAuto.c
@@ -128,7 +128,7 @@ void Abc_NtkAutoPrintAll( DdManager * dd, int nInputs, DdNode * pbOutputs[], int
     int nAutoSymsMaxSupp;
     int nAutoSymOuts;
     int nSuppSizeMax;
-    int clk;
+    clock_t clk;
     
     nAutoSymOuts = 0;
     nAutoSyms    = 0;
diff --git a/src/base/abci/abcBidec.c b/src/base/abci/abcBidec.c
index fc093420..507b7355 100644
--- a/src/base/abci/abcBidec.c
+++ b/src/base/abci/abcBidec.c
@@ -114,7 +114,7 @@ void Abc_NtkBidecResyn( Abc_Ntk_t * pNtk, int fVerbose )
     Abc_Obj_t * pObj;
     Vec_Int_t * vTruth;
     int i, nGainTotal = 0, nNodes1, nNodes2;
-    int clk = clock();
+    clock_t clk = clock();
     assert( Abc_NtkIsLogic(pNtk) );
     if ( !Abc_NtkToAig(pNtk) )
         return;
diff --git a/src/base/abci/abcBm.c b/src/base/abci/abcBm.c
index d2f80aeb..19c8e9ff 100644
--- a/src/base/abci/abcBm.c
+++ b/src/base/abci/abcBm.c
@@ -870,7 +870,8 @@ int Abc_NtkMiterSatBm( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nIn
 {
     static sat_solver * pSat = NULL;
     lbool   status;
-    int RetValue, clk;    
+    int RetValue;
+    clock_t clk;    
 
     extern int Abc_NodeAddClausesTop( sat_solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars );
     extern Vec_Int_t * Abc_NtkGetCiSatVarNums( Abc_Ntk_t * pNtk );    
@@ -1582,7 +1583,7 @@ float refineBySAT(Abc_Ntk_t * pNtk1, Vec_Int_t ** iMatch1, int * iGroup1, Vec_In
     Vec_Int_t * oMatchedGroups;
     FILE *result;    
     int matchFound;
-    int clk = clock();
+    clock_t clk = clock();
     float satTime = 0.0;
 
     /*matchFile = fopen("satmatch.txt", "w");*/
@@ -1787,7 +1788,7 @@ void bmGateWay( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int p_equivalence )
     
     char * vPiValues1, * vPiValues2;
     int * observability1, * observability2;
-    int clk = clock();
+    clock_t clk = clock();
     float initTime;
     float simulTime;
     float satTime;
diff --git a/src/base/abci/abcCas.c b/src/base/abci/abcCas.c
index 7e80c919..51ab4130 100644
--- a/src/base/abci/abcCas.c
+++ b/src/base/abci/abcCas.c
@@ -60,8 +60,8 @@ Abc_Ntk_t * Abc_NtkCascade( Abc_Ntk_t * pNtk, int nLutSize, int fCheck, int fVer
     Abc_Obj_t * pNode;
     char * pFileGeneric;
     int fBddSizeMax = 500000;
-    int fReorder = 1;
-    int i, clk = clock();
+    int i, fReorder = 1;
+    clock_t clk = clock();
 
     assert( Abc_NtkIsStrash(pNtk) );
     // compute the global BDDs
diff --git a/src/base/abci/abcCollapse.c b/src/base/abci/abcCollapse.c
index 69525e2f..e6a6db79 100644
--- a/src/base/abci/abcCollapse.c
+++ b/src/base/abci/abcCollapse.c
@@ -49,7 +49,7 @@ static Abc_Obj_t * Abc_NodeFromGlobalBdds( Abc_Ntk_t * pNtkNew, DdManager * dd,
 Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, int fReorder, int fVerbose )
 {
     Abc_Ntk_t * pNtkNew;
-    int clk = clock();
+    clock_t clk = clock();
 
     assert( Abc_NtkIsStrash(pNtk) );
     // compute the global BDDs
diff --git a/src/base/abci/abcCut.c b/src/base/abci/abcCut.c
index 6116649e..a2ab9315 100644
--- a/src/base/abci/abcCut.c
+++ b/src/base/abci/abcCut.c
@@ -128,7 +128,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 );
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index a5ae7e9b..82b3d916 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -1047,7 +1047,7 @@ Abc_Ntk_t * Abc_NtkDRewrite( Abc_Ntk_t * pNtk, Dar_RwrPar_t * pPars )
 {
     Aig_Man_t * pMan, * pTemp;
     Abc_Ntk_t * pNtkAig;
-    int clk;
+    clock_t clk;
     assert( Abc_NtkIsStrash(pNtk) );
     pMan = Abc_NtkToDar( pNtk, 0, 0 );
     if ( pMan == NULL )
@@ -1091,7 +1091,7 @@ Abc_Ntk_t * Abc_NtkDRefactor( Abc_Ntk_t * pNtk, Dar_RefPar_t * pPars )
 {
     Aig_Man_t * pMan, * pTemp;
     Abc_Ntk_t * pNtkAig;
-    int clk;
+    clock_t clk;
     assert( Abc_NtkIsStrash(pNtk) );
     pMan = Abc_NtkToDar( pNtk, 0, 0 );
     if ( pMan == NULL )
@@ -1128,7 +1128,7 @@ Abc_Ntk_t * Abc_NtkDC2( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, int fF
 {
     Aig_Man_t * pMan, * pTemp;
     Abc_Ntk_t * pNtkAig;
-    int clk;
+    clock_t clk;
     assert( Abc_NtkIsStrash(pNtk) );
     pMan = Abc_NtkToDar( pNtk, 0, 0 );
     if ( pMan == NULL )
@@ -1191,7 +1191,7 @@ Abc_Ntk_t * Abc_NtkDch( Abc_Ntk_t * pNtk, Dch_Pars_t * pPars )
     Aig_Man_t * pMan, * pTemp;
     Abc_Ntk_t * pNtkAig;
     Gia_Man_t * pGia;
-    int clk;
+    clock_t clk;
     assert( Abc_NtkIsStrash(pNtk) );
     pMan = Abc_NtkToDar( pNtk, 0, 0 );
     if ( pMan == NULL )
@@ -1234,7 +1234,7 @@ Abc_Ntk_t * Abc_NtkDrwsat( Abc_Ntk_t * pNtk, int fBalance, int fVerbose )
 {
     Aig_Man_t * pMan, * pTemp;
     Abc_Ntk_t * pNtkAig;
-    int clk;
+    clock_t clk;
     assert( Abc_NtkIsStrash(pNtk) );
     pMan = Abc_NtkToDar( pNtk, 0, 0 );
     if ( pMan == NULL )
@@ -1342,7 +1342,7 @@ Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName, int fFastAlgo,
 //    Cnf_Man_t * pManCnf = NULL;
     Cnf_Dat_t * pCnf;
     Abc_Ntk_t * pNtkNew = NULL;
-    int clk = clock();
+    clock_t clk = clock();
     assert( Abc_NtkIsStrash(pNtk) );
 
     // convert to the AIG manager
@@ -1457,7 +1457,8 @@ int Abc_NtkDarCec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int fPa
 {
     Aig_Man_t * pMan, * pMan1, * pMan2;
     Abc_Ntk_t * pMiter;
-    int RetValue, clkTotal = clock();
+    int RetValue;
+    clock_t clkTotal = clock();
 /*
     {
     extern void Cec_ManVerifyTwoAigs( Aig_Man_t * pAig0, Aig_Man_t * pAig1, int fVerbose );
@@ -1574,7 +1575,7 @@ Abc_Ntk_t * Abc_NtkDarSeqSweep( Abc_Ntk_t * pNtk, Fra_Ssw_t * pPars )
     Fraig_Params_t Params;
     Abc_Ntk_t * pNtkAig = NULL, * pNtkFraig;
     Aig_Man_t * pMan, * pTemp;
-    int clk = clock();
+    clock_t clk = clock();
 
     // preprocess the miter by fraiging it
     // (note that for each functional class, fraiging leaves one representative;
@@ -1857,8 +1858,9 @@ int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nStart, int nFrames, int nSizeMax, int
 {
     Aig_Man_t * pMan;
     Vec_Int_t * vMap = NULL;
-    int status, RetValue = -1, clk = clock();
-    int nTimeLimit = nTimeOut ? time(NULL) + nTimeOut : 0;
+    int status, RetValue = -1;
+    clock_t clk = clock();
+    clock_t nTimeLimit = nTimeOut ? nTimeOut * CLOCKS_PER_SEC + clock(): 0;
     // derive the AIG manager
     if ( fOrDecomp )
         pMan = Abc_NtkToDarBmc( pNtk, &vMap );
@@ -1889,7 +1891,7 @@ int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nStart, int nFrames, int nSizeMax, int
         else if ( RetValue == -1 )
         {
             Abc_Print( 1, "No output asserted in %d frames. Resource limit reached ", Abc_MaxInt(iFrame,0) );
-            if ( nTimeLimit && time(NULL) > nTimeLimit )
+            if ( nTimeLimit && clock() > nTimeLimit )
                 Abc_Print( 1, "(timeout %d sec). ", nTimeLimit );
             else
                 Abc_Print( 1, "(conf limit %d). ", nBTLimit );
@@ -1938,8 +1940,9 @@ int Abc_NtkDarBmc3( Abc_Ntk_t * pNtk, Saig_ParBmc_t * pPars, int fOrDecomp )
 {
     Aig_Man_t * pMan;
     Vec_Int_t * vMap = NULL;
-    int status, RetValue = -1, clk = clock();
-    int nTimeOut = pPars->nTimeOut ? time(NULL) + pPars->nTimeOut : 0;
+    int status, RetValue = -1;
+    clock_t clk = clock();
+    clock_t nTimeOut = pPars->nTimeOut ? pPars->nTimeOut * CLOCKS_PER_SEC + clock(): 0;
     if ( fOrDecomp && !pPars->fSolveAll )
         pMan = Abc_NtkToDarBmc( pNtk, &vMap );
     else
@@ -1966,7 +1969,7 @@ int Abc_NtkDarBmc3( Abc_Ntk_t * pNtk, Saig_ParBmc_t * pPars, int fOrDecomp )
         if ( pPars->nFailOuts == 0 )
         {
             Abc_Print( 1, "No output asserted in %d frames. Resource limit reached ", Abc_MaxInt(pPars->iFrame,0) );
-            if ( nTimeOut && time(NULL) > nTimeOut )
+            if ( nTimeOut && clock() > nTimeOut )
                 Abc_Print( 1, "(timeout %d sec). ", pPars->nTimeOut );
             else
                 Abc_Print( 1, "(conf limit %d). ", pPars->nConfLimit );
@@ -1974,7 +1977,7 @@ int Abc_NtkDarBmc3( Abc_Ntk_t * pNtk, Saig_ParBmc_t * pPars, int fOrDecomp )
         else
         {
             Abc_Print( 1, "The total of %d outputs asserted in %d frames. Resource limit reached ", pPars->nFailOuts, pPars->iFrame );
-            if ( time(NULL) > nTimeOut )
+            if ( clock() > nTimeOut )
                 Abc_Print( 1, "(timeout %d sec). ", pPars->nTimeOut );
             else
                 Abc_Print( 1, "(conf limit %d). ", pPars->nConfLimit );
@@ -2030,7 +2033,8 @@ int Abc_NtkDarBmc3( Abc_Ntk_t * pNtk, Saig_ParBmc_t * pPars, int fOrDecomp )
 ***********************************************************************/
 int Abc_NtkDarBmcInter_int( Aig_Man_t * pMan, Inter_ManParams_t * pPars, Aig_Man_t ** ppNtkRes )
 {
-    int RetValue = -1, iFrame, clk = clock();
+    int RetValue = -1, iFrame;
+    clock_t clk = clock();
     int nTotalProvedSat = 0;
     assert( pMan->nRegs > 0 );
     if ( ppNtkRes )
@@ -2354,12 +2358,14 @@ int Abc_NtkDarDemiterDual( Abc_Ntk_t * pNtk, int fVerbose )
 int Abc_NtkDarProve( Abc_Ntk_t * pNtk, Fra_Sec_t * pSecPar, int nBmcFramesMax, int nBmcConfMax )
 {
     Aig_Man_t * pMan;
-    int iFrame = -1, RetValue = -1, clkTotal = clock();
+    int iFrame = -1, RetValue = -1;
+    clock_t clkTotal = clock();
     if ( pSecPar->fTryComb || Abc_NtkLatchNum(pNtk) == 0 )
     {
         Prove_Params_t Params, * pParams = &Params;
         Abc_Ntk_t * pNtkComb;
-        int RetValue, clk = clock();
+        int RetValue;
+        clock_t clk = clock();
         if ( Abc_NtkLatchNum(pNtk) == 0 )
             Abc_Print( 1, "The network has no latches. Running CEC.\n" );
         // create combinational network
@@ -2549,7 +2555,8 @@ int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Fra_Sec_t * pSecPar )
 ***********************************************************************/
 int Abc_NtkDarPdr( Abc_Ntk_t * pNtk, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex )
 {
-    int RetValue = -1, clk = clock();
+    int RetValue = -1;
+    clock_t clk = clock();
     Aig_Man_t * pMan;
     *ppCex = NULL;
     pMan = Abc_NtkToDar( pNtk, 0, 1 );
@@ -3004,7 +3011,8 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, in
     extern int Raig_ManSimulate( Aig_Man_t * pAig, int nWords, int nIters, int TimeLimit, int fMiter, int fVerbose );
     Aig_Man_t * pMan;
     Abc_Cex_t * pCex;
-    int status, RetValue = -1, clk = clock();
+    int status, RetValue = -1;
+    clock_t clk = clock();
     if ( Abc_NtkGetChoiceNum(pNtk) )
     {
         Abc_Print( 1, "Removing %d choices from the AIG.\n", Abc_NtkGetChoiceNum(pNtk) );
@@ -3194,7 +3202,8 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, in
 int Abc_NtkDarSeqSim3( Abc_Ntk_t * pNtk, int nFrames, int nWords, int nBinSize, int nRounds, int nRandSeed, int TimeOut, int fVerbose )
 {
     Aig_Man_t * pMan;
-    int status, RetValue = -1, clk = clock();
+    int status, RetValue = -1;
+    clock_t clk = clock();
     if ( Abc_NtkGetChoiceNum(pNtk) )
     {
         Abc_Print( 1, "Removing %d choices from the AIG.\n", Abc_NtkGetChoiceNum(pNtk) );
@@ -3328,7 +3337,7 @@ Abc_Ntk_t * Abc_NtkDarTempor( Abc_Ntk_t * pNtk, int nFrames, int TimeOut, int nC
 int Abc_NtkDarInduction( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fUnique, int fUniqueAll, int fGetCex, int fVerbose, int fVeryVerbose )
 { 
     Aig_Man_t * pMan;
-    int clkTotal = clock();
+    clock_t clkTotal = clock();
     int RetValue;
     pMan = Abc_NtkToDar( pNtk, 0, 1 );
     if ( pMan == NULL )
@@ -3442,9 +3451,9 @@ void Abc_NtkInterFast( Abc_Ntk_t * pNtkOn, Abc_Ntk_t * pNtkOff, int fVerbose )
     Aig_ManStop( pManOff );
 }
 
-int timeCnf;
-int timeSat;
-int timeInt;
+clock_t timeCnf;
+clock_t timeSat;
+clock_t timeInt;
 
 /**Function*************************************************************
 
diff --git a/src/base/abci/abcDebug.c b/src/base/abci/abcDebug.c
index baf87944..ebed2efa 100644
--- a/src/base/abci/abcDebug.c
+++ b/src/base/abci/abcDebug.c
@@ -51,7 +51,8 @@ void Abc_NtkAutoDebug( Abc_Ntk_t * pNtk, int (*pFuncError) (Abc_Ntk_t *) )
 {
     Abc_Ntk_t * pNtkMod;
     char * pFileName = "bug_found.blif";
-    int i, nSteps, nIter, ModNum, RandNum = 1, clk, clkTotal = clock();
+    int i, nSteps, nIter, ModNum, RandNum = 1;
+    clock_t clk, clkTotal = clock();
     assert( Abc_NtkIsLogic(pNtk) );
     srand( 0x123123 );
     // create internal copy of the network
diff --git a/src/base/abci/abcDress2.c b/src/base/abci/abcDress2.c
index efd7db3b..84bf1229 100644
--- a/src/base/abci/abcDress2.c
+++ b/src/base/abci/abcDress2.c
@@ -358,7 +358,7 @@ void Abc_NtkDressPrintEquivs( Vec_Ptr_t * vRes )
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkDressPrintStats( Vec_Ptr_t * vRes, int nNodes0, int nNodes1, int Time )
+void Abc_NtkDressPrintStats( Vec_Ptr_t * vRes, int nNodes0, int nNodes1, clock_t Time )
 {
     Vec_Int_t * vClass;
     int i, k, Entry;
@@ -419,7 +419,7 @@ void Abc_NtkDressPrintStats( Vec_Ptr_t * vRes, int nNodes0, int nNodes1, int Tim
 void Abc_NtkDress2( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConflictLimit, int fVerbose )
 {
     Vec_Ptr_t * vRes;
-    int clk = clock();
+    clock_t clk = clock();
     vRes = Abc_NtkDressComputeEquivs( pNtk1, pNtk2, nConflictLimit, fVerbose );
 //    Abc_NtkDressPrintEquivs( vRes );
     Abc_NtkDressPrintStats( vRes, Abc_NtkNodeNum(pNtk1), Abc_NtkNodeNum(pNtk1), clock() - clk );
diff --git a/src/base/abci/abcIf.c b/src/base/abci/abcIf.c
index cf32d8ec..0a4b9d56 100644
--- a/src/base/abci/abcIf.c
+++ b/src/base/abci/abcIf.c
@@ -70,7 +70,8 @@ void Abc_NtkIfComputeSwitching( Abc_Ntk_t * pNtk, If_Man_t * pIfMan )
     Aig_Obj_t * pObjAig;
     Aig_Man_t * pAig;
     If_Obj_t * pObjIf;
-    int i, clk = clock();
+    int i;
+    clock_t clk = clock();
     // map IF objects into old network
     Abc_NtkForEachObj( pNtk, pObjAbc, i )
         if ( (pObjIf = (If_Obj_t *)pObjAbc->pTemp) )
diff --git a/src/base/abci/abcIvy.c b/src/base/abci/abcIvy.c
index c2637a08..0c422ab5 100644
--- a/src/base/abci/abcIvy.c
+++ b/src/base/abci/abcIvy.c
@@ -197,7 +197,7 @@ Abc_Ntk_t * Abc_NtkIvyHaig( Abc_Ntk_t * pNtk, int nIters, int fUseZeroCost, int
 {
     Abc_Ntk_t * pNtkAig;
     Ivy_Man_t * pMan;
-    int clk;
+    clock_t clk;
 //    int i;
 /*
 extern int nMoves;
diff --git a/src/base/abci/abcLutmin.c b/src/base/abci/abcLutmin.c
index bbea264c..bdeb53ff 100644
--- a/src/base/abci/abcLutmin.c
+++ b/src/base/abci/abcLutmin.c
@@ -85,7 +85,8 @@ void Abc_NtkCheckAbsorb( Abc_Ntk_t * pNtk, int nLutSize )
     Vec_Int_t * vCounts;
     Vec_Ptr_t * vFanins;
     Abc_Obj_t * pObj, * pFanin;
-    int i, k, Counter = 0, Counter2 = 0, clk = clock();
+    int i, k, Counter = 0, Counter2 = 0;
+    clock_t clk = clock();
     vCounts = Vec_IntStart( Abc_NtkObjNumMax(pNtk) );
     vFanins = Vec_PtrAlloc( 100 );
     Abc_NtkForEachNode( pNtk, pObj, i )
diff --git a/src/base/abci/abcMap.c b/src/base/abci/abcMap.c
index 723e5688..988da5c2 100644
--- a/src/base/abci/abcMap.c
+++ b/src/base/abci/abcMap.c
@@ -64,7 +64,7 @@ Abc_Ntk_t * Abc_NtkMap( Abc_Ntk_t * pNtk, double DelayTarget, int fRecovery, int
     Map_Man_t * pMan;
     Vec_Int_t * vSwitching = NULL;
     float * pSwitching = NULL;
-    int clk, clkTotal = clock();
+    clock_t clk, clkTotal = clock();
 
     assert( Abc_NtkIsStrash(pNtk) );
 
diff --git a/src/base/abci/abcMerge.c b/src/base/abci/abcMerge.c
index 917a97da..cc606488 100644
--- a/src/base/abci/abcMerge.c
+++ b/src/base/abci/abcMerge.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/abci/abcMffc.c b/src/base/abci/abcMffc.c
index f26cd233..3a911c67 100644
--- a/src/base/abci/abcMffc.c
+++ b/src/base/abci/abcMffc.c
@@ -545,7 +545,8 @@ void Abc_NktMffcTestSuper( Abc_Ntk_t * pNtk )
     Abc_Obj_t * pObj, * pFanin; 
     Vec_Int_t * vCounts, * vNumbers, * vSizes, * vMarks;
     Vec_Int_t * vNode1, * vNode2;
-    int i, k, Entry, nSizes, clk = clock();
+    int i, k, Entry, nSizes;
+    clock_t clk = clock();
     vRoots   = Abc_NktMffcMarkRoots( pNtk, 1 );
     vFanins  = Vec_PtrStart( Abc_NtkObjNumMax(pNtk) );
     vFanouts = Vec_PtrStart( Abc_NtkObjNumMax(pNtk) );
@@ -892,7 +893,8 @@ Vec_Ptr_t * Abc_NktMffcDerive( Abc_Ntk_t * pNtk, Vec_Ptr_t ** pvFanins, Vec_Ptr_
 {
     Vec_Ptr_t * vRoots, * vFanins, * vFanouts, * vVolumes, * vNodes, * vLeaves;
     Abc_Obj_t * pObj, * pFanin; 
-    int i, k, clk = clock();
+    int i, k;
+    clock_t clk = clock();
     // create roots
     vRoots   = Abc_NktMffcMarkRoots( pNtk, 0 );
     // create fanins/fanouts/volumes
@@ -1205,7 +1207,8 @@ void Abc_NktMffcServerTest( Abc_Ntk_t * pNtk )
     Vec_Ptr_t * vGlobs;
     Vec_Int_t * vGlob, * vLeaves, * vRoots;
     double Cost, CostAll = 0.0;
-    int i, k, Entry, nNodes = 0, clk = clock();
+    int i, k, Entry, nNodes = 0;
+    clock_t clk = clock();
     vGlobs  = Abc_NktMffcServer( pNtk, 18, 3 );
     vLeaves = Vec_IntAlloc( 100 );
     vRoots  = Vec_IntAlloc( 100 );
diff --git a/src/base/abci/abcNpnSave.c b/src/base/abci/abcNpnSave.c
index b57d2ef3..b99b1e52 100644
--- a/src/base/abci/abcNpnSave.c
+++ b/src/base/abci/abcNpnSave.c
@@ -392,7 +392,8 @@ void Npn_ManResize( Npn_Man_t * p )
 {
     Npn_Obj_t * pEntry, * pNext;
     int * 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/base/abci/abcNtbdd.c b/src/base/abci/abcNtbdd.c
index a1fab695..2fac9497 100644
--- a/src/base/abci/abcNtbdd.c
+++ b/src/base/abci/abcNtbdd.c
@@ -571,7 +571,8 @@ void Abc_NtkBddImplicationTest()
     DdNode * bImp, * bSum, * bTemp;
     int nVars = 200;
     int nImps = 200;
-    int i, clk;
+    int i;
+    clock_t clk;
 clk = clock();
     dd = Cudd_Init( nVars, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
     Cudd_AutodynEnable( dd, CUDD_REORDER_SIFT );
diff --git a/src/base/abci/abcOdc.c b/src/base/abci/abcOdc.c
index e0f6d6de..ff85035b 100644
--- a/src/base/abci/abcOdc.c
+++ b/src/base/abci/abcOdc.c
@@ -86,14 +86,14 @@ struct Odc_Man_t_
     int                     nTotalDcs;   // total percentage of DCs
 
     // runtime
-    int                     timeClean;   // windowing
-    int                     timeWin;     // windowing
-    int                     timeMiter;   // computing the miter
-    int                     timeSim;     // simulation
-    int                     timeQuant;   // quantification
-    int                     timeTruth;   // truth table
-    int                     timeTotal;   // useful runtime
-    int                     timeAbort;   // aborted runtime
+    clock_t                 timeClean;   // windowing
+    clock_t                 timeWin;     // windowing
+    clock_t                 timeMiter;   // computing the miter
+    clock_t                 timeSim;     // simulation
+    clock_t                 timeQuant;   // quantification
+    clock_t                 timeTruth;   // truth table
+    clock_t                 timeTotal;   // useful runtime
+    clock_t                 timeAbort;   // aborted runtime
 };
 
 
@@ -241,7 +241,7 @@ Odc_Man_t * Abc_NtkDontCareAlloc( int nVarsMax, int nLevels, int fVerbose, int f
 ***********************************************************************/
 void Abc_NtkDontCareClear( Odc_Man_t * p )
 {
-    int clk = clock();
+    clock_t clk = clock();
     // clean the structural hashing table
     if ( Vec_IntSize(p->vUsedSpots) > p->nTableSize/3 ) // more than one third
         memset( p->pTable, 0, sizeof(Odc_Lit_t) * p->nTableSize );
@@ -1033,7 +1033,7 @@ int Abc_NtkDontCareSimulateBefore( Odc_Man_t * p, unsigned * puTruth )
 int Abc_NtkDontCareCompute( Odc_Man_t * p, Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves, unsigned * puTruth )
 {
     int nMints, RetValue;
-    int clk, clkTotal = clock();
+    clock_t clk, clkTotal = clock();
 
     p->nWins++;
     
diff --git a/src/base/abci/abcPart.c b/src/base/abci/abcPart.c
index 7ae435d8..163c81b9 100644
--- a/src/base/abci/abcPart.c
+++ b/src/base/abci/abcPart.c
@@ -725,7 +725,8 @@ Vec_Ptr_t * Abc_NtkPartitionSmart( Abc_Ntk_t * pNtk, int nSuppSizeLimit, int fVe
     Vec_Ptr_t * vPartSuppsChar;
     Vec_Ptr_t * vSupps, * vPartsAll, * vPartsAll2, * vPartSuppsAll;
     Vec_Int_t * vOne, * vPart, * vPartSupp, * vTemp;
-    int i, iPart, iOut, clk, clk2, timeFind = 0;
+    int i, iPart, iOut, timeFind = 0;
+    clock_t clk, clk2;
 
     // compute the supports for all outputs
 clk = clock();
@@ -1163,7 +1164,7 @@ void Abc_NtkFraigPartitionedTime( Abc_Ntk_t * pNtk, void * pParams )
     Vec_Int_t * vOne;
     Abc_Ntk_t * pNtkAig, * pNtkFraig;
     int i;
-    int clk = clock();
+    clock_t clk = clock();
 
     // perform partitioning
     assert( Abc_NtkIsStrash(pNtk) );
diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c
index 664ddec1..c0f97530 100644
--- a/src/base/abci/abcPrint.c
+++ b/src/base/abci/abcPrint.c
@@ -1294,7 +1294,8 @@ void Abc_ObjPrint( FILE * pFile, Abc_Obj_t * pObj )
 void Abc_NtkPrintMiter( Abc_Ntk_t * pNtk )
 {
     Abc_Obj_t * pObj, * pChild, * pConst1 = Abc_AigConst1(pNtk);
-    int i, iOut = -1, Time = clock();
+    int i, iOut = -1;
+    clock_t Time = clock();
     int nUnsat = 0;
     int nSat   = 0;
     int nUndec = 0;
diff --git a/src/base/abci/abcProve.c b/src/base/abci/abcProve.c
index 3a6c42a4..f4bd89ef 100644
--- a/src/base/abci/abcProve.c
+++ b/src/base/abci/abcProve.c
@@ -60,7 +60,8 @@ int Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, void * pPars )
 {
     Prove_Params_t * pParams = (Prove_Params_t *)pPars;
     Abc_Ntk_t * pNtk, * pNtkTemp;
-    int RetValue = -1, nIter, nSatFails, Counter, clk; //, timeStart = clock();
+    int RetValue = -1, nIter, nSatFails, Counter;
+    clock_t clk; //, timeStart = clock();
     ABC_INT64_T nSatConfs, nSatInspects, nInspectLimit;
 
     // get the starting network
diff --git a/src/base/abci/abcQbf.c b/src/base/abci/abcQbf.c
index 98cb3eb6..2fec2a07 100644
--- a/src/base/abci/abcQbf.c
+++ b/src/base/abci/abcQbf.c
@@ -64,7 +64,7 @@ void Abc_NtkQbf( Abc_Ntk_t * pNtk, int nPars, int nItersMax, int fVerbose )
 {
     Abc_Ntk_t * pNtkVer, * pNtkSyn, * pNtkSyn2, * pNtkTemp;
     Vec_Int_t * vPiValues;
-    int clkTotal = clock(), clkS, clkV;
+    clock_t clkTotal = clock(), clkS, clkV;
     int nIters, nIterMax = 500, nInputs, RetValue, fFound = 0;
 
     assert( Abc_NtkIsStrash(pNtk) );
diff --git a/src/base/abci/abcQuant.c b/src/base/abci/abcQuant.c
index 7185cf8d..0951795f 100644
--- a/src/base/abci/abcQuant.c
+++ b/src/base/abci/abcQuant.c
@@ -327,10 +327,11 @@ Abc_Ntk_t * Abc_NtkReachability( Abc_Ntk_t * pNtkRel, int nIters, int fVerbose )
 {
     Abc_Obj_t * pObj;
     Abc_Ntk_t * pNtkFront, * pNtkReached, * pNtkNext, * pNtkTemp;
-    int clk, i, v, nVars, nNodesOld, nNodesNew, nNodesPrev;
+    int i, v, nVars, nNodesOld, nNodesNew, nNodesPrev;
     int fFixedPoint = 0;
     int fSynthesis  = 1;
     int fMoreEffort = 1;
+    clock_t clk;
 
     assert( Abc_NtkIsStrash(pNtkRel) );
     assert( Abc_NtkLatchNum(pNtkRel) == 0 );
diff --git a/src/base/abci/abcReach.c b/src/base/abci/abcReach.c
index e1ffa309..216dc2d2 100644
--- a/src/base/abci/abcReach.c
+++ b/src/base/abci/abcReach.c
@@ -258,7 +258,8 @@ void Abc_NtkVerifyUsingBdds( Abc_Ntk_t * pNtk, int nBddMax, int nIterMax, int fP
     DdManager * dd;
     DdNode ** pbParts;
     DdNode * bOutput, * bReached, * bInitial;
-    int i, clk = clock();
+    int i;
+    clock_t clk = clock();
 
     assert( Abc_NtkIsStrash(pNtk) );
     assert( Abc_NtkPoNum(pNtk) == 1 );
diff --git a/src/base/abci/abcRec.c b/src/base/abci/abcRec.c
index 4e5b7d6e..276f29c9 100644
--- a/src/base/abci/abcRec.c
+++ b/src/base/abci/abcRec.c
@@ -107,23 +107,23 @@ struct Abc_ManRec_t_
     int               nFunsDelayComput;         // the times delay computed, just for statistics
     int               nNoBetter;                // the number of functions found but no better than the current structures.
     // rewriting runtime
-    int               timeIfTotal;              // time used on the whole process of rewriting a structure.
-    int               timeIfComputDelay;        // time used on the structure's delay computation.
-    int               timeIfCanonicize;         // time used on canonicize the function
-    int               timeIfDerive;             // time used on derive the final network;
-    int               timeIfCopmutCur;          // time used on compute the current structures info
-    int               timeIfOther;              // time used on other things
+    clock_t           timeIfTotal;              // time used on the whole process of rewriting a structure.
+    clock_t           timeIfComputDelay;        // time used on the structure's delay computation.
+    clock_t           timeIfCanonicize;         // time used on canonicize the function
+    clock_t           timeIfDerive;             // time used on derive the final network;
+    clock_t           timeIfCopmutCur;          // time used on compute the current structures info
+    clock_t           timeIfOther;              // time used on other things
     // record runtime
-    int               timeTrim;                 // the runtime to filter the library
-    int               timeCollect;              // the runtime to collect the node of a structure.
-    int               timeTruth;                // the runtime to compute truth table.
-    int               timeCanon;                // the runtime to canonicize
-    int               timeInsert;               // the runtime to insert a structure.
-    int               timeBuild;                // the runtime to build a new structure in the library.
-    int               timeMerge;                // the runtime to merge libraries;
-    int               timeReHash;                // the runtime to resize the hash table.
-    int               timeOther;                // the runtime of other
-    int               timeTotal;                // the runtime to total.
+    clock_t           timeTrim;                 // the runtime to filter the library
+    clock_t           timeCollect;              // the runtime to collect the node of a structure.
+    clock_t           timeTruth;                // the runtime to compute truth table.
+    clock_t           timeCanon;                // the runtime to canonicize
+    clock_t           timeInsert;               // the runtime to insert a structure.
+    clock_t           timeBuild;                // the runtime to build a new structure in the library.
+    clock_t           timeMerge;                // the runtime to merge libraries;
+    clock_t           timeReHash;                // the runtime to resize the hash table.
+    clock_t           timeOther;                // the runtime of other
+    clock_t           timeTotal;                // the runtime to total.
 };
 
 
@@ -860,7 +860,7 @@ Hop_Obj_t * Abc_RecToHop( Hop_Man_t * pMan, If_Man_t * pIfMan, If_Cut_t * pCut,
     char pCanonPerm[16];
     unsigned *pInOut = s_pMan->pTemp1;
     unsigned *pTemp = s_pMan->pTemp2;
-    int time = clock();
+    clock_t time = clock();
     int fCompl;
     int * pCompl = &fCompl;
     nLeaves = If_CutLeaveNum(pCut);
@@ -1008,7 +1008,7 @@ void Abc_NtkRecFilter(int nLimit)
     Rec_Obj_t * previous = NULL, * entry = NULL, * pTemp;
     int i;
     Abc_Ntk_t * pNtk = s_pMan->pNtk;
-    int time = clock();
+    clock_t time = clock();
     if (nLimit > 0)
     {
         for ( i = 0; i < s_pMan->nBins; i++ )
@@ -1135,7 +1135,7 @@ void Abc_NtkRecLibMerge(Abc_Ntk_t* pNtk)
     int i;
     Abc_Obj_t * pObj;
     Abc_ManRec_t * p = s_pMan;
-    int clk = clock();
+    clock_t clk = clock();
     if ( Abc_NtkPiNum(pNtk) > s_pMan->nVars )
     {
         printf( "The library has more inputs than the record.\n");
@@ -1183,7 +1183,7 @@ void Abc_NtkRecRezieHash(Abc_ManRec_t* p)
     Rec_Obj_t ** pBinsNew, **ppSpot;
     Rec_Obj_t * pEntry, * pTemp;
     int nBinsNew, Counter, i;
-    int clk = clock();
+    clock_t clk = clock();
     // get the new table size
     nBinsNew = Cudd_Prime( 3 * p->nBins ); 
     printf("Hash table resize from %d to %d.\n", p->nBins, nBinsNew);
@@ -1232,7 +1232,7 @@ void Abc_NtkRecStart( Abc_Ntk_t * pNtk, int nVars, int nCuts, int fTrim )
     char Buffer[10];
     unsigned * pTruth;
     int i, RetValue;
-    int clkTotal = clock(), clk, timeInsert;
+    clock_t clkTotal = clock(), clk, timeInsert;
     //int testNum = 0;
 
     assert( s_pMan == NULL );
@@ -1690,7 +1690,7 @@ void Abc_NtkRecAdd( Abc_Ntk_t * pNtk, int fUseSOPB)
 
     If_Par_t Pars, * pPars = &Pars;
     Abc_Ntk_t * pNtkNew;
-    int clk = clock();
+    clock_t clk = clock();
 
     if ( Abc_NtkGetChoiceNum( pNtk ) )
         printf( "Performing renoding with choices.\n" );
@@ -2068,7 +2068,7 @@ void Abc_NtkRecAddSOPB( If_Man_t * pIfMan, If_Cut_t * pCut, unsigned* pInOut, ch
     If_And_t This;
     Rec_Obj_t ** ppSpot;
     char Buffer[40], Name[20], Truth[20];
-    int timeBuild = clock();
+    clock_t timeBuild = clock();
     unsigned * pTruth;
     vAnds = If_CutDelaySopArray( pIfMan, pCut );
     if(Vec_WrdSize(vAnds) > nLeaves + 3*(nLeaves-1) + s_MaxSize[nLeaves])
@@ -2778,7 +2778,7 @@ void SetUseCut(If_Cut_t* pCut, Rec_Obj_t * pRecObj, char * pCanonPerm)
 int If_CutDelayRecCost(If_Man_t* p, If_Cut_t* pCut, If_Obj_t * pObj)
 {
     //int fVerbose = 0;
-    int timeDelayComput, timeTotal = clock(), timeCanonicize;
+    clock_t timeDelayComput, timeTotal = clock(), timeCanonicize;
     int nLeaves, i, DelayMin = ABC_INFINITY , * pDelayBest = &DelayMin;
     char pCanonPerm[16];
     unsigned uCanonPhase;
diff --git a/src/base/abci/abcRefactor.c b/src/base/abci/abcRefactor.c
index 69d84b0c..361b91ce 100644
--- a/src/base/abci/abcRefactor.c
+++ b/src/base/abci/abcRefactor.c
@@ -50,15 +50,15 @@ struct Abc_ManRef_t_
     int              nNodesBeg;
     int              nNodesEnd;
     // runtime statistics
-    int              timeCut;
-    int              timeBdd;
-    int              timeDcs;
-    int              timeSop;
-    int              timeFact;
-    int              timeEval;
-    int              timeRes;
-    int              timeNtk;
-    int              timeTotal;
+    clock_t          timeCut;
+    clock_t          timeBdd;
+    clock_t          timeDcs;
+    clock_t          timeSop;
+    clock_t          timeFact;
+    clock_t          timeEval;
+    clock_t          timeRes;
+    clock_t          timeNtk;
+    clock_t          timeTotal;
 };
  
 static void           Abc_NtkManRefPrintStats( Abc_ManRef_t * p );
@@ -95,7 +95,7 @@ int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, int f
     Dec_Graph_t * pFForm;
     Vec_Ptr_t * vFanins;
     Abc_Obj_t * pNode;
-    int clk, clkStart = clock();
+    clock_t clk, clkStart = clock();
     int i, nNodes;
 
     assert( Abc_NtkIsStrash(pNtk) );
diff --git a/src/base/abci/abcRestruct.c b/src/base/abci/abcRestruct.c
index 66b1d8e8..4be177f7 100644
--- a/src/base/abci/abcRestruct.c
+++ b/src/base/abci/abcRestruct.c
@@ -107,7 +107,7 @@ int Abc_NtkRestructure( Abc_Ntk_t * pNtk, int nCutMax, int fUpdateLevel, int fUs
     Cut_Cut_t * pCutList;
     Dec_Graph_t * pGraph;
     Abc_Obj_t * pNode;
-    int clk, clkStart = clock();
+    clock_t clk, clkStart = clock();
     int fMulti = 1;
     int fResub = 0;
     int i, nNodes;
diff --git a/src/base/abci/abcResub.c b/src/base/abci/abcResub.c
index b03c36aa..6e2b95c3 100644
--- a/src/base/abci/abcResub.c
+++ b/src/base/abci/abcResub.c
@@ -62,18 +62,18 @@ struct Abc_ManRes_t_
     // other data
     Vec_Ptr_t        * vTemp;      // temporary array of nodes
     // runtime statistics
-    int                timeCut;
-    int                timeTruth;
-    int                timeRes;
-    int                timeDiv;
-    int                timeMffc;
-    int                timeSim;
-    int                timeRes1;
-    int                timeResD;
-    int                timeRes2;
-    int                timeRes3;
-    int                timeNtk;
-    int                timeTotal;
+    clock_t            timeCut;
+    clock_t            timeTruth;
+    clock_t            timeRes;
+    clock_t            timeDiv;
+    clock_t            timeMffc;
+    clock_t            timeSim;
+    clock_t            timeRes1;
+    clock_t            timeResD;
+    clock_t            timeRes2;
+    clock_t            timeRes3;
+    clock_t            timeNtk;
+    clock_t            timeTotal;
     // improvement statistics
     int                nUsedNodeC;
     int                nUsedNode0;
@@ -144,7 +144,7 @@ int Abc_NtkResubstitute( Abc_Ntk_t * pNtk, int nCutMax, int nStepsMax, int nLeve
     Dec_Graph_t * pFForm;
     Vec_Ptr_t * vLeaves;
     Abc_Obj_t * pNode;
-    int clk, clkStart = clock();
+    clock_t clk, clkStart = clock();
     int i, nNodes;
 
     assert( Abc_NtkIsStrash(pNtk) );
@@ -1624,7 +1624,7 @@ Dec_Graph_t * Abc_ManResubEval( Abc_ManRes_t * p, Abc_Obj_t * pRoot, Vec_Ptr_t *
     extern int Abc_NodeMffcInside( Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vInside );
     Dec_Graph_t * pGraph;
     int Required;
-    int clk;
+    clock_t clk;
 
     Required = fUpdateLevel? Abc_ObjRequiredLevel(pRoot) : ABC_INFINITY;
 
diff --git a/src/base/abci/abcRewrite.c b/src/base/abci/abcRewrite.c
index 5e2745b9..091ac647 100644
--- a/src/base/abci/abcRewrite.c
+++ b/src/base/abci/abcRewrite.c
@@ -68,7 +68,7 @@ int Abc_NtkRewrite( Abc_Ntk_t * pNtk, int fUpdateLevel, int fUseZeros, int fVerb
 //    Vec_Ptr_t * vAddedCells = NULL, * vUpdatedNets = NULL;
     Dec_Graph_t * pGraph;
     int i, nNodes, nGain, fCompl;
-    int clk, clkStart = clock();
+    clock_t clk, clkStart = clock();
 
     assert( Abc_NtkIsStrash(pNtk) );
     // cleanup the AIG
diff --git a/src/base/abci/abcRr.c b/src/base/abci/abcRr.c
index 61c8d085..83b7e85e 100644
--- a/src/base/abci/abcRr.c
+++ b/src/base/abci/abcRr.c
@@ -56,11 +56,11 @@ struct Abc_RRMan_t_
     int              nLevelsOld;       // the old number of levels
     int              nEdgesTried;      // the number of nodes tried
     int              nEdgesRemoved;    // the number of nodes proved
-    int              timeWindow;       // the time to construct the window
-    int              timeMiter;        // the time to construct the miter
-    int              timeProve;        // the time to prove the miter
-    int              timeUpdate;       // the network update time
-    int              timeTotal;        // the total runtime
+    clock_t          timeWindow;       // the time to construct the window
+    clock_t          timeMiter;        // the time to construct the miter
+    clock_t          timeProve;        // the time to prove the miter
+    clock_t          timeUpdate;       // the network update time
+    clock_t          timeTotal;        // the total runtime
 };
 
 static Abc_RRMan_t * Abc_RRManStart();
@@ -100,7 +100,8 @@ int Abc_NtkRR( Abc_Ntk_t * pNtk, int nFaninLevels, int nFanoutLevels, int fUseFa
     ProgressBar * pProgress;
     Abc_RRMan_t * p;
     Abc_Obj_t * pNode, * pFanin, * pFanout;
-    int i, k, m, nNodes, RetValue, clk, clkTotal = clock();
+    int i, k, m, nNodes, RetValue;
+    clock_t clk, clkTotal = clock();
     // start the manager
     p = Abc_RRManStart();
     p->pNtk          = pNtk;
@@ -351,7 +352,8 @@ void Abc_RRManClean( Abc_RRMan_t * p )
 int Abc_NtkRRProve( Abc_RRMan_t * p )
 {
     Abc_Ntk_t * pWndCopy;
-    int RetValue, clk;
+    int RetValue;
+    clock_t clk;
 //    Abc_NtkShowAig( p->pWnd, 0 );
     pWndCopy = Abc_NtkDup( p->pWnd );
     Abc_NtkRRUpdate( pWndCopy, p->pNode->pCopy->pCopy, p->pFanin->pCopy->pCopy, p->pFanout? p->pFanout->pCopy->pCopy : NULL );
diff --git a/src/base/abci/abcSat.c b/src/base/abci/abcSat.c
index 29f13bda..a10be364 100644
--- a/src/base/abci/abcSat.c
+++ b/src/base/abci/abcSat.c
@@ -54,7 +54,8 @@ int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsL
 {
     sat_solver * pSat;
     lbool   status;
-    int RetValue, clk;
+    int RetValue;
+    clock_t clk;
  
     if ( pNumConfs )
         *pNumConfs = 0;
diff --git a/src/base/abci/abcSymm.c b/src/base/abci/abcSymm.c
index 2a36be14..29927563 100644
--- a/src/base/abci/abcSymm.c
+++ b/src/base/abci/abcSymm.c
@@ -89,7 +89,7 @@ void Abc_NtkSymmetriesUsingSandS( Abc_Ntk_t * pNtk, int fVerbose )
 void Abc_NtkSymmetriesUsingBdds( Abc_Ntk_t * pNtk, int fNaive, int fReorder, int fVerbose )
 {
     DdManager * dd;
-    int clk, clkBdd, clkSym;
+    clock_t clk, clkBdd, clkSym;
     int fGarbCollect = 1;
 
     // compute the global functions
diff --git a/src/base/abci/abcUnate.c b/src/base/abci/abcUnate.c
index a56973b6..870b462b 100644
--- a/src/base/abci/abcUnate.c
+++ b/src/base/abci/abcUnate.c
@@ -73,8 +73,9 @@ void Abc_NtkPrintUnateBdd( Abc_Ntk_t * pNtk, int fUseNaive, int fVerbose )
 //    DdNode ** pbGlobal;     // temporary storage for global BDDs
     int TotalSupps = 0;
     int TotalUnate = 0;
-    int i, clk = clock();
-    int clkBdd, clkUnate;
+    int i;
+    clock_t clk = clock();
+    clock_t clkBdd, clkUnate;
 
     // compute the global BDDs
     dd = (DdManager *)Abc_NtkBuildGlobalBdds(pNtk, 10000000, 1, 1, fVerbose);
diff --git a/src/base/cmd/cmdPlugin.c b/src/base/cmd/cmdPlugin.c
index f14eed55..e6b36f2a 100644
--- a/src/base/cmd/cmdPlugin.c
+++ b/src/base/cmd/cmdPlugin.c
@@ -417,7 +417,8 @@ int Cmd_CommandAbcPlugIn( Abc_Frame_t * pAbc, int argc, char ** argv )
     Vec_Int_t * vCex;
     FILE * pFile;
     Gia_Man_t * pGia;
-    int i, fd, clk;
+    int i, fd;
+    clock_t clk;
     int fLeaveFiles;
 /*
     Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
diff --git a/src/base/io/ioReadAiger.c b/src/base/io/ioReadAiger.c
index 0644aed9..8ff32ac9 100644
--- a/src/base/io/ioReadAiger.c
+++ b/src/base/io/ioReadAiger.c
@@ -25,7 +25,6 @@
 #include <stdlib.h>
 #include <string.h>
 #include <assert.h>
-#include <time.h>
 
 #include "src/misc/bzlib/bzlib.h"
 #include "src/misc/zlib/zlib.h"
diff --git a/src/base/io/ioReadBblif.c b/src/base/io/ioReadBblif.c
index 873a5671..ee7c5ee7 100644
--- a/src/base/io/ioReadBblif.c
+++ b/src/base/io/ioReadBblif.c
@@ -164,7 +164,8 @@ Abc_Ntk_t * Bbl_ManToAig( Bbl_Man_t * p )
     Bbl_Obj_t * pObj, * pFanin;
     Vec_Ptr_t * vCopy, * vNodes, * vFaninAigs;
     Dec_Graph_t ** pFForms;
-    int i, clk;
+    int i;
+    clock_t clk;
 clk = clock();
     // map SOP handles into factored forms
     pFForms = ABC_CALLOC( Dec_Graph_t *, Bbl_ManFncSize(p) );
@@ -270,7 +271,7 @@ void Bbl_ManTest( Abc_Ntk_t * pNtk )
     Abc_Ntk_t * pNtkNew;
     Bbl_Man_t * p, * pNew;
     char * pFileName = "test.bblif";
-    int clk, clk1, clk2, clk3, clk4, clk5;
+    clock_t clk, clk1, clk2, clk3, clk4, clk5;
 clk = clock();
     p = Bbl_ManFromAbc( pNtk );
     Bbl_ManPrintStats( p );
diff --git a/src/base/io/ioWriteAiger.c b/src/base/io/ioWriteAiger.c
index a22d16ba..ef2be673 100644
--- a/src/base/io/ioWriteAiger.c
+++ b/src/base/io/ioWriteAiger.c
@@ -25,8 +25,6 @@
 #include <stdlib.h>
 #include <string.h>
 #include <assert.h>
-#include <time.h>
-#include <stdarg.h>
 
 #include "src/misc/bzlib/bzlib.h"
 #include "src/misc/zlib/zlib.h"