From cec6bd645e87a722f7144e29859617ae9dc6e5c2 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 21 Jun 2013 12:52:23 -0700 Subject: Limiting runtime limit checks in 'pdr'. --- src/sat/bsat/satSolver.c | 2 +- src/sat/bsat/satSolver2.c | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) (limited to 'src/sat') diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c index 8d1bd455..56bd128c 100644 --- a/src/sat/bsat/satSolver.c +++ b/src/sat/bsat/satSolver.c @@ -1576,7 +1576,7 @@ static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts) int next; // Reached bound on number of conflicts: - if ((nof_conflicts >= 0 && conflictC >= nof_conflicts) || (s->nRuntimeLimit && Abc_Clock() > s->nRuntimeLimit)){ + if ((nof_conflicts >= 0 && conflictC >= nof_conflicts) || (s->nRuntimeLimit && (s->stats.conflicts & 63) == 0 && Abc_Clock() > s->nRuntimeLimit)){ s->progress_estimate = sat_solver_progress(s); sat_solver_canceluntil(s,s->root_level); veci_delete(&learnt_clause); diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c index cde1d3b1..84d59f62 100644 --- a/src/sat/bsat/satSolver2.c +++ b/src/sat/bsat/satSolver2.c @@ -1037,7 +1037,7 @@ static lbool solver2_search(sat_solver2* s, ABC_INT64_T nof_conflicts) // NO CONFLICT int next; - if ((nof_conflicts >= 0 && conflictC >= nof_conflicts) || (s->nRuntimeLimit && Abc_Clock() > s->nRuntimeLimit)){ + if ((nof_conflicts >= 0 && conflictC >= nof_conflicts) || (s->nRuntimeLimit && (s->stats.conflicts & 63) == 0 && Abc_Clock() > s->nRuntimeLimit)){ // Reached bound on number of conflicts: s->progress_estimate = solver2_progress(s); solver2_canceluntil(s,s->root_level); -- cgit v1.2.3