diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-06-24 18:44:15 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-06-25 10:44:54 -0400 |
| commit | b4e8ea46bed824f1403b1dddcf56a0e8a56bb380 (patch) | |
| tree | 70ce76501ae9feb98eaf408d0e931e27f6729f18 /src/main/command_executor_portfolio.cpp | |
| parent | 7e5245639848594e5ff72a5104c340defe4aac7c (diff) | |
Stack-size portfolio fix. If using Boost 1.50, --thread-stack=MB is now supported.
Diffstat (limited to 'src/main/command_executor_portfolio.cpp')
| -rw-r--r-- | src/main/command_executor_portfolio.cpp | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/src/main/command_executor_portfolio.cpp b/src/main/command_executor_portfolio.cpp index 1a5d2f8ac..964ce07c1 100644 --- a/src/main/command_executor_portfolio.cpp +++ b/src/main/command_executor_portfolio.cpp @@ -304,8 +304,11 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd) &d_channelsIn[0], &d_smts[0]); + uint64_t threadStackSize = d_options[options::threadStackSize]; + threadStackSize *= 1024 * 1024; + pair<int, bool> portfolioReturn = - runPortfolio(d_numThreads, smFn, fns, + runPortfolio(d_numThreads, smFn, fns, threadStackSize, d_options[options::waitToJoin], d_statWaitTime); #ifdef CVC4_STATISTICS_ON |