From d8a8300a4f4e2280366a674fd7a479bed94a92b3 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 23 Jun 2014 16:55:51 -0700 Subject: [PATCH] fix(kernel/expr): initialization problem Signed-off-by: Leonardo de Moura --- src/kernel/expr.cpp | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp index 43f26c85b..15b2ef185 100644 --- a/src/kernel/expr.cpp +++ b/src/kernel/expr.cpp @@ -403,9 +403,14 @@ unsigned get_app_num_args(expr const & e) { return n; } -static name g_default_var_name("a"); -bool is_default_var_name(name const & n) { return n == g_default_var_name; } -expr mk_arrow(expr const & t, expr const & e) { return mk_pi(g_default_var_name, t, e); } +static name const & get_default_var_name() { + static name r("a"); + return r; +} +static name const & g_default_var_name = get_default_var_name(); // force it to be initialized + +bool is_default_var_name(name const & n) { return n == get_default_var_name(); } +expr mk_arrow(expr const & t, expr const & e) { return mk_pi(get_default_var_name(), t, e); } expr mk_pi(unsigned sz, expr const * domain, expr const & range) { expr r = range;