From 34f24aee720721b844fb566d852ef88934c31e00 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 30 Oct 2017 13:50:31 -0500 Subject: [PATCH] fix order of instantiation for recursive functions, #1274 Signed-off-by: Nikolaj Bjorner --- src/smt/smt_context.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index c508a65cb..7b508c7d8 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -4389,7 +4389,8 @@ namespace smt { subst.push_back(arg); } expr_ref bodyr(m); - var_subst sub(m, false); + var_subst sub(m, true); + TRACE("context", tout << expr_ref(q, m) << " " << subst << "\n";); sub(body, subst.size(), subst.c_ptr(), bodyr); func_decl* f = to_app(fn)->get_decl(); func_interp* fi = alloc(func_interp, m, f->get_arity());