From 1080edd490f6f7cb5893feb0791da8649c4e81b7 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 15 Feb 2019 15:22:33 -0800 Subject: [PATCH] fix(library/compiler/lambda_lifting): make sure auxiliary `_lambda` declarations come before the declarations that use them This fixes a nasty initialization bug where an auxiliary `_closed` declaration for an auxiliary `_lambda` is accessed before it is initialized. --- src/library/compiler/lambda_lifting.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/library/compiler/lambda_lifting.cpp b/src/library/compiler/lambda_lifting.cpp index 793585d802..3a6d73bd35 100644 --- a/src/library/compiler/lambda_lifting.cpp +++ b/src/library/compiler/lambda_lifting.cpp @@ -200,7 +200,8 @@ public: m_base_name = cdecl.fst(); expr r = visit(cdecl.snd(), true); comp_decl new_cdecl(cdecl.fst(), r); - return mk_pair(m_env, comp_decls(new_cdecl, comp_decls(m_new_decls))); + m_new_decls.push_back(new_cdecl); + return mk_pair(m_env, comp_decls(m_new_decls)); } };