diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp
index e0cf84dc1..b6eb94448 100644
--- a/src/smt/smt_parallel.cpp
+++ b/src/smt/smt_parallel.cpp
@@ -991,6 +991,8 @@ namespace smt {
         // auto candidates = ctx->m_pq_scores.get_heap();
         std::vector<std::pair<double, expr*>> top_k; // will hold at most k elements
 
+        ctx->pop_to_search_lvl();
+
         for (bool_var v = 0; v < ctx->get_num_bool_vars(); ++v) {
             if (ctx->get_assignment(v) != l_undef)
                 continue;
diff --git a/src/smt/smt_parallel2.cpp b/src/smt/smt_parallel2.cpp
index 4404387d2..ad0f89d36 100644
--- a/src/smt/smt_parallel2.cpp
+++ b/src/smt/smt_parallel2.cpp
@@ -62,6 +62,7 @@ namespace smt {
 #include <mutex>
 #include <condition_variable>
 
+#define SHARE_SEARCH_TREE 1
 
 #define LOG_WORKER(lvl, s) IF_VERBOSE(lvl, verbose_stream() << "Worker " << id << s)
 
@@ -73,9 +74,9 @@ namespace smt {
         search_tree::node<cube_config>* node = nullptr;
         expr_ref_vector cube(m);
         while (true) { 
-            collect_shared_clauses(m_g2l);
 
-#if 0
+
+#if SHARE_SEARCH_TREE
             if (!b.get_cube(m_g2l, id, cube, node)) {
                 LOG_WORKER(1, " no more cubes\n");
                 return;
@@ -84,6 +85,7 @@ namespace smt {
             if (!get_cube(cube, node))
                 return;
 #endif
+            collect_shared_clauses(m_g2l);
 
         check_cube_start:
             LOG_WORKER(1, " CUBE SIZE IN MAIN LOOP: " << cube.size() << "\n");
@@ -101,10 +103,13 @@ namespace smt {
                     // return unprocessed cubes to the batch manager
                     // add a split literal to the batch manager.
                     // optionally process other cubes and delay sending back unprocessed cubes to batch manager.
+                    if (m_config.m_max_cube_depth <= cube.size()) 
+                        goto check_cube_start;
+
                     auto atom = get_split_atom();
                     if (!atom)
                         goto check_cube_start;
-#if 0
+#if SHARE_SEARCH_TREE
                     b.split(m_l2g, id, node, atom);
 #else
                     split(node, atom);
@@ -133,7 +138,7 @@ namespace smt {
                             b.report_assumption_used(m_l2g, e); // report assumptions used in unsat core, so they can be used in final core
 
                     LOG_WORKER(1, " found unsat cube\n");    
-#if 0
+#if SHARE_SEARCH_TREE
                     b.backtrack(m_l2g, unsat_core, node);
 #else
                     backtrack(unsat_core, node);
@@ -208,6 +213,7 @@ namespace smt {
         m_config.m_beam_search = pp.beam_search();
         m_config.m_explicit_hardness = pp.explicit_hardness();
         m_config.m_cubetree = pp.cubetree();
+        m_config.m_max_cube_depth = pp.max_cube_depth();
 
         // don't share initial units
         ctx->pop_to_base_lvl();
diff --git a/src/smt/smt_parallel2.h b/src/smt/smt_parallel2.h
index 1d387ea82..59605f331 100644
--- a/src/smt/smt_parallel2.h
+++ b/src/smt/smt_parallel2.h
@@ -130,6 +130,7 @@ namespace smt {
                 bool m_cube_initial_only = false;
                 unsigned m_max_greedy_cubes = 1000;
                 unsigned m_num_split_lits = 2;
+                unsigned m_max_cube_depth = 20;
                 bool m_backbone_detection = false;
                 bool m_iterative_deepening = false;
                 bool m_beam_search = false;