diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index c2b99e8397..5afc626f8d 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -42,6 +42,7 @@ option(ABSTRACTION_CACHE   "ABSTRACTION_CACHE"    ON)
 option(TYPE_CLASS_CACHE    "TYPE_CLASS_CACHE"     ON)
 option(TYPE_INFER_CACHE    "TYPE_INFER_CACHE"     ON)
 option(ALPHA               "ALPHA FEATURES"       OFF)
+option(TRACK_CUSTOM_ALLOCATORS "TRACK_CUSTOM_ALLOCATORS" OFF)
 
 # emacs site-lisp dir
 set(EMACS_LISP_DIR        "share/emacs/site-lisp/lean" CACHE STRING "emacs site-lisp dir")
@@ -74,6 +75,9 @@ if ("${ALPHA}" MATCHES "ON")
   set(LEAN_EXTRA_CXX_FLAGS "${LEAN_EXTRA_CXX_FLAGS} -D LEAN_USE_ALPHA")
 endif()
 
+if ("${TRACK_CUSTOM_ALLOCATORS}" MATCHES "ON")
+  set(LEAN_EXTRA_CXX_FLAGS "${LEAN_EXTRA_CXX_FLAGS} -D LEAN_TRACK_CUSTOM_ALLOCATORS")
+endif()
 
 message(STATUS "Lean emacs-mode will be installed at "
   "${CMAKE_INSTALL_PREFIX}/${EMACS_LISP_DIR}")
diff --git a/src/init/init.cpp b/src/init/init.cpp
index 7dbdfbbc51..1f4d1c8b6d 100644
--- a/src/init/init.cpp
+++ b/src/init/init.cpp
@@ -77,7 +77,13 @@ initializer::initializer() {
 }
 
 initializer::~initializer() {
+#ifdef LEAN_TRACK_CUSTOM_ALLOCATORS
+    std::cout << "memory deallocated by memory_pool and small_object_allocator (before finalization): " << get_memory_deallocated() << "\n";
+#endif
     finalize();
     delete_thread_finalizer_manager();
+#ifdef LEAN_TRACK_CUSTOM_ALLOCATORS
+    std::cout << "memory deallocated by memory_pool and small_object_allocator (after finalization): " << get_memory_deallocated() << "\n";
+#endif
 }
 }
diff --git a/src/util/memory.cpp b/src/util/memory.cpp
index c6d73cbddb..7bd19614c1 100644
--- a/src/util/memory.cpp
+++ b/src/util/memory.cpp
@@ -118,4 +118,14 @@ void check_memory(char const * component_name) {
 size_t get_allocated_memory() {
     return get_current_rss();
 }
+
+static atomic<size_t> g_memory_deallocated(0);
+
+void report_memory_deallocated(size_t s) {
+    atomic_fetch_add_explicit(&g_memory_deallocated, s, memory_order_release);
+}
+
+size_t get_memory_deallocated() {
+    return g_memory_deallocated;
+}
 }
diff --git a/src/util/memory.h b/src/util/memory.h
index e57f757f36..df4d1f1e5b 100644
--- a/src/util/memory.h
+++ b/src/util/memory.h
@@ -14,4 +14,14 @@ void set_max_memory(size_t max);
 void set_max_memory_megabyte(unsigned max);
 void check_memory(char const * component_name);
 size_t get_allocated_memory();
+
+#ifdef LEAN_TRACK_CUSTOM_ALLOCATORS
+/* We use report_memory_deallocated to track memory released by custom allocators such
+   as memory_pool and small_object_allocator. */
+void report_memory_deallocated(size_t s);
+size_t get_memory_deallocated();
+#define lean_report_memory_deallocated(s) report_memory_deallocated(s)
+#else
+#define lean_report_memory_deallocated(s)
+#endif
 }
diff --git a/src/util/memory_pool.cpp b/src/util/memory_pool.cpp
index f84a113a2c..021715f52f 100644
--- a/src/util/memory_pool.cpp
+++ b/src/util/memory_pool.cpp
@@ -15,6 +15,7 @@ memory_pool::~memory_pool() {
         void * r = m_free_list;
         m_free_list = *(reinterpret_cast<void **>(r));
         free(r);
+        lean_report_memory_deallocated(m_size);
     }
 }
 
diff --git a/src/util/small_object_allocator.cpp b/src/util/small_object_allocator.cpp
index aacf3b6e03..5c777946d1 100644
--- a/src/util/small_object_allocator.cpp
+++ b/src/util/small_object_allocator.cpp
@@ -27,6 +27,7 @@ small_object_allocator::~small_object_allocator() {
         while (c) {
             chunk * next = c->m_next;
             delete c;
+            lean_report_memory_deallocated(sizeof(chunk));
             c = next;
         }
     }
@@ -44,6 +45,7 @@ void small_object_allocator::reset() {
         while (c) {
             chunk * next = c->m_next;
             delete c;
+            lean_report_memory_deallocated(sizeof(chunk));
             c = next;
         }
         m_chunks[i] = 0;
@@ -193,6 +195,7 @@ void small_object_allocator::consolidate() {
             }
             if (num_free_in_chunk == num_objs_per_chunk) {
                 delete curr_chunk;
+                lean_report_memory_deallocated(sizeof(chunk));
             } else {
                 curr_chunk->m_next = last_chunk;
                 last_chunk = curr_chunk;