diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
index 785649e3d..1cfb10179 100644
--- a/src/api/python/z3/z3.py
+++ b/src/api/python/z3/z3.py
@@ -8266,7 +8266,7 @@ def tree_interpolant(pat,p=None,ctx=None):
     solver that determines satisfiability.
 
     >>> x = Int('x')
-    >>> y = Int('y')
+    >>> y = Int('y')	
     >>> print(tree_interpolant(And(Interpolant(x < 0), Interpolant(y > 2), x == y)))
     [Not(x >= 0), Not(y <= 2)]
 
diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp
index 444069d8c..ab9bb0895 100644
--- a/src/smt/asserted_formulas.cpp
+++ b/src/smt/asserted_formulas.cpp
@@ -27,8 +27,9 @@ Revision History:
 #include "ast/macros/quasi_macros.h"
 #include "smt/asserted_formulas.h"
 
-asserted_formulas::asserted_formulas(ast_manager & m, smt_params & p):
+asserted_formulas::asserted_formulas(ast_manager & m, smt_params & sp, params_ref const& p):
     m(m),
+    m_smt_params(sp),
     m_params(p),
     m_rewriter(m),
     m_substitution(m),
@@ -65,20 +66,20 @@ asserted_formulas::asserted_formulas(ast_manager & m, smt_params & p):
 }
 
 void asserted_formulas::setup() {
-    switch (m_params.m_lift_ite) {
+    switch (m_smt_params.m_lift_ite) {
     case LI_FULL:
-        m_params.m_ng_lift_ite = LI_NONE;
+        m_smt_params.m_ng_lift_ite = LI_NONE;
         break;
     case LI_CONSERVATIVE:
-        if (m_params.m_ng_lift_ite == LI_CONSERVATIVE)
-            m_params.m_ng_lift_ite = LI_NONE;
+        if (m_smt_params.m_ng_lift_ite == LI_CONSERVATIVE)
+            m_smt_params.m_ng_lift_ite = LI_NONE;
         break;
     default:
         break;
     }
 
-    if (m_params.m_relevancy_lvl == 0)
-        m_params.m_relevancy_lemma = false;
+    if (m_smt_params.m_relevancy_lvl == 0)
+        m_smt_params.m_relevancy_lemma = false;
 }
 
 
@@ -118,24 +119,23 @@ void asserted_formulas::push_assertion(expr * e, proof * pr, vector<justified_ex
 }
 
 void asserted_formulas::updt_params(params_ref const& p) {
-    m_rewriter.updt_params(p);
+    m_params.append(p);
 }
 
 void asserted_formulas::set_eliminate_and(bool flag) {
     if (flag == m_elim_and) return;
     m_elim_and = flag;
-    params_ref p;
-    if (m_params.m_pull_cheap_ite) p.set_bool("pull_cheap_ite", true);
-    p.set_bool("elim_and", flag);
-    p.set_bool("arith_ineq_lhs", true);
-    p.set_bool("sort_sums", true);
-    p.set_bool("rewrite_patterns", true);
-    p.set_bool("eq2ineq", m_params.m_arith_eq2ineq);
-    p.set_bool("gcd_rounding", true);
-    p.set_bool("expand_select_store", true);
-    p.set_bool("bv_sort_ac", true);
-    p.set_bool("som", true);
-    m_rewriter.updt_params(p);
+    if (m_smt_params.m_pull_cheap_ite) m_params.set_bool("pull_cheap_ite", true);
+    m_params.set_bool("elim_and", flag);
+    m_params.set_bool("arith_ineq_lhs", true);
+    m_params.set_bool("sort_sums", true);
+    m_params.set_bool("rewrite_patterns", true);
+    m_params.set_bool("eq2ineq", m_smt_params.m_arith_eq2ineq);
+    m_params.set_bool("gcd_rounding", true);
+    m_params.set_bool("expand_select_store", true);
+    m_params.set_bool("bv_sort_ac", true);
+    m_params.set_bool("som", true);
+    m_rewriter.updt_params(m_params);
     flush_cache();
 }
 
@@ -147,7 +147,7 @@ void asserted_formulas::assert_expr(expr * e, proof * _in_pr) {
     if (inconsistent())
         return;
 
-    if (m_params.m_preprocess) {
+    if (m_smt_params.m_preprocess) {
         TRACE("assert_expr_bug", tout << r << "\n";);
         set_eliminate_and(false); // do not eliminate and before nnf.
         m_rewriter(e, r, pr);
@@ -230,7 +230,7 @@ void asserted_formulas::reduce() {
         return;
     if (m_qhead == m_formulas.size())
         return;
-    if (!m_params.m_preprocess)
+    if (!m_smt_params.m_preprocess)
         return;
     if (m_macro_manager.has_macros())
         invoke(m_find_macros);
diff --git a/src/smt/asserted_formulas.h b/src/smt/asserted_formulas.h
index c2f2b6a97..9c82b1314 100644
--- a/src/smt/asserted_formulas.h
+++ b/src/smt/asserted_formulas.h
@@ -43,7 +43,8 @@ Revision History:
 class asserted_formulas {
     
     ast_manager &               m;
-    smt_params &                m_params;
+    smt_params &                m_smt_params;
+    params_ref                  m_params;
     th_rewriter                 m_rewriter;
     expr_substitution           m_substitution;
     scoped_expr_substitution    m_scoped_substitution;
@@ -88,7 +89,7 @@ class asserted_formulas {
     public:
         find_macros_fn(asserted_formulas& af): simplify_fmls(af, "find-macros") {}
         void operator()() override { af.find_macros_core(); }
-        bool should_apply() const override { return af.m_params.m_macro_finder && af.has_quantifiers(); }
+        bool should_apply() const override { return af.m_smt_params.m_macro_finder && af.has_quantifiers(); }
         void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) override { UNREACHABLE(); }
     };
 
@@ -96,7 +97,7 @@ class asserted_formulas {
     public:
         apply_quasi_macros_fn(asserted_formulas& af): simplify_fmls(af, "find-quasi-macros") {}
         void operator()() override { af.apply_quasi_macros(); }
-        bool should_apply() const override { return af.m_params.m_quasi_macros && af.has_quantifiers(); }
+        bool should_apply() const override { return af.m_smt_params.m_quasi_macros && af.has_quantifiers(); }
         void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) override { UNREACHABLE(); }
     };
 
@@ -104,7 +105,7 @@ class asserted_formulas {
     public:
         nnf_cnf_fn(asserted_formulas& af): simplify_fmls(af, "nnf-cnf") {}
         void operator()() override { af.nnf_cnf(); }
-        bool should_apply() const override { return af.m_params.m_nnf_cnf || (af.m_params.m_mbqi && af.has_quantifiers()); }
+        bool should_apply() const override { return af.m_smt_params.m_nnf_cnf || (af.m_smt_params.m_mbqi && af.has_quantifiers()); }
         void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) override { UNREACHABLE(); }
     };
 
@@ -112,7 +113,7 @@ class asserted_formulas {
     public:
         propagate_values_fn(asserted_formulas& af): simplify_fmls(af, "propagate-values") {}
         void operator()() override { af.propagate_values(); }
-        bool should_apply() const override { return af.m_params.m_propagate_values; }
+        bool should_apply() const override { return af.m_smt_params.m_propagate_values; }
         void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) override { UNREACHABLE(); }
     };
 
@@ -121,30 +122,30 @@ class asserted_formulas {
     public:
         distribute_forall_fn(asserted_formulas& af): simplify_fmls(af, "distribute-forall"), m_functor(af.m) {}
         void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) override { m_functor(j.get_fml(), n); }
-        bool should_apply() const override { return af.m_params.m_distribute_forall && af.has_quantifiers(); }
+        bool should_apply() const override { return af.m_smt_params.m_distribute_forall && af.has_quantifiers(); }
         void post_op() override { af.reduce_and_solve();  TRACE("asserted_formulas", af.display(tout);); }
     };
 
     class pattern_inference_fn : public simplify_fmls {
         pattern_inference_rw m_infer;
     public:
-        pattern_inference_fn(asserted_formulas& af): simplify_fmls(af, "pattern-inference"), m_infer(af.m, af.m_params) {}
+        pattern_inference_fn(asserted_formulas& af): simplify_fmls(af, "pattern-inference"), m_infer(af.m, af.m_smt_params) {}
         void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) override { m_infer(j.get_fml(), n, p); }
-        bool should_apply() const override { return af.m_params.m_ematching && af.has_quantifiers(); }
+        bool should_apply() const override { return af.m_smt_params.m_ematching && af.has_quantifiers(); }
     };
 
     class refine_inj_axiom_fn : public simplify_fmls {
     public:
         refine_inj_axiom_fn(asserted_formulas& af): simplify_fmls(af, "refine-injectivity") {}
         void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) override;
-        bool should_apply() const override { return af.m_params.m_refine_inj_axiom && af.has_quantifiers(); }
+        bool should_apply() const override { return af.m_smt_params.m_refine_inj_axiom && af.has_quantifiers(); }
     };
 
     class max_bv_sharing_fn : public simplify_fmls {
     public:
         max_bv_sharing_fn(asserted_formulas& af): simplify_fmls(af, "maximizing-bv-sharing") {}
         void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) override { af.m_bv_sharing(j.get_fml(), n, p); }
-        bool should_apply() const override { return af.m_params.m_max_bv_sharing; }
+        bool should_apply() const override { return af.m_smt_params.m_max_bv_sharing; }
         void post_op() override { af.m_reduce_asserted_formulas(); }
     };
 
@@ -153,7 +154,7 @@ class asserted_formulas {
     public:
         elim_term_ite_fn(asserted_formulas& af): simplify_fmls(af, "elim-term-ite"), m_elim(af.m, af.m_defined_names) {}
         void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) override { m_elim(j.get_fml(), n, p); }
-        bool should_apply() const override { return af.m_params.m_eliminate_term_ite && af.m_params.m_lift_ite != LI_FULL; }
+        bool should_apply() const override { return af.m_smt_params.m_eliminate_term_ite && af.m_smt_params.m_lift_ite != LI_FULL; }
         void post_op() override { af.m_formulas.append(m_elim.new_defs()); af.reduce_and_solve(); m_elim.reset(); }
     };
 
@@ -171,12 +172,12 @@ class asserted_formulas {
 
 #define MK_SIMPLIFIERF(NAME, FUNCTOR, MSG, APP, REDUCE) MK_SIMPLIFIERA(NAME, FUNCTOR, MSG, APP, (af.m), REDUCE)
 
-    MK_SIMPLIFIERF(pull_nested_quantifiers, pull_nested_quant, "pull-nested-quantifiers", af.m_params.m_pull_nested_quantifiers && af.has_quantifiers(), false);
-    MK_SIMPLIFIERF(cheap_quant_fourier_motzkin, elim_bounds_rw, "cheap-fourier-motzkin", af.m_params.m_eliminate_bounds && af.has_quantifiers(), true);
-    MK_SIMPLIFIERF(elim_bvs_from_quantifiers, bv_elim_rw, "eliminate-bit-vectors-from-quantifiers", af.m_params.m_bb_quantifiers, true);
-    MK_SIMPLIFIERF(apply_bit2int, bit2int, "propagate-bit-vector-over-integers", af.m_params.m_simplify_bit2int, true);
-    MK_SIMPLIFIERA(lift_ite, push_app_ite_rw, "lift-ite", af.m_params.m_lift_ite != LI_NONE, (af.m, af.m_params.m_lift_ite == LI_CONSERVATIVE), true);
-    MK_SIMPLIFIERA(ng_lift_ite, ng_push_app_ite_rw, "lift-ite", af.m_params.m_ng_lift_ite != LI_NONE, (af.m, af.m_params.m_ng_lift_ite == LI_CONSERVATIVE), true);
+    MK_SIMPLIFIERF(pull_nested_quantifiers, pull_nested_quant, "pull-nested-quantifiers", af.m_smt_params.m_pull_nested_quantifiers && af.has_quantifiers(), false);
+    MK_SIMPLIFIERF(cheap_quant_fourier_motzkin, elim_bounds_rw, "cheap-fourier-motzkin", af.m_smt_params.m_eliminate_bounds && af.has_quantifiers(), true);
+    MK_SIMPLIFIERF(elim_bvs_from_quantifiers, bv_elim_rw, "eliminate-bit-vectors-from-quantifiers", af.m_smt_params.m_bb_quantifiers, true);
+    MK_SIMPLIFIERF(apply_bit2int, bit2int, "propagate-bit-vector-over-integers", af.m_smt_params.m_simplify_bit2int, true);
+    MK_SIMPLIFIERA(lift_ite, push_app_ite_rw, "lift-ite", af.m_smt_params.m_lift_ite != LI_NONE, (af.m, af.m_smt_params.m_lift_ite == LI_CONSERVATIVE), true);
+    MK_SIMPLIFIERA(ng_lift_ite, ng_push_app_ite_rw, "lift-ite", af.m_smt_params.m_ng_lift_ite != LI_NONE, (af.m, af.m_smt_params.m_ng_lift_ite == LI_CONSERVATIVE), true);
 
 
     reduce_asserted_formulas_fn m_reduce_asserted_formulas;
@@ -220,7 +221,7 @@ class asserted_formulas {
     void init(unsigned num_formulas, expr * const * formulas, proof * const * prs);
 
 public:
-    asserted_formulas(ast_manager & m, smt_params & p);
+    asserted_formulas(ast_manager & m, smt_params & smtp, params_ref const& p);
     ~asserted_formulas();
 
     void updt_params(params_ref const& p);
diff --git a/src/smt/mam.cpp b/src/smt/mam.cpp
index 5c881684f..d31cbc905 100644
--- a/src/smt/mam.cpp
+++ b/src/smt/mam.cpp
@@ -3924,7 +3924,7 @@ namespace smt {
         }
 
 #ifdef Z3DEBUG
-        virtual bool check_missing_instances() {
+        bool check_missing_instances() override {
             TRACE("missing_instance", tout << "checking for missing instances...\n";);
             flet<bool> l(m_check_missing_instances, true);
             rematch(false);
diff --git a/src/smt/params/preprocessor_params.cpp b/src/smt/params/preprocessor_params.cpp
index 57b11e7fd..ee4b7c2e4 100644
--- a/src/smt/params/preprocessor_params.cpp
+++ b/src/smt/params/preprocessor_params.cpp
@@ -25,7 +25,6 @@ void preprocessor_params::updt_local_params(params_ref const & _p) {
     m_quasi_macros            = p.quasi_macros();
     m_restricted_quasi_macros = p.restricted_quasi_macros();
     m_pull_nested_quantifiers = p.pull_nested_quantifiers();
-//    m_pull_cheap_ite          = _p.get_bool("pull_cheap_ite", m_pull_cheap_ite);
     m_refine_inj_axiom        = p.refine_inj_axioms();
 }
 
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 513bf7665..e20eae0bd 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -45,7 +45,7 @@ namespace smt {
         m_fparams(p),
         m_params(_p),
         m_setup(*this, p),
-        m_asserted_formulas(m, p),
+        m_asserted_formulas(m, p, _p),
         m_qmanager(alloc(quantifier_manager, *this, p, _p)),
         m_model_generator(alloc(model_generator, m)),
         m_relevancy_propagator(mk_relevancy_propagator(*this)),
diff --git a/src/smt/smt_relevancy.cpp b/src/smt/smt_relevancy.cpp
index 9eabb8319..7db5110ee 100644
--- a/src/smt/smt_relevancy.cpp
+++ b/src/smt/smt_relevancy.cpp
@@ -527,7 +527,7 @@ namespace smt {
         }
 
 #ifdef Z3DEBUG
-        bool check_relevancy_app(app * n) const {
+        bool check_relevancy_app(app * n) const  {
             SASSERT(is_relevant(n));
             unsigned num_args = n->get_num_args();
             for (unsigned i = 0; i < num_args; i++) {
@@ -537,7 +537,7 @@ namespace smt {
             return true;
         }
         
-        virtual bool check_relevancy_or(app * n, bool root) const {
+        bool check_relevancy_or(app * n, bool root) const override {
             lbool val    = root ? l_true : m_context.find_assignment(n);
             if (val == l_false)
                 return check_relevancy_app(n);
@@ -600,7 +600,7 @@ namespace smt {
             return true;
         }
         
-        bool check_relevancy(expr_ref_vector const & v) const {
+        bool check_relevancy(expr_ref_vector const & v) const override {
             SASSERT(!can_propagate());
             ast_manager & m = get_manager();
             unsigned sz = v.size();
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 12764fd9d..b90735a07 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -2449,7 +2449,6 @@ expr_ref theory_seq::digit2int(expr* ch) {
 }
 
 void theory_seq::add_itos_axiom(expr* e) {
-    context& ctx = get_context();
     rational val;
     expr* n = nullptr;
     TRACE("seq", tout << mk_pp(e, m) << "\n";);