diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp
index 2119ae8b9..d79067bb1 100644
--- a/src/smt/smt_parallel.cpp
+++ b/src/smt/smt_parallel.cpp
@@ -675,14 +675,7 @@ namespace smt {
 
         LOG_BB_WORKER(1, " RESULT: " << r << " FOR CANDIDATE: " << mk_bounded_pp(bb_candidate, m, 3) << "\n");
 
-        if (r == l_false) {
-            auto core = ctx->unsat_core();
-            if (core.size() == 1) {
-                return true;
-            }                
-        }
-
-        return false;
+        return r == l_false && ctx->unsat_core().size() == 1;
     }
 
     void parallel::worker::share_units() {
@@ -1315,8 +1308,7 @@ namespace smt {
         m_batch_manager.initialize(num_global_bb_threads);
         
         // Launch threads
-        vector<std::thread> threads;
-        threads.resize(total_threads);
+        vector<std::thread> threads(total_threads);
         unsigned thread_idx = 0;
         for (auto* w : m_workers) 
             threads[thread_idx++] = std::thread([&, w]() { w->run(); });                
diff --git a/src/smt/smt_parallel.h b/src/smt/smt_parallel.h
index abf098de9..f895cb179 100644
--- a/src/smt/smt_parallel.h
+++ b/src/smt/smt_parallel.h
@@ -234,8 +234,9 @@ namespace smt {
             void share_units();
 
             void update_max_thread_conflicts() {
+                // allow for backoff scheme of conflicts within the thread for cube timeouts.
                 m_config.m_threads_max_conflicts = (unsigned)(m_config.m_max_conflict_mul * m_config.m_threads_max_conflicts);
-            } // allow for backoff scheme of conflicts within the thread for cube timeouts.
+            }
 
             void simplify();
             bb_candidates find_backbone_candidates(unsigned k = 10);
diff --git a/src/util/search_tree.h b/src/util/search_tree.h
index fc2337b8a..2c42657d3 100644
--- a/src/util/search_tree.h
+++ b/src/util/search_tree.h
@@ -32,9 +32,9 @@ Author:
 
 --*/
 
+#pragma once
 #include "util/util.h"
 #include "util/vector.h"
-#pragma once
 
 namespace search_tree {
 
@@ -100,7 +100,11 @@ namespace search_tree {
             for (unsigned i = 0; i < indent; ++i)
                 out << " ";
             Config::display_literal(out, m_literal);
-            out << (get_status() == status::open ? " (o)" : get_status() == status::closed ? " (c)" : " (a)");
+            switch (get_status()) {
+            case status::open:   out << " (o)"; break;
+            case status::closed: out << " (c)"; break;
+            case status::active: out << " (a)"; break;
+            }
             out << "\n";
             if (m_left)
                 m_left->display(out, indent + 2);
@@ -528,6 +532,7 @@ namespace search_tree {
             find_nonclosed_nodes_with_literal_rec(m_root.get(), lit, out);
         }
 
+    private:
         void find_nonclosed_nodes_with_literal_rec(node<Config>* n, literal const& lit, ptr_vector<node<Config>>& out) {
             if (!n)
                 return;
@@ -539,6 +544,7 @@ namespace search_tree {
             find_nonclosed_nodes_with_literal_rec(n->right(), lit, out);
         }
 
+    public:
         void dec_active_workers(node<Config>* n) {
             if (!n)
                 return;