From e11fe27de27f01f9cefbc7461e026e71b8a6a823 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 1 Nov 2018 14:26:04 -0700
Subject: [PATCH] chore(library/compiler/lambda_lifting): temporary hack

Make sure that a join point that has been lambda lifted is not tagged as
a join point anymore.
---
 src/library/compiler/lambda_lifting.cpp | 14 ++++++++++++--
 1 file changed, 12 insertions(+), 2 deletions(-)

diff --git a/src/library/compiler/lambda_lifting.cpp b/src/library/compiler/lambda_lifting.cpp
index 7558df6517..003cc89472 100644
--- a/src/library/compiler/lambda_lifting.cpp
+++ b/src/library/compiler/lambda_lifting.cpp
@@ -19,6 +19,10 @@ class lambda_lifting_fn {
     buffer<comp_decl>   m_new_decls;
     name                m_base_name;
     unsigned            m_next_idx{1};
+    name                m_y;
+    unsigned            m_next_let_idx{1};
+
+
     typedef std::unordered_set<name, name_hash> name_set;
 
     environment const & env() { return m_env; }
@@ -38,6 +42,12 @@ class lambda_lifting_fn {
         return m_lctx.mk_lambda(fvars, r);
     }
 
+    name next_let_name() {
+        name r = m_y.append_after(m_next_let_idx);
+        m_next_let_idx++;
+        return r;
+    }
+
     expr visit_let(expr e) {
         flet<local_ctx> save_lctx(m_lctx, m_lctx);
         buffer<expr> fvars;
@@ -46,7 +56,7 @@ class lambda_lifting_fn {
             bool not_root = false;
             bool jp       = is_join_point_name(let_name(e));
             expr new_val  = visit(instantiate_rev(let_value(e), fvars.size(), fvars.data()), not_root, jp);
-            expr new_fvar = m_lctx.mk_local_decl(ngen(), let_name(e), let_type(e), new_val);
+            expr new_fvar = m_lctx.mk_local_decl(ngen(), next_let_name(), let_type(e), new_val);
             fvars.push_back(new_fvar);
             e = let_body(e);
         }
@@ -153,7 +163,7 @@ class lambda_lifting_fn {
 
 public:
     lambda_lifting_fn(environment const & env):
-        m_env(env) {}
+        m_env(env), m_y("_y") {}
 
     comp_decls operator()(comp_decl const & cdecl) {
         m_base_name = cdecl.fst();