From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Wed, 3 Oct 2012 19:05:32 +0000 (+0000)
Subject: --wait-to-join / --no-wait-to-join option
X-Git-Tag: cvc5-1.0.0~7749
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=98db56a7b94d62a1fb0aa3be555fb09b0f98449f;p=cvc5.git

--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.)
---

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