diff --git a/src/tests/util/CMakeLists.txt b/src/tests/util/CMakeLists.txt
index 28b3e5038..98a14913f 100644
--- a/src/tests/util/CMakeLists.txt
+++ b/src/tests/util/CMakeLists.txt
@@ -31,3 +31,6 @@ add_test(pdeque ${CMAKE_CURRENT_BINARY_DIR}/pdeque)
 add_executable(pvector pvector.cpp)
 target_link_libraries(pvector ${EXTRA_LIBS})
 add_test(pvector ${CMAKE_CURRENT_BINARY_DIR}/pvector)
+add_executable(memory memory.cpp)
+target_link_libraries(memory ${EXTRA_LIBS})
+add_test(memory ${CMAKE_CURRENT_BINARY_DIR}/memory)
diff --git a/src/tests/util/memory.cpp b/src/tests/util/memory.cpp
new file mode 100644
index 000000000..7c57a8c2e
--- /dev/null
+++ b/src/tests/util/memory.cpp
@@ -0,0 +1,35 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include <iostream>
+#include "util/test.h"
+#include "util/memory.cpp"
+
+static void tst1() {
+    std::cout << "Initial: " << lean::get_allocated_memory() << "\n";
+    size_t old_mem = lean::get_allocated_memory();
+    int N = 5;
+    int * a = static_cast<int*>(lean::malloc(N * sizeof(N)));
+    lean_assert(lean::get_allocated_memory() >= old_mem + N * sizeof(N));
+    for (int i = 0; i < N; i++) {
+        a[i] = i;
+    }
+    a = static_cast<int*>(lean::realloc(a, N * 2 * sizeof(N)));
+    lean_assert(lean::get_allocated_memory() >= old_mem + N * 2 * sizeof(N));
+    std::cout << "Total: "  << static_cast<size_t>(lean::get_allocated_memory()) << "\n";
+    std::cout << "Thread: " << static_cast<size_t>(lean::get_thread_allocated_memory()) << "\n";
+    lean_assert(lean::get_allocated_memory() == static_cast<size_t>(lean::get_thread_allocated_memory()));
+    for (int i = 0; i < N; i++) {
+        lean_assert(a[i] == i);
+    }
+    lean::free(a);
+    lean_assert(old_mem == lean::get_allocated_memory());
+}
+
+int main() {
+    tst1();
+    return lean::has_violations() ? 1 : 0;
+}
diff --git a/src/util/memory.cpp b/src/util/memory.cpp
index bc3b07fd7..4dc5713cb 100644
--- a/src/util/memory.cpp
+++ b/src/util/memory.cpp
@@ -88,8 +88,8 @@ void * save_alloc_size(void * ptr, size_t sz) {
     }
 }
 inline size_t malloc_size(void * ptr)             { return static_cast<size_t*>(ptr)[-1]; }
-inline void * malloc_core(size_t sz)              { return save_alloc_size(::malloc(sz + sizeof(size_t)), sz); }
-inline void * realloc_core(void * ptr, size_t sz) { return save_alloc_size(::realloc(static_cast<size_t*>(ptr) - 1, sz + sizeof(size_t)), sz); }
+inline void * malloc_core(size_t sz)              { return save_alloc_size(::malloc(sz + sizeof(sz)), sz); }
+inline void * realloc_core(void * ptr, size_t sz) { return save_alloc_size(::realloc(static_cast<size_t*>(ptr) - 1, sz + sizeof(sz)), sz); }
 inline void   free_core(void * ptr)               { ::free(static_cast<size_t*>(ptr) - 1); }
 }
 #endif