From e65a5d0f4739ec7a89ec4500f5ab00ca9ca96de8 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 24 Jul 2019 09:56:11 -0700 Subject: [PATCH] fix #2420 Signed-off-by: Nikolaj Bjorner --- src/model/model_evaluator.cpp | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp index 08edb1001..1b7c54bde 100644 --- a/src/model/model_evaluator.cpp +++ b/src/model/model_evaluator.cpp @@ -141,16 +141,15 @@ struct evaluator_cfg : public default_rewriter_cfg { br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { - TRACE("model_evaluator", tout << f->get_name() << "\n";); result_pr = nullptr; family_id fid = f->get_family_id(); bool is_uninterp = fid != null_family_id && m.get_plugin(fid)->is_considered_uninterpreted(f); br_status st = BR_FAILED; - if (num == 0 && (fid == null_family_id || is_uninterp)) { + TRACE("model_evaluator", tout << f->get_name() << " " << is_uninterp << "\n";); + if (num == 0 && (fid == null_family_id || is_uninterp || m_ar.is_as_array(f))) { expr * val = m_model.get_const_interp(f); if (val != nullptr) { result = val; - // return BR_DONE; return m_ar.is_as_array(val)? BR_REWRITE1 : BR_DONE; } else if (m_model_completion) {