Fixing time primtouts throughout the code.

78 files changed, 280 insertions, 253 deletions

diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index 3c390a37..adad1837 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.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"
@@ -165,8 +164,8 @@ struct Aig_Man_t_
     Vec_Int_t *      vCiNumsOrig;    // original CI names
     int              nComplEdges;    // complemented edges
     // timing statistics
-    int              time1;
-    int              time2;
+    clock_t          time1;
+    clock_t          time2;
 };
 
 // cut computation
diff --git a/src/aig/aig/aigCuts.c b/src/aig/aig/aigCuts.c
index ed824fac..5e3bb93a 100644
--- a/src/aig/aig/aigCuts.c
+++ b/src/aig/aig/aigCuts.c
@@ -632,7 +632,8 @@ Aig_ManCut_t * Aig_ComputeCuts( Aig_Man_t * pAig, int nCutsMax, int nLeafMax, in
 {
     Aig_ManCut_t * p;
     Aig_Obj_t * pObj;
-    int i, clk = clock();
+    int i;
+    clock_t clk = clock();
     assert( pAig->pManCuts == NULL );
     // start the manager
     p = Aig_ManCutStart( pAig, nCutsMax, nLeafMax, fTruth, fVerbose );
diff --git a/src/aig/aig/aigDfs.c b/src/aig/aig/aigDfs.c
index ace723a2..b4b7862e 100644
--- a/src/aig/aig/aigDfs.c
+++ b/src/aig/aig/aigDfs.c
@@ -767,7 +767,8 @@ int Aig_SupportSize( Aig_Man_t * p, Aig_Obj_t * pObj )
 int Aig_SupportSizeTest( Aig_Man_t * p )
 {
     Aig_Obj_t * pObj;
-    int i, Counter = 0, clk = clock();
+    int i, Counter = 0;
+    clock_t clk = clock();
     Aig_ManForEachObj( p, pObj, i )
         if ( Aig_ObjIsNode(pObj) )
             Counter += (Aig_SupportSize(p, pObj) <= 16);
diff --git a/src/aig/aig/aigDoms.c b/src/aig/aig/aigDoms.c
index 00350304..fe9403b5 100644
--- a/src/aig/aig/aigDoms.c
+++ b/src/aig/aig/aigDoms.c
@@ -623,7 +623,8 @@ Aig_Sto_t * Aig_ManComputeDomsFlops( Aig_Man_t * pAig, int Limit )
     Aig_Sto_t * pSto;
     Vec_Ptr_t * vNodes;
     Aig_Obj_t * pObj;
-    int i, clk = clock();
+    int i;
+    clock_t clk = clock();
     pSto = Aig_ManDomStart( pAig, Limit );
     // initialize flop inputs
     Saig_ManForEachLi( pAig, pObj, i )
@@ -663,7 +664,8 @@ Aig_Sto_t * Aig_ManComputeDomsPis( Aig_Man_t * pAig, int Limit )
     Aig_Sto_t * pSto;
     Vec_Ptr_t * vNodes;
     Aig_Obj_t * pObj;
-    int i, clk = clock();
+    int i;
+    clock_t clk = clock();
     pSto = Aig_ManDomStart( pAig, Limit );
     // initialize flop inputs
     Aig_ManForEachCo( pAig, pObj, i )
@@ -703,7 +705,8 @@ Aig_Sto_t * Aig_ManComputeDomsNodes( Aig_Man_t * pAig, int Limit )
     Aig_Sto_t * pSto;
     Vec_Ptr_t * vNodes;
     Aig_Obj_t * pObj;
-    int i, clk = clock();
+    int i;
+    clock_t clk = clock();
     pSto = Aig_ManDomStart( pAig, Limit );
     // initialize flop inputs
     Aig_ManForEachCo( pAig, pObj, i )
diff --git a/src/aig/aig/aigInter.c b/src/aig/aig/aigInter.c
index fcf32236..6f183925 100644
--- a/src/aig/aig/aigInter.c
+++ b/src/aig/aig/aigInter.c
@@ -29,9 +29,9 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-extern int timeCnf;
-extern int timeSat;
-extern int timeInt;
+extern clock_t timeCnf;
+extern clock_t timeSat;
+extern clock_t timeInt;
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -156,7 +156,7 @@ Aig_Man_t * Aig_ManInter( Aig_Man_t * pManOn, Aig_Man_t * pManOff, int fRelation
     Vec_Int_t * vVarsAB;
     Aig_Obj_t * pObj, * pObj2;
     int Lits[3], status, i;
-    int clk;
+    clock_t clk;
     int iLast = -1; // Suppress "might be used uninitialized"
 
     assert( Aig_ManCiNum(pManOn) == Aig_ManCiNum(pManOff) );
diff --git a/src/aig/aig/aigJust.c b/src/aig/aig/aigJust.c
index 2c524c85..2ee60748 100644
--- a/src/aig/aig/aigJust.c
+++ b/src/aig/aig/aigJust.c
@@ -253,7 +253,9 @@ void Aig_ManJustExperiment( Aig_Man_t * pAig )
     Aig_ManPack_t * pPack;
     Vec_Int_t * vSuppLits, * vNodes;
     Aig_Obj_t * pObj;
-    int i, clk = clock(), Count0 = 0, Count0f = 0, Count1 = 0, Count1f = 0;
+    int i;
+    clock_t clk = clock();
+    int Count0 = 0, Count0f = 0, Count1 = 0, Count1f = 0;
     int nTotalLits = 0;
     vSuppLits = Vec_IntAlloc( 100 );
     pPack = Aig_ManPackStart( pAig );
diff --git a/src/aig/aig/aigPart.c b/src/aig/aig/aigPart.c
index 56d2fd3f..fdbba36a 100644
--- a/src/aig/aig/aigPart.c
+++ b/src/aig/aig/aigPart.c
@@ -688,7 +688,8 @@ Vec_Ptr_t * Aig_ManPartitionSmart( Aig_Man_t * p, int nSuppSizeLimit, int fVerbo
     Vec_Ptr_t * vPartSuppsBit;
     Vec_Ptr_t * vSupports, * vPartsAll, * vPartsAll2, * vPartSuppsAll;//, * vPartPtr;
     Vec_Int_t * vOne, * vPart, * vPartSupp, * vTemp;
-    int i, iPart, iOut, clk;
+    int i, iPart, iOut;
+    clock_t clk;
 
     // compute the supports for all outputs
 clk = clock();
@@ -812,7 +813,8 @@ Vec_Ptr_t * Aig_ManPartitionSmartRegisters( Aig_Man_t * pAig, int nSuppSizeLimit
     Vec_Ptr_t * vPartSuppsBit;
     Vec_Ptr_t * vSupports, * vPartsAll, * vPartsAll2, * vPartSuppsAll;
     Vec_Int_t * vOne, * vPart, * vPartSupp, * vTemp;
-    int i, iPart, iOut, clk;
+    int i, iPart, iOut;
+    clock_t clk;
 
     // add output number to each
 clk = clock();
diff --git a/src/aig/aig/aigPartSat.c b/src/aig/aig/aigPartSat.c
index 839a17ee..d187a19b 100644
--- a/src/aig/aig/aigPartSat.c
+++ b/src/aig/aig/aigPartSat.c
@@ -497,7 +497,8 @@ int Aig_ManPartitionedSat( Aig_Man_t * p, int nAlgo, int nPartSize,
     Aig_Man_t * pAig, * pTemp;
     Vec_Int_t * vNode2Part, * vNode2Var;
     int nConfRemaining = nConfTotal, nNodes = 0;
-    int i, clk, status, RetValue = -1;
+    int i, status, RetValue = -1;
+    clock_t clk;
 
     // perform partitioning according to the selected algorithm
     clk = clock();
diff --git a/src/aig/aig/aigRepar.c b/src/aig/aig/aigRepar.c
index 1b017346..7f9699fd 100644
--- a/src/aig/aig/aigRepar.c
+++ b/src/aig/aig/aigRepar.c
@@ -129,7 +129,7 @@ void Aig_ManInterTest( Aig_Man_t * pMan, int fVerbose )
     Cnf_Dat_t * pCnf;
     Aig_Obj_t * pObj;
     int Lit, Cid, Var, status, i;
-    int clk = clock();
+    clock_t clk = clock();
     assert( Aig_ManRegNum(pMan) == 0 );
     assert( Aig_ManCoNum(pMan) == 1 );
 
@@ -251,7 +251,7 @@ Aig_Man_t * Aig_ManInterRepar( Aig_Man_t * pMan, int fVerbose )
     int nOuts = Aig_ManCoNum(pMan);
     int ShiftP[2], ShiftCnf[2], ShiftOr[2], ShiftAssume;
     int Cid, Lit, status, i, k, c;
-    int clk = clock();
+    clock_t clk = clock();
     assert( Aig_ManRegNum(pMan) == 0 );
 
     // derive CNFs
diff --git a/src/aig/aig/aigRet.c b/src/aig/aig/aigRet.c
index 58a04fb0..1cf45ebe 100644
--- a/src/aig/aig/aigRet.c
+++ b/src/aig/aig/aigRet.c
@@ -839,7 +839,7 @@ Aig_Man_t * Rtm_ManRetime( Aig_Man_t * p, int fForward, int nStepsMax, int fVerb
     Rtm_Obj_t * pObj, * pNext;
     Aig_Obj_t * pObjAig;
     int i, k, nAutos, Degree, DegreeMax = 0; 
-    int clk;
+    clock_t clk;
 
     // create the retiming manager
 clk = clock();
diff --git a/src/aig/aig/aigSplit.c b/src/aig/aig/aigSplit.c
index f187860f..50f96a81 100644
--- a/src/aig/aig/aigSplit.c
+++ b/src/aig/aig/aigSplit.c
@@ -258,7 +258,8 @@ Aig_Man_t * Aig_ManSplit( Aig_Man_t * p, int nVars, int fVerbose )
     DdNode * bFunc;
     DdManager * dd;
     Vec_Ptr_t * vSupp, * vSubs, * vCofs;
-    int i, clk = clock();
+    int i;
+    clock_t clk = clock();
     if ( Saig_ManPoNum(p) != 1 )
     {
         printf( "Currently works only for one primary output.\n" );
diff --git a/src/aig/aig/aigTable.c b/src/aig/aig/aigTable.c
index ec2531c7..abd9960a 100644
--- a/src/aig/aig/aigTable.c
+++ b/src/aig/aig/aigTable.c
@@ -70,7 +70,8 @@ void Aig_TableResize( Aig_Man_t * p )
 {
     Aig_Obj_t * pEntry, * pNext;
     Aig_Obj_t ** pTableOld, ** ppPlace;
-    int nTableSizeOld, Counter, i, clk;
+    int nTableSizeOld, Counter, i;
+    clock_t clk;
     assert( p->pTable != NULL );
 clk = clock();
     // save the old table
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();
diff --git a/src/aig/hop/hop.h b/src/aig/hop/hop.h
index 6411265f..d23f3508 100644
--- a/src/aig/hop/hop.h
+++ b/src/aig/hop/hop.h
@@ -30,7 +30,6 @@
 #include <stdlib.h>
 #include <string.h>
 #include <assert.h>
-#include <time.h>
 
 #include "src/misc/vec/vec.h"
 
@@ -106,8 +105,8 @@ struct Hop_Man_t_
     Vec_Ptr_t *      vPages;         // memory pages used by nodes
     Hop_Obj_t *      pListFree;      // the list of free nodes 
     // timing statistics
-    int              time1;
-    int              time2;
+    clock_t          time1;
+    clock_t          time2;
 };
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/hop/hopTable.c b/src/aig/hop/hopTable.c
index 7db93f62..1adab015 100644
--- a/src/aig/hop/hopTable.c
+++ b/src/aig/hop/hopTable.c
@@ -167,7 +167,8 @@ void Hop_TableResize( Hop_Man_t * p )
 {
     Hop_Obj_t * pEntry, * pNext;
     Hop_Obj_t ** pTableOld, ** ppPlace;
-    int nTableSizeOld, Counter, nEntries, i, clk;
+    int nTableSizeOld, Counter, nEntries, i;
+    clock_t clk;
 clk = clock();
     // save the old table
     pTableOld = p->pTable;
diff --git a/src/aig/ioa/ioa.h b/src/aig/ioa/ioa.h
index a427f507..809e8e3f 100644
--- a/src/aig/ioa/ioa.h
+++ b/src/aig/ioa/ioa.h
@@ -30,7 +30,6 @@
 #include <stdlib.h>
 #include <string.h>
 #include <assert.h>
-#include <time.h>
 
 #include "src/misc/vec/vec.h"
 //#include "bar.h"
diff --git a/src/aig/ivy/ivy.h b/src/aig/ivy/ivy.h
index 8d062134..f0292e6c 100644
--- a/src/aig/ivy/ivy.h
+++ b/src/aig/ivy/ivy.h
@@ -125,8 +125,8 @@ struct Ivy_Man_t_
     Vec_Ptr_t *      vPages;         // memory pages used by nodes
     Ivy_Obj_t *      pListFree;      // the list of free nodes 
     // timing statistics
-    int              time1;
-    int              time2;
+    clock_t          time1;
+    clock_t          time2;
 };
 
 struct Ivy_FraigParams_t_
diff --git a/src/aig/ivy/ivyCut.c b/src/aig/ivy/ivyCut.c
index d5a31dee..19d37bb2 100644
--- a/src/aig/ivy/ivyCut.c
+++ b/src/aig/ivy/ivyCut.c
@@ -969,7 +969,7 @@ void Ivy_ManTestCutsAll( Ivy_Man_t * p )
 {
     Ivy_Obj_t * pObj;
     int i, nCutsCut, nCutsTotal, nNodeTotal, nNodeOver;
-    int clk = clock();
+    clock_t clk = clock();
     nNodeTotal = nNodeOver = 0;
     nCutsTotal = -Ivy_ManNodeNum(p);
     Ivy_ManForEachObj( p, pObj, i )
diff --git a/src/aig/ivy/ivyCutTrav.c b/src/aig/ivy/ivyCutTrav.c
index a053c713..5834a6fc 100644
--- a/src/aig/ivy/ivyCutTrav.c
+++ b/src/aig/ivy/ivyCutTrav.c
@@ -439,7 +439,7 @@ void Ivy_ManTestCutsTravAll( Ivy_Man_t * p )
     Vec_Int_t * vStore;
     Vec_Vec_t * vBitCuts;
     int i, nCutsCut, nCutsTotal, nNodeTotal, nNodeOver;
-    int clk = clock();
+    clock_t clk = clock();
 
     vNodes = Vec_PtrAlloc( 100 );
     vFront = Vec_PtrAlloc( 100 );
diff --git a/src/aig/ivy/ivyFastMap.c b/src/aig/ivy/ivyFastMap.c
index 1d9efca1..feeb36f2 100644
--- a/src/aig/ivy/ivyFastMap.c
+++ b/src/aig/ivy/ivyFastMap.c
@@ -67,7 +67,7 @@ static inline Ivy_Supp_t * Ivy_ObjSuppStart( Ivy_Man_t * pAig, Ivy_Obj_t * pObj
     return pSupp;
 }
 
-static void Ivy_FastMapPrint( Ivy_Man_t * pAig, int Delay, int Area, int Time, char * pStr );
+static void Ivy_FastMapPrint( Ivy_Man_t * pAig, int Delay, int Area, clock_t Time, char * pStr );
 static int  Ivy_FastMapDelay( Ivy_Man_t * pAig );
 static int  Ivy_FastMapArea( Ivy_Man_t * pAig );
 static void Ivy_FastMapNode( Ivy_Man_t * pAig, Ivy_Obj_t * pObj, int nLimit );
@@ -83,8 +83,8 @@ static int  Ivy_FastMapNodeRef( Ivy_Man_t * pAig, Ivy_Obj_t * pObj );
 static int  Ivy_FastMapNodeDeref( Ivy_Man_t * pAig, Ivy_Obj_t * pObj );
 
 
-extern int s_MappingTime;
-extern int s_MappingMem;
+extern clock_t s_MappingTime;
+extern clock_t s_MappingMem;
 
 
 ////////////////////////////////////////////////////////////////////////
@@ -106,7 +106,8 @@ void Ivy_FastMapPerform( Ivy_Man_t * pAig, int nLimit, int fRecovery, int fVerbo
 {
     Ivy_SuppMan_t * pMan;
     Ivy_Obj_t * pObj;
-    int i, Delay, Area, clk, clkTotal = clock();
+    int i, Delay, Area;
+    clock_t clk, clkTotal = clock();
     // start the memory for supports
     pMan = ABC_ALLOC( Ivy_SuppMan_t, 1 );
     memset( pMan, 0, sizeof(Ivy_SuppMan_t) );
@@ -210,7 +211,7 @@ void Ivy_FastMapStop( Ivy_Man_t * pAig )
   SeeAlso     []
 
 ***********************************************************************/
-void Ivy_FastMapPrint( Ivy_Man_t * pAig, int Delay, int Area, int Time, char * pStr )
+void Ivy_FastMapPrint( Ivy_Man_t * pAig, int Delay, int Area, clock_t Time, char * pStr )
 {
     printf( "%s : Delay = %3d. Area = %6d. ", pStr, Delay, Area );
     ABC_PRT( "Time", Time );
diff --git a/src/aig/ivy/ivyFraig.c b/src/aig/ivy/ivyFraig.c
index cc6250e4..411402fb 100644
--- a/src/aig/ivy/ivyFraig.c
+++ b/src/aig/ivy/ivyFraig.c
@@ -93,16 +93,16 @@ struct Ivy_FraigMan_t_
     int                 nSatFails;
     int                 nSatFailsReal;
     // runtime
-    int                 timeSim;
-    int                 timeTrav;
-    int                 timeSat;
-    int                 timeSatUnsat;
-    int                 timeSatSat;
-    int                 timeSatFail;
-    int                 timeRef;
-    int                 timeTotal;
-    int                 time1;
-    int                 time2;
+    clock_t             timeSim;
+    clock_t             timeTrav;
+    clock_t             timeSat;
+    clock_t             timeSatUnsat;
+    clock_t             timeSatSat;
+    clock_t             timeSatFail;
+    clock_t             timeRef;
+    clock_t             timeTotal;
+    clock_t             time1;
+    clock_t             time2;
 };
 
 typedef struct Prove_ParamsStruct_t_      Prove_Params_t;
@@ -198,7 +198,7 @@ static int           Ivy_FraigSetActivityFactors( Ivy_FraigMan_t * p, Ivy_Obj_t
 static void          Ivy_FraigAddToPatScores( Ivy_FraigMan_t * p, Ivy_Obj_t * pClass, Ivy_Obj_t * pClassNew );
 static int           Ivy_FraigMiterStatus( Ivy_Man_t * pMan );
 static void          Ivy_FraigMiterProve( Ivy_FraigMan_t * p );
-static void          Ivy_FraigMiterPrint( Ivy_Man_t * pNtk, char * pString, int clk, int fVerbose );
+static void          Ivy_FraigMiterPrint( Ivy_Man_t * pNtk, char * pString, clock_t clk, int fVerbose );
 static int *         Ivy_FraigCreateModel( Ivy_FraigMan_t * p );
 
 static int Ivy_FraigNodesAreEquivBdd( Ivy_Obj_t * pObj1, Ivy_Obj_t * pObj2 );
@@ -257,7 +257,8 @@ int Ivy_FraigProve( Ivy_Man_t ** ppManAig, void * pPars )
     Prove_Params_t * pParams = (Prove_Params_t *)pPars;
     Ivy_FraigParams_t Params, * pIvyParams = &Params; 
     Ivy_Man_t * pManAig, * pManTemp;
-    int RetValue, nIter, clk;//, Counter;
+    int RetValue, nIter;
+    clock_t clk;//, Counter;
     ABC_INT64_T nSatConfs = 0, nSatInspects = 0;
 
     // start the network and parameters
@@ -414,7 +415,7 @@ Ivy_Man_t * Ivy_FraigPerform_int( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pPara
 { 
     Ivy_FraigMan_t * p;
     Ivy_Man_t * pManAigNew;
-    int clk;
+    clock_t clk;
     if ( Ivy_ManNodeNum(pManAig) == 0 )
         return Ivy_ManDup(pManAig);
 clk = clock();
@@ -451,7 +452,7 @@ Ivy_Man_t * Ivy_FraigPerform( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams )
 {
     Ivy_FraigMan_t * p;
     Ivy_Man_t * pManAigNew;
-    int clk;
+    clock_t clk;
     if ( Ivy_ManNodeNum(pManAig) == 0 )
         return Ivy_ManDup(pManAig);
 clk = clock();
@@ -481,7 +482,8 @@ Ivy_Man_t * Ivy_FraigMiter( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams )
     Ivy_FraigMan_t * p;
     Ivy_Man_t * pManAigNew;
     Ivy_Obj_t * pObj;
-    int i, clk;
+    int i;
+    clock_t clk;
 clk = clock();
     assert( Ivy_ManLatchNum(pManAig) == 0 );
     p = Ivy_FraigStartSimple( pManAig, pParams );
@@ -988,7 +990,8 @@ unsigned Ivy_NodeHash( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj )
 void Ivy_FraigSimulateOne( Ivy_FraigMan_t * p )
 {
     Ivy_Obj_t * pObj;
-    int i, clk;
+    int i;
+    clock_t clk;
 clk = clock();
     Ivy_ManForEachNode( p->pManAig, pObj, i )
     {
@@ -1020,7 +1023,7 @@ p->nSimRounds++;
 void Ivy_FraigSimulateOneSim( Ivy_FraigMan_t * p )
 {
     Ivy_FraigSim_t * pSims;
-    int clk;
+    clock_t clk;
 clk = clock();
     for ( pSims = p->pSimStart; pSims; pSims = pSims->pNext )
         Ivy_NodeSimulateSim( p, pSims );
@@ -1384,7 +1387,8 @@ int Ivy_FraigCheckOutputSims( Ivy_FraigMan_t * p )
 int Ivy_FraigRefineClasses( Ivy_FraigMan_t * p )
 {
     Ivy_Obj_t * pClass, * pClass2;
-    int clk, RetValue, Counter = 0;
+    int RetValue, Counter = 0;
+    clock_t clk;
     // check if some outputs already became non-constant
     // this is a special case when computation can be stopped!!!
     if ( p->pParams->fProve )
@@ -1789,7 +1793,7 @@ void Ivy_FraigResimulate( Ivy_FraigMan_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Ivy_FraigMiterPrint( Ivy_Man_t * pNtk, char * pString, int clk, int fVerbose )
+void Ivy_FraigMiterPrint( Ivy_Man_t * pNtk, char * pString, clock_t clk, int fVerbose )
 {
     if ( !fVerbose )
         return;
@@ -1876,7 +1880,8 @@ int Ivy_FraigMiterStatus( Ivy_Man_t * pMan )
 void Ivy_FraigMiterProve( Ivy_FraigMan_t * p )
 {
     Ivy_Obj_t * pObj, * pObjNew;
-    int i, RetValue, clk = clock();
+    int i, RetValue;
+    clock_t clk = clock();
     int fVerbose = 0;
     Ivy_ManForEachPo( p->pManAig, pObj, i )
     {
@@ -2093,7 +2098,8 @@ void Ivy_FraigPrintActivity( Ivy_FraigMan_t * p )
 ***********************************************************************/
 int Ivy_FraigNodesAreEquiv( Ivy_FraigMan_t * p, Ivy_Obj_t * pOld, Ivy_Obj_t * pNew )
 {
-    int pLits[4], RetValue, RetValue1, nBTLimit, clk; //, clk2 = clock();
+    int pLits[4], RetValue, RetValue1, nBTLimit;
+    clock_t clk; //, clk2 = clock();
 
     // make sure the nodes are not complemented
     assert( !Ivy_IsComplement(pNew) );
@@ -2259,7 +2265,8 @@ p->timeSatFail += clock() - clk;
 ***********************************************************************/
 int Ivy_FraigNodeIsConst( Ivy_FraigMan_t * p, Ivy_Obj_t * pNew )
 {
-    int pLits[2], RetValue1, clk;
+    int pLits[2], RetValue1;
+    clock_t clk;
     int RetValue;
 
     // make sure the nodes are not complemented
@@ -2628,7 +2635,8 @@ int Ivy_FraigSetActivityFactors_rec( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj, int L
 ***********************************************************************/
 int Ivy_FraigSetActivityFactors( Ivy_FraigMan_t * p, Ivy_Obj_t * pOld, Ivy_Obj_t * pNew )
 {
-    int clk, LevelMin, LevelMax;
+    int LevelMin, LevelMax;
+    clock_t clk;
     assert( pOld || pNew );
 clk = clock(); 
     // reset the active variables
diff --git a/src/aig/ivy/ivyResyn.c b/src/aig/ivy/ivyResyn.c
index 8d571110..dc483bf6 100644
--- a/src/aig/ivy/ivyResyn.c
+++ b/src/aig/ivy/ivyResyn.c
@@ -44,7 +44,7 @@ ABC_NAMESPACE_IMPL_START
 ***********************************************************************/
 Ivy_Man_t * Ivy_ManResyn0( Ivy_Man_t * pMan, int fUpdateLevel, int fVerbose )
 {
-    int clk;
+    clock_t clk;
     Ivy_Man_t * pTemp;
 
 if ( fVerbose ) { printf( "Original:\n" ); }
@@ -85,7 +85,7 @@ if ( fVerbose ) Ivy_ManPrintStats( pMan );
 ***********************************************************************/
 Ivy_Man_t * Ivy_ManResyn( Ivy_Man_t * pMan, int fUpdateLevel, int fVerbose )
 {
-    int clk;
+    clock_t clk;
     Ivy_Man_t * pTemp;
 
 if ( fVerbose ) { printf( "Original:\n" ); }
@@ -154,7 +154,7 @@ if ( fVerbose ) Ivy_ManPrintStats( pMan );
 ***********************************************************************/
 Ivy_Man_t * Ivy_ManRwsat( Ivy_Man_t * pMan, int fVerbose )
 {
-    int clk;
+    clock_t clk;
     Ivy_Man_t * pTemp;
 
 if ( fVerbose ) { printf( "Original:\n" ); }
diff --git a/src/aig/ivy/ivyRwr.c b/src/aig/ivy/ivyRwr.c
index 39131210..292bd3f9 100644
--- a/src/aig/ivy/ivyRwr.c
+++ b/src/aig/ivy/ivyRwr.c
@@ -57,7 +57,7 @@ int Ivy_ManRewritePre( Ivy_Man_t * p, int fUpdateLevel, int fUseZeroCost, int fV
     Rwt_Man_t * pManRwt;
     Ivy_Obj_t * pNode;
     int i, nNodes, nGain;
-    int clk, clkStart = clock();
+    clock_t clk, clkStart = clock();
     // start the rewriting manager
     pManRwt = Rwt_ManStart( 0 );
     p->pData = pManRwt;
@@ -164,7 +164,7 @@ int Ivy_NodeRewrite( Ivy_Man_t * pMan, Rwt_Man_t * p, Ivy_Obj_t * pNode, int fUp
     int Required, nNodesSaved;
     int nNodesSaveCur = -1; // Suppress "might be used uninitialized"
     int i, c, GainCur, GainBest = -1;
-    int clk, clk2;
+    clock_t clk, clk2;
 
     p->nNodesConsidered++;
     // get the required times
diff --git a/src/aig/ivy/ivySeq.c b/src/aig/ivy/ivySeq.c
index 283bf9fe..4a999780 100644
--- a/src/aig/ivy/ivySeq.c
+++ b/src/aig/ivy/ivySeq.c
@@ -65,7 +65,7 @@ int Ivy_ManRewriteSeq( Ivy_Man_t * p, int fUseZeroCost, int fVerbose )
     Rwt_Man_t * pManRwt;
     Ivy_Obj_t * pNode;
     int i, nNodes, nGain;
-    int clk, clkStart = clock();
+    clock_t clk, clkStart = clock();
 
     // set the DC latch values
     Ivy_ManForEachLatch( p, pNode, i )
@@ -157,7 +157,7 @@ int Ivy_NodeRewriteSeq( Ivy_Man_t * pMan, Rwt_Man_t * p, Ivy_Obj_t * pNode, int
     int nNodesSaved;
     int nNodesSaveCur = -1; // Suppress "might be used uninitialized"
     int i, c, GainCur, GainBest = -1;
-    int clk, clk2;//, clk3;
+    clock_t clk, clk2;//, clk3;
 
     p->nNodesConsidered++;
     // get the node's cuts
@@ -1110,7 +1110,7 @@ void Ivy_CutComputeAll( Ivy_Man_t * p, int nInputs )
     Ivy_Store_t * pStore;
     Ivy_Obj_t * pObj;
     int i, nCutsTotal, nCutsTotalM, nNodeTotal, nNodeOver;
-    int clk = clock();
+    clock_t clk = clock();
     if ( nInputs > IVY_CUT_INPUT )
     {
         printf( "Cannot compute cuts for more than %d inputs.\n", IVY_CUT_INPUT );
diff --git a/src/aig/ivy/ivyTable.c b/src/aig/ivy/ivyTable.c
index d2c1ab9a..d2753aa8 100644
--- a/src/aig/ivy/ivyTable.c
+++ b/src/aig/ivy/ivyTable.c
@@ -206,7 +206,8 @@ int Ivy_TableCountEntries( Ivy_Man_t * p )
 void Ivy_TableResize( Ivy_Man_t * p )
 {
     int * pTableOld, * pPlace;
-    int nTableSizeOld, Counter, nEntries, e, clk;
+    int nTableSizeOld, Counter, nEntries, e;
+    clock_t clk;
 clk = clock();
     // save the old table
     pTableOld = p->pTable;
diff --git a/src/aig/saig/saigAbsCba.c b/src/aig/saig/saigAbsCba.c
index 55a429e1..0b59274a 100644
--- a/src/aig/saig/saigAbsCba.c
+++ b/src/aig/saig/saigAbsCba.c
@@ -721,7 +721,7 @@ Abc_Cex_t * Saig_ManCbaFindCexCareBits( Aig_Man_t * pAig, Abc_Cex_t * pCex, int
     Saig_ManCba_t * p;
     Vec_Int_t * vReasons;
     Abc_Cex_t * pCare;
-    int clk = clock();
+    clock_t clk = clock();
 
     clk = clock();
     p = Saig_ManCbaStart( pAig, pCex, nInputs, fVerbose );
@@ -831,7 +831,8 @@ ABC_PRT( "Time", clock() - clk );
 Vec_Int_t * Saig_ManCbaPerform( Aig_Man_t * pAbs, int nInputs, Saig_ParBmc_t * pPars )
 {
     Vec_Int_t * vAbsFfsToAdd;
-    int RetValue, clk = clock();
+    int RetValue;
+    clock_t clk = clock();
 //    assert( pAbs->nRegs > 0 );
     // perform BMC
     RetValue = Saig_ManBmcScalable( pAbs, pPars );
diff --git a/src/aig/saig/saigAbsPba.c b/src/aig/saig/saigAbsPba.c
index 42744459..9a10edb6 100644
--- a/src/aig/saig/saigAbsPba.c
+++ b/src/aig/saig/saigAbsPba.c
@@ -254,9 +254,9 @@ Vec_Int_t * Saig_ManPbaDerive( Aig_Man_t * pAig, int nInputs, int nStart, int nF
     sat_solver * pSat;
     Cnf_Dat_t * pCnf;
     Aig_Obj_t * pObj;
-    int nTimeToStop = time(NULL) + TimeLimit;
     int nCoreLits, * pCoreLits;
-    int i, iVar, RetValue, clk;
+    int i, iVar, RetValue;
+    clock_t clk;
 if ( fVerbose )
 {
 if ( TimeLimit )
@@ -296,7 +296,7 @@ Abc_PrintTime( 1, "Preparing", clock() - clk );
 
     // set runtime limit
     if ( TimeLimit )
-        sat_solver_set_runtime_limit( pSat, nTimeToStop );
+        sat_solver_set_runtime_limit( pSat, TimeLimit ? TimeLimit * CLOCKS_PER_SEC + clock(): 0 );
 
     // run SAT solver
 clk = clock();
diff --git a/src/aig/saig/saigAbsStart.c b/src/aig/saig/saigAbsStart.c
index 0054d8b0..77517c18 100644
--- a/src/aig/saig/saigAbsStart.c
+++ b/src/aig/saig/saigAbsStart.c
@@ -172,7 +172,8 @@ int Saig_ManCexRefineStep( Aig_Man_t * p, Vec_Int_t * vFlops, Vec_Int_t * vFlopC
 {
     Aig_Man_t * pAbs;
     Vec_Int_t * vFlopsNew;
-    int i, Entry, clk = clock();
+    int i, Entry;
+    clock_t clk = clock();
     pAbs = Saig_ManDupAbstraction( p, vFlops );
     if ( fSensePath )
         vFlopsNew = Saig_ManExtendCounterExampleTest2( pAbs, Saig_ManCexFirstFlopPi(p, pAbs), pCex, fVerbose );
diff --git a/src/aig/saig/saigAbsVfa.c b/src/aig/saig/saigAbsVfa.c
index 24414c5a..e991ac35 100644
--- a/src/aig/saig/saigAbsVfa.c
+++ b/src/aig/saig/saigAbsVfa.c
@@ -209,7 +209,8 @@ int Abs_VfaManCreateFrame_rec( Abs_VfaMan_t * p, Aig_Obj_t * pObj, int f )
 void Abs_VfaManCreateFrame( Abs_VfaMan_t * p, int f )
 {
     Aig_Obj_t * pObj;
-    int i, clk = clock();
+    int i;
+    clock_t clk = clock();
 
     Saig_ManForEachPo( p->pAig, pObj, i )
         Abs_VfaManCreateFrame_rec( p, pObj, f );
diff --git a/src/aig/saig/saigBmc.c b/src/aig/saig/saigBmc.c
index 60f406ad..021ad5d0 100644
--- a/src/aig/saig/saigBmc.c
+++ b/src/aig/saig/saigBmc.c
@@ -190,7 +190,8 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim
     Cnf_Dat_t * pCnf;
     Aig_Man_t * pFrames, * pAigTemp;
     Aig_Obj_t * pObj;
-    int status, clk, Lit, i, RetValue = -1;
+    int status, Lit, i, RetValue = -1;
+    clock_t clk;
 
     // derive the timeframes
     clk = clock();
@@ -264,7 +265,7 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim
     }
     else
     {
-        int clkPart = clock();
+        clock_t clkPart = clock();
         Aig_ManForEachCo( pFrames, pObj, i )
         {
 //if ( s_fInterrupt )
diff --git a/src/aig/saig/saigBmc2.c b/src/aig/saig/saigBmc2.c
index 4a95bdbc..8ff9a7a7 100644
--- a/src/aig/saig/saigBmc2.c
+++ b/src/aig/saig/saigBmc2.c
@@ -202,7 +202,7 @@ Vec_Ptr_t * Abs_ManTernarySimulate( Aig_Man_t * p, int nFramesMax, int fVerbose
     Vec_Ptr_t * vSimInfo;
     Aig_Obj_t * pObj;
     int i, f, nFramesLimit, nFrameWords;
-    int clk = clock();
+    clock_t clk = clock();
     assert( Aig_ManRegNum(p) > 0 );
     // the maximum number of frames will be determined to use at most 200Mb of RAM
     nFramesLimit = 1 + (200000000 * 4)/Aig_ManObjNum(p);
@@ -742,9 +742,10 @@ int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax
     Saig_Bmc_t * p;
     Aig_Man_t * pNew;
     Cnf_Dat_t * pCnf;
-    int nTimeToStop = time(NULL) + nTimeOut;
     int nOutsSolved = 0;
-    int Iter, RetValue = -1, clk = clock(), clk2, clkTotal = clock();
+    int Iter, RetValue = -1;
+    clock_t nTimeToStop = nTimeOut ? nTimeOut * CLOCKS_PER_SEC + clock(): 0;
+    clock_t clk = clock(), clk2, clkTotal = clock();
     int Status = -1;
 /*
     Vec_Ptr_t * vSimInfo;
@@ -763,7 +764,7 @@ int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax
     p = Saig_BmcManStart( pAig, nFramesMax, nNodesMax, nConfMaxOne, nConfMaxAll, fVerbose );
     // set runtime limit
     if ( nTimeOut )
-        sat_solver_set_runtime_limit( p->pSat, nTimeToStop );
+        sat_solver_set_runtime_limit( p->pSat, nTimeOut );
     for ( Iter = 0; ; Iter++ )
     {
         clk2 = clock();
@@ -796,7 +797,7 @@ int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax
         if ( RetValue != l_False )
             break;
         // check the timeout
-        if ( nTimeOut && time(NULL) > nTimeToStop )
+        if ( nTimeOut && clock() > nTimeToStop )
         {
             printf( "Reached timeout (%d seconds).\n",  nTimeOut );
             if ( piFrames )
@@ -839,7 +840,7 @@ int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax
             printf( "Reached limit on the number of timeframes (%d).\n", p->nFramesMax );
         else if ( p->nConfMaxAll && p->pSat->stats.conflicts > p->nConfMaxAll )
             printf( "Reached global conflict limit (%d).\n", p->nConfMaxAll );
-        else if ( nTimeOut && time(NULL) > nTimeToStop )
+        else if ( nTimeOut && clock() > nTimeToStop )
             printf( "Reached timeout (%d seconds).\n", nTimeOut );
         else
             printf( "Reached local conflict limit (%d).\n", p->nConfMaxOne );
diff --git a/src/aig/saig/saigBmc3.c b/src/aig/saig/saigBmc3.c
index 9107a796..12e982cc 100644
--- a/src/aig/saig/saigBmc3.c
+++ b/src/aig/saig/saigBmc3.c
@@ -1251,8 +1251,9 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
     unsigned * pInfo;
     int RetValue = -1, fFirst = 1, nJumpFrame = 0, fUnfinished = 0;
     int nOutDigits = Abc_Base10Log( Saig_ManPoNum(pAig) );
-    int i, f, Lit, status, clk, clk2, clkOther = 0, clkTotal = clock();
-    int nTimeToStop = time(NULL) + pPars->nTimeOut;
+    int i, f, Lit, status;
+    clock_t clk, clk2, clkOther = 0, clkTotal = clock();
+    clock_t nTimeToStop = pPars->nTimeOut ? pPars->nTimeOut * CLOCKS_PER_SEC + clock(): 0;
     p = Saig_Bmc3ManStart( pAig );
     p->pPars = pPars;
     if ( pPars->fVerbose )
@@ -1411,7 +1412,7 @@ clkOther += clock() - clk2;
             else 
             {
                 assert( status == l_Undef );
-                if ( pPars->nTimeOut && time(NULL) > nTimeToStop )
+                if ( pPars->nTimeOut && clock() > nTimeToStop )
                 {
                     printf( "Reached timeout (%d seconds).\n",  pPars->nTimeOut );
                     Saig_Bmc3ManStop( p );
@@ -1427,7 +1428,7 @@ clkOther += clock() - clk2;
                 Saig_Bmc3ManStop( p );
                 return RetValue;
             }
-            if ( pPars->nTimeOut && time(NULL) > nTimeToStop )
+            if ( pPars->nTimeOut && clock() > nTimeToStop )
             {
                 printf( "Reached timeout (%d seconds).\n",  pPars->nTimeOut );
                 Saig_Bmc3ManStop( p );
@@ -1450,7 +1451,7 @@ clkOther += clock() - clk2;
 //            printf( "%4.0f Mb",     4.0*Vec_IntSize(p->vVisited) /(1<<20) );
             printf( "%4.0f Mb",     4.0*(f+1)*p->nObjNums /(1<<20) );
             printf( "%4.0f Mb",     1.0*sat_solver_memory(p->pSat)/(1<<20) );
-            printf( "%9.2f sec ",  (float)(clock() - clkTotal)/(float)(CLOCKS_PER_SEC) );
+            printf( "%9.2f sec ",  1.0*(clock() - clkTotal)/CLOCKS_PER_SEC );
 //            printf( "\n" );
 //            ABC_PRMn( "Id2Var", (f+1)*p->nObjNums*4 );
 //            ABC_PRMn( "SAT", 42 * p->pSat->size + 16 * (int)p->pSat->stats.clauses + 4 * (int)p->pSat->stats.clauses_literals );
diff --git a/src/aig/saig/saigConstr2.c b/src/aig/saig/saigConstr2.c
index f54f2dbe..85e79e3f 100644
--- a/src/aig/saig/saigConstr2.c
+++ b/src/aig/saig/saigConstr2.c
@@ -59,7 +59,8 @@ int Ssw_ManProfileConstraints( Aig_Man_t * p, int nWords, int nFrames, int fVerb
     Vec_Int_t * vProbs, * vProbs2;
     Aig_Obj_t * pObj, * pObjLi;
     unsigned * pInfo, * pInfo0, * pInfo1, * pInfoMask, * pInfoMask2;
-    int i, w, f, RetValue = 1, clk = clock();
+    int i, w, f, RetValue = 1;
+    clock_t clk = clock();
     if ( fVerbose )
         printf( "Simulating %d nodes and %d flops for %d frames with %d words... ", 
             Aig_ManNodeNum(p), Aig_ManRegNum(p), nFrames, nWords );
diff --git a/src/aig/saig/saigGlaCba.c b/src/aig/saig/saigGlaCba.c
index 459d8ede..d39ff944 100644
--- a/src/aig/saig/saigGlaCba.c
+++ b/src/aig/saig/saigGlaCba.c
@@ -59,9 +59,9 @@ struct Aig_Gla1Man_t_
     // SAT solver
     sat_solver *   pSat;
     // statistics
-    int            timeSat;
-    int            timeRef;
-    int            timeTotal;
+    clock_t        timeSat;
+    clock_t        timeRef;
+    clock_t        timeTotal;
 };
 
 ////////////////////////////////////////////////////////////////////////
@@ -687,8 +687,9 @@ Vec_Int_t * Aig_Gla1ManPerform( Aig_Man_t * pAig, Vec_Int_t * vGateClassesOld, i
     Abc_Cex_t * pCex;
     Vec_Int_t * vPPiRefine;
     int f, g, r, i, iSatVar, Lit, Entry, RetValue;
-    int nConfBef, nConfAft, clk, clkTotal = clock();
-    int nTimeToStop = time(NULL) + TimeLimit;
+    int nConfBef, nConfAft;
+    clock_t clk, clkTotal = clock();
+    clock_t nTimeToStop = TimeLimit ? TimeLimit * CLOCKS_PER_SEC + clock(): 0;
     assert( Saig_ManPoNum(pAig) == 1 );
 
     if ( nFramesMax == 0 )
@@ -753,7 +754,7 @@ Vec_Int_t * Aig_Gla1ManPerform( Aig_Man_t * pAig, Vec_Int_t * vGateClassesOld, i
                         printf( "== %3d ==", f );
                     else
                         printf( "         " );
-                    if ( TimeLimit && time(NULL) > nTimeToStop )
+                    if ( TimeLimit && clock() > nTimeToStop )
                         printf( "       SAT solver timed out after %d seconds.\n", TimeLimit );
                     else if ( RetValue != l_False )
                         printf( "       SAT solver returned UNDECIDED after %5d conflicts.\n", nConfAft - nConfBef );
diff --git a/src/aig/saig/saigGlaPba.c b/src/aig/saig/saigGlaPba.c
index 6f461995..e039ed75 100644
--- a/src/aig/saig/saigGlaPba.c
+++ b/src/aig/saig/saigGlaPba.c
@@ -48,46 +48,15 @@ struct Aig_Gla2Man_t_
     // SAT solver
     sat_solver *   pSat;
     // statistics
-    int            timePre;
-    int            timeSat;
-    int            timeTotal;
+    clock_t        timePre;
+    clock_t        timeSat;
+    clock_t        timeTotal;
 };
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
-#define ABC_CPS 1000
-
-/**Function*************************************************************
-
-  Synopsis    [Procedure returns miliseconds elapsed since the last reset.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_Clock( int Timer, int fReset )
-{
-    static int Time[16], Clock[16];
-    int Clock2, Diff;
-    assert( Timer >= 0 && Timer < 16 );
-    if ( fReset )
-    {
-        Time[Timer] = time(NULL);
-        Clock[Timer] = clock();
-        return 0;
-    }
-    Clock2 = clock();
-    if ( Clock2 > Clock[Timer] )
-        Diff = (Clock2 - Clock[Timer]) % CLOCKS_PER_SEC;
-    else
-        Diff = CLOCKS_PER_SEC - (Clock[Timer] - Clock2) % CLOCKS_PER_SEC;
-    return (time(NULL) - Time[Timer]) * ABC_CPS + (Diff * ABC_CPS) / CLOCKS_PER_SEC;
-}
 
 /**Function*************************************************************
 
@@ -432,7 +401,8 @@ Vec_Int_t * Saig_AbsSolverUnsatCore( sat_solver * pSat, int nConfMax, int fVerbo
     Vec_Int_t * vCore;
     void * pSatCnf; 
     Intp_Man_t * pManProof;
-    int RetValue, clk = clock();
+    int RetValue;
+    clock_t clk = clock();
     if ( piRetValue )
         *piRetValue = -1;
     // solve the problem
@@ -556,8 +526,8 @@ Vec_Int_t * Aig_Gla2ManPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, in
 {
     Aig_Gla2Man_t * p;
     Vec_Int_t * vCore, * vResult;
-    int nTimeToStop = time(NULL) + TimeLimit;
-    int clk, clk2 = clock();
+    clock_t nTimeToStop = TimeLimit ? TimeLimit * CLOCKS_PER_SEC + clock(): 0;
+    clock_t clk, clk2 = clock();
     assert( Saig_ManPoNum(pAig) == 1 );
 
     if ( fVerbose )
diff --git a/src/aig/saig/saigGlaPba2.c b/src/aig/saig/saigGlaPba2.c
index a7122d01..42850e01 100644
--- a/src/aig/saig/saigGlaPba2.c
+++ b/src/aig/saig/saigGlaPba2.c
@@ -47,9 +47,9 @@ struct Aig_Gla3Man_t_
     // SAT solver
     sat_solver2 *  pSat;
     // statistics
-    int            timePre;
-    int            timeSat;
-    int            timeTotal;
+    clock_t        timePre;
+    clock_t        timeSat;
+    clock_t        timeTotal;
 };
 
 ////////////////////////////////////////////////////////////////////////
@@ -393,7 +393,8 @@ void Aig_Gla3ManStop( Aig_Gla3Man_t * p )
 Vec_Int_t * Aig_Gla3ManUnsatCore( sat_solver2 * pSat, int nConfMax, int fVerbose, int * piRetValue )
 {
     Vec_Int_t * vCore;
-    int RetValue, clk = clock();
+    int RetValue;
+    clock_t clk = clock();
     if ( piRetValue )
         *piRetValue = -1;
     // solve the problem
@@ -495,8 +496,7 @@ Vec_Int_t * Aig_Gla3ManPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, in
 {
     Aig_Gla3Man_t * p;
     Vec_Int_t * vCore, * vResult;
-    int nTimeToStop = time(NULL) + TimeLimit;
-    int clk, clk2 = clock();
+    clock_t clk, clk2 = clock();
     assert( Saig_ManPoNum(pAig) == 1 );
 
     if ( fVerbose )
@@ -521,7 +521,7 @@ Vec_Int_t * Aig_Gla3ManPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, in
 
     // set runtime limit
     if ( TimeLimit )
-        sat_solver2_set_runtime_limit( p->pSat, nTimeToStop );
+        sat_solver2_set_runtime_limit( p->pSat, TimeLimit * CLOCKS_PER_SEC + clock() );
 
     // compute UNSAT core
     clk = clock();
diff --git a/src/aig/saig/saigHaig.c b/src/aig/saig/saigHaig.c
index aedc98e2..b92b7a9b 100644
--- a/src/aig/saig/saigHaig.c
+++ b/src/aig/saig/saigHaig.c
@@ -206,7 +206,7 @@ int Aig_ManHaigVerify( Aig_Man_t * p, Aig_Man_t * pAig, Aig_Man_t * pHaig, int n
     sat_solver * pSat;
     Aig_Obj_t * pObj1, * pObj2;
     int i, RetValue1, RetValue2, Counter, Lits[2], nOvers;
-    int clk = clock(), clkVerif;
+    clock_t clk = clock(), clkVerif;
 
     nOvers = Aig_ManMapHaigNodes( pHaig );
 
@@ -412,7 +412,7 @@ int Aig_ManHaigVerify2( Aig_Man_t * p, Aig_Man_t * pAig, Aig_Man_t * pHaig, int
     sat_solver * pSat;
     Aig_Obj_t * pObj1, * pObj2;
     int i, RetValue1, RetValue2, Counter, Lits[2];
-    int clk = clock();
+    clock_t clk = clock();
     int Delta;
     int Id1, Id2;
 
@@ -624,7 +624,8 @@ Aig_Man_t * Saig_ManHaigRecord( Aig_Man_t * p, int nIters, int nSteps, int fReti
     Dar_RwrPar_t ParsRwr, * pParsRwr = &ParsRwr;
     Aig_Man_t * pNew, * pTemp;
     Aig_Obj_t * pObj;
-    int i, k, nStepsReal, clk = clock(), clkSynth;
+    int i, k, nStepsReal;
+    clock_t clk = clock(), clkSynth;
     Dar_ManDefaultRwrParams( pParsRwr );
 
 clk = clock();
diff --git a/src/aig/saig/saigInd.c b/src/aig/saig/saigInd.c
index aa417fb0..39ec734a 100644
--- a/src/aig/saig/saigInd.c
+++ b/src/aig/saig/saigInd.c
@@ -150,8 +150,9 @@ int Saig_ManInduction( Aig_Man_t * p, int nFramesMax, int nConfMax, int fUnique,
     Vec_Int_t * vTopVarNums, * vState, * vTopVarIds = NULL;
     Vec_Ptr_t * vTop, * vBot;
     Aig_Obj_t * pObjPi, * pObjPiCopy, * pObjPo;
-    int i, k, f, clk, Lits[2], status = -1, RetValue, nSatVarNum, nConfPrev;
+    int i, k, f, Lits[2], status = -1, RetValue, nSatVarNum, nConfPrev;
     int nOldSize, iReg, iLast, fAdded, nConstrs = 0, nClauses = 0;
+    clock_t clk;
     assert( fUnique == 0 || fUniqueAll == 0 );
     assert( Saig_ManPoNum(p) == 1 );
     Aig_ManSetCioIds( p );
diff --git a/src/aig/saig/saigIso.c b/src/aig/saig/saigIso.c
index 2250126b..ccff1bde 100644
--- a/src/aig/saig/saigIso.c
+++ b/src/aig/saig/saigIso.c
@@ -426,7 +426,8 @@ Aig_Man_t * Iso_ManFilterPos( Aig_Man_t * pAig, Vec_Ptr_t ** pvPosEquivs, int fV
     Vec_Ptr_t * vBuffers, * vClasses;
     Vec_Int_t * vLevel, * vRemain;
     Vec_Str_t * vStr, * vPrev;
-    int i, nPos, clk = clock();
+    int i, nPos;
+    clock_t clk = clock();
     int clkDup = 0, clkAig = 0, clkIso = 0, clk2;
     *pvPosEquivs = NULL;
 
@@ -539,7 +540,7 @@ Aig_Man_t * Iso_ManFilterPos( Aig_Man_t * pAig, Vec_Ptr_t ** pvPosEquivs, int fV
 Aig_Man_t * Iso_ManTest( Aig_Man_t * pAig, int fVerbose )
 {
     Vec_Int_t * vPerm;
-    int clk = clock();
+    clock_t clk = clock();
     vPerm = Saig_ManFindIsoPerm( pAig, fVerbose );
     Vec_IntFree( vPerm );
     Abc_PrintTime( 1, "Time", clock() - clk );
@@ -560,7 +561,7 @@ Aig_Man_t * Iso_ManTest( Aig_Man_t * pAig, int fVerbose )
 Aig_Man_t * Saig_ManIsoReduce( Aig_Man_t * pAig, Vec_Ptr_t ** pvPosEquivs, int fVerbose )
 { 
     Aig_Man_t * pPart;
-    int clk = clock();
+    clock_t clk = clock();
     pPart = Iso_ManFilterPos( pAig, pvPosEquivs, fVerbose );
     printf( "Reduced %d outputs to %d outputs.  ", Saig_ManPoNum(pAig), Saig_ManPoNum(pPart) );
     Abc_PrintTime( 1, "Time", clock() - clk );
diff --git a/src/aig/saig/saigIsoFast.c b/src/aig/saig/saigIsoFast.c
index a7cc942c..8b60368f 100644
--- a/src/aig/saig/saigIsoFast.c
+++ b/src/aig/saig/saigIsoFast.c
@@ -160,7 +160,7 @@ void Iso_StoCollectInfo_rec( Aig_Man_t * p, Aig_Obj_t * pObj, int fCompl, Vec_In
     Vec_IntPush( vVisited, Aig_ObjId(pObj) );
 }
 
-//static int time_Trav = 0;
+//static clock_t time_Trav = 0;
 
 /**Function*************************************************************
 
@@ -286,7 +286,8 @@ Vec_Vec_t * Saig_IsoDetectFast( Aig_Man_t * pAig )
     Aig_Obj_t * pObj;
     Vec_Ptr_t * vClasses, * vInfos;
     Vec_Int_t * vInfo, * vPrev, * vLevel;
-    int i, Number, nUnique = 0, clk = clock();
+    int i, Number, nUnique = 0;
+    clock_t clk = clock();
 
     // collect infos and remember their number
     pMan = Iso_StoStart( pAig );
diff --git a/src/aig/saig/saigIsoSlow.c b/src/aig/saig/saigIsoSlow.c
index 3dcd7777..25cd68f0 100644
--- a/src/aig/saig/saigIsoSlow.c
+++ b/src/aig/saig/saigIsoSlow.c
@@ -290,11 +290,11 @@ struct Iso_Man_t_
     Vec_Ptr_t *   vClasses;       // other classes
     Vec_Ptr_t *   vTemp1;         // other classes
     Vec_Ptr_t *   vTemp2;         // other classes
-    int           timeHash;
-    int           timeFout;
-    int           timeSort;
-    int           timeOther;
-    int           timeTotal;
+    clock_t       timeHash;
+    clock_t       timeFout;
+    clock_t       timeSort;
+    clock_t       timeOther;
+    clock_t       timeTotal;
 };
 
 static inline Iso_Obj_t *  Iso_ManObj( Iso_Man_t * p, int i )            { assert( i >= 0 && i < p->nObjs ); return i ? p->pObjs + i : NULL;                }
@@ -556,7 +556,8 @@ static inline int Iso_ObjHashAdd( Iso_Man_t * p, Iso_Obj_t * pIso )
 void Iso_ManCollectClasses( Iso_Man_t * p )
 {
     Iso_Obj_t * pIso;
-    int i, clk = clock();
+    int i;
+    clock_t clk = clock();
     Vec_PtrClear( p->vSingles );
     Vec_PtrClear( p->vClasses );
     for ( i = 0; i < p->nBins; i++ )
@@ -1171,8 +1172,7 @@ Vec_Int_t * Saig_ManFindIsoPerm( Aig_Man_t * pAig, int fVerbose )
     int fVeryVerbose = 0;
     Vec_Int_t * vRes;
     Iso_Man_t * p;
-    int clk, clk2 = clock();
-    clk = clock();
+    clock_t clk = clock(), clk2 = clock();
     p = Iso_ManCreate( pAig );
     p->timeFout += clock() - clk;
     Iso_ManPrintClasses( p, fVerbose, fVeryVerbose );
diff --git a/src/aig/saig/saigMiter.c b/src/aig/saig/saigMiter.c
index f7832f10..f3f6f279 100644
--- a/src/aig/saig/saigMiter.c
+++ b/src/aig/saig/saigMiter.c
@@ -1076,7 +1076,8 @@ int Ssw_SecSpecial( Aig_Man_t * pPart0, Aig_Man_t * pPart1, int nFrames, int fVe
 //    extern int Fra_FraigCec( Aig_Man_t ** ppAig, int nConfLimit, int fVerbose );
     int iOut, nOuts;
     Aig_Man_t * pMiterCec;
-    int RetValue, clkTotal = clock();
+    int RetValue;
+    clock_t clkTotal = clock();
     if ( fVerbose )
     {
         Aig_ManPrintStats( pPart0 );
diff --git a/src/aig/saig/saigRefSat.c b/src/aig/saig/saigRefSat.c
index 6a351e10..d99320ce 100644
--- a/src/aig/saig/saigRefSat.c
+++ b/src/aig/saig/saigRefSat.c
@@ -510,7 +510,7 @@ Abc_Cex_t * Saig_RefManRunSat( Saig_RefMan_t * p, int fNewOrder )
     Vec_Int_t * vAssumps, * vVar2PiId;
     int i, k, Entry, RetValue;//, f = 0, Counter = 0;
     int nCoreLits, * pCoreLits;
-    int clk = clock();
+    clock_t clk = clock();
     // create CNF
     assert( Aig_ManRegNum(p->pFrames) == 0 );
 //    pCnf = Cnf_Derive( p->pFrames, 0 ); // too slow
@@ -868,7 +868,7 @@ Abc_Cex_t * Saig_ManFindCexCareBits( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nIn
     Saig_RefMan_t * p;
     Vec_Int_t * vReasons;
     Abc_Cex_t * pCare;
-    int clk = clock();
+    clock_t clk = clock();
 
     clk = clock();
     p = Saig_RefManStart( pAig, pCex, nInputs, fVerbose );
@@ -931,7 +931,7 @@ Vec_Int_t * Saig_ManExtendCounterExampleTest3( Aig_Man_t * pAig, int iFirstFlopP
 {
     Saig_RefMan_t * p;
     Vec_Int_t * vRes, * vReasons;
-    int clk;
+    clock_t clk;
     if ( Saig_ManPiNum(pAig) != pCex->nPis )
     {
         printf( "Saig_ManExtendCounterExampleTest3(): The PI count of AIG (%d) does not match that of cex (%d).\n", 
diff --git a/src/aig/saig/saigRetFwd.c b/src/aig/saig/saigRetFwd.c
index bbd7f397..006167d5 100644
--- a/src/aig/saig/saigRetFwd.c
+++ b/src/aig/saig/saigRetFwd.c
@@ -213,7 +213,8 @@ Aig_Man_t * Saig_ManRetimeForwardOne( Aig_Man_t * p, int * pnRegFixed, int * pnR
 Aig_Man_t * Saig_ManRetimeForward( Aig_Man_t * p, int nMaxIters, int fVerbose )
 {
     Aig_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/saig/saigSimExt.c b/src/aig/saig/saigSimExt.c
index c83a7a64..36f3d903 100644
--- a/src/aig/saig/saigSimExt.c
+++ b/src/aig/saig/saigSimExt.c
@@ -521,7 +521,7 @@ Vec_Int_t * Saig_ManExtendCounterExampleTest( Aig_Man_t * p, int iFirstFlopPi, A
 {
     Vec_Int_t * vRes;
     Vec_Ptr_t * vSimInfo;
-    int clk;
+    clock_t clk;
     if ( Saig_ManPiNum(p) != pCex->nPis )
     {
         printf( "Saig_ManExtendCounterExampleTest(): The PI count of AIG (%d) does not match that of cex (%d).\n", 
diff --git a/src/aig/saig/saigSimExt2.c b/src/aig/saig/saigSimExt2.c
index f5aecc71..335c4034 100644
--- a/src/aig/saig/saigSimExt2.c
+++ b/src/aig/saig/saigSimExt2.c
@@ -337,7 +337,7 @@ Vec_Int_t * Saig_ManExtendCounterExampleTest2( Aig_Man_t * p, int iFirstFlopPi,
 {
     Vec_Int_t * vRes;
     Vec_Ptr_t * vSimInfo;
-    int clk;
+    clock_t clk;
     if ( Saig_ManPiNum(p) != pCex->nPis )
     {
         printf( "Saig_ManExtendCounterExampleTest2(): The PI count of AIG (%d) does not match that of cex (%d).\n", 
@@ -446,7 +446,7 @@ Abc_Cex_t * Saig_ManFindCexCareBitsSense( Aig_Man_t * p, Abc_Cex_t * pCex, int i
 {
     Abc_Cex_t * pCare;
     Vec_Ptr_t * vSimInfo;
-    int clk;
+    clock_t clk;
     if ( Saig_ManPiNum(p) != pCex->nPis )
     {
         printf( "Saig_ManExtendCounterExampleTest2(): The PI count of AIG (%d) does not match that of cex (%d).\n", 
diff --git a/src/aig/saig/saigSimFast.c b/src/aig/saig/saigSimFast.c
index 27855bfd..e54e58ac 100644
--- a/src/aig/saig/saigSimFast.c
+++ b/src/aig/saig/saigSimFast.c
@@ -348,7 +348,8 @@ Vec_Int_t * Faig_ManComputeSwitchProbs4( Aig_Man_t * p, int nFrames, int nPref,
     Vec_Int_t * vSwitching;
     int * pProbs;
     float * pSwitching;
-    int nFramesReal, clk;//, clkTotal = clock();
+    int nFramesReal;
+    clock_t clk;//, clkTotal = clock();
     if ( fProbOne )
         fTrans = 0;
     vSwitching = Vec_IntStart( Aig_ManObjNumMax(p) );
diff --git a/src/aig/saig/saigSimMv.c b/src/aig/saig/saigSimMv.c
index 11bd088c..71259930 100644
--- a/src/aig/saig/saigSimMv.c
+++ b/src/aig/saig/saigSimMv.c
@@ -881,7 +881,8 @@ Vec_Ptr_t * Saig_MvManSimulate( Aig_Man_t * pAig, int nFramesSymb, int nFramesSa
     Vec_Ptr_t * vMap;
     Saig_MvMan_t * p;
     Saig_MvObj_t * pEntry;
-    int f, i, iState, clk = clock();
+    int f, i, iState;
+    clock_t clk = clock();
     assert( nFramesSymb >= 1 && nFramesSymb <= nFramesSatur );
 
     // start manager
diff --git a/src/aig/saig/saigSimSeq.c b/src/aig/saig/saigSimSeq.c
index 86c45f37..ee4085b1 100644
--- a/src/aig/saig/saigSimSeq.c
+++ b/src/aig/saig/saigSimSeq.c
@@ -456,7 +456,7 @@ int Raig_ManSimulate( Aig_Man_t * pAig, int nWords, int nIters, int TimeLimit, i
     Raig_Man_t * p;
     Sec_MtrStatus_t Status;
     int i, iPat, RetValue = 0;
-    int clk, clkTotal = clock();
+    clock_t clk, clkTotal = clock();
     assert( Aig_ManRegNum(pAig) > 0 );
     Status = Sec_MiterStatus( pAig );
     if ( Status.nSat > 0 )
diff --git a/src/aig/saig/saigStrSim.c b/src/aig/saig/saigStrSim.c
index 5d33595f..2feaba1b 100644
--- a/src/aig/saig/saigStrSim.c
+++ b/src/aig/saig/saigStrSim.c
@@ -877,7 +877,8 @@ Vec_Int_t * Saig_StrSimPerformMatching( Aig_Man_t * p0, Aig_Man_t * p1, int nDis
     Vec_Int_t * vPairs;
     Aig_Man_t * pPart0, * pPart1;
     Aig_Obj_t * pObj0, * pObj1;
-    int i, nMatches, clk, clkTotal = clock();
+    int i, nMatches;
+    clock_t clk, clkTotal = clock();
     Aig_ManRandom( 1 );
     // consider the case when a miter is given
     if ( p1 == NULL )
diff --git a/src/aig/saig/saigSwitch.c b/src/aig/saig/saigSwitch.c
index 4c54e3ad..8f4f962f 100644
--- a/src/aig/saig/saigSwitch.c
+++ b/src/aig/saig/saigSwitch.c
@@ -268,7 +268,8 @@ Vec_Int_t * Saig_ManComputeSwitchProb4s( Aig_Man_t * p, int nFrames, int nPref,
     Saig_SimObj_t * pAig, * pEntry;
     Vec_Int_t * vSwitching;
     float * pSwitching;
-    int nFramesReal, clk;//, clkTotal = clock();
+    int nFramesReal;
+    clock_t clk;//, clkTotal = clock();
     vSwitching = Vec_IntStart( Aig_ManObjNumMax(p) );
     pSwitching = (float *)vSwitching->pArray;
 clk = clock();
diff --git a/src/aig/saig/saigSynch.c b/src/aig/saig/saigSynch.c
index c592d0a5..28c8150f 100644
--- a/src/aig/saig/saigSynch.c
+++ b/src/aig/saig/saigSynch.c
@@ -504,7 +504,8 @@ Aig_Man_t * Saig_SynchSequenceApply( Aig_Man_t * pAig, int nWords, int fVerbose
     Aig_Man_t * pAigZero;
     Vec_Str_t * vSequence;
     Vec_Ptr_t * vSimInfo;
-    int RetValue, clk;
+    int RetValue;
+    clock_t clk;
 
 clk = clock();
     // derive synchronization sequence
@@ -557,7 +558,8 @@ Aig_Man_t * Saig_Synchronize( Aig_Man_t * pAig1, Aig_Man_t * pAig2, int nWords,
     Aig_Man_t * pAig1z, * pAig2z, * pMiter;
     Vec_Str_t * vSeq1, * vSeq2;
     Vec_Ptr_t * vSimInfo;
-    int RetValue, clk;
+    int RetValue;
+    clock_t clk;
 /*
     {
         unsigned u = Saig_SynchRandomTernary();
diff --git a/src/aig/saig/saigTrans.c b/src/aig/saig/saigTrans.c
index 9be84e31..55c9772a 100644
--- a/src/aig/saig/saigTrans.c
+++ b/src/aig/saig/saigTrans.c
@@ -379,7 +379,7 @@ Aig_Man_t * Saig_ManTimeframeSimplify( Aig_Man_t * pAig, int nFrames, int nFrame
 {
 //    extern Aig_Man_t * Fra_FraigEquivence( Aig_Man_t * pManAig, int nConfMax, int fProve );
     Aig_Man_t * pFrames, * pFraig, * pRes1, * pRes2;
-    int clk;
+    clock_t clk;
     // create uninitialized timeframes with map1
     pFrames = Saig_ManFramesNonInitial( pAig, nFrames );
     // perform fraiging for the unrolled timeframes