diff --git a/src/include/lean/lean.h b/src/include/lean/lean.h
index 609a7b95b1..4bebcc80d4 100644
--- a/src/include/lean/lean.h
+++ b/src/include/lean/lean.h
@@ -116,7 +116,8 @@ reference counting is not needed (== 0). We don't use reference counting for obj
 marked as persistent.
 
 For "small" objects stored in compact regions, the field `m_cs_sz` contains the object size. For "small" objects not
-stored in compact regions, we use the page information to retrieve its size.
+stored in compact regions, we use the page information to retrieve its size. This is not an option
+with mimalloc, so there we always use `m_cs_sz` (TODO: do everywhere?).
 
 During deallocation and 64-bit machines, the fields `m_rc` and `m_cs_sz` store the next object in the deletion TODO list.
 These two fields together have 48-bits, and this is enough for modern computers.
@@ -351,14 +352,18 @@ static inline lean_object * lean_alloc_small_object(unsigned sz) {
 #ifdef LEAN_MIMALLOC
     // HACK: emulate behavior of small allocator to avoid `leangz` breakage for now
     sz = lean_align(sz, LEAN_OBJECT_SIZE_DELTA);
-    void * mem = mi_malloc_small(sizeof(size_t) + sz);
+    void * mem = mi_malloc_small(sz);
+    if (mem == 0) lean_internal_panic_out_of_memory();
+    lean_object * o = (lean_object*)mem;
+    o->m_cs_sz = sz;
+    return o;
 #else
     void * mem = malloc(sizeof(size_t) + sz);
-#endif
     if (mem == 0) lean_internal_panic_out_of_memory();
     *(size_t*)mem = sz;
     return (lean_object*)((size_t*)mem + 1);
 #endif
+#endif
 }
 
 static inline lean_object * lean_alloc_ctor_memory(unsigned sz) {
@@ -397,6 +402,8 @@ static inline lean_object * lean_alloc_ctor_memory(unsigned sz) {
 static inline unsigned lean_small_object_size(lean_object * o) {
 #ifdef LEAN_SMALL_ALLOCATOR
     return lean_small_mem_size(o);
+#elif defined(LEAN_MIMALLOC)
+    return o->m_cs_sz;
 #else
     return *((size_t*)o - 1);
 #endif
@@ -414,8 +421,7 @@ static inline void lean_free_small_object(lean_object * o) {
 #ifdef LEAN_SMALL_ALLOCATOR
     lean_free_small(o);
 #elif defined(LEAN_MIMALLOC)
-    size_t* ptr = (size_t*)o - 1;
-    mi_free_size(ptr, *ptr + sizeof(size_t));
+    mi_free_size((void *)o, o->m_cs_sz);
 #else
     size_t* ptr = (size_t*)o - 1;
     free_sized(ptr, *ptr + sizeof(size_t));
@@ -554,7 +560,10 @@ static inline void lean_set_st_header(lean_object * o, unsigned tag, unsigned ot
     o->m_rc       = 1;
     o->m_tag      = tag;
     o->m_other    = other;
-    o->m_cs_sz    = 0;
+#ifndef LEAN_MIMALLOC
+    // already initialized by `lean_alloc(_small)_object` when using mimalloc
+     o->m_cs_sz    = 0;
+#endif
 }
 
 /* Remark: we don't need a reference counter for objects that are not stored in the heap.
diff --git a/src/runtime/object.cpp b/src/runtime/object.cpp
index a2299468e4..daf02a9e7d 100644
--- a/src/runtime/object.cpp
+++ b/src/runtime/object.cpp
@@ -299,7 +299,10 @@ extern "C" LEAN_EXPORT lean_object * lean_alloc_object(size_t sz) {
 #elif defined(LEAN_MIMALLOC)
     void * r = mi_malloc(sz);
     if (r == nullptr) lean_internal_panic_out_of_memory();
-    return (lean_object*)r;
+    lean_object * o = (lean_object*)r;
+    // not a small object
+    o->m_cs_sz = 0;
+    return o;
 #else
     void * r = malloc(sz);
     if (r == nullptr) lean_internal_panic_out_of_memory();
@@ -1207,7 +1210,14 @@ void deactivate_promise(lean_promise_object * promise) {
 
 object * alloc_mpz(mpz const & m) {
     void * mem = lean_alloc_small_object(sizeof(mpz_object));
+#ifdef LEAN_MIMALLOC
+    // placement new is not guaranteed to preserve this field so store and restore it
+    unsigned sz = ((lean_object *)mem)->m_cs_sz;
+#endif
     mpz_object * o = new (mem) mpz_object(m);
+#ifdef LEAN_MIMALLOC
+    o->m_header.m_cs_sz = sz;
+#endif
     lean_set_st_header((lean_object*)o, LeanMPZ, 0);
     return (lean_object*)o;
 }