diff --git a/src/sat/smt/euf_model.cpp b/src/sat/smt/euf_model.cpp index be4c824b3..412aec533 100644 --- a/src/sat/smt/euf_model.cpp +++ b/src/sat/smt/euf_model.cpp @@ -61,6 +61,7 @@ namespace euf { }; void solver::update_model(model_ref& mdl) { + mdl->reset_eval_cache(); for (auto* mb : m_solvers) mb->init_model(); m_values.reset();