From 868a1b9aeb2bf825a68c37c530107efe72d50d5d Mon Sep 17 00:00:00 2001 From: Alan Mishchenko 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 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) (limited to 'src/sat/bsat/satSolver.c') 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"); -- cgit v1.2.3