diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-11-12 18:13:17 -0500 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-11-12 18:13:17 -0500 |
commit | c8e1acb9d8280ee61919d192d61881348bc36f91 (patch) | |
tree | 9789cdf340304a000441fefd72cb4e3ab4e3833e /src/main | |
parent | 362114a95855497568694c59cb0f5a72d2c30d29 (diff) |
Minor portfolio fixes for some platforms.
Diffstat (limited to 'src/main')
-rw-r--r-- | src/main/command_executor_portfolio.cpp | 3 | ||||
-rw-r--r-- | src/main/portfolio.cpp | 14 |
2 files changed, 12 insertions, 5 deletions
diff --git a/src/main/command_executor_portfolio.cpp b/src/main/command_executor_portfolio.cpp index e58df5699..971aa2131 100644 --- a/src/main/command_executor_portfolio.cpp +++ b/src/main/command_executor_portfolio.cpp @@ -270,7 +270,7 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd) lemmaSharingInit(); /* Portfolio */ - boost::function<bool()> fns[d_numThreads]; + boost::function<bool()>* fns = new boost::function<bool()>[d_numThreads]; for(unsigned i = 0; i < d_numThreads; ++i) { fns[i] = boost::bind(smtEngineInvoke, d_smts[i], @@ -326,6 +326,7 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd) /* cleanup this check sat specific stuff */ lemmaSharingCleanup(); + delete[] fns; return portfolioReturn.second; } else if(mode == 2) { Command* cmdExported = diff --git a/src/main/portfolio.cpp b/src/main/portfolio.cpp index cf8bba1ba..56a05795a 100644 --- a/src/main/portfolio.cpp +++ b/src/main/portfolio.cpp @@ -62,8 +62,8 @@ std::pair<int, S> runPortfolio(int numThreads, boost::function<S()> threadFns[], bool optionWaitToJoin) { boost::thread thread_driver; - boost::thread threads[numThreads]; - S threads_returnValue[numThreads]; + boost::thread* threads = new boost::thread[numThreads]; + S* threads_returnValue = new S[numThreads]; global_flag_done = false; global_winner = -1; @@ -78,8 +78,9 @@ std::pair<int, S> runPortfolio(int numThreads, thread_driver = boost::thread(driverFn); boost::unique_lock<boost::mutex> lock(mutex_main_wait); - while(global_flag_done == false) + while(global_flag_done == false) { condition_var_main_wait.wait(lock); + } if(not driverFn.empty()) { thread_driver.interrupt(); @@ -92,7 +93,12 @@ std::pair<int, S> runPortfolio(int numThreads, } } - return std::pair<int, S>(global_winner,threads_returnValue[global_winner]); + std::pair<int, S> retval(global_winner, threads_returnValue[global_winner]); + + delete[] threads; + delete[] threads_returnValue; + + return retval; } // instantiation |