diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp
index 0d737500a..d4d1e615f 100644
--- a/src/sat/sat_lookahead.cpp
+++ b/src/sat/sat_lookahead.cpp
@@ -1034,7 +1034,7 @@ namespace sat {
         }
         
         if (m_s.m_ext) {
-            m_ext = m_s.m_ext->copy(this, learned);
+            // m_ext = m_s.m_ext->copy(this, learned);
         }
         propagate();
         m_qhead = m_trail.size();
diff --git a/src/sat/sat_lookahead.h b/src/sat/sat_lookahead.h
index b86b7cb14..3213c5a80 100644
--- a/src/sat/sat_lookahead.h
+++ b/src/sat/sat_lookahead.h
@@ -247,7 +247,7 @@ namespace sat {
         stats                  m_stats;
         model                  m_model; 
         cube_state             m_cube_state;
-        scoped_ptr<extension>  m_ext;
+        //scoped_ptr<extension>  m_ext;
  
         // ---------------------------------------
         // truth values
diff --git a/src/smt/params/smt_params.cpp b/src/smt/params/smt_params.cpp
index a8eb81a2e..3ad20cf90 100644
--- a/src/smt/params/smt_params.cpp
+++ b/src/smt/params/smt_params.cpp
@@ -39,6 +39,7 @@ void smt_params::updt_local_params(params_ref const & _p) {
     m_timeout = p.timeout();
     m_rlimit  = p.rlimit();
     m_max_conflicts = p.max_conflicts();
+    m_restart_max   = p.restart_max();
     m_core_validate = p.core_validate();
     m_logic = _p.get_sym("logic", m_logic);
     m_string_solver = p.string_solver();
diff --git a/src/smt/params/smt_params.h b/src/smt/params/smt_params.h
index b01499c04..32b634626 100644
--- a/src/smt/params/smt_params.h
+++ b/src/smt/params/smt_params.h
@@ -99,6 +99,7 @@ struct smt_params : public preprocessor_params,
     unsigned         m_phase_caching_off;
     bool             m_minimize_lemmas;
     unsigned         m_max_conflicts;
+    unsigned         m_restart_max;
     bool             m_simplify_clauses;
     unsigned         m_tick;
     bool             m_display_features;
diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg
index c6749f678..2f16c5798 100644
--- a/src/smt/params/smt_params_helper.pyg
+++ b/src/smt/params/smt_params_helper.pyg
@@ -21,6 +21,7 @@ def_module_params(module_name='smt',
                           ('timeout', UINT, UINT_MAX, 'timeout (in milliseconds) (UINT_MAX and 0 mean no timeout)'),
                           ('rlimit', UINT, 0, 'resource limit (0 means no limit)'),
                           ('max_conflicts', UINT, UINT_MAX, 'maximum number of conflicts before giving up.'),
+                          ('restart.max', UINT, UINT_MAX, 'maximal number of restarts.'),
                           ('mbqi', BOOL, True, 'model based quantifier instantiation (MBQI)'),
                           ('mbqi.max_cexs', UINT, 1, 'initial maximal number of counterexamples used in MBQI, each counterexample generates a quantifier instantiation'),
                           ('mbqi.max_cexs_incr', UINT, 0, 'increment for MBQI_MAX_CEXS, the increment is performed after each round of MBQI'),
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 4535b29c2..cdfdd208f 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -1829,6 +1829,15 @@ namespace smt {
         m_bvar_inc *= INV_ACTIVITY_LIMIT;
     }
 
+    expr* context::next_decision() {
+        bool_var var;
+        lbool phase;
+        m_case_split_queue->next_case_split(var, phase);
+        if (var == null_bool_var) return m_manager.mk_true();
+        m_case_split_queue->unassign_var_eh(var);
+        return bool_var2expr(var);
+    }
+
     /**
        \brief Execute next clase split, return false if there are no
        more case splits to be performed.
@@ -3433,6 +3442,7 @@ namespace smt {
         m_num_conflicts                = 0;
         m_num_conflicts_since_restart  = 0;
         m_num_conflicts_since_lemma_gc = 0;
+        m_num_restarts                 = 0;
         m_restart_threshold            = m_fparams.m_restart_initial;
         m_restart_outer_threshold      = m_fparams.m_restart_initial;
         m_agility                      = 0.0;
@@ -3564,7 +3574,7 @@ namespace smt {
         inc_limits();
         if (status == l_true || !m_fparams.m_restart_adaptive || m_agility < m_fparams.m_restart_agility_threshold) {
             SASSERT(!inconsistent());
-                IF_VERBOSE(2, verbose_stream() << "(smt.restarting :propagations " << m_stats.m_num_propagations
+            IF_VERBOSE(2, verbose_stream() << "(smt.restarting :propagations " << m_stats.m_num_propagations
                        << " :decisions " << m_stats.m_num_decisions
                        << " :conflicts " << m_stats.m_num_conflicts << " :restart " << m_restart_threshold;
                        if (m_fparams.m_restart_strategy == RS_IN_OUT_GEOMETRIC) {
@@ -3573,9 +3583,10 @@ namespace smt {
                        if (m_fparams.m_restart_adaptive) {
                            verbose_stream() << " :agility " << m_agility;
                        }
-                       verbose_stream() << ")" << std::endl; verbose_stream().flush(););
+                       verbose_stream() << ")\n");
             // execute the restart
             m_stats.m_num_restarts++;
+            m_num_restarts++;
             if (m_scope_lvl > curr_lvl) {
                 pop_scope(m_scope_lvl - curr_lvl);
                 SASSERT(at_search_level());
@@ -3593,6 +3604,11 @@ namespace smt {
                 status = l_false;
                 return false;
             }
+            if (m_num_restarts >= m_fparams.m_restart_max) {
+                status = l_undef;
+                m_last_search_failure = NUM_CONFLICTS;
+                return false;
+            }
         }
         if (m_fparams.m_simplify_clauses)
             simplify_clauses();
diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h
index 8a4fc9471..ed78b9825 100644
--- a/src/smt/smt_context.h
+++ b/src/smt/smt_context.h
@@ -889,6 +889,8 @@ namespace smt {
         unsigned           m_num_conflicts;
         unsigned           m_num_conflicts_since_restart;
         unsigned           m_num_conflicts_since_lemma_gc;
+        unsigned           m_num_restarts;
+        unsigned           m_num_simplifications;
         unsigned           m_restart_threshold;
         unsigned           m_restart_outer_threshold;
         unsigned           m_luby_idx;
@@ -1030,6 +1032,8 @@ namespace smt {
 
         enode * get_enode_eq_to(func_decl * f, unsigned num_args, enode * const * args);
 
+        expr* next_decision();
+
     protected:
         bool decide();
 
diff --git a/src/smt/smt_kernel.cpp b/src/smt/smt_kernel.cpp
index a7948725c..78e33c7dd 100644
--- a/src/smt/smt_kernel.cpp
+++ b/src/smt/smt_kernel.cpp
@@ -175,11 +175,15 @@ namespace smt {
         void get_guessed_literals(expr_ref_vector & result) {
             m_kernel.get_guessed_literals(result);
         }
-        
+
+        expr* next_decision() {
+            return m_kernel.next_decision();
+        }
+                
         void collect_statistics(::statistics & st) const {
             m_kernel.collect_statistics(st);
         }
-        
+
         void reset_statistics() {
         }
 
@@ -347,6 +351,10 @@ namespace smt {
         m_imp->get_guessed_literals(result);
     }
 
+    expr* kernel::next_decision() {
+        return m_imp->next_decision();
+    }        
+
     void kernel::display(std::ostream & out) const {
         m_imp->display(out);
     }
diff --git a/src/smt/smt_kernel.h b/src/smt/smt_kernel.h
index d10cab4f3..d15790429 100644
--- a/src/smt/smt_kernel.h
+++ b/src/smt/smt_kernel.h
@@ -212,6 +212,11 @@ namespace smt {
         */
         void get_guessed_literals(expr_ref_vector & result);
 
+        /**
+           \brief return the next case split literal.
+        */
+        expr* next_decision();
+
         /**
            \brief (For debubbing purposes) Prints the state of the kernel
         */
diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp
index 780495e9c..2a7d52a48 100644
--- a/src/smt/smt_solver.cpp
+++ b/src/smt/smt_solver.cpp
@@ -30,9 +30,35 @@ Notes:
 namespace smt {
 
     class smt_solver : public solver_na2as {
+
+        struct cuber {
+            smt_solver& m_solver;
+            unsigned    m_round;
+            expr_ref    m_result;
+            cuber(smt_solver& s):
+                m_solver(s),
+                m_round(0),
+                m_result(s.get_manager()) {}
+            expr_ref cube() {
+                switch (m_round) {
+                case 0:
+                    m_result = m_solver.m_context.next_decision();
+                    break;
+                case 1:
+                    m_result = m_solver.get_manager().mk_not(m_result);
+                    break;
+                default:
+                    m_result = m_solver.get_manager().mk_false();
+                    break;
+                }
+                ++m_round;
+                return m_result;
+            }
+        };
+
         smt_params           m_smt_params;
         smt::kernel          m_context;
-        progress_callback  * m_callback;
+        cuber*               m_cuber;
         symbol               m_logic;
         bool                 m_minimizing_core;
         bool                 m_core_extend_patterns;
@@ -45,6 +71,7 @@ namespace smt {
             solver_na2as(m),
             m_smt_params(p),
             m_context(m, m_smt_params),
+            m_cuber(nullptr),
             m_minimizing_core(false),
             m_core_extend_patterns(false),
             m_core_extend_patterns_max_distance(UINT_MAX),
@@ -72,6 +99,7 @@ namespace smt {
 
         virtual ~smt_solver() {
             dec_ref_values(get_manager(), m_name2assertion);
+            dealloc(m_cuber);
         }
 
         virtual void updt_params(params_ref const & p) {
@@ -204,7 +232,6 @@ namespace smt {
         virtual ast_manager & get_manager() const { return m_context.m(); }
 
         virtual void set_progress_callback(progress_callback * callback) {
-            m_callback = callback;
             m_context.set_progress_callback(callback);
         }
 
@@ -217,13 +244,24 @@ namespace smt {
             return m_context.get_formula(idx);
         }
 
-        virtual expr_ref lookahead(expr_ref_vector const& assumptions, expr_ref_vector const& candidates) { 
+        virtual expr_ref_vector cube(expr_ref_vector& vars, unsigned cutoff) {
             ast_manager& m = get_manager();
-            return expr_ref(m.mk_true(), m);
-        }
-
-        virtual expr_ref_vector cube(expr_ref_vector&, unsigned) {
-            return expr_ref_vector(get_manager());
+            if (!m_cuber) {
+                m_cuber = alloc(cuber, *this);
+            }
+            expr_ref result = m_cuber->cube();
+            expr_ref_vector lits(m);
+            if (m.is_false(result)) {
+                dealloc(m_cuber);
+                m_cuber = nullptr;
+            }
+            if (m.is_true(result)) {
+                dealloc(m_cuber);
+                m_cuber = nullptr;
+                return lits;
+            }
+            lits.push_back(result);
+            return lits;
         }
 
         struct collect_fds_proc {
diff --git a/src/tactic/portfolio/CMakeLists.txt b/src/tactic/portfolio/CMakeLists.txt
index 055251467..e16992f9a 100644
--- a/src/tactic/portfolio/CMakeLists.txt
+++ b/src/tactic/portfolio/CMakeLists.txt
@@ -8,6 +8,7 @@ z3_add_component(portfolio
     pb2bv_solver.cpp
     smt_strategic_solver.cpp
     solver2lookahead.cpp
+    solver_sat_extension.cpp
   COMPONENT_DEPENDENCIES
     aig_tactic
     fp
diff --git a/src/tactic/portfolio/parallel_tactic.cpp b/src/tactic/portfolio/parallel_tactic.cpp
index 988ab2ec4..fed4bde0a 100644
--- a/src/tactic/portfolio/parallel_tactic.cpp
+++ b/src/tactic/portfolio/parallel_tactic.cpp
@@ -41,8 +41,13 @@ Notes:
 #include "solver/solver.h"
 #include "solver/solver2tactic.h"
 #include "tactic/tactic.h"
+#include "tactic/tactical.h"
 #include "tactic/portfolio/fd_solver.h"
 #include "tactic/smtlogics/parallel_params.hpp"
+#include "smt/tactic/smt_tactic.h"
+#include "smt/smt_solver.h"
+#include "sat/sat_solver/inc_sat_solver.h"
+#include "sat/tactic/sat_tactic.h"
 
 class parallel_tactic : public tactic {
 
@@ -184,7 +189,6 @@ class parallel_tactic : public tactic {
         ref<solver>     m_solver;                 // solver state
         unsigned        m_depth;                  // number of nested calls to cubing
         double          m_width;                  // estimate of fraction of problem handled by state
-        unsigned        m_restart_max;            // saved configuration value
 
     public:
         solver_state(ast_manager* m, solver* s, params_ref const& p, task_type t): 
@@ -196,8 +200,6 @@ class parallel_tactic : public tactic {
             m_depth(0),
             m_width(1.0)
         {
-            parallel_params pp(p);
-            m_restart_max = pp.restart_max();
         }
 
         ast_manager& m() { return m_solver->get_manager(); }
@@ -255,27 +257,12 @@ class parallel_tactic : public tactic {
 
         lbool simplify() {
             lbool r = l_undef;
-            if (m_depth == 1) {
-                IF_VERBOSE(2, verbose_stream() << "(parallel.tactic simplify-1)\n";);
-                set_simplify_params(true, true);         // retain PB, retain blocked
-                r = get_solver().check_sat(0,0);
-                if (r != l_undef) return r;
-                
-                // copy over the resulting clauses with a configuration that blasts PB constraints
-                set_simplify_params(false, true);
-                expr_ref_vector fmls(m());
-                get_solver().get_assertions(fmls);
-                model_converter_ref mc = get_solver().get_model_converter();
-                m_solver = mk_fd_solver(m(), m_params);
-                m_solver->set_model_converter(mc.get());
-                m_solver->assert_expr(fmls);
-            }
-            IF_VERBOSE(2, verbose_stream() << "(parallel.tactic simplify-2)\n";);
-            set_simplify_params(false, true);         // remove PB, retain blocked
+            IF_VERBOSE(2, verbose_stream() << "(parallel.tactic simplify-1)\n";);
+            set_simplify_params(true);         // retain blocked
             r = get_solver().check_sat(0,0);
             if (r != l_undef) return r;
-            IF_VERBOSE(2, verbose_stream() << "(parallel.tactic simplify-3)\n";);
-            set_simplify_params(false, false);        // remove any PB, remove blocked
+            IF_VERBOSE(2, verbose_stream() << "(parallel.tactic simplify-2)\n";);
+            set_simplify_params(false);        // remove blocked
             r = get_solver().check_sat(0,0);
             return r;            
         }
@@ -299,27 +286,26 @@ class parallel_tactic : public tactic {
         }
 
         void set_conquer_params(solver& s) {
+            parallel_params pp(m_params);
             params_ref p;
             p.copy(m_params);
             p.set_bool("gc.burst", true);             // apply eager gc
             p.set_uint("simplify.delay", 1000);       // delay simplification by 1000 conflicts
             p.set_bool("lookahead_simplify", false);
-            p.set_uint("restart.max", m_restart_max);
+            p.set_uint("restart.max", pp.conquer_restart_max());
             p.set_uint("inprocess.max", UINT_MAX);    // base bounds on restart.max
             s.updt_params(p);
         }
 
-        void set_simplify_params(bool pb_simp, bool retain_blocked) {
+        void set_simplify_params(bool retain_blocked) {
             parallel_params pp(m_params);
+            double mul = pp.simplify_multiplier();
+            unsigned mult = (mul == 0 ? 1 : std::max((unsigned)1, static_cast<unsigned>(m_depth * mul)));
             params_ref p;
             p.copy(m_params);
-
-            p.set_bool("cardinality.solver", pb_simp);
-            p.set_sym ("pb.solver", pb_simp ? symbol("solver") : symbol("circuit"));
-            if (p.get_uint("inprocess.max", UINT_MAX) == UINT_MAX) 
-                p.set_uint("inprocess.max", pp.inprocess_max());
+            p.set_uint("inprocess.max", pp.simplify_inprocess_max() * mult);
+            p.set_uint("restart.max", pp.simplify_restart_max() * mult);
             p.set_bool("lookahead_simplify", true);
-            p.set_uint("restart.max", UINT_MAX);
             p.set_bool("retain_blocked_clauses", retain_blocked);
             get_solver().updt_params(p);
         }
@@ -337,6 +323,7 @@ class parallel_tactic : public tactic {
 
 private:
 
+    solver_ref   m_solver;
     ast_manager& m_manager;
     params_ref   m_params;
     sref_vector<model> m_models;
@@ -355,7 +342,8 @@ private:
     std::string  m_exn_msg;
 
     void init() {
-        m_num_threads = omp_get_num_procs();  // TBD adjust by possible threads used inside each solver.
+        parallel_params pp(m_params);
+        m_num_threads = std::min((unsigned)omp_get_num_procs(), pp.threads_max());
         m_progress = 0;
         m_has_undef = false;
         m_allsat = false;
@@ -375,6 +363,7 @@ private:
     }
 
     void add_branches(unsigned b) {
+        if (b == 0) return;
         {
             std::lock_guard<std::mutex> lock(m_mutex);
             m_branches += b;
@@ -617,7 +606,6 @@ private:
         }
         else if (cubes.empty()) {
             dec_branch();
-            return;
         }
         else {
             s.inc_width(width);
@@ -746,15 +734,16 @@ private:
 
 public:
 
-    parallel_tactic(ast_manager& m, params_ref const& p) :
-        m_manager(m),
+    parallel_tactic(solver* s, params_ref const& p) :
+        m_solver(s),
+        m_manager(s->get_manager()),        
         m_params(p) {
         init();
     }
 
     void operator ()(const goal_ref & g,goal_ref_buffer & result) {
         ast_manager& m = g->m();
-        solver* s = mk_fd_solver(m, m_params);
+        solver* s = m_solver->translate(m, m_params);
         solver_state* st = alloc(solver_state, 0, s, m_params, cube_task);
         m_queue.add_task(st);
         expr_ref_vector clauses(m);
@@ -799,7 +788,8 @@ public:
     }
 
     tactic* translate(ast_manager& m) {
-        return alloc(parallel_tactic, m, m_params);
+        solver* s = m_solver->translate(m, m_params);
+        return alloc(parallel_tactic, s, m_params);
     }
 
     virtual void updt_params(params_ref const & p) {
@@ -817,12 +807,40 @@ public:
     virtual void reset_statistics() {
         m_stats.reset();
     }
-
 };
 
 
 
-tactic * mk_parallel_tactic(ast_manager& m, params_ref const& p) {
-    return alloc(parallel_tactic, m, p);
+tactic * mk_parallel_qffd_tactic(ast_manager& m, params_ref const& p) {
+    solver* s = mk_fd_solver(m, p);
+    return alloc(parallel_tactic, s, p);
 }
 
+tactic * mk_parallel_tactic(solver* s, params_ref const& p) {
+    return alloc(parallel_tactic, s, p);
+}
+
+
+tactic * mk_psat_tactic(ast_manager& m, params_ref const& p) {
+    parallel_params pp(p);
+    bool use_parallel = pp.enable();
+    return pp.enable() ? mk_parallel_tactic(mk_inc_sat_solver(m, p), p) : mk_sat_tactic(m);
+}
+
+tactic * mk_psmt_tactic(ast_manager& m, params_ref const& p, symbol const& logic) {
+    parallel_params pp(p);
+    bool use_parallel = pp.enable();
+    return pp.enable() ? mk_parallel_tactic(mk_smt_solver(m, p, logic), p) : mk_smt_tactic(p);
+}
+
+tactic * mk_psmt_tactic_using(ast_manager& m, bool auto_config, params_ref const& _p, symbol const& logic) {
+    parallel_params pp(_p);
+    bool use_parallel = pp.enable();
+    params_ref p = _p;
+    p.set_bool("auto_config", auto_config);
+    return using_params(pp.enable() ? mk_parallel_tactic(mk_smt_solver(m, p, logic), p) : mk_smt_tactic(p), p);
+}
+
+tactic * mk_parallel_smt_tactic(ast_manager& m, params_ref const& p) {
+    return mk_parallel_tactic(mk_smt_solver(m, p, symbol::null), p);
+}
diff --git a/src/tactic/portfolio/parallel_tactic.h b/src/tactic/portfolio/parallel_tactic.h
index 8fd9a29fa..f3dc36d0e 100644
--- a/src/tactic/portfolio/parallel_tactic.h
+++ b/src/tactic/portfolio/parallel_tactic.h
@@ -21,11 +21,20 @@ Notes:
 
 class solver;
 class tactic;
+class solver;
 
-tactic * mk_parallel_tactic(ast_manager& m, params_ref const& p);
+tactic * mk_parallel_tactic(solver* s, params_ref const& p);
+tactic * mk_parallel_qffd_tactic(ast_manager& m, params_ref const& p);
+tactic * mk_parallel_smt_tactic(ast_manager& m, params_ref const& p);
+
+// create parallel sat/smt tactics if parallel.enable=true, otherwise return sequential versions.
+tactic * mk_psat_tactic(ast_manager& m, params_ref const& p);
+tactic * mk_psmt_tactic(ast_manager& m, params_ref const& p, symbol const& logic = symbol::null);
+tactic * mk_psmt_tactic_using(ast_manager& m, bool auto_config, params_ref const& p, symbol const& logic = symbol::null);
 
 /*
-    ADD_TACTIC("qffdp", "builtin strategy for solving QF_FD problems in parallel.", "mk_parallel_tactic(m, p)")
+    ADD_TACTIC("pqffd", "builtin strategy for solving QF_FD problems in parallel.", "mk_parallel_qffd_tactic(m, p)")
+    ADD_TACTIC("psmt", "builtin strategy for SMT tactic in parallel.", "mk_parallel_smt_tactic(m, p)")
 */
 
 #endif
diff --git a/src/tactic/smtlogics/nra_tactic.cpp b/src/tactic/smtlogics/nra_tactic.cpp
index 381bc4bb6..a9b32e5a8 100644
--- a/src/tactic/smtlogics/nra_tactic.cpp
+++ b/src/tactic/smtlogics/nra_tactic.cpp
@@ -19,13 +19,13 @@ Notes:
 #include "tactic/tactical.h"
 #include "tactic/core/simplify_tactic.h"
 #include "tactic/core/propagate_values_tactic.h"
-#include "smt/tactic/smt_tactic.h"
 #include "tactic/core/nnf_tactic.h"
+#include "tactic/arith/probe_arith.h"
+#include "smt/tactic/smt_tactic.h"
 #include "qe/qe_tactic.h"
 #include "qe/nlqsat.h"
-#include "nlsat/tactic/qfnra_nlsat_tactic.h"
 #include "qe/qe_lite.h"
-#include "tactic/arith/probe_arith.h"
+#include "nlsat/tactic/qfnra_nlsat_tactic.h"
 
 tactic * mk_nra_tactic(ast_manager & m, params_ref const& p) {
     params_ref p1 = p;
diff --git a/src/tactic/smtlogics/parallel_params.pyg b/src/tactic/smtlogics/parallel_params.pyg
index 84f4eb2c4..590fc02d2 100644
--- a/src/tactic/smtlogics/parallel_params.pyg
+++ b/src/tactic/smtlogics/parallel_params.pyg
@@ -4,8 +4,11 @@ def_module_params('parallel',
                   export=True,
                   params=(
                           ('enable', BOOL, False, 'enable parallel solver by default on selected tactics (for QF_BV)'),
-                          ('conquer_batch_size', UINT, 1000, 'number of cubes to batch together for fast conquer'),
-                          ('inprocess.max', UINT, 2, 'maximal number of inprocessing steps during simplification'),
-                          ('restart.max', UINT, 5, 'maximal number of restarts during conquer phase'),
-                          ('conquer_threshold', UINT, 10, 'number of cubes generated before simple conquer solver is created'),
+                          ('threads.max', UINT, 10000, 'caps maximal number of threads below the number of processors'),
+                          ('simplify.multiplier', DOUBLE, 0, 'restart and inprocess max is increased by depth * simplify.multipler, unless the multiplier is 0'),
+                          ('conquer.batch_size', UINT, 1000, 'number of cubes to batch together for fast conquer'),
+                          ('conquer.threshold', UINT, 10, 'number of cubes generated before simple conquer solver is created'),
+                          ('conquer.restart.max', UINT, 5, 'maximal number of restarts during conquer phase'),
+	                  ('simplify.restart.max', UINT, 5000, 'maximal number of restarts during simplification phase'),
+                          ('simplify.inprocess.max', UINT, 2, 'maximal number of inprocessing steps during simplification'),
                           ))
diff --git a/src/tactic/smtlogics/qfbv_tactic.cpp b/src/tactic/smtlogics/qfbv_tactic.cpp
index 25741c09e..68f054640 100644
--- a/src/tactic/smtlogics/qfbv_tactic.cpp
+++ b/src/tactic/smtlogics/qfbv_tactic.cpp
@@ -28,6 +28,7 @@ Notes:
 #include "tactic/bv/bv_size_reduction_tactic.h"
 #include "tactic/aig/aig_tactic.h"
 #include "sat/tactic/sat_tactic.h"
+#include "sat/sat_solver/inc_sat_solver.h"
 #include "tactic/portfolio/parallel_tactic.h"
 #include "tactic/smtlogics/parallel_params.hpp"
 #include "ackermannization/ackermannize_bv_tactic.h"
@@ -129,12 +130,10 @@ static tactic * mk_qfbv_tactic(ast_manager& m, params_ref const & p, tactic* sat
 
 
 tactic * mk_qfbv_tactic(ast_manager & m, params_ref const & p) {
-    parallel_params pp(p);
-    bool use_parallel = pp.enable();
     tactic * new_sat = cond(mk_produce_proofs_probe(),
                             and_then(mk_simplify_tactic(m), mk_smt_tactic()),
-                            use_parallel ? mk_parallel_tactic(m, p): mk_sat_tactic(m));
+                            mk_psat_tactic(m, p));
 
-    return mk_qfbv_tactic(m, p, new_sat, mk_smt_tactic());
+    return mk_qfbv_tactic(m, p, new_sat, mk_psmt_tactic(m, p));
 
 }
diff --git a/src/tactic/smtlogics/qflia_tactic.cpp b/src/tactic/smtlogics/qflia_tactic.cpp
index 248829c49..b30103f43 100644
--- a/src/tactic/smtlogics/qflia_tactic.cpp
+++ b/src/tactic/smtlogics/qflia_tactic.cpp
@@ -24,7 +24,6 @@ Notes:
 #include "tactic/core/solve_eqs_tactic.h"
 #include "tactic/core/elim_uncnstr_tactic.h"
 #include "smt/tactic/smt_tactic.h"
-// include"mip_tactic.h"
 #include "tactic/arith/add_bounds_tactic.h"
 #include "tactic/arith/pb2bv_tactic.h"
 #include "tactic/arith/lia2pb_tactic.h"
@@ -35,6 +34,7 @@ Notes:
 #include "sat/tactic/sat_tactic.h"
 #include "tactic/arith/bound_manager.h"
 #include "tactic/arith/probe_arith.h"
+#include "tactic/portfolio/parallel_tactic.h"
 
 struct quasi_pb_probe : public probe {
     virtual result operator()(goal const & g) {
@@ -42,10 +42,7 @@ struct quasi_pb_probe : public probe {
         bound_manager bm(g.m());
         bm(g);
         rational l, u; bool st;
-        bound_manager::iterator it  = bm.begin();
-        bound_manager::iterator end = bm.end();
-        for (; it != end; ++it) {
-            expr * t = *it;
+        for (expr * t : bm) {
             if (bm.has_lower(t, l, st) && bm.has_upper(t, u, st) && (l.is_zero() || l.is_one()) && (u.is_zero() || u.is_one()))
                 continue;
             if (found_non_01)
@@ -93,7 +90,7 @@ static tactic * mk_bv2sat_tactic(ast_manager & m) {
                                  mk_max_bv_sharing_tactic(m),
                                  mk_bit_blaster_tactic(m),
                                  mk_aig_tactic(),
-                                 mk_sat_tactic(m)),
+                                 mk_sat_tactic(m, solver_p)),
                         solver_p);
 }
 
@@ -224,7 +221,7 @@ tactic * mk_qflia_tactic(ast_manager & m, params_ref const & p) {
                                                          using_params(mk_lia2sat_tactic(m), quasi_pb_p),
                                                          mk_fail_if_undecided_tactic()),
                                                 mk_bounded_tactic(m),
-                                                mk_smt_tactic())),
+                                                mk_psmt_tactic(m, p))),
                                main_p);
     
     st->updt_params(p);