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/command_executor_portfolio.cpp | |
parent | 362114a95855497568694c59cb0f5a72d2c30d29 (diff) |
Minor portfolio fixes for some platforms.
Diffstat (limited to 'src/main/command_executor_portfolio.cpp')
-rw-r--r-- | src/main/command_executor_portfolio.cpp | 3 |
1 files changed, 2 insertions, 1 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 = |