diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp
index 2d242f9b0..f197e8ad8 100644
--- a/src/api/api_context.cpp
+++ b/src/api/api_context.cpp
@@ -323,7 +323,7 @@ namespace api {
 
     smt::kernel & context::get_smt_kernel() {
         if (!m_solver) {
-            // PARAM-TODO: copy config_params -> fparams
+            m_fparams.updt_params(m_params);
             m_solver = alloc(smt::kernel, m_manager, m_fparams);
         }
         return *m_solver;
diff --git a/src/smt/params/preprocessor_params.cpp b/src/smt/params/preprocessor_params.cpp
new file mode 100644
index 000000000..375fef787
--- /dev/null
+++ b/src/smt/params/preprocessor_params.cpp
@@ -0,0 +1,32 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    preprocessor_params.h
+
+Abstract:
+
+    Preprocess AST before adding them to the logical context
+
+Author:
+
+    Leonardo de Moura (leonardo) 2012-12-02.
+
+Revision History:
+
+--*/
+#include"preprocessor_params.h"
+#include"smt_params_helper.hpp"
+
+void preprocessor_params::updt_local_params(params_ref const & _p) {
+    smt_params_helper p(_p);
+    m_macro_finder = p.macro_finder();
+}
+
+void preprocessor_params::updt_params(params_ref const & p) {
+    pattern_inference_params::updt_params(p);
+    bv_simplifier_params::updt_params(p);
+    arith_simplifier_params::updt_params(p);
+    updt_local_params(p);
+}
diff --git a/src/smt/params/preprocessor_params.h b/src/smt/params/preprocessor_params.h
index e4b20b87a..d53f26318 100644
--- a/src/smt/params/preprocessor_params.h
+++ b/src/smt/params/preprocessor_params.h
@@ -56,7 +56,7 @@ struct preprocessor_params : public pattern_inference_params,
     bool            m_nlquant_elim;
 
 public:
-    preprocessor_params():
+    preprocessor_params(params_ref const & p = params_ref()):
         m_lift_ite(LI_NONE),
         m_ng_lift_ite(LI_NONE), 
         m_pull_cheap_ite_trees(false),
@@ -77,36 +77,12 @@ public:
         m_max_bv_sharing(true),
         m_pre_simplifier(true),
         m_nlquant_elim(false) {
+        updt_local_params(p);
     }
 
-#if 0
-    void register_params(ini_params & p) {
-        pattern_inference_params::register_params(p);
-        bit_blaster_params::register_params(p);
-        bv_simplifier_params::register_params(p);
-        arith_simplifier_params::register_params(p);
-        p.register_int_param("lift_ite", 0, 2, reinterpret_cast<int&>(m_lift_ite), "ite term lifting: 0 - no lifting, 1 - conservative, 2 - full");
-        p.register_int_param("ng_lift_ite", 0, 2, reinterpret_cast<int&>(m_ng_lift_ite), "ite (non-ground) term lifting: 0 - no lifting, 1 - conservative, 2 - full");
-        p.register_bool_param("elim_term_ite", m_eliminate_term_ite, "eliminate term if-then-else in the preprocessor");
-        p.register_bool_param("elim_and", m_eliminate_and, "represent (and a b) as (not (or (not a) (not b)))");
-        p.register_bool_param("macro_finder", m_macro_finder, "try to find universally quantified formulas that can be viewed as macros");
-        p.register_bool_param("propagate_values", m_propagate_values, "propagate values during preprocessing step");
-        p.register_bool_param("propagate_booleans", m_propagate_booleans, "propagate boolean values during preprocessing step");
-        p.register_bool_param("pull_cheap_ite_trees", m_pull_cheap_ite_trees);
-        p.register_bool_param("pull_nested_quantifiers", m_pull_nested_quantifiers, "eliminate nested quantifiers by moving nested quantified variables to the outermost quantifier, it is unnecessary if the formula is converted into CNF");
-        p.register_bool_param("refine_inj_axiom", m_refine_inj_axiom);
-        p.register_bool_param("elim_bounds", m_eliminate_bounds, "cheap Fourier-Motzkin");
-
-        p.register_bool_param("bit2int", m_simplify_bit2int, "hoist bit2int conversions over arithmetical expressions");
-        p.register_bool_param("distribute_forall", m_distribute_forall);
-        p.register_bool_param("reduce_args", m_reduce_args);
-        p.register_bool_param("quasi_macros", m_quasi_macros);
-        p.register_bool_param("restricted_quasi_macros", m_restricted_quasi_macros);
-        p.register_bool_param("bv_max_sharing", m_max_bv_sharing);
-        p.register_bool_param("pre_simplifier", m_pre_simplifier);
-    }
-#endif
+    void updt_local_params(params_ref const & p);
 
+    void updt_params(params_ref const & p);
 };
 
 #endif /* _PREPROCESSOR_PARAMS_H_ */
diff --git a/src/smt/params/qi_params.cpp b/src/smt/params/qi_params.cpp
new file mode 100644
index 000000000..f5506d35b
--- /dev/null
+++ b/src/smt/params/qi_params.cpp
@@ -0,0 +1,37 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    qi_params.cpp
+
+Abstract:
+
+    <abstract>
+
+Author:
+
+    Leonardo de Moura (leonardo) 2012-12-02.
+
+Revision History:
+
+--*/
+#include"qi_params.h"
+#include"smt_params_helper.hpp"
+
+void qi_params::updt_params(params_ref const & _p) {
+    smt_params_helper p(_p);
+    m_mbqi = p.mbqi();
+    m_mbqi_max_cexs = p.mbqi_max_cexs();
+    m_mbqi_max_cexs_incr = p.mbqi_max_cexs_incr();
+    m_mbqi_max_iterations = p.mbqi_max_iterations();
+    m_mbqi_trace = p.mbqi_trace();
+    m_mbqi_force_template = p.mbqi_force_template();
+    m_qi_profile = p.qi_profile();
+    m_qi_profile_freq = p.qi_profile_freq();
+    m_qi_max_instances = p.qi_max_instances();
+    m_qi_eager_threshold = p.qi_eager_threshold();
+    m_qi_lazy_threshold = p.qi_lazy_threshold();
+    m_qi_cost = p.qi_cost();
+    m_qi_max_eager_multipatterns = p.qi_max_multi_patterns();
+}
diff --git a/src/smt/params/qi_params.h b/src/smt/params/qi_params.h
index 1a8edb3a8..b0a21e75b 100644
--- a/src/smt/params/qi_params.h
+++ b/src/smt/params/qi_params.h
@@ -20,6 +20,7 @@ Revision History:
 #define _QI_PARAMS_H_
 
 #include"util.h"
+#include"params.h"
 
 enum quick_checker_mode {
     MC_NO,     // do not use (cheap) model checking based instantiation
@@ -53,7 +54,7 @@ struct qi_params {
 
     bool               m_instgen;
 
-    qi_params():
+    qi_params(params_ref const & p = params_ref()):
         /*
           The "weight 0" performance bug
           ------------------------------
@@ -93,49 +94,17 @@ struct qi_params {
         m_qi_max_instances(UINT_MAX),
         m_qi_lazy_instantiation(false),
         m_qi_conservative_final_check(false),
-#ifdef _EXTERNAL_RELEASE
         m_mbqi(true), // enabled by default
-#else
-        m_mbqi(false), // to avoid Rustan whining that the models are not partial anymore.
-#endif
         m_mbqi_max_cexs(1),
         m_mbqi_max_cexs_incr(1),
         m_mbqi_max_iterations(1000),
         m_mbqi_trace(false),
         m_mbqi_force_template(10),
         m_instgen(false) {
+        updt_params(p);
     }
 
-#if 0    
-    void register_params(ini_params & p) {
-        p.register_unsigned_param("qi_max_eager_multi_patterns", m_qi_max_eager_multipatterns,
-                                  "Specify the number of extra multi patterns that are processed eagerly. By default, the prover use at most one multi-pattern eagerly when there is no unary pattern. This value should be smaller than or equal to PI_MAX_MULTI_PATTERNS");
-        p.register_unsigned_param("qi_max_lazy_multi_pattern_matching", m_qi_max_lazy_multipattern_matching, "Maximum number of rounds of matching in a branch for delayed multipatterns. A multipattern is delayed based on the value of QI_MAX_EAGER_MULTI_PATTERNS");
-        p.register_string_param("qi_cost", m_qi_cost, "The cost function for quantifier instantiation");
-        p.register_string_param("qi_new_gen", m_qi_new_gen, "The function for calculating the generation of newly constructed terms");
-        p.register_double_param("qi_eager_threshold", m_qi_eager_threshold, "Threshold for eager quantifier instantiation");
-        p.register_double_param("qi_lazy_threshold", m_qi_lazy_threshold, "Threshold for lazy quantifier instantiation");
-        p.register_bool_param("qi_profile", m_qi_profile);
-        p.register_unsigned_param("qi_profile_freq", m_qi_profile_freq);
-        p.register_int_param("qi_quick_checker", 0, 2, reinterpret_cast<int&>(m_qi_quick_checker), "0 - do not use (cheap) model checker, 1 - instantiate instances unsatisfied by current model, 2 - 1 + instantiate instances not satisfied by current model");
-        p.register_bool_param("qi_lazy_quick_checker", m_qi_lazy_quick_checker);
-        p.register_bool_param("qi_promote_unsat", m_qi_promote_unsat);
-        p.register_unsigned_param("qi_max_instances", m_qi_max_instances);
-        p.register_bool_param("qi_lazy_instantiation", m_qi_lazy_instantiation);
-        p.register_bool_param("qi_conservative_final_check", m_qi_conservative_final_check);
-
-
-        p.register_bool_param("mbqi", m_mbqi, "Model Based Quantifier Instantiation (MBQI)");
-        p.register_unsigned_param("mbqi_max_cexs", m_mbqi_max_cexs, "Initial maximal number of counterexamples used in MBQI, each counterexample generates a quantifier instantiation", true);
-        p.register_unsigned_param("mbqi_max_cexs_incr", m_mbqi_max_cexs_incr, "Increment for MBQI_MAX_CEXS, the increment is performed after each round of MBQI", true);
-        p.register_unsigned_param("mbqi_max_iterations", m_mbqi_max_iterations, "Maximum number of rounds of MBQI", true);
-        p.register_bool_param("mbqi_trace", m_mbqi_trace, "Generate tracing messages for Model Based Quantifier Instantiation (MBQI). It will display a message before every round of MBQI, and the quantifiers that were not satisfied.", true);
-        p.register_unsigned_param("mbqi_force_template", m_mbqi_force_template, "Some quantifiers can be used as templates for building interpretations for functions. Z3 uses heuristics to decide whether a quantifier will be used as a template or not. Quantifiers with weight >= MBQI_FORCE_TEMPLATE are forced to be used as a template", true);
-
-        p.register_bool_param("inst_gen", m_instgen, "Enable Instantiation Generation solver (disables other quantifier reasoning)", false);
-    }
-#endif
-
+    void updt_params(params_ref const & p);
 };
 
 #endif /* _QI_PARAMS_H_ */
diff --git a/src/smt/params/smt_params.cpp b/src/smt/params/smt_params.cpp
index 77d3660e6..70f0ad811 100644
--- a/src/smt/params/smt_params.cpp
+++ b/src/smt/params/smt_params.cpp
@@ -17,105 +17,33 @@ Revision History:
 
 --*/
 #include"smt_params.h"
-#include"trace.h"
-
-#if 0
-void smt_params::register_params(ini_params & p) {
-    dyn_ack_params::register_params(p);
-    qi_params::register_params(p);
-    theory_arith_params::register_params(p);
-    theory_array_params::register_params(p);
-    theory_bv_params::register_params(p);
-    theory_datatype_params::register_params(p);
-
-    p.register_bool_param("check_proof", m_check_proof);
-    p.register_bool_param("display_proof", m_display_proof);
-    p.register_bool_param("display_dot_proof", m_display_dot_proof);
-    p.register_bool_param("display_unsat_core", m_display_unsat_core);
-    p.register_bool_param("eq_propagation", m_eq_propagation);
-    p.register_bool_param("bin_clauses", m_binary_clause_opt);
-    p.register_unsigned_param("relevancy", m_relevancy_lvl, "relevancy propagation heuristic: 0 - disabled, 1 - relevancy is tracked by only affects quantifier instantiation, 2 - relevancy is tracked, and an atom is only asserted if it is relevant", true);
-    p.register_bool_param("relevancy_lemma", m_relevancy_lemma, "true if lemmas are used to propagate relevancy");
-    p.register_unsigned_param("random_seed", m_random_seed, "random seed for Z3");
-    p.register_percentage_param("random_case_split_freq", m_random_var_freq, "frequency of random case splits");
-    p.register_int_param("phase_selection", 0, 6, reinterpret_cast<int&>(m_phase_selection), "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");
-    p.register_bool_param("minimize_lemmas", m_minimize_lemmas, "enable/disable lemma minimization algorithm");
-    p.register_unsigned_param("max_conflicts", m_max_conflicts, "maximum number of conflicts");
-
-    p.register_unsigned_param("recent_lemma_threshold", m_recent_lemmas_size);
-    p.register_unsigned_param("tick", m_tick);
-
-    PRIVATE_PARAMS({
-            p.register_bool_param("theory_resolve", m_theory_resolve, "Apply theory resolution to produce auxiliary conflict clauses", true);
-        });
-
-    p.register_int_param("restart_strategy", 0, 4, reinterpret_cast<int&>(m_restart_strategy), "0 - geometric, 1 - inner-outer-geometric, 2 - luby, 3 - fixed, 4 - arithmetic");
-    p.register_unsigned_param("restart_initial", m_restart_initial, 
-                              "inital restart frequency in number of conflicts, it is also the unit for the luby sequence");
-    p.register_double_param("restart_factor", m_restart_factor, "when using geometric (or inner-outer-geometric) progression of restarts, it specifies the constant used to multiply the currect restart threshold");
-    p.register_bool_param("restart_adaptive", m_restart_adaptive, "disable restarts based on the search 'agility'");
-    p.register_percentage_param("restart_agility_threshold", m_restart_agility_threshold);
-
-    p.register_int_param("lemma_gc_strategy", 0, 2, reinterpret_cast<int&>(m_lemma_gc_strategy), "0 - fixed, 1 - geometric, 2 - at every restart");
-    p.register_bool_param("lemma_gc_half", m_lemma_gc_half, "true for simple gc algorithm (delete approx. half of the clauses)");
-    p.register_unsigned_param("lemma_gc_initial", m_lemma_gc_initial, "lemma initial gc frequency (in number of conflicts), used by fixed or geometric strategies");
-    p.register_double_param("lemma_gc_factor", m_lemma_gc_factor, "used by geometric strategy");
-    p.register_unsigned_param("lemma_gc_new_old_ratio", m_new_old_ratio);
-    p.register_unsigned_param("lemma_gc_new_clause_activity", m_new_clause_activity);
-    p.register_unsigned_param("lemma_gc_old_clause_activity", m_old_clause_activity);
-    p.register_unsigned_param("lemma_gc_new_clause_relevancy", m_new_clause_relevancy);
-    p.register_unsigned_param("lemma_gc_old_clause_relevancy", m_old_clause_activity);
-    
-    p.register_bool_param("simplify_clauses", m_simplify_clauses);
-    
-    p.register_int_param("random_initial_activity", 0, 2, reinterpret_cast<int&>(m_random_initial_activity));
-
-    PRIVATE_PARAMS({
-
-        p.register_double_param("inv_decay", m_inv_decay);
-        p.register_unsigned_param("phase_caching_on_duration", m_phase_caching_on);
-        p.register_unsigned_param("phase_caching_off_duration", m_phase_caching_off);
-    });
-
-    p.register_bool_param("smtlib_dump_lemmas", m_smtlib_dump_lemmas);
-    p.register_string_param("smtlib_logic", m_smtlib_logic, "Name used for the :logic field when generating SMT-LIB benchmarks");
-    p.register_bool_param("display_features", m_display_features);
-
-    p.register_bool_param("new_core2th_eq", m_new_core2th_eq);
-    p.register_bool_param("ematching", m_ematching, "E-Matching based quantifier instantiation");
-
-    p.register_bool_param("profile_res_sub", m_profile_res_sub);
-#ifndef _EXTERNAL_RELEASE 
-    p.register_bool_param("display_bool_var2expr", m_display_bool_var2expr);
-    p.register_bool_param("display_ll_bool_var2expr", m_display_ll_bool_var2expr);
-    p.register_bool_param("abort_after_preproc", m_abort_after_preproc, "abort after preprocessing step, this flag is only useful for debugging purposes");
-    p.register_bool_param("display_installed_theories", m_display_installed_theories, "display theories installed at smt::context", true);
-#endif
-    p.register_int_param("case_split", 0, 5, reinterpret_cast<int&>(m_case_split_strategy), "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");
-    p.register_unsigned_param("rel_case_split_order", 0, 2, m_rel_case_split_order, "structural (relevancy) splitting order: 0 - left-to-right (default), 1 - random, 2 - right-to-left");
-    p.register_bool_param("lookahead_diseq", m_lookahead_diseq);
-
-    p.register_bool_param("delay_units", m_delay_units);
-    p.register_unsigned_param("delay_units_threshold", m_delay_units_threshold);
-
-    p.register_bool_param("model", m_model, "enable/disable model construction", true);
-    p.register_bool_param("model_validate", m_model_validate, "validate the model", true);
-    p.register_bool_param("model_on_timeout", m_model_on_timeout, "after hitting soft-timeout or memory high watermark, generate a candidate model", true);
-    p.register_bool_param("model_on_final_check", m_model_on_final_check, "display candidate model (in the standard output) whenever Z3 hits a final check", true);
-    
-    p.register_unsigned_param("progress_sampling_freq", m_progress_sampling_freq, "frequency for progress output in miliseconds");
-
-
-    p.register_bool_param("user_theory_preprocess_axioms", 
-                          m_user_theory_preprocess_axioms, 
-                          "Apply full pre-processing to user theory axioms",
-                          true);
-
-    p.register_bool_param("user_theory_persist_axioms",
-                          m_user_theory_persist_axioms,
-                          "Persist user axioms to the base level",
-                          true);
+#include"smt_params_helper.hpp"
 
+void smt_params::updt_local_params(params_ref const & _p) {
+    smt_params_helper p(_p);
+    m_auto_config = p.auto_config();
+    m_ematching   = p.ematching();
+    m_phase_selection = static_cast<phase_selection>(p.phase_selection());
+    m_restart_strategy = static_cast<restart_strategy>(p.restart_strategy());
+    m_restart_factor = p.restart_factor();
+    m_case_split_strategy = static_cast<case_split_strategy>(p.case_split());
+    m_delay_units = p.delay_units();
+    m_delay_units_threshold = p.delay_units_threshold();
+}
+
+void smt_params::updt_params(params_ref const & p) {
+    preprocessor_params::updt_params(p);
+    qi_params::updt_params(p);
+    theory_arith_params::updt_params(p);
+    theory_bv_params::updt_params(p);
+    updt_local_params(p);
+}
+
+void smt_params::updt_params(context_params const & p) {
+    m_auto_config    = p.m_auto_config;
+    m_soft_timeout   = p.m_timeout;
+    m_model          = p.m_model;
+    m_model_validate = p.m_validate_model;
+    m_proof_mode     = p.m_proof ? PGM_FINE : PGM_DISABLED;
 }
 
-#endif
diff --git a/src/smt/params/smt_params.h b/src/smt/params/smt_params.h
index 68e5a596d..ec057239a 100644
--- a/src/smt/params/smt_params.h
+++ b/src/smt/params/smt_params.h
@@ -27,6 +27,7 @@ Revision History:
 #include"theory_bv_params.h"
 #include"theory_datatype_params.h"
 #include"preprocessor_params.h"
+#include"context_params.h"
 
 enum phase_selection { 
     PS_ALWAYS_FALSE,
@@ -209,23 +210,7 @@ struct smt_params : public preprocessor_params,
     proof_gen_mode      m_proof_mode;
     bool                m_auto_config;
 
-#if 0
-    unsigned            m_memory_high_watermark;
-    unsigned            m_memory_max_size;
-
-    bool                m_auto_config;
-
-    bool                m_debug_ref_count;
-    
-        m_well_sorted_check(true),
-        m_memory_high_watermark(0),
-        m_memory_max_size(0),
-
-        m_auto_config(true),
-        m_debug_ref_count(false) {
-#endif
-
-    smt_params():
+    smt_params(params_ref const & p = params_ref()):
         m_display_proof(false),
         m_display_dot_proof(false),
         m_display_unsat_core(false),
@@ -294,7 +279,14 @@ struct smt_params : public preprocessor_params,
         m_dump_goal_as_smt(false),
         m_proof_mode(PGM_DISABLED),
         m_auto_config(true) {
+        updt_local_params(p);
     }
+
+    void updt_local_params(params_ref const & p);
+
+    void updt_params(params_ref const & p);
+
+    void updt_params(context_params const & p);
 };
 
 #endif /* _SMT_PARAMS_H_ */
diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg
new file mode 100644
index 000000000..8db95a581
--- /dev/null
+++ b/src/smt/params/smt_params_helper.pyg
@@ -0,0 +1,38 @@
+def_module_params(module_name='smt', 
+                  class_name='smt_params_helper',
+                  description='smt solver based on lazy smt',
+                  export=True,
+                  params=(('auto_config', BOOL, True, 'automatically configure solver'),
+                          ('macro_finder', BOOL, False, 'try to find universally quantified formulas that can be viewed as macros'),
+                          ('ematching', BOOL, True, 'E-Matching based quantifier instantiation'),
+                          ('phase_selection', UINT, 4, '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'),
+                          ('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 currect 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'),
+                          ('delay_units', BOOL, False, 'if true then z3 will not restart when a unit clause is learned'),
+                          ('delay_units_threshold', UINT, 32, 'maximum number of learned unit clauses before restarting, ingored if delay_units is false'),
+                          ('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'),
+                          ('mbqi.max_iterations', UINT, 1000, 'maximum number of rounds of MBQI'),
+                          ('mbqi.trace', BOOL, False, 'generate tracing messages for Model Based Quantifier Instantiation (MBQI). It will display a message before every round of MBQI, and the quantifiers that were not satisfied'),
+                          ('mbqi.force_template', UINT, 10, 'some quantifiers can be used as templates for building interpretations for functions. Z3 uses heuristics to decide whether a quantifier will be used as a template or not. Quantifiers with weight >= mbqi.force_template are forced to be used as a template'),
+                          ('qi.profile', BOOL, False, 'profile quantifier instantiation'),
+                          ('qi.profile_freq', UINT, UINT_MAX, 'how frequent results are reported by qi.profile'),
+                          ('qi.max_instances', UINT, UINT_MAX, 'maximum number of quantifier instantiations'),
+                          ('qi.eager_threshold', DOUBLE, 10.0, 'threshold for eager quantifier instantiation'),
+                          ('qi.lazy_threshold', DOUBLE, 20.0, 'threshold for lazy quantifier instantiation'),
+                          ('qi.cost', STRING, '(+ weight generation)', 'expression specifying what is the cost of a given quantifier instantiation'),
+                          ('qi.max_multi_patterns', UINT, 0, 'specify the number of extra multi patterns'),
+                          ('bv.reflect', BOOL, True, 'create enode for every bit-vector term'),
+                          ('arith.random_initial_value', BOOL, False, 'use random initial values in the simplex-based procedure for linear arithmetic'),
+                          ('arith.solver', UINT, 2, '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'),
+                          ('arith.nl', BOOL, True, '(incomplete) nonlinear arithmetic support based on Groebner basis and interval propagation'),
+                          ('arith.nl.gb', BOOL, True, 'groebner Basis computation, this option is ignored when arith.nl=false'),
+                          ('arith.nl.branching', BOOL, True, 'branching on integer variables in non linear clusters'),
+                          ('arith.nl.rounds', UINT, 1024, 'threshold for number of (nested) final checks for non linear arithmetic'),
+                          ('arith.euclidean_solver', BOOL, False, 'eucliean solver for linear integer arithmetic'),
+                          ('arith.propagate_eqs', BOOL, True, 'propagate (cheap) equalities'),
+                          ('arith.branch_cut_ratio', UINT, 2, 'branch/cut ratio for linear integer arithmetic'),
+                          ('arith.int_eq_branch', BOOL, False, 'branching using derived integer equations'),
+                          ('arith.ignore_int', BOOL, False, 'treat integer variables as real')))
diff --git a/src/smt/params/theory_arith_params.cpp b/src/smt/params/theory_arith_params.cpp
index 8dde26e94..5a1101524 100644
--- a/src/smt/params/theory_arith_params.cpp
+++ b/src/smt/params/theory_arith_params.cpp
@@ -16,63 +16,22 @@ Author:
 Revision History:
 
 --*/
-
 #include"theory_arith_params.h"
+#include"smt_params_helper.hpp"
 
-#if 0
-void theory_arith_params::register_params(ini_params & p) {
-#ifdef _EXTERNAL_RELEASE
-    p.register_int_param("arith_solver", 0, 3, reinterpret_cast<int&>(m_arith_mode), "select 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");
-#else
-    p.register_int_param("arith_solver", 0, 4, reinterpret_cast<int&>(m_arith_mode), "select 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 - model guided arith_solver");
-#endif
-    p.register_bool_param("arith_force_simplex", m_arith_auto_config_simplex, "force Z3 to use simplex solver.");
-    p.register_unsigned_param("arith_blands_rule_threshold", m_arith_blands_rule_threshold);
-    p.register_bool_param("arith_propagate_eqs", m_arith_propagate_eqs);
-    p.register_int_param("arith_propagation_mode", 0, 2, reinterpret_cast<int&>(m_arith_bound_prop));
-    p.register_bool_param("arith_stronger_lemmas", m_arith_stronger_lemmas);
-    p.register_bool_param("arith_skip_big_coeffs", m_arith_skip_rows_with_big_coeffs);
-    p.register_unsigned_param("arith_max_lemma_size", m_arith_max_lemma_size);
-    p.register_unsigned_param("arith_small_lemma_size", m_arith_small_lemma_size);
-    p.register_bool_param("arith_reflect", m_arith_reflect);
-    p.register_bool_param("arith_ignore_int", m_arith_ignore_int);
-    p.register_unsigned_param("arith_lazy_pivoting", m_arith_lazy_pivoting_lvl);
-    p.register_unsigned_param("arith_random_seed", m_arith_random_seed);
-    p.register_bool_param("arith_random_initial_value", m_arith_random_initial_value);
-    p.register_int_param("arith_random_lower", m_arith_random_lower);
-    p.register_int_param("arith_random_upper", m_arith_random_upper);
-    p.register_bool_param("arith_adaptive", m_arith_adaptive);
-    p.register_double_param("arith_adaptive_assertion_threshold", m_arith_adaptive_assertion_threshold, "Delay arithmetic atoms if the num-arith-conflicts/total-conflicts < threshold");
-    p.register_double_param("arith_adaptive_propagation_threshold", m_arith_adaptive_propagation_threshold, "Disable arithmetic theory propagation if the num-arith-conflicts/total-conflicts < threshold");
-    p.register_bool_param("arith_dump_lemmas", m_arith_dump_lemmas);
-    p.register_bool_param("arith_eager_eq_axioms", m_arith_eager_eq_axioms);
-    p.register_unsigned_param("arith_branch_cut_ratio", m_arith_branch_cut_ratio);
-
-    p.register_bool_param("arith_add_binary_bounds", m_arith_add_binary_bounds);
-    p.register_unsigned_param("arith_prop_strategy", 0, 1, reinterpret_cast<unsigned&>(m_arith_propagation_strategy), "Propagation strategy: 0 - use agility measures based on ration of theory conflicts, 1 - propagate proportional to ratio of theory conflicts (default)");
-
-    p.register_bool_param("arith_eq_bounds", m_arith_eq_bounds);
-    p.register_bool_param("arith_lazy_adapter", m_arith_lazy_adapter);
-    p.register_bool_param("arith_gcd_test", m_arith_gcd_test);
-    p.register_bool_param("arith_eager_gcd", m_arith_eager_gcd);
-    p.register_bool_param("arith_adaptive_gcd", m_arith_adaptive_gcd);
-    p.register_unsigned_param("arith_propagation_threshold", m_arith_propagation_threshold);
-
-    p.register_bool_param("nl_arith", m_nl_arith, "enable/disable non linear arithmetic support. This option is ignored when ARITH_SOLVER != 2.");
-    p.register_bool_param("nl_arith_gb", m_nl_arith_gb, "enable/disable Grobner Basis computation. This option is ignored when NL_ARITH=false");
-    p.register_bool_param("nl_arith_gb_eqs", m_nl_arith_gb_eqs, "enable/disable equations in the Grobner Basis to be copied to the Simplex tableau.");
-    p.register_bool_param("nl_arith_gb_perturbate", m_nl_arith_gb_perturbate, "enable/disable perturbation of the variable order in GB when searching for new polynomials.");
-    p.register_unsigned_param("nl_arith_gb_threshold", m_nl_arith_gb_threshold, "Grobner basis computation can be very expensive. This is a threshold on the number of new equalities that can be generated.");
-    p.register_bool_param("nl_arith_branching", m_nl_arith_branching, "enable/disable branching on integer variables in non linear clusters");
-    p.register_unsigned_param("nl_arith_rounds", m_nl_arith_rounds, "threshold for number of (nested) final checks for non linear arithmetic.");
-    p.register_unsigned_param("nl_arith_max_degree", m_nl_arith_max_degree, "max degree for internalizing new monomials.");
-    PRIVATE_PARAMS({
-        p.register_bool_param("arith_fixnum", m_arith_fixnum);
-        p.register_bool_param("arith_int_only", m_arith_int_only);
-        p.register_bool_param("arith_enum_const_mod", m_arith_enum_const_mod, "Create axioms for the finite set of equalities for (mod x k) where k is a positive numeral constant");
-        p.register_bool_param("arith_int_eq_branching",  m_arith_int_eq_branching, "Determine branch predicates based on integer equation solving");       
-    });
-    p.register_bool_param("arith_euclidean_solver", m_arith_euclidean_solver, "");
+void theory_arith_params::updt_params(params_ref const & _p) {
+    smt_params_helper p(_p);
+    m_arith_random_initial_value = p.arith_random_initial_value();
+    m_arith_mode = static_cast<arith_solver_id>(p.arith_solver());
+    m_nl_arith = p.arith_nl();
+    m_nl_arith_gb = p.arith_nl_gb();
+    m_nl_arith_branching = p.arith_nl_branching();
+    m_nl_arith_rounds = p.arith_nl_rounds();
+    m_arith_euclidean_solver = p.arith_euclidean_solver();
+    m_arith_propagate_eqs = p.arith_propagate_eqs();
+    m_arith_branch_cut_ratio = p.arith_branch_cut_ratio();
+    m_arith_int_eq_branching = p.arith_int_eq_branch();
+    m_arith_ignore_int = p.arith_ignore_int();
 }
 
-#endif
+
diff --git a/src/smt/params/theory_arith_params.h b/src/smt/params/theory_arith_params.h
index 01163dd0a..52fef8ca4 100644
--- a/src/smt/params/theory_arith_params.h
+++ b/src/smt/params/theory_arith_params.h
@@ -20,6 +20,7 @@ Revision History:
 #define _THEORY_ARITH_PARAMS_H_
 
 #include<limits.h>
+#include"params.h"
 
 enum arith_solver_id {
     AS_NO_ARITH,
@@ -104,7 +105,7 @@ struct theory_arith_params {
     bool                    m_arith_euclidean_solver;
 
 
-    theory_arith_params():
+    theory_arith_params(params_ref const & p = params_ref()):
         m_arith_mode(AS_ARITH),
         m_arith_auto_config_simplex(false),
         m_arith_blands_rule_threshold(1000),
@@ -149,7 +150,10 @@ struct theory_arith_params {
         m_nl_arith_branching(true),
         m_nl_arith_rounds(1024),
         m_arith_euclidean_solver(false) {
+        updt_params(p);
     }
+
+    void updt_params(params_ref const & p);
 };
 
 #endif /* _THEORY_ARITH_PARAMS_H_ */
diff --git a/src/smt/params/theory_bv_params.cpp b/src/smt/params/theory_bv_params.cpp
new file mode 100644
index 000000000..c2a31c59d
--- /dev/null
+++ b/src/smt/params/theory_bv_params.cpp
@@ -0,0 +1,25 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    theory_bv_params.cpp
+
+Abstract:
+
+    <abstract>
+
+Author:
+
+    Leonardo de Moura (leonardo) 2012-12-02.
+
+Revision History:
+
+--*/
+#include"theory_bv_params.h"
+#include"smt_params_helper.hpp"
+
+void theory_bv_params::updt_params(params_ref const & _p) {
+    smt_params_helper p(_p);
+    m_bv_reflect = p.bv_reflect();
+}
diff --git a/src/smt/params/theory_bv_params.h b/src/smt/params/theory_bv_params.h
index 18a3bac77..a3052b4e9 100644
--- a/src/smt/params/theory_bv_params.h
+++ b/src/smt/params/theory_bv_params.h
@@ -19,6 +19,8 @@ Revision History:
 #ifndef _THEORY_BV_PARAMS_H_
 #define _THEORY_BV_PARAMS_H_
 
+#include"params.h"
+
 enum bv_solver_id {
     BS_NO_BV,
     BS_BLASTER
@@ -31,24 +33,17 @@ struct theory_bv_params {
     bool         m_bv_cc;
     unsigned     m_bv_blast_max_size;
     bool         m_bv_enable_int2bv2int;
-    theory_bv_params():
+    theory_bv_params(params_ref const & p = params_ref()):
         m_bv_mode(BS_BLASTER),
         m_bv_reflect(true),
         m_bv_lazy_le(false),
         m_bv_cc(false),
         m_bv_blast_max_size(INT_MAX),
-        m_bv_enable_int2bv2int(false) {}
-#if 0
-     void register_params(ini_params & p) {
-         p.register_int_param("bv_solver", 0, 2, reinterpret_cast<int&>(m_bv_mode), "0 - no bv, 1 - simple");
-         p.register_unsigned_param("bv_blast_max_size", m_bv_blast_max_size, "Maximal size for bit-vectors to blast");
-         p.register_bool_param("bv_reflect", m_bv_reflect);
-         p.register_bool_param("bv_lazy_le", m_bv_lazy_le);
-         p.register_bool_param("bv_cc", m_bv_cc, "enable congruence closure for BV operators");
-         p.register_bool_param("bv_enable_int2bv_propagation", m_bv_enable_int2bv2int, 
-                               "enable full (potentially expensive) propagation for int2bv and bv2int");
-     }
-#endif
+        m_bv_enable_int2bv2int(false) {
+        updt_params(p);
+    }
+    
+    void updt_params(params_ref const & p);
 };
 
 #endif /* _THEORY_BV_PARAMS_H_ */
diff --git a/src/smt/smt_kernel.cpp b/src/smt/smt_kernel.cpp
index 977f0ee4a..23687af8c 100644
--- a/src/smt/smt_kernel.cpp
+++ b/src/smt/smt_kernel.cpp
@@ -179,7 +179,9 @@ namespace smt {
         }
 
         void updt_params(params_ref const & p) {
-            params2smt_params(p, fparams());
+            // We don't need params2smt_params anymore. smt_params has support for reading params_ref.
+            // The update is performed at smt_kernel "users".
+            // params2smt_params(p, fparams());
         }
     };
 
diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp
index ad653a968..2aa4ee28f 100644
--- a/src/smt/smt_solver.cpp
+++ b/src/smt/smt_solver.cpp
@@ -36,7 +36,7 @@ namespace smt {
         }
 
         virtual void updt_params(params_ref const & p) {
-            // PARAM-TODO copy p --> m_params
+            m_params.updt_params(p);
             if (m_context == 0)
                 return;
             m_context->updt_params(p);
diff --git a/src/smt/tactic/smt_tactic.cpp b/src/smt/tactic/smt_tactic.cpp
index a8694363c..20b6585e1 100644
--- a/src/smt/tactic/smt_tactic.cpp
+++ b/src/smt/tactic/smt_tactic.cpp
@@ -24,7 +24,7 @@ Notes:
 #include"rewriter_types.h"
 
 class smt_tactic : public tactic {
-    smt_params             m_params;
+    smt_params                   m_params;
     params_ref                   m_params_ref;
     statistics                   m_stats;
     std::string                  m_failure;
@@ -63,9 +63,7 @@ public:
     virtual void updt_params(params_ref const & p) {
         TRACE("smt_tactic", tout << this << "\nupdt_params: " << p << "\n";);
         updt_params_core(p);
-        m_params_ref = p;
-        // PARAM-TODO update params2smt_params p ---> m_params
-        params2smt_params(m_params_ref, fparams());
+        fparams().updt_params(p);
         SASSERT(p.get_bool("auto_config", fparams().m_auto_config) == fparams().m_auto_config);
     }