From cf284ce3eb6db66a9400ef842e4eef54a109f5d9 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 10 Jun 2016 15:05:03 -0700
Subject: [PATCH] fix(library/lazy_abstraction): missing case

---
 src/library/lazy_abstraction.cpp | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/src/library/lazy_abstraction.cpp b/src/library/lazy_abstraction.cpp
index 9c42d87bd5..776ee5269b 100644
--- a/src/library/lazy_abstraction.cpp
+++ b/src/library/lazy_abstraction.cpp
@@ -144,6 +144,14 @@ struct push_lazy_abstraction_fn : public replace_visitor {
         return e;
     }
 
+    expr visit_local(expr const & e) override {
+        for (pair<name, unsigned> const & p : m_s) {
+            if (p.first == mlocal_name(e))
+                return mk_var(p.second);
+        }
+        return e;
+    }
+
     expr visit_macro(expr const & e) override {
         if (is_lazy_abstraction(e)) {
             unsigned sz = m_s.size();