Skip to content

Commit 9156288

Browse files
committed
mcsat: gate l2o/recache trigger to base level only
Match the smtcomp2025 branch's recache heuristic: drop the extra non-base-level recache trigger at the top of the search loop, leaving only the base-level-gated trigger after propagation. The recache intervals and every-other-recache l2o split were already identical.
1 parent 583b7a4 commit 9156288

1 file changed

Lines changed: 0 additions & 7 deletions

File tree

src/mcsat/solver.c

Lines changed: 0 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -3055,13 +3055,6 @@ void mcsat_solve(mcsat_solver_t* mcsat, const param_t *params, model_t* mdl, uin
30553055
luby_next(&luby);
30563056
mcsat_request_restart(mcsat);
30573057

3058-
} else if ((*mcsat->solver_stats.conflicts) > recache_limit) {
3059-
// recache
3060-
++recache_round;
3061-
mcsat_request_recache(mcsat);
3062-
double l = log10(recache_round + 9);
3063-
recache_limit = (*mcsat->solver_stats.conflicts) +
3064-
(recache_round * l * l * l * mcsat->heuristic_params.recache_interval);
30653058
}
30663059

30673060
// Process any outstanding requests

0 commit comments

Comments
 (0)