clear all caches before setting hints

src/mcsat/solver.c

@@ -2654,7 +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_clear_cache(mcsat->trail);
   trail_update_extra_cache(mcsat->trail);
 
   for (uint32_t i = 0; i < n_mdl_filter; ++i) {

src/mcsat/trail.c

@@ -381,6 +381,15 @@ void trail_copy_unassigned_cache(mcsat_trail_t* trail, mcsat_model_t* to_cache,
   }
 }
 
+inline static
+void trail_clear_unassigned_cache(mcsat_trail_t* trail, mcsat_model_t* cache) {
+  for (variable_t var = 0; var < cache->size; ++var) {
+    if (!trail_has_value(trail, var) && mcsat_model_get_value(cache, var)->type != VALUE_NONE) {
+      mcsat_model_unset_value(cache, var);
+    }
+  }
+}
+
 inline static
 void trail_clear_unassigned_bool_cache(mcsat_trail_t* trail, mcsat_model_t* cache) {
   for (variable_t var = 0; var < cache->size; ++var) {
@@ -449,3 +458,8 @@ void trail_clear_extra_cache(mcsat_trail_t* trail) {
   trail->target_depth = 0;
   trail->best_depth = 0;
 }
+
+void trail_clear_cache(mcsat_trail_t* trail) {
+  trail_clear_unassigned_cache(trail, &trail->model);
+  trail_clear_extra_cache(trail);
+}

src/mcsat/trail.h

@@ -301,4 +301,7 @@ void trail_update_extra_cache(mcsat_trail_t* trail);
 /** clear target/best cache */
 void trail_clear_extra_cache(mcsat_trail_t* trail);
 
+/** clear all caches */
+void trail_clear_cache(mcsat_trail_t* trail);
+
 #endif /* MCSAT_TRAIL_H_ */