From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Tue, 12 Nov 2013 23:13:17 +0000 (-0500)
Subject: Minor portfolio fixes for some platforms.
X-Git-Tag: cvc5-1.0.0~7257
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c8e1acb9d8280ee61919d192d61881348bc36f91;p=cvc5.git

Minor portfolio fixes for some platforms.
---

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