fix and update param

SRI-CSL · Apr 20, 2024 · 701f5d6 · 701f5d6
1 parent 882ee5f
commit 701f5d6
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 2 deletions.
diff --git a/src/mcsat/solver.c b/src/mcsat/solver.c
@@ -337,7 +337,7 @@ 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.recache_interval = 1000;
+  mcsat->heuristic_params.recache_interval = 10000;
   mcsat->heuristic_params.random_decision_freq = 0.02;
   mcsat->heuristic_params.random_decision_seed = 0xabcdef98;
 }

diff --git a/src/mcsat/trail.c b/src/mcsat/trail.c
@@ -301,7 +301,8 @@ void trail_gc_sweep(mcsat_trail_t* trail, const gc_info_t* gc_vars) {
 void trail_model_cache_clear(mcsat_trail_t* trail) {
   variable_t var;
   for (var = 0; var < trail->model.size; ++var) {
-    if (!trail_has_value(trail, var)) {
+    if (!trail_has_value(trail, var) &&
+	mcsat_model_get_value(&trail->model, var)->type != VALUE_NONE) {
       mcsat_model_unset_value(&trail->model, var);
     }
   }