From 868a1b9aeb2bf825a68c37c530107efe72d50d5d Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Mon, 31 Oct 2011 14:59:47 -0500
Subject: Fixed the overflow timeout problem in bmc/bmc2/bmc3/int/pdr/sim, etc.

---
 src/sat/bsat/satSolver.c | 7 ++++---
 src/sat/pdr/pdrCore.c    | 6 +++---
 2 files changed, 7 insertions(+), 6 deletions(-)

(limited to 'src/sat')

diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c
index a3da3e30..ac2202dc 100644
--- a/src/sat/bsat/satSolver.c
+++ b/src/sat/bsat/satSolver.c
@@ -1485,7 +1485,7 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit
 //        int nConfs = 0;
         double Ratio = (s->stats.learnts == 0)? 0.0 :
             s->stats.learnts_literals / (double)s->stats.learnts;
-        if ( s->nRuntimeLimit && clock() > s->nRuntimeLimit )
+        if ( s->nRuntimeLimit && time(NULL) > s->nRuntimeLimit )
             break;
 
         if (s->verbosity >= 1)
@@ -1510,7 +1510,7 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit
 
 //        nof_conflicts = nof_conflicts * 3 / 2; //*= 1.5;
         nof_learnts    = nof_learnts * 11 / 10; //*= 1.1;
-
+//printf( "%d ", s->stats.conflicts  );
         // quit the loop if reached an external limit
         if ( s->nConfLimit && s->stats.conflicts > s->nConfLimit )
         {
@@ -1523,9 +1523,10 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit
 //            printf( "Reached the limit on the number of implications (%d).\n", s->nInsLimit );
             break;
         }
-        if ( s->nRuntimeLimit && clock() > s->nRuntimeLimit )
+        if ( s->nRuntimeLimit && time(NULL) > s->nRuntimeLimit )
             break;
     }
+//printf( "\n" );
     if (s->verbosity >= 1)
         printf("==============================================================================\n");
 
diff --git a/src/sat/pdr/pdrCore.c b/src/sat/pdr/pdrCore.c
index 04caba1e..e3c3781f 100644
--- a/src/sat/pdr/pdrCore.c
+++ b/src/sat/pdr/pdrCore.c
@@ -514,7 +514,7 @@ int Pdr_ManBlockCube( Pdr_Man_t * p, Pdr_Set_t * pCube )
         }
 
         // check the timeout
-        if ( p->timeToStop && clock() >= p->timeToStop )
+        if ( p->timeToStop && time(NULL) > p->timeToStop )
             return -1;
     }
     return 1;
@@ -538,7 +538,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
     int k, RetValue = -1;
     int clkTotal = clock();
     int clkStart = clock();
-    p->timeToStop = (p->pPars->nTimeOut == 0) ? 0 : clock() + (CLOCKS_PER_SEC * p->pPars->nTimeOut);
+    p->timeToStop = p->pPars->nTimeOut ? time(NULL) + p->pPars->nTimeOut : 0;
     assert( Vec_PtrSize(p->vSolvers) == 0 );
     // create the first timeframe
     Pdr_ManCreateSolver( p, (k = 0) );
@@ -619,7 +619,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
         }
 
         // check the timeout
-        if ( p->timeToStop && clock() >= p->timeToStop )
+        if ( p->timeToStop && time(NULL) > p->timeToStop )
         {
             if ( fPrintClauses )
             {
-- 
cgit v1.2.3