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; }