From 703659a3a88d2b7e2f03b2905ebacf3fb75330e3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 28 Jul 2021 17:15:55 -0700 Subject: [PATCH] fix #5439 --- src/ast/recfun_decl_plugin.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/ast/recfun_decl_plugin.cpp b/src/ast/recfun_decl_plugin.cpp index bd23e1838..04c5d0545 100644 --- a/src/ast/recfun_decl_plugin.cpp +++ b/src/ast/recfun_decl_plugin.cpp @@ -338,7 +338,9 @@ namespace recfun { void util::set_definition(replace& subst, promise_def & d, bool is_macro, unsigned n_vars, var * const * vars, expr * rhs) { - expr_ref rhs1 = get_plugin().redirect_ite(subst, n_vars, vars, rhs); + expr_ref rhs1(rhs, m()); + if (!is_macro) + rhs1 = get_plugin().redirect_ite(subst, n_vars, vars, rhs); d.set_definition(subst, is_macro, n_vars, vars, rhs1); }