From 4a430167352abe762a0228ac2e85553ef8c72482 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 6 Jun 2014 18:00:26 -0700 Subject: [PATCH] fix(kernel/expr): expr_cache initialization Signed-off-by: Leonardo de Moura --- src/kernel/expr.cpp | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp index 6699b9f61..4fe5ffdff 100644 --- a/src/kernel/expr.cpp +++ b/src/kernel/expr.cpp @@ -268,11 +268,13 @@ expr_macro::~expr_macro() { #ifdef LEAN_CACHE_EXPRS typedef lru_cache expr_cache; -static expr_cache LEAN_THREAD_LOCAL g_expr_cache(LEAN_INITIAL_EXPR_CACHE_CAPACITY); +static std::unique_ptr LEAN_THREAD_LOCAL g_expr_cache; static bool LEAN_THREAD_LOCAL g_expr_cache_enabled = true; inline expr cache(expr const & e) { if (g_expr_cache_enabled) { - if (auto r = g_expr_cache.insert(e)) + if (!g_expr_cache) + g_expr_cache.reset(new expr_cache(LEAN_INITIAL_EXPR_CACHE_CAPACITY)); + if (auto r = g_expr_cache->insert(e)) return *r; } return e;