diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp
index 5bc64b177..48d922123 100644
--- a/src/kernel/expr.cpp
+++ b/src/kernel/expr.cpp
@@ -271,8 +271,10 @@ static bool LEAN_THREAD_LOCAL g_expr_cache_enabled = true;
 typedef lru_cache<expr, expr_hash, is_bi_equal_proc> expr_cache;
 inline expr cache(expr const & e) {
     if (g_expr_cache_enabled) {
-        static expr_cache LEAN_THREAD_LOCAL g_expr_cache(LEAN_INITIAL_EXPR_CACHE_CAPACITY);
-        if (auto r = g_expr_cache.insert(e))
+        LEAN_THREAD_PTR(expr_cache) g_expr_cache;
+        if (!g_expr_cache.get())
+            g_expr_cache.reset(new expr_cache(LEAN_INITIAL_EXPR_CACHE_CAPACITY));
+        if (auto r = g_expr_cache->insert(e))
             return *r;
     }
     return e;
diff --git a/src/util/thread.h b/src/util/thread.h
index 42988d2ca..2c9511b30 100644
--- a/src/util/thread.h
+++ b/src/util/thread.h
@@ -146,3 +146,11 @@ public:
 };
 }
 #endif
+
+// LEAN_THREAD_PTR macro
+#if defined(LEAN_USE_BOOST)
+  #include <boost/thread/tss.hpp>
+  #define LEAN_THREAD_PTR(T) static boost::thread_specific_ptr<T>
+#else
+  #define LEAN_THREAD_PTR(T) static std::unique_ptr<T> LEAN_THREAD_LOCAL
+#endif