diff --git a/src/smt/params/smt_params.cpp b/src/smt/params/smt_params.cpp
index de09e42d0..44df3fa55 100644
--- a/src/smt/params/smt_params.cpp
+++ b/src/smt/params/smt_params.cpp
@@ -30,6 +30,8 @@ void smt_params::updt_local_params(params_ref const & _p) {
     m_clause_proof = p.clause_proof();
     m_phase_selection = static_cast<phase_selection>(p.phase_selection());
     if (m_phase_selection > PS_THEORY) throw default_exception("illegal phase selection numeral");
+    m_phase_caching_on = p.phase_caching_on();
+    m_phase_caching_off = p.phase_caching_off();
     m_restart_strategy = static_cast<restart_strategy>(p.restart_strategy());
     if (m_restart_strategy > RS_ARITHMETIC) throw default_exception("illegal restart strategy numeral");
     m_restart_factor = p.restart_factor();
@@ -41,8 +43,10 @@ void smt_params::updt_local_params(params_ref const & _p) {
     m_preprocess = _p.get_bool("preprocess", true); // hidden parameter
     m_max_conflicts = p.max_conflicts();
     m_restart_max   = p.restart_max();
+    m_cube_depth    = p.cube_depth();
     m_threads       = p.threads();
     m_threads_max_conflicts  = p.threads_max_conflicts();
+    m_threads_cube_frequency = p.threads_cube_frequency();
     m_core_validate = p.core_validate();
     m_logic = _p.get_sym("logic", m_logic);
     m_string_solver = p.string_solver();
@@ -105,8 +109,10 @@ void smt_params::display(std::ostream & out) const {
     DISPLAY_PARAM(m_phase_caching_off);
     DISPLAY_PARAM(m_minimize_lemmas);
     DISPLAY_PARAM(m_max_conflicts);
+    DISPLAY_PARAM(m_cube_depth);
     DISPLAY_PARAM(m_threads);
     DISPLAY_PARAM(m_threads_max_conflicts);
+    DISPLAY_PARAM(m_threads_cube_frequency);
     DISPLAY_PARAM(m_simplify_clauses);
     DISPLAY_PARAM(m_tick);
     DISPLAY_PARAM(m_display_features);
diff --git a/src/smt/params/smt_params.h b/src/smt/params/smt_params.h
index 2575f95c9..01d83403c 100644
--- a/src/smt/params/smt_params.h
+++ b/src/smt/params/smt_params.h
@@ -102,8 +102,10 @@ struct smt_params : public preprocessor_params,
     bool             m_minimize_lemmas;
     unsigned         m_max_conflicts;
     unsigned         m_restart_max;
+    unsigned         m_cube_depth;
     unsigned         m_threads;
     unsigned         m_threads_max_conflicts;
+    unsigned         m_threads_cube_frequency;
     bool             m_simplify_clauses;
     unsigned         m_tick;
     bool             m_display_features;
@@ -251,12 +253,14 @@ struct smt_params : public preprocessor_params,
         m_clause_decay(1),
         m_random_initial_activity(IA_RANDOM_WHEN_SEARCHING),
         m_phase_selection(PS_CACHING_CONSERVATIVE),
-        m_phase_caching_on(400),
+        m_phase_caching_on(700),
         m_phase_caching_off(100),
         m_minimize_lemmas(true),
         m_max_conflicts(UINT_MAX),
+        m_cube_depth(1),
         m_threads(1),
         m_threads_max_conflicts(UINT_MAX),
+        m_threads_cube_frequency(2),
         m_simplify_clauses(true),
         m_tick(1000),
         m_display_features(false),
diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg
index 8ffbc2c7f..b3aa7d073 100644
--- a/src/smt/params/smt_params_helper.pyg
+++ b/src/smt/params/smt_params_helper.pyg
@@ -11,6 +11,8 @@ def_module_params(module_name='smt',
                           ('restricted_quasi_macros', BOOL, False, 'try to find universally quantified formulas that are restricted quasi-macros'),
                           ('ematching', BOOL, True, 'E-Matching based quantifier instantiation'),
                           ('phase_selection', UINT, 3, 'phase selection heuristic: 0 - always false, 1 - always true, 2 - phase caching, 3 - phase caching conservative, 4 - phase caching conservative 2, 5 - random, 6 - number of occurrences, 7 - theory'),
+	                  ('phase_caching_on', UINT, 400, 'number of conflicts while phase caching is on'),
+	                  ('phase_caching_off', UINT, 100, 'number of conflicts while phase caching is off'),
                           ('restart_strategy', UINT, 1, '0 - geometric, 1 - inner-outer-geometric, 2 - luby, 3 - fixed, 4 - arithmetic'),
                           ('restart_factor', DOUBLE, 1.1, 'when using geometric (or inner-outer-geometric) progression of restarts, it specifies the constant used to multiply the current restart threshold'),
                           ('case_split', UINT, 1, '0 - case split based on variable activity, 1 - similar to 0, but delay case splits created during the search, 2 - similar to 0, but cache the relevancy, 3 - case split based on relevancy (structural splitting), 4 - case split on relevancy and activity, 5 - case split on relevancy and current goal, 6 - activity-based case split with theory-aware branching activity'),
@@ -20,8 +22,10 @@ def_module_params(module_name='smt',
                           ('refine_inj_axioms', BOOL, True, 'refine injectivity axioms'),
                           ('max_conflicts', UINT, UINT_MAX, 'maximum number of conflicts before giving up.'),
                           ('restart.max', UINT, UINT_MAX, 'maximal number of restarts.'),
+	                  ('cube_depth', UINT, 1, 'cube depth.'),
                           ('threads', UINT, 1, 'maximal number of parallel threads.'),
                           ('threads.max_conflicts', UINT, 400, 'maximal number of conflicts between rounds of cubing for parallel SMT'),
+                          ('threads.cube_frequency', UINT, 2, 'frequency for using cubing'), 
                           ('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'),
@@ -40,6 +44,8 @@ def_module_params(module_name='smt',
                           ('induction', BOOL, False, 'enable generation of induction lemmas'),
                           ('bv.reflect', BOOL, True, 'create enode for every bit-vector term'),
                           ('bv.enable_int2bv', BOOL, True, 'enable support for int2bv and bv2int operators'),
+	                  ('bv.eq_axioms', BOOL, True, 'add dynamic equality axioms'),
+                          ('bv.watch_diseq', BOOL, False, 'use watch lists instead of eager axioms for bit-vectors'),
                           ('arith.random_initial_value', BOOL, False, 'use random initial values in the simplex-based procedure for linear arithmetic'),
                           ('arith.cheap_eqs', BOOL, True, 'false - do not run, true - run cheap equality heuristic'),
                           ('arith.solver', UINT, 6, 'arithmetic solver: 0 - no solver, 1 - bellman-ford based solver (diff. logic only), 2 - simplex based solver, 3 - floyd-warshall based solver (diff. logic only) and no theory combination 4 - utvpi, 5 - infinitary lra, 6 - lra solver'),
diff --git a/src/smt/params/theory_bv_params.cpp b/src/smt/params/theory_bv_params.cpp
index 156fda592..fbd7647a4 100644
--- a/src/smt/params/theory_bv_params.cpp
+++ b/src/smt/params/theory_bv_params.cpp
@@ -26,6 +26,7 @@ void theory_bv_params::updt_params(params_ref const & _p) {
     m_hi_div0 = rp.hi_div0();
     m_bv_reflect = p.bv_reflect();
     m_bv_enable_int2bv2int = p.bv_enable_int2bv(); 
+    m_bv_eq_axioms = p.bv_eq_axioms();
 }
 
 #define DISPLAY_PARAM(X) out << #X"=" << X << std::endl;
@@ -36,6 +37,7 @@ void theory_bv_params::display(std::ostream & out) const {
     DISPLAY_PARAM(m_bv_reflect);
     DISPLAY_PARAM(m_bv_lazy_le);
     DISPLAY_PARAM(m_bv_cc);
+    DISPLAY_PARAM(m_bv_eq_axioms);
     DISPLAY_PARAM(m_bv_blast_max_size);
     DISPLAY_PARAM(m_bv_enable_int2bv2int);
 }
diff --git a/src/smt/params/theory_bv_params.h b/src/smt/params/theory_bv_params.h
index 90db967ac..c0bb135de 100644
--- a/src/smt/params/theory_bv_params.h
+++ b/src/smt/params/theory_bv_params.h
@@ -31,16 +31,20 @@ struct theory_bv_params {
     bool         m_bv_reflect;
     bool         m_bv_lazy_le;
     bool         m_bv_cc;
+    bool         m_bv_eq_axioms;
     unsigned     m_bv_blast_max_size;
     bool         m_bv_enable_int2bv2int;
+    bool         m_bv_watch_diseq;
     theory_bv_params(params_ref const & p = params_ref()):
         m_bv_mode(BS_BLASTER),
         m_hi_div0(false),
         m_bv_reflect(true),
         m_bv_lazy_le(false),
         m_bv_cc(false),
+        m_bv_eq_axioms(true),
         m_bv_blast_max_size(INT_MAX),
-        m_bv_enable_int2bv2int(true) {
+        m_bv_enable_int2bv2int(true),
+        m_bv_watch_diseq(false) {
         updt_params(p);
     }
     
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 40e9e6570..e4dc193ca 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -3963,6 +3963,7 @@ namespace smt {
         }
     }
 
+
     bool context::resolve_conflict() {
         m_stats.m_num_conflicts++;
         m_num_conflicts ++;
diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h
index e4e46f77b..1817cc1ad 100644
--- a/src/smt/smt_context.h
+++ b/src/smt/smt_context.h
@@ -893,7 +893,11 @@ namespace smt {
 
         void mk_clause(literal l1, literal l2, literal l3, justification * j);
 
-        void mk_th_axiom(theory_id tid, unsigned num_lits, literal * lits, unsigned num_params = 0, parameter * params = nullptr);
+        void context::mk_th_clause(theory_id tid, unsigned num_lits, literal * lits, unsigned num_params, parameter * params, clause_kind k);
+
+        void mk_th_axiom(theory_id tid, unsigned num_lits, literal * lits, unsigned num_params = 0, parameter * params = nullptr) {
+            mk_th_clause(tid, num_lits, lits, num_params, params, CLS_TH_AXIOM);
+        }
 
         void mk_th_axiom(theory_id tid, literal l1, literal l2, unsigned num_params = 0, parameter * params = nullptr);
 
@@ -903,6 +907,24 @@ namespace smt {
             mk_th_axiom(tid, ls.size(), ls.c_ptr(), num_params, params);
         }
 
+        void mk_th_lemma(theory_id tid, literal l1, literal l2, unsigned num_params = 0, parameter * params = nullptr) {
+            literal ls[2] = { l1, l2 };
+            mk_th_lemma(tid, 2, ls, num_params, params);
+        }
+
+        void mk_th_lemma(theory_id tid, literal l1, literal l2, literal l3, unsigned num_params = 0, parameter * params = nullptr) {
+            literal ls[3] = { l1, l2, l3 };
+            mk_th_lemma(tid, 3, ls, num_params, params);
+        }
+
+        void mk_th_lemma(theory_id tid, unsigned num_lits, literal * lits, unsigned num_params = 0, parameter * params = nullptr) {
+            mk_th_clause(tid, num_lits, lits, num_params, params, CLS_TH_LEMMA);
+        }
+
+        void mk_th_lemma(theory_id tid, literal_vector const& ls, unsigned num_params = 0, parameter * params = nullptr) {
+            mk_th_lemma(tid, ls.size(), ls.c_ptr(), num_params, params);
+        }
+
         /*
          * Provide a hint to the core solver that the specified literals form a "theory case split".
          * The core solver will enforce the condition that exactly one of these literals can be
@@ -1209,6 +1231,7 @@ namespace smt {
 
         virtual bool resolve_conflict();
 
+
         // -----------------------------------
         //
         // Propagation
diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp
index a90648200..29eb06b78 100644
--- a/src/smt/smt_internalizer.cpp
+++ b/src/smt/smt_internalizer.cpp
@@ -1488,7 +1488,7 @@ namespace smt {
         mk_clause(3, ls, j);
     }
     
-    void context::mk_th_axiom(theory_id tid, unsigned num_lits, literal * lits, unsigned num_params, parameter * params) {
+    void context::mk_th_clause(theory_id tid, unsigned num_lits, literal * lits, unsigned num_params, parameter * params, clause_kind k) {
         justification * js = nullptr;
         TRACE("mk_th_axiom", display_literals_verbose(tout, num_lits, lits) << "\n";);
 
@@ -1501,7 +1501,7 @@ namespace smt {
             SASSERT(tmp.size() == num_lits);
             display_lemma_as_smt_problem(tmp.size(), tmp.c_ptr(), false_literal, m_fparams.m_logic);
         }
-        mk_clause(num_lits, lits, js, CLS_TH_AXIOM);
+        mk_clause(num_lits, lits, js, k);
     }
     
     void context::mk_th_axiom(theory_id tid, literal l1, literal l2, unsigned num_params, parameter * params) {
diff --git a/src/smt/smt_kernel.cpp b/src/smt/smt_kernel.cpp
index de785cfae..4f48aec33 100644
--- a/src/smt/smt_kernel.cpp
+++ b/src/smt/smt_kernel.cpp
@@ -204,6 +204,11 @@ namespace smt {
             lookahead lh(m_kernel);
             return lh.choose();
         }
+
+        expr_ref_vector cubes(unsigned depth) {
+            lookahead lh(m_kernel);
+            return lh.choose_rec(depth);
+        }
                 
         void collect_statistics(::statistics & st) const {
             m_kernel.collect_statistics(st);
@@ -379,6 +384,10 @@ namespace smt {
         return m_imp->next_cube();
     }        
 
+    expr_ref_vector kernel::cubes(unsigned depth) {
+        return m_imp->cubes(depth);
+    }        
+
     std::ostream& kernel::display(std::ostream & out) const {
         m_imp->display(out);
         return out;
diff --git a/src/smt/smt_kernel.h b/src/smt/smt_kernel.h
index f210d69ec..b9f80ac01 100644
--- a/src/smt/smt_kernel.h
+++ b/src/smt/smt_kernel.h
@@ -218,6 +218,11 @@ namespace smt {
         */
         expr_ref next_cube();
 
+        /**
+           \brief return up to 2^depth cubes to case split on.
+        */
+        expr_ref_vector cubes(unsigned depth);
+
         /**
            \brief retrieve upper/lower bound for arithmetic term, if it is implied.
            retrieve implied values if terms are fixed to a value.
diff --git a/src/smt/smt_lookahead.cpp b/src/smt/smt_lookahead.cpp
index 879e9baee..191b03e49 100644
--- a/src/smt/smt_lookahead.cpp
+++ b/src/smt/smt_lookahead.cpp
@@ -64,7 +64,7 @@ namespace smt {
         }
     };
     
-    expr_ref lookahead::choose() {
+    expr_ref lookahead::choose(unsigned budget) {
         ctx.pop_to_base_lvl();
         unsigned sz = ctx.m_bool_var2expr.size();
         bool_var best_v = null_bool_var;
@@ -79,9 +79,12 @@ namespace smt {
         compare comp(ctx);
         std::sort(vars.begin(), vars.end(), comp);
         
-        unsigned nf = 0, nc = 0, ns = 0, bound = 2000, n = 0;
+        unsigned nf = 0, nc = 0, ns = 0, n = 0;
         for (bool_var v : vars) {
-            if (!ctx.bool_var2expr(v)) continue;
+            if (!ctx.bool_var2expr(v)) 
+                continue;
+            if (!m.inc())
+                break;
             literal lit(v, false);
             ctx.propagate();
             if (ctx.inconsistent())
@@ -116,16 +119,22 @@ namespace smt {
             }
             double score = score1 + score2 + 1024*score1*score2;
 
-            if (score > best_score || (score == best_score && ctx.get_random_value() % (++n) == 0)) {
-                if (score > best_score) n = 0;
-                best_score = score;
-                best_v = v;
-                bound += ns;
+            if (score <= 1.1*best_score && best_score <= 1.1*score) {
+                if (ctx.get_random_value() % (++n) == 0) {
+                    best_score = score;
+                    best_v = v;
+                }
                 ns = 0;
             }
+            else if (score > best_score && (ctx.get_random_value() % 2) == 0) {
+                n = 0;
+                best_score = score;
+                best_v = v;
+                ns = 0;
+            } 
             ++nc;
             ++ns;
-            if (ns > bound) {
+            if (ns > budget) {
                 break;
             }
         }
@@ -141,4 +150,38 @@ namespace smt {
         }
         return result;
     }
+
+    expr_ref_vector lookahead::choose_rec(unsigned depth) {
+        expr_ref_vector trail(m), result(m);
+        choose_rec(trail, result, depth, 2000);
+        return result;
+    }
+
+    void lookahead::choose_rec(expr_ref_vector & trail, expr_ref_vector& result, unsigned depth, unsigned budget) {
+            
+        expr_ref r = choose(budget);
+        if (m.is_true(r)) 
+            result.push_back(mk_and(trail));
+        else if (m.is_false(r))
+            ;
+        else {
+            auto recurse = [&]() {
+                trail.push_back(r);
+                if (depth <= 1 || !m.inc()) {
+                    result.push_back(mk_and(trail));
+                }
+                else {
+                    ctx.push();
+                    ctx.assert_expr(r);
+                    ctx.propagate();
+                    choose_rec(trail, result, depth-1, 2 * (budget / 3));
+                    ctx.pop(1);
+                }
+                trail.pop_back();
+            };
+            recurse();
+            r = m.mk_not(r);
+            recurse();
+        }
+    }
 }
diff --git a/src/smt/smt_lookahead.h b/src/smt/smt_lookahead.h
index fdcea58de..5deccad2c 100644
--- a/src/smt/smt_lookahead.h
+++ b/src/smt/smt_lookahead.h
@@ -32,9 +32,14 @@ namespace smt {
 
         double get_score();
 
+        void choose_rec(expr_ref_vector& trail, expr_ref_vector& result, unsigned depth, unsigned budget);
+
     public:
         lookahead(context& ctx);
 
-        expr_ref choose();
+        expr_ref choose(unsigned budget = 2000);
+
+        expr_ref_vector choose_rec(unsigned depth);
+
     };
 }
diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp
index 1ef4ffcf4..45cb6fc30 100644
--- a/src/smt/smt_parallel.cpp
+++ b/src/smt/smt_parallel.cpp
@@ -136,6 +136,7 @@ namespace smt {
                 }
                 unit_lim[i] = sz;
             }
+            IF_VERBOSE(1, verbose_stream() << "(smt.thread :units " << sz << ")\n");
         };
 
         std::mutex mux;
@@ -148,12 +149,12 @@ namespace smt {
                 expr_ref c(pm);
 
                 pctx.get_fparams().m_max_conflicts = std::min(thread_max_conflicts, max_conflicts);
-                if (num_rounds > 0) {
+                if (num_rounds > 0 && (pctx.get_fparams().m_threads_cube_frequency % num_rounds) == 0) {
                     cube(pctx, lasms, c);
                 }
                 IF_VERBOSE(1, verbose_stream() << "(smt.thread " << i; 
                            if (num_rounds > 0) verbose_stream() << " :round " << num_rounds;
-                           if (c) verbose_stream() << " :cube: " << mk_bounded_pp(c, pm, 3);
+                           if (c) verbose_stream() << " :cube " << mk_bounded_pp(c, pm, 3);
                            verbose_stream() << ")\n";);
                 lbool r = pctx.check(lasms.size(), lasms.c_ptr());
                 
@@ -164,6 +165,7 @@ namespace smt {
                     return;
                 }                
                 else if (r == l_false && pctx.unsat_core().contains(c)) {
+                    IF_VERBOSE(1, verbose_stream() << "(smt.thread " << i << " :learn " << mk_bounded_pp(c, pm, 3) << ")");
                     pctx.assert_expr(mk_not(mk_and(pctx.unsat_core())));
                     return;
                 } 
diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp
index 2ebd0c967..495448eeb 100644
--- a/src/smt/smt_solver.cpp
+++ b/src/smt/smt_solver.cpp
@@ -34,25 +34,26 @@ namespace {
         struct cuber {
             smt_solver& m_solver;
             unsigned    m_round;
-            expr_ref    m_result;
+            expr_ref_vector  m_result;
+            unsigned    m_depth;
             cuber(smt_solver& s):
                 m_solver(s),
                 m_round(0),
-                m_result(s.get_manager()) {}
+                m_result(s.get_manager()),
+                m_depth(s.m_smt_params.m_cube_depth) {}
             expr_ref cube() {
-                switch (m_round) {
-                case 0:
-                    m_result = m_solver.m_context.next_cube();
-                    break;
-                case 1:
-                    m_result = m_solver.get_manager().mk_not(m_result);
-                    break;
-                default:
-                    m_result = m_solver.get_manager().mk_false();
-                    break;
+                if (m_round == 0) {
+                    m_result = m_solver.m_context.cubes(m_depth);
+                }
+                expr_ref r(m_result.m());
+                if (m_round < m_result.size()) {
+                    r = m_result.get(m_round);
+                }
+                else {
+                    r = m_result.m().mk_false();
                 }
                 ++m_round;
-                return m_result;
+                return r;
             }
         };
 
diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp
index cfc75d0c6..c0218fdf8 100644
--- a/src/smt/theory_bv.cpp
+++ b/src/smt/theory_bv.cpp
@@ -24,7 +24,6 @@ Revision History:
 #include "smt/smt_model_generator.h"
 #include "util/stats.h"
 
-#define WATCH_DISEQ 0
 
 namespace smt {
 
@@ -222,25 +221,25 @@ namespace smt {
        \brief v1[idx] = ~v2[idx], then v1 /= v2 is a theory axiom.
     */
     void theory_bv::mk_new_diseq_axiom(theory_var v1, theory_var v2, unsigned idx) {
+        if (!params().m_bv_eq_axioms)
+            return;
         SASSERT(m_bits[v1][idx] == ~m_bits[v2][idx]);
         TRACE("bv_diseq_axiom", tout << "found new diseq axiom\n"; display_var(tout, v1); display_var(tout, v2););
         // found new disequality
         m_stats.m_num_diseq_static++;
-        enode * e1       = get_enode(v1);
-        enode * e2       = get_enode(v2);
-        literal l        = ~(mk_eq(e1->get_owner(), e2->get_owner(), true));
-        expr * eq        = ctx.bool_var2expr(l.var());
-        if (m.has_trace_stream()) {
-            app_ref body(m);
-            body = m.mk_implies(m.mk_eq(mk_bit2bool(get_enode(v1)->get_owner(), idx), m.mk_not(mk_bit2bool(get_enode(v2)->get_owner(), idx))), m.mk_not(eq));
-            log_axiom_instantiation(body);
-        }
+        app * e1       = get_expr(v1);
+        app * e2       = get_expr(v2);
+        literal l       = ~(mk_eq(e1, e2, true));
+        expr * eq       = ctx.bool_var2expr(l.var());
+        std::function<expr*(void)> logfn = [&]() {
+            return m.mk_implies(m.mk_eq(mk_bit2bool(e1, idx), m.mk_not(mk_bit2bool(e2, idx))), m.mk_not(eq));
+        };
+        scoped_trace_stream ts(*this, logfn);
         ctx.mk_th_axiom(get_id(), 1, &l);
-        if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
         if (ctx.relevancy()) {
-            relevancy_eh * eh = ctx.mk_relevancy_eh(pair_relevancy_eh(e1->get_owner(), e2->get_owner(), eq));
-            ctx.add_relevancy_eh(e1->get_owner(), eh);
-            ctx.add_relevancy_eh(e2->get_owner(), eh);
+            relevancy_eh * eh = ctx.mk_relevancy_eh(pair_relevancy_eh(e1, e2, eq));
+            ctx.add_relevancy_eh(e1, eh);
+            ctx.add_relevancy_eh(e2, eh);
         }
     }
 
@@ -421,6 +420,9 @@ namespace smt {
     };
 
     void theory_bv::add_fixed_eq(theory_var v1, theory_var v2) {
+        if (!params().m_bv_eq_axioms)
+            return;
+
         if (v1 > v2) {
             std::swap(v1, v2);
         }
@@ -445,17 +447,15 @@ namespace smt {
             e1 = mk_bit2bool(o1, i);
             e2 = mk_bit2bool(o2, i);
             literal eq = mk_eq(e1, e2, true);
-            if (m.has_trace_stream()) {
-                app_ref body(m);
-                body = m.mk_implies(m.mk_not(ctx.bool_var2expr(eq.var())), m.mk_not(ctx.bool_var2expr(oeq.var())));
-                log_axiom_instantiation(body);
-            }
+            std::function<expr*()> logfn = [&]() {
+                return m.mk_implies(m.mk_not(ctx.bool_var2expr(eq.var())), m.mk_not(ctx.bool_var2expr(oeq.var())));
+            };
+            scoped_trace_stream st(*this, logfn);
             ctx.mk_th_axiom(get_id(),  l1, ~l2, ~eq);
             ctx.mk_th_axiom(get_id(), ~l1,  l2, ~eq);
             ctx.mk_th_axiom(get_id(),  l1,  l2,  eq);
             ctx.mk_th_axiom(get_id(), ~l1, ~l2,  eq);
             ctx.mk_th_axiom(get_id(), eq, ~oeq);
-            if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
             eqs.push_back(~eq);
         }
         eqs.push_back(oeq);
@@ -497,15 +497,21 @@ namespace smt {
 
     bool theory_bv::get_fixed_value(theory_var v, numeral & result)  const {
         result.reset();
-        literal_vector const & bits        = m_bits[v];
-        literal_vector::const_iterator it  = bits.begin();
-        literal_vector::const_iterator end = bits.end();
-        for (unsigned i = 0; it != end; ++it, ++i) {
-            switch (ctx.get_assignment(*it)) {
-            case l_false: break;
-            case l_undef: return false; 
-            case l_true:  result += m_bb.power(i); break;
+        unsigned i = 0;
+        for (literal b : m_bits[v]) {
+            switch (ctx.get_assignment(b)) {
+            case l_false: 
+                break;
+            case l_undef: 
+                return false; 
+            case l_true:  {
+                for (unsigned j = m_power2.size(); j <= i; ++j) 
+                    m_power2.push_back(m_bb.power(j));
+                result += m_power2[i];
+                break;
             }
+            }
+            ++i;
         }
         return true;
     }
@@ -1095,6 +1101,9 @@ namespace smt {
     }
 
     void theory_bv::expand_diseq(theory_var v1, theory_var v2) {
+        if (!params().m_bv_eq_axioms)
+            return;
+
         SASSERT(get_bv_size(v1) == get_bv_size(v2));
         if (v1 > v2) {
             std::swap(v1, v2);
@@ -1114,37 +1123,36 @@ namespace smt {
             }
         }
 
-#if WATCH_DISEQ
-        bool_var watch_var = null_bool_var;
-        it1 = bits1.begin();
-        it2 = bits2.begin();
-        unsigned h = hash_u_u(v1, v2);
-        unsigned act = m_diseq_activity[hash_u_u(v1, v2) & 0xFF]++;
-
-        for (; it1 != end1 && ((act & 0x3) != 0x3); ++it1, ++it2) {
-            lbool val1 = ctx.get_assignment(*it1);
-            lbool val2 = ctx.get_assignment(*it2);
-        
-            if (val1 == l_undef) {
-                watch_var = it1->var();
+        if (params().m_bv_watch_diseq) {
+            bool_var watch_var = null_bool_var;
+            it1 = bits1.begin();
+            it2 = bits2.begin();
+            unsigned h = hash_u_u(v1, v2);
+            unsigned act = m_diseq_activity[hash_u_u(v1, v2) & 0xFF]++;
+            
+            for (; it1 != end1 && ((act & 0x3) != 0x3); ++it1, ++it2) {
+                lbool val1 = ctx.get_assignment(*it1);
+                lbool val2 = ctx.get_assignment(*it2);
+                
+                if (val1 == l_undef) {
+                    watch_var = it1->var();
+                }
+                else if (val2 == l_undef) {
+                    watch_var = it2->var();
+                }
+                else {
+                    continue;
+                }
+                
+                m_diseq_watch.reserve(watch_var+1);
+                m_diseq_watch[watch_var].push_back(std::make_pair(v1, v2));
+                m_diseq_watch_trail.push_back(watch_var);
+                return;
+                //m_replay_diseq.push_back(std::make_pair(v1, v2));            
             }
-            else if (val2 == l_undef) {
-                watch_var = it2->var();
-            }
-            else {
-                continue;
-            }
-
-            m_diseq_watch.reserve(watch_var+1);
-            m_diseq_watch[watch_var].push_back(std::make_pair(v1, v2));
-            m_diseq_watch_trail.push_back(watch_var);
-            return;
-            //m_replay_diseq.push_back(std::make_pair(v1, v2));            
         }
-#endif
 
         literal_vector & lits = m_tmp_literals;
-        expr_ref_vector exprs(m);
         lits.reset();
         literal eq = mk_eq(get_enode(v1)->get_owner(), get_enode(v2)->get_owner(), true);
         lits.push_back(eq);
@@ -1158,30 +1166,16 @@ namespace smt {
             ctx.internalize(diff, true);
             literal arg = ctx.get_literal(diff);
             lits.push_back(arg);
-            exprs.push_back(std::move(diff));
         }
         m_stats.m_num_diseq_dynamic++;
-        if (m.has_trace_stream()) {
-            app_ref body(m);
-            body = m.mk_implies(m.mk_not(ctx.bool_var2expr(eq.var())), m.mk_or(exprs.size(), exprs.c_ptr()));
-            log_axiom_instantiation(body);
-        }
+        scoped_trace_stream st(*this, lits);
         ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
-        if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
     }
 
     void theory_bv::assign_eh(bool_var v, bool is_true) {
         atom * a      = get_bv2a(v);
         TRACE("bv", tout << "assert: p" << v << " #" << ctx.bool_var2expr(v)->get_id() << " is_true: " << is_true << "\n";);
         if (a->is_bit()) {
-            // The following optimization is not correct.
-            // Boolean variables created for performing bit-blasting are reused.
-            // See regression\trevor6.smt for example.
-            // 
-            // if (ctx.has_th_justification(v, get_id())) {
-            //    TRACE("bv", tout << "has th_justification\n";);
-            //    return;
-            // }
             m_prop_queue.reset();
             bit_atom * b = static_cast<bit_atom*>(a);
             var_pos_occ * curr = b->m_occs;
@@ -1191,8 +1185,7 @@ namespace smt {
             }
             propagate_bits();
 
-#if WATCH_DISEQ
-            if (!ctx.inconsistent() && m_diseq_watch.size() > static_cast<unsigned>(v)) {
+            if (params().m_bv_watch_diseq && !ctx.inconsistent() && m_diseq_watch.size() > static_cast<unsigned>(v)) {
                 unsigned sz = m_diseq_watch[v].size();
                 for (unsigned i = 0; i < sz; ++i) {
                     auto const & p = m_diseq_watch[v][i];
@@ -1200,7 +1193,6 @@ namespace smt {
                 }
                 m_diseq_watch[v].reset();
             }
-#endif
         }
     }
     
@@ -1269,26 +1261,28 @@ namespace smt {
         }
         else {
             ctx.assign(consequent, mk_bit_eq_justification(v1, v2, consequent, antecedent));
-            literal_vector lits;
-            lits.push_back(~consequent);
-            lits.push_back(antecedent);
-            literal eq = mk_eq(get_enode(v1)->get_owner(), get_enode(v2)->get_owner(), false);
-            lits.push_back(~eq);
-            //
-            // Issue #3035:
-            // merge_eh invokes assign_bit, which updates the propagation queue and includes the 
-            // theory axiom for the propagated equality. When relevancy is non-zero, propagation may get
-            // lost on backtracking because the propagation queue is reset on conflicts.
-            // An alternative approach is to ensure the propagation queue is chronological with
-            // backtracking scopes (ie., it doesn't get reset, but shrunk to a previous level, and similar
-            // with a qhead indicator.
-            // 
-            ctx.mark_as_relevant(lits[0]);
-            ctx.mark_as_relevant(lits[1]);
-            ctx.mark_as_relevant(lits[2]);
-            {
-                scoped_trace_stream _sts(*this, lits);
-                ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
+            if (params().m_bv_eq_axioms) {
+                literal_vector lits;
+                lits.push_back(~consequent);
+                lits.push_back(antecedent);
+                literal eq = mk_eq(get_expr(v1), get_expr(v2), false);
+                lits.push_back(~eq);
+                //
+                // Issue #3035:
+                // merge_eh invokes assign_bit, which updates the propagation queue and includes the 
+                // theory axiom for the propagated equality. When relevancy is non-zero, propagation may get
+                // lost on backtracking because the propagation queue is reset on conflicts.
+                // An alternative approach is to ensure the propagation queue is chronological with
+                // backtracking scopes (ie., it doesn't get reset, but shrunk to a previous level, and similar
+                // with a qhead indicator.
+                // 
+                ctx.mark_as_relevant(lits[0]);
+                ctx.mark_as_relevant(lits[1]);
+                ctx.mark_as_relevant(lits[2]);
+                {
+                    scoped_trace_stream _sts(*this, lits);
+                    ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
+                }
             }
      
             if (m_wpos[v2] == idx)
@@ -1353,9 +1347,7 @@ namespace smt {
         theory::push_scope_eh();
         m_trail_stack.push_scope();
         // check_invariant();
-#if WATCH_DISEQ
         m_diseq_watch_lim.push_back(m_diseq_watch_trail.size());
-#endif
     }
     
     void theory_bv::pop_scope_eh(unsigned num_scopes) {
@@ -1364,7 +1356,6 @@ namespace smt {
         m_bits.shrink(num_old_vars);
         m_wpos.shrink(num_old_vars);
         m_zero_one_bits.shrink(num_old_vars);
-#if WATCH_DISEQ
         unsigned old_trail_sz = m_diseq_watch_lim[m_diseq_watch_lim.size()-num_scopes];
         for (unsigned i = m_diseq_watch_trail.size(); i-- > old_trail_sz;) {
             if (!m_diseq_watch[m_diseq_watch_trail[i]].empty()) {
@@ -1373,7 +1364,6 @@ namespace smt {
         }
         m_diseq_watch_trail.shrink(old_trail_sz);
         m_diseq_watch_lim.shrink(m_diseq_watch_lim.size()-num_scopes);
-#endif
         theory::pop_scope_eh(num_scopes);
         TRACE("bv_verbose", m_find.display(tout << ctx.get_scope_level() << " - " 
                                    << num_scopes << " = " << (ctx.get_scope_level() - num_scopes) << "\n"););
@@ -1422,9 +1412,7 @@ namespace smt {
         m_find(*this),
         m_approximates_large_bvs(false) {
         memset(m_eq_activity, 0, sizeof(m_eq_activity));
-#if WATCH_DISEQ
         memset(m_diseq_activity, 0, sizeof(m_diseq_activity));
-#endif
     }
 
     theory_bv::~theory_bv() {
@@ -1517,9 +1505,11 @@ namespace smt {
         m_merge_aux[0].reserve(bv_size+1, null_theory_var);
         m_merge_aux[1].reserve(bv_size+1, null_theory_var);
 
-#define RESET_MERGET_AUX()  for (auto & zo : bits1) m_merge_aux[zo.m_is_true][zo.m_idx] = null_theory_var; 
+        auto reset_merge_aux = [&]() { for (auto & zo : bits1) m_merge_aux[zo.m_is_true][zo.m_idx] = null_theory_var; };
 
-        DEBUG_CODE(for (unsigned i = 0; i < bv_size; i++) { SASSERT(m_merge_aux[0][i] == null_theory_var || m_merge_aux[1][i] == null_theory_var); });
+        DEBUG_CODE(for (unsigned i = 0; i < bv_size; i++) { 
+                SASSERT(m_merge_aux[0][i] == null_theory_var || m_merge_aux[1][i] == null_theory_var); }
+            );
         // save info about bits1
         for (auto & zo : bits1) m_merge_aux[zo.m_is_true][zo.m_idx] = zo.m_owner;
         // check if bits2 is consistent with bits1, and copy new bits to bits1
@@ -1531,7 +1521,7 @@ namespace smt {
                 SASSERT(m_bits[v1][zo.m_idx] == ~(m_bits[v2][zo.m_idx]));
                 SASSERT(m_bits[v1].size() == m_bits[v2].size());
                 mk_new_diseq_axiom(v1, v2, zo.m_idx);
-                RESET_MERGET_AUX();
+                reset_merge_aux();
                 return false;
             }
             if (m_merge_aux[zo.m_is_true][zo.m_idx] == null_theory_var) {
@@ -1540,7 +1530,7 @@ namespace smt {
             }
         }
         // reset m_merge_aux vector
-        RESET_MERGET_AUX();
+        reset_merge_aux();
         DEBUG_CODE(for (unsigned i = 0; i < bv_size; i++) { SASSERT(m_merge_aux[0][i] == null_theory_var || m_merge_aux[1][i] == null_theory_var); });
         return true;
     }
diff --git a/src/smt/theory_bv.h b/src/smt/theory_bv.h
index 1f309331d..bb4385114 100644
--- a/src/smt/theory_bv.h
+++ b/src/smt/theory_bv.h
@@ -122,13 +122,14 @@ namespace smt {
         typedef map<value_sort_pair, theory_var, value_sort_pair_hash, default_eq<value_sort_pair> > value2var;
 
         value2var                m_fixed_var_table;
+        mutable vector<rational>         m_power2;
         
         unsigned char            m_eq_activity[256];
-        //unsigned char            m_diseq_activity[256];
         svector<std::pair<theory_var, theory_var>> m_replay_diseq;
-        //vector<vector<std::pair<theory_var, theory_var>>> m_diseq_watch;
-        //svector<bool_var> m_diseq_watch_trail;
-        //unsigned_vector   m_diseq_watch_lim;
+        vector<vector<std::pair<theory_var, theory_var>>> m_diseq_watch;
+        unsigned char            m_diseq_activity[256];
+        svector<bool_var> m_diseq_watch_trail;
+        unsigned_vector   m_diseq_watch_lim;
 
         literal_vector           m_tmp_literals;
         svector<var_pos>         m_prop_queue;
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 88219d3e1..2ebcb9689 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -1007,10 +1007,6 @@ public:
         lp().settings().int_run_gcd_test() = ctx().get_fparams().m_arith_gcd_test;
         lp().settings().set_random_seed(ctx().get_fparams().m_random_seed);
         m_lia = alloc(lp::int_solver, *m_solver.get());
-        get_one(true);
-        get_zero(true);
-        get_one(false);
-        get_zero(false);
     }
         
     void internalize_is_int(app * n) {
diff --git a/src/solver/parallel_tactic.cpp b/src/solver/parallel_tactic.cpp
index 7dc1d06d3..8e3c3bb97 100644
--- a/src/solver/parallel_tactic.cpp
+++ b/src/solver/parallel_tactic.cpp
@@ -146,9 +146,18 @@ class parallel_tactic : public tactic {
             }
         }
 
+        void stats(::statistics& st) {
+            for (auto* t : m_tasks) 
+                t->get_solver().collect_statistics(st);
+            for (auto* t : m_active) 
+                t->get_solver().collect_statistics(st);
+        }
+
         void reset() {
-            for (auto* t : m_tasks) dealloc(t);
-            for (auto* t : m_active) dealloc(t);
+            for (auto* t : m_tasks) 
+                dealloc(t);
+            for (auto* t : m_active) 
+                dealloc(t);
             m_tasks.reset();
             m_active.reset();
             m_num_waiters = 0;
@@ -270,6 +279,7 @@ class parallel_tactic : public tactic {
             set_simplify_params(true);         // retain blocked
             r = get_solver().check_sat(m_assumptions);
             if (r != l_undef) return r;
+            if (canceled()) return l_undef;
             IF_VERBOSE(2, verbose_stream() << "(parallel.tactic simplify-2)\n";);
             set_simplify_params(false);        // remove blocked
             r = get_solver().check_sat(m_assumptions);
@@ -317,17 +327,20 @@ class parallel_tactic : public tactic {
             double exp = pp.simplify_exp();
             exp = std::max(exp, 1.0);
             unsigned mult = static_cast<unsigned>(pow(exp, m_depth - 1));
+            unsigned max_conflicts = pp.simplify_max_conflicts();
+            if (max_conflicts < 1000000)
+                max_conflicts *= std::max(m_depth, 1u);
             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", m_depth > 2);
             p.set_bool("retain_blocked_clauses", retain_blocked);
-            p.set_uint("max_conflicts", pp.simplify_max_conflicts());
+            p.set_uint("max_conflicts", max_conflicts);
             if (m_depth > 1) p.set_uint("bce_delay", 0);
             get_solver().updt_params(p);
         }
 
         bool canceled() { 
-            return m_giveup ||! m().inc();
+            return m_giveup || !m().inc();
         }
 
         std::ostream& display(std::ostream& out) {
@@ -469,6 +482,7 @@ private:
         unsigned num_simplifications = 0;
 
     cube_again:
+        if (canceled(s)) return;
         // extract up to one cube and add it.
         cube.reset();
         cube.append(s.split_cubes(1));
@@ -640,7 +654,7 @@ private:
     void run_solver() {
         try {
             while (solver_state* st = m_queue.get_task()) {
-                cube_and_conquer(*st);
+                cube_and_conquer(*st);                
                 collect_statistics(*st);
                 m_queue.task_done(st);
                 if (!st->m().inc()) m_queue.shutdown();
@@ -648,7 +662,7 @@ private:
                 dealloc(st);
             }
         }
-        catch (z3_exception& ex) {            
+        catch (z3_exception& ex) {   
             IF_VERBOSE(1, verbose_stream() << ex.msg() << "\n";);
             if (m_queue.in_shutdown()) return;
             m_queue.shutdown();
@@ -679,6 +693,7 @@ private:
             threads.push_back(std::thread([this]() { run_solver(); }));
         for (std::thread& t : threads) 
             t.join();
+        m_queue.stats(m_stats);
         m_manager.limit().reset_cancel();
         if (m_exn_code == -1) 
             throw default_exception(std::move(m_exn_msg));
@@ -720,7 +735,7 @@ public:
         init();
     }
 
-    void operator ()(const goal_ref & g,goal_ref_buffer & result) override {
+    void operator()(const goal_ref & g,goal_ref_buffer & result) override {
         cleanup();
         fail_if_proof_generation("parallel-tactic", g);
         ast_manager& m = g->m();        
@@ -773,7 +788,6 @@ public:
     void cleanup() override {
         m_queue.reset();
         m_models.reset();
-        m_stats.reset();
     }
 
     tactic* translate(ast_manager& m) override {