diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp
index b610043a0..ece523a51 100644
--- a/src/smt/smt_parallel.cpp
+++ b/src/smt/smt_parallel.cpp
@@ -569,16 +569,6 @@ namespace smt {
     void parallel::batch_manager::initialize() {
         m_state = state::is_running; 
         m_search_tree.reset();
-        #if 0
-        smt_parallel_params sp(p.ctx.m_params);
-        m_config.m_max_cube_depth = sp.max_cube_depth();
-        m_config.m_frugal_cube_only = sp.frugal_cube_only();
-        m_config.m_never_cube = sp.never_cube();
-        m_config.m_depth_splitting_only = sp.depth_splitting_only();
-        m_config.m_iterative_deepening = sp.iterative_deepening();
-        m_config.m_beam_search = sp.beam_search();
-        m_config.m_cubetree = sp.cubetree();
-        #endif
     }
 
     void parallel::batch_manager::collect_statistics(::statistics& st) const {
@@ -595,19 +585,25 @@ namespace smt {
         struct scoped_clear {
             parallel& p;
             scoped_clear(parallel& p) : p(p) {}
-            ~scoped_clear() { p.m_workers.reset(); p.m_assumptions_used.reset(); }
+            ~scoped_clear() { 
+                p.m_workers.reset(); 
+                p.m_assumptions_used.reset(); 
+                p.m_assumptions.reset();
+            }
         };
         scoped_clear clear(*this);
 
         {
             m_batch_manager.initialize();
             m_workers.reset();
+            for (auto e : asms) 
+                m_assumptions.insert(e);
             scoped_limits sl(m.limit());
             flet<unsigned> _nt(ctx.m_fparams.m_threads, 1);
             SASSERT(num_threads > 1);
             for (unsigned i = 0; i < num_threads; ++i)
-                m_workers.push_back(alloc(worker, i, *this, asms)); // i.e. "new worker(i, *this, asms)"
-                
+                m_workers.push_back(alloc(worker, i, *this, asms)); 
+
             for (auto w : m_workers)
                 sl.push_child(&(w->limit()));
 
diff --git a/src/smt/smt_parallel.h b/src/smt/smt_parallel.h
index dcd988653..16532e668 100644
--- a/src/smt/smt_parallel.h
+++ b/src/smt/smt_parallel.h
@@ -21,9 +21,7 @@ Revision History:
 #include "smt/smt_context.h"
 #include "util/search_tree.h"
 #include <thread>
-#include <condition_variable>
 #include <mutex>
-#include <condition_variable>
 
 
 namespace smt {
@@ -51,15 +49,6 @@ namespace smt {
                 is_exception_msg,
                 is_exception_code
             };
-            struct config {
-                unsigned m_max_cube_depth = 20;
-                bool m_frugal_cube_only = false;
-                bool m_never_cube = false; 
-                bool m_depth_splitting_only = false;
-                bool m_iterative_deepening = false;
-                bool m_beam_search = false;
-                bool m_cubetree = false;
-            };
             struct stats {
                 unsigned m_max_cube_depth = 0;
                 unsigned m_num_cubes = 0;
@@ -70,7 +59,6 @@ namespace smt {
             parallel& p;
             std::mutex mux;
             state m_state = state::is_running;
-            config m_config;
             stats m_stats;
             using node = search_tree::node<cube_config>;
             search_tree::tree<cube_config> m_search_tree;
@@ -90,7 +78,7 @@ namespace smt {
             void init_parameters_state();
 
             bool is_assumption(expr* e) const {
-                return false; // m_assumptions_used.contains(e);
+                return p.m_assumptions.contains(e);
             }
 
         public:
@@ -120,22 +108,14 @@ namespace smt {
                 unsigned m_threads_max_conflicts = 1000;
                 unsigned m_max_conflicts = 10000000;
                 bool m_relevant_units_only = true;
-                bool m_never_cube = false;
                 bool m_share_conflicts = true;
                 bool m_share_units = true;
                 double m_max_conflict_mul = 1.5;
-                bool m_share_units_initial_only = false;
-                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;
-                bool m_explicit_hardness = false;
-                bool m_cubetree = false;
-                bool m_inprocessing = false;
+                bool m_share_units_initial_only = true;
+                bool m_cube_initial_only = true;
+                bool m_inprocessing = true;
                 unsigned m_inprocessing_delay = 0;
+                unsigned m_max_cube_depth = 20;
             };
 
             using node = search_tree::node<cube_config>;
@@ -187,6 +167,7 @@ namespace smt {
         };
 
         obj_hashtable<expr> m_assumptions_used; // assumptions used in unsat cores, to be used in final core
+        obj_hashtable<expr> m_assumptions;       // all assumptions
         batch_manager m_batch_manager;
         scoped_ptr_vector<worker> m_workers;