mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

fix #5252

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-05-17 16:16:12 -07:00
parent 55f8ad068f
commit 4f9ad28a05
1 changed files with 3 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/model/model_evaluator.cpp
View file

@ -18,6 +18,7 @@ Revision History:
--*/ --*/
#include "ast/ast_pp.h" #include "ast/ast_pp.h"
#include "ast/ast_util.h" #include "ast/ast_util.h"
#include "ast/recfun_decl_plugin.h"
#include "ast/rewriter/rewriter_types.h" #include "ast/rewriter/rewriter_types.h"
#include "ast/rewriter/bool_rewriter.h" #include "ast/rewriter/bool_rewriter.h"
#include "ast/rewriter/arith_rewriter.h" #include "ast/rewriter/arith_rewriter.h"
@ -374,6 +375,8 @@ struct evaluator_cfg : public default_rewriter_cfg {
var_subst vs(m, false); var_subst vs(m, false);
result = vs(fi->get_interp(), num, args); 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; return BR_REWRITE_FULL;
} }