diff --git a/src/tests/util/stackinfo.cpp b/src/tests/util/stackinfo.cpp
index 8c6bc2de8..1e8149414 100644
--- a/src/tests/util/stackinfo.cpp
+++ b/src/tests/util/stackinfo.cpp
@@ -10,8 +10,16 @@ Author: Leonardo de Moura
 using namespace lean;
 
 static char foo(int i) {
-    #define SZ 1000000
-    char buffer[SZ];
+    #define SZ_FOO 1000000
+    char buffer[SZ_FOO];
+    buffer[i] = i;
+    std::cout << get_available_stack_size() << "\n";
+    return buffer[i];
+}
+
+static char bar(int i) {
+    #define SZ_BAR 10000
+    char buffer[SZ_BAR];
     buffer[i] = i;
     std::cout << get_available_stack_size() << "\n";
     return buffer[i];
@@ -23,8 +31,16 @@ static void tst1() {
     std::cout << get_available_stack_size() << "\n";
 }
 
+static void tst2() {
+    std::cout << get_available_stack_size() << "\n";
+    bar(10);
+    std::cout << get_available_stack_size() << "\n";
+}
+
 int main() {
     save_stack_info();
     tst1();
+    save_stack_info();
+    tst2();
     return has_violations() ? 1 : 0;
 }
diff --git a/src/util/stackinfo.cpp b/src/util/stackinfo.cpp
index 85ebd76a6..a77e91830 100644
--- a/src/util/stackinfo.cpp
+++ b/src/util/stackinfo.cpp
@@ -16,6 +16,19 @@ namespace lean {
 size_t get_stack_size() {
     return LEAN_WIN_STACK_SIZE
 }
+#endif
+#ifdef __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) {
+        // pthread_attr_getstacksize is supposed to return 0
+        throw stack_space_exception();
+    }
+    return result;
+}
 #else
 size_t get_stack_size() {
     pthread_attr_t attr;