From 8ee10e202fad28d24b3a07cc3dfaa8902ef965ab Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 11 Sep 2018 17:58:54 -0700 Subject: [PATCH] chore(library/compiler/lcnf): use `_x_` instead of `_x.` This is a temporary change while we debug the new compiler. --- src/library/compiler/lcnf.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/library/compiler/lcnf.cpp b/src/library/compiler/lcnf.cpp index 8b9e215663..82bbb612e1 100644 --- a/src/library/compiler/lcnf.cpp +++ b/src/library/compiler/lcnf.cpp @@ -46,7 +46,10 @@ public: return e; } else { expr type = infer_type(e); - expr fvar = m_lctx.mk_local_decl(m_ngen, name(m_x, m_next_idx), type, e); + /* Remark: we use `m_x.append_after(m_next_idx)` instead of `name(m_x, m_next_idx)` + because the resulting name is confusing during debugging: it looks like a projection application. + We should replace it with `name(m_x, m_next_idx)` when the compiler code gets more stable. */ + expr fvar = m_lctx.mk_local_decl(m_ngen, m_x.append_after(m_next_idx), type, e); m_next_idx++; m_fvars.push_back(fvar); return fvar;