diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp index 2fa79b2ce..b1dc9c1ab 100644 --- a/src/model/model_evaluator.cpp +++ b/src/model/model_evaluator.cpp @@ -266,6 +266,7 @@ struct evaluator_cfg : public default_rewriter_cfg { func_interp * fi = m_model.get_func_interp(g); if (fi && (result = fi->get_array_interp(g))) { model_evaluator ev(m_model, m_params); + ev.set_model_completion(false); result = ev(result); m_pinned.push_back(result); m_def_cache.insert(g, result);