Fixing time primtouts throughout the code.

1 files changed, 15 insertions, 9 deletions

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