From 1be2a30c8cab4243abac017a1bdd1b35ccb64f1d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 16 Sep 2013 09:14:18 -0700
Subject: [PATCH] Fix bug in normalizer. We must create a scope whenever we
 extend the value stack.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/kernel/normalizer.cpp | 20 ++++++++++++++++----
 src/util/scoped_map.h     |  8 +++++++-
 2 files changed, 23 insertions(+), 5 deletions(-)

diff --git a/src/kernel/normalizer.cpp b/src/kernel/normalizer.cpp
index 0d79a0931..ea1afada4 100644
--- a/src/kernel/normalizer.cpp
+++ b/src/kernel/normalizer.cpp
@@ -83,9 +83,17 @@ class normalizer::imp {
     */
     struct save_context {
         imp &           m_imp;
-        context         m_old_ctx;
-        save_context(imp & imp):m_imp(imp), m_old_ctx(m_imp.m_ctx) { m_imp.m_cache.clear(); }
-        ~save_context() { m_imp.m_ctx = m_old_ctx; }
+        context         m_saved_ctx;
+        cache           m_saved_cache;
+        save_context(imp & imp):
+            m_imp(imp),
+            m_saved_ctx(m_imp.m_ctx) {
+            m_imp.m_cache.swap(m_saved_cache);
+        }
+        ~save_context() {
+            m_imp.m_ctx = m_saved_ctx;
+            m_imp.m_cache.swap(m_saved_cache);
+        }
     };
 
     svalue lookup(value_stack const & s, unsigned i, unsigned k) {
@@ -114,7 +122,11 @@ class normalizer::imp {
     expr reify_closure(expr const & a, value_stack const & s, unsigned k) {
         lean_assert(is_lambda(a));
         expr new_t = reify(normalize(abst_domain(a), s, k), k);
-        expr new_b = reify(normalize(abst_body(a), extend(s, svalue(k)), k+1), k+1);
+        expr new_b;
+        {
+            cache::mk_scope sc(m_cache);
+            new_b = reify(normalize(abst_body(a), extend(s, svalue(k)), k+1), k+1);
+        }
         return mk_lambda(abst_name(a), new_t, new_b);
     }
 
diff --git a/src/util/scoped_map.h b/src/util/scoped_map.h
index 0b1664219..59382563f 100644
--- a/src/util/scoped_map.h
+++ b/src/util/scoped_map.h
@@ -26,7 +26,7 @@ class scoped_map {
     typedef typename map::size_type                    size_type;
     typedef typename map::value_type                   value_type;
     enum class action_kind { Insert, Replace, Erase };
-    map                                      m_map;
+    map                                             m_map;
     std::vector<std::pair<action_kind, value_type>> m_actions;
     std::vector<unsigned>                           m_scopes;
 public:
@@ -35,6 +35,12 @@ public:
                         const KeyEqual& equal = KeyEqual()):
         m_map(bucket_count, hash, equal) {}
 
+    void swap(scoped_map & other) {
+        m_map.swap(other.m_map);
+        m_actions.swap(other.m_actions);
+        m_scopes.swap(other.m_scopes);
+    }
+
     /** \brief Return the number of scopes. */
     unsigned num_scopes() const {
         return m_scopes.size();