diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index 2906b11fe..98fae665a 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -1507,11 +1507,15 @@ def def_module_params(module_name, export, params, class_name=None, description=
         print "Generated '%s'" % hpp
 
 def max_memory_param():
-    return ('max_memory', UINT, UINT_MAX, 'maximum amount of memory in megabytes.')
+    return ('max_memory', UINT, UINT_MAX, 'maximum amount of memory in megabytes')
+
+def max_steps_param():
+    return ('max_steps', UINT, UINT_MAX, 'maximum number of steps')
 
 PYG_GLOBALS = { 'UINT' : UINT, 'BOOL' : BOOL, 'DOUBLE' : DOUBLE, 'STRING' : STRING, 'SYMBOL' : SYMBOL, 
                 'UINT_MAX' : UINT_MAX, 
                 'max_memory_param' : max_memory_param,
+                'max_steps_param' : max_steps_param,
                 'def_module_params' : def_module_params }
 
 # Execute python auxiliary scripts that generate extra code for Z3.
diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp
index f5fdcf8af..a5dfda6e7 100644
--- a/src/ast/rewriter/arith_rewriter.cpp
+++ b/src/ast/rewriter/arith_rewriter.cpp
@@ -17,23 +17,25 @@ Notes:
 
 --*/
 #include"arith_rewriter.h"
+#include"arith_rewriter_params.hpp"
 #include"poly_rewriter_def.h"
 #include"algebraic_numbers.h"
 #include"ast_pp.h"
 
-void arith_rewriter::updt_local_params(params_ref const & p) {
-    m_arith_lhs       = p.get_bool("arith_lhs", false);
-    m_gcd_rounding    = p.get_bool("gcd_rounding", false);
-    m_eq2ineq         = p.get_bool("eq2ineq", false);
-    m_elim_to_real    = p.get_bool("elim_to_real", false);
-    m_push_to_real    = p.get_bool("push_to_real", true);
-    m_anum_simp       = p.get_bool("algebraic_number_evaluator", true);
-    m_max_degree      = p.get_uint("max_degree", 64);
-    m_expand_power    = p.get_bool("expand_power", false);
-    m_mul2power       = p.get_bool("mul_to_power", false);
-    m_elim_rem        = p.get_bool("elim_rem", false);
-    m_expand_tan      = p.get_bool("expand_tan", false);
-    set_sort_sums(p.get_bool("sort_sums", false)); // set here to avoid collision with bvadd
+void arith_rewriter::updt_local_params(params_ref const & _p) {
+    arith_rewriter_params p(_p);
+    m_arith_lhs       = p.arith_lhs();
+    m_gcd_rounding    = p.gcd_rounding();
+    m_eq2ineq         = p.eq2ineq();
+    m_elim_to_real    = p.elim_to_real();
+    m_push_to_real    = p.push_to_real();
+    m_anum_simp       = p.algebraic_number_evaluator();
+    m_max_degree      = p.max_degree();
+    m_expand_power    = p.expand_power();
+    m_mul2power       = p.mul_to_power();
+    m_elim_rem        = p.elim_rem();
+    m_expand_tan      = p.expand_tan();
+    set_sort_sums(p.sort_sums());
 }
 
 void arith_rewriter::updt_params(params_ref const & p) {
@@ -43,18 +45,7 @@ void arith_rewriter::updt_params(params_ref const & p) {
 
 void arith_rewriter::get_param_descrs(param_descrs & r) {
     poly_rewriter<arith_rewriter_core>::get_param_descrs(r);
-    r.insert("algebraic_number_evaluator", CPK_BOOL, "(default: true) simplify/evaluate expressions containing (algebraic) irrational numbers.");
-    r.insert("mul_to_power", CPK_BOOL, "(default: false) collpase (* t ... t) into (^ t k), it is ignored if expand_power is true.");
-    r.insert("expand_power", CPK_BOOL, "(default: false) expand (^ t k) into (* t ... t) if  1 < k <= max_degree.");
-    r.insert("expand_tan", CPK_BOOL, "(default: false) replace (tan x) with (/ (sin x) (cos x)).");
-    r.insert("max_degree", CPK_UINT, "(default: 64) max degree of algebraic numbers (and power operators) processed by simplifier.");
-    r.insert("eq2ineq", CPK_BOOL, "(default: false) split arithmetic equalities into two inequalities.");
-    r.insert("sort_sums", CPK_BOOL, "(default: false) sort the arguments of + application.");
-    r.insert("gcd_rounding", CPK_BOOL, "(default: false) use gcd rounding on integer arithmetic atoms.");
-    r.insert("arith_lhs", CPK_BOOL, "(default: false) all monomials are moved to the left-hand-side, and the right-hand-side is just a constant.");
-    r.insert("elim_to_real", CPK_BOOL, "(default: false) eliminate to_real from arithmetic predicates that contain only integers.");
-    r.insert("push_to_real", CPK_BOOL, "(default: true) distribute to_real over * and +.");
-    r.insert("elim_rem", CPK_BOOL, "(default: false) replace (rem x y) with (ite (>= y 0) (mod x y) (- (mod x y))).");
+    arith_rewriter_params::collect_param_descrs(r);
 }
 
 br_status arith_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
diff --git a/src/ast/rewriter/arith_rewriter_params.pyg b/src/ast/rewriter/arith_rewriter_params.pyg
new file mode 100644
index 000000000..8a41d838d
--- /dev/null
+++ b/src/ast/rewriter/arith_rewriter_params.pyg
@@ -0,0 +1,15 @@
+def_module_params(module_name='rewriter',
+                  class_name='arith_rewriter_params',
+                  export=True,
+                  params=(("algebraic_number_evaluator", BOOL, True, "simplify/evaluate expressions containing (algebraic) irrational numbers."),
+                          ("mul_to_power", BOOL, False, "collpase (* t ... t) into (^ t k), it is ignored if expand_power is true."),
+                          ("expand_power", BOOL, False, "expand (^ t k) into (* t ... t) if  1 < k <= max_degree."),
+                          ("expand_tan", BOOL, False, "replace (tan x) with (/ (sin x) (cos x))."),
+                          ("max_degree", UINT, 64, "max degree of algebraic numbers (and power operators) processed by simplifier."),
+                          ("eq2ineq", BOOL, False, "split arithmetic equalities into two inequalities."),
+                          ("sort_sums", BOOL, False, "sort the arguments of + application."),
+                          ("gcd_rounding", BOOL, False, "use gcd rounding on integer arithmetic atoms."),
+                          ("arith_lhs", BOOL, False, "all monomials are moved to the left-hand-side, and the right-hand-side is just a constant."),
+                          ("elim_to_real", BOOL, False, "eliminate to_real from arithmetic predicates that contain only integers."),
+                          ("push_to_real", BOOL, True, "distribute to_real over * and +."),
+                          ("elim_rem", BOOL, False, "replace (rem x y) with (ite (>= y 0) (mod x y) (- (mod x y))).")))
diff --git a/src/ast/rewriter/array_rewriter.cpp b/src/ast/rewriter/array_rewriter.cpp
index ac93e0f87..9dbbeb231 100644
--- a/src/ast/rewriter/array_rewriter.cpp
+++ b/src/ast/rewriter/array_rewriter.cpp
@@ -17,17 +17,18 @@ Notes:
 
 --*/
 #include"array_rewriter.h"
+#include"array_rewriter_params.hpp"
 #include"ast_lt.h"
 #include"ast_pp.h"
 
-void array_rewriter::updt_params(params_ref const & p) {
-    m_sort_store = p.get_bool("sort_store", false);
-    m_expand_select_store = p.get_bool("expand_select_store", false);
+void array_rewriter::updt_params(params_ref const & _p) {
+    array_rewriter_params p(_p);
+    m_sort_store = p.sort_store();
+    m_expand_select_store = p.expand_select_store();
 }
 
 void array_rewriter::get_param_descrs(param_descrs & r) {
-    r.insert("expand_select_store", CPK_BOOL, "(default: false) replace a (select (store ...) ...) term by an if-then-else term.");
-    r.insert("sort_store", CPK_BOOL, "(default: false) sort nested stores when the indices are known to be different.");
+    array_rewriter_params::collect_param_descrs(r);
 }
 
 br_status array_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
diff --git a/src/ast/rewriter/array_rewriter_params.pyg b/src/ast/rewriter/array_rewriter_params.pyg
new file mode 100644
index 000000000..2e3ae9f6a
--- /dev/null
+++ b/src/ast/rewriter/array_rewriter_params.pyg
@@ -0,0 +1,5 @@
+def_module_params(module_name='rewriter',
+                  class_name='array_rewriter_params',
+                  export=True,
+                  params=(("expand_select_store", BOOL, False, "replace a (select (store ...) ...) term by an if-then-else term"),
+                          ("sort_store", BOOL, False, "sort nested stores when the indices are known to be different")))
diff --git a/src/ast/rewriter/bool_rewriter.cpp b/src/ast/rewriter/bool_rewriter.cpp
index b3f422fe5..4fcaf02fe 100644
--- a/src/ast/rewriter/bool_rewriter.cpp
+++ b/src/ast/rewriter/bool_rewriter.cpp
@@ -17,25 +17,21 @@ Notes:
 
 --*/
 #include"bool_rewriter.h"
+#include"bool_rewriter_params.hpp"
 #include"rewriter_def.h"
 
-void bool_rewriter::updt_params(params_ref const & p) {
-    m_flat                 = p.get_bool("flat", true);
-    m_elim_and             = p.get_bool("elim_and", false);
-    m_local_ctx            = p.get_bool("local_ctx", false);
-    m_local_ctx_limit      = p.get_uint("local_ctx_limit", UINT_MAX);
-    m_blast_distinct       = p.get_bool("blast_distinct", false); 
-    m_ite_extra_rules      = p.get_bool("ite_extra_rules", false);
+void bool_rewriter::updt_params(params_ref const & _p) {
+    bool_rewriter_params p(_p);
+    m_flat                 = p.flat();
+    m_elim_and             = p.elim_and();
+    m_local_ctx            = p.local_ctx();
+    m_local_ctx_limit      = p.local_ctx_limit();
+    m_blast_distinct       = p.blast_distinct();
+    m_ite_extra_rules      = p.ite_extra_rules();
 }
 
 void bool_rewriter::get_param_descrs(param_descrs & r) {
-    r.insert("ite_extra_rules", CPK_BOOL, 
-             "(default: false) extra ite simplifications, these additional simplifications may reduce size locally but increase globally.");
-    r.insert("flat", CPK_BOOL, "(default: true) create nary applications for and,or,+,*,bvadd,bvmul,bvand,bvor,bvxor.");
-    r.insert("elim_and", CPK_BOOL, "(default: false) conjunctions are rewritten using negation and disjunctions.");
-    r.insert("local_ctx", CPK_BOOL, "(default: false) perform local (i.e., cheap) context simplifications.");
-    r.insert("local_ctx_limit", CPK_UINT, "(default: inf) limit for applying local context simplifier.");
-    r.insert("blast_distinct", CPK_BOOL, "(default: false) expand a distinct predicate into a quadratic number of disequalities."); 
+    bool_rewriter_params::collect_param_descrs(r);
 }
 
 br_status bool_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
diff --git a/src/ast/rewriter/bool_rewriter_params.pyg b/src/ast/rewriter/bool_rewriter_params.pyg
new file mode 100644
index 000000000..a5bcf6f5d
--- /dev/null
+++ b/src/ast/rewriter/bool_rewriter_params.pyg
@@ -0,0 +1,9 @@
+def_module_params(module_name='rewriter',
+                  class_name='bool_rewriter_params',
+                  export=True,
+                  params=(("ite_extra_rules", BOOL, False, "extra ite simplifications, these additional simplifications may reduce size locally but increase globally"),
+                          ("flat", BOOL, True, "create nary applications for and,or,+,*,bvadd,bvmul,bvand,bvor,bvxor"),
+                          ("elim_and", BOOL, False, "conjunctions are rewritten using negation and disjunctions"),
+                          ("local_ctx", BOOL, False, "perform local (i.e., cheap) context simplifications"),
+                          ("local_ctx_limit", UINT, UINT_MAX, "limit for applying local context simplifier"),
+                          ("blast_distinct", BOOL, False, "expand a distinct predicate into a quadratic number of disequalities")))
diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp
index fbc1f7c11..5fd562676 100644
--- a/src/ast/rewriter/bv_rewriter.cpp
+++ b/src/ast/rewriter/bv_rewriter.cpp
@@ -17,6 +17,7 @@ Notes:
 
 --*/
 #include"bv_rewriter.h"
+#include"bv_rewriter_params.hpp"
 #include"poly_rewriter_def.h"
 #include"ast_smt2_pp.h"
 
@@ -53,15 +54,16 @@ app * mk_extract_proc::operator()(unsigned high, unsigned low, expr * arg) {
     return r;
 }
 
-void bv_rewriter::updt_local_params(params_ref const & p) {
-    m_hi_div0 = p.get_bool("hi_div0", true);
-    m_elim_sign_ext = p.get_bool("elim_sign_ext", true);
-    m_mul2concat = p.get_bool("mul2concat", false);
-    m_bit2bool = p.get_bool("bit2bool", true);
-    m_blast_eq_value = p.get_bool("blast_eq_value", false);
-    m_mkbv2num = p.get_bool("mkbv2num", false);
-    m_split_concat_eq = p.get_bool("split_concat_eq", false);
-    m_udiv2mul = p.get_bool("udiv2mul", false);
+void bv_rewriter::updt_local_params(params_ref const & _p) {
+    bv_rewriter_params p(_p);
+    m_hi_div0 = p.hi_div0();
+    m_elim_sign_ext = p.elim_sign_ext();
+    m_mul2concat = p.mul2concat();
+    m_bit2bool = p.bit2bool();
+    m_blast_eq_value = p.blast_eq_value();
+    m_split_concat_eq = p.split_concat_eq();
+    m_udiv2mul = p.udiv2mul();
+    m_mkbv2num = _p.get_bool("mkbv2num", false);
 }
 
 void bv_rewriter::updt_params(params_ref const & p) {
@@ -71,13 +73,7 @@ void bv_rewriter::updt_params(params_ref const & p) {
 
 void bv_rewriter::get_param_descrs(param_descrs & r) {
     poly_rewriter<bv_rewriter_core>::get_param_descrs(r);
-    r.insert("udiv2mul", CPK_BOOL, "(default: false) convert constant udiv to mul.");
-    r.insert("split_concat_eq", CPK_BOOL, "(default: false) split equalities of the form (= (concat t1 t2) t3).");
-    r.insert("bit2bool", CPK_BOOL, "(default: true) try to convert bit-vector terms of size 1 into Boolean terms.");
-    r.insert("blast_eq_value", CPK_BOOL, "(default: false) blast (some) Bit-vector equalities into bits.");
-    r.insert("elim_sign_ext", CPK_BOOL, "(default: true) expand sign-ext operator using concat and extract.");
-    r.insert("hi_div0", CPK_BOOL, "(default: true) use the 'hardware interpretation' for division by zero (for bit-vector terms).");
-    r.insert("mul2concat", CPK_BOOL, "(default: false) replace multiplication by a power of two into a concatenation.");
+    bv_rewriter_params::collect_param_descrs(r);
 #ifndef _EXTERNAL_RELEASE
     r.insert("mkbv2num", CPK_BOOL, "(default: false) convert (mkbv [true/false]*) into a numeral");         
 #endif
diff --git a/src/ast/rewriter/bv_rewriter_params.pyg b/src/ast/rewriter/bv_rewriter_params.pyg
new file mode 100644
index 000000000..780d8e724
--- /dev/null
+++ b/src/ast/rewriter/bv_rewriter_params.pyg
@@ -0,0 +1,10 @@
+def_module_params(module_name='rewriter',
+                  class_name='bv_rewriter_params',
+                  export=True,
+                  params=(("udiv2mul", BOOL, False, "convert constant udiv to mul"),
+                          ("split_concat_eq", BOOL, False, "split equalities of the form (= (concat t1 t2) t3)"),
+                          ("bit2bool", BOOL, True, "try to convert bit-vector terms of size 1 into Boolean terms"),
+                          ("blast_eq_value", BOOL, False, "blast (some) Bit-vector equalities into bits"),
+                          ("elim_sign_ext", BOOL, True, "expand sign-ext operator using concat and extract"),
+                          ("hi_div0", BOOL, True, "use the 'hardware interpretation' for division by zero (for bit-vector terms)"),
+                          ("mul2concat", BOOL, False, "replace multiplication by a power of two into a concatenation")))
diff --git a/src/ast/rewriter/poly_rewriter_def.h b/src/ast/rewriter/poly_rewriter_def.h
index e6c8a653c..290144c75 100644
--- a/src/ast/rewriter/poly_rewriter_def.h
+++ b/src/ast/rewriter/poly_rewriter_def.h
@@ -17,6 +17,7 @@ Notes:
 
 --*/
 #include"poly_rewriter.h"
+#include"poly_rewriter_params.hpp"
 #include"ast_lt.h"
 #include"ast_ll_pp.h"
 #include"ast_smt2_pp.h"
@@ -26,20 +27,18 @@ char const * poly_rewriter<Config>::g_ste_blowup_msg = "sum of monomials blowup"
 
 
 template<typename Config>
-void poly_rewriter<Config>::updt_params(params_ref const & p) {
-    m_flat = p.get_bool("flat", true);
-    m_som  = p.get_bool("som", false);
-    m_hoist_mul = p.get_bool("hoist_mul", false);
-    m_hoist_cmul = p.get_bool("hoist_cmul", false);
-    m_som_blowup = p.get_uint("som_blowup", UINT_MAX);
+void poly_rewriter<Config>::updt_params(params_ref const & _p) {
+    poly_rewriter_params p(_p);
+    m_flat = p.flat();
+    m_som  = p.som();
+    m_hoist_mul = p.hoist_mul();
+    m_hoist_cmul = p.hoist_cmul();
+    m_som_blowup = p.som_blowup();
 }
 
 template<typename Config>
 void poly_rewriter<Config>::get_param_descrs(param_descrs & r) {
-    r.insert("som", CPK_BOOL, "(default: false) put polynomials in som-of-monomials form.");
-    r.insert("som_blowup", CPK_UINT, "(default: infty) maximum number of monomials generated when putting a polynomial in sum-of-monomials normal form");
-    r.insert("hoist_mul", CPK_BOOL, "(default: false) hoist multiplication over summation to minimize number of multiplications");
-    r.insert("hoist_cmul", CPK_BOOL, "(default: false) hoist constant multiplication over summation to minimize number of multiplications");
+    poly_rewriter_params::collect_param_descrs(r);
 }
 
 template<typename Config>
diff --git a/src/ast/rewriter/poly_rewriter_params.pyg b/src/ast/rewriter/poly_rewriter_params.pyg
new file mode 100644
index 000000000..18d1e1dba
--- /dev/null
+++ b/src/ast/rewriter/poly_rewriter_params.pyg
@@ -0,0 +1,8 @@
+def_module_params(module_name='rewriter',
+                  class_name='poly_rewriter_params',
+                  export=True,
+                  params=(("som", BOOL, False, "put polynomials in som-of-monomials form"),
+                          ("som_blowup", UINT, UINT_MAX, "maximum number of monomials generated when putting a polynomial in sum-of-monomials normal form"),
+                          ("hoist_mul", BOOL, False, "hoist multiplication over summation to minimize number of multiplications"),
+                          ("hoist_cmul", BOOL, False, "hoist constant multiplication over summation to minimize number of multiplications"),
+                          ("flat", BOOL, True, "create nary applications for and,or,+,*,bvadd,bvmul,bvand,bvor,bvxor")))
diff --git a/src/ast/rewriter/rewriter_params.pyg b/src/ast/rewriter/rewriter_params.pyg
new file mode 100644
index 000000000..3a8ed5d5e
--- /dev/null
+++ b/src/ast/rewriter/rewriter_params.pyg
@@ -0,0 +1,11 @@
+def_module_params('rewriter',
+                  description='new formula simplification module used in the tactic framework, and new solvers',
+                  export=True,
+                  params=(max_memory_param(),
+                          max_steps_param(),
+                          ("flat", BOOL, True, "create nary applications for and,or,+,*,bvadd,bvmul,bvand,bvor,bvxor"),
+                          ("push_ite_arith", BOOL, False, "push if-then-else over arithmetic terms."),
+                          ("push_ite_bv", BOOL, False, "push if-then-else over bit-vector terms."),
+                          ("pull_cheap_ite", BOOL, False, "pull if-then-else terms when cheap."),
+                          ("cache_all", BOOL, False, "cache all intermediate results.")))
+
diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp
index da4dd3860..07ee7698d 100644
--- a/src/ast/rewriter/th_rewriter.cpp
+++ b/src/ast/rewriter/th_rewriter.cpp
@@ -17,6 +17,7 @@ Notes:
 
 --*/
 #include"th_rewriter.h"
+#include"rewriter_params.hpp"
 #include"bool_rewriter.h"
 #include"arith_rewriter.h"
 #include"bv_rewriter.h"
@@ -56,14 +57,15 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
 
     ast_manager & m() const { return m_b_rw.m(); }
 
-    void updt_local_params(params_ref const & p) {
-        m_flat           = p.get_bool("flat", true);
-        m_max_memory     = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX));
-        m_max_steps      = p.get_uint("max_steps", UINT_MAX);
-        m_pull_cheap_ite = p.get_bool("pull_cheap_ite", false);
-        m_cache_all      = p.get_bool("cache_all", false);
-        m_push_ite_arith = p.get_bool("push_ite_arith", false);
-        m_push_ite_bv    = p.get_bool("push_ite_bv", false);
+    void updt_local_params(params_ref const & _p) {
+        rewriter_params p(_p);
+        m_flat           = p.flat();
+        m_max_memory     = megabytes_to_bytes(p.max_memory());
+        m_max_steps      = p.max_steps();
+        m_pull_cheap_ite = p.pull_cheap_ite();
+        m_cache_all      = p.cache_all();
+        m_push_ite_arith = p.push_ite_arith();
+        m_push_ite_bv    = p.push_ite_bv();
     }
         
     void updt_params(params_ref const & p) {
@@ -693,12 +695,7 @@ void th_rewriter::get_param_descrs(param_descrs & r) {
     arith_rewriter::get_param_descrs(r);
     bv_rewriter::get_param_descrs(r);
     array_rewriter::get_param_descrs(r);
-    insert_max_memory(r);
-    insert_max_steps(r);
-    r.insert("push_ite_arith", CPK_BOOL, "(default: false) push if-then-else over arithmetic terms.");
-    r.insert("push_ite_bv", CPK_BOOL, "(default: false) push if-then-else over bit-vector terms.");
-    r.insert("pull_cheap_ite", CPK_BOOL, "(default: false) pull if-then-else terms when cheap.");
-    r.insert("cache_all", CPK_BOOL, "(default: false) cache all intermediate results.");
+    rewriter_params::collect_param_descrs(r);
 }
 
 th_rewriter::~th_rewriter() {
diff --git a/src/ast/rewriter/th_rewriter.h b/src/ast/rewriter/th_rewriter.h
index 19a89d286..b25558dd9 100644
--- a/src/ast/rewriter/th_rewriter.h
+++ b/src/ast/rewriter/th_rewriter.h
@@ -37,9 +37,6 @@ public:
 
     void updt_params(params_ref const & p);
     static void get_param_descrs(param_descrs & r);
-    /*
-      REG_MODULE_PARAMS('simplify', 'th_rewriter::get_param_descrs')
-    */
     unsigned get_cache_size() const;
     unsigned get_num_steps() const;
 
diff --git a/src/sat/sat_asymm_branch.cpp b/src/sat/sat_asymm_branch.cpp
index a7209306a..81d631e4e 100644
--- a/src/sat/sat_asymm_branch.cpp
+++ b/src/sat/sat_asymm_branch.cpp
@@ -17,6 +17,7 @@ Revision History:
 
 --*/
 #include"sat_asymm_branch.h"
+#include"sat_asymm_branch_params.hpp"
 #include"sat_solver.h"
 #include"stopwatch.h"
 #include"trace.h"
@@ -193,18 +194,17 @@ namespace sat {
         }
     }
     
-    void asymm_branch::updt_params(params_ref const & p) {
-        m_asymm_branch        = p.get_bool("asymm_branch", true);
-        m_asymm_branch_rounds = p.get_uint("asymm_branch_rounds", 32);
-        m_asymm_branch_limit  = p.get_uint("asymm_branch_limit", 100000000);
+    void asymm_branch::updt_params(params_ref const & _p) {
+        sat_asymm_branch_params p(_p);
+        m_asymm_branch        = p.asymm_branch();
+        m_asymm_branch_rounds = p.asymm_branch_rounds();
+        m_asymm_branch_limit  = p.asymm_branch_limit();
         if (m_asymm_branch_limit > INT_MAX)
             m_asymm_branch_limit = INT_MAX;
     }
 
     void asymm_branch::collect_param_descrs(param_descrs & d) {
-        d.insert("asymm_branch", CPK_BOOL, "(default: true) asymmetric branching.");
-        d.insert("asymm_branch_rounds", CPK_UINT, "(default: 32) maximum number of rounds of asymmetric branching.");
-        d.insert("asymm_branch_limit", CPK_UINT, "approx. maximum number of literals visited during asymmetric branching.");
+        sat_asymm_branch_params::collect_param_descrs(d);
     }
     
     void asymm_branch::collect_statistics(statistics & st) {
diff --git a/src/sat/sat_asymm_branch_params.pyg b/src/sat/sat_asymm_branch_params.pyg
new file mode 100644
index 000000000..8940c64a6
--- /dev/null
+++ b/src/sat/sat_asymm_branch_params.pyg
@@ -0,0 +1,6 @@
+def_module_params(module_name='sat', 
+                  class_name='sat_asymm_branch_params',
+                  export=True,
+                  params=(('asymm_branch', BOOL, True, 'asymmetric branching'),
+                          ('asymm_branch.rounds', UINT, 32, 'maximum number of rounds of asymmetric branching'),
+                          ('asymm_branch.limit', UINT, 100000000, 'approx. maximum number of literals visited during asymmetric branching')))
diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp
index e30569d89..cc0f97ff0 100644
--- a/src/sat/sat_config.cpp
+++ b/src/sat/sat_config.cpp
@@ -18,6 +18,7 @@ Revision History:
 --*/
 #include"sat_config.h"
 #include"sat_types.h"
+#include"sat_params.hpp"
 
 namespace sat {
 
@@ -36,10 +37,11 @@ namespace sat {
         updt_params(p); 
     }
 
-    void config::updt_params(params_ref const & p) {
-        m_max_memory  = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX));
+    void config::updt_params(params_ref const & _p) {
+        sat_params p(_p);
+        m_max_memory  = megabytes_to_bytes(p.max_memory());
 
-        symbol s = p.get_sym("restart", m_luby);
+        symbol s = p.restart();
         if (s == m_luby)
             m_restart = RS_LUBY;
         else if (s == m_geometric)
@@ -47,7 +49,7 @@ namespace sat {
         else
             throw sat_param_exception("invalid restart strategy");
 
-        s = p.get_sym("phase", m_caching);
+        s = p.phase();
         if (s == m_always_false) 
             m_phase = PS_ALWAYS_FALSE;
         else if (s == m_always_true)
@@ -59,29 +61,31 @@ namespace sat {
         else
             throw sat_param_exception("invalid phase selection strategy");
 
-        m_phase_caching_on  = p.get_uint("phase_caching_on", 400);
-        m_phase_caching_off = p.get_uint("phase_caching_off", 100);
+        m_phase_caching_on  = p.phase_caching_on();
+        m_phase_caching_off = p.phase_caching_off();
 
-        m_restart_initial = p.get_uint("restart_initial", 100);
-        m_restart_factor  = p.get_double("restart_factor", 1.5);
+        m_restart_initial = p.restart_initial();
+        m_restart_factor  = p.restart_factor();
         
-        m_random_freq     = p.get_double("random_freq", 0.01);
+        m_random_freq     = p.random_freq();
 
-        m_burst_search    = p.get_uint("burst_search", 100);
+        m_burst_search    = p.burst_search();
         
-        m_max_conflicts   = p.get_uint("max_conflicts", UINT_MAX);
+        m_max_conflicts   = p.max_conflicts();
+        
+        // These parameters are not exposed
+        m_simplify_mult1  = _p.get_uint("simplify_mult1", 300);
+        m_simplify_mult2  = _p.get_double("simplify_mult2", 1.5);
+        m_simplify_max    = _p.get_uint("simplify_max", 500000);
+        // --------------------------------
 
-        m_simplify_mult1  = p.get_uint("simplify_mult1", 300);
-        m_simplify_mult2  = p.get_double("simplify_mult2", 1.5);
-        m_simplify_max    = p.get_uint("simplify_max", 500000);
-
-        s = p.get_sym("gc_strategy", m_glue_psm);
+        s = p.gc();
         if (s == m_dyn_psm) {
             m_gc_strategy     = GC_DYN_PSM;
-            m_gc_initial      = p.get_uint("gc_initial", 500);
-            m_gc_increment    = p.get_uint("gc_increment", 100);
-            m_gc_small_lbd    = p.get_uint("gc_small_lbd", 3);
-            m_gc_k            = p.get_uint("gc_k", 7);
+            m_gc_initial      = p.gc_initial();
+            m_gc_increment    = p.gc_increment();
+            m_gc_small_lbd    = p.gc_small_lbd();
+            m_gc_k            = p.gc_k();
             if (m_gc_k > 255)
                 m_gc_k = 255;
         }
@@ -96,31 +100,15 @@ namespace sat {
                 m_gc_strategy = GC_PSM_GLUE;
             else 
                 throw sat_param_exception("invalid gc strategy");
-            m_gc_initial      = p.get_uint("gc_initial", 20000);
-            m_gc_increment    = p.get_uint("gc_increment", 500);
+            m_gc_initial      = p.gc_initial();
+            m_gc_increment    = p.gc_increment();
         }
-        m_minimize_lemmas = p.get_bool("minimize_lemmas", true);
-        m_dyn_sub_res     = p.get_bool("dyn_sub_res", true);
+        m_minimize_lemmas = p.minimize_lemmas();
+        m_dyn_sub_res     = p.dyn_sub_res();
     }
 
     void config::collect_param_descrs(param_descrs & r) {
-        insert_max_memory(r);
-        r.insert("phase", CPK_SYMBOL, "(default: caching) phase selection strategy: always_false, always_true, caching, random.");
-        r.insert("phase_caching_on", CPK_UINT, "(default: 400)");
-        r.insert("phase_caching_off", CPK_UINT, "(default: 100)");
-        r.insert("restart", CPK_SYMBOL, "(default: luby) restart strategy: luby or geometric.");
-        r.insert("restart_initial", CPK_UINT, "(default: 100) initial restart (number of conflicts).");  
-        r.insert("restart_factor", CPK_DOUBLE, "(default: 1.5) restart increment factor for geometric strategy.");
-        r.insert("random_freq", CPK_DOUBLE, "(default: 0.01) frequency of random case splits.");                                                      
-        r.insert("burst_search", CPK_UINT, "(default: 100) number of conflicts before first global simplification.");
-        r.insert("max_conflicts", CPK_UINT, "(default: inf) maximum number of conflicts.");
-        r.insert("gc_strategy", CPK_SYMBOL, "(default: glue_psm) garbage collection strategy: psm, glue, glue_psm, dyn_psm.");
-        r.insert("gc_initial", CPK_UINT, "(default: 20000) learned clauses garbage collection frequence.");
-        r.insert("gc_increment", CPK_UINT, "(default: 500) increment to the garbage collection threshold.");
-        r.insert("gc_small_lbd", CPK_UINT, "(default: 3) learned clauses with small LBD are never deleted (only used in dyn_psm).");
-        r.insert("gc_k", CPK_UINT, "(default: 7) learned clauses that are inactive for k gc rounds are permanently deleted (only used in dyn_psm).");
-        r.insert("minimize_lemmas", CPK_BOOL, "(default: true) minimize learned clauses.");
-        r.insert("dyn_sub_res", CPK_BOOL, "(default: true) dynamic subsumption resolution for minimizing learned clauses.");
+        sat_params::collect_param_descrs(r);
     }
 
 };
diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg
new file mode 100644
index 000000000..71579b86a
--- /dev/null
+++ b/src/sat/sat_params.pyg
@@ -0,0 +1,20 @@
+def_module_params('sat', 
+                  export=True,
+                  description='propositional SAT solver',
+                  params=(max_memory_param(),
+                          ('phase', SYMBOL, 'caching', 'phase selection strategy: always_false, always_true, caching, random'),
+                          ('phase.caching.on', UINT, 400, 'phase caching on period (in number of conflicts)'),
+                          ('phase.caching.off', UINT, 100, 'phase caching off period (in number of conflicts)'),
+                          ('restart', SYMBOL, 'luby', 'restart strategy: luby or geometric'),
+                          ('restart.initial', UINT, 100, 'initial restart (number of conflicts)'),
+                          ('restart.factor', DOUBLE, 1.5, 'restart increment factor for geometric strategy'),
+                          ('random_freq', DOUBLE, 0.01, 'frequency of random case splits'),
+                          ('burst_search', UINT, 100, 'number of conflicts before first global simplification'),
+                          ('max_conflicts', UINT, UINT_MAX, 'maximum number of conflicts'),
+                          ('gc', SYMBOL, 'glue_psm', 'garbage collection strategy: psm, glue, glue_psm, dyn_psm'),
+                          ('gc.initial', UINT, 20000, 'learned clauses garbage collection frequence'),
+                          ('gc.increment', UINT, 500, 'increment to the garbage collection threshold'),
+                          ('gc.small_lbd', UINT, 3, 'learned clauses with small LBD are never deleted (only used in dyn_psm)'),
+                          ('gc.k', UINT, 7, 'learned clauses that are inactive for k gc rounds are permanently deleted (only used in dyn_psm)'),
+                          ('minimize_lemmas', BOOL, True, 'minimize learned clauses'),
+                          ('dyn_sub_res', BOOL, True, 'dynamic subsumption resolution for minimizing learned clauses')))
diff --git a/src/sat/sat_scc.cpp b/src/sat/sat_scc.cpp
index f2598119f..29f3f006f 100644
--- a/src/sat/sat_scc.cpp
+++ b/src/sat/sat_scc.cpp
@@ -21,6 +21,7 @@ Revision History:
 #include"sat_elim_eqs.h"
 #include"stopwatch.h"
 #include"trace.h"
+#include"sat_scc_params.hpp"
 
 namespace sat {
 
@@ -230,12 +231,13 @@ namespace sat {
         m_num_elim = 0;
     }
 
-    void scc::updt_params(params_ref const & p) {
-        m_scc = p.get_bool("scc", true);
+    void scc::updt_params(params_ref const & _p) {
+        sat_scc_params p(_p);
+        m_scc = p.scc();
     }
 
     void scc::collect_param_descrs(param_descrs & d) {
-        d.insert("scc", CPK_BOOL, "(default: true) eliminate Boolean variables by computing strongly connected components.");
+        sat_scc_params::collect_param_descrs(d);
     }
 
 };
diff --git a/src/sat/sat_scc_params.pyg b/src/sat/sat_scc_params.pyg
new file mode 100644
index 000000000..b88de4de8
--- /dev/null
+++ b/src/sat/sat_scc_params.pyg
@@ -0,0 +1,5 @@
+def_module_params(module_name='sat', 
+                  class_name='sat_scc_params',
+                  export=True,
+                  params=(('scc', BOOL, True, 'eliminate Boolean variables by computing strongly connected components'),))
+
diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp
index 8a1713647..623c73758 100644
--- a/src/sat/sat_simplifier.cpp
+++ b/src/sat/sat_simplifier.cpp
@@ -19,6 +19,7 @@ Revision History:
 
 --*/
 #include"sat_simplifier.h"
+#include"sat_simplifier_params.hpp"
 #include"sat_solver.h"
 #include"stopwatch.h"
 #include"trace.h"
@@ -1430,45 +1431,28 @@ namespace sat {
         m_new_cls.finalize();
     }
 
-    void simplifier::updt_params(params_ref const & p) {
-        m_elim_blocked_clauses    = p.get_bool("elim_blocked_clauses", false);
-        m_elim_blocked_clauses_at = p.get_uint("elim_blocked_clauses_at", 2);
-        m_blocked_clause_limit    = p.get_uint("blocked_clause_limit", 100000000);
-        m_resolution              = p.get_bool("resolution", true);
-        m_res_limit               = p.get_uint("resolution_limit", 500000000);
-        m_res_occ_cutoff          = p.get_uint("res_occ_cutoff", 10);
-        m_res_occ_cutoff1         = p.get_uint("res_occ_cutoff_range1", 8);
-        m_res_occ_cutoff2         = p.get_uint("res_occ_cutoff_range2", 5);
-        m_res_occ_cutoff3         = p.get_uint("res_occ_cutoff_range3", 3);
-        m_res_lit_cutoff1         = p.get_uint("res_lit_cutoff_range1", 700);
-        m_res_lit_cutoff2         = p.get_uint("res_lit_cutoff_range2", 400);
-        m_res_lit_cutoff3         = p.get_uint("res_lit_cutoff_range3", 300);
-        m_res_cls_cutoff1         = p.get_uint("res_cls_cutoff1", 100000);
-        m_res_cls_cutoff2         = p.get_uint("res_cls_cutoff2", 700000);
-        m_subsumption             = p.get_bool("subsumption", true);
-        m_subsumption_limit       = p.get_uint("subsumption_limit", 100000000);
+    void simplifier::updt_params(params_ref const & _p) {
+        sat_simplifier_params p(_p);
+        m_elim_blocked_clauses    = p.elim_blocked_clauses();
+        m_elim_blocked_clauses_at = p.elim_blocked_clauses_at();
+        m_blocked_clause_limit    = p.blocked_clause_limit();
+        m_resolution              = p.resolution();
+        m_res_limit               = p.resolution_limit();
+        m_res_occ_cutoff          = p.resolution_occ_cutoff();
+        m_res_occ_cutoff1         = p.resolution_occ_cutoff_range1();
+        m_res_occ_cutoff2         = p.resolution_occ_cutoff_range2();
+        m_res_occ_cutoff3         = p.resolution_occ_cutoff_range3();
+        m_res_lit_cutoff1         = p.resolution_lit_cutoff_range1();
+        m_res_lit_cutoff2         = p.resolution_lit_cutoff_range2();
+        m_res_lit_cutoff3         = p.resolution_lit_cutoff_range3();
+        m_res_cls_cutoff1         = p.resolution_cls_cutoff1();
+        m_res_cls_cutoff2         = p.resolution_cls_cutoff2();
+        m_subsumption             = p.subsumption();
+        m_subsumption_limit       = p.subsumption_limit();
     }
 
     void simplifier::collect_param_descrs(param_descrs & r) {
-        r.insert("elim_blocked_clauses", CPK_BOOL, "(default: false) eliminate blocked clauses.");
-        r.insert("elim_blocked_clauses_at", CPK_UINT, "(default: 2) eliminate blocked clauses only once at the given simplification round.");
-        r.insert("blocked_clause_limit", CPK_UINT, "(default: 100000000) maximum number of literals visited during blocked clause elimination.");
-        r.insert("resolution", CPK_BOOL, "(default: true) eliminate boolean variables using resolution.");
-        r.insert("resolution_limit", CPK_UINT, "(default: 500000000) approx. maximum number of literals visited during variable elimination.");
-        r.insert("res_occ_cutoff", CPK_UINT, "(default: 10) first cutoff (on number of positive/negative occurrences) for Boolean variable elimination.");
-        r.insert("res_occ_cutoff_range1", CPK_UINT, "(default: 8) second cutoff (number of positive/negative occurrences) for Boolean variable elimination, for problems containing less than res_cls_cutoff1 clauses.");
-        r.insert("res_occ_cutoff_range2", CPK_UINT, "(default: 5) second cutoff (number of positive/negative occurrences) for Boolean variable elimination, for problems containing more than res_cls_cutoff1 and less than res_cls_cutoff2.");
-        r.insert("res_occ_cutoff_range3", CPK_UINT, "(default: 3) second cutoff (number of positive/negative occurrences) for Boolean variable elimination, for problems containing more than res_cls_cutoff2.");
-
-        r.insert("res_lit_cutoff_range1", CPK_UINT, "(default: 700) second cutoff (total number of literals) for Boolean variable elimination, for problems containing less than res_cls_cutoff1 clauses.");
-        r.insert("res_lit_cutoff_range2", CPK_UINT, "(default: 400) second cutoff (total number of literals) for Boolean variable elimination, for problems containing more than res_cls_cutoff1 and less than res_cls_cutoff2.");
-        r.insert("res_lit_cutoff_range3", CPK_UINT, "(default: 300) second cutoff (total number of literals) for Boolean variable elimination, for problems containing more than res_cls_cutoff2.");
-
-        r.insert("res_cls_cutoff1", CPK_UINT, "(default: 100000000) limit1 - total number of problems clauses for the second cutoff of Boolean variable elimination.");
-        r.insert("res_cls_cutoff2", CPK_UINT, "(default: 700000000) limit2 - total number of problems clauses for the second cutoff of Boolean variable elimination.");
-
-        r.insert("subsumption", CPK_BOOL, "(default: true) eliminate subsumed clauses.");         
-        r.insert("subsumption_limit", CPK_UINT, "(default: 100000000) approx. maximum number of literals visited during subsumption (and subsumption resolution).");
+        sat_simplifier_params::collect_param_descrs(r);
     }
         
     void simplifier::collect_statistics(statistics & st) {
diff --git a/src/sat/sat_simplifier_params.pyg b/src/sat/sat_simplifier_params.pyg
new file mode 100644
index 000000000..6165e7e62
--- /dev/null
+++ b/src/sat/sat_simplifier_params.pyg
@@ -0,0 +1,19 @@
+def_module_params(module_name='sat', 
+                  class_name='sat_simplifier_params',
+                  export=True,
+                  params=(('elim_blocked_clauses', BOOL, False, 'eliminate blocked clauses'),
+                          ('elim_blocked_clauses_at', UINT, 2, 'eliminate blocked clauses only once at the given simplification round'),
+                          ('blocked_clause_limit', UINT, 100000000, 'maximum number of literals visited during blocked clause elimination'),
+                          ('resolution', BOOL, True, 'eliminate boolean variables using resolution'),
+                          ('resolution.limit', UINT, 500000000, 'approx. maximum number of literals visited during variable elimination'),
+                          ('resolution.occ_cutoff', UINT, 10, 'first cutoff (on number of positive/negative occurrences) for Boolean variable elimination'),
+                          ('resolution.occ_cutoff_range1', UINT, 8, 'second cutoff (number of positive/negative occurrences) for Boolean variable elimination, for problems containing less than res_cls_cutoff1 clauses'),
+                          ('resolution.occ_cutoff_range2', UINT, 5, 'second cutoff (number of positive/negative occurrences) for Boolean variable elimination, for problems containing more than res_cls_cutoff1 and less than res_cls_cutoff2'),
+                          ('resolution.occ_cutoff_range3', UINT, 3, 'second cutoff (number of positive/negative occurrences) for Boolean variable elimination, for problems containing more than res_cls_cutoff2'),
+                          ('resolution.lit_cutoff_range1', UINT, 700, 'second cutoff (total number of literals) for Boolean variable elimination, for problems containing less than res_cls_cutoff1 clauses'),
+                          ('resolution.lit_cutoff_range2', UINT, 400, 'second cutoff (total number of literals) for Boolean variable elimination, for problems containing more than res_cls_cutoff1 and less than res_cls_cutoff2'),
+                          ('resolution.lit_cutoff_range3', UINT, 300, 'second cutoff (total number of literals) for Boolean variable elimination, for problems containing more than res_cls_cutoff2'),
+                          ('resolution.cls_cutoff1', UINT, 100000000, 'limit1 - total number of problems clauses for the second cutoff of Boolean variable elimination'),
+                          ('resolution.cls_cutoff2', UINT, 700000000, 'limit2 - total number of problems clauses for the second cutoff of Boolean variable elimination'),
+                          ('subsumption', BOOL, True, 'eliminate subsumed clauses'),
+                          ('subsumption.limit', UINT, 100000000, 'approx. maximum number of literals visited during subsumption (and subsumption resolution)')))
diff --git a/src/shell/main.cpp b/src/shell/main.cpp
index fb205c872..21ee8b71c 100644
--- a/src/shell/main.cpp
+++ b/src/shell/main.cpp
@@ -77,7 +77,10 @@ void display_usage() {
     std::cout << "  " << OPT << "version    prints version number of Z3.\n";
     std::cout << "  " << OPT << "v:level    be verbose, where <level> is the verbosity level.\n";
     std::cout << "  " << OPT << "nw         disable warning messages.\n";
-    std::cout << "  " << OPT << "ps         display Z3 global (and module) parameters.\n";
+    std::cout << "  " << OPT << "p          display Z3 global (and module) parameters.\n";
+    std::cout << "  " << OPT << "pd         display Z3 global (and module) parameter descriptions.\n";
+    std::cout << "  " << OPT << "pm:name    display Z3 module ('name') parameters.\n";
+    std::cout << "  " << OPT << "pp:name    display Z3 parameter description, if 'name' is not provided, then all module names are listed.\n";
     std::cout << "  --"      << "          all remaining arguments are assumed to be part of the input file name. This option allows Z3 to read files with strange names such as: -foo.smt2.\n";
     std::cout << "\nResources:\n";
     // timeout and memout are now available on Linux and OSX too.
@@ -166,7 +169,7 @@ void parse_cmd_line_args(int argc, char ** argv) {
             }
             else if (strcmp(opt_name, "v") == 0) {
                 if (!opt_arg)
-                    error("option argument (/v:level) is missing.");
+                    error("option argument (-v:level) is missing.");
                 long lvl = strtol(opt_arg, 0, 10);
                 set_verbosity_level(lvl);
             }
@@ -175,39 +178,59 @@ void parse_cmd_line_args(int argc, char ** argv) {
             }
             else if (strcmp(opt_name, "T") == 0) {
                 if (!opt_arg)
-                    error("option argument (/T:timeout) is missing.");
+                    error("option argument (-T:timeout) is missing.");
                 long tm = strtol(opt_arg, 0, 10);
                 set_timeout(tm * 1000);
             }
             else if (strcmp(opt_name, "t") == 0) {
                 if (!opt_arg)
-                    error("option argument (/t:timeout) is missing.");
+                    error("option argument (-t:timeout) is missing.");
                 gparams::set("timeout", opt_arg);
             }
             else if (strcmp(opt_name, "nw") == 0) {
                 enable_warning_messages(false);
             }
-            else if (strcmp(opt_name, "ps") == 0) {
-                gparams::display(std::cout);
+            else if (strcmp(opt_name, "p") == 0) {
+                gparams::display(std::cout, 0, false, false);
+                exit(0);
+            }
+            else if (strcmp(opt_name, "pd") == 0) {
+                gparams::display(std::cout, 0, false, true);
+                exit(0);
+            }
+            else if (strcmp(opt_name, "pm") == 0) {
+                if (opt_arg) {
+                    gparams::display_module(std::cout, opt_arg);
+                }
+                else {
+                    gparams::display_modules(std::cout);
+                    std::cout << "\nUse -pm:name to display all parameters available at module 'name'\n";
+                }
+                exit(0);
+            }
+            else if (strcmp(opt_name, "pp") == 0) {
+                if (!opt_arg)
+                    error("option argument (-pp:name) is missing.");
+                gparams::display_parameter(std::cout, opt_arg);
                 exit(0);
             }
 #ifdef _TRACE
             else if (strcmp(opt_name, "tr") == 0) {
                 if (!opt_arg)
-                    error("option argument (/tr:tag) is missing.");
+                    error("option argument (-tr:tag) is missing.");
                 enable_trace(opt_arg);
             }
 #endif
 #ifdef Z3DEBUG
             else if (strcmp(opt_name, "dbg") == 0) {
                 if (!opt_arg)
-                    error("option argument (/dbg:tag) is missing.");
+                    error("option argument (-dbg:tag) is missing.");
                 enable_debug(opt_arg);
             }
 #endif
             else if (strcmp(opt_name, "memory") == 0) {
                 if (!opt_arg)
-                    error("option argument (/memory:val) is missing.");
+                    error("option argument (-memory:val) is missing.");
                 gparams::set("memory_max_size", opt_arg);
             }
             else {
diff --git a/src/tactic/fpa/fpa2bv_converter.cpp b/src/tactic/fpa/fpa2bv_converter.cpp
index f45400a55..8a4b31612 100644
--- a/src/tactic/fpa/fpa2bv_converter.cpp
+++ b/src/tactic/fpa/fpa2bv_converter.cpp
@@ -1403,7 +1403,7 @@ void fpa2bv_converter::mk_to_ieee_bv(func_decl * f, unsigned num, expr * const *
     SASSERT(num == 1);
     expr * sgn, * s, * e;
     split(args[0], sgn, s, e);    
-    result = m_bv_util.mk_concat(m_bv_util.mk_concat(sgn, s), e);
+    result = m_bv_util.mk_concat(m_bv_util.mk_concat(sgn, e), s);
 }
 
 void fpa2bv_converter::split(expr * e, expr * & sgn, expr * & sig, expr * & exp) const {
diff --git a/src/util/gparams.cpp b/src/util/gparams.cpp
index 8a5532ee0..4aecd0c05 100644
--- a/src/util/gparams.cpp
+++ b/src/util/gparams.cpp
@@ -36,13 +36,27 @@ bool is_old_param_name(symbol const & name) {
 }
 
 struct gparams::imp {
+    bool                      m_modules_registered;
     dictionary<param_descrs*> m_module_param_descrs;
     dictionary<char const *>  m_module_descrs;
     param_descrs              m_param_descrs;
     dictionary<params_ref *>  m_module_params;
     params_ref                m_params;
+
+    void check_registered() {
+        if (m_modules_registered)
+            return;
+        m_modules_registered = true;
+        gparams_register_modules();
+    }
+
+    dictionary<param_descrs*> & get_module_param_descrs() { check_registered(); return m_module_param_descrs; }
+    dictionary<char const *> & get_module_descrs() { check_registered(); return m_module_descrs; }
+    param_descrs & get_param_descrs() { check_registered(); return m_param_descrs; }
+
 public:
-    imp() {
+    imp():
+        m_modules_registered(false) {
     }
 
     ~imp() {
@@ -62,54 +76,44 @@ public:
         }
     }
 
+    // -----------------------------------------------
+    //
+    // Module registration routines.
+    // They are invoked when descriptions are initialized
+    //
+    // -----------------------------------------------
+
     void register_global(param_descrs & d) {
-        #pragma omp critical (gparams)
-        {
-           m_param_descrs.copy(d);
-        }
+        // Don't need synchronization here, this method
+        // is invoked from check_registered that is already protected.
+        m_param_descrs.copy(d);
     }
 
     void register_module(char const * module_name, param_descrs * d) {
-        #pragma omp critical (gparams)
-        {
-            symbol s(module_name);
-            param_descrs * old_d;
-            if (m_module_param_descrs.find(s, old_d)) {
-                old_d->copy(*d);
-                dealloc(d);
-            }
-            else {
-                m_module_param_descrs.insert(s, d);
-            }
+        // Don't need synchronization here, this method
+        // is invoked from check_registered that is already protected.
+        symbol s(module_name);
+        param_descrs * old_d;
+        if (m_module_param_descrs.find(s, old_d)) {
+            old_d->copy(*d);
+            dealloc(d);
+        }
+        else {
+            m_module_param_descrs.insert(s, d);
         }
     }
 
     void register_module_descr(char const * module_name, char const * descr) {
-        #pragma omp critical (gparams)
-        {
-            m_module_descrs.insert(symbol(module_name), descr);
-        }
+        // Don't need synchronization here, this method
+        // is invoked from check_registered that is already protected.
+        m_module_descrs.insert(symbol(module_name), descr);
     }
 
-    void display(std::ostream & out, unsigned indent, bool smt2_style) {
-        #pragma omp critical (gparams)
-        {
-            out << "Global parameters\n";
-            m_param_descrs.display(out, indent + 4, smt2_style);
-            out << "\n";
-            dictionary<param_descrs*>::iterator it  = m_module_param_descrs.begin();
-            dictionary<param_descrs*>::iterator end = m_module_param_descrs.end();
-            for (; it != end; ++it) {
-                out << "[module] " << it->m_key;
-                char const * descr = 0;
-                if (m_module_descrs.find(it->m_key, descr)) {
-                    out << ", description: " << descr;
-                }
-                out << "\n";
-                it->m_value->display(out, indent + 4, smt2_style);
-            }
-        }
-    }
+    // -----------------------------------------------
+    //
+    // Parameter setting & retrieval
+    //
+    // -----------------------------------------------
 
     void normalize(char const * name, /* out */ symbol & mod_name, /* out */ symbol & param_name) {
         if (*name == ':')
@@ -152,7 +156,7 @@ public:
     void throw_unknown_parameter(symbol const & param_name, symbol const & mod_name) {
         if (mod_name == symbol::null) {
             if (is_old_param_name(param_name)) {
-                throw exception("unknown parameter '%s', this is an old parameter name, invoke 'z3 -ps' to obtain the new parameter list", 
+                throw exception("unknown parameter '%s', this is an old parameter name, invoke 'z3 -p' to obtain the new parameter list", 
                                 param_name.bare_str());
             }
             else {
@@ -211,11 +215,11 @@ public:
                 symbol m, p;
                 normalize(name, m, p);
                 if (m == symbol::null) {
-                    set(m_param_descrs, p, value, m);
+                    set(get_param_descrs(), p, value, m);
                 }
                 else {
                     param_descrs * d;
-                    if (m_module_param_descrs.find(m, d)) {
+                    if (get_module_param_descrs().find(m, d)) {
                         set(*d, p, value, m);
                     }
                     else {
@@ -223,7 +227,7 @@ public:
                     }
                 }
             }
-            catch (exception & ex) {
+            catch (z3_exception & ex) {
                 // Exception cannot cross critical section boundaries.
                 error = true;
                 error_msg = ex.msg();
@@ -263,7 +267,7 @@ public:
                         r = get_value(m_params, p);
                     }
                     else {
-                        r = get_default(m_param_descrs, p, m);
+                        r = get_default(get_param_descrs(), p, m);
                     }
                 }
                 else {
@@ -273,7 +277,7 @@ public:
                     }
                     else {
                         param_descrs * d;
-                        if (m_module_param_descrs.find(m, d)) {
+                        if (get_module_param_descrs().find(m, d)) {
                             r = get_default(*d, p, m);
                         }
                         else {
@@ -282,7 +286,7 @@ public:
                     }
                 }
             }
-            catch (exception & ex) {
+            catch (z3_exception & ex) {
                 // Exception cannot cross critical section boundaries.
                 error = true;
                 error_msg = ex.msg();
@@ -315,6 +319,117 @@ public:
         return result;
     }
 
+    // -----------------------------------------------
+    //
+    // Pretty printing
+    //
+    // -----------------------------------------------
+
+    void display(std::ostream & out, unsigned indent, bool smt2_style, bool include_descr) {
+        #pragma omp critical (gparams)
+        {
+            out << "Global parameters\n";
+            get_param_descrs().display(out, indent + 4, smt2_style, include_descr);
+            out << "\n";
+            if (!smt2_style) {
+                out << "To set a module parameter, use <module-name>.<parameter-name>=value\n";
+                out << "Example:  pp.decimal=true\n";
+                out << "\n";
+            }
+            dictionary<param_descrs*>::iterator it  = get_module_param_descrs().begin();
+            dictionary<param_descrs*>::iterator end = get_module_param_descrs().end();
+            for (; it != end; ++it) {
+                out << "[module] " << it->m_key;
+                char const * descr = 0;
+                if (get_module_descrs().find(it->m_key, descr)) {
+                    out << ", description: " << descr;
+                }
+                out << "\n";
+                it->m_value->display(out, indent + 4, smt2_style, include_descr);
+            }
+        }
+    }
+
+    void display_modules(std::ostream & out) {
+        #pragma omp critical (gparams)
+        {
+            dictionary<param_descrs*>::iterator it  = get_module_param_descrs().begin();
+            dictionary<param_descrs*>::iterator end = get_module_param_descrs().end();
+            for (; it != end; ++it) {
+                out << "[module] " << it->m_key;
+                char const * descr = 0;
+                if (get_module_descrs().find(it->m_key, descr)) {
+                    out << ", description: " << descr;
+                }
+                out << "\n";
+            }
+        }
+    }
+
+    void display_module(std::ostream & out, symbol const & module_name) {
+        bool error = false;
+        std::string error_msg;
+        #pragma omp critical (gparams)
+        {
+            try {
+                param_descrs * d = 0;
+                if (!get_module_param_descrs().find(module_name, d))
+                    throw exception("unknown module '%s'", module_name.bare_str());
+                out << "[module] " << module_name;
+                char const * descr = 0;
+                if (get_module_descrs().find(module_name, descr)) {
+                    out << ", description: " << descr;
+                }
+                out << "\n";
+                d->display(out, 4, false);
+            }
+            catch (z3_exception & ex) {
+                // Exception cannot cross critical section boundaries.
+                error = true;
+                error_msg = ex.msg();
+            }
+        }
+        if (error)
+            throw exception(error_msg);
+    }
+
+    void display_parameter(std::ostream & out, char const * name) {
+        bool error = false;
+        std::string error_msg;
+        #pragma omp critical (gparams)
+        {
+            try {
+                symbol m, p;
+                normalize(name, m, p);
+                std::cout << name << " " << m << " " << p << "\n";
+                param_descrs * d;
+                if (m == symbol::null) {
+                    d = &get_param_descrs();
+                }
+                else {
+                    if (!get_module_param_descrs().find(m, d))
+                        throw exception("unknown module '%s'", m.bare_str());
+                }
+                if (!d->contains(p))
+                    throw_unknown_parameter(p, m);
+                out << "  name:           " << p << "\n";
+                if (m != symbol::null) {
+                    out << "  module:         " << m << "\n";
+                    out << "  qualified name: " << m << "." << p << "\n";
+                }
+                out << "  type:           " << d->get_kind(p) << "\n";
+                out << "  description:    " << d->get_descr(p) << "\n";
+                out << "  default value:  " << d->get_default(p) << "\n";
+            }
+            catch (z3_exception & ex) {
+                // Exception cannot cross critical section boundaries.
+                error = true;
+                error_msg = ex.msg();
+            }
+        }
+        if (error)
+            throw exception(error_msg);
+    }
 };
 
 gparams::imp * gparams::g_imp = 0;
@@ -370,15 +485,29 @@ params_ref gparams::get() {
     return g_imp->get();
 }
 
-void gparams::display(std::ostream & out, unsigned indent, bool smt2_style) {
+void gparams::display(std::ostream & out, unsigned indent, bool smt2_style, bool include_descr) {
     SASSERT(g_imp != 0);
-    g_imp->display(out, indent, smt2_style);
+    g_imp->display(out, indent, smt2_style, include_descr);
+}
+
+void gparams::display_modules(std::ostream & out) {
+    SASSERT(g_imp != 0);
+    g_imp->display_modules(out);
+}
+
+void gparams::display_module(std::ostream & out, char const * module_name) {
+    SASSERT(g_imp != 0);
+    g_imp->display_module(out, symbol(module_name));
+}
+
+void gparams::display_parameter(std::ostream & out, char const * name) {
+    SASSERT(g_imp != 0);
+    g_imp->display_parameter(out, name);
 }
 
 void gparams::init() {
     TRACE("gparams", tout << "gparams::init()\n";);
     g_imp = alloc(imp);
-    gparams_register_modules();
 }
 
 void gparams::finalize() {
diff --git a/src/util/gparams.h b/src/util/gparams.h
index 2a784a239..a41044c84 100644
--- a/src/util/gparams.h
+++ b/src/util/gparams.h
@@ -106,8 +106,13 @@ public:
     /**
        \brief Dump information about available parameters in the given output stream.
     */
-    static void display(std::ostream & out, unsigned indent = 0, bool smt2_style=false);
+    static void display(std::ostream & out, unsigned indent = 0, bool smt2_style=false, bool include_descr=true);
     
+    // Auxiliary APIs for better command line support
+    static void display_modules(std::ostream & out);
+    static void display_module(std::ostream & out, char const * module_name);
+    static void display_parameter(std::ostream & out, char const * name);
+
     /**
        \brief Initialize the global parameter management module.
        
diff --git a/src/util/params.cpp b/src/util/params.cpp
index 4f2a73e99..c0b8653ae 100644
--- a/src/util/params.cpp
+++ b/src/util/params.cpp
@@ -95,7 +95,7 @@ struct param_descrs::imp {
         bool operator()(symbol const & s1, symbol const & s2) const { return strcmp(s1.bare_str(), s2.bare_str()) < 0; }
     };
 
-    void display(std::ostream & out, unsigned indent, bool smt2_style) const {
+    void display(std::ostream & out, unsigned indent, bool smt2_style, bool include_descr) const {
         svector<symbol> names;
         dictionary<info>::iterator it  = m_info.begin();
         dictionary<info>::iterator end = m_info.end();
@@ -124,7 +124,9 @@ struct param_descrs::imp {
             info d;
             m_info.find(*it2, d);
             SASSERT(d.m_descr);
-            out << " (" << d.m_kind << ") " << d.m_descr;
+            out << " (" << d.m_kind << ")";
+            if (include_descr)
+                out << " " << d.m_descr;
             if (d.m_default != 0)
                 out << " (default: " << d.m_default << ")";
             out << "\n";
@@ -209,8 +211,8 @@ symbol param_descrs::get_param_name(unsigned i) const {
     return m_imp->get_param_name(i);
 }
 
-void param_descrs::display(std::ostream & out, unsigned indent, bool smt2_style) const {
-    return m_imp->display(out, indent, smt2_style);
+void param_descrs::display(std::ostream & out, unsigned indent, bool smt2_style, bool include_descr) const {
+    return m_imp->display(out, indent, smt2_style, include_descr);
 }
 
 void insert_max_memory(param_descrs & r) {
diff --git a/src/util/params.h b/src/util/params.h
index 68f4c967b..164de9ab3 100644
--- a/src/util/params.h
+++ b/src/util/params.h
@@ -119,7 +119,7 @@ public:
     char const * get_descr(symbol const & name) const;
     char const * get_default(char const * name) const;
     char const * get_default(symbol const & name) const;
-    void display(std::ostream & out, unsigned indent = 0, bool smt2_style=false) const;
+    void display(std::ostream & out, unsigned indent = 0, bool smt2_style=false, bool include_descr=true) const;
     unsigned size() const; 
     symbol get_param_name(unsigned idx) const;
 };