Merge remote-tracking branch 'origin/master' into segfaultfix

1 files changed, 19 insertions, 3 deletions

diff --git a/src/main/portfolio.cpp b/src/main/portfolio.cpp
index 8bfbeff7c..abe27eb06 100644
--- a/src/main/portfolio.cpp
+++ b/src/main/portfolio.cpp
@@ -5,7 +5,7 @@
  ** Major contributors: Kshitij Bansal
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
@@ -63,6 +63,7 @@ template<typename T, typename S>
 std::pair<int, S> runPortfolio(int numThreads,
                                boost::function<T()> driverFn,
                                boost::function<S()> threadFns[],
+                               size_t stackSize,
                                bool optionWaitToJoin,
                                TimerStat& statWaitTime) {
   boost::thread thread_driver;
@@ -74,13 +75,27 @@ std::pair<int, S> runPortfolio(int numThreads,
 
   for(int t = 0; t < numThreads; ++t) {
 
+#if BOOST_HAS_THREAD_ATTR
     boost::thread::attributes attrs;
-    attrs.set_stack_size(256 * 1024 * 1024);
 
-    threads[t] = 
+    if(stackSize > 0) {
+      attrs.set_stack_size(stackSize);
+    }
+
+    threads[t] =
       boost::thread(attrs, boost::bind(runThread<S>, t, threadFns[t],
+                                       boost::ref(threads_returnValue[t]) ) );
+#else /* BOOST_HAS_THREAD_ATTR */
+    if(stackSize > 0) {
+      throw OptionException("cannot specify a stack size for worker threads; requires CVC4 to be built with Boost thread library >= 1.50.0");
+    }
+
+    threads[t] =
+      boost::thread(boost::bind(runThread<S>, t, threadFns[t],
                                 boost::ref(threads_returnValue[t]) ) );
 
+#endif /* BOOST_HAS_THREAD_ATTR */
+
     if(Chat.isOn()) {
       void *stackaddr;
       size_t stacksize;
@@ -126,6 +141,7 @@ std::pair<int, bool>
 runPortfolio<void, bool>(int,
                          boost::function<void()>, 
                          boost::function<bool()>*,
+                         size_t,
                          bool,
                          TimerStat&);