diff --git a/src/util/interrupt.h b/src/util/interrupt.h
index c916b930b1..eb32d88b43 100644
--- a/src/util/interrupt.h
+++ b/src/util/interrupt.h
@@ -71,7 +71,7 @@ public:
         m_thread(
             [&](Function&& fun, Args&&... args) {
                 m_flag_addr.store(get_flag_addr());
-                save_stack_info();
+                save_stack_info(false);
                 fun(std::forward<Args>(args)...);
                 m_flag_addr.store(&m_dummy_addr); // see comment before m_dummy_addr
             },
diff --git a/src/util/stackinfo.cpp b/src/util/stackinfo.cpp
index d7891216b7..be36c2904d 100644
--- a/src/util/stackinfo.cpp
+++ b/src/util/stackinfo.cpp
@@ -17,22 +17,34 @@ void throw_get_stack_size_failed() {
 }
 
 #ifdef LEAN_WINDOWS
-size_t get_stack_size() {
+size_t get_stack_size(int main) {
     return LEAN_WIN_STACK_SIZE;
 }
 #elif defined (__APPLE__)
-size_t get_stack_size() {
-    pthread_attr_t attr;
-    memset (&attr, 0, sizeof(attr));
-    pthread_attr_init(&attr);
-    size_t result;
-    if (pthread_attr_getstacksize(&attr, &result) != 0) {
-        throw_get_stack_size_failed();
+#include <sys/resource.h>
+size_t get_stack_size(int main) {
+    if (main) {
+        // Retrieve stack size of the main thread.
+        struct rlimit curr;
+        if (getrlimit(RLIMIT_STACK, &curr) != 0) {
+            throw_get_stack_size_failed();
+        }
+        return curr.rlim_max;
+    } else {
+        // This branch retrieves the default thread size for pthread threads.
+        // This is *not* the stack size of the main thread.
+        pthread_attr_t attr;
+        memset (&attr, 0, sizeof(attr));
+        pthread_attr_init(&attr);
+        size_t result;
+        if (pthread_attr_getstacksize(&attr, &result) != 0) {
+            throw_get_stack_size_failed();
+        }
+        return result;
     }
-    return result;
 }
 #else
-size_t get_stack_size() {
+size_t get_stack_size(int ) {
     pthread_attr_t attr;
     memset (&attr, 0, sizeof(attr));
     if (pthread_getattr_np(pthread_self(), &attr) != 0) {
@@ -53,8 +65,8 @@ size_t get_stack_size() {
 static thread_local size_t g_stack_size;
 static thread_local size_t g_stack_base;
 
-void save_stack_info() {
-    g_stack_size = get_stack_size();
+void save_stack_info(bool main) {
+    g_stack_size = get_stack_size(main);
     char x;
     g_stack_base = reinterpret_cast<size_t>(&x);
 }
diff --git a/src/util/stackinfo.h b/src/util/stackinfo.h
index 2ccda5fd7b..f2d9f4746d 100644
--- a/src/util/stackinfo.h
+++ b/src/util/stackinfo.h
@@ -6,8 +6,8 @@ Author: Leonardo de Moura
 */
 #pragma once
 namespace lean {
-size_t get_stack_size();
-void save_stack_info();
+size_t get_stack_size(bool main);
+void save_stack_info(bool main = true);
 size_t get_used_stack_size();
 size_t get_available_stack_size();
 /**