diff --git a/src/util/lean_obj.cpp b/src/util/lean_obj.cpp
index ecbe857bdd..7fdf64b905 100644
--- a/src/util/lean_obj.cpp
+++ b/src/util/lean_obj.cpp
@@ -37,11 +37,15 @@ size_t obj_header_size(lean_obj * o) {
 /* We use the field m_rc to implement a linked list of lean objects to be deleted.
    This hack is safe because m_rc has type uintptr_t. */
 
+static_assert(sizeof(atomic<rc_type>) == sizeof(lean_obj*),  "unexpected atomic<rc_type> size, the object GC assumes these two types have the same size");
+
 inline lean_obj * get_next(lean_obj * o) {
+    static_assert(o == static_cast<void*>(&(o->m_rc)), "the object GC relies on the fact that the first field of a structure is stored at offset 0");
     return *reinterpret_cast<lean_obj**>(o);
 }
 
 inline void set_next(lean_obj * o, lean_obj * n) {
+    static_assert(o == static_cast<void*>(&(o->m_rc)), "the object GC relies on the fact that the first field of a structure is stored at offset 0");
     *reinterpret_cast<lean_obj**>(o) = n;
 }
 
diff --git a/src/util/lean_obj.h b/src/util/lean_obj.h
index 9c23610799..7c7f923d14 100644
--- a/src/util/lean_obj.h
+++ b/src/util/lean_obj.h
@@ -189,7 +189,13 @@ inline lean_obj * alloc_mpz(mpz const & m) {
     return new lean_mpz(m);
 }
 
-/* The memory associated with all Lean objects but mpz and external can be deallocated using `free`. */
+/* The memory associated with all Lean objects but `lean_mpz` and `lean_external` can be deallocated using `free`.
+   All fields in these objects are integral types, but `std::atomic<uintptr_t> m_rc`.
+   However, `std::atomic<Integral>` has a trivial destructor.
+   In the C++ reference manual (http://en.cppreference.com/w/cpp/atomic/atomic), we find the following sentence:
+
+   "Additionally, the resulting std::atomic<Integral> specialization has standard layout, a trivial default constructor,
+   and a trivial destructor." */
 inline void dealloc_mpz(lean_obj * o) { delete to_mpz(o); }
 inline void dealloc_external(lean_obj * o) { delete to_external(o); }