MacOS has even stricter stack limits in catalina.

Invoking sby in macOS Catalina fails because of bizarre stack limits in Catalina.

diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py
index 9f7c8c6d98fa868fa9cb742fa2e6b8aa82c378d0..9d03e162eec74f152da4ce45fdc1a27d49bc6b59 100644 (file)
--- a/backends/smt2/smtio.py
+++ b/backends/smt2/smtio.py
@@ -39,7 +39,7 @@ if os.name == "posix":
         smtio_stacksize = 128 * 1024 * 1024
         if os.uname().sysname == "Darwin":
             # MacOS has rather conservative stack limits
-            smtio_stacksize = 16 * 1024 * 1024
+            smtio_stacksize = 16 * 1024 * 512
         if current_rlimit_stack[1] != resource.RLIM_INFINITY:
             smtio_stacksize = min(smtio_stacksize, current_rlimit_stack[1])
         if current_rlimit_stack[0] < smtio_stacksize: