diff --git a/src/mcsat/solver.c b/src/mcsat/solver.c index 030983f75..9c2e4d2f3 100644 --- a/src/mcsat/solver.c +++ b/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) { diff --git a/src/mcsat/trail.c b/src/mcsat/trail.c index 40b808375..a061d0050 100644 --- a/src/mcsat/trail.c +++ b/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; +} diff --git a/src/mcsat/trail.h b/src/mcsat/trail.h index b35d28d0c..24a6d216a 100644 --- a/src/mcsat/trail.h +++ b/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_ */