From 57c0c69872ad0598102871807f0826da3b9ecf34 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 4 Sep 2013 04:28:09 -0700 Subject: [PATCH] Fix bug reported by Valgrind. Reason: m_metavars is a vector of metavar_info; each metavar_info has a context; when we invoke mk_metavar the vector can grow in size, and the context is moved to a new location. The previous location is invalidated. To avoid the problem we have to save ctx in a local variable. Signed-off-by: Leonardo de Moura --- src/frontends/lean/lean_elaborator.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/frontends/lean/lean_elaborator.cpp b/src/frontends/lean/lean_elaborator.cpp index 1e257b1b9..cf4243f16 100644 --- a/src/frontends/lean/lean_elaborator.cpp +++ b/src/frontends/lean/lean_elaborator.cpp @@ -121,7 +121,8 @@ class elaborator::imp { if (m_metavars[midx].m_type) { return m_metavars[midx].m_type; } else { - expr t = mk_metavar(m_metavars[midx].m_ctx); + context ctx = m_metavars[midx].m_ctx; + expr t = mk_metavar(ctx); m_metavars[midx].m_type = t; return t; }