From 20cfe9e02e266c7bcdfe6cece2d1ef99c11613bf Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 23 Nov 2015 11:32:45 -0800 Subject: [PATCH] feat(library/blast/state): improve lazy initialization --- src/library/blast/state.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/library/blast/state.cpp b/src/library/blast/state.cpp index 9732f9ad5..5242bc631 100644 --- a/src/library/blast/state.cpp +++ b/src/library/blast/state.cpp @@ -729,11 +729,11 @@ branch_extension & state::get_extension(unsigned extid) { m_branch.m_extensions[extid] = ext; lean_assert(ext->get_rc() == 1); ext->initialized(); + ext->target_updated(); m_branch.m_active.for_each([&](hypothesis_idx hidx) { hypothesis const & h = get_hypothesis_decl(hidx); ext->hypothesis_activated(h, hidx); }); - ext->target_updated(); return *ext; } else { branch_extension * ext = get_extension_core(extid);