correct lemmas limit in the multi-check mode (#484)

SRI-CSL · Jan 9, 2024 · 893861f · 893861f
1 parent f0c57b4
commit 893861f
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