diff --git a/src/mcsat/bool/bool_plugin.c b/src/mcsat/bool/bool_plugin.c index 06736418a..f37aece2a 100644 --- a/src/mcsat/bool/bool_plugin.c +++ b/src/mcsat/bool/bool_plugin.c @@ -1007,7 +1007,7 @@ void bool_plugin_event_notify(plugin_t* plugin, plugin_notify_kind_t kind) { switch (kind) { case MCSAT_SOLVER_START: // Re-initialize the heuristics - bp->lemmas_limit = bp->heuristic_params.lemma_limit_init; + bp->lemmas_limit = bp->lemmas.size + bp->heuristic_params.lemma_limit_init; break; case MCSAT_SOLVER_RESTART: // Check if clause compaction needed