Use conservative stack size for SMT2 on MacOS

diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py
index 3fc823e3ed89b0b832d277fa6af8d3315e320389..e8ed5e63bc65541807fcac24e885d4eb37bf2786 100644 (file)
--- a/backends/smt2/smtio.py
+++ b/backends/smt2/smtio.py
@@ -32,10 +32,15 @@ from threading import Thread
 if os.name == "posix":
     smtio_reclimit = 64 * 1024
     smtio_stacksize = 128 * 1024 * 1024
+    smtio_stacklimit = resource.RLIM_INFINITY
+    if os.uname().sysname == "Darwin":
+        # MacOS has rather conservative stack limits
+        smtio_stacksize = 16 * 1024 * 1024
+        smtio_stacklimit = resource.getrlimit(resource.RLIMIT_STACK)[1]
     if sys.getrecursionlimit() < smtio_reclimit:
         sys.setrecursionlimit(smtio_reclimit)
     if resource.getrlimit(resource.RLIMIT_STACK)[0] < smtio_stacksize:
-        resource.setrlimit(resource.RLIMIT_STACK, (smtio_stacksize, -1))
+        resource.setrlimit(resource.RLIMIT_STACK, (smtio_stacksize, smtio_stacklimit))
 
 
 # currently running solvers (so we can kill them)