From 267e9e827db145d2986b789fad154ec44e80c1f0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 10 Oct 2023 15:52:54 +0900 Subject: [PATCH] #6935 --- src/model/model_evaluator.cpp | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp index 28b726100..6ecb3c337 100644 --- a/src/model/model_evaluator.cpp +++ b/src/model/model_evaluator.cpp @@ -428,11 +428,15 @@ struct evaluator_cfg : public default_rewriter_cfg { } else if (!fi && m_au.is_considered_partially_interpreted(f, num, args, f_ui)) { fi = m_model.get_func_interp(f_ui); + if (fi) { - var_subst vs(m, false); - result = vs(fi->get_interp(), num, args); - result = m.mk_ite(m.mk_eq(m_au.mk_real(rational(0)), args[1]), result, m.mk_app(f, num, args)); - return BR_DONE; + auto interp = fi->get_interp(); + if (interp) { + var_subst vs(m, false); + result = vs(fi->get_interp(), num, args); + result = m.mk_ite(m.mk_eq(m_au.mk_real(rational(0)), args[1]), result, m.mk_app(f, num, args)); + return BR_DONE; + } } } else if (!fi && m_fpau.is_considered_uninterpreted(f, num, args)) {