From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Fri, 19 Oct 2012 19:10:42 +0000 (+0000)
Subject: Fix problem with incremental with portfolio. Fixes bug 420.
X-Git-Tag: cvc5-1.0.0~7695
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5796f9398adfab80860f17f4c99f143801689d56;p=cvc5.git

Fix problem with incremental with portfolio. Fixes bug 420.

(this commit was certified error- and warning-free by the test-and-commit script.)
---

diff --git a/src/main/portfolio.cpp b/src/main/portfolio.cpp
index 91037df17..4c542f548 100644
--- a/src/main/portfolio.cpp
+++ b/src/main/portfolio.cpp
@@ -29,8 +29,8 @@ boost::mutex mutex_done;
 boost::mutex mutex_main_wait;
 boost::condition condition_var_main_wait;
 
-bool global_flag_done = false;
-int global_winner = -1;
+bool global_flag_done;
+int global_winner;
 
 template<typename S>
 void runThread(int thread_id, boost::function<S()> threadFn, S& returnValue)
@@ -56,6 +56,9 @@ std::pair<int, S> runPortfolio(int numThreads,
   boost::thread threads[numThreads];
   S threads_returnValue[numThreads];
 
+  global_flag_done = false;
+  global_winner = -1;
+
   for(int t = 0; t < numThreads; ++t) {
     threads[t] = 
       boost::thread(boost::bind(runThread<S>, t, threadFns[t],