Fixed the overflow timeout problem in bmc/bmc2/bmc3/int/pdr/sim, etc.

4 files changed, 12 insertions, 22 deletions

diff --git a/src/aig/llb/llb1Reach.c b/src/aig/llb/llb1Reach.c
index 16b62850..e427eb24 100644
--- a/src/aig/llb/llb1Reach.c
+++ b/src/aig/llb/llb1Reach.c
@@ -586,10 +586,7 @@ int Llb_ManReachability( Llb_Man_t * p, Vec_Int_t * vHints, DdManager ** pddGlo
     int nThreshold = 10000;
 
     // compute time to stop
-    if ( p->pPars->TimeLimit )
-        p->pPars->TimeTarget = clock() + p->pPars->TimeLimit * CLOCKS_PER_SEC;
-    else
-        p->pPars->TimeTarget = 0;
+    p->pPars->TimeTarget = p->pPars->TimeLimit ? time(NULL) + p->pPars->TimeLimit : 0;
 
     // define variable limits
     Llb_ManPrepareVarLimits( p );
@@ -660,7 +657,7 @@ int Llb_ManReachability( Llb_Man_t * p, Vec_Int_t * vHints, DdManager ** pddGlo
     { 
         clk2 = clock();
         // check the runtime limit
-        if ( p->pPars->TimeLimit && clock() >= p->pPars->TimeTarget )
+        if ( p->pPars->TimeLimit && time(NULL) > p->pPars->TimeTarget )
         {
             if ( !p->pPars->fSilent )
                 printf( "Reached timeout during image computation (%d seconds).\n",  p->pPars->TimeLimit );
diff --git a/src/aig/llb/llb2Core.c b/src/aig/llb/llb2Core.c
index 7badc1fb..4ecd1cdf 100644
--- a/src/aig/llb/llb2Core.c
+++ b/src/aig/llb/llb2Core.c
@@ -218,7 +218,7 @@ int Llb_CoreReachability_int( Llb_Img_t * p, Vec_Ptr_t * vQuant0, Vec_Ptr_t * vQ
         p->pPars->TimeTarget = 0;
 */
 
-    if ( p->pPars->TimeLimit && clock() >= p->pPars->TimeTarget )
+    if ( time(NULL) > p->pPars->TimeTarget )
     {
         if ( !p->pPars->fSilent )
             printf( "Reached timeout (%d seconds) before image computation.\n", p->pPars->TimeLimit );
@@ -286,7 +286,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 && clock() >= p->pPars->TimeTarget )
+        if ( p->pPars->TimeLimit && time(NULL) > p->pPars->TimeTarget )
         {
             if ( !p->pPars->fSilent )
                 printf( "Reached timeout (%d seconds) during image computation.\n",  p->pPars->TimeLimit );
@@ -729,10 +729,7 @@ int Llb_ManReachMinCut( Aig_Man_t * pAig, Gia_ParLlb_t * pPars )
     int clk = clock();
 
     // compute time to stop
-    if ( pPars->TimeLimit )
-        pPars->TimeTarget = clock() + pPars->TimeLimit * CLOCKS_PER_SEC;
-    else
-        pPars->TimeTarget = 0;
+    pPars->TimeTarget = pPars->TimeLimit ? time(NULL) + pPars->TimeLimit : 0;
 
     p = Aig_ManDupFlopsOnly( pAig );
 //Aig_ManShow( p, 0, NULL );
@@ -744,7 +741,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 && clock() >= pPars->TimeTarget )
+    if ( pPars->TimeLimit && time(NULL) > pPars->TimeTarget )
     {
         if ( !pPars->fSilent )
             printf( "Reached timeout (%d seconds) after partitioning.\n", pPars->TimeLimit );
diff --git a/src/aig/llb/llb3Nonlin.c b/src/aig/llb/llb3Nonlin.c
index f41e0f6e..e20a1541 100644
--- a/src/aig/llb/llb3Nonlin.c
+++ b/src/aig/llb/llb3Nonlin.c
@@ -433,10 +433,8 @@ int Llb_NonlinReachability( Llb_Mnn_t * p )
     assert( Aig_ManRegNum(p->pAig) > 0 );
 
     // compute time to stop
-    if ( p->pPars->TimeLimit )
-        p->pPars->TimeTarget = clock() + p->pPars->TimeLimit * CLOCKS_PER_SEC;
-    else
-        p->pPars->TimeTarget = 0;
+    p->pPars->TimeTarget = p->pPars->TimeLimit ? time(NULL) + p->pPars->TimeLimit : 0;
+
     // set the stop time parameter
     p->dd->TimeStop  = p->pPars->TimeTarget;
     p->ddG->TimeStop = p->pPars->TimeTarget;
@@ -474,7 +472,7 @@ int Llb_NonlinReachability( Llb_Mnn_t * p )
     { 
         // check the runtime limit
         clk2 = clock();
-        if ( p->pPars->TimeLimit && clock() >= p->pPars->TimeTarget )
+        if ( p->pPars->TimeLimit && time(NULL) > p->pPars->TimeTarget )
         {
             if ( !p->pPars->fSilent )
                 printf( "Reached timeout (%d seconds) during image computation.\n",  p->pPars->TimeLimit );
diff --git a/src/aig/llb/llb4Nonlin.c b/src/aig/llb/llb4Nonlin.c
index 8d096b20..24cd0ac5 100644
--- a/src/aig/llb/llb4Nonlin.c
+++ b/src/aig/llb/llb4Nonlin.c
@@ -725,7 +725,7 @@ int Llb_Nonlin4Reachability( Llb_Mnx_t * p )
     { 
         clkIter = clock();
         // check the runtime limit
-        if ( p->pPars->TimeLimit && clock() >= p->pPars->TimeTarget )
+        if ( p->pPars->TimeLimit && time(NULL) > p->pPars->TimeTarget )
         {
             if ( !p->pPars->fSilent )
                 printf( "Reached timeout (%d seconds) during image computation.\n",  p->pPars->TimeLimit );
@@ -929,10 +929,8 @@ Llb_Mnx_t * Llb_MnxStart( Aig_Man_t * pAig, Gia_ParLlb_t * pPars )
     p->pPars   = pPars;
 
     // compute time to stop
-    if ( p->pPars->TimeLimit )
-        p->pPars->TimeTarget = clock() + p->pPars->TimeLimit * CLOCKS_PER_SEC;
-    else
-        p->pPars->TimeTarget = 0;
+    p->pPars->TimeTarget = p->pPars->TimeLimit ? time(NULL) + p->pPars->TimeLimit : 0;
+
     if ( pPars->fCluster )
     {
 //        Llb_Nonlin4Cluster( p->pAig, &p->dd, &p->vOrder, &p->vRoots, pPars->nBddMax, pPars->fVerbose );