fix mcsat clause rescaling (#530)

SRI-CSL · Sep 14, 2024 · f13608a · f13608a
1 parent c36eb74
commit f13608a
Showing 1 changed file with 2 additions and 2 deletions.
diff --git 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