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

1 files changed, 4 insertions, 3 deletions

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