correct lemmas limit in the multi-check mode

SRI-CSL · Dec 20, 2023 · c129800 · c129800
1 parent cda317c
commit c129800
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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