From c1298005f3f3fbe75bed2bb1166b2f868f7d633a Mon Sep 17 00:00:00 2001
From: Ahmed <43099566+ahmed-irfan@users.noreply.github.com>
Date: Tue, 19 Dec 2023 21:02:17 -0800
Subject: [PATCH] correct lemmas limit in the multi-check mode

---
 src/mcsat/bool/bool_plugin.c | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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