From f13608acfea891282092e5e5673452f0c777cea8 Mon Sep 17 00:00:00 2001
From: Ahmed Irfan <43099566+ahmed-irfan@users.noreply.github.com>
Date: Sat, 14 Sep 2024 01:50:16 -0700
Subject: [PATCH] fix mcsat clause rescaling (#530)

---
 src/mcsat/bool/bool_plugin.c | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/mcsat/bool/bool_plugin.c b/src/mcsat/bool/bool_plugin.c
index 5106a4d82..f684be47a 100644
--- a/src/mcsat/bool/bool_plugin.c
+++ b/src/mcsat/bool/bool_plugin.c
@@ -398,10 +398,10 @@ void bool_plugin_rescale_clause_scores(bool_plugin_t* bp) {
     clause = bp->lemmas.data[i];
     tag = clause_db_get_tag(&bp->clause_db, clause);
     assert(tag->type == CLAUSE_LEMMA);
-    tag->score /= bp->heuristic_params.lemma_limit_factor;
+    tag->score /= bp->heuristic_params.clause_score_limit;
   }
 
-  bp->heuristic_params.clause_score_bump_factor /= bp->heuristic_params.lemma_limit_factor;
+  bp->heuristic_params.clause_score_bump_factor /= bp->heuristic_params.clause_score_limit;
 }
 
 static