From 334977b8bd6d33c1a284a4f82f891b8de100cc6f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 29 Sep 2014 16:39:43 -0700 Subject: [PATCH] fix(frontends/lean/info_manager): crash when accessing INFO in the end of the file --- src/frontends/lean/info_manager.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/frontends/lean/info_manager.cpp b/src/frontends/lean/info_manager.cpp index 8479a5cbf..e8c156bf0 100644 --- a/src/frontends/lean/info_manager.cpp +++ b/src/frontends/lean/info_manager.cpp @@ -597,7 +597,9 @@ struct info_manager::imp { lean_assert(it != m_env_info.end() && it->m_line <= linenum); auto next = it; next++; - if (next == m_env_info.end() || next->m_line > linenum) + if (next == m_env_info.end()) + return optional>(mk_pair(it->m_env, it->m_options)); + if (next->m_line > linenum) return optional>(mk_pair(next->m_env, next->m_options)); it = next; }