diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index 07748e0e1..5ef92b931 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -1428,7 +1428,7 @@ extern "C" {
     /**
        \brief Set a value of a context parameter.
 
-       \sa Use #Z3_global_param_set.
+       \sa Z3_global_param_set
 
        def_API('Z3_update_param_value', VOID, (_in(CONTEXT), _in(STRING), _in(STRING)))
     */
@@ -1437,7 +1437,7 @@ extern "C" {
     /**
        \brief Return the value of a context parameter.
       
-       \sa Use #Z3_global_param_get
+       \sa Z3_global_param_get
 
        def_API('Z3_get_param_value', BOOL, (_in(CONTEXT), _in(STRING), _out(STRING)))
     */
@@ -1707,7 +1707,7 @@ extern "C" {
        use the APIs for creating numerals and pass a numeric
        constant together with the sort returned by this call.
 
-       \sa Z3_get_finite_domain_sort_size.
+       \sa Z3_get_finite_domain_sort_size
 
        def_API('Z3_mk_finite_domain_sort', SORT, (_in(CONTEXT), _in(SYMBOL), _in(UINT64)))
     */
diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp
index df9efc4dd..8f65485ae 100644
--- a/src/cmd_context/basic_cmds.cpp
+++ b/src/cmd_context/basic_cmds.cpp
@@ -307,7 +307,7 @@ class set_option_cmd : public set_get_option_cmd {
         try {
             gparams::set(m_option, value);
             env_params::updt_params();
-            ctx.params().updt_params();
+            ctx.global_params_updated();
         }
         catch (gparams::exception ex) {
             throw cmd_exception(ex.msg());
@@ -517,7 +517,7 @@ public:
         }
         else {
             try {
-                std::string val = gparams::get_value(opt);
+                ctx.regular_stream() << gparams::get_value(opt) << std::endl;
             }
             catch (gparams::exception ex) {
                 ctx.print_unsupported(opt);
diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index b27e1e177..0380e91ea 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -342,6 +342,16 @@ cmd_context::~cmd_context() {
     m_check_sat_result = 0;
 }
 
+void cmd_context::global_params_updated() {
+    m_params.updt_params();
+    if (m_solver) {
+        params_ref p;
+        if (!m_params.m_auto_config)
+            p.set_bool("auto_config", false);
+        m_solver->updt_params(p);
+    }
+}
+
 void cmd_context::set_produce_models(bool f) {
     if (m_solver)
         m_solver->set_produce_models(f);
diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h
index ca3ada7cf..2edc87ca6 100644
--- a/src/cmd_context/cmd_context.h
+++ b/src/cmd_context/cmd_context.h
@@ -249,6 +249,7 @@ public:
     cmd_context(bool main_ctx = true, ast_manager * m = 0, symbol const & l = symbol::null);
     ~cmd_context(); 
     context_params  & params() { return m_params; }
+    void global_params_updated(); // this method should be invoked when global (and module) params are updated.
     void set_logic(symbol const & s);
     bool has_logic() const { return m_logic != symbol::null; }
     symbol const & get_logic() const { return m_logic; }
diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp
index c0c8d5bc5..ee93dca2f 100644
--- a/src/parsers/smt2/smt2parser.cpp
+++ b/src/parsers/smt2/smt2parser.cpp
@@ -35,6 +35,7 @@ namespace smt2 {
 
     class parser {
         cmd_context &        m_ctx;
+        params_ref           m_params;
         scanner              m_scanner;
         scanner::token       m_curr;
         cmd *                m_curr_cmd;
@@ -2285,6 +2286,10 @@ namespace smt2 {
                     shrink(m_sexpr_stack, sexpr_spos);
                     m_symbol_stack.shrink(sym_spos);
                     m_num_bindings = 0;
+                    // HACK for propagating the update of parser parameters
+                    if (norm_param_name(s) == "set_option") {
+                        updt_params();
+                    }
                     return;
                 }
                 else {
@@ -2357,9 +2362,10 @@ namespace smt2 {
         }
 
     public:
-        parser(cmd_context & ctx, std::istream & is, bool interactive, params_ref const & _p):
+        parser(cmd_context & ctx, std::istream & is, bool interactive, params_ref const & p):
             m_ctx(ctx), 
-            m_scanner(ctx, is, interactive, _p), 
+            m_params(p),
+            m_scanner(ctx, is, interactive, p), 
             m_curr(scanner::NULL_TOKEN),
             m_curr_cmd(0),
             m_num_bindings(0),
@@ -2397,15 +2403,19 @@ namespace smt2 {
             // the following assertion does not hold if ctx was already attached to an AST manager before the parser object is created.
             // SASSERT(!m_ctx.has_manager());
             
-            parser_params p(_p);
-            m_ignore_user_patterns = p.ignore_user_patterns();
-            m_ignore_bad_patterns  = p.ignore_bad_patterns();
-            m_display_error_for_vs = p.error_for_visual_studio();
+            updt_params();
         }
         
         ~parser() {
             reset_stack();
         }
+
+        void updt_params() {
+            parser_params p(m_params);
+            m_ignore_user_patterns = p.ignore_user_patterns();
+            m_ignore_bad_patterns  = p.ignore_bad_patterns();
+            m_display_error_for_vs = p.error_for_visual_studio();
+        }
   
         void reset() {
             reset_stack();
diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg
index bcdf78b73..ee583ff85 100644
--- a/src/smt/params/smt_params_helper.pyg
+++ b/src/smt/params/smt_params_helper.pyg
@@ -35,6 +35,7 @@ def_module_params(module_name='smt',
                           ('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.propagation_mode', UINT, 2, '0 - no propagation, 1 - propagate existing literals, 2 - refine bounds'),
                           ('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 5a1101524..7281a5daa 100644
--- a/src/smt/params/theory_arith_params.cpp
+++ b/src/smt/params/theory_arith_params.cpp
@@ -32,6 +32,7 @@ void theory_arith_params::updt_params(params_ref const & _p) {
     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();
+    m_arith_bound_prop = static_cast<bound_prop_mode>(p.arith_propagation_mode());
 }
 
 
diff --git a/src/tactic/core/nnf_tactic.cpp b/src/tactic/core/nnf_tactic.cpp
index fdaf03d55..a79a4ed06 100644
--- a/src/tactic/core/nnf_tactic.cpp
+++ b/src/tactic/core/nnf_tactic.cpp
@@ -120,7 +120,7 @@ tactic * mk_snf_tactic(ast_manager & m, params_ref const & p) {
 
 tactic * mk_nnf_tactic(ast_manager & m, params_ref const & p) {
     params_ref new_p(p);
-    new_p.set_sym("nnf_mode", symbol("full"));
+    new_p.set_sym("mode", symbol("full"));
     TRACE("nnf", tout << "mk_nnf: " << new_p << "\n";);
     return using_params(mk_snf_tactic(m, p), new_p);
 }