diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c index 815626ad8..e8e13ee75 100644 --- a/src/sat/bsat/satSolver.c +++ b/src/sat/bsat/satSolver.c @@ -1659,6 +1659,13 @@ static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts) // NO CONFLICT int next; + // Reached bound on number of conflicts: + 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); + return l_Undef; } + // Reached bound on number of conflicts: if ( (s->nConfLimit && s->stats.conflicts > s->nConfLimit) || (s->nInsLimit && s->stats.propagations > s->nInsLimit) )