mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-05 21:53:23 +00:00
Code Activity

fix definition expression

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-02-27 16:18:26 -08:00
parent 15f5444b8c
commit 1dcfe583e7
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/ast/recfun_decl_plugin.cpp
View file

@ -511,7 +511,7 @@ namespace recfun {
auto pd = mk_def(fresh_name, n, domain.c_ptr(), m().get_sort(max_expr)); auto pd = mk_def(fresh_name, n, domain.c_ptr(), m().get_sort(max_expr));
func_decl* f = pd.get_def()->get_decl(); func_decl* f = pd.get_def()->get_decl();
expr_ref new_body(m().mk_app(f, n, args.c_ptr()), m()); expr_ref new_body(m().mk_app(f, n, args.c_ptr()), m());
set_definition(subst, pd, n, vars, new_body); set_definition(subst, pd, n, vars, max_expr);
subst.insert(max_expr, new_body); subst.insert(max_expr, new_body);
result = subst(result); result = subst(result);
TRACEFN("substituted " << mk_pp(max_expr, m()) << " -> " << new_body << "\n" << result); TRACEFN("substituted " << mk_pp(max_expr, m()) << " -> " << new_body << "\n" << result);