From a30232b99a48889a5fa97841c2e22d6b7831b6fc Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 14 Oct 2014 15:19:50 -0700
Subject: [PATCH] fix(library/module): race condition on m_imported

---
 src/library/module.cpp | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/library/module.cpp b/src/library/module.cpp
index 179db6f75..32d591fd7 100644
--- a/src/library/module.cpp
+++ b/src/library/module.cpp
@@ -252,8 +252,8 @@ struct import_modules_fn {
     };
     typedef std::shared_ptr<module_info> module_info_ptr;
     name_map<module_info_ptr> m_module_info;
-    name_set                  m_visited;
-    name_set                  m_imported; // all imported files
+    name_set                  m_visited; // contains visited files in the current call
+    name_set                  m_imported; // contains all imported files, even ones from previous calls
 
     import_modules_fn(environment const & env, unsigned num_threads, bool keep_proofs, io_state const & ios):
         m_senv(env), m_num_threads(num_threads), m_keep_proofs(keep_proofs), m_ios(ios),
@@ -282,6 +282,7 @@ struct import_modules_fn {
         if (m_visited.contains(fname))
             throw exception(sstream() << "circular dependency detected at '" << fname << "'");
         m_visited.insert(fname);
+        m_imported.insert(fname);
         std::ifstream in(fname, std::ifstream::binary);
         if (!in.good())
             throw exception(sstream() << "failed to open file '" << fname << "'");
@@ -430,7 +431,6 @@ struct import_modules_fn {
                 add_import_module_task(d);
             }
         }
-        m_imported.insert(r->m_fname);
     }
 
     optional<asynch_update_fn> next_task() {