From c8c02060ee6b7394f8a492b34fdd20f9ca6406ab Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 18 May 2020 15:01:27 -0700
Subject: [PATCH] another module level ifdef for #4382

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/seq_decl_plugin.cpp    | 2 +-
 src/smt/seq_unicode.cpp        | 2 +-
 src/smt/seq_unicode.h          | 3 +--
 src/solver/parallel_tactic.cpp | 9 +++++++++
 4 files changed, 12 insertions(+), 4 deletions(-)

diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp
index 356d77dde..23eaaa17c 100644
--- a/src/ast/seq_decl_plugin.cpp
+++ b/src/ast/seq_decl_plugin.cpp
@@ -569,7 +569,6 @@ void seq_decl_plugin::init() {
     sort* str2TintT[3] = { strT, strT, intT };
     sort* seqAintT[2] = { seqA, intT };
     sort* seq3A[3] = { seqA, seqA, seqA };
-    sort* charTcharT[2] = { m_char, m_char };
     m_sigs.resize(LAST_SEQ_OP);
     // TBD: have (par ..) construct and load parameterized signature from premable.
     m_sigs[OP_SEQ_UNIT]      = alloc(psig, m, "seq.unit",     1, 1, &A, seqA);
@@ -609,6 +608,7 @@ void seq_decl_plugin::init() {
     m_sigs[OP_STRING_CONST]      = nullptr;
 #if _USE_UNICODE
     m_sigs[OP_CHAR_CONST]        = nullptr;
+    sort* charTcharT[2] = { m_char, m_char };
     m_sigs[OP_CHAR_LE]           = alloc(psig, m, "char.<=", 0, 2, charTcharT, boolT);
 #endif
     m_sigs[_OP_STRING_STRIDOF]   = alloc(psig, m, "str.indexof", 0, 3, str2TintT, intT);
diff --git a/src/smt/seq_unicode.cpp b/src/smt/seq_unicode.cpp
index 0a947b1c6..8077a968b 100644
--- a/src/smt/seq_unicode.cpp
+++ b/src/smt/seq_unicode.cpp
@@ -28,7 +28,7 @@ namespace smt {
         seq(m),
         dl(),
         m_qhead(0),
-        m_nc_functor(*this),
+        m_nc_functor(),
         m_var_value_hash(*this),
         m_var_value_eq(*this),
         m_var_value_table(DEFAULT_HASHTABLE_INITIAL_CAPACITY, m_var_value_hash, m_var_value_eq)
diff --git a/src/smt/seq_unicode.h b/src/smt/seq_unicode.h
index 91578d3a6..53a183e38 100644
--- a/src/smt/seq_unicode.h
+++ b/src/smt/seq_unicode.h
@@ -35,9 +35,8 @@ namespace smt {
 
         class nc_functor {
             literal_vector m_literals;
-            seq_unicode& m_super;
         public:
-            nc_functor(seq_unicode& s): m_super(s) {}
+            nc_functor() {}
             void operator()(literal const& l) {
                 if (l != null_literal) m_literals.push_back(l);
             }
diff --git a/src/solver/parallel_tactic.cpp b/src/solver/parallel_tactic.cpp
index 3520fc8cd..564788194 100644
--- a/src/solver/parallel_tactic.cpp
+++ b/src/solver/parallel_tactic.cpp
@@ -28,6 +28,14 @@ Notes:
  
 --*/
 
+#ifdef SINGLE_THREAD
+
+tactic * mk_parallel_tactic(solver* s, params_ref const& p) {
+    throw default_exception("parallel tactic is disabled in single threaded mode");
+}
+
+#else
+
 #include <thread>
 #include <mutex>
 #include <cmath>
@@ -795,3 +803,4 @@ tactic * mk_parallel_tactic(solver* s, params_ref const& p) {
     return alloc(parallel_tactic, s, p);
 }
 
+#endif