diff --git a/src/smt/smt_lookahead.cpp b/src/smt/smt_lookahead.cpp
index 221c2d0ea..eb4f96320 100644
--- a/src/smt/smt_lookahead.cpp
+++ b/src/smt/smt_lookahead.cpp
@@ -72,9 +72,14 @@ namespace smt {
         svector<bool_var> vars;
         for (bool_var v = 0; v < static_cast<bool_var>(sz); ++v) {
             expr* b = ctx.bool_var2expr(v);
-            if (b && ctx.get_assignment(v) == l_undef) {
-                vars.push_back(v);
-            }
+            if (!b)
+                continue;
+            if (ctx.get_assignment(v) != l_undef)
+                continue;
+            if (m.is_and(b) || m.is_or(b) || m.is_not(b) || m.is_ite(b) || m.is_implies(b) || m.is_iff(b) || m.is_xor(b))
+                continue; // do not choose connectives
+            vars.push_back(v);
+            
         }
         compare comp(ctx);
         std::sort(vars.begin(), vars.end(), comp);
diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp
index c8958c61c..b3951ce62 100644
--- a/src/smt/smt_parallel.cpp
+++ b/src/smt/smt_parallel.cpp
@@ -77,13 +77,16 @@ namespace smt {
             throw default_exception("trace streams have to be off in parallel mode");
 
         
+        params_ref params = ctx.get_params();
         for (unsigned i = 0; i < num_threads; ++i) {
             smt_params.push_back(ctx.get_fparams());
+            smt_params.back().m_preprocess = false;
         }
+                    
         for (unsigned i = 0; i < num_threads; ++i) {
             ast_manager* new_m = alloc(ast_manager, m, true);
             pms.push_back(new_m);
-            pctxs.push_back(alloc(context, *new_m, smt_params[i], ctx.get_params())); 
+            pctxs.push_back(alloc(context, *new_m, smt_params[i], params)); 
             context& new_ctx = *pctxs.back();
             context::copy(ctx, new_ctx, true);
             new_ctx.set_random_seed(i + ctx.get_fparams().m_random_seed);
@@ -108,6 +111,7 @@ namespace smt {
         for (unsigned i = 0; i < num_threads; ++i) unit_lim.push_back(0);
 
         std::function<void(void)> collect_units = [&,this]() {
+            //return; -- has overhead
             for (unsigned i = 0; i < num_threads; ++i) {
                 context& pctx = *pctxs[i];
                 pctx.pop_to_base_lvl();