diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2016-04-30 10:42:10 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2016-04-30 10:42:10 -0700 |
| commit | e3e62366638f0395c12b0d1e9b7fcb60fc1908eb (patch) | |
| tree | 5efdbae2db2395177d3a5a09591d80383212561c /src/sat/bsat | |
| parent | 1c245b4a4aedb95c3943f792416f5a9bd781f194 (diff) | |
| download | abc-e3e62366638f0395c12b0d1e9b7fcb60fc1908eb.tar.gz abc-e3e62366638f0395c12b0d1e9b7fcb60fc1908eb.tar.bz2 abc-e3e62366638f0395c12b0d1e9b7fcb60fc1908eb.zip | |
This code was accidentally deleted from the SAT solver (effectively disabling restarts!)
Diffstat (limited to 'src/sat/bsat')
| -rw-r--r-- | src/sat/bsat/satSolver.c | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c index 815626ad..e8e13ee7 100644 --- a/src/sat/bsat/satSolver.c +++ b/src/sat/bsat/satSolver.c @@ -1660,6 +1660,13 @@ 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 && (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) ) { |