[Solver] Tune down the shared memory region size on Darwin.

 - See comment, this is a gross workaround for Darwin's very small default limit
   on shared memory size. I'm not sure how big of a counterexample users can
   actually expect STP to solve in practice -- if there is a practical use for
   larger ones it would probably be good for us to write a fallback strategy.

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);