From 97145c0f88650d8536202e44d726cacdc3d7addd Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 21 Dec 2013 06:41:09 -0800
Subject: [PATCH] fix(library/elaborator): bug in free variable normalization
 (lift was missing)

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/library/elaborator/elaborator.cpp       | 2 +-
 src/tests/library/elaborator/elaborator.cpp | 9 +++++----
 2 files changed, 6 insertions(+), 5 deletions(-)

diff --git a/src/library/elaborator/elaborator.cpp b/src/library/elaborator/elaborator.cpp
index 2de1d48f6..23ce36787 100644
--- a/src/library/elaborator/elaborator.cpp
+++ b/src/library/elaborator/elaborator.cpp
@@ -562,7 +562,7 @@ class elaborator::imp {
         if (is_var(a)) {
             auto e = find(ctx, var_idx(a));
             if (e && e->get_body())
-                a = *(e->get_body());
+                a = lift_free_vars(*(e->get_body()), var_idx(a) + 1, m_state.m_menv);
         }
     }
 
diff --git a/src/tests/library/elaborator/elaborator.cpp b/src/tests/library/elaborator/elaborator.cpp
index 4a7ab2a9c..f3d0122a0 100644
--- a/src/tests/library/elaborator/elaborator.cpp
+++ b/src/tests/library/elaborator/elaborator.cpp
@@ -633,11 +633,12 @@ void tst19() {
 void tst20() {
     std::cout << "\nTST 20\n";
     environment env;
+    import_all(env);
     metavar_env menv;
-    expr N  = Const("N");
-    expr M  = Const("M");
-    env->add_var("N", Type());
-    env->add_var("M", Type());
+    expr N  = Const("N1");
+    expr M  = Const("M1");
+    env->add_var("N1", Type());
+    env->add_var("M1", Type());
     env->add_var("f", N >> (M >> M));
     env->add_var("a", N);
     env->add_var("b", M);