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);