From 42288198db21def856bdf448793b69fc9f0eb7c0 Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Tue, 28 Feb 2017 14:22:35 +0100
Subject: [PATCH] fix(kernel/expr): disable caching by default

---
 src/kernel/expr.cpp  | 2 +-
 src/kernel/level.cpp | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp
index c07ca7e3c9..86652aed9d 100644
--- a/src/kernel/expr.cpp
+++ b/src/kernel/expr.cpp
@@ -339,7 +339,7 @@ expr_macro::~expr_macro() {}
 
 // =======================================
 // Constructors
-LEAN_THREAD_VALUE(bool, g_expr_cache_enabled, true);
+LEAN_THREAD_VALUE(bool, g_expr_cache_enabled, false);
 typedef typename std::unordered_set<expr, expr_hash, is_bi_equal_proc> expr_cache;
 MK_THREAD_LOCAL_GET_DEF(expr_cache, get_expr_cache);
 inline expr cache(expr const & e) {
diff --git a/src/kernel/level.cpp b/src/kernel/level.cpp
index b53d329fc7..87e7cd7525 100644
--- a/src/kernel/level.cpp
+++ b/src/kernel/level.cpp
@@ -246,7 +246,7 @@ level const & mk_level_one() { return *g_level_one; }
 bool is_one(level const & l) { return l == mk_level_one(); }
 
 typedef typename std::unordered_set<level, level_hash> level_cache;
-LEAN_THREAD_VALUE(bool, g_level_cache_enabled, true);
+LEAN_THREAD_VALUE(bool, g_level_cache_enabled, false);
 MK_THREAD_LOCAL_GET_DEF(level_cache, get_level_cache);
 bool enable_level_caching(bool f) {
     bool r = g_level_cache_enabled;