diff options
author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2012-10-03 19:05:32 +0000 |
---|---|---|
committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2012-10-03 19:05:32 +0000 |
commit | 98db56a7b94d62a1fb0aa3be555fb09b0f98449f (patch) | |
tree | 3f783ddfc3b17d3ddb992b9ea600729778ab3150 /src | |
parent | f0547f8a6fe9cecefde8b1d0c3dc8fcf50219c6b (diff) |
--wait-to-join / --no-wait-to-join option
workaround option till we fix bug 409. for now, I have kept --wait-to-join to
be default (old behavior). We could technically make --no-wait-to-join the
default when using non-incremental mode, but still possible for problems at
exit I think
(this commit was certified error- and warning-free by the test-and-commit script.)
Diffstat (limited to 'src')
-rw-r--r-- | src/main/command_executor_portfolio.cpp | 4 | ||||
-rw-r--r-- | src/main/options | 3 |
2 files changed, 6 insertions, 1 deletions
diff --git a/src/main/command_executor_portfolio.cpp b/src/main/command_executor_portfolio.cpp index 4867082e6..00527702e 100644 --- a/src/main/command_executor_portfolio.cpp +++ b/src/main/command_executor_portfolio.cpp @@ -262,7 +262,8 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd) &d_smts[0]); pair<int, bool> portfolioReturn = - runPortfolio(d_numThreads, smFn, fns, true); + runPortfolio(d_numThreads, smFn, fns, + d_options[options::waitToJoin]); d_seq = NULL; delete d_seq; @@ -290,6 +291,7 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd) } else { // Unreachable(); assert(false); + return false; } }/* CommandExecutorPortfolio::doCommandSingleton() */ diff --git a/src/main/options b/src/main/options index 02c4643b3..e78acf7d9 100644 --- a/src/main/options +++ b/src/main/options @@ -38,4 +38,7 @@ option separateOutput bool :default false option sharingFilterByLength --filter-lemma-length=N int :default -1 :read-write don't share lemmas strictly longer than N +expert-option waitToJoin --wait-to-join bool :default true + wait for other threads to join before quitting + endmodule |