diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-06-11 18:33:52 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-06-11 18:41:21 -0400 |
commit | bc2d62fd104deaaff3474385ef76b5c057192da1 (patch) | |
tree | 02f1348d9eeb24e0b2eb997066e6927c6c382e7e /src/main/command_executor_portfolio.cpp | |
parent | c698c4ced6708a2adc422edc9c4e98a84946b4b7 (diff) |
Fix for competition mode + parallel.
Diffstat (limited to 'src/main/command_executor_portfolio.cpp')
-rw-r--r-- | src/main/command_executor_portfolio.cpp | 14 |
1 files changed, 14 insertions, 0 deletions
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 */ |