From 4f9ad28a057eb1dfc8deb66881b2b9093fc7ab69 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 17 May 2021 16:16:12 -0700 Subject: [PATCH] fix #5252 --- src/model/model_evaluator.cpp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp index b1dc9c1ab..23bab1761 100644 --- a/src/model/model_evaluator.cpp +++ b/src/model/model_evaluator.cpp @@ -18,6 +18,7 @@ Revision History: --*/ #include "ast/ast_pp.h" #include "ast/ast_util.h" +#include "ast/recfun_decl_plugin.h" #include "ast/rewriter/rewriter_types.h" #include "ast/rewriter/bool_rewriter.h" #include "ast/rewriter/arith_rewriter.h" @@ -374,6 +375,8 @@ struct evaluator_cfg : public default_rewriter_cfg { var_subst vs(m, false); result = vs(fi->get_interp(), num, args); + if (!is_ground(result.get()) && recfun::util(m).is_defined(f)) + return BR_DONE; return BR_REWRITE_FULL; }