summaryrefslogtreecommitdiff
path: root/src/main/command_executor_portfolio.cpp
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@cs.nyu.edu>2013-11-12 18:13:17 -0500
committerMorgan Deters <mdeters@cs.nyu.edu>2013-11-12 18:13:17 -0500
commitc8e1acb9d8280ee61919d192d61881348bc36f91 (patch)
tree9789cdf340304a000441fefd72cb4e3ab4e3833e /src/main/command_executor_portfolio.cpp
parent362114a95855497568694c59cb0f5a72d2c30d29 (diff)
Minor portfolio fixes for some platforms.
Diffstat (limited to 'src/main/command_executor_portfolio.cpp')
-rw-r--r--src/main/command_executor_portfolio.cpp3
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 =
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback