diff --git a/src/mcsat/bool/bool_plugin.c b/src/mcsat/bool/bool_plugin.c
index f37aece2a..5106a4d82 100644
--- a/src/mcsat/bool/bool_plugin.c
+++ b/src/mcsat/bool/bool_plugin.c
@@ -128,7 +128,7 @@ void bool_plugin_heuristics_init(bool_plugin_t* bp) {
 
   // Clause database compact
   bp->heuristic_params.lemma_limit_init = 1000;
-  bp->heuristic_params.lemma_limit_factor = 1.1;
+  bp->heuristic_params.lemma_limit_factor = 1.05;
 
   // Bool var scoring
   bp->heuristic_params.bool_var_bump_factor = 5;
diff --git a/src/mcsat/solver.c b/src/mcsat/solver.c
index f097301d5..143dcfe4c 100644
--- a/src/mcsat/solver.c
+++ b/src/mcsat/solver.c
@@ -330,8 +330,8 @@ static
 void mcsat_heuristics_init(mcsat_solver_t* mcsat) {
   mcsat->heuristic_params.restart_interval = 10;
   mcsat->heuristic_params.lemma_restart_weight_type = LEMMA_WEIGHT_SIZE;
-  mcsat->heuristic_params.random_decision_freq = 0;
-  mcsat->heuristic_params.random_decision_seed = 0;
+  mcsat->heuristic_params.random_decision_freq = 0.02;
+  mcsat->heuristic_params.random_decision_seed = 0xabcdef98;
 }
 
 static