update on caches when setting model hints

src/mcsat/solver.c

@@ -2654,6 +2654,7 @@ void mcsat_set_model_hint(mcsat_solver_t* mcsat, model_t* mdl, uint32_t n_mdl_fi
 
   value_table_t* vtbl = model_get_vtbl(mdl);
 
+  trail_clear_extra_cache(mcsat->trail);
   trail_update_extra_cache(mcsat->trail);
 
   for (uint32_t i = 0; i < n_mdl_filter; ++i) {

src/mcsat/trail.c

@@ -168,10 +168,7 @@ uint32_t trail_pop_base_level(mcsat_trail_t* trail) {
   assert(trail->decision_level_base > 0);
 
   // clear target and best cache, setting their depths to zero
-  clear_cache(&trail->target_cache);
-  clear_cache(&trail->best_cache);
-  trail->best_depth = 0;
-  trail->target_depth = 0;
+  trail_clear_extra_cache(trail);
 
   trail->decision_level_base --;
   return trail->decision_level_base;
@@ -434,3 +431,10 @@ void trail_update_extra_cache(mcsat_trail_t* trail) {
     trail->target_depth = trail->elements.size;
   }
 }
+
+void trail_clear_extra_cache(mcsat_trail_t* trail) {
+  clear_cache(&trail->target_cache);
+  clear_cache(&trail->best_cache);
+  trail->target_depth = 0;
+  trail->best_depth = 0;
+}

src/mcsat/trail.h

@@ -290,12 +290,15 @@ void trail_gc_mark(mcsat_trail_t* trail, gc_info_t* gc_vars);
 void trail_gc_sweep(mcsat_trail_t* trail, const gc_info_t* gc_vars);
 
 /** compare variables based on the trail level, unassigned to the front, then assigned ones by decreasing level */
-bool trail_variable_compare(const mcsat_trail_t *trail, variable_t t1, variable_t t2);
+bool trail_variable_compare(const mcsat_trail_t* trail, variable_t t1, variable_t t2);
 
 /** Recache */
 void trail_recache(mcsat_trail_t* trail, uint32_t round);
 
-/** save target cache */
-void trail_update_extra_cache(mcsat_trail_t *trail);
+/** save target/best cache */
+void trail_update_extra_cache(mcsat_trail_t* trail);
+
+/** clear target/best cache */
+void trail_clear_extra_cache(mcsat_trail_t* trail);
 
 #endif /* MCSAT_TRAIL_H_ */