1 files changed, 10 insertions, 1 deletions
diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp
index d4e572cf..3903ab0d 100644
--- a/lib/Solver/Solver.cpp
+++ b/lib/Solver/Solver.cpp
@@ -518,8 +518,17 @@ public:
 };
 
 static unsigned char *shared_memory_ptr;
-static const unsigned shared_memory_size = 1<<20;
 static int shared_memory_id = 0;
+// Darwin by default has a very small limit on the maximum amount of shared
+// memory, which will quickly be exhausted by KLEE running its tests in
+// parallel. For now, we work around this by just requesting a smaller size --
+// in practice users hitting this limit on counterexample sizes probably already
+// are hitting more serious scalability issues.
+#ifdef __APPLE__
+static const unsigned shared_memory_size = 1<<16;
+#else
+static const unsigned shared_memory_size = 1<<20;
+#endif
 
 static void stp_error_handler(const char* err_msg) {
   fprintf(stderr, "error: STP Error: %s\n", err_msg);