From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Wed, 11 Jun 2014 22:33:52 +0000 (-0400)
Subject: Fix for competition mode + parallel.
X-Git-Tag: cvc5-1.0.0~6829^2~5
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=bc2d62fd104deaaff3474385ef76b5c057192da1;p=cvc5.git

Fix for competition mode + parallel.
---

diff --git a/src/main/command_executor_portfolio.cpp b/src/main/command_executor_portfolio.cpp
index 9de3b2134..fa1d8c7f5 100644
--- a/src/main/command_executor_portfolio.cpp
+++ b/src/main/command_executor_portfolio.cpp
@@ -30,6 +30,12 @@
 #include "options/options.h"
 #include "smt/options.h"
 
+#include "cvc4autoconfig.h"
+
+#if HAVE_UNISTD_H
+#  include <unistd.h>
+#endif /* HAVE_UNISTD_H */
+
 using namespace std;
 
 namespace CVC4 {
@@ -302,8 +308,10 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd)
         runPortfolio(d_numThreads, smFn, fns,
                      d_options[options::waitToJoin], d_statWaitTime);
 
+#ifdef CVC4_STATISTICS_ON
     assert( d_statWaitTime.running() );
     d_statWaitTime.stop();
+#endif /* CVC4_STATISTICS_ON */
 
     delete d_seq;
     d_seq = new CommandSequence();
@@ -330,6 +338,12 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd)
 
       *d_options[options::out]
         << d_ostringstreams[portfolioReturn.first]->str();
+
+#ifdef CVC4_COMPETITION_MODE
+      // There's some hang-up in thread destruction?
+      // Anyway for SMT-COMP we don't care, just exit now.
+      _exit(0);
+#endif /* CVC4_COMPETITION_MODE */
     }
 
     /* cleanup this check sat specific stuff */