Fixing time primtouts throughout the code.

26 files changed, 99 insertions, 82 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index a5c075c3..0d97dd61 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.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/misc/util/utilCex.h"
diff --git a/src/aig/gia/giaAbsGla.c b/src/aig/gia/giaAbsGla.c
index 1a4e9cd2..c25c6e48 100644
--- a/src/aig/gia/giaAbsGla.c
+++ b/src/aig/gia/giaAbsGla.c
@@ -800,13 +800,10 @@ Vec_Int_t * Gla_ManRefinement( Gla_Man_t * p )
 
     // select objects
     vSelect = Vec_IntAlloc( 100 );
-//    Vec_IntFill( p->vPrioSels, Vec_IntSize(vPPis)+1, 0 );
     Vec_IntFill( p->vObjCounts, p->pPars->iFrame+1, 0 );
     Gla_ManRefSelect_rec( p, Gia_ObjFanin0(Gia_ManPo(p->pGia, 0)), p->pPars->iFrame, vSelect, Sign );
     Vec_IntUniqify( vSelect );
 
-//    printf( "\nSelected %d.\n", Vec_IntSize(vSelect) );
-
 /*
     for ( f = 0; f < p->pPars->iFrame; f++ )
         printf( "%2d", Vec_IntEntry(p->vObjCounts, f) );
@@ -976,7 +973,6 @@ Gla_Man_t * Gla_ManStart( Gia_Man_t * pGia0, Gia_ParVta_t * pPars )
     p->pGia = Gia_ManDupMapped( pGia0, p->pCnf->vMapping );
     if ( pPars->fPropFanout )
         Gia_ManStaticFanoutStart( p->pGia );
-//printf( "Old GIA = %d.  New GIA = %d.\n", Gia_ManObjNum(pGia0), Gia_ManObjNum(p->pGia) );
 
     // derive new gate map
     assert( pGia0->vGateClasses != 0 );
@@ -1797,7 +1793,7 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta )
     p->timeInit = clock() - clk;
     // set runtime limit
     if ( p->pPars->nTimeOut )
-        sat_solver2_set_runtime_limit( p->pSat, time(NULL) + p->pPars->nTimeOut - 1 );
+        sat_solver2_set_runtime_limit( p->pSat, p->pPars->nTimeOut * CLOCKS_PER_SEC + clock() );
     // perform initial abstraction
     if ( p->pPars->fVerbose )
     {
@@ -1831,9 +1827,9 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta )
                 goto finish;
             }
             // check timeout
-            if ( p->pSat->nRuntimeLimit && time(NULL) > p->pSat->nRuntimeLimit )
+            if ( p->pSat->nRuntimeLimit && clock() > p->pSat->nRuntimeLimit )
             {
-                Gla_ManRollBack( p ); // 1155046
+                Gla_ManRollBack( p );
                 goto finish;
             }
             if ( vCore != NULL )
@@ -1960,7 +1956,7 @@ finish:
         pAig->vGateClasses = Gla_ManTranslate( p );
         if ( Status == -1 )
         {
-            if ( p->pPars->nTimeOut && time(NULL) >= p->pSat->nRuntimeLimit ) 
+            if ( p->pPars->nTimeOut && clock() >= p->pSat->nRuntimeLimit ) 
                 Abc_Print( 1, "SAT solver ran out of time at %d sec in frame %d.  ", p->pPars->nTimeOut, f );
             else if ( pPars->nConfLimit && sat_solver2_nconflicts(p->pSat) >= pPars->nConfLimit )
                 Abc_Print( 1, "SAT solver ran out of resources at %d conflicts in frame %d.  ", pPars->nConfLimit, f );
diff --git a/src/aig/gia/giaAbsVta.c b/src/aig/gia/giaAbsVta.c
index 7b66b7dd..11c84853 100644
--- a/src/aig/gia/giaAbsVta.c
+++ b/src/aig/gia/giaAbsVta.c
@@ -1564,7 +1564,7 @@ int Gia_VtaPerformInt( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
     p = Vga_ManStart( pAig, pPars );
     // set runtime limit
     if ( p->pPars->nTimeOut )
-        sat_solver2_set_runtime_limit( p->pSat, time(NULL) + p->pPars->nTimeOut - 1 );
+        sat_solver2_set_runtime_limit( p->pSat, p->pPars->nTimeOut * CLOCKS_PER_SEC + clock() );
     // perform initial abstraction
     if ( p->pPars->fVerbose )
     {
@@ -1609,7 +1609,7 @@ int Gia_VtaPerformInt( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
                 goto finish;
             }
             // check timeout
-            if ( p->pSat->nRuntimeLimit && time(NULL) > p->pSat->nRuntimeLimit )
+            if ( p->pSat->nRuntimeLimit && clock() > p->pSat->nRuntimeLimit )
             {
                 Vga_ManRollBack( p, nObjOld );
                 goto finish;
@@ -1716,7 +1716,7 @@ finish:
             pAig->vObjClasses = Gia_VtaFramesToAbs( (Vec_Vec_t *)p->vCores );
             if ( Status == -1 )
             {
-                if ( p->pPars->nTimeOut && time(NULL) >= p->pSat->nRuntimeLimit ) 
+                if ( p->pPars->nTimeOut && clock() >= p->pSat->nRuntimeLimit ) 
                     Abc_Print( 1, "SAT solver ran out of time at %d sec in frame %d.  ", p->pPars->nTimeOut, f );
                 else if ( pPars->nConfLimit && sat_solver2_nconflicts(p->pSat) >= pPars->nConfLimit )
                     Abc_Print( 1, "SAT solver ran out of resources at %d conflicts in frame %d.  ", pPars->nConfLimit, f );
diff --git a/src/aig/gia/giaCCof.c b/src/aig/gia/giaCCof.c
index 6fbd1095..ce863051 100644
--- a/src/aig/gia/giaCCof.c
+++ b/src/aig/gia/giaCCof.c
@@ -219,8 +219,9 @@ int Gia_ManCofOneDerive( Ccf_Man_t * p, int LitProp )
 ***********************************************************************/
 int Gia_ManCofGetReachable( Ccf_Man_t * p, int Lit )
 {
-    int ObjPrev = 0, ConfPrev = 0, clk;
+    int ObjPrev = 0, ConfPrev = 0;
     int Count = 0, LitOut, RetValue;
+    clock_t clk;
     // try solving for the first time and quit if converged
     RetValue = sat_solver_solve( p->pSat, &Lit, &Lit + 1, p->nConfMax, 0, 0, 0 );
     if ( RetValue == l_False )
@@ -268,8 +269,8 @@ Gia_Man_t * Gia_ManCofTest( Gia_Man_t * pGia, int nFrameMax, int nConfMax, int n
     Ccf_Man_t * p;
     Gia_Obj_t * pObj;
     int f, i, Lit, RetValue = -1, fFailed = 0;
-    int nTimeToStop = time(NULL) + nTimeMax;
-    int clk = clock();
+    clock_t nTimeToStop = clock() + nTimeMax * CLOCKS_PER_SEC;
+    clock_t clk = clock();
     assert( Gia_ManPoNum(pGia) == 1 );
 
     // create reachability manager
@@ -309,7 +310,7 @@ Gia_Man_t * Gia_ManCofTest( Gia_Man_t * pGia, int nFrameMax, int nConfMax, int n
     }
 
     // report the result
-    if ( nTimeToStop && time(NULL) > nTimeToStop )
+    if ( nTimeToStop && clock() > nTimeToStop )
         printf( "Runtime limit (%d sec) is reached after %d frames.  ", nTimeMax, f );
     else if ( f == nFrameMax )
         printf( "Completed %d frames without converging.  ", f );
diff --git a/src/aig/gia/giaCSat.c b/src/aig/gia/giaCSat.c
index d83f79e9..b4bc5b3e 100644
--- a/src/aig/gia/giaCSat.c
+++ b/src/aig/gia/giaCSat.c
@@ -81,10 +81,10 @@ struct Cbs_Man_t_
     int           nConfSat;     // conflicts in sat problems
     int           nConfUndec;   // conflicts in undec problems
     // runtime stats
-    int           timeSatUnsat; // unsat
-    int           timeSatSat;   // sat
-    int           timeSatUndec; // undecided
-    int           timeTotal;    // total runtime
+    clock_t       timeSatUnsat; // unsat
+    clock_t       timeSatSat;   // sat
+    clock_t       timeSatUndec; // undecided
+    clock_t       timeTotal;    // total runtime
 };
 
 static inline int   Cbs_VarIsAssigned( Gia_Obj_t * pVar )      { return pVar->fMark0;                        }
@@ -1003,7 +1003,8 @@ Vec_Int_t * Cbs_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvSt
     Vec_Int_t * vCex, * vVisit, * vCexStore;
     Vec_Str_t * vStatus;
     Gia_Obj_t * pRoot; 
-    int i, status, clk, clkTotal = clock();
+    int i, status;
+    clock_t clk, clkTotal = clock();
     assert( Gia_ManRegNum(pAig) == 0 );
 //    Gia_ManCollectTest( pAig );
     // prepare AIG
diff --git a/src/aig/gia/giaCSatOld.c b/src/aig/gia/giaCSatOld.c
index 8198c17f..1dd4a425 100644
--- a/src/aig/gia/giaCSatOld.c
+++ b/src/aig/gia/giaCSatOld.c
@@ -73,10 +73,10 @@ struct Cbs0_Man_t_
     int           nConfSat;     // conflicts in sat problems
     int           nConfUndec;   // conflicts in undec problems
     // runtime stats
-    int           timeSatUnsat; // unsat
-    int           timeSatSat;   // sat
-    int           timeSatUndec; // undecided
-    int           timeTotal;    // total runtime
+    clock_t       timeSatUnsat; // unsat
+    clock_t       timeSatSat;   // sat
+    clock_t       timeSatUndec; // undecided
+    clock_t       timeTotal;    // total runtime
 };
 
 static inline int   Cbs0_VarIsAssigned( Gia_Obj_t * pVar )      { return pVar->fMark0;                        }
@@ -712,7 +712,8 @@ Vec_Int_t * Cbs_ManSolveMiter( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvStat
     Vec_Int_t * vCex, * vVisit, * vCexStore;
     Vec_Str_t * vStatus;
     Gia_Obj_t * pRoot; 
-    int i, status, clk, clkTotal = clock();
+    int i, status;
+    clock_t clk, clkTotal = clock();
     assert( Gia_ManRegNum(pAig) == 0 );
     // prepare AIG
     Gia_ManCreateRefs( pAig );
diff --git a/src/aig/gia/giaCTas.c b/src/aig/gia/giaCTas.c
index 8cfa9efc..6dd0e0fa 100644
--- a/src/aig/gia/giaCTas.c
+++ b/src/aig/gia/giaCTas.c
@@ -108,10 +108,10 @@ struct Tas_Man_t_
     int           nConfSat;     // conflicts in sat problems
     int           nConfUndec;   // conflicts in undec problems
     // runtime stats
-    int           timeSatUnsat; // unsat
-    int           timeSatSat;   // sat
-    int           timeSatUndec; // undecided
-    int           timeTotal;    // total runtime
+    clock_t       timeSatUnsat; // unsat
+    clock_t       timeSatSat;   // sat
+    clock_t       timeSatUndec; // undecided
+    clock_t       timeTotal;    // total runtime
 };
 
 static inline int   Tas_VarIsAssigned( Gia_Obj_t * pVar )      { return pVar->fMark0;                        }
@@ -1524,7 +1524,8 @@ Vec_Int_t * Tas_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvSt
     Gia_Obj_t * pRoot;//, * pRootCopy; 
 //    Gia_Man_t * pAigCopy = Gia_ManDup( pAig ), * pAigTemp;
 
-    int i, status, clk, clkTotal = clock();
+    int i, status;
+    clock_t clk, clkTotal = clock();
     assert( Gia_ManRegNum(pAig) == 0 );
 //    Gia_ManCollectTest( pAig );
     // prepare AIG
@@ -1703,7 +1704,8 @@ void Tas_ManSolveMiterNc2( Gia_Man_t * pAig, int nConfs, Gia_Man_t * pAigOld, Ve
     Vec_Int_t * vCex, * vVisit, * vCexStore;
     Vec_Str_t * vStatus;
     Gia_Obj_t * pRoot, * pOldRoot; 
-    int i, status, clk, clkTotal = clock();
+    int i, status;
+    clock_t clk, clkTotal = clock();
     int Tried = 0, Stored = 0, Step = Gia_ManCoNum(pAig) / nPatMax;
     assert( Gia_ManRegNum(pAig) == 0 );
 //    Gia_ManCollectTest( pAig );
diff --git a/src/aig/gia/giaCTas2.c b/src/aig/gia/giaCTas2.c
index 855dcdd3..2b1d7169 100644
--- a/src/aig/gia/giaCTas2.c
+++ b/src/aig/gia/giaCTas2.c
@@ -115,10 +115,10 @@ struct Tas_Man_t_
     int           nConfUndec;   // conflicts in undec problems
     int           nConfTotal;   // total conflicts
     // runtime stats
-    int           timeSatUnsat; // unsat
-    int           timeSatSat;   // sat
-    int           timeSatUndec; // undecided
-    int           timeTotal;    // total runtime
+    clock_t       timeSatUnsat; // unsat
+    clock_t       timeSatSat;   // sat
+    clock_t       timeSatUndec; // undecided
+    clock_t       timeTotal;    // total runtime
 };
 
 static inline int         Tas_VarIsAssigned( Tas_Var_t * pVar )        { return pVar->fAssign;                                      }
diff --git a/src/aig/gia/giaCof.c b/src/aig/gia/giaCof.c
index cf8ecf00..68d269cd 100644
--- a/src/aig/gia/giaCof.c
+++ b/src/aig/gia/giaCof.c
@@ -672,7 +672,7 @@ void Cof_ManPrintFanio( Cof_Man_t * p )
 void Gia_ManPrintFanio( Gia_Man_t * pGia, int nNodes )
 {
     Cof_Man_t * p;
-    int clk = clock();
+    clock_t clk = clock();
     p = Cof_ManCreateLogicSimple( pGia );
     p->nLevels = 1 + Gia_ManLevelNum( pGia );
     p->pLevels = ABC_CALLOC( int, p->nLevels );
diff --git a/src/aig/gia/giaDfs.c b/src/aig/gia/giaDfs.c
index 1ec18767..1da2da1f 100644
--- a/src/aig/gia/giaDfs.c
+++ b/src/aig/gia/giaDfs.c
@@ -209,7 +209,8 @@ void Gia_ManCollectTest( Gia_Man_t * p )
 {
     Vec_Int_t * vNodes;
     Gia_Obj_t * pObj;
-    int i, iNode, clk = clock();
+    int i, iNode;
+    clock_t clk = clock();
     vNodes = Vec_IntAlloc( 100 );
     Gia_ManIncrementTravId( p );
     Gia_ManForEachCo( p, pObj, i )
@@ -275,7 +276,8 @@ int Gia_ManSuppSizeOne( Gia_Man_t * p, Gia_Obj_t * pObj )
 int Gia_ManSuppSizeTest( Gia_Man_t * p )
 {
     Gia_Obj_t * pObj;
-    int i, Counter = 0, clk = clock();
+    int i, Counter = 0;
+    clock_t clk = clock();
     Gia_ManForEachObj( p, pObj, i )
         if ( Gia_ObjIsAnd(pObj) )
             Counter += (Gia_ManSuppSizeOne(p, pObj) <= 16);
diff --git a/src/aig/gia/giaEmbed.c b/src/aig/gia/giaEmbed.c
index 1daf52a1..f71281cb 100644
--- a/src/aig/gia/giaEmbed.c
+++ b/src/aig/gia/giaEmbed.c
@@ -838,7 +838,8 @@ int Emb_ManComputeDistance_old( Emb_Man_t * p, Emb_Obj_t * pPivot )
 void Gia_ManTestDistanceInternal( Emb_Man_t * p )
 {
     int nAttempts = 20;
-    int i, iNode, Dist, clk;
+    int i, iNode, Dist;
+    clock_t clk;
     Emb_Obj_t * pPivot, * pNext;
     Gia_ManRandom( 1 );
     Emb_ManResetTravId( p );
@@ -903,7 +904,7 @@ void Gia_ManTestDistanceInternal( Emb_Man_t * p )
 void Gia_ManTestDistance( Gia_Man_t * pGia )
 {
     Emb_Man_t * p;
-    int clk = clock();
+    clock_t clk = clock();
     p = Emb_ManStart( pGia );
 //    Emb_ManPrintFanio( p );
     Emb_ManPrintStats( p );
@@ -1529,7 +1530,7 @@ void Emb_ManPlacementRefine( Emb_Man_t * p, int nIters, int fVerbose )
     float VertX, VertY;
     int * pPermX, * pPermY;
     int i, k, Iter, iMinX, iMaxX, iMinY, iMaxY;
-    int clk = clock();
+    clock_t clk = clock();
     if ( p->pPlacement == NULL )
         return;
     pEdgeX = ABC_ALLOC( float, p->nObjs );
@@ -1790,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, clk, clkSetup;
+    int i, clkSetup;
+    clock_t clk;
 //   Gia_ManTestDistance( pGia );
 
     // transform AIG into internal data-structure
diff --git a/src/aig/gia/giaEra.c b/src/aig/gia/giaEra.c
index 672149bc..03832e4a 100644
--- a/src/aig/gia/giaEra.c
+++ b/src/aig/gia/giaEra.c
@@ -501,7 +501,8 @@ int Gia_ManCollectReachable( Gia_Man_t * pAig, int nStatesMax, int fMiter, int f
 { 
     Gia_ManEra_t * p;
     Gia_ObjEra_t * pState;
-    int Hash, clk = clock();
+    int Hash;
+    clock_t clk = clock();
     int RetValue = 1;
     assert( Gia_ManPiNum(pAig) <= 12 );
     assert( Gia_ManRegNum(pAig) > 0 );
diff --git a/src/aig/gia/giaEra2.c b/src/aig/gia/giaEra2.c
index 265335e2..f5f9fdb3 100644
--- a/src/aig/gia/giaEra2.c
+++ b/src/aig/gia/giaEra2.c
@@ -1536,7 +1536,8 @@ int Gia_ManAreDeriveNexts_rec( Gia_ManAre_t * p, Gia_PtrAre_t Sta )
     Gia_Obj_t * pPivot;
     Vec_Int_t * vLits, * vTfos;
     Gia_Obj_t * pObj;
-    int i, clk;
+    int i;
+    clock_t clk;
     if ( ++p->nRecCalls == MAX_CALL_NUM )
         return 0;
     if ( (pPivot = Gia_ManAreMostUsedPi(p)) == NULL )
@@ -1611,7 +1612,8 @@ int Gia_ManAreDeriveNexts( Gia_ManAre_t * p, Gia_PtrAre_t Sta )
 {
     Gia_StaAre_t * pSta;
     Gia_Obj_t * pObj;
-    int i, RetValue, clk = clock();
+    int i, RetValue;
+    clock_t clk = clock();
     pSta = Gia_ManAreSta( p, Sta );
     if ( Gia_StaIsUnused(pSta) )
         return 0;
@@ -1671,7 +1673,7 @@ int Gia_ManAreDeriveNexts( Gia_ManAre_t * p, Gia_PtrAre_t Sta )
   SeeAlso     []
 
 ***********************************************************************/
-void Gia_ManArePrintReport( Gia_ManAre_t * p, int Time, int fFinal )
+void Gia_ManArePrintReport( Gia_ManAre_t * p, clock_t Time, int fFinal )
 {
     printf( "States =%10d. Reached =%10d. R = %5.3f. Depth =%6d. Mem =%9.2f Mb.  ", 
         p->iStaCur, p->nStas, 1.0*p->iStaCur/p->nStas, Gia_ManAreDepth(p, p->iStaCur), 
@@ -1703,7 +1705,7 @@ int Gia_ManArePerform( Gia_Man_t * pAig, int nStatesMax, int fMiter, int fVerbos
 //    extern Gia_Man_t * Gia_ManCompress2( Gia_Man_t * p, int fUpdateLevel, int fVerbose );
     extern Abc_Cex_t * Gia_ManAreDeriveCex( Gia_ManAre_t * p, Gia_StaAre_t * pLast );
     Gia_ManAre_t * p;
-    int clk = clock();
+    clock_t clk = clock();
     int RetValue = 1;
     if ( Gia_ManRegNum(pAig) > MAX_VARS_NUM )
     {
diff --git a/src/aig/gia/giaForce.c b/src/aig/gia/giaForce.c
index 94ad069b..a905b220 100644
--- a/src/aig/gia/giaForce.c
+++ b/src/aig/gia/giaForce.c
@@ -892,7 +892,7 @@ void Frc_ManPlacementRefine( Frc_Man_t * p, int nIters, int fVerbose )
     float * pVertX, VertX;
     int * pPermX, * pHandles;
     int k, h, Iter, iMinX, iMaxX, Counter, nCutStart, nCutCur, nCutCur2, nCutPrev;
-    int clk = clock(), clk2, clk2Total = 0;
+    clock_t clk = clock(), clk2, clk2Total = 0;
     // create starting one-dimensional placement
     vCoOrder = Frc_ManCollectCos( p );
     if ( fRandomize )
@@ -1068,7 +1068,7 @@ void For_ManFileExperiment()
     FILE * pFile;
     int * pBuffer;
     int i, Size, Exp = 25;
-    int clk = clock();
+    clock_t clk = clock();
     int RetValue;
 
     Size = (1 << Exp);
diff --git a/src/aig/gia/giaFrames.c b/src/aig/gia/giaFrames.c
index 48a0568e..f3dbd95c 100644
--- a/src/aig/gia/giaFrames.c
+++ b/src/aig/gia/giaFrames.c
@@ -226,7 +226,7 @@ Gia_ManUnr_t * Gia_ManUnrStart( Gia_Man_t * pAig, Gia_ParFra_t * pPars )
     Gia_ManUnr_t * p;
     Gia_Obj_t * pObj;
     int i, k, iRank, iFanin, Degree, Shift;
-    int clk = clock();
+    clock_t clk = clock();
 
     p = ABC_CALLOC( Gia_ManUnr_t, 1 );
     p->pAig   = pAig;
@@ -605,7 +605,7 @@ Gia_Man_t * Gia_ManUnroll( Gia_ManUnr_t * p )
 Gia_Man_t * Gia_ManFrames2( Gia_Man_t * pAig, Gia_ParFra_t * pPars )
 {
     Gia_Man_t * pNew;
-    int clk = clock();
+    clock_t clk = clock();
     pNew = Gia_ManUnroll( pAig, pPars );
     if ( pPars->fVerbose )
         Abc_PrintTime( 1, "Time", clock() - clk );
diff --git a/src/aig/gia/giaGiarf.c b/src/aig/gia/giaGiarf.c
index 2f18c16d..1e2d1d18 100644
--- a/src/aig/gia/giaGiarf.c
+++ b/src/aig/gia/giaGiarf.c
@@ -764,7 +764,7 @@ int Gia_ComputeEquivalencesLevel( Hcd_Man_t * p, Gia_Man_t * pGiaLev, Vec_Ptr_t
     Gia_Obj_t * pRoot, * pMember, * pMemberPrev, * pRepr, * pTempRepr;
     int i, k, nIter, iRoot, iRootNew, iMember, iMemberPrev, status, fOneFailed;//, iRepr;//, fTwoMember;
     int nSaved = 0, nRecords = 0, nUndec = 0, nClassRefs = 0, nTsat = 0, nMiniSat = 0;
-    int clk, timeTsat = 0, timeMiniSat = 0, timeSim = 0, timeTotal = clock();
+    clock_t clk, timeTsat = 0, timeMiniSat = 0, timeSim = 0, timeTotal = clock();
     if ( Vec_PtrSize(vOldRoots) == 0 )
         return 0;
     // start SAT solvers
@@ -1031,7 +1031,8 @@ void Gia_ComputeEquivalences( Gia_Man_t * pGia, int nBTLimit, int fUseMiniSat, i
     Hcd_Man_t * p;
     Vec_Ptr_t * vRoots;
     Gia_Man_t * pGiaLev;
-    int i, Lev, nLevels, nIters, clk;
+    int i, Lev, nLevels, nIters;
+    clock_t clk;
     Gia_ManRandom( 1 );
     Gia_ManSetPhase( pGia );
     nLevels = Gia_ManLevelNum( pGia );
diff --git a/src/aig/gia/giaGlitch.c b/src/aig/gia/giaGlitch.c
index fc4d2736..2b958cba 100644
--- a/src/aig/gia/giaGlitch.c
+++ b/src/aig/gia/giaGlitch.c
@@ -740,7 +740,8 @@ void Gli_ManSetPiRandomSeq( Gli_Man_t * p, float PiTransProb )
 ***********************************************************************/
 void Gli_ManSwitchesAndGlitches( Gli_Man_t * p, int nPatterns, float PiTransProb, int fVerbose )
 {
-    int i, k, clk = clock();
+    int i, k;
+    clock_t clk = clock();
     Gia_ManRandom( 1 );
     Gli_ManFinalize( p );
     if ( p->nRegs == 0 )
diff --git a/src/aig/gia/giaHcd.c b/src/aig/gia/giaHcd.c
index 3f37e724..656c880a 100644
--- a/src/aig/gia/giaHcd.c
+++ b/src/aig/gia/giaHcd.c
@@ -44,7 +44,7 @@ struct Hcd_Pars_t_
     int              fUseGia;       // uses GIA package 
     int              fUseCSat;      // uses circuit-based solver
     int              fVerbose;      // verbose stats
-    int              timeSynth;     // synthesis runtime
+    clock_t          timeSynth;     // synthesis runtime
     int              nNodesAhead;   // the lookahead in terms of nodes
     int              nCallsRecycle; // calls to perform before recycling SAT solver
 };
@@ -610,7 +610,8 @@ Aig_Man_t * Hcd_ComputeChoices( Aig_Man_t * pAig, int nBTLimit, int fSynthesis,
     Vec_Ptr_t * vGias;
     Gia_Man_t * pGia, * pMiter;
     Aig_Man_t * pAigNew;
-    int i, clk = clock();
+    int i;
+    clock_t clk = clock();
     // perform synthesis
     if ( fSynthesis )
     {
diff --git a/src/aig/gia/giaIso.c b/src/aig/gia/giaIso.c
index dcfee68f..16d0e46c 100644
--- a/src/aig/gia/giaIso.c
+++ b/src/aig/gia/giaIso.c
@@ -82,12 +82,12 @@ struct Gia_IsoMan_t_
     Vec_Int_t *      vClasses;
     Vec_Int_t *      vClasses2;
     // statistics 
-    int              timeStart;
-    int              timeSim;
-    int              timeRefine;
-    int              timeSort;
-    int              timeOther;
-    int              timeTotal;
+    clock_t          timeStart;
+    clock_t          timeSim;
+    clock_t          timeRefine;
+    clock_t          timeSort;
+    clock_t          timeOther;
+    clock_t          timeTotal;
 };
 
 static inline unsigned  Gia_IsoGetValue( Gia_IsoMan_t * p, int i )             { return (unsigned)(p->pStoreW[i]);       }
@@ -178,7 +178,7 @@ void Gia_IsoPrintClasses( Gia_IsoMan_t * p )
         printf( "\n" );
     }
 }
-void Gia_IsoPrint( Gia_IsoMan_t * p, int Iter, int Time )
+void Gia_IsoPrint( Gia_IsoMan_t * p, int Iter, clock_t Time )
 {
     printf( "Iter %4d :  ", Iter );
     printf( "Entries =%8d.  ", p->nEntries );
@@ -298,8 +298,9 @@ void Gia_IsoAssignUnique( Gia_IsoMan_t * p )
 int Gia_IsoSort( Gia_IsoMan_t * p )
 {
     Gia_Obj_t * pObj, * pObj0;
-    int i, k, fSameValue, iBegin, iBeginOld, nSize, nSizeNew, clk;
+    int i, k, fSameValue, iBegin, iBeginOld, nSize, nSizeNew;
     int fRefined = 0;
+    clock_t clk;
 
     // go through the equiv classes
     p->nSingles = 0;
@@ -722,7 +723,8 @@ Vec_Ptr_t * Gia_IsoDeriveEquivPos( Gia_Man_t * pGia, int fForward, int fVerbose
     Gia_IsoMan_t * p;
     Vec_Ptr_t * vEquivs = NULL;
     int fRefined, fRefinedAll;
-    int i, c, clk = clock(), clkTotal = clock();
+    int i, c;
+    clock_t clk = clock(), clkTotal = clock();
     assert( Gia_ManCiNum(pGia) > 0 );
     assert( Gia_ManPoNum(pGia) > 0 );
 
@@ -1070,7 +1072,8 @@ Gia_Man_t * Gia_ManIsoReduce( Gia_Man_t * pInit, Vec_Ptr_t ** pvPosEquivs, int f
     Vec_Ptr_t * vEquivs, * vEquivs2, * vStrings;
     Vec_Int_t * vRemain, * vLevel, * vLevel2;
     Vec_Str_t * vStr, * vStr2;
-    int i, k, s, sStart, Entry, Counter, clk = clock();
+    int i, k, s, sStart, Entry, Counter;
+    clock_t clk = clock();
     if ( pvPosEquivs )
         *pvPosEquivs = NULL;
 
@@ -1203,7 +1206,7 @@ Gia_Man_t * Gia_ManIsoReduce( Gia_Man_t * pInit, Vec_Ptr_t ** pvPosEquivs, int f
 void Gia_IsoTest( Gia_Man_t * p, int fVerbose )
 {
     Vec_Ptr_t * vEquivs;
-    int clk = clock(); 
+    clock_t clk = clock(); 
     vEquivs = Gia_IsoDeriveEquivPos( p, 0, fVerbose );
     printf( "Reduced %d outputs to %d.  ", Gia_ManPoNum(p), vEquivs ? Vec_PtrSize(vEquivs) : 1 );
     Abc_PrintTime( 1, "Time", clock() - clk );
diff --git a/src/aig/gia/giaRetime.c b/src/aig/gia/giaRetime.c
index 0b9a6bfb..c1ff852e 100644
--- a/src/aig/gia/giaRetime.c
+++ b/src/aig/gia/giaRetime.c
@@ -266,7 +266,8 @@ Gia_Man_t * Gia_ManRetimeForwardOne( Gia_Man_t * p, int * pnRegFixed, int * pnRe
 Gia_Man_t * Gia_ManRetimeForward( Gia_Man_t * p, int nMaxIters, int fVerbose )
 {
     Gia_Man_t * pNew, * pTemp;
-    int i, clk, nRegFixed, nRegMoves = 1;
+    int i, nRegFixed, nRegMoves = 1;
+    clock_t clk;
     pNew = p;
     for ( i = 0; i < nMaxIters && nRegMoves > 0; i++ )
     {
diff --git a/src/aig/gia/giaShrink.c b/src/aig/gia/giaShrink.c
index ad03f1e4..2db815fc 100644
--- a/src/aig/gia/giaShrink.c
+++ b/src/aig/gia/giaShrink.c
@@ -52,7 +52,8 @@ Gia_Man_t * Gia_ManPerformMapShrink( Gia_Man_t * p, int fKeepLevel, int fVerbose
     Gia_Man_t * pNew, * pTemp;
     Gia_Obj_t * pObj, * pFanin;
     unsigned * pTruth;
-    int i, k, iFan, clk = clock();
+    int i, k, iFan;
+    clock_t clk = clock();
 //    int ClassCounts[222] = {0};
     int * pLutClass, Counter = 0;
     assert( p->pMapping != NULL );
diff --git a/src/aig/gia/giaSim.c b/src/aig/gia/giaSim.c
index 37406c8d..3f11679d 100644
--- a/src/aig/gia/giaSim.c
+++ b/src/aig/gia/giaSim.c
@@ -109,7 +109,7 @@ Vec_Int_t * Gia_ManSimDeriveResets( Gia_Man_t * pGia )
     int i, k, Lit, Count;
     int Counter0 = 0, Counter1 = 0;
     int CounterPi0 = 0, CounterPi1 = 0;
-    int clk = clock();
+    clock_t clk = clock();
 
     // create reset counters for each literal
     vCountLits = Vec_IntStart( 2 * Gia_ManObjNum(pGia) );
@@ -609,9 +609,9 @@ int Gia_ManSimSimulate( Gia_Man_t * pAig, Gia_ParSim_t * pPars )
 {
     extern int Gia_ManSimSimulateEquiv( Gia_Man_t * pAig, Gia_ParSim_t * pPars );
     Gia_ManSim_t * p;
-    int i, clkTotal = clock();
-    int iOut, iPat, RetValue = 0;
-//    int nTimeToStop = pPars->TimeLimit ? pPars->TimeLimit + time(NULL) : 0;
+    clock_t clkTotal = clock();
+    int i, iOut, iPat, RetValue = 0;
+    clock_t nTimeToStop = pPars->TimeLimit ? pPars->TimeLimit * CLOCKS_PER_SEC + clock(): 0;
     if ( pAig->pReprs && pAig->pNexts )
         return Gia_ManSimSimulateEquiv( pAig, pPars );
     ABC_FREE( pAig->pCexSeq );
@@ -648,7 +648,7 @@ int Gia_ManSimSimulate( Gia_Man_t * pAig, Gia_ParSim_t * pPars )
             RetValue = 1;
             break;
         }
-        if ( time(NULL) > pPars->TimeLimit )
+        if ( clock() > nTimeToStop )
         {
             i++;
             break;
diff --git a/src/aig/gia/giaSim2.c b/src/aig/gia/giaSim2.c
index 74a34d1b..5ac1392f 100644
--- a/src/aig/gia/giaSim2.c
+++ b/src/aig/gia/giaSim2.c
@@ -639,9 +639,9 @@ int Gia_ManSimSimulateEquiv( Gia_Man_t * pAig, Gia_ParSim_t * pPars )
 {
     Gia_Sim2_t * p;
     Gia_Obj_t * pObj;
-    int i, clkTotal = clock();
-    int RetValue = 0, iOut, iPat;
-    int nTimeToStop = pPars->TimeLimit ? pPars->TimeLimit + time(NULL) : 0;
+    clock_t clkTotal = clock();
+    int i, RetValue = 0, iOut, iPat;
+    clock_t nTimeToStop = pPars->TimeLimit ? pPars->TimeLimit * CLOCKS_PER_SEC + clock(): 0;
     assert( pAig->pReprs && pAig->pNexts );
     ABC_FREE( pAig->pCexSeq );
     p = Gia_Sim2Create( pAig, pPars );
@@ -682,7 +682,7 @@ int Gia_ManSimSimulateEquiv( Gia_Man_t * pAig, Gia_ParSim_t * pPars )
         }
         if ( pAig->pReprs && pAig->pNexts )
             Gia_Sim2InfoRefineEquivs( p );
-        if ( time(NULL) > nTimeToStop )
+        if ( clock() > nTimeToStop )
         {
             i++;
             break;
diff --git a/src/aig/gia/giaSort.c b/src/aig/gia/giaSort.c
index f73e92bb..5183c441 100644
--- a/src/aig/gia/giaSort.c
+++ b/src/aig/gia/giaSort.c
@@ -160,7 +160,7 @@ void Gia_SortTest()
 {
     int nSize = 100000000;
     int * pArray;
-    int clk = clock();
+    clock_t clk = clock();
 
     printf( "Sorting %d integers\n", nSize );
     pArray = Gia_SortGetTest( nSize );
diff --git a/src/aig/gia/giaSwitch.c b/src/aig/gia/giaSwitch.c
index 628427d0..d1440ae0 100644
--- a/src/aig/gia/giaSwitch.c
+++ b/src/aig/gia/giaSwitch.c
@@ -559,7 +559,8 @@ Vec_Int_t * Gia_ManSwiSimulate( Gia_Man_t * pAig, Gia_ParSwi_t * pPars )
     Gia_Obj_t * pObj;
     Vec_Int_t * vSwitching;
     float * pSwitching;
-    int i, clk, clkTotal = clock();
+    int i;
+    clock_t clk, clkTotal = clock();
     if ( pPars->fProbOne && pPars->fProbTrans )
         printf( "Conflict of options: Can either compute probability of 1, or probability of switching by observing transitions.\n" );
     // create manager
diff --git a/src/aig/gia/giaTsim.c b/src/aig/gia/giaTsim.c
index c306e867..2f5e0293 100644
--- a/src/aig/gia/giaTsim.c
+++ b/src/aig/gia/giaTsim.c
@@ -669,7 +669,8 @@ Gia_ManTer_t * Gia_ManTerSimulate( Gia_Man_t * pAig, int fVerbose )
 {
     Gia_ManTer_t * p;
     unsigned * pState, * pPrev, * pLoop;
-    int i, Counter, clk, clkTotal = clock();
+    int i, Counter;
+    clock_t clk, clkTotal = clock();
     assert( Gia_ManRegNum(pAig) > 0 );
     // create manager
     clk = clock();