From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Thu, 15 Nov 2012 22:39:58 +0000 (+0000)
Subject: some fixes for --threads=1
X-Git-Tag: cvc5-1.0.0~7586
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9d55fef4dfa9d4b98457d36c3ef56b6771d0bd65;p=cvc5.git

some fixes for --threads=1
---

diff --git a/src/main/command_executor_portfolio.cpp b/src/main/command_executor_portfolio.cpp
index a4a0fcad3..d492bf26c 100644
--- a/src/main/command_executor_portfolio.cpp
+++ b/src/main/command_executor_portfolio.cpp
@@ -142,6 +142,9 @@ void CommandExecutorPortfolio::lemmaSharingCleanup()
 {
   assert(d_numThreads == d_options[options::threads]);
 
+  if(d_numThreads == 1)
+    return;
+
   // Channel cleanup
   assert(d_channelsIn.size() == d_numThreads);
   assert(d_channelsOut.size() == d_numThreads);
@@ -248,11 +251,14 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd)
                            );
     }
 
-    assert(d_channelsIn.size() == d_numThreads);
-    assert(d_channelsOut.size() == d_numThreads);
+    assert(d_channelsIn.size() == d_numThreads
+           || d_numThreads == 1);
+    assert(d_channelsOut.size() == d_numThreads
+           || d_numThreads == 1);
     assert(d_smts.size() == d_numThreads);
     boost::function<void()>
-      smFn = boost::bind(sharingManager<ChannelFormat>,
+      smFn = d_numThreads <= 1 ? boost::function<void()>() :
+             boost::bind(sharingManager<ChannelFormat>,
                          d_numThreads,
                          &d_channelsOut[0],
                          &d_channelsIn[0],