Fixing time primtouts throughout the code.

15 files changed, 110 insertions, 88 deletions

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 );