Fixing time primtouts throughout the code.

82 files changed, 409 insertions, 311 deletions

diff --git a/src/proof/bbr/bbrCex.c b/src/proof/bbr/bbrCex.c
index 7ee95e7c..60fef07c 100644
--- a/src/proof/bbr/bbrCex.c
+++ b/src/proof/bbr/bbrCex.c
@@ -55,7 +55,7 @@ Abc_Cex_t * Aig_ManVerifyUsingBddsCountExample( Aig_Man_t * p, DdManager * dd,
     DdNode * bTemp, * bVar, * bRing;
     int i, v, RetValue, nPiOffset;
     char * pValues;
-    int clk = clock();
+    clock_t clk = clock();
 //printf( "\nDeriving counter-example.\n" );
 
     // allocate room for the counter-example
diff --git a/src/proof/bbr/bbrReach.c b/src/proof/bbr/bbrReach.c
index 1cce1a90..19d87bc2 100644
--- a/src/proof/bbr/bbrReach.c
+++ b/src/proof/bbr/bbrReach.c
@@ -246,7 +246,8 @@ int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, D
     DdNode * bTemp;
     Cudd_ReorderingType method;
     int i, nIters, nBddSize = 0, status;
-    int nThreshold = 10000, clk = clock();
+    int nThreshold = 10000;
+    clock_t clk = clock();
     Vec_Ptr_t * vOnionRings;
 
     status = Cudd_ReorderingStatus( dd, &method );
@@ -280,7 +281,7 @@ int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, D
     for ( nIters = 0; nIters < pPars->nIterMax; nIters++ )
     { 
         // check the runtime limit
-        if ( pPars->TimeLimit && ((float)pPars->TimeLimit <= (float)(clock()-clk)/(float)(CLOCKS_PER_SEC)) )
+        if ( pPars->TimeLimit && pPars->TimeLimit <= (clock()-clk)/CLOCKS_PER_SEC )
         {
             printf( "Reached timeout after image computation (%d seconds).\n",  pPars->TimeLimit );
             Vec_PtrFree( vOnionRings );
@@ -433,7 +434,8 @@ int Aig_ManVerifyUsingBdds_int( Aig_Man_t * p, Saig_ParBbr_t * pPars )
     DdManager * dd;
     DdNode ** pbParts, ** pbOutputs;
     DdNode * bInitial, * bTemp;
-    int RetValue, i, clk = clock();
+    int RetValue, i;
+    clock_t clk = clock();
     Vec_Ptr_t * vOnionRings;
 
     assert( Saig_ManRegNum(p) > 0 );
@@ -450,7 +452,7 @@ int Aig_ManVerifyUsingBdds_int( Aig_Man_t * p, Saig_ParBbr_t * pPars )
         printf( "Shared BDD size is %6d nodes.\n", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
 
     // check the runtime limit
-    if ( pPars->TimeLimit && ((float)pPars->TimeLimit <= (float)(clock()-clk)/(float)(CLOCKS_PER_SEC)) )
+    if ( pPars->TimeLimit && pPars->TimeLimit <= (clock()-clk)/CLOCKS_PER_SEC )
     {
         printf( "Reached timeout after constructing global BDDs (%d seconds).\n",  pPars->TimeLimit );
         Cudd_Quit( dd );
diff --git a/src/proof/cec/cecCec.c b/src/proof/cec/cecCec.c
index b9b3e1f1..841b6a0b 100644
--- a/src/proof/cec/cecCec.c
+++ b/src/proof/cec/cecCec.c
@@ -72,7 +72,8 @@ int Cec_ManVerifyOld( Gia_Man_t * pMiter, int fVerbose, int * piOutFail )
     extern int Ssw_SecCexResimulate( Aig_Man_t * p, int * pModel, int * pnOutputs );
     Gia_Man_t * pTemp = Gia_ManTransformMiter( pMiter );
     Aig_Man_t * pMiterCec = Gia_ManToAig( pTemp, 0 );
-    int RetValue, iOut, nOuts, clkTotal = clock();
+    int RetValue, iOut, nOuts;
+    clock_t clkTotal = clock();
     if ( piOutFail )
         *piOutFail = -1;
     Gia_ManStop( pTemp );
@@ -134,7 +135,8 @@ int Cec_ManHandleSpecialCases( Gia_Man_t * p, Cec_ParCec_t * pPars )
 {
     Gia_Obj_t * pObj1, * pObj2;
     Gia_Obj_t * pDri1, * pDri2;
-    int i, clk = clock();
+    int i;
+    clock_t clk = clock();
     Gia_ManSetPhase( p );
     Gia_ManForEachPo( p, pObj1, i )
     {
@@ -206,8 +208,9 @@ int Cec_ManVerify( Gia_Man_t * pInit, Cec_ParCec_t * pPars )
     int fDumpUndecided = 0;
     Cec_ParFra_t ParsFra, * pParsFra = &ParsFra;
     Gia_Man_t * p, * pNew;
-    int RetValue, clk = clock();
-    double clkTotal = clock();
+    int RetValue;
+    clock_t clk = clock();
+    clock_t clkTotal = clock();
     // consider special cases:
     // 1) (SAT) a pair of POs have different value under all-0 pattern
     // 2) (SAT) a pair of POs has different PI/Const drivers
@@ -263,7 +266,7 @@ int Cec_ManVerify( Gia_Man_t * pInit, Cec_ParCec_t * pPars )
         Gia_WriteAiger( pNew, "gia_cec_undecided.aig", 0, 0 );
         Abc_Print( 1, "The result is written into file \"%s\".\n", "gia_cec_undecided.aig" );
     }
-    if ( pPars->TimeLimit && ((double)clock() - clkTotal)/CLOCKS_PER_SEC >= pPars->TimeLimit )
+    if ( pPars->TimeLimit && (clock() - clkTotal)/CLOCKS_PER_SEC >= pPars->TimeLimit )
     {
         Gia_ManStop( pNew );
         return -1;
diff --git a/src/proof/cec/cecChoice.c b/src/proof/cec/cecChoice.c
index 3ddb975e..05b372f8 100644
--- a/src/proof/cec/cecChoice.c
+++ b/src/proof/cec/cecChoice.c
@@ -208,8 +208,8 @@ int Cec_ManChoiceComputation_int( Gia_Man_t * pAig, Cec_ParChc_t * pPars )
     Cec_ManSim_t * pSim;
     Gia_Man_t * pSrm;
     int r, RetValue;
-    int clkSat = 0, clkSim = 0, clkSrm = 0, clkTotal = clock();
-    int clk2, clk = clock();
+    clock_t clkSat = 0, clkSim = 0, clkSrm = 0, clkTotal = clock();
+    clock_t clk2, clk = clock();
     ABC_FREE( pAig->pReprs );
     ABC_FREE( pAig->pNexts );
     Gia_ManRandom( 1 );
diff --git a/src/proof/cec/cecCore.c b/src/proof/cec/cecCore.c
index 65c4b970..71519323 100644
--- a/src/proof/cec/cecCore.c
+++ b/src/proof/cec/cecCore.c
@@ -257,7 +257,8 @@ Gia_Man_t * Cec_ManSatSolving( Gia_Man_t * pAig, Cec_ParSat_t * pPars )
 int Cec_ManSimulationOne( Gia_Man_t * pAig, Cec_ParSim_t * pPars )
 {
     Cec_ManSim_t * pSim;
-    int RetValue = 0, clkTotal = clock();
+    int RetValue = 0;
+    clock_t clkTotal = clock();
     pSim = Cec_ManSimStart( pAig, pPars );
     if ( (pAig->pReprs == NULL && (RetValue = Cec_ManSimClassesPrepare( pSim, -1 ))) ||
          (RetValue == 0 &&        (RetValue = Cec_ManSimClassesRefine( pSim ))) )
@@ -342,8 +343,8 @@ Gia_Man_t * Cec_ManSatSweeping( Gia_Man_t * pAig, Cec_ParFra_t * pPars )
     Cec_ManFra_t * p;
     Cec_ManSim_t * pSim;
     Cec_ManPat_t * pPat;
-    int i, fTimeOut = 0, nMatches = 0, clk, clk2;
-    double clkTotal = clock();
+    int i, fTimeOut = 0, nMatches = 0;
+    clock_t clk, clk2, clkTotal = clock();
 
     // duplicate AIG and transfer equivalence classes
     Gia_ManRandom( 1 );
@@ -457,7 +458,7 @@ p->timeSat += clock() - clk;
             break;
         }
         // check resource limits
-        if ( p->pPars->TimeLimit && ((double)clock() - clkTotal)/CLOCKS_PER_SEC >= p->pPars->TimeLimit )
+        if ( p->pPars->TimeLimit && (clock() - clkTotal)/CLOCKS_PER_SEC >= p->pPars->TimeLimit )
         {
             fTimeOut = 1;
             break;
diff --git a/src/proof/cec/cecCorr.c b/src/proof/cec/cecCorr.c
index d080dfea..e8b25b48 100644
--- a/src/proof/cec/cecCorr.c
+++ b/src/proof/cec/cecCorr.c
@@ -719,7 +719,7 @@ Gia_Man_t * Gia_ManCorrReduce( Gia_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Cec_ManRefinedClassPrintStats( Gia_Man_t * p, Vec_Str_t * vStatus, int iIter, int Time )
+void Cec_ManRefinedClassPrintStats( Gia_Man_t * p, Vec_Str_t * vStatus, int iIter, clock_t Time )
 { 
     int nLits, CounterX = 0, Counter0 = 0, Counter = 0;
     int i, Entry, nProve = 0, nDispr = 0, nFail = 0;
@@ -789,7 +789,7 @@ void Cec_ManLSCorrespondenceBmc( Gia_Man_t * pAig, Cec_ParCor_t * pPars, int nPr
     fChanges = 1;
     while ( fChanges )
     {
-        int clkBmc = clock();
+        clock_t clkBmc = clock();
         fChanges = 0;
         pSrm = Gia_ManCorrSpecReduceInit( pAig, pPars->nFrames, nPrefs, !pPars->fLatchCorr, &vOutputs, pPars->fUseRings );
         if ( Gia_ManPoNum(pSrm) == 0 )
@@ -844,9 +844,10 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
     Cec_ParSat_t ParsSat, * pParsSat = &ParsSat;
     Cec_ManSim_t * pSim;
     Gia_Man_t * pSrm;
-    int r, RetValue, clkTotal = clock();
-    int clkSat = 0, clkSim = 0, clkSrm = 0;
-    int clk2, clk = clock();
+    int r, RetValue;
+    clock_t clkTotal = clock();
+    clock_t clkSat = 0, clkSim = 0, clkSrm = 0;
+    clock_t clk2, clk = clock();
     if ( Gia_ManRegNum(pAig) == 0 )
     {
         Abc_Print( 1, "Cec_ManLatchCorrespondence(): Not a sequential AIG.\n" );
diff --git a/src/proof/cec/cecCorr_updated.c b/src/proof/cec/cecCorr_updated.c
index 1db30705..3bea8dbf 100644
--- a/src/proof/cec/cecCorr_updated.c
+++ b/src/proof/cec/cecCorr_updated.c
@@ -728,7 +728,7 @@ Gia_Man_t * Gia_ManCorrReduce( Gia_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Cec_ManRefinedClassPrintStats( Gia_Man_t * p, Vec_Str_t * vStatus, int iIter, int Time )
+void Cec_ManRefinedClassPrintStats( Gia_Man_t * p, Vec_Str_t * vStatus, int iIter, clock_t Time )
 { 
     int nLits, CounterX = 0, Counter0 = 0, Counter = 0;
     int i, Entry, nProve = 0, nDispr = 0, nFail = 0;
diff --git a/src/proof/cec/cecInt.h b/src/proof/cec/cecInt.h
index 371dedda..8d9fe472 100644
--- a/src/proof/cec/cecInt.h
+++ b/src/proof/cec/cecInt.h
@@ -61,13 +61,13 @@ struct Cec_ManPat_t_
     int              nSeries;        // simulation series
     int              fVerbose;       // verbose stats
     // runtime statistics
-    int              timeFind;       // detecting the pattern  
-    int              timeShrink;     // minimizing the pattern
-    int              timeVerify;     // verifying the result of minimisation
-    int              timeSort;       // sorting literals 
-    int              timePack;       // packing into sim info structures 
-    int              timeTotal;      // total runtime  
-    int              timeTotalSave;  // total runtime for saving  
+    clock_t          timeFind;       // detecting the pattern  
+    clock_t          timeShrink;     // minimizing the pattern
+    clock_t          timeVerify;     // verifying the result of minimisation
+    clock_t          timeSort;       // sorting literals 
+    clock_t          timePack;       // packing into sim info structures 
+    clock_t          timeTotal;      // total runtime  
+    clock_t          timeTotalSave;  // total runtime for saving  
 };
 
 // SAT solving manager
@@ -154,10 +154,10 @@ struct Cec_ManFra_t_
     int              nAllDisproved;  // total number of disproved nodes
     int              nAllFailed;     // total number of failed nodes
     // runtime stats
-    int              timeSim;        // unsat
-    int              timePat;        // unsat
-    int              timeSat;        // sat
-    int              timeTotal;      // total runtime
+    clock_t          timeSim;        // unsat
+    clock_t          timePat;        // unsat
+    clock_t          timeSat;        // sat
+    clock_t          timeTotal;      // total runtime
 };
 
 ////////////////////////////////////////////////////////////////////////
@@ -169,7 +169,7 @@ struct Cec_ManFra_t_
 ////////////////////////////////////////////////////////////////////////
 
 /*=== cecCorr.c ============================================================*/
-extern void                 Cec_ManRefinedClassPrintStats( Gia_Man_t * p, Vec_Str_t * vStatus, int iIter, int Time );
+extern void                 Cec_ManRefinedClassPrintStats( Gia_Man_t * p, Vec_Str_t * vStatus, int iIter, clock_t Time );
 /*=== cecClass.c ============================================================*/
 extern int                  Cec_ManSimClassRemoveOne( Cec_ManSim_t * p, int i );
 extern int                  Cec_ManSimClassesPrepare( Cec_ManSim_t * p, int LevelMax );
diff --git a/src/proof/cec/cecPat.c b/src/proof/cec/cecPat.c
index cb1dae46..f372f3bb 100644
--- a/src/proof/cec/cecPat.c
+++ b/src/proof/cec/cecPat.c
@@ -359,7 +359,8 @@ void Cec_ManPatCleanMark0( Gia_Man_t * p, Gia_Obj_t * pObj )
 void Cec_ManPatSavePattern( Cec_ManPat_t * pMan, Cec_ManSat_t *  p, Gia_Obj_t * pObj )
 {
     Vec_Int_t * vPat;
-    int nPatLits, clk, clkTotal = clock();
+    int nPatLits;
+    clock_t clk, clkTotal = clock();
     assert( Gia_ObjIsCo(pObj) );
     pMan->nPats++;
     pMan->nPatsAll++;
@@ -451,7 +452,7 @@ Vec_Ptr_t * Cec_ManPatCollectPatterns( Cec_ManPat_t *  pMan, int nInputs, int nW
     int iStartOld = pMan->iStart;
     int nWords = nWordsInit;
     int nBits = 32 * nWords;
-    int clk = clock();
+    clock_t clk = clock();
     vInfo = Vec_PtrAllocSimInfo( nInputs, nWords );
     Gia_ManRandomInfo( vInfo, 0, 0, nWords );
     vPres = Vec_PtrAllocSimInfo( nInputs, nWords );
diff --git a/src/proof/cec/cecSeq.c b/src/proof/cec/cecSeq.c
index 2ccbe524..3afbd1c8 100644
--- a/src/proof/cec/cecSeq.c
+++ b/src/proof/cec/cecSeq.c
@@ -215,7 +215,8 @@ int Cec_ManSeqResimulateInfo( Gia_Man_t * pAig, Vec_Ptr_t * vSimInfo, Abc_Cex_t
 int Cec_ManSeqResimulateCounter( Gia_Man_t * pAig, Cec_ParSim_t * pPars, Abc_Cex_t * pCex )
 {
     Vec_Ptr_t * vSimInfo;
-    int RetValue, clkTotal = clock();
+    int RetValue;
+    clock_t clkTotal = clock();
     if ( pCex == NULL )
     {
         Abc_Print( 1, "Cec_ManSeqResimulateCounter(): Counter-example is not available.\n" );
diff --git a/src/proof/cec/cecSolve.c b/src/proof/cec/cecSolve.c
index e779e68c..5e108ae5 100644
--- a/src/proof/cec/cecSolve.c
+++ b/src/proof/cec/cecSolve.c
@@ -471,7 +471,8 @@ int Cec_ManSatCheckNode( Cec_ManSat_t * p, Gia_Obj_t * pObj )
 {
     Gia_Obj_t * pObjR = Gia_Regular(pObj);
     int nBTLimit = p->pPars->nBTLimit;
-    int Lit, RetValue, status, clk, clk2, nConflicts;
+    int Lit, RetValue, status, nConflicts;
+    clock_t clk, clk2;
 
     if ( pObj == Gia_ManConst0(p->pAig) )
         return 1;
@@ -570,7 +571,8 @@ int Cec_ManSatCheckNodeTwo( Cec_ManSat_t * p, Gia_Obj_t * pObj1, Gia_Obj_t * pOb
     Gia_Obj_t * pObjR1 = Gia_Regular(pObj1);
     Gia_Obj_t * pObjR2 = Gia_Regular(pObj2);
     int nBTLimit = p->pPars->nBTLimit;
-    int Lits[2], RetValue, status, clk, clk2, nConflicts;
+    int Lits[2], RetValue, status, nConflicts;
+    clock_t clk, clk2;
 
     if ( pObj1 == Gia_ManConst0(p->pAig) || pObj2 == Gia_ManConst0(p->pAig) || pObj1 == Gia_Not(pObj2) )
         return 1;
@@ -676,7 +678,8 @@ void Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPar
     Bar_Progress_t * pProgress = NULL;
     Cec_ManSat_t * p;
     Gia_Obj_t * pObj;
-    int i, status, clk = clock(), clk2;
+    int i, status;
+    clock_t clk = clock(), clk2;
     // reset the manager
     if ( pPat )
     {
@@ -717,7 +720,7 @@ clk2 = clock();
         // save the pattern
         if ( pPat )
         {
-            int clk3 = clock();
+            clock_t clk3 = clock();
             Cec_ManPatSavePattern( pPat, p, pObj );
             pPat->timeTotalSave += clock() - clk3;
         }
@@ -799,7 +802,8 @@ Vec_Str_t * Cec_ManSatSolveSeq( Vec_Ptr_t * vPatts, Gia_Man_t * pAig, Cec_ParSat
     Cec_ManSat_t * p;
     Gia_Obj_t * pObj;
     int iPat = 0, nPatsInit, nPats;
-    int i, status, clk = clock();
+    int i, status;
+    clock_t clk = clock();
     nPatsInit = nPats = 32 * Vec_PtrReadWordsSimInfo(vPatts);
     Gia_ManSetPhase( pAig );
     Gia_ManLevelNum( pAig );
@@ -957,7 +961,8 @@ Vec_Int_t * Cec_ManSatSolveMiter( Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_St
     Vec_Str_t * vStatus;
     Cec_ManSat_t * p;
     Gia_Obj_t * pObj;
-    int i, status, clk = clock();
+    int i, status;
+    clock_t clk = clock();
     // prepare AIG
     Gia_ManSetPhase( pAig );
     Gia_ManLevelNum( pAig );
diff --git a/src/proof/cec/cecSweep.c b/src/proof/cec/cecSweep.c
index 4523810e..505de076 100644
--- a/src/proof/cec/cecSweep.c
+++ b/src/proof/cec/cecSweep.c
@@ -188,7 +188,8 @@ int Cec_ManFraClassesUpdate( Cec_ManFra_t * p, Cec_ManSim_t * pSim, Cec_ManPat_t
 {
     Vec_Ptr_t * vInfo;
     Gia_Obj_t * pObj, * pObjOld, * pReprOld;
-    int i, k, iRepr, iNode, clk;
+    int i, k, iRepr, iNode;
+    clock_t clk;
 clk = clock();
     vInfo = Cec_ManPatCollectPatterns( pPat, Gia_ManCiNum(p->pAig), pSim->nWords );
 p->timePat += clock() - clk;
diff --git a/src/proof/cec/cecSynth.c b/src/proof/cec/cecSynth.c
index 21470dd4..b13b5204 100644
--- a/src/proof/cec/cecSynth.c
+++ b/src/proof/cec/cecSynth.c
@@ -297,7 +297,8 @@ int Cec_SequentialSynthesisPart( Gia_Man_t * p, Cec_ParSeq_t * pPars )
     Vec_Int_t * vPart;
     int * pMapBack, * pReprs;
     int i, nCountPis, nCountRegs;
-    int nClasses, clk = clock();
+    int nClasses;
+    clock_t clk = clock();
 
     // save parameters
     if ( fPrintParts )
diff --git a/src/proof/dch/dch.h b/src/proof/dch/dch.h
index 731eb776..ff29f0da 100644
--- a/src/proof/dch/dch.h
+++ b/src/proof/dch/dch.h
@@ -54,7 +54,7 @@ struct Dch_Pars_t_
     int              fUseCSat;      // uses circuit-based solver
     int              fLightSynth;   // uses lighter version of synthesis
     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
 };
diff --git a/src/proof/dch/dchCore.c b/src/proof/dch/dchCore.c
index bc78682b..bfef8d8c 100644
--- a/src/proof/dch/dchCore.c
+++ b/src/proof/dch/dchCore.c
@@ -89,7 +89,7 @@ Aig_Man_t * Dch_ComputeChoices( Aig_Man_t * pAig, Dch_Pars_t * pPars )
 {
     Dch_Man_t * p;
     Aig_Man_t * pResult;
-    int clk, clkTotal = clock();
+    clock_t clk, clkTotal = clock();
     // reset random numbers
     Aig_ManRandom(1);
     // start the choicing manager
@@ -131,7 +131,7 @@ p->timeTotal = clock() - clkTotal;
 void Dch_ComputeEquivalences( Aig_Man_t * pAig, Dch_Pars_t * pPars )
 {
     Dch_Man_t * p;
-    int clk, clkTotal = clock();
+    clock_t clk, clkTotal = clock();
     // reset random numbers
     Aig_ManRandom(1);
     // start the choicing manager
diff --git a/src/proof/dch/dchInt.h b/src/proof/dch/dchInt.h
index c9f2f4f6..b22834cf 100644
--- a/src/proof/dch/dchInt.h
+++ b/src/proof/dch/dchInt.h
@@ -84,15 +84,15 @@ struct Dch_Man_t_
     int              nEquivs;        // the number of final equivalences
     int              nChoices;       // the number of final choice nodes
     // runtime stats
-    int              timeSimInit;    // simulation and class computation
-    int              timeSimSat;     // simulation of the counter-examples
-    int              timeSat;        // solving SAT
-    int              timeSatSat;     // sat
-    int              timeSatUnsat;   // unsat
-    int              timeSatUndec;   // undecided
-    int              timeChoice;     // choice computation
-    int              timeOther;      // other runtime
-    int              timeTotal;      // total runtime
+    clock_t          timeSimInit;    // simulation and class computation
+    clock_t          timeSimSat;     // simulation of the counter-examples
+    clock_t          timeSat;        // solving SAT
+    clock_t          timeSatSat;     // sat
+    clock_t          timeSatUnsat;   // unsat
+    clock_t          timeSatUndec;   // undecided
+    clock_t          timeChoice;     // choice computation
+    clock_t          timeOther;      // other runtime
+    clock_t          timeTotal;      // total runtime
 };
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/proof/dch/dchSat.c b/src/proof/dch/dchSat.c
index f5e346ef..fefd5ce2 100644
--- a/src/proof/dch/dchSat.c
+++ b/src/proof/dch/dchSat.c
@@ -45,7 +45,8 @@ ABC_NAMESPACE_IMPL_START
 int Dch_NodesAreEquiv( Dch_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
 {
     int nBTLimit = p->pPars->nBTLimit;
-    int pLits[2], RetValue, RetValue1, status, clk;
+    int pLits[2], RetValue, RetValue1, status;
+    clock_t clk;
     p->nSatCalls++;
 
     // sanity checks
diff --git a/src/proof/dch/dchSimSat.c b/src/proof/dch/dchSimSat.c
index 6f69b47e..26de4643 100644
--- a/src/proof/dch/dchSimSat.c
+++ b/src/proof/dch/dchSimSat.c
@@ -177,7 +177,8 @@ void Dch_ManResimulateOther_rec( Dch_Man_t * p, Aig_Obj_t * pObj )
 void Dch_ManResimulateCex( Dch_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr )
 {
     Aig_Obj_t * pRoot, ** ppClass;
-    int i, k, nSize, RetValue1, RetValue2, clk = clock();
+    int i, k, nSize, RetValue1, RetValue2;
+    clock_t clk = clock();
     // get the equivalence classes
     Dch_ManCollectTfoCands( p, pObj, pRepr );
     // resimulate the cone of influence of the solved nodes
@@ -224,7 +225,8 @@ p->timeSimSat += clock() - clk;
 void Dch_ManResimulateCex2( Dch_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr )
 {
     Aig_Obj_t * pRoot;
-    int i, RetValue, clk = clock();
+    int i, RetValue;
+    clock_t clk = clock();
     // get the equivalence class
     if ( Dch_ObjIsConst1Cand(p->pAigTotal, pObj) )
         Dch_ClassesCollectConst1Group( p->ppClasses, pObj, 500, p->vSimRoots );
diff --git a/src/proof/fra/fra.h b/src/proof/fra/fra.h
index 3e50ff57..c1dd6b44 100644
--- a/src/proof/fra/fra.h
+++ b/src/proof/fra/fra.h
@@ -30,7 +30,6 @@
 #include <stdlib.h>
 #include <string.h>
 #include <assert.h>
-#include <time.h>
 
 #include "src/misc/vec/vec.h"
 #include "src/aig/aig/aig.h"
@@ -238,17 +237,17 @@ struct Fra_Man_t_
     int              nSatCallsRecent;
     int              nSatCallsSkipped;
     // runtime
-    int              timeSim;
-    int              timeTrav;
-    int              timeRwr;
-    int              timeSat;
-    int              timeSatUnsat;
-    int              timeSatSat;
-    int              timeSatFail;
-    int              timeRef;
-    int              timeTotal;
-    int              time1;
-    int              time2;
+    clock_t          timeSim;
+    clock_t          timeTrav;
+    clock_t          timeRwr;
+    clock_t          timeSat;
+    clock_t          timeSatUnsat;
+    clock_t          timeSatSat;
+    clock_t          timeSatFail;
+    clock_t          timeRef;
+    clock_t          timeTotal;
+    clock_t          time1;
+    clock_t          time2;
 };
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/proof/fra/fraBmc.c b/src/proof/fra/fraBmc.c
index 2ddecf48..4b68a79a 100644
--- a/src/proof/fra/fraBmc.c
+++ b/src/proof/fra/fraBmc.c
@@ -311,7 +311,8 @@ Aig_Man_t * Fra_BmcFrames( Fra_Bmc_t * p, int fKeepPos )
 void Fra_BmcPerform( Fra_Man_t * p, int nPref, int nDepth )
 {
     Aig_Obj_t * pObj;
-    int i, nImpsOld = 0, clk = clock();
+    int i, nImpsOld = 0;
+    clock_t clk = clock();
     assert( p->pBmc == NULL );
     // derive and fraig the frames
     p->pBmc = Fra_BmcStart( p->pManAig, nPref, nDepth );
@@ -385,7 +386,8 @@ void Fra_BmcPerformSimple( Aig_Man_t * pAig, int nFrames, int nBTLimit, int fRew
     Fra_Man_t * pTemp;
     Fra_Bmc_t * pBmc;
     Aig_Man_t * pAigTemp;
-    int clk, iOutput;
+    clock_t clk;
+    int iOutput;
     // derive and fraig the frames
     clk = clock();
     pBmc = Fra_BmcStart( pAig, 0, nFrames );
diff --git a/src/proof/fra/fraCec.c b/src/proof/fra/fraCec.c
index 0acca245..20805ec2 100644
--- a/src/proof/fra/fraCec.c
+++ b/src/proof/fra/fraCec.c
@@ -53,7 +53,8 @@ int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimi
 
         sat_solver2 * pSat;
         Cnf_Dat_t * pCnf;
-        int status, RetValue, clk = clock();
+        int status, RetValue;
+        clock_t clk = clock();
         Vec_Int_t * vCiIds;
 
         assert( Aig_ManRegNum(pMan) == 0 );
@@ -159,7 +160,8 @@ int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimi
     {
         sat_solver * pSat;
         Cnf_Dat_t * pCnf;
-        int status, RetValue, clk = clock();
+        int status, RetValue;
+        clock_t clk = clock();
         Vec_Int_t * vCiIds;
 
         assert( Aig_ManRegNum(pMan) == 0 );
@@ -282,7 +284,8 @@ int Fra_FraigCec( Aig_Man_t ** ppAig, int nConfLimit, int fVerbose )
 
     Fra_Par_t Params, * pParams = &Params;
     Aig_Man_t * pAig = *ppAig, * pTemp;
-    int i, RetValue, clk;
+    int i, RetValue;
+    clock_t clk;
 
     // report the original miter
     if ( fVerbose )
@@ -457,7 +460,8 @@ int Fra_FraigCecTop( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nConfLimit, int n
 {
     Aig_Man_t * pTemp;
     //Abc_NtkDarCec( pNtk1, pNtk2, fPartition, fVerbose );
-    int RetValue, clkTotal = clock();
+    int RetValue;
+    clock_t clkTotal = clock();
 
     if ( Aig_ManCiNum(pMan1) != Aig_ManCiNum(pMan1) )
     {
diff --git a/src/proof/fra/fraClaus.c b/src/proof/fra/fraClaus.c
index f651b0ad..97ac3e40 100644
--- a/src/proof/fra/fraClaus.c
+++ b/src/proof/fra/fraClaus.c
@@ -605,7 +605,8 @@ int Fra_ClausProcessClauses( Clu_Man_t * p, int fRefs )
     Fra_Sml_t * pComb, * pSeq;
     Aig_Obj_t * pObj;
     Dar_Cut_t * pCut;
-    int Scores[16], uScores, i, k, j, clk, nCuts = 0;
+    int Scores[16], uScores, i, k, j, nCuts = 0;
+    clock_t clk;
 
     // simulate the AIG
 clk = clock();
@@ -727,7 +728,8 @@ int Fra_ClausProcessClauses2( Clu_Man_t * p, int fRefs )
     Fra_Sml_t * pComb, * pSeq;
     Aig_Obj_t * pObj;
     Aig_Cut_t * pCut;
-    int i, k, j, clk, nCuts = 0;
+    int i, k, j, nCuts = 0;
+    clock_t clk;
     int ScoresSeq[1<<12], ScoresComb[1<<12];
     assert( p->nLutSize < 13 );
 
@@ -1622,7 +1624,7 @@ void Fra_ClausEstimateCoverage( Clu_Man_t * p )
     unsigned * pResultTot, * pResultOne;
     int nCovered, Beg, End, i, w;
     int * pStart, * pVar2Id; 
-    int clk = clock();
+    clock_t clk = clock();
     // simulate the circuit with nCombSimWords * 32 = 64K patterns
 //    srand( 0xAABBAABB );
     Aig_ManRandom(1);
@@ -1680,7 +1682,7 @@ void Fra_ClausEstimateCoverage( Clu_Man_t * p )
 int Fra_Claus( Aig_Man_t * pAig, int nFrames, int nPref, int nClausesMax, int nLutSize, int nLevels, int nCutsMax, int nBatches, int fStepUp, int fBmc, int fRefs, int fTarget, int fVerbose, int fVeryVerbose )
 {
     Clu_Man_t * p;
-    int clk, clkTotal = clock(), clkInd;
+    clock_t clk, clkTotal = clock(), clkInd;
     int b, Iter, Counter, nPrefOld;
     int nClausesBeg = 0;
 
diff --git a/src/proof/fra/fraCore.c b/src/proof/fra/fraCore.c
index 37aaa0da..35888f43 100644
--- a/src/proof/fra/fraCore.c
+++ b/src/proof/fra/fraCore.c
@@ -376,7 +376,7 @@ Aig_Man_t * Fra_FraigPerform( Aig_Man_t * pManAig, Fra_Par_t * pPars )
 {
     Fra_Man_t * p;
     Aig_Man_t * pManAigNew;
-    int clk;
+    clock_t clk;
     if ( Aig_ManNodeNum(pManAig) == 0 )
         return Aig_ManDupOrdered(pManAig);
 clk = clock();
@@ -402,7 +402,7 @@ Fra_ClassesPrint( p->pCla, 1 );
     Fra_ManFinalizeComb( p );
     if ( p->pPars->fChoicing )
     { 
-int clk2 = clock();
+clock_t clk2 = clock();
         Fra_ClassesCopyReprs( p->pCla, p->vTimeouts );
         pManAigNew = Aig_ManDupRepr( p->pManAig, 1 );
         Aig_ManReprStart( pManAigNew, Aig_ManObjNumMax(pManAigNew) );
diff --git a/src/proof/fra/fraHot.c b/src/proof/fra/fraHot.c
index 338b5717..a91c939f 100644
--- a/src/proof/fra/fraHot.c
+++ b/src/proof/fra/fraHot.c
@@ -332,7 +332,7 @@ void Fra_OneHotEstimateCoverage( Fra_Man_t * p, Vec_Int_t * vOneHots )
     Vec_Ptr_t * vSimInfo;
     unsigned * pSim1, * pSim2, * pSimTot;
     int i, w, Out1, Out2, nCovered, Counter = 0;
-    int clk = clock();
+    clock_t clk = clock();
 
     // generate random sim-info at register outputs
     vSimInfo = Vec_PtrAllocSimInfo( nRegs + 1, nSimWords );
diff --git a/src/proof/fra/fraImp.c b/src/proof/fra/fraImp.c
index f65aca5c..4d33717a 100644
--- a/src/proof/fra/fraImp.c
+++ b/src/proof/fra/fraImp.c
@@ -327,7 +327,8 @@ Vec_Int_t * Fra_ImpDerive( Fra_Man_t * p, int nImpMaxLimit, int nImpUseLimit, in
     int * pImpCosts, * pNodesI, * pNodesK;
     int nImpsTotal = 0, nImpsTried = 0, nImpsNonSeq = 0, nImpsComb = 0, nImpsCollected = 0;
     int CostMin = ABC_INFINITY, CostMax = 0;
-    int i, k, Imp, CostRange, clk = clock();
+    int i, k, Imp, CostRange;
+    clock_t clk = clock();
     assert( Aig_ManObjNumMax(p->pManAig) < (1 << 15) );
     assert( nImpMaxLimit > 0 && nImpUseLimit > 0 && nImpUseLimit <= nImpMaxLimit );
     // normalize both managers
diff --git a/src/proof/fra/fraInd.c b/src/proof/fra/fraInd.c
index 29a76eea..633f8979 100644
--- a/src/proof/fra/fraInd.c
+++ b/src/proof/fra/fraInd.c
@@ -49,7 +49,8 @@ void Fra_FraigInductionRewrite( Fra_Man_t * p )
 {
     Aig_Man_t * pTemp;
     Aig_Obj_t * pObj, * pObjPo;
-    int nTruePis, k, i, clk = clock();
+    int nTruePis, k, i;
+    clock_t clk = clock();
     // perform AIG rewriting on the speculated frames
 //    pTemp = Dar_ManRwsat( pTemp, 1, 0 );
     pTemp = Dar_ManRewriteDefault( p->pManFraig );
@@ -259,7 +260,7 @@ Aig_Man_t * Fra_FraigInductionPart( Aig_Man_t * pAig, Fra_Ssw_t * pPars )
     int * pMapBack;
     int i, nCountPis, nCountRegs;
     int nClasses, nPartSize, fVerbose;
-    int clk = clock();
+    clock_t clk = clock();
 
     // save parameters
     nPartSize = pPars->nPartSize; pPars->nPartSize = 0;
@@ -357,8 +358,9 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, Fra_Ssw_t * pParams )
     Aig_Man_t * pManAigNew = NULL;
     int nNodesBeg, nRegsBeg;
     int nIter = -1; // Suppress "might be used uninitialized"
-    int i, clk = clock(), clk2;
-    int TimeToStop = (pParams->TimeLimit == 0.0)? 0 : clock() + (int)(pParams->TimeLimit * CLOCKS_PER_SEC);
+    int i;
+    clock_t clk = clock(), clk2;
+    clock_t TimeToStop = pParams->TimeLimit ? pParams->TimeLimit * CLOCKS_PER_SEC + clock() : 0;
 
     if ( Aig_ManNodeNum(pManAig) == 0 )
     {
@@ -473,7 +475,7 @@ ABC_PRT( "Time", clock() - clk );
         int nLitsOld = Fra_ClassesCountLits(p->pCla);
         int nImpsOld = p->pCla->vImps? Vec_IntSize(p->pCla->vImps) : 0;
         int nHotsOld = p->vOneHots? Fra_OneHotCount(p, p->vOneHots) : 0;
-        int clk3 = clock();
+        clock_t clk3 = clock();
 
         if ( pParams->TimeLimit != 0.0 && clock() > TimeToStop )
         {
diff --git a/src/proof/fra/fraIndVer.c b/src/proof/fra/fraIndVer.c
index 7c5e9e70..099256ac 100644
--- a/src/proof/fra/fraIndVer.c
+++ b/src/proof/fra/fraIndVer.c
@@ -50,7 +50,7 @@ int Fra_InvariantVerify( Aig_Man_t * pAig, int nFrames, Vec_Int_t * vClauses, Ve
     int * pStart;
     int RetValue, Beg, End, i, k;
     int CounterBase = 0, CounterInd = 0;
-    int clk = clock();
+    clock_t clk = clock();
 
     if ( nFrames != 1 )
     {
diff --git a/src/proof/fra/fraLcr.c b/src/proof/fra/fraLcr.c
index 8ea6d297..2941f24f 100644
--- a/src/proof/fra/fraLcr.c
+++ b/src/proof/fra/fraLcr.c
@@ -54,12 +54,12 @@ struct Fra_Lcr_t_
     int              nRegsBeg;
     int              nRegsEnd;
     // runtime
-    int              timeSim;
-    int              timePart;
-    int              timeTrav;
-    int              timeFraig;
-    int              timeUpdate;
-    int              timeTotal;
+    clock_t          timeSim;
+    clock_t          timePart;
+    clock_t          timeTrav;
+    clock_t          timeFraig;
+    clock_t          timeUpdate;
+    clock_t          timeTotal;
 };
 
 ////////////////////////////////////////////////////////////////////////
@@ -538,8 +538,9 @@ Aig_Man_t * Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int nFramesP, int nC
     Fra_Man_t * pTemp;
     Aig_Man_t * pAigPart, * pAigTemp, * pAigNew = NULL;
     Vec_Int_t * vPart;
-    int i, nIter, timeSim, clk2, clk3, clk = clock();
-    int TimeToStop = (TimeLimit == 0.0)? 0 : clock() + (int)(TimeLimit * CLOCKS_PER_SEC);
+    int i, nIter;
+    clock_t timeSim, clk2, clk3, clk = clock();
+    clock_t TimeToStop = TimeLimit ? TimeLimit * CLOCKS_PER_SEC + clock() : 0;
     if ( Aig_ManNodeNum(pAig) == 0 )
     {
         if ( pnIter ) *pnIter = 0;
diff --git a/src/proof/fra/fraPart.c b/src/proof/fra/fraPart.c
index e3bb2850..e1c8ddf4 100644
--- a/src/proof/fra/fraPart.c
+++ b/src/proof/fra/fraPart.c
@@ -53,7 +53,7 @@ void Fra_ManPartitionTest( Aig_Man_t * p, int nComLim )
     int i, k, nCommon, CountOver, CountQuant;
     int nTotalSupp, nTotalSupp2, Entry, Largest;//, iVar;
     double Ratio, R;
-    int clk;
+    clock_t clk;
 
     nTotalSupp = 0;
     nTotalSupp2 = 0;
@@ -190,7 +190,8 @@ void Fra_ManPartitionTest2( Aig_Man_t * p )
     Vec_Int_t * vSup, * vSup2, * vSup3;
     Aig_Obj_t * pObj;
     int Entry, Entry2, Entry3, Counter;
-    int i, k, m, n, clk;
+    int i, k, m, n;
+    clock_t clk;
     char * pSupp;
  
     // compute supports
diff --git a/src/proof/fra/fraSat.c b/src/proof/fra/fraSat.c
index 2702113c..fc95fd62 100644
--- a/src/proof/fra/fraSat.c
+++ b/src/proof/fra/fraSat.c
@@ -47,7 +47,8 @@ static int Fra_SetActivityFactors( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t *
 ***********************************************************************/
 int Fra_NodesAreEquiv( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
 {
-    int pLits[4], RetValue, RetValue1, nBTLimit, clk;//, clk2 = clock();
+    int pLits[4], RetValue, RetValue1, nBTLimit;
+    clock_t clk;//, clk2 = clock();
     int status;
 
     // make sure the nodes are not complemented
@@ -207,7 +208,8 @@ p->timeSatFail += clock() - clk;
 ***********************************************************************/
 int Fra_NodesAreImp( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew, int fComplL, int fComplR )
 {
-    int pLits[4], RetValue, RetValue1, nBTLimit, clk;//, clk2 = clock();
+    int pLits[4], RetValue, RetValue1, nBTLimit;
+    clock_t clk;//, clk2 = clock();
     int status;
 
     // make sure the nodes are not complemented
@@ -314,7 +316,8 @@ p->timeSatFail += clock() - clk;
 ***********************************************************************/
 int Fra_NodesAreClause( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew, int fComplL, int fComplR )
 {
-    int pLits[4], RetValue, RetValue1, nBTLimit, clk;//, clk2 = clock();
+    int pLits[4], RetValue, RetValue1, nBTLimit;
+    clock_t clk;//, clk2 = clock();
     int status;
 
     // make sure the nodes are not complemented
@@ -421,7 +424,8 @@ p->timeSatFail += clock() - clk;
 ***********************************************************************/
 int Fra_NodeIsConst( Fra_Man_t * p, Aig_Obj_t * pNew )
 {
-    int pLits[2], RetValue1, RetValue, clk;
+    int pLits[2], RetValue1, RetValue;
+    clock_t clk;
 
     // make sure the nodes are not complemented
     assert( !Aig_IsComplement(pNew) );
@@ -535,7 +539,8 @@ int Fra_SetActivityFactors_rec( Fra_Man_t * p, Aig_Obj_t * pObj, int LevelMin, i
 ***********************************************************************/
 int Fra_SetActivityFactors( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_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/proof/fra/fraSec.c b/src/proof/fra/fraSec.c
index cde56809..ac6cd67e 100644
--- a/src/proof/fra/fraSec.c
+++ b/src/proof/fra/fraSec.c
@@ -98,7 +98,8 @@ int Fra_FraigSec( Aig_Man_t * p, Fra_Sec_t * pParSec, Aig_Man_t ** ppResult )
     Fra_Ssw_t Pars, * pPars = &Pars;
     Fra_Sml_t * pSml;
     Aig_Man_t * pNew, * pTemp;
-    int nFrames, RetValue, nIter, clk, clkTotal = clock();
+    int nFrames, RetValue, nIter;
+    clock_t clk, clkTotal = clock();
     int TimeOut = 0;
     int fLatchCorr = 0;
     float TimeLeft = 0.0;
diff --git a/src/proof/fra/fraSim.c b/src/proof/fra/fraSim.c
index 66579be3..555789e2 100644
--- a/src/proof/fra/fraSim.c
+++ b/src/proof/fra/fraSim.c
@@ -662,7 +662,8 @@ int Fra_SmlCheckNonConstOutputs( Fra_Sml_t * p )
 void Fra_SmlSimulateOne( Fra_Sml_t * p )
 {
     Aig_Obj_t * pObj, * pObjLi, * pObjLo;
-    int f, i, clk;
+    int f, i;
+    clock_t clk;
 clk = clock();
     for ( f = 0; f < p->nFrames; f++ )
     {
@@ -700,7 +701,8 @@ p->nSimRounds++;
 ***********************************************************************/
 void Fra_SmlResimulate( Fra_Man_t * p )
 {
-    int nChanges, clk;
+    int nChanges;
+    clock_t clk;
     Fra_SmlAssignDist1( p->pSml, p->pPatWords );
     Fra_SmlSimulateOne( p->pSml );
 //    if ( p->pPars->fPatScores )
@@ -735,7 +737,8 @@ p->timeRef += clock() - clk;
 void Fra_SmlSimulate( Fra_Man_t * p, int fInit )
 {
     int fVerbose = 0;
-    int nChanges, nClasses, clk;
+    int nChanges, nClasses;
+    clock_t clk;
     assert( !fInit || Aig_ManRegNum(p->pManAig) );
     // start the classes
     Fra_SmlInitialize( p->pSml, fInit );
diff --git a/src/proof/fraig/fraig.h b/src/proof/fraig/fraig.h
index 6d672716..0c021feb 100644
--- a/src/proof/fraig/fraig.h
+++ b/src/proof/fraig/fraig.h
@@ -154,9 +154,6 @@ extern void                Fraig_ManSetDoSparse( Fraig_Man_t * p, int fDoSparse
 extern void                Fraig_ManSetChoicing( Fraig_Man_t * p, int fChoicing ); 
 extern void                Fraig_ManSetTryProve( Fraig_Man_t * p, int fTryProve );
 extern void                Fraig_ManSetVerbose( Fraig_Man_t * p, int fVerbose );        
-extern void                Fraig_ManSetTimeToGraph( Fraig_Man_t * p, int Time );        
-extern void                Fraig_ManSetTimeToNet( Fraig_Man_t * p, int Time );          
-extern void                Fraig_ManSetTimeTotal( Fraig_Man_t * p, int Time );          
 extern void                Fraig_ManSetOutputNames( Fraig_Man_t * p, char ** ppNames ); 
 extern void                Fraig_ManSetInputNames( Fraig_Man_t * p, char ** ppNames );  
 extern void                Fraig_ManSetPo( Fraig_Man_t * p, Fraig_Node_t * pNode );
diff --git a/src/proof/fraig/fraigApi.c b/src/proof/fraig/fraigApi.c
index 6e0ab959..b0b47075 100644
--- a/src/proof/fraig/fraigApi.c
+++ b/src/proof/fraig/fraigApi.c
@@ -91,9 +91,6 @@ void            Fraig_ManSetDoSparse( Fraig_Man_t * p, int fDoSparse )      { p-
 void            Fraig_ManSetChoicing( Fraig_Man_t * p, int fChoicing )      { p->fChoicing = fChoicing; }
 void            Fraig_ManSetTryProve( Fraig_Man_t * p, int fTryProve )      { p->fTryProve = fTryProve; }
 void            Fraig_ManSetVerbose( Fraig_Man_t * p, int fVerbose )        { p->fVerbose  = fVerbose;  }
-void            Fraig_ManSetTimeToGraph( Fraig_Man_t * p, int Time )        { p->timeToAig = Time;      }
-void            Fraig_ManSetTimeToNet( Fraig_Man_t * p, int Time )          { p->timeToNet = Time;      }
-void            Fraig_ManSetTimeTotal( Fraig_Man_t * p, int Time )          { p->timeTotal = Time;      }
 void            Fraig_ManSetOutputNames( Fraig_Man_t * p, char ** ppNames ) { p->ppOutputNames = ppNames; }
 void            Fraig_ManSetInputNames( Fraig_Man_t * p, char ** ppNames )  { p->ppInputNames  = ppNames; }
 
diff --git a/src/proof/fraig/fraigChoice.c b/src/proof/fraig/fraigChoice.c
index 21d4fe10..e1d6e8a7 100644
--- a/src/proof/fraig/fraigChoice.c
+++ b/src/proof/fraig/fraigChoice.c
@@ -45,7 +45,7 @@ void Fraig_ManAddChoices( Fraig_Man_t * pMan, int fVerbose, int nLimit )
 {
 //    ProgressBar * pProgress;
     char Buffer[100];
-    int clkTotal = clock();
+    clock_t clkTotal = clock();
     int i, nNodesBefore, nNodesAfter, nInputs, nMaxNodes;
     int /*nMaxLevel,*/ nDistributive;
     Fraig_Node_t *pNode, *pRepr;
diff --git a/src/proof/fraig/fraigFeed.c b/src/proof/fraig/fraigFeed.c
index 47f946e1..4cb1276b 100644
--- a/src/proof/fraig/fraigFeed.c
+++ b/src/proof/fraig/fraigFeed.c
@@ -80,7 +80,8 @@ void Fraig_FeedBackInit( Fraig_Man_t * p )
 void Fraig_FeedBack( Fraig_Man_t * p, int * pModel, Msat_IntVec_t * vVars, Fraig_Node_t * pOld, Fraig_Node_t * pNew )
 {
     int nVarsPi, nWords;
-    int i, clk = clock();
+    int i;
+    clock_t clk = clock();
 
     // get the number of PI vars in the feedback (also sets the PI values)
     nVarsPi = Fraig_FeedBackPrepare( p, pModel, vVars );
diff --git a/src/proof/fraig/fraigInt.h b/src/proof/fraig/fraigInt.h
index f6a5d74f..1ff8727e 100644
--- a/src/proof/fraig/fraigInt.h
+++ b/src/proof/fraig/fraigInt.h
@@ -28,7 +28,6 @@
 #include <stdlib.h>
 #include <string.h>
 #include <assert.h>
-#include <time.h>
 
 #include "src/misc/util/abc_global.h"
 #include "fraig.h"
@@ -189,18 +188,18 @@ struct Fraig_ManStruct_t_
     int                   nImplies1;
 
     // runtime statistics
-    int                   timeToAig;     // time to transfer to the mapping structure
-    int                   timeSims;      // time to compute k-feasible cuts
-    int                   timeTrav;      // time to traverse the network
-    int                   timeFeed;      // time for solver feedback (recording and resimulating)
-    int                   timeImply;     // time to analyze implications
-    int                   timeSat;       // time to compute the truth table for each cut
-    int                   timeToNet;     // time to transfer back to the network
-    int                   timeTotal;     // the total mapping time
-    int                   time1;         // time to perform one task
-    int                   time2;         // time to perform another task
-    int                   time3;         // time to perform another task
-    int                   time4;         // time to perform another task
+    clock_t               timeToAig;     // time to transfer to the mapping structure
+    clock_t               timeSims;      // time to compute k-feasible cuts
+    clock_t               timeTrav;      // time to traverse the network
+    clock_t               timeFeed;      // time for solver feedback (recording and resimulating)
+    clock_t               timeImply;     // time to analyze implications
+    clock_t               timeSat;       // time to compute the truth table for each cut
+    clock_t               timeToNet;     // time to transfer back to the network
+    clock_t               timeTotal;     // the total mapping time
+    clock_t               time1;         // time to perform one task
+    clock_t               time2;         // time to perform another task
+    clock_t               time3;         // time to perform another task
+    clock_t               time4;         // time to perform another task
 };
 
 // the mapping node
diff --git a/src/proof/fraig/fraigMan.c b/src/proof/fraig/fraigMan.c
index 125a4da1..bc7c423d 100644
--- a/src/proof/fraig/fraigMan.c
+++ b/src/proof/fraig/fraigMan.c
@@ -25,8 +25,8 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-int timeSelect;
-int timeAssign;
+clock_t timeSelect;
+clock_t timeAssign;
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -323,8 +323,8 @@ void Fraig_ManFree( Fraig_Man_t * p )
 ***********************************************************************/
 void Fraig_ManCreateSolver( Fraig_Man_t * p )
 {
-    extern int timeSelect;
-    extern int timeAssign;
+    extern clock_t timeSelect;
+    extern clock_t timeAssign;
     assert( p->pSat == NULL );
     // allocate data for SAT solving
     p->pSat       = Msat_SolverAlloc( 500, 1, 1, 1, 1, 0 );
diff --git a/src/proof/fraig/fraigNode.c b/src/proof/fraig/fraigNode.c
index 609d5f65..5310534b 100644
--- a/src/proof/fraig/fraigNode.c
+++ b/src/proof/fraig/fraigNode.c
@@ -87,7 +87,8 @@ Fraig_Node_t * Fraig_NodeCreateConst( Fraig_Man_t * p )
 Fraig_Node_t * Fraig_NodeCreatePi( Fraig_Man_t * p )
 {
     Fraig_Node_t * pNode, * pNodeRes;
-    int i, clk;
+    int i;
+    clock_t clk;
 
     // create the node
     pNode = (Fraig_Node_t *)Fraig_MemFixedEntryFetch( p->mmNodes );
@@ -159,7 +160,7 @@ p->timeSims += clock() - clk;
 Fraig_Node_t * Fraig_NodeCreate( Fraig_Man_t * p, Fraig_Node_t * p1, Fraig_Node_t * p2 )
 {
     Fraig_Node_t * pNode;
-    int clk;
+    clock_t clk;
 
     // create the node
     pNode = (Fraig_Node_t *)Fraig_MemFixedEntryFetch( p->mmNodes );
diff --git a/src/proof/fraig/fraigSat.c b/src/proof/fraig/fraigSat.c
index 6ccd1b86..7a11c072 100644
--- a/src/proof/fraig/fraigSat.c
+++ b/src/proof/fraig/fraigSat.c
@@ -85,7 +85,8 @@ int Fraig_NodesAreEqual( Fraig_Man_t * p, Fraig_Node_t * pNode1, Fraig_Node_t *
 void Fraig_ManProveMiter( Fraig_Man_t * p )
 {
     Fraig_Node_t * pNode;
-    int i, clk;
+    int i;
+    clock_t clk;
 
     if ( !p->fTryProve )
         return;
@@ -300,7 +301,8 @@ void Fraig_VarsStudy( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * pNew
 ***********************************************************************/
 int Fraig_NodeIsEquivalent( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * pNew, int nBTLimit, int nTimeLimit )
 {
-    int RetValue, RetValue1, i, fComp, clk;
+    int RetValue, RetValue1, i, fComp;
+    clock_t clk;
     int fVerbose = 0;
     int fSwitch = 0;
 
@@ -548,7 +550,8 @@ p->time3 += clock() - clk;
 ***********************************************************************/
 int Fraig_NodeIsImplication( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * pNew, int nBTLimit )
 {
-    int RetValue, RetValue1, i, fComp, clk;
+    int RetValue, RetValue1, i, fComp;
+    clock_t clk;
     int fVerbose = 0;
 
     // make sure the nodes are not complemented
@@ -650,7 +653,8 @@ p->time3 += clock() - clk;
 int Fraig_ManCheckClauseUsingSat( Fraig_Man_t * p, Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int nBTLimit )
 {
     Fraig_Node_t * pNode1R, * pNode2R;
-    int RetValue, RetValue1, i, clk;
+    int RetValue, RetValue1, i;
+    clock_t clk;
     int fVerbose = 0;
 
     pNode1R = Fraig_Regular(pNode1);
diff --git a/src/proof/fraig/fraigTable.c b/src/proof/fraig/fraigTable.c
index 6611e4fa..d184ab7f 100644
--- a/src/proof/fraig/fraigTable.c
+++ b/src/proof/fraig/fraigTable.c
@@ -260,7 +260,8 @@ void Fraig_TableResizeS( Fraig_HashTable_t * p )
 {
     Fraig_Node_t ** pBinsNew;
     Fraig_Node_t * pEnt, * pEnt2;
-    int nBinsNew, Counter, i, clk;
+    int nBinsNew, Counter, i;
+    clock_t clk;
     unsigned Key;
 
 clk = clock();
@@ -303,7 +304,8 @@ void Fraig_TableResizeF( Fraig_HashTable_t * p, int fUseSimR )
 {
     Fraig_Node_t ** pBinsNew;
     Fraig_Node_t * pEnt, * pEnt2;
-    int nBinsNew, Counter, i, clk;
+    int nBinsNew, Counter, i;
+    clock_t clk;
     unsigned Key;
 
 clk = clock();
diff --git a/src/proof/fraig/fraigUtil.c b/src/proof/fraig/fraigUtil.c
index ae78a61f..316b492e 100644
--- a/src/proof/fraig/fraigUtil.c
+++ b/src/proof/fraig/fraigUtil.c
@@ -844,7 +844,7 @@ int Fraig_ManPrintRefs( Fraig_Man_t * pMan )
     Fraig_NodeVec_t * vPivots;
     Fraig_Node_t * pNode, * pNode2;
     int i, k, Counter, nProved;
-    int clk;
+    clock_t clk;
 
     vPivots = Fraig_NodeVecAlloc( 1000 );
     for ( i = 0; i < pMan->vNodes->nSize; i++ )
diff --git a/src/proof/int/intCheck.c b/src/proof/int/intCheck.c
index 2b14d8ae..28ef54a7 100644
--- a/src/proof/int/intCheck.c
+++ b/src/proof/int/intCheck.c
@@ -217,7 +217,7 @@ void Inter_CheckAddEqual( Inter_Check_t * p, int iVarA, int iVarB )
   SeeAlso     []
 
 ***********************************************************************/
-int Inter_CheckPerform( Inter_Check_t * p, Cnf_Dat_t * pCnfInt, int nTimeNewOut )
+int Inter_CheckPerform( Inter_Check_t * p, Cnf_Dat_t * pCnfInt, clock_t nTimeNewOut )
 {
     Aig_Obj_t * pObj, * pObj2;
     int i, f, VarA, VarB, RetValue, Entry, status;
diff --git a/src/proof/int/intCore.c b/src/proof/int/intCore.c
index d4ef1f94..c226c7e1 100644
--- a/src/proof/int/intCore.c
+++ b/src/proof/int/intCore.c
@@ -80,8 +80,9 @@ int Inter_ManPerformInterpolation( Aig_Man_t * pAig, Inter_ManParams_t * pPars,
     Inter_Man_t * p;
     Inter_Check_t * pCheck = NULL;
     Aig_Man_t * pAigTemp;
-    int s, i, RetValue, Status, clk, clk2, clkTotal = clock(), timeTemp = 0;
-    int nTimeNewOut = pPars->nSecLimit ? time(NULL) + pPars->nSecLimit : 0;
+    int s, i, RetValue, Status;
+    clock_t clk, clk2, clkTotal = clock(), timeTemp = 0;
+    clock_t nTimeNewOut = pPars->nSecLimit ? pPars->nSecLimit * CLOCKS_PER_SEC + clock() : 0;
 
     // enable ORing of the interpolants, if containment check is performed inductively with K > 1
     if ( pPars->nFramesK > 1 )
@@ -256,7 +257,7 @@ p->timeEqu += clock() - clk;
             }
             else if ( RetValue == -1 ) 
             {
-                if ( pPars->nSecLimit && time(NULL) > nTimeNewOut ) // timed out
+                if ( pPars->nSecLimit && clock() > nTimeNewOut ) // timed out
                 {
                     if ( pPars->fVerbose )
                         printf( "Reached timeout (%d seconds).\n",  pPars->nSecLimit );
@@ -341,7 +342,7 @@ p->timeEqu += clock() - clk - timeTemp;
                 Inter_CheckStop( pCheck );
                 return 1;
             }
-            if ( pPars->nSecLimit && time(NULL) > nTimeNewOut )
+            if ( pPars->nSecLimit && clock() > nTimeNewOut )
             {
                 printf( "Reached timeout (%d seconds).\n",  pPars->nSecLimit );
                 p->timeTotal = clock() - clkTotal;
diff --git a/src/proof/int/intCtrex.c b/src/proof/int/intCtrex.c
index 04aaa271..840ae75d 100644
--- a/src/proof/int/intCtrex.c
+++ b/src/proof/int/intCtrex.c
@@ -99,7 +99,8 @@ void * Inter_ManGetCounterExample( Aig_Man_t * pAig, int nFrames, int fVerbose )
     Aig_Man_t * pFrames;
     sat_solver * pSat;
     Cnf_Dat_t * pCnf;
-    int status, clk = clock();
+    int status;
+    clock_t clk = clock();
     Vec_Int_t * vCiIds;
     // create timeframes
     assert( Saig_ManPoNum(pAig) == 1 );
diff --git a/src/proof/int/intInt.h b/src/proof/int/intInt.h
index 6a033d85..ec2a0356 100644
--- a/src/proof/int/intInt.h
+++ b/src/proof/int/intInt.h
@@ -70,13 +70,13 @@ struct Inter_Man_t_
     int              nConfLimit;   // the limit on the number of conflicts
     int              fVerbose;     // the verbosiness flag
     // runtime
-    int              timeRwr;
-    int              timeCnf;
-    int              timeSat;
-    int              timeInt;
-    int              timeEqu;
-    int              timeOther;
-    int              timeTotal;
+    clock_t          timeRwr;
+    clock_t          timeCnf;
+    clock_t          timeSat;
+    clock_t          timeInt;
+    clock_t          timeEqu;
+    clock_t          timeOther;
+    clock_t          timeTotal;
 };
 
 // containment checking manager
@@ -93,7 +93,7 @@ typedef struct Inter_Check_t_ Inter_Check_t;
 /*=== intCheck.c ============================================================*/
 extern Inter_Check_t * Inter_CheckStart( Aig_Man_t * pTrans, int nFramesK );
 extern void            Inter_CheckStop( Inter_Check_t * p );
-extern int             Inter_CheckPerform( Inter_Check_t * p, Cnf_Dat_t * pCnf, int nTimeNewOut );
+extern int             Inter_CheckPerform( Inter_Check_t * p, Cnf_Dat_t * pCnf, clock_t nTimeNewOut );
 
 /*=== intContain.c ============================================================*/
 extern int             Inter_ManCheckContainment( Aig_Man_t * pNew, Aig_Man_t * pOld );
@@ -117,7 +117,7 @@ extern void            Inter_ManClean( Inter_Man_t * p );
 extern void            Inter_ManStop( Inter_Man_t * p, int fProved );
 
 /*=== intM114.c ============================================================*/
-extern int             Inter_ManPerformOneStep( Inter_Man_t * p, int fUseBias, int fUseBackward, int nTimeNewOut );
+extern int             Inter_ManPerformOneStep( Inter_Man_t * p, int fUseBias, int fUseBackward, clock_t nTimeNewOut );
 
 /*=== intM114p.c ============================================================*/
 #ifdef ABC_USE_LIBRARIES
diff --git a/src/proof/int/intM114.c b/src/proof/int/intM114.c
index ed3ef80e..bf44696d 100644
--- a/src/proof/int/intM114.c
+++ b/src/proof/int/intM114.c
@@ -200,15 +200,16 @@ sat_solver * Inter_ManDeriveSatSolver(
   SeeAlso     []
 
 ***********************************************************************/
-int Inter_ManPerformOneStep( Inter_Man_t * p, int fUseBias, int fUseBackward, int nTimeNewOut )
+int Inter_ManPerformOneStep( Inter_Man_t * p, int fUseBias, int fUseBackward, clock_t nTimeNewOut )
 {
     sat_solver * pSat;
     void * pSatCnf = NULL;
     Inta_Man_t * pManInterA; 
 //    Intb_Man_t * pManInterB; 
     int * pGlobalVars;
-    int clk, status, RetValue;
+    int status, RetValue;
     int i, Var;
+    clock_t clk;
 //    assert( p->pInterNew == NULL );
 
     // derive the SAT solver
diff --git a/src/proof/int/intUtil.c b/src/proof/int/intUtil.c
index 8027bdef..b93a7453 100644
--- a/src/proof/int/intUtil.c
+++ b/src/proof/int/intUtil.c
@@ -49,7 +49,7 @@ int Inter_ManCheckInitialState( Aig_Man_t * p )
     Aig_Obj_t * pObj;
     sat_solver * pSat;
     int i, status;
-    int clk = clock();
+    clock_t clk = clock();
     pCnf = Cnf_Derive( p, Saig_ManRegNum(p) ); 
     pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 1 );
     if ( pSat == NULL )
@@ -87,7 +87,7 @@ int Inter_ManCheckAllStates( Aig_Man_t * p )
     Cnf_Dat_t * pCnf;
     sat_solver * pSat;
     int status;
-    int clk = clock();
+    clock_t clk = clock();
     pCnf = Cnf_Derive( p, Saig_ManRegNum(p) ); 
     pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
     Cnf_DataFree( pCnf );
diff --git a/src/proof/llb/llb.h b/src/proof/llb/llb.h
index a9bfd891..464f4526 100644
--- a/src/proof/llb/llb.h
+++ b/src/proof/llb/llb.h
@@ -65,7 +65,7 @@ struct Gia_ParLlb_t_
     int         TimeLimit;     // time limit for one reachability run
     int         TimeLimitGlo;  // time limit for all reachability runs
     // internal parameters
-    int         TimeTarget;    // the time to stop
+    clock_t     TimeTarget;    // the time to stop
     int         iFrame;        // explored up to this frame
 };
 
diff --git a/src/proof/llb/llb1Core.c b/src/proof/llb/llb1Core.c
index 56e0cc6b..b16fdee7 100644
--- a/src/proof/llb/llb1Core.c
+++ b/src/proof/llb/llb1Core.c
@@ -114,7 +114,7 @@ int Llb_ManModelCheckAig( Aig_Man_t * pAigGlo, Gia_ParLlb_t * pPars, Vec_Int_t *
     Llb_Man_t * p = NULL; 
     Aig_Man_t * pAig;
     int RetValue = -1;
-    int clk = clock();
+    clock_t clk = clock();
 
     if ( pPars->fIndConstr )
     {
diff --git a/src/proof/llb/llb1Hint.c b/src/proof/llb/llb1Hint.c
index 51d3a9fc..07877a98 100644
--- a/src/proof/llb/llb1Hint.c
+++ b/src/proof/llb/llb1Hint.c
@@ -165,7 +165,7 @@ int Llb_ManModelCheckAigWithHints( Aig_Man_t * pAigGlo, Gia_ParLlb_t * pPars )
     Vec_Int_t * vHints;
     Vec_Int_t * vHFCands;
     int i, Entry, RetValue = -1;
-    int clk = clock();
+    clock_t clk = clock();
     assert( pPars->nHintDepth > 0 );
 /*
     // perform reachability without hints
diff --git a/src/proof/llb/llb1Reach.c b/src/proof/llb/llb1Reach.c
index 60124378..fed0389a 100644
--- a/src/proof/llb/llb1Reach.c
+++ b/src/proof/llb/llb1Reach.c
@@ -47,7 +47,8 @@ DdNode * Llb_ManConstructOutBdd( Aig_Man_t * pAig, Aig_Obj_t * pNode, DdManager
     DdNode * bBdd0, * bBdd1, * bFunc;
     Vec_Ptr_t * vNodes;
     Aig_Obj_t * pObj;
-    int i, TimeStop;
+    int i;
+    clock_t TimeStop;
     if ( Aig_ObjFanin0(pNode) == Aig_ManConst1(pAig) )
         return Cudd_NotCond( Cudd_ReadOne(dd), Aig_ObjFaninC0(pNode) );
     TimeStop = dd->TimeStop;  dd->TimeStop = 0;
@@ -156,7 +157,7 @@ DdNode * Llb_ManConstructQuantCubeIntern( Llb_Man_t * p, Llb_Grp_t * pGroup, int
     Aig_Obj_t * pObj;
     DdNode * bRes, * bTemp, * bVar;
     int i, iGroupFirst, iGroupLast;
-    int TimeStop;
+    clock_t TimeStop;
     TimeStop = p->dd->TimeStop; p->dd->TimeStop = 0;
     bRes = Cudd_ReadOne( p->dd );   Cudd_Ref( bRes );
     Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vIns, pObj, i )
@@ -205,7 +206,8 @@ DdNode * Llb_ManConstructQuantCubeFwd( Llb_Man_t * p, Llb_Grp_t * pGroup, int iG
 {
     Aig_Obj_t * pObj;
     DdNode * bRes, * bTemp, * bVar;
-    int i, iGroupLast, TimeStop;
+    int i, iGroupLast;
+    clock_t TimeStop;
     TimeStop = p->dd->TimeStop; p->dd->TimeStop = 0;
     bRes = Cudd_ReadOne( p->dd );   Cudd_Ref( bRes );
     Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vIns, pObj, i )
@@ -248,7 +250,8 @@ DdNode * Llb_ManConstructQuantCubeBwd( Llb_Man_t * p, Llb_Grp_t * pGroup, int iG
 {
     Aig_Obj_t * pObj;
     DdNode * bRes, * bTemp, * bVar;
-    int i, iGroupFirst, TimeStop;
+    int i, iGroupFirst;
+    clock_t TimeStop;
     TimeStop = p->dd->TimeStop; p->dd->TimeStop = 0;
     bRes = Cudd_ReadOne( p->dd );   Cudd_Ref( bRes );
     Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vIns, pObj, i )
@@ -295,7 +298,8 @@ DdNode * Llb_ManComputeInitState( Llb_Man_t * p, DdManager * dd )
 {
     Aig_Obj_t * pObj;
     DdNode * bRes, * bVar, * bTemp;
-    int i, iVar, TimeStop;
+    int i, iVar;
+    clock_t TimeStop;
     TimeStop = dd->TimeStop; dd->TimeStop = 0;
     bRes = Cudd_ReadOne( dd );   Cudd_Ref( bRes );
     Saig_ManForEachLo( p->pAig, pObj, i )
@@ -409,7 +413,8 @@ DdNode * Llb_ManCreateConstraints( Llb_Man_t * p, Vec_Int_t * vHints, int fUseNs
 {
     DdNode * bConstr, * bFunc, * bTemp;
     Aig_Obj_t * pObj;
-    int i, Entry, TimeStop;
+    int i, Entry;
+    clock_t TimeStop;
     if ( vHints == NULL )
         return Cudd_ReadOne( p->dd );
     TimeStop = p->dd->TimeStop; p->dd->TimeStop = 0;
@@ -581,11 +586,12 @@ int Llb_ManReachability( Llb_Man_t * p, Vec_Int_t * vHints, DdManager ** pddGlo
     int * pGlo2Cs = Vec_IntArray( p->vGlo2Cs );
     DdNode * bCurrent, * bReached, * bNext, * bTemp, * bCube;
     DdNode * bConstrCs, * bConstrNs;
-    int clk2, clk = clock(), nIters, nBddSize = 0;
+    clock_t clk2, clk = clock();
+    int nIters, nBddSize = 0;
 //    int nThreshold = 10000;
 
     // compute time to stop
-    p->pPars->TimeTarget = p->pPars->TimeLimit ? time(NULL) + p->pPars->TimeLimit : 0;
+    p->pPars->TimeTarget = p->pPars->TimeLimit ? p->pPars->TimeLimit * CLOCKS_PER_SEC + clock(): 0;
 
     // define variable limits
     Llb_ManPrepareVarLimits( p );
@@ -656,7 +662,7 @@ int Llb_ManReachability( Llb_Man_t * p, Vec_Int_t * vHints, DdManager ** pddGlo
     { 
         clk2 = clock();
         // check the runtime limit
-        if ( p->pPars->TimeLimit && time(NULL) > p->pPars->TimeTarget )
+        if ( p->pPars->TimeLimit && clock() > p->pPars->TimeTarget )
         {
             if ( !p->pPars->fSilent )
                 printf( "Reached timeout during image computation (%d seconds).\n",  p->pPars->TimeLimit );
diff --git a/src/proof/llb/llb2Bad.c b/src/proof/llb/llb2Bad.c
index f4359493..57745c1d 100644
--- a/src/proof/llb/llb2Bad.c
+++ b/src/proof/llb/llb2Bad.c
@@ -42,7 +42,7 @@ ABC_NAMESPACE_IMPL_START
   SeeAlso     []
 
 ***********************************************************************/
-DdNode * Llb_BddComputeBad( Aig_Man_t * pInit, DdManager * dd, int TimeOut )
+DdNode * Llb_BddComputeBad( Aig_Man_t * pInit, DdManager * dd, clock_t TimeOut )
 {
     Vec_Ptr_t * vNodes;
     DdNode * bBdd0, * bBdd1, * bTemp, * bResult;
@@ -110,7 +110,8 @@ DdNode * Llb_BddQuantifyPis( Aig_Man_t * pInit, DdManager * dd, DdNode * bFunc )
 {
     DdNode * bVar, * bCube, * bTemp;
     Aig_Obj_t * pObj;
-    int i, TimeStop;
+    int i;
+    clock_t TimeStop;
     assert( Cudd_ReadSize(dd) == Aig_ManCiNum(pInit) );
     TimeStop = dd->TimeStop; dd->TimeStop = 0;
     // create PI cube
diff --git a/src/proof/llb/llb2Core.c b/src/proof/llb/llb2Core.c
index 3b98c32a..f19f757e 100644
--- a/src/proof/llb/llb2Core.c
+++ b/src/proof/llb/llb2Core.c
@@ -68,7 +68,8 @@ struct Llb_Img_t_
 DdNode * Llb_CoreComputeCube( DdManager * dd, Vec_Int_t * vVars, int fUseVarIndex, char * pValues )
 {
     DdNode * bRes, * bVar, * bTemp;
-    int i, iVar, Index, TimeStop;
+    int i, iVar, Index;
+    clock_t TimeStop;
     TimeStop = dd->TimeStop; dd->TimeStop = 0;
     bRes = Cudd_ReadOne( dd );   Cudd_Ref( bRes );
     Vec_IntForEachEntry( vVars, Index, i )
@@ -209,7 +210,8 @@ int Llb_CoreReachability_int( Llb_Img_t * p, Vec_Ptr_t * vQuant0, Vec_Ptr_t * vQ
     int * pLoc2GloR = p->pPars->fBackward? Vec_IntArray( p->vNs2Glo ) : Vec_IntArray( p->vCs2Glo );
     int * pGlo2Loc  = p->pPars->fBackward? Vec_IntArray( p->vGlo2Ns ) : Vec_IntArray( p->vGlo2Cs );
     DdNode * bCurrent, * bReached, * bNext, * bTemp;
-    int clk2, clk = clock(), nIters, nBddSize;//, iOutFail = -1;
+    clock_t clk2, clk = clock();
+    int nIters, nBddSize;//, iOutFail = -1;
 /*
     // compute time to stop
     if ( p->pPars->TimeLimit )
@@ -218,7 +220,7 @@ int Llb_CoreReachability_int( Llb_Img_t * p, Vec_Ptr_t * vQuant0, Vec_Ptr_t * vQ
         p->pPars->TimeTarget = 0;
 */
 
-    if ( time(NULL) > p->pPars->TimeTarget )
+    if ( clock() > p->pPars->TimeTarget )
     {
         if ( !p->pPars->fSilent )
             printf( "Reached timeout (%d seconds) before image computation.\n", p->pPars->TimeLimit );
@@ -286,7 +288,7 @@ int Llb_CoreReachability_int( Llb_Img_t * p, Vec_Ptr_t * vQuant0, Vec_Ptr_t * vQ
     { 
         clk2 = clock();
         // check the runtime limit
-        if ( p->pPars->TimeLimit && time(NULL) > p->pPars->TimeTarget )
+        if ( p->pPars->TimeLimit && clock() > p->pPars->TimeTarget )
         {
             if ( !p->pPars->fSilent )
                 printf( "Reached timeout (%d seconds) during image computation.\n",  p->pPars->TimeLimit );
@@ -529,7 +531,7 @@ int Llb_CoreReachability( Llb_Img_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Ptr_t * Llb_CoreConstructAll( Aig_Man_t * p, Vec_Ptr_t * vResult, Vec_Int_t * vVarsNs, int TimeTarget )
+Vec_Ptr_t * Llb_CoreConstructAll( Aig_Man_t * p, Vec_Ptr_t * vResult, Vec_Int_t * vVarsNs, clock_t TimeTarget )
 {
     DdManager * dd;
     Vec_Ptr_t * vDdMans;
@@ -689,7 +691,7 @@ void Llb_CoreStop( Llb_Img_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-int Llb_CoreExperiment( Aig_Man_t * pInit, Aig_Man_t * pAig, Gia_ParLlb_t * pPars, Vec_Ptr_t * vResult, int TimeTarget )
+int Llb_CoreExperiment( Aig_Man_t * pInit, Aig_Man_t * pAig, Gia_ParLlb_t * pPars, Vec_Ptr_t * vResult, clock_t TimeTarget )
 {
     int RetValue;
     Llb_Img_t * p;
@@ -726,10 +728,10 @@ int Llb_ManReachMinCut( Aig_Man_t * pAig, Gia_ParLlb_t * pPars )
     Vec_Ptr_t * vResult;
     Aig_Man_t * p;
     int RetValue = -1;
-    int clk = clock();
+    clock_t clk = clock();
 
     // compute time to stop
-    pPars->TimeTarget = pPars->TimeLimit ? time(NULL) + pPars->TimeLimit : 0;
+    pPars->TimeTarget = pPars->TimeLimit ? pPars->TimeLimit * CLOCKS_PER_SEC + clock(): 0;
 
     p = Aig_ManDupFlopsOnly( pAig );
 //Aig_ManShow( p, 0, NULL );
@@ -741,7 +743,7 @@ int Llb_ManReachMinCut( Aig_Man_t * pAig, Gia_ParLlb_t * pPars )
 
     vResult = Llb_ManComputeCuts( p, pPars->nPartValue, pPars->fVerbose, pPars->fVeryVerbose );
 
-    if ( pPars->TimeLimit && time(NULL) > pPars->TimeTarget )
+    if ( pPars->TimeLimit && clock() > pPars->TimeTarget )
     {
         if ( !pPars->fSilent )
             printf( "Reached timeout (%d seconds) after partitioning.\n", pPars->TimeLimit );
diff --git a/src/proof/llb/llb2Driver.c b/src/proof/llb/llb2Driver.c
index 4998b1ad..40d7a116 100644
--- a/src/proof/llb/llb2Driver.c
+++ b/src/proof/llb/llb2Driver.c
@@ -129,7 +129,8 @@ DdNode * Llb_DriverPhaseCube( Aig_Man_t * pAig, Vec_Int_t * vDriRefs, DdManager
 {
     DdNode * bCube, * bVar, * bTemp;
     Aig_Obj_t * pObj;
-    int i, TimeStop;
+    int i;
+    clock_t TimeStop;
     TimeStop = dd->TimeStop; dd->TimeStop = 0;
     bCube = Cudd_ReadOne( dd );  Cudd_Ref( bCube );
     Saig_ManForEachLi( pAig, pObj, i )
@@ -159,7 +160,7 @@ DdNode * Llb_DriverPhaseCube( Aig_Man_t * pAig, Vec_Int_t * vDriRefs, DdManager
   SeeAlso     []
 
 ***********************************************************************/
-DdManager * Llb_DriverLastPartition( Aig_Man_t * p, Vec_Int_t * vVarsNs, int TimeTarget )
+DdManager * Llb_DriverLastPartition( Aig_Man_t * p, Vec_Int_t * vVarsNs, clock_t TimeTarget )
 {
 //    int fVerbose = 1;
     DdManager * dd;
diff --git a/src/proof/llb/llb2Flow.c b/src/proof/llb/llb2Flow.c
index 40ca19e5..f82fcf58 100644
--- a/src/proof/llb/llb2Flow.c
+++ b/src/proof/llb/llb2Flow.c
@@ -1226,7 +1226,8 @@ Vec_Ptr_t * Llb_ManComputeCuts( Aig_Man_t * p, int Num, int fVerbose, int fVeryV
 {
     int nVolMax = Aig_ManNodeNum(p) / Num;
     Vec_Ptr_t * vResult, * vMinCut = NULL, * vLower, * vUpper;
-    int i, k, nVol, clk = clock();
+    int i, k, nVol;
+    clock_t clk = clock();
     vResult = Vec_PtrAlloc( 100 );
     Vec_PtrPush( vResult, Llb_ManComputeCutLo(p) );
     Vec_PtrPush( vResult, Llb_ManComputeCutLi(p) );
diff --git a/src/proof/llb/llb2Image.c b/src/proof/llb/llb2Image.c
index 99ffbdc4..cfaef13c 100644
--- a/src/proof/llb/llb2Image.c
+++ b/src/proof/llb/llb2Image.c
@@ -179,7 +179,7 @@ void Llb_ImgSchedule( Vec_Ptr_t * vSupps, Vec_Ptr_t ** pvQuant0, Vec_Ptr_t ** pv
   SeeAlso     []
 
 ***********************************************************************/
-DdManager * Llb_ImgPartition( Aig_Man_t * p, Vec_Ptr_t * vLower, Vec_Ptr_t * vUpper, int TimeTarget )
+DdManager * Llb_ImgPartition( Aig_Man_t * p, Vec_Ptr_t * vLower, Vec_Ptr_t * vUpper, clock_t TimeTarget )
 {
     Vec_Ptr_t * vNodes, * vRange;
     Aig_Obj_t * pObj;
@@ -259,7 +259,8 @@ DdNode * Llb_ImgComputeCube( Aig_Man_t * pAig, Vec_Int_t * vNodeIds, DdManager *
 {
     DdNode * bProd, * bTemp;
     Aig_Obj_t * pObj;
-    int i, TimeStop;
+    int i;
+    clock_t TimeStop;
     TimeStop = dd->TimeStop; dd->TimeStop = 0;
     bProd = Cudd_ReadOne(dd);   Cudd_Ref( bProd );
     Aig_ManForEachObjVec( vNodeIds, pAig, pObj, i )
@@ -287,7 +288,8 @@ void Llb_ImgQuantifyFirst( Aig_Man_t * pAig, Vec_Ptr_t * vDdMans, Vec_Ptr_t * vQ
 {
     DdManager * dd;
     DdNode * bProd, * bRes, * bTemp;
-    int i, clk = clock();
+    int i;
+    clock_t clk = clock();
     Vec_PtrForEachEntry( DdManager *, vDdMans, dd, i )
     {
         // remember unquantified ones
@@ -360,12 +362,13 @@ void Llb_ImgQuantifyReset( Vec_Ptr_t * vDdMans )
 ***********************************************************************/
 DdNode * Llb_ImgComputeImage( Aig_Man_t * pAig, Vec_Ptr_t * vDdMans, DdManager * dd, DdNode * bInit, 
     Vec_Ptr_t * vQuant0, Vec_Ptr_t * vQuant1, Vec_Int_t * vDriRefs, 
-    int TimeTarget, int fBackward, int fReorder, int fVerbose )
+    clock_t TimeTarget, int fBackward, int fReorder, int fVerbose )
 {
 //    int fCheckSupport = 0;
     DdManager * ddPart;
     DdNode * bImage, * bGroup, * bCube, * bTemp;
-    int i, clk, clk0 = clock();
+    int i;
+    clock_t clk, clk0 = clock();
 
     bImage = bInit;  Cudd_Ref( bImage );
     if ( fBackward )
diff --git a/src/proof/llb/llb3Image.c b/src/proof/llb/llb3Image.c
index 708af6d5..dcce8441 100644
--- a/src/proof/llb/llb3Image.c
+++ b/src/proof/llb/llb3Image.c
@@ -79,7 +79,7 @@ static inline Llb_Prt_t * Llb_MgrPart( Llb_Mgr_t * p, int i )  { return p->pPart
     for ( i = 0; (i < Vec_IntSize(pVar->vParts)) && (((pPart) = Llb_MgrPart(p, Vec_IntEntry(pVar->vParts,i))), 1); i++ )
 
 // statistics
-int timeBuild, timeAndEx, timeOther;
+clock_t timeBuild, timeAndEx, timeOther;
 int nSuppMax;
 
 ////////////////////////////////////////////////////////////////////////
@@ -140,7 +140,8 @@ DdNode * Llb_NonlinCreateCube1( Llb_Mgr_t * p, Llb_Prt_t * pPart )
 {
     DdNode * bCube, * bTemp;
     Llb_Var_t * pVar;
-    int i, TimeStop;
+    int i;
+    clock_t TimeStop;
     TimeStop = p->dd->TimeStop; p->dd->TimeStop = 0;
     bCube = Cudd_ReadOne(p->dd);   Cudd_Ref( bCube );
     Llb_PartForEachVar( p, pPart, pVar, i )
@@ -172,7 +173,8 @@ DdNode * Llb_NonlinCreateCube2( Llb_Mgr_t * p, Llb_Prt_t * pPart1, Llb_Prt_t * p
 {
     DdNode * bCube, * bTemp;
     Llb_Var_t * pVar;
-    int i, TimeStop;
+    int i;
+    clock_t TimeStop;
     TimeStop = p->dd->TimeStop; p->dd->TimeStop = 0;
     bCube = Cudd_ReadOne(p->dd);   Cudd_Ref( bCube );
     Llb_PartForEachVar( p, pPart1, pVar, i )
@@ -337,7 +339,7 @@ int Llb_NonlinQuantify1( Llb_Mgr_t * p, Llb_Prt_t * pPart, int fSubset )
   SeeAlso     []
 
 ***********************************************************************/
-int Llb_NonlinQuantify2( Llb_Mgr_t * p, Llb_Prt_t * pPart1, Llb_Prt_t * pPart2, int Limit, int TimeOut )
+int Llb_NonlinQuantify2( Llb_Mgr_t * p, Llb_Prt_t * pPart1, Llb_Prt_t * pPart2 )
 {
     int fVerbose = 0;
     Llb_Var_t * pVar;
@@ -373,7 +375,7 @@ Extra_bddPrintSupport( p->dd, bCube );  printf( "\n" );
             RetValue = Llb_NonlinQuantify1( p, pPart2, 1 );
         if ( RetValue )
             Limit = Limit + 1000;
-        Llb_NonlinQuantify2( p, pPart1, pPart2, Limit, TimeOut );
+        Llb_NonlinQuantify2( p, pPart1, pPart2 );
         return 0;
     }
     Cudd_Ref( bFunc );
@@ -537,7 +539,7 @@ Vec_Ptr_t * Llb_NonlinCutNodes( Aig_Man_t * p, Vec_Ptr_t * vLower, Vec_Ptr_t * v
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Ptr_t * Llb_NonlinBuildBdds( Aig_Man_t * p, Vec_Ptr_t * vLower, Vec_Ptr_t * vUpper, DdManager * dd, int TimeOut )
+Vec_Ptr_t * Llb_NonlinBuildBdds( Aig_Man_t * p, Vec_Ptr_t * vLower, Vec_Ptr_t * vUpper, DdManager * dd )
 {
     Vec_Ptr_t * vNodes, * vResult;
     Aig_Obj_t * pObj;
@@ -655,13 +657,13 @@ void Llb_NonlinAddPartition( Llb_Mgr_t * p, int i, DdNode * bFunc )
   SeeAlso     []
 
 ***********************************************************************/
-int Llb_NonlinStart( Llb_Mgr_t * p, int TimeOut )
+int Llb_NonlinStart( Llb_Mgr_t * p )
 {
     Vec_Ptr_t * vRootBdds;
     DdNode * bFunc;
     int i;
     // create and collect BDDs
-    vRootBdds = Llb_NonlinBuildBdds( p->pAig, p->vLeaves, p->vRoots, p->dd, TimeOut ); // come referenced
+    vRootBdds = Llb_NonlinBuildBdds( p->pAig, p->vLeaves, p->vRoots, p->dd ); // come referenced
     if ( vRootBdds == NULL )
         return 0;
     // add pairs (refs are consumed inside)
@@ -745,7 +747,7 @@ int Llb_NonlinNextPartitions( Llb_Mgr_t * p, Llb_Prt_t ** ppPart1, Llb_Prt_t **
 ***********************************************************************/
 void Llb_NonlinReorder( DdManager * dd, int fTwice, int fVerbose )
 {
-    int clk = clock();
+    clock_t clk = clock();
     if ( fVerbose )
         Abc_Print( 1, "Reordering... Before =%5d. ", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
     Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 );
@@ -880,17 +882,17 @@ void Llb_NonlinFree( Llb_Mgr_t * p )
 
 ***********************************************************************/
 DdNode * Llb_NonlinImage( Aig_Man_t * pAig, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRoots, int * pVars2Q, 
-    DdManager * dd, DdNode * bCurrent, int fReorder, int fVerbose, int * pOrder, int Limit, int TimeOut )
+    DdManager * dd, DdNode * bCurrent, int fReorder, int fVerbose, int * pOrder )
 {
     Llb_Prt_t * pPart, * pPart1, * pPart2;
     Llb_Mgr_t * p;
     DdNode * bFunc, * bTemp;
     int i, nReorders, timeInside;
-    int clk = clock(), clk2;
+    clock_t clk = clock(), clk2;
     // start the manager
     clk2 = clock();
     p = Llb_NonlinAlloc( pAig, vLeaves, vRoots, pVars2Q, dd );
-    if ( !Llb_NonlinStart( p, TimeOut ) )
+    if ( !Llb_NonlinStart( p ) )
     {
         Llb_NonlinFree( p );
         return NULL;
@@ -913,7 +915,7 @@ DdNode * Llb_NonlinImage( Aig_Man_t * pAig, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRo
     {
         clk2 = clock();
         nReorders = Cudd_ReadReorderings(dd);
-        if ( !Llb_NonlinQuantify2( p, pPart1, pPart2, Limit, TimeOut ) )
+        if ( !Llb_NonlinQuantify2( p, pPart1, pPart2 ) )
         {
             Llb_NonlinFree( p );
             return NULL;
@@ -958,10 +960,10 @@ static Llb_Mgr_t * p = NULL;
   SeeAlso     []
 
 ***********************************************************************/
-DdManager * Llb_NonlinImageStart( Aig_Man_t * pAig, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRoots, int * pVars2Q, int * pOrder, int fFirst, int TimeTarget )
+DdManager * Llb_NonlinImageStart( Aig_Man_t * pAig, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRoots, int * pVars2Q, int * pOrder, int fFirst, clock_t TimeTarget )
 {
     DdManager * dd;
-    int clk = clock();
+    clock_t clk = clock();
     assert( p == NULL );
     // start a new manager (disable reordering)
     dd = Cudd_Init( Aig_ManObjNumMax(pAig), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
@@ -971,7 +973,7 @@ DdManager * Llb_NonlinImageStart( Aig_Man_t * pAig, Vec_Ptr_t * vLeaves, Vec_Ptr
         Cudd_AutodynEnable( dd,  CUDD_REORDER_SYMM_SIFT );
     // start the manager
     p = Llb_NonlinAlloc( pAig, vLeaves, vRoots, pVars2Q, dd );
-    if ( !Llb_NonlinStart( p, 0 ) )
+    if ( !Llb_NonlinStart( p ) )
     {
         Llb_NonlinFree( p );
         p = NULL;
@@ -999,7 +1001,7 @@ DdNode * Llb_NonlinImageCompute( DdNode * bCurrent, int fReorder, int fDrop, int
     Llb_Prt_t * pPart, * pPart1, * pPart2;
     DdNode * bFunc, * bTemp;
     int i, nReorders, timeInside = 0;
-    int clk = clock(), clk2;
+    clock_t clk = clock(), clk2;
 
     // add partition
     Llb_NonlinAddPartition( p, p->iPartFree++, bCurrent );
@@ -1020,7 +1022,7 @@ DdNode * Llb_NonlinImageCompute( DdNode * bCurrent, int fReorder, int fDrop, int
     {
         clk2 = clock();
         nReorders = Cudd_ReadReorderings(p->dd);
-        if ( !Llb_NonlinQuantify2( p, pPart1, pPart2, 0, 0 ) )
+        if ( !Llb_NonlinQuantify2( p, pPart1, pPart2 ) )
         {
             Llb_NonlinFree( p );
             return NULL;
diff --git a/src/proof/llb/llb3Nonlin.c b/src/proof/llb/llb3Nonlin.c
index 38d9b8ae..48724136 100644
--- a/src/proof/llb/llb3Nonlin.c
+++ b/src/proof/llb/llb3Nonlin.c
@@ -54,14 +54,14 @@ struct Llb_Mnn_t_
     int             ddLocReos;
     int             ddLocGrbs;
 
-    int             timeImage;
-    int             timeTran1;
-    int             timeTran2;
-    int             timeGloba;
-    int             timeOther;
-    int             timeTotal;
-    int             timeReo;
-    int             timeReoG;
+    clock_t         timeImage;
+    clock_t         timeTran1;
+    clock_t         timeTran2;
+    clock_t         timeGloba;
+    clock_t         timeOther;
+    clock_t         timeTotal;
+    clock_t         timeReo;
+    clock_t         timeReoG;
 
 };
 
@@ -90,7 +90,7 @@ int Llb_NonlinFindBestVar( DdManager * dd, DdNode * bFunc, Aig_Man_t * pAig )
     DdNode * bCof, * bVar;
     int i, iVar, iVarBest = -1, iValue, iValueBest = ABC_INFINITY, Size0Best = -1;
     int Size, Size0, Size1;
-    int clk = clock();
+    clock_t clk = clock();
     Size = Cudd_DagSize(bFunc);
 //    printf( "Original = %6d.  SuppSize = %3d. Vars = %3d.\n", 
 //        Size = Cudd_DagSize(bFunc), Cudd_SupportSize(dd, bFunc), Aig_ManRegNum(pAig) );
@@ -215,7 +215,8 @@ DdNode * Llb_NonlinComputeInitState( Aig_Man_t * pAig, DdManager * dd )
 {
     Aig_Obj_t * pObj;
     DdNode * bRes, * bVar, * bTemp;
-    int i, iVar, TimeStop;
+    int i, iVar;
+    clock_t TimeStop;
     TimeStop = dd->TimeStop;  dd->TimeStop = 0;
     bRes = Cudd_ReadOne( dd );   Cudd_Ref( bRes );
     Saig_ManForEachLo( pAig, pObj, i )
@@ -302,7 +303,7 @@ Abc_Cex_t * Llb_NonlinDeriveCex( Llb_Mnn_t * p )
 //Extra_bddPrintSupport( p->dd, bRing );   printf( "\n" );
         // compute the next states
         bImage = Llb_NonlinImage( p->pAig, p->vLeaves, p->vRoots, p->pVars2Q, p->dd, bState, 
-            p->pPars->fReorder, p->pPars->fVeryVerbose, NULL, ABC_INFINITY, ABC_INFINITY ); // consumed reference
+            p->pPars->fReorder, p->pPars->fVeryVerbose, NULL ); // consumed reference
         assert( bImage != NULL );
         Cudd_Ref( bImage );
 //Extra_bddPrintSupport( p->dd, bImage );  printf( "\n" );
@@ -429,11 +430,11 @@ int Llb_NonlinReachability( Llb_Mnn_t * p )
 { 
     DdNode * bTemp, * bNext;
     int nIters, nBddSize0, nBddSize = -1, NumCmp;//, Limit = p->pPars->nBddMax;
-    int clk2, clk3, clk = clock();
+    clock_t clk2, clk3, clk = clock();
     assert( Aig_ManRegNum(p->pAig) > 0 );
 
     // compute time to stop
-    p->pPars->TimeTarget = p->pPars->TimeLimit ? time(NULL) + p->pPars->TimeLimit : 0;
+    p->pPars->TimeTarget = p->pPars->TimeLimit ? p->pPars->TimeLimit * CLOCKS_PER_SEC + clock(): 0;
 
     // set the stop time parameter
     p->dd->TimeStop  = p->pPars->TimeTarget;
@@ -472,7 +473,7 @@ int Llb_NonlinReachability( Llb_Mnn_t * p )
     { 
         // check the runtime limit
         clk2 = clock();
-        if ( p->pPars->TimeLimit && time(NULL) > p->pPars->TimeTarget )
+        if ( p->pPars->TimeLimit && clock() > p->pPars->TimeTarget )
         {
             if ( !p->pPars->fSilent )
                 printf( "Reached timeout (%d seconds) during image computation.\n",  p->pPars->TimeLimit );
@@ -807,7 +808,7 @@ void Llb_NonlinExperiment( Aig_Man_t * pAig, int Num )
     Llb_Mnn_t * pMnn;
     Gia_ParLlb_t Pars, * pPars = &Pars;
     Aig_Man_t * p;
-    int clk = clock();
+    clock_t clk = clock();
 
     Llb_ManSetDefaultParams( pPars );
     pPars->fVerbose = 1;
@@ -851,7 +852,7 @@ int Llb_NonlinCoreReach( Aig_Man_t * pAig, Gia_ParLlb_t * pPars )
 
     if ( !pPars->fSkipReach )
     {
-        int clk = clock();
+        clock_t clk = clock();
         pMnn = Llb_MnnStart( pAig, p, pPars );
         RetValue = Llb_NonlinReachability( pMnn );
         pMnn->timeTotal = clock() - clk;
diff --git a/src/proof/llb/llb4Image.c b/src/proof/llb/llb4Image.c
index 039be164..4ae087b5 100644
--- a/src/proof/llb/llb4Image.c
+++ b/src/proof/llb/llb4Image.c
@@ -77,7 +77,7 @@ static inline Llb_Prt_t * Llb_MgrPart( Llb_Mgr_t * p, int i )  { return p->pPart
     for ( i = 0; (i < Vec_IntSize(pVar->vParts)) && (((pPart) = Llb_MgrPart(p, Vec_IntEntry(pVar->vParts,i))), 1); i++ )
 
 // statistics
-//int timeBuild, timeAndEx, timeOther;
+//clock_t timeBuild, timeAndEx, timeOther;
 //int nSuppMax;
 
 ////////////////////////////////////////////////////////////////////////
@@ -139,7 +139,8 @@ DdNode * Llb_Nonlin4CreateCube1( Llb_Mgr_t * p, Llb_Prt_t * pPart )
 {
     DdNode * bCube, * bTemp;
     Llb_Var_t * pVar;
-    int i, TimeStop;
+    int i;
+    clock_t TimeStop;
     TimeStop = p->dd->TimeStop; p->dd->TimeStop = 0;
     bCube = Cudd_ReadOne(p->dd);   Cudd_Ref( bCube );
     Llb_PartForEachVar( p, pPart, pVar, i )
@@ -171,7 +172,8 @@ DdNode * Llb_Nonlin4CreateCube2( Llb_Mgr_t * p, Llb_Prt_t * pPart1, Llb_Prt_t *
 {
     DdNode * bCube, * bTemp;
     Llb_Var_t * pVar;
-    int i, TimeStop;
+    int i;
+    clock_t TimeStop;
     TimeStop = p->dd->TimeStop; p->dd->TimeStop = 0;
     bCube = Cudd_ReadOne(p->dd);   Cudd_Ref( bCube );
     Llb_PartForEachVar( p, pPart1, pVar, i )
diff --git a/src/proof/llb/llb4Nonlin.c b/src/proof/llb/llb4Nonlin.c
index af8dad75..f2973922 100644
--- a/src/proof/llb/llb4Nonlin.c
+++ b/src/proof/llb/llb4Nonlin.c
@@ -47,11 +47,11 @@ struct Llb_Mnx_t_
     Vec_Int_t *     vOrder;         // for each object ID, its BDD variable number or -1
     Vec_Int_t *     vVars2Q;        // 1 if variable is quantifiable; 0 othervise
 
-    int             timeImage;
-    int             timeRemap;
-    int             timeReo;
-    int             timeOther;
-    int             timeTotal;
+    clock_t         timeImage;
+    clock_t         timeRemap;
+    clock_t         timeReo;
+    clock_t         timeOther;
+    clock_t         timeTotal;
 };
 
 //extern int timeBuild, timeAndEx, timeOther;
@@ -446,7 +446,8 @@ DdNode * Llb_Nonlin4ComputeInitState( DdManager * dd, Aig_Man_t * pAig, Vec_Int_
 {
     Aig_Obj_t * pObjLi, * pObjLo;
     DdNode * bRes, * bVar, * bTemp;
-    int i, TimeStop;
+    int i;
+    clock_t TimeStop;
     TimeStop = dd->TimeStop;  dd->TimeStop = 0;
     bRes = Cudd_ReadOne( dd );   Cudd_Ref( bRes );
     Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i )
@@ -475,7 +476,8 @@ DdNode * Llb_Nonlin4ComputeCube( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * v
 {
     Aig_Obj_t * pObjLo, * pObjLi, * pObjTemp;
     DdNode * bRes, * bVar, * bTemp;
-    int i, TimeStop;
+    int i;
+    clock_t TimeStop;
     TimeStop = dd->TimeStop;  dd->TimeStop = 0;
     bRes = Cudd_ReadOne( dd );   Cudd_Ref( bRes );
     Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i )
@@ -667,7 +669,7 @@ int Llb_Nonlin4Reachability( Llb_Mnx_t * p )
 { 
     DdNode * bAux;
     int nIters, nBddSizeFr = 0, nBddSizeTo = 0, nBddSizeTo2 = 0;
-    int clkTemp, clkIter, clk = clock();
+    clock_t clkTemp, clkIter, clk = clock();
     assert( Aig_ManRegNum(p->pAig) > 0 );
 
     if ( p->pPars->fBackward )
@@ -736,7 +738,7 @@ int Llb_Nonlin4Reachability( Llb_Mnx_t * p )
     { 
         clkIter = clock();
         // check the runtime limit
-        if ( p->pPars->TimeLimit && time(NULL) > p->pPars->TimeTarget )
+        if ( p->pPars->TimeLimit && clock() > p->pPars->TimeTarget )
         {
             if ( !p->pPars->fSilent )
                 printf( "Reached timeout (%d seconds) during image computation.\n",  p->pPars->TimeLimit );
@@ -904,7 +906,7 @@ printf( "Before = %d.  After = %d.\n", Cudd_DagSize(bAux), Cudd_DagSize(p->bCurr
 ***********************************************************************/
 void Llb_Nonlin4Reorder( DdManager * dd, int fTwice, int fVerbose )
 {
-    int clk = clock();
+    clock_t clk = clock();
     if ( fVerbose )
         Abc_Print( 1, "Reordering... Before =%5d. ", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
     Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 );
@@ -940,7 +942,7 @@ Llb_Mnx_t * Llb_MnxStart( Aig_Man_t * pAig, Gia_ParLlb_t * pPars )
     p->pPars   = pPars;
 
     // compute time to stop
-    p->pPars->TimeTarget = p->pPars->TimeLimit ? time(NULL) + p->pPars->TimeLimit : 0;
+    p->pPars->TimeTarget = p->pPars->TimeLimit ? p->pPars->TimeLimit * CLOCKS_PER_SEC + clock(): 0;
 
     if ( pPars->fCluster )
     {
@@ -1071,7 +1073,7 @@ int Llb_Nonlin4CoreReach( Aig_Man_t * pAig, Gia_ParLlb_t * pPars )
         return RetValue;
     }
     {
-        int clk = clock();
+        clock_t clk = clock();
         pMnn = Llb_MnxStart( pAig, pPars );
 //Llb_MnxCheckNextStateVars( pMnn );
         if ( !pPars->fSkipReach )
diff --git a/src/proof/llb/llb4Sweep.c b/src/proof/llb/llb4Sweep.c
index 6b223ab9..709bd61a 100644
--- a/src/proof/llb/llb4Sweep.c
+++ b/src/proof/llb/llb4Sweep.c
@@ -286,7 +286,8 @@ DdNode * Llb4_Nonlin4SweepBadMonitor( Aig_Man_t * pAig, Vec_Int_t * vOrder, DdMa
 {
     Aig_Obj_t * pObj;
     DdNode * bRes, * bVar, * bTemp;
-    int i, TimeStop;
+    int i;
+    clock_t TimeStop;
     TimeStop = dd->TimeStop;  dd->TimeStop = 0;
     bRes = Cudd_ReadOne( dd );   Cudd_Ref( bRes );
     Saig_ManForEachPo( pAig, pObj, i )
diff --git a/src/proof/llb/llbInt.h b/src/proof/llb/llbInt.h
index d81aadcf..58e2b543 100644
--- a/src/proof/llb/llbInt.h
+++ b/src/proof/llb/llbInt.h
@@ -152,34 +152,34 @@ extern int             Llb_ManReachability( Llb_Man_t * p, Vec_Int_t * vHints, D
 extern void            Llb_MtrSchedule( Llb_Mtr_t * p );
 
 /*=== llb2Bad.c ======================================================*/
-extern DdNode *        Llb_BddComputeBad( Aig_Man_t * pInit, DdManager * dd, int TimeOut );
+extern DdNode *        Llb_BddComputeBad( Aig_Man_t * pInit, DdManager * dd, clock_t TimeOut );
 extern DdNode *        Llb_BddQuantifyPis( Aig_Man_t * pInit, DdManager * dd, DdNode * bFunc );
 /*=== llb2Core.c ======================================================*/
 extern DdNode *        Llb_CoreComputeCube( DdManager * dd, Vec_Int_t * vVars, int fUseVarIndex, char * pValues );
-extern int             Llb_CoreExperiment( Aig_Man_t * pInit, Aig_Man_t * pAig, Gia_ParLlb_t * pPars, Vec_Ptr_t * vResult, int TimeTarget ); 
+extern int             Llb_CoreExperiment( Aig_Man_t * pInit, Aig_Man_t * pAig, Gia_ParLlb_t * pPars, Vec_Ptr_t * vResult, clock_t TimeTarget ); 
 /*=== llb2Driver.c ======================================================*/
 extern Vec_Int_t *     Llb_DriverCountRefs( Aig_Man_t * p );
 extern Vec_Int_t *     Llb_DriverCollectNs( Aig_Man_t * pAig, Vec_Int_t * vDriRefs );
 extern Vec_Int_t *     Llb_DriverCollectCs( Aig_Man_t * pAig );
 extern DdNode *        Llb_DriverPhaseCube( Aig_Man_t * pAig, Vec_Int_t * vDriRefs, DdManager * dd );
-extern DdManager *     Llb_DriverLastPartition( Aig_Man_t * p, Vec_Int_t * vVarsNs, int TimeTarget );
+extern DdManager *     Llb_DriverLastPartition( Aig_Man_t * p, Vec_Int_t * vVarsNs, clock_t TimeTarget );
 /*=== llb2Image.c ======================================================*/
 extern Vec_Ptr_t *     Llb_ImgSupports( Aig_Man_t * p, Vec_Ptr_t * vDdMans, Vec_Int_t * vStart, Vec_Int_t * vStop, int fAddPis, int fVerbose );
 extern void            Llb_ImgSchedule( Vec_Ptr_t * vSupps, Vec_Ptr_t ** pvQuant0, Vec_Ptr_t ** pvQuant1, int fVerbose );
-extern DdManager *     Llb_ImgPartition( Aig_Man_t * p, Vec_Ptr_t * vLower, Vec_Ptr_t * vUpper, int TimeTarget );
+extern DdManager *     Llb_ImgPartition( Aig_Man_t * p, Vec_Ptr_t * vLower, Vec_Ptr_t * vUpper, clock_t TimeTarget );
 extern void            Llb_ImgQuantifyFirst( Aig_Man_t * pAig, Vec_Ptr_t * vDdMans, Vec_Ptr_t * vQuant0, int fVerbose );
 extern void            Llb_ImgQuantifyReset( Vec_Ptr_t * vDdMans );
 extern DdNode *        Llb_ImgComputeImage( Aig_Man_t * pAig, Vec_Ptr_t * vDdMans, DdManager * dd, DdNode * bInit, 
                            Vec_Ptr_t * vQuant0, Vec_Ptr_t * vQuant1, Vec_Int_t * vDriRefs, 
-                           int TimeTarget, int fBackward, int fReorder, int fVerbose );
+                           clock_t TimeTarget, int fBackward, int fReorder, int fVerbose );
 
-extern DdManager *     Llb_NonlinImageStart( Aig_Man_t * pAig, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRoots, int * pVars2Q, int * pOrder, int fFirst, int TimeTarget );
+extern DdManager *     Llb_NonlinImageStart( Aig_Man_t * pAig, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRoots, int * pVars2Q, int * pOrder, int fFirst, clock_t TimeTarget );
 extern DdNode *        Llb_NonlinImageCompute( DdNode * bCurrent, int fReorder, int fDrop, int fVerbose, int * pOrder );
 extern void            Llb_NonlinImageQuit();
 
 /*=== llb3Image.c =======================================================*/
 extern DdNode *        Llb_NonlinImage( Aig_Man_t * pAig, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRoots, int * pVars2Q, 
-                           DdManager * dd, DdNode * bCurrent, int fReorder, int fVerbose, int * pOrder, int Limit, int TimeTarget );
+                           DdManager * dd, DdNode * bCurrent, int fReorder, int fVerbose, int * pOrder );
 /*=== llb3Nonlin.c ======================================================*/
 extern DdNode *        Llb_NonlinComputeInitState( Aig_Man_t * pAig, DdManager * dd );
 
diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c
index 9cecbd78..765894e3 100644
--- a/src/proof/pdr/pdrCore.c
+++ b/src/proof/pdr/pdrCore.c
@@ -418,7 +418,8 @@ int Pdr_ManBlockCube( Pdr_Man_t * p, Pdr_Set_t * pCube )
     Pdr_Obl_t * pThis;
     Pdr_Set_t * pPred, * pCubeMin;
     int i, k, RetValue, Prio = ABC_INFINITY, Counter = 0;
-    int kMax = Vec_PtrSize(p->vSolvers)-1, clk;
+    int kMax = Vec_PtrSize(p->vSolvers)-1;
+    clock_t clk;
     p->nBlocks++;
     // create first proof obligation
     assert( p->pQueue == NULL );
@@ -528,7 +529,7 @@ int Pdr_ManBlockCube( Pdr_Man_t * p, Pdr_Set_t * pCube )
         }
 
         // check the timeout
-        if ( p->timeToStop && time(NULL) > p->timeToStop )
+        if ( p->timeToStop && clock() > p->timeToStop )
             return -1;
     }
     return 1;
@@ -551,7 +552,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
     Pdr_Set_t * pCube;
     int k, RetValue = -1;
     clock_t clkStart = clock();
-    p->timeToStop = p->pPars->nTimeOut ? time(NULL) + p->pPars->nTimeOut : 0;
+    p->timeToStop = p->pPars->nTimeOut ? p->pPars->nTimeOut * CLOCKS_PER_SEC + clock(): 0;
     assert( Vec_PtrSize(p->vSolvers) == 0 );
     // create the first timeframe
     Pdr_ManCreateSolver( p, (k = 0) );
@@ -633,7 +634,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
         }
 
         // check the timeout
-        if ( p->timeToStop && time(NULL) > p->timeToStop )
+        if ( p->timeToStop && clock() > p->timeToStop )
         {
             if ( fPrintClauses )
             {
diff --git a/src/proof/ssw/sswBmc.c b/src/proof/ssw/sswBmc.c
index ff428fa1..4fa9c07a 100644
--- a/src/proof/ssw/sswBmc.c
+++ b/src/proof/ssw/sswBmc.c
@@ -128,7 +128,8 @@ int Ssw_BmcDynamic( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int fVerbo
     Ssw_Frm_t * pFrm;
     Ssw_Sat_t * pSat;
     Aig_Obj_t * pObj, * pObjFrame;
-    int status, clkPart, Lit, i, f, RetValue;
+    int status, Lit, i, f, RetValue;
+    clock_t clkPart;
 
     // start managers
     assert( Saig_ManRegNum(pAig) > 0 );
diff --git a/src/proof/ssw/sswClass.c b/src/proof/ssw/sswClass.c
index 581b8aed..28c4947a 100644
--- a/src/proof/ssw/sswClass.c
+++ b/src/proof/ssw/sswClass.c
@@ -610,7 +610,8 @@ Ssw_Cla_t * Ssw_ClassesPrepare( Aig_Man_t * pAig, int nFramesK, int fLatchCorr,
     Ssw_Sml_t * pSml;
     Vec_Ptr_t * vCands;
     Aig_Obj_t * pObj;
-    int i, k, RetValue, clk;
+    int i, k, RetValue;
+    clock_t clk;
 
     // start the classes
     p = Ssw_ClassesStart( pAig );
diff --git a/src/proof/ssw/sswConstr.c b/src/proof/ssw/sswConstr.c
index 82977edb..5459aa72 100644
--- a/src/proof/ssw/sswConstr.c
+++ b/src/proof/ssw/sswConstr.c
@@ -408,7 +408,8 @@ int Ssw_ManSweepBmcConstr_old( Ssw_Man_t * p )
 {
     Bar_Progress_t * pProgress = NULL;
     Aig_Obj_t * pObj, * pObjNew, * pObjLi, * pObjLo;
-    int i, f, iLits, clk;
+    int i, f, iLits;
+    clock_t clk;
 clk = clock();
 
     // start initialized timeframes
@@ -497,7 +498,8 @@ p->timeBmc += clock() - clk;
 int Ssw_ManSweepBmcConstr( Ssw_Man_t * p )
 {
     Aig_Obj_t * pObj, * pObjNew, * pObjLi, * pObjLo;
-    int i, f, iLits, clk;
+    int i, f, iLits;
+    clock_t clk;
 clk = clock();
 
     // start initialized timeframes
@@ -618,7 +620,8 @@ int Ssw_ManSweepConstr( Ssw_Man_t * p )
 { 
     Bar_Progress_t * pProgress = NULL;
     Aig_Obj_t * pObj, * pObj2, * pObjNew;
-    int nConstrPairs, clk, i, f, iLits;
+    int nConstrPairs, i, f, iLits;
+    clock_t clk;
 //Ssw_ManPrintPolarity( p->pAig );
 
     // perform speculative reduction
diff --git a/src/proof/ssw/sswCore.c b/src/proof/ssw/sswCore.c
index c51d421c..b27e7eaf 100644
--- a/src/proof/ssw/sswCore.c
+++ b/src/proof/ssw/sswCore.c
@@ -236,7 +236,7 @@ Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p )
     int nSatProof, nSatCallsSat, nRecycles, nSatFailsReal, nUniques;
     Aig_Man_t * pAigNew;
     int RetValue, nIter = -1;
-    int clk, clkTotal = clock();
+    clock_t clk, clkTotal = clock();
     // get the starting stats
     p->nLitsBeg  = Ssw_ClassesLitNum( p->ppClasses );
     p->nNodesBeg = Aig_ManNodeNum(p->pAig);
diff --git a/src/proof/ssw/sswDyn.c b/src/proof/ssw/sswDyn.c
index 617bb40f..760f457a 100644
--- a/src/proof/ssw/sswDyn.c
+++ b/src/proof/ssw/sswDyn.c
@@ -262,7 +262,8 @@ void Ssw_ManSweepTransferDyn( Ssw_Man_t * p )
 ***********************************************************************/
 int Ssw_ManSweepResimulateDyn( Ssw_Man_t * p, int f )
 {
-    int RetValue1, RetValue2, clk = clock();
+    int RetValue1, RetValue2;
+    clock_t clk = clock();
     // transfer PI simulation information from storage
 //    Ssw_SmlAssignDist1Plus( p->pSml, p->pPatWords );
     Ssw_ManSweepTransferDyn( p );
@@ -294,7 +295,8 @@ p->timeSimSat += clock() - clk;
 int Ssw_ManSweepResimulateDynLocal( Ssw_Man_t * p, int f )
 {
     Aig_Obj_t * pObj, * pRepr, ** ppClass;
-    int i, k, nSize, RetValue1, RetValue2, clk = clock();
+    int i, k, nSize, RetValue1, RetValue2;
+    clock_t clk = clock();
     p->nSimRounds++;
     // transfer PI simulation information from storage
 //    Ssw_SmlAssignDist1Plus( p->pSml, p->pPatWords );
@@ -372,7 +374,8 @@ int Ssw_ManSweepDyn( Ssw_Man_t * p )
 { 
     Bar_Progress_t * pProgress = NULL;
     Aig_Obj_t * pObj, * pObjNew;
-    int clk, i, f;
+    int i, f;
+    clock_t clk;
 
     // perform speculative reduction
 clk = clock();
diff --git a/src/proof/ssw/sswFilter.c b/src/proof/ssw/sswFilter.c
index 5f467123..3fff79bb 100644
--- a/src/proof/ssw/sswFilter.c
+++ b/src/proof/ssw/sswFilter.c
@@ -278,7 +278,8 @@ Aig_Obj_t * Ssw_ManSweepBmcFilter_rec( Ssw_Man_t * p, Aig_Obj_t * pObj, int f )
 int Ssw_ManSweepBmcFilter( Ssw_Man_t * p, int TimeLimit )
 {
     Aig_Obj_t * pObj, * pObjNew, * pObjLi, * pObjLo;
-    int f, f1, i, clkTotal = clock();
+    int f, f1, i;
+    clock_t clkTotal = clock();
     // start initialized timeframes
     p->pFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * p->pPars->nFramesK );
     Saig_ManForEachLo( p->pAig, pObj, i )
@@ -383,7 +384,7 @@ void Ssw_SignalFilter( Aig_Man_t * pAig, int nFramesMax, int nConfMax, int nRoun
     Ssw_Pars_t Pars, * pPars = &Pars;
     Ssw_Man_t * p;
     int r, TimeLimitPart;//, clkTotal = clock();
-    int nTimeToStop = TimeLimit ? TimeLimit + time(NULL) : 0;
+    clock_t nTimeToStop = TimeLimit ? TimeLimit * CLOCKS_PER_SEC + clock(): 0;
     assert( Aig_ManRegNum(pAig) > 0 );
     assert( Aig_ManConstrNum(pAig) == 0 );
     // consider the case of empty AIG
@@ -429,7 +430,7 @@ void Ssw_SignalFilter( Aig_Man_t * pAig, int nFramesMax, int nConfMax, int nRoun
             Ssw_ClassesPrint( p->ppClasses, 0 );
         }
         p->pMSat = Ssw_SatStart( 0 );
-        TimeLimitPart = TimeLimit ? nTimeToStop - time(NULL) : 0;
+        TimeLimitPart = TimeLimit ? (nTimeToStop - clock()) / CLOCKS_PER_SEC : 0;
         if ( TimeLimit2 )
         {
             if ( TimeLimitPart )
@@ -444,7 +445,7 @@ void Ssw_SignalFilter( Aig_Man_t * pAig, int nFramesMax, int nConfMax, int nRoun
         // simulate pattern forward
         Ssw_ManRollForward( p, p->pPars->nFramesK );
         // check timeout
-        if ( TimeLimit && time(NULL) > nTimeToStop )
+        if ( TimeLimit && clock() > nTimeToStop )
         {
             printf( "Reached timeout (%d seconds).\n",  TimeLimit );
             break;
diff --git a/src/proof/ssw/sswInt.h b/src/proof/ssw/sswInt.h
index acd273fd..8749cec1 100644
--- a/src/proof/ssw/sswInt.h
+++ b/src/proof/ssw/sswInt.h
@@ -127,16 +127,16 @@ struct Ssw_Man_t_
     int              nRegsBegC;
     int              nRegsEndC;
     // runtime stats
-    int              timeBmc;        // bounded model checking
-    int              timeReduce;     // speculative reduction
-    int              timeMarkCones;  // marking the cones not to be refined
-    int              timeSimSat;     // simulation of the counter-examples
-    int              timeSat;        // solving SAT
-    int              timeSatSat;     // sat
-    int              timeSatUnsat;   // unsat
-    int              timeSatUndec;   // undecided
-    int              timeOther;      // other runtime
-    int              timeTotal;      // total runtime
+    clock_t          timeBmc;        // bounded model checking
+    clock_t          timeReduce;     // speculative reduction
+    clock_t          timeMarkCones;  // marking the cones not to be refined
+    clock_t          timeSimSat;     // simulation of the counter-examples
+    clock_t          timeSat;        // solving SAT
+    clock_t          timeSatSat;     // sat
+    clock_t          timeSatUnsat;   // unsat
+    clock_t          timeSatUndec;   // undecided
+    clock_t          timeOther;      // other runtime
+    clock_t          timeTotal;      // total runtime
 };
 
 // internal SAT manager
diff --git a/src/proof/ssw/sswIslands.c b/src/proof/ssw/sswIslands.c
index 8f54432d..97e9cf54 100644
--- a/src/proof/ssw/sswIslands.c
+++ b/src/proof/ssw/sswIslands.c
@@ -479,7 +479,8 @@ int Ssw_SecWithSimilarityPairs( Aig_Man_t * p0, Aig_Man_t * p1, Vec_Int_t * vPai
 {
     Ssw_Pars_t Pars;
     Aig_Man_t * pAigRes;
-    int RetValue, clk = clock();
+    int RetValue;
+    clock_t clk = clock();
     // derive parameters if not given
     if ( pPars == NULL )
         Ssw_ManSetDefaultParams( pPars = &Pars );
diff --git a/src/proof/ssw/sswLcorr.c b/src/proof/ssw/sswLcorr.c
index 71f148e3..e58e9b50 100644
--- a/src/proof/ssw/sswLcorr.c
+++ b/src/proof/ssw/sswLcorr.c
@@ -77,7 +77,8 @@ void Ssw_ManSweepTransfer( Ssw_Man_t * p )
 ***********************************************************************/
 int Ssw_ManSweepResimulate( Ssw_Man_t * p )
 {
-    int RetValue1, RetValue2, clk = clock();
+    int RetValue1, RetValue2;
+    clock_t clk = clock();
     // transfer PI simulation information from storage
     Ssw_ManSweepTransfer( p );
     // simulate internal nodes
@@ -159,7 +160,8 @@ void Ssw_ManBuildCone_rec( Ssw_Man_t * p, Aig_Obj_t * pObj )
 void Ssw_ManSweepLatchOne( Ssw_Man_t * p, Aig_Obj_t * pObjRepr, Aig_Obj_t * pObj )
 {
     Aig_Obj_t * pObjFraig, * pObjReprFraig, * pObjLi;
-    int RetValue, clk;
+    int RetValue;
+    clock_t clk;
     assert( Aig_ObjIsCi(pObj) );
     assert( Aig_ObjIsCi(pObjRepr) || Aig_ObjIsConst1(pObjRepr) );
     // check if it makes sense to skip some calls
diff --git a/src/proof/ssw/sswPairs.c b/src/proof/ssw/sswPairs.c
index e356aa60..e4228685 100644
--- a/src/proof/ssw/sswPairs.c
+++ b/src/proof/ssw/sswPairs.c
@@ -320,7 +320,8 @@ Aig_Man_t * Ssw_SignalCorrespondeceTestPairs( Aig_Man_t * pAig )
     Ssw_Pars_t Pars, * pPars = &Pars;
     Vec_Int_t * vIds1, * vIds2;
     Aig_Obj_t * pObj, * pRepr;
-    int RetValue, i, clk = clock();
+    int RetValue, i;
+    clock_t clk = clock();
     Ssw_ManSetDefaultParams( pPars );
     pPars->fVerbose = 1;
     pAigNew = Ssw_SignalCorrespondence( pAig, pPars );
@@ -379,7 +380,8 @@ Aig_Man_t * Ssw_SignalCorrespondeceTestPairs( Aig_Man_t * pAig )
 int Ssw_SecWithPairs( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Vec_Int_t * vIds1, Vec_Int_t * vIds2, Ssw_Pars_t * pPars )
 {
     Aig_Man_t * pAigRes;
-    int RetValue, clk = clock();
+    int RetValue;
+    clock_t clk = clock();
     assert( vIds1 != NULL && vIds2 != NULL );
     // try the new AIGs
     printf( "Performing specialized verification with node pairs.\n" );
@@ -413,7 +415,8 @@ int Ssw_SecWithPairs( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Vec_Int_t * vIds1, V
 int Ssw_SecGeneral( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Ssw_Pars_t * pPars )
 {
     Aig_Man_t * pAigRes, * pMiter;
-    int RetValue, clk = clock();
+    int RetValue;
+    clock_t clk = clock();
     // try the new AIGs
     printf( "Performing general verification without node pairs.\n" );
     pMiter = Saig_ManCreateMiter( pAig1, pAig2, 0 );
@@ -449,7 +452,8 @@ int Ssw_SecGeneral( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Ssw_Pars_t * pPars )
 int Ssw_SecGeneralMiter( Aig_Man_t * pMiter, Ssw_Pars_t * pPars )
 {
     Aig_Man_t * pAigRes;
-    int RetValue, clk = clock();
+    int RetValue;
+    clock_t clk = clock();
     // try the new AIGs
 //    printf( "Performing general verification without node pairs.\n" );
     pAigRes = Ssw_SignalCorrespondence( pMiter, pPars );
diff --git a/src/proof/ssw/sswPart.c b/src/proof/ssw/sswPart.c
index 5a3aea10..22340779 100644
--- a/src/proof/ssw/sswPart.c
+++ b/src/proof/ssw/sswPart.c
@@ -53,7 +53,7 @@ Aig_Man_t * Ssw_SignalCorrespondencePart( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
     int * pMapBack;
     int i, nCountPis, nCountRegs;
     int nClasses, nPartSize, fVerbose;
-    int clk = clock();
+    clock_t clk = clock();
     if ( pPars->fConstrs )
     {
         printf( "Cannot use partitioned computation with constraints.\n" );
diff --git a/src/proof/ssw/sswRarity.c b/src/proof/ssw/sswRarity.c
index 032bc5ba..7048927f 100644
--- a/src/proof/ssw/sswRarity.c
+++ b/src/proof/ssw/sswRarity.c
@@ -286,7 +286,8 @@ void transpose64Simple( word A[64], word B[64] )
 void TransposeTest()
 {
     word M[64], N[64];
-    int i, clk;
+    int i;
+    clock_t clk;
     Aig_ManRandom64( 1 );
 //    for ( i = 0; i < 64; i++ )
 //        M[i] = Aig_ManRandom64( 0 );
@@ -896,8 +897,9 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, in
     int fTryBmc = 0;
     int fMiter = 1;
     Ssw_RarMan_t * p;
-    int r, f = -1, clk, clkTotal = clock();
-    int nTimeToStop = time(NULL) + TimeOut;
+    int r, f = -1;
+    clock_t clk, clkTotal = clock();
+    clock_t nTimeToStop = TimeOut ? TimeOut * CLOCKS_PER_SEC + clock(): 0;
     int RetValue = -1;
     int iFrameFail = -1;
     assert( Aig_ManRegNum(pAig) > 0 );
@@ -945,7 +947,7 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, in
                 goto finish;
             }
             // check timeout
-            if ( TimeOut && time(NULL) > nTimeToStop )
+            if ( TimeOut && clock() > nTimeToStop )
             {
                 if ( fVerbose ) printf( "\n" );
                 printf( "Reached timeout (%d seconds).\n",  TimeOut );
@@ -1013,8 +1015,9 @@ int Ssw_RarSimulateGia( Gia_Man_t * p, int nFrames, int nWords, int nBinSize, in
 int Ssw_RarSignalFilter( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int nRandSeed, int TimeOut, int fMiter, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose )
 {
     Ssw_RarMan_t * p;
-    int r, f = -1, i, k, clkTotal = clock();
-    int nTimeToStop = time(NULL) + TimeOut;
+    int r, f = -1, i, k;
+    clock_t clkTotal = clock();
+    clock_t nTimeToStop = TimeOut ? TimeOut * CLOCKS_PER_SEC + clock(): 0;
     int RetValue = -1;
     assert( Aig_ManRegNum(pAig) > 0 );
     assert( Aig_ManConstrNum(pAig) == 0 );
@@ -1084,7 +1087,7 @@ int Ssw_RarSignalFilter( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize
                 goto finish;
             }
             // check timeout
-            if ( TimeOut && time(NULL) > nTimeToStop )
+            if ( TimeOut && clock() > nTimeToStop )
             {
                 if ( fVerbose ) printf( "\n" );
                 printf( "Reached timeout (%d seconds).\n",  TimeOut );
diff --git a/src/proof/ssw/sswRarity2.c b/src/proof/ssw/sswRarity2.c
index 0851cf3d..1d93de60 100644
--- a/src/proof/ssw/sswRarity2.c
+++ b/src/proof/ssw/sswRarity2.c
@@ -308,8 +308,9 @@ int Ssw_RarSimulate2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, i
 {
     int fMiter = 1;
     Ssw_RarMan_t * p;
-    int r, clk, clkTotal = clock();
-    int nTimeToStop = time(NULL) + TimeOut;
+    int r;
+    clock_t clk, clkTotal = clock();
+    clock_t nTimeToStop = TimeOut ? TimeOut * CLOCKS_PER_SEC + clock(): 0;
     int RetValue = -1;
     assert( Aig_ManRegNum(pAig) > 0 );
     assert( Aig_ManConstrNum(pAig) == 0 );
@@ -352,7 +353,7 @@ int Ssw_RarSimulate2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, i
             printf( "." );
         }
         // check timeout
-        if ( TimeOut && time(NULL) > nTimeToStop )
+        if ( TimeOut && clock() > nTimeToStop )
         {
             if ( fVerbose ) printf( "\n" );
             printf( "Reached timeout (%d seconds).\n",  TimeOut );
@@ -386,8 +387,9 @@ int Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSiz
 {
     int fMiter = 0;
     Ssw_RarMan_t * p;
-    int r, i, k, clkTotal = clock();
-    int nTimeToStop = time(NULL) + TimeOut;
+    int r, i, k;
+    clock_t clkTotal = clock();
+    clock_t nTimeToStop = TimeOut ? TimeOut * CLOCKS_PER_SEC + clock(): 0;
     int RetValue = -1;
     assert( Aig_ManRegNum(pAig) > 0 );
     assert( Aig_ManConstrNum(pAig) == 0 );
@@ -460,7 +462,7 @@ int Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSiz
         Ssw_RarTransferPatterns( p, p->vInits );
         Ssw_SmlInitializeSpecial( p->pSml, p->vInits );
         // check timeout
-        if ( TimeOut && time(NULL) > nTimeToStop )
+        if ( TimeOut && clock() > nTimeToStop )
         {
             if ( fVerbose ) printf( "\n" );
             printf( "Reached timeout (%d seconds).\n",  TimeOut );
diff --git a/src/proof/ssw/sswSat.c b/src/proof/ssw/sswSat.c
index 7d371cac..e5971a64 100644
--- a/src/proof/ssw/sswSat.c
+++ b/src/proof/ssw/sswSat.c
@@ -45,7 +45,8 @@ ABC_NAMESPACE_IMPL_START
 int Ssw_NodesAreEquiv( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
 {
     int nBTLimit = p->pPars->nBTLimit;
-    int pLits[3], nLits, RetValue, RetValue1, clk;//, status;
+    int pLits[3], nLits, RetValue, RetValue1;
+    clock_t clk;//, status;
     p->nSatCalls++;
     p->pMSat->nSolverCalls++;
 
diff --git a/src/proof/ssw/sswSemi.c b/src/proof/ssw/sswSemi.c
index a04f6f54..e58ba848 100644
--- a/src/proof/ssw/sswSemi.c
+++ b/src/proof/ssw/sswSemi.c
@@ -179,7 +179,8 @@ int Ssw_ManFilterBmc( Ssw_Sem_t * pBmc, int iPat, int fCheckTargets )
     Ssw_Man_t * p = pBmc->pMan;
     Aig_Obj_t * pObj, * pObjNew, * pObjLi, * pObjLo;
     unsigned * pInfo;
-    int i, f, clk, RetValue, fFirst = 0;
+    int i, f, RetValue, fFirst = 0;
+    clock_t clk;
 clk = clock();
 
     // start initialized timeframes
@@ -260,7 +261,8 @@ p->timeBmc += clock() - clk;
 int Ssw_FilterUsingSemi( Ssw_Man_t * pMan, int fCheckTargets, int nConfMax, int fVerbose )
 {
     Ssw_Sem_t * p;
-    int RetValue, Frames, Iter, clk = clock();
+    int RetValue, Frames, Iter;
+    clock_t clk = clock();
     p = Ssw_SemManStart( pMan, nConfMax, fVerbose );
     if ( fCheckTargets && Ssw_SemCheckTargets( p ) )
     {
diff --git a/src/proof/ssw/sswSim.c b/src/proof/ssw/sswSim.c
index b53e8baf..bb4a55d2 100644
--- a/src/proof/ssw/sswSim.c
+++ b/src/proof/ssw/sswSim.c
@@ -38,7 +38,7 @@ struct Ssw_Sml_t_
     int              nWordsPref;        // the number of word in the prefix
     int              fNonConstOut;      // have seen a non-const-0 output during simulation
     int              nSimRounds;        // statistics
-    int              timeSim;           // statistics
+    clock_t          timeSim;           // statistics
     unsigned         pData[0];          // simulation data for the nodes
 };
 
@@ -1005,7 +1005,8 @@ int Ssw_SmlCheckNonConstOutputs( Ssw_Sml_t * p )
 void Ssw_SmlSimulateOne( Ssw_Sml_t * p )
 {
     Aig_Obj_t * pObj, * pObjLi, * pObjLo;
-    int f, i, clk;
+    int f, i;
+    clock_t clk;
 clk = clock();
     for ( f = 0; f < p->nFrames; f++ )
     {
@@ -1116,7 +1117,8 @@ void Ssw_SmlSimulateOneDyn_rec( Ssw_Sml_t * p, Aig_Obj_t * pObj, int f, int * pV
 void Ssw_SmlSimulateOneFrame( Ssw_Sml_t * p )
 {
     Aig_Obj_t * pObj, * pObjLi, * pObjLo;
-    int i, clk;
+    int i;
+    clock_t clk;
 clk = clock();
     // simulate the nodes
     Aig_ManForEachNode( p->pAig, pObj, i )
diff --git a/src/proof/ssw/sswSimSat.c b/src/proof/ssw/sswSimSat.c
index 098b1e0f..4d1b3ba2 100644
--- a/src/proof/ssw/sswSimSat.c
+++ b/src/proof/ssw/sswSimSat.c
@@ -45,7 +45,8 @@ ABC_NAMESPACE_IMPL_START
 void Ssw_ManResimulateBit( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pRepr )
 {
     Aig_Obj_t * pObj;
-    int i, RetValue1, RetValue2, clk = clock();
+    int i, RetValue1, RetValue2;
+    clock_t clk = clock();
     // set the PI simulation information
     Aig_ManConst1(p->pAig)->fMarkB = 1;
     Aig_ManForEachCi( p->pAig, pObj, i )
@@ -90,7 +91,8 @@ p->timeSimSat += clock() - clk;
 ***********************************************************************/
 void Ssw_ManResimulateWord( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pRepr, int f )
 {
-    int RetValue1, RetValue2, clk = clock();
+    int RetValue1, RetValue2;
+    clock_t clk = clock();
     // set the PI simulation information
     Ssw_SmlAssignDist1Plus( p->pSml, p->pPatWords );
     // simulate internal nodes
diff --git a/src/proof/ssw/sswSweep.c b/src/proof/ssw/sswSweep.c
index 5dd7a1f2..ab6952a2 100644
--- a/src/proof/ssw/sswSweep.c
+++ b/src/proof/ssw/sswSweep.c
@@ -187,7 +187,8 @@ void Ssw_SmlAddPatternDyn( Ssw_Man_t * p )
 int Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc, Vec_Int_t * vPairs )
 { 
     Aig_Obj_t * pObjRepr, * pObjFraig, * pObjFraig2, * pObjReprFraig;
-    int RetValue, clk;
+    int RetValue;
+    clock_t clk;
     // get representative of this class
     pObjRepr = Aig_ObjRepr( p->pAig, pObj );
     if ( pObjRepr == NULL )
@@ -267,7 +268,8 @@ int Ssw_ManSweepBmc( Ssw_Man_t * p )
 {
     Bar_Progress_t * pProgress = NULL;
     Aig_Obj_t * pObj, * pObjNew, * pObjLi, * pObjLo;
-    int i, f, clk;
+    int i, f;
+    clock_t clk;
 clk = clock();
 
     // start initialized timeframes
@@ -365,7 +367,8 @@ int Ssw_ManSweep( Ssw_Man_t * p )
     static int Counter;
     Bar_Progress_t * pProgress = NULL;
     Aig_Obj_t * pObj, * pObj2, * pObjNew;
-    int nConstrPairs, clk, i, f;
+    int nConstrPairs, i, f;
+    clock_t clk;
     Vec_Int_t * vDisproved;
 
     // perform speculative reduction