From 2ca16a099b206f6cd82e3daac57152742bba9f47 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 6 May 2015 13:57:36 -0700
Subject: [PATCH] fix(library/max_sharing): conflict with the kernel
 approximate caching

---
 src/library/max_sharing.cpp | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/src/library/max_sharing.cpp b/src/library/max_sharing.cpp
index 43e8744a1..aab155a8a 100644
--- a/src/library/max_sharing.cpp
+++ b/src/library/max_sharing.cpp
@@ -52,7 +52,11 @@ struct max_sharing_fn::imp {
         return res;
     }
 
-    expr operator()(expr const & a) { return apply(a); }
+    expr operator()(expr const & a) {
+        // we must disable approximate/opportunistic hash-consing used in the kernel
+        scoped_expr_caching disable(false);
+        return apply(a);
+    }
 
     bool already_processed(expr const & a) const {
         auto r = m_cache.find(a);