diff --git a/src/util/small_object_allocator.cpp b/src/util/small_object_allocator.cpp
index edc3885cd..6ad1af112 100644
--- a/src/util/small_object_allocator.cpp
+++ b/src/util/small_object_allocator.cpp
@@ -77,7 +77,7 @@ void small_object_allocator::deallocate(size_t size, void * p) {
     SASSERT(m_alloc_size >= size);
     SASSERT(p);
     m_alloc_size -= size;
-    if (size > SMALL_OBJ_SIZE - (1 << PTR_ALIGNMENT)) {
+    if (size >= SMALL_OBJ_SIZE - (1 << PTR_ALIGNMENT)) {
         memory::deallocate(p);
         return;
     }
@@ -96,7 +96,7 @@ void * small_object_allocator::allocate(size_t size) {
     return memory::allocate(size);
 #endif
     m_alloc_size += size;
-    if (size > SMALL_OBJ_SIZE - (1 << PTR_ALIGNMENT))
+    if (size >= SMALL_OBJ_SIZE - (1 << PTR_ALIGNMENT))
         return memory::allocate(size);
 #ifdef Z3DEBUG
     size_t osize = size;