From 53ee205dc62c36f8f7296e474a110e52dfd41c63 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 17 Feb 2014 15:32:27 -0800 Subject: [PATCH] fix(kernel): memory corruption bugs Signed-off-by: Leonardo de Moura --- src/kernel/expr.cpp | 2 +- src/kernel/instantiate.cpp | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp index 83346152f1..434a49bf42 100644 --- a/src/kernel/expr.cpp +++ b/src/kernel/expr.cpp @@ -149,7 +149,7 @@ void expr_app::dealloc(buffer & todelete) { // Expr binders (Lambda, Pi and Sigma) expr_binder::expr_binder(expr_kind k, name const & n, expr const & t, expr const & b): expr_composite(k, ::lean::hash(t.hash(), b.hash()), t.has_metavar() || b.has_metavar(), - std::max(get_depth(m_domain), get_depth(m_body)) + 1), + std::max(get_depth(t), get_depth(b)) + 1), m_name(n), m_domain(t), m_body(b) { diff --git a/src/kernel/instantiate.cpp b/src/kernel/instantiate.cpp index 65eafe0abf..010cdabf3d 100644 --- a/src/kernel/instantiate.cpp +++ b/src/kernel/instantiate.cpp @@ -93,7 +93,7 @@ expr head_beta_reduce(expr const & t) { expr const * it = &t; while (true) { lean_assert(is_app(*it)); - expr f = app_fn(*it); + expr const & f = app_fn(*it); args.push_back(app_arg(*it)); if (is_lambda(f)) { return apply_beta(f, args.size(), args.data());