diff --git a/src/ast/expr2var.cpp b/src/ast/expr2var.cpp
index 1f5a8fe5c..a0d93a620 100644
--- a/src/ast/expr2var.cpp
+++ b/src/ast/expr2var.cpp
@@ -73,5 +73,22 @@ void expr2var::reset() {
     dec_ref_map_keys(m(), m_mapping);
     SASSERT(m_mapping.empty());
     m_recent_exprs.reset();
+    m_recent_lim.reset();
     m_interpreted_vars = false;
 }
+
+void expr2var::push() {
+    m_recent_lim.push_back(m_recent_exprs.size());
+}
+
+void expr2var::pop(unsigned num_scopes) {
+    if (num_scopes > 0) {
+        unsigned sz = m_recent_lim[m_recent_lim.size() - num_scopes];
+        for (unsigned i = sz; i < m_recent_exprs.size(); ++i) {
+            m_mapping.erase(m_recent_exprs[i]);
+            m().dec_ref(m_recent_exprs[i]);
+        }
+        m_recent_exprs.shrink(sz);
+        m_recent_lim.shrink(m_recent_lim.size() - num_scopes);
+    }
+}
diff --git a/src/ast/expr2var.h b/src/ast/expr2var.h
index cbb02b66d..43d9c31f4 100644
--- a/src/ast/expr2var.h
+++ b/src/ast/expr2var.h
@@ -39,6 +39,7 @@ protected:
     ast_manager &    m_manager;
     expr2var_mapping m_mapping;
     ptr_vector<expr> m_recent_exprs;
+    unsigned_vector  m_recent_lim;
     bool             m_interpreted_vars;
 public:
     expr2var(ast_manager & m);
@@ -62,7 +63,7 @@ public:
     iterator begin() const { return m_mapping.begin(); }
     iterator end() const { return m_mapping.end(); }
 
-    void reset_recent() { m_recent_exprs.reset(); }
+    void reset_recent() { SASSERT(m_recent_lim.empty()); m_recent_exprs.reset(); }
 
     // Iterators for traversing the recently registered expressions.
     // The set of recent registered expressions is reset by using reset_recent().
@@ -70,6 +71,9 @@ public:
     recent_iterator end_recent() const { return m_recent_exprs.end(); }
     
     void reset();
+
+    void push();
+    void pop(unsigned num_scopes);
 };
 
 #endif
diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp
index 63843d31e..0d78a8dc4 100644
--- a/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp
+++ b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp
@@ -92,6 +92,9 @@ struct blaster_rewriter_cfg : public default_rewriter_cfg {
     expr_ref_vector                          m_out;
     obj_map<func_decl, expr*>                m_const2bits;
     expr_ref_vector                          m_bindings;
+    func_decl_ref_vector                     m_keys;
+    expr_ref_vector                          m_values;
+    unsigned_vector                          m_keyval_lim;
 
     bool                                     m_blast_mul;
     bool                                     m_blast_add;
@@ -116,12 +119,13 @@ struct blaster_rewriter_cfg : public default_rewriter_cfg {
         m_in1(m),
         m_in2(m),
         m_out(m),
-        m_bindings(m) {
+        m_bindings(m),
+        m_keys(m), 
+        m_values(m) {
         updt_params(p);
     }
 
     ~blaster_rewriter_cfg() {
-        dec_ref_map_key_values(m_manager, m_const2bits);
     }
 
     void updt_params(params_ref const & p) {
@@ -157,6 +161,24 @@ struct blaster_rewriter_cfg : public default_rewriter_cfg {
         }
     }
 
+    void push() {
+        m_keyval_lim.push_back(m_keys.size());
+    }
+
+    void pop(unsigned num_scopes) {
+        if (num_scopes > 0) {
+            unsigned new_sz = m_keyval_lim.size() - num_scopes;
+            unsigned lim = m_keyval_lim[new_sz];
+            for (unsigned i = m_keys.size(); i > lim; ) {
+                --i;
+                m_const2bits.remove(m_keys[i].get());
+            }
+            m_keys.resize(lim);
+            m_values.resize(lim);
+            m_keyval_lim.resize(new_sz);
+        }
+    }
+
     template<typename V>
     app * mk_mkbv(V const & bits) {
         return m().mk_app(butil().get_family_id(), OP_MKBV, bits.size(), bits.c_ptr());
@@ -180,8 +202,8 @@ struct blaster_rewriter_cfg : public default_rewriter_cfg {
         }
         r = mk_mkbv(m_out);
         m_const2bits.insert(f, r);
-        m_manager.inc_ref(f);
-        m_manager.inc_ref(r);
+        m_keys.push_back(f);
+        m_values.push_back(r);
         result = r;
     }
 
@@ -611,6 +633,8 @@ struct bit_blaster_rewriter::imp : public rewriter_tpl<blaster_rewriter_cfg> {
         m_cfg(m, m_blaster, p) {
         SASSERT(m_blaster.butil().get_family_id() == m.get_family_id("bv"));
     }
+    void push() { m_cfg.push(); }
+    void pop(unsigned s) { m_cfg.pop(s); }
 };
 
 bit_blaster_rewriter::bit_blaster_rewriter(ast_manager & m, params_ref const & p):
@@ -630,6 +654,14 @@ void bit_blaster_rewriter::set_cancel(bool f) {
     m_imp->m_blaster.set_cancel(f);
 }
 
+void bit_blaster_rewriter::push() {
+    m_imp->push();
+}
+
+void bit_blaster_rewriter::pop(unsigned num_scopes) {
+    m_imp->pop(num_scopes);
+}
+
 ast_manager & bit_blaster_rewriter::m() const {
     return m_imp->m();
 }
diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.h b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.h
index 8265d30e5..3b4715657 100644
--- a/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.h
+++ b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.h
@@ -36,6 +36,8 @@ public:
     void cleanup();
     obj_map<func_decl, expr*> const& const2bits() const; 
     void operator()(expr * e, expr_ref & result, proof_ref & result_proof);
+    void push();
+    void pop(unsigned num_scopes);
 };
 
 #endif
diff --git a/src/opt/opt_params.pyg b/src/opt/opt_params.pyg
index 65740acf2..37b9ff372 100644
--- a/src/opt/opt_params.pyg
+++ b/src/opt/opt_params.pyg
@@ -19,7 +19,7 @@ def_module_params('opt',
                           ('maxres.maximize_assignment', BOOL, False, 'find an MSS/MCS to improve current assignment'), 
                           ('maxres.max_correction_set_size', UINT, 3, 'allow generating correction set constraints up to maximal size'),
                           ('maxres.wmax', BOOL, False, 'use weighted theory solver to constrain upper bounds'),
-                          ('maxres.pivot_on_correction_set', BOOL, True, 'prefer reducing soft constraints if the current correction set is smaller than current core')
+                          ('maxres.pivot_on_correction_set', BOOL, True, 'reduce soft constraints if the current correction set is smaller than current core')
 
                           ))
 
diff --git a/src/sat/sat_simplifier.h b/src/sat/sat_simplifier.h
index 9a69ab779..85922cf7c 100644
--- a/src/sat/sat_simplifier.h
+++ b/src/sat/sat_simplifier.h
@@ -173,6 +173,7 @@ namespace sat {
         ~simplifier();
 
         void insert_todo(bool_var v) { m_elim_todo.insert(v); }
+        void reset_todo() { m_elim_todo.reset(); }
 
         void operator()(bool learned);
 
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index d3608f3ae..4c0318c22 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -97,7 +97,7 @@ namespace sat {
                     if (!it2->is_binary_non_learned_clause())
                         continue;
                     literal l2 = it2->get_literal();
-                    mk_clause(l, l2);
+                    mk_clause_core(l, l2);
                 }
             }
         }
@@ -111,7 +111,7 @@ namespace sat {
                 buffer.reset();
                 for (unsigned i = 0; i < c.size(); i++)
                     buffer.push_back(c[i]);
-                mk_clause(buffer);
+                mk_clause_core(buffer);
             }
         }
     }
@@ -553,7 +553,7 @@ namespace sat {
             m_cleaner.dec();
             SASSERT(!m_inconsistent);
             l = m_trail[m_qhead];
-            TRACE("sat_propagate", tout << "propagating: " << l << "\n";);
+            TRACE("sat_propagate", tout << "propagating: " << l << " " << m_justification[l.var()] << "\n";);
             m_qhead++;
             not_l = ~l;
             SASSERT(value(l) == l_true);
@@ -881,7 +881,7 @@ namespace sat {
 
     bool solver::check_inconsistent() {
         if (inconsistent()) {
-            if (tracking_assumptions()) 
+            if (tracking_assumptions() || !m_user_scope_literals.empty()) 
                 resolve_conflict();
             return true;
         }
@@ -919,7 +919,7 @@ namespace sat {
             assign(nlit, justification());                   
         }
 
-        if (weights) {
+        if (weights && !inconsistent()) {
             if (m_config.m_optimize_model) {
                 m_wsls.set_soft(num_lits, lits, weights);
             }
@@ -1033,7 +1033,7 @@ namespace sat {
             TRACE("opt", tout << "blocking soft correction set: " << m_blocker << "\n";); 
             IF_VERBOSE(11, verbose_stream() << "blocking " << m_blocker << "\n";);
             pop_to_base_level();
-            mk_clause(m_blocker);
+            mk_clause_core(m_blocker);
             return false;
         }
         return true;
@@ -1094,7 +1094,7 @@ namespace sat {
     }
 
     bool solver::tracking_assumptions() const {
-        return !m_assumptions.empty();
+        return !m_assumptions.empty() || !m_user_scope_literals.empty();
     }
 
     bool solver::is_assumption(literal l) const {
@@ -1648,6 +1648,7 @@ namespace sat {
             resolve_conflict_for_unsat_core();
             return false;
         }
+        
         if (m_conflict_lvl == 0) {
             return false;
         }
@@ -2568,16 +2569,10 @@ namespace sat {
 
     void solver::user_push() {
         literal lit;
-        if (m_user_scope_literal_pool.empty()) {
-            bool_var new_v = mk_var(true, false);
-            lit = literal(new_v, false);
-        }
-        else {
-            lit = m_user_scope_literal_pool.back();
-            m_user_scope_literal_pool.pop_back();
-        }
-        TRACE("sat", tout << "user_push: " << lit << "\n";);
+        bool_var new_v = mk_var(true, false);
+        lit = literal(new_v, false);
         m_user_scope_literals.push_back(lit);
+        TRACE("sat", tout << "user_push: " << lit << "\n";);
     }
 
     void solver::gc_lit(clause_vector &clauses, literal lit) {
@@ -2608,11 +2603,69 @@ namespace sat {
         }
     }
 
+    bool_var solver::max_var(bool learned, bool_var v) {
+        m_user_bin_clauses.reset();
+        collect_bin_clauses(m_user_bin_clauses, learned);
+        for (unsigned i = 0; i < m_user_bin_clauses.size(); ++i) {
+            literal l1 = m_user_bin_clauses[i].first;
+            literal l2 = m_user_bin_clauses[i].second;
+            if (l1.var() > v) v = l1.var();
+            if (l2.var() > v) v = l2.var();
+        }
+        return v;
+    }
+
+    bool_var solver::max_var(clause_vector& clauses, bool_var v) {
+        for (unsigned i = 0; i < clauses.size(); ++i) {
+            clause & c = *(clauses[i]);
+            literal* it = c.begin();
+            literal * end = c.end();
+            for (; it != end; ++it) {
+                if (it->var() > v) {
+                    v = it->var();
+                }
+            }
+        }
+        return v;
+    }
+
+    void solver::gc_var(bool_var v) {
+        if (v > 0) {
+            bool_var w = max_var(m_learned, v-1);
+            w = max_var(m_clauses, w);
+            w = max_var(true, w);
+            w = max_var(false, w);
+            for (unsigned i = 0; i < m_trail.size(); ++i) {
+                if (m_trail[i].var() > w) w = m_trail[i].var();
+            }
+            v = std::max(v, w + 1);
+        }
+        // v is an index of a variable that does not occur in solver state.
+        if (v < m_level.size()) {
+            for (bool_var i = v; i < m_level.size(); ++i) {
+                m_case_split_queue.del_var_eh(i);
+            }
+            m_watches.shrink(2*v);
+            m_assignment.shrink(2*v);
+            m_justification.shrink(v);
+            m_decision.shrink(v);
+            m_eliminated.shrink(v);
+            m_external.shrink(v);
+            m_activity.shrink(v);
+            m_level.shrink(v);
+            m_mark.shrink(v);
+            m_lit_mark.shrink(2*v);
+            m_phase.shrink(v);
+            m_prev_phase.shrink(v);
+            m_assigned_since_gc.shrink(v);
+            m_simplifier.reset_todo();
+        }
+    }
+
     void solver::user_pop(unsigned num_scopes) {
         pop_to_base_level();
         while (num_scopes > 0) {
             literal lit = m_user_scope_literals.back();
-            m_user_scope_literal_pool.push_back(lit);   
             m_user_scope_literals.pop_back();
             gc_lit(m_learned, lit);
             gc_lit(m_clauses, lit);
@@ -2620,6 +2673,14 @@ namespace sat {
             gc_bin(false, lit);
             TRACE("sat", tout << "gc: " << lit << "\n"; display(tout););
             --num_scopes;
+            for (unsigned i = 0; i < m_trail.size(); ++i) {
+                if (m_trail[i] == lit) {
+                    TRACE("sat", tout << m_trail << "\n";);
+                    unassign_vars(i);
+                    break;
+                }
+            }            
+            gc_var(lit.var());
         }
     }
 
diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h
index a49fb3c31..97a27502d 100644
--- a/src/sat/sat_solver.h
+++ b/src/sat/sat_solver.h
@@ -183,6 +183,9 @@ namespace sat {
     protected:
         void del_clause(clause & c);
         clause * mk_clause_core(unsigned num_lits, literal * lits, bool learned);
+        void mk_clause_core(literal_vector const& lits) { mk_clause_core(lits.size(), lits.c_ptr()); }
+        void mk_clause_core(unsigned num_lits, literal * lits) { mk_clause_core(num_lits, lits, false); }
+        void mk_clause_core(literal l1, literal l2) { literal lits[2] = { l1, l2 }; mk_clause_core(2, lits); }
         void mk_bin_clause(literal l1, literal l2, bool learned);
         bool propagate_bin_clause(literal l1, literal l2);
         clause * mk_ter_clause(literal * lits, bool learned);
@@ -400,11 +403,14 @@ namespace sat {
         void reinit_clauses(unsigned old_sz);
 
         literal_vector m_user_scope_literals;
-        literal_vector m_user_scope_literal_pool;
         literal_vector m_aux_literals;
         svector<bin_clause> m_user_bin_clauses;
         void gc_lit(clause_vector& clauses, literal lit);
         void gc_bin(bool learned, literal nlit);
+        void gc_var(bool_var v);
+        bool_var max_var(clause_vector& clauses, bool_var v);
+        bool_var max_var(bool learned, bool_var v);
+
     public:
         void user_push();
         void user_pop(unsigned num_scopes);
diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp
index 1b4063b17..a0eb5a7e2 100644
--- a/src/sat/sat_solver/inc_sat_solver.cpp
+++ b/src/sat/sat_solver/inc_sat_solver.cpp
@@ -31,6 +31,7 @@ Notes:
 #include "ast_pp.h"
 #include "model_smt2_pp.h"
 #include "filter_model_converter.h"
+#include "bit_blaster_model_converter.h"
 
 // incremental SAT solver.
 class inc_sat_solver : public solver {
@@ -48,7 +49,8 @@ class inc_sat_solver : public solver {
     expr_ref_vector     m_core;
     atom2bool_var       m_map;
     model_ref           m_model;
-    model_converter_ref m_mc;   
+    model_converter_ref m_mc;  
+    bit_blaster_rewriter m_bb_rewriter; 
     tactic_ref          m_preprocess;
     unsigned            m_num_scopes;
     sat::literal_vector m_asms;
@@ -67,6 +69,7 @@ public:
         m_asmsf(m),
         m_fmls_head(0),
         m_core(m), 
+        m_bb_rewriter(m, p),
         m_map(m),
         m_num_scopes(0), 
         m_dep_core(m) {
@@ -84,7 +87,7 @@ public:
             and_then(mk_card2bv_tactic(m, m_params),
                      using_params(mk_simplify_tactic(m), simp2_p),
                      mk_max_bv_sharing_tactic(m),
-                     mk_bit_blaster_tactic(m), 
+                     mk_bit_blaster_tactic(m, &m_bb_rewriter), 
                      mk_aig_tactic(),
                      using_params(mk_simplify_tactic(m), simp2_p));               
     }
@@ -157,11 +160,15 @@ public:
         m_fmls_lim.push_back(m_fmls.size());
         m_asms_lim.push_back(m_asmsf.size());
         m_fmls_head_lim.push_back(m_fmls_head);
+        m_bb_rewriter.push();
+        m_map.push();
     }
     virtual void pop(unsigned n) {
         if (n < m_num_scopes) {   // allow inc_sat_solver to 
             n = m_num_scopes;     // take over for another solver.
         }
+        m_bb_rewriter.pop(n);
+        m_map.pop(n);
         SASSERT(n >= m_num_scopes);
         m_solver.user_pop(n);        
         m_num_scopes -= n;
@@ -258,11 +265,11 @@ private:
             IF_VERBOSE(0, verbose_stream() << "exception in tactic " << ex.msg() << "\n";);
             return l_undef;                    
         }
-        m_mc = concat(m_mc.get(), m_mc2.get());
         if (m_subgoals.size() != 1) {
             IF_VERBOSE(0, verbose_stream() << "size of subgoals is not 1, it is: " << m_subgoals.size() << "\n";);
             return l_undef;
         }
+        CTRACE("sat", m_mc.get(), m_mc->display(tout); );
         g = m_subgoals[0];
         TRACE("sat", g->display_with_dependencies(tout););
         m_goal2sat(*g, m_params, m_solver, m_map, dep2asm, true);
@@ -384,8 +391,12 @@ private:
             }
         }
         m_model = md;
-        if (m_mc) {
-            (*m_mc)(m_model);
+        if (m_mc || !m_bb_rewriter.const2bits().empty()) {
+            model_converter_ref mc = m_mc;
+            if (!m_bb_rewriter.const2bits().empty()) {
+                mc = concat(mc.get(), mk_bit_blaster_model_converter(m, m_bb_rewriter.const2bits())); 
+            }
+            (*mc)(m_model);
         }
         SASSERT(m_model);
 
diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp
index ff201042b..9f066e33b 100644
--- a/src/sat/tactic/goal2sat.cpp
+++ b/src/sat/tactic/goal2sat.cpp
@@ -105,14 +105,14 @@ struct goal2sat::imp {
     }
 
     sat::bool_var mk_true() {
-        // create fake variable to represent true;
         if (m_true == sat::null_bool_var) {
+            // create fake variable to represent true;
             m_true = m_solver.mk_var();
             mk_clause(sat::literal(m_true, false)); // v is true
         }
         return m_true;
     }
-    
+
     void convert_atom(expr * t, bool root, bool sign) {
         SASSERT(m.is_bool(t));
         sat::literal  l;
@@ -515,6 +515,7 @@ void goal2sat::set_cancel(bool f) {
     }
 }
 
+
 struct sat2goal::imp {
 
     // Wrapper for sat::model_converter: converts it into an "AST level" model_converter.
diff --git a/src/sat/tactic/goal2sat.h b/src/sat/tactic/goal2sat.h
index a6b89564f..e1f78d916 100644
--- a/src/sat/tactic/goal2sat.h
+++ b/src/sat/tactic/goal2sat.h
@@ -60,6 +60,7 @@ public:
     void operator()(goal const & g, params_ref const & p, sat::solver & t, atom2bool_var & m, dep2asm_map& dep2asm, bool default_external = false);
 
     void set_cancel(bool f);
+
 };
 
 
diff --git a/src/tactic/bv/bit_blaster_model_converter.cpp b/src/tactic/bv/bit_blaster_model_converter.cpp
index 6c1c6911c..a18862ee8 100644
--- a/src/tactic/bv/bit_blaster_model_converter.cpp
+++ b/src/tactic/bv/bit_blaster_model_converter.cpp
@@ -98,6 +98,11 @@ struct bit_blaster_model_converter : public model_converter {
         SASSERT(m_vars.size() == m_bits.size());
         unsigned sz = m_vars.size();
         for (unsigned i = 0; i < sz; i++) {
+            expr* new_val = old_model->get_const_interp(m_vars.get(i));
+            if (new_val) {
+                new_model->register_decl(m_vars.get(i), new_val);
+                continue;
+            }
             expr * bs = m_bits.get(i);
             val.reset();
             unsigned bv_sz = to_app(bs)->get_num_args();
@@ -132,7 +137,7 @@ struct bit_blaster_model_converter : public model_converter {
                         val++;
                 }
             }
-            expr * new_val = util.mk_numeral(val, bv_sz);
+            new_val = util.mk_numeral(val, bv_sz);
             new_model->register_decl(m_vars.get(i), new_val);
         }
     }
diff --git a/src/tactic/bv/bit_blaster_tactic.cpp b/src/tactic/bv/bit_blaster_tactic.cpp
index 0391aad51..924843af0 100644
--- a/src/tactic/bv/bit_blaster_tactic.cpp
+++ b/src/tactic/bv/bit_blaster_tactic.cpp
@@ -25,13 +25,16 @@ Notes:
 
 class bit_blaster_tactic : public tactic {
 
-    struct imp {
-        bit_blaster_rewriter  m_rewriter;
-        unsigned              m_num_steps;
-        bool                  m_blast_quant;
 
-        imp(ast_manager & m, params_ref const & p):
-            m_rewriter(m, p) {
+    struct imp {
+        bit_blaster_rewriter   m_base_rewriter;
+        bit_blaster_rewriter*  m_rewriter;    
+        unsigned               m_num_steps;
+        bool                   m_blast_quant;
+
+        imp(ast_manager & m, bit_blaster_rewriter* rw, params_ref const & p):
+            m_base_rewriter(m, p),
+            m_rewriter(rw?rw:&m_base_rewriter) {
             updt_params(p);
         }
 
@@ -40,14 +43,14 @@ class bit_blaster_tactic : public tactic {
         }
 
         void updt_params(params_ref const & p) {
-            m_rewriter.updt_params(p);
+            m_rewriter->updt_params(p);
             updt_params_core(p);
         }
         
-        ast_manager & m() const { return m_rewriter.m(); }
+        ast_manager & m() const { return m_rewriter->m(); }
         
         void set_cancel(bool f) {
-            m_rewriter.set_cancel(f);
+            m_rewriter->set_cancel(f);
         }
 
         void operator()(goal_ref const & g, 
@@ -74,8 +77,8 @@ class bit_blaster_tactic : public tactic {
                 if (g->inconsistent())
                     break;
                 expr * curr = g->form(idx);
-                m_rewriter(curr, new_curr, new_pr);
-                m_num_steps += m_rewriter.get_num_steps();
+                (*m_rewriter)(curr, new_curr, new_pr);
+                m_num_steps += m_rewriter->get_num_steps();
                 if (proofs_enabled) {
                     proof * pr = g->pr(idx);
                     new_pr     = m().mk_modus_ponens(pr, new_pr);
@@ -88,29 +91,32 @@ class bit_blaster_tactic : public tactic {
             }
             
             if (change && g->models_enabled())  
-                mc = mk_bit_blaster_model_converter(m(), m_rewriter.const2bits());
+                mc = mk_bit_blaster_model_converter(m(), m_rewriter->const2bits());
             else
                 mc = 0;
             g->inc_depth();
             result.push_back(g.get());
             TRACE("after_bit_blaster", g->display(tout); if (mc) mc->display(tout); tout << "\n";);
-            m_rewriter.cleanup();
+            m_rewriter->cleanup();
         }
         
         unsigned get_num_steps() const { return m_num_steps; }
     };
-    
+
     imp *      m_imp;
+    bit_blaster_rewriter* m_rewriter;
     params_ref m_params;
 
 public:
-    bit_blaster_tactic(ast_manager & m, params_ref const & p):
-        m_params(p){
-        m_imp = alloc(imp, m, p);
+    bit_blaster_tactic(ast_manager & m, bit_blaster_rewriter* rw, params_ref const & p):
+        m_rewriter(rw),
+        m_params(p) {
+        m_imp = alloc(imp, m, m_rewriter, p);
     }
 
     virtual tactic * translate(ast_manager & m) {
-        return alloc(bit_blaster_tactic, m, m_params);
+        SASSERT(!m_rewriter); // assume translation isn't used where rewriter is external.
+        return alloc(bit_blaster_tactic, m, 0, m_params); 
     }
 
     virtual ~bit_blaster_tactic() {
@@ -145,7 +151,7 @@ public:
     }
 
     virtual void cleanup() {
-        imp * d = alloc(imp, m_imp->m(), m_params);
+        imp * d = alloc(imp, m_imp->m(), m_rewriter, m_params);
         #pragma omp critical (tactic_cancel)
         {
             std::swap(d, m_imp);
@@ -166,5 +172,9 @@ protected:
 
 
 tactic * mk_bit_blaster_tactic(ast_manager & m, params_ref const & p) {
-    return clean(alloc(bit_blaster_tactic, m, p));
+    return clean(alloc(bit_blaster_tactic, m, 0, p));
+}
+
+tactic * mk_bit_blaster_tactic(ast_manager & m, bit_blaster_rewriter* rw, params_ref const & p) {
+    return clean(alloc(bit_blaster_tactic, m, rw, p));
 }
diff --git a/src/tactic/bv/bit_blaster_tactic.h b/src/tactic/bv/bit_blaster_tactic.h
index 2c359ada4..cb7f6f7a9 100644
--- a/src/tactic/bv/bit_blaster_tactic.h
+++ b/src/tactic/bv/bit_blaster_tactic.h
@@ -20,10 +20,12 @@ Notes:
 #define BIT_BLASTER_TACTIC_H_
 
 #include"params.h"
+#include"bit_blaster_rewriter.h"
 class ast_manager;
 class tactic;
 
 tactic * mk_bit_blaster_tactic(ast_manager & m, params_ref const & p = params_ref());
+tactic * mk_bit_blaster_tactic(ast_manager & m, bit_blaster_rewriter* rw, params_ref const & p = params_ref());
 /*
   ADD_TACTIC("bit-blast", "reduce bit-vector expressions into SAT.", "mk_bit_blaster_tactic(m, p)")
 */
diff --git a/src/tactic/portfolio/smt_strategic_solver.cpp b/src/tactic/portfolio/smt_strategic_solver.cpp
index c868fdcb9..b128b9b1f 100644
--- a/src/tactic/portfolio/smt_strategic_solver.cpp
+++ b/src/tactic/portfolio/smt_strategic_solver.cpp
@@ -92,7 +92,7 @@ tactic * mk_tactic_for_logic(ast_manager & m, params_ref const & p, symbol const
         return mk_default_tactic(m, p);
 }
 
-solver* mk_solver_for_logic(ast_manager & m, params_ref const & p, symbol const& logic) {
+static solver* mk_solver_for_logic(ast_manager & m, params_ref const & p, symbol const& logic) {
     if (logic == "QF_BV") 
         return mk_inc_sat_solver(m, p);
     return mk_smt_solver(m, p, logic);
@@ -112,8 +112,8 @@ public:
             l = logic;
         tactic * t = mk_tactic_for_logic(m, p, l);
         return mk_combined_solver(mk_tactic2solver(m, t, p, proofs_enabled, models_enabled, unsat_core_enabled, l),
-                                  //mk_solver_for_logic(m, p, l), 
-                                  mk_smt_solver(m, p, l),
+                                  mk_solver_for_logic(m, p, l), 
+                                  //mk_smt_solver(m, p, l),
                                   p);
     }
 };