diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index 782990cd7..1df3c082e 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -1472,7 +1472,7 @@ def def_module_params(module_name, export, params):
     out.write('struct %s_params {\n' % module_name)
     out.write('  params_ref const & p;\n')
     if export:
-        out.write('  params_ref const & g;\n')
+        out.write('  params_ref g;\n')
     out.write('  %s_params(params_ref const & _p = params_ref()):\n' % module_name)
     out.write('     p(_p)')
     if export:
diff --git a/src/api/api_config_params.cpp b/src/api/api_config_params.cpp
index 7a0303234..6adcced44 100644
--- a/src/api/api_config_params.cpp
+++ b/src/api/api_config_params.cpp
@@ -36,9 +36,45 @@ namespace api {
 };
 
 extern "C" {
+    void Z3_API Z3_global_param_set(Z3_string param_id, Z3_string param_value) {
+        memory::initialize(UINT_MAX);
+        LOG_Z3_global_param_set(param_id, param_value);
+        try { 
+            gparams::set(param_id, param_value);
+        }
+        catch (z3_exception & ex) {
+            // The error handler is only available for contexts
+            // Just throw a warning.
+            std::ostringstream buffer;
+            buffer << "Error setting " << param_id << ", " << ex.msg();
+            warning_msg(buffer.str().c_str());
+        }
+    }
+
+    std::string g_Z3_global_param_get_buffer;
+    
+    Z3_bool_opt Z3_API Z3_global_param_get(Z3_string param_id, Z3_string_ptr param_value) {
+        memory::initialize(UINT_MAX);
+        LOG_Z3_global_param_get(param_id, param_value);
+        *param_value = 0;
+        try {
+            g_Z3_global_param_get_buffer = gparams::get_value(param_id);
+            *param_value = g_Z3_global_param_get_buffer.c_str();
+            return Z3_TRUE;
+        }
+        catch (z3_exception & ex) {
+            // The error handler is only available for contexts
+            // Just throw a warning.
+            std::ostringstream buffer;
+            buffer << "Error setting " << param_id << ", " << ex.msg();
+            warning_msg(buffer.str().c_str());
+            return Z3_FALSE;
+        }
+    }
+
     Z3_config Z3_API Z3_mk_config() {
+        memory::initialize(UINT_MAX);
         LOG_Z3_mk_config();
-        memory::initialize(0);
         Z3_config r = reinterpret_cast<Z3_config>(alloc(api::config_params));
         RETURN_Z3(r);
     }
@@ -49,35 +85,19 @@ extern "C" {
     }
     
     void Z3_API Z3_set_param_value(Z3_config c, char const * param_id, char const * param_value) {
-        // REMARK: we don't need Z3_config anymore
-        try { 
-            LOG_Z3_set_param_value(c, param_id, param_value);
-            gparams::set(param_id, param_value);
-        }
-        catch (gparams::exception & ex) {
-            // The error handler was not set yet.
-            // Just throw a warning.
-            std::ostringstream buffer;
-            buffer << "Error setting " << param_id << ", " << ex.msg();
-            warning_msg(buffer.str().c_str());
-        }
+        LOG_Z3_set_param_value(c, param_id, param_value);
+        // PARAM-TODO save the parameter
     }
 
     void Z3_API Z3_update_param_value(Z3_context c, Z3_string param_id, Z3_string param_value) {
-        Z3_TRY;
         LOG_Z3_update_param_value(c, param_id, param_value);
         RESET_ERROR_CODE();
-        gparams::set(param_id, param_value);
-        // TODO: set memory limits
-        // memory::set_high_watermark(static_cast<size_t>(mk_c(c)->fparams().m_memory_high_watermark)*1024*1024);
-        // memory::set_max_size(static_cast<size_t>(mk_c(c)->fparams().m_memory_max_size)*1024*1024);
-        Z3_CATCH;
+        // NOOP in the current version
     }
 
     Z3_bool Z3_API Z3_get_param_value(Z3_context c, Z3_string param_id, Z3_string* param_value) {
         LOG_Z3_get_param_value(c, param_id, param_value);
-        // TODO: we don't really have support for that anymore.
-        return false;
+        return Z3_FALSE;
     }
 
 };
diff --git a/src/api/api_datalog.cpp b/src/api/api_datalog.cpp
index 3c434600b..34ca9627a 100644
--- a/src/api/api_datalog.cpp
+++ b/src/api/api_datalog.cpp
@@ -344,7 +344,7 @@ extern "C" {
         std::istream& s) {
         ast_manager& m = mk_c(c)->m();
         dl_collected_cmds coll(m);
-        cmd_context ctx(&mk_c(c)->fparams(), false, &m);
+        cmd_context ctx(false, &m);
         install_dl_collect_cmds(coll, ctx);
         ctx.set_ignore_check(true);
         if (!parse_smt2_commands(ctx, s)) {
diff --git a/src/api/api_model.cpp b/src/api/api_model.cpp
index a6ada4ae6..80577efee 100644
--- a/src/api/api_model.cpp
+++ b/src/api/api_model.cpp
@@ -25,6 +25,7 @@ Revision History:
 #include"model.h"
 #include"model_v2_pp.h"
 #include"model_smt2_pp.h"
+#include"model_params.hpp"
 
 extern "C" {
 
@@ -488,7 +489,8 @@ extern "C" {
                            Z3_model m,
                            Z3_ast t,
                            Z3_ast * v) {
-        return Z3_model_eval(c, m, t, mk_c(c)->fparams().m_model_completion, v);
+        model_params p;
+        return Z3_model_eval(c, m, t, p.completion(), v);
     }
 
     Z3_bool Z3_API Z3_eval_func_decl(Z3_context c, 
@@ -660,7 +662,8 @@ extern "C" {
                 result.resize(result.size()-1);
         }
         else {
-            model_v2_pp(buffer, *(to_model_ref(m)), mk_c(c)->fparams().m_model_partial);
+            model_params p;
+            model_v2_pp(buffer, *(to_model_ref(m)), p.partial());
             result = buffer.str();
         }
         return mk_c(c)->mk_external_string(result);
diff --git a/src/api/api_parsers.cpp b/src/api/api_parsers.cpp
index b6d18096f..69ca1fc81 100644
--- a/src/api/api_parsers.cpp
+++ b/src/api/api_parsers.cpp
@@ -296,7 +296,7 @@ extern "C" {
                                 Z3_symbol const decl_names[],
                                 Z3_func_decl const decls[]) {
         Z3_TRY;
-        cmd_context ctx(&mk_c(c)->fparams(), false, &(mk_c(c)->m()));
+        cmd_context ctx(false, &(mk_c(c)->m()));
         ctx.set_ignore_check(true);
         if (exec) {
             ctx.set_solver(alloc(z3_context_solver, *mk_c(c)));
@@ -362,7 +362,7 @@ extern "C" {
                                          Z3_symbol decl_names[],
                                          Z3_func_decl decls[]) { 
         Z3_TRY;
-        cmd_context ctx(&mk_c(c)->fparams(), false, &(mk_c(c)->m()));
+        cmd_context ctx(false, &(mk_c(c)->m()));
         std::string s(str);
         std::istringstream is(s);
         // No logging for this one, since it private.
diff --git a/src/api/python/z3.py b/src/api/python/z3.py
index 94031cce6..b03cf1fd8 100644
--- a/src/api/python/z3.py
+++ b/src/api/python/z3.py
@@ -169,28 +169,6 @@ class Context:
         """
         Z3_interrupt(self.ref())
         
-    def set(self, *args, **kws):
-        """Set global configuration options. 
-
-        Z3 command line options can be set using this method. 
-        The option names can be specified in different ways:
-        
-        >>> ctx = Context()
-        >>> ctx.set('WELL_SORTED_CHECK', True)
-        >>> ctx.set(':well-sorted-check', True)
-        >>> ctx.set(well_sorted_check=True)
-        """
-        if __debug__:
-            _z3_assert(len(args) % 2 == 0, "Argument list must have an even number of elements.")
-        for key, value in kws.iteritems():
-            Z3_update_param_value(self.ctx, str(key).upper(), _to_param_value(value))
-        prev = None
-        for a in args:
-            if prev == None:
-                prev = a
-            else:
-                Z3_update_param_value(self.ctx, str(prev), _to_param_value(a))
-                prev = None
 
 # Global Z3 context
 _main_ctx = None
@@ -221,15 +199,37 @@ def _get_ctx(ctx):
         return ctx
 
 def set_option(*args, **kws):
-    """Update parameters of the global context `main_ctx()`, and global configuration options of Z3Py. See `Context.set()`.
-    
+    """Set Z3 global (or module) parameters.
+
     >>> set_option(precision=10)
     """
+    if __debug__:
+        _z3_assert(len(args) % 2 == 0, "Argument list must have an even number of elements.")
     new_kws = {}
     for k, v in kws.iteritems():
         if not set_pp_option(k, v):
             new_kws[k] = v
-    main_ctx().set(*args, **new_kws)
+    for key, value in new_kws.iteritems():
+        Z3_global_param_set(str(key).upper(), _to_param_value(value))
+    prev = None
+    for a in args:
+        if prev == None:
+            prev = a
+        else:
+            Z3_global_param_set(str(prev), _to_param_value(a))
+            prev = None
+
+def get_option(name):
+    """Return the value of a Z3 global (or module) parameter
+
+    >>> get_option('nlsat.reorder')
+    true
+    """
+    ptr = (ctypes.c_char_p * 1)()
+    if Z3_global_param_get(str(name), ptr):
+        r = str(ptr[0])
+        return r
+    raise Z3Exception("failed to retrieve value for '%s'" % name)
 
 #########################################
 #
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index 9570af43b..a0c6434c2 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -1233,25 +1233,82 @@ extern "C" {
 #endif // CAMLIDL
     
 #ifdef CorML3
+    /**
+        @name Configuration
+    */
+
+    /*@{*/
+    /**
+       \brief Set a global (or module) parameter.
+       This setting is shared by all Z3 contexts.
+       
+       When a Z3 module is initialized it will use the value of these parameters
+       when Z3_params objects are not provided.
+
+       The name of parameter can be composed of characters [a-z][A-Z], digits [0-9], '-' and '_'. 
+       The character '.' is a delimiter (more later).
+       
+       The parameter names are case-insensitive. The character '-' should be viewed as an "alias" for '_'.
+       Thus, the following parameter names are considered equivalent: "pp.decimal-precision"  and "PP.DECIMAL_PRECISION".
+       
+       This function can be used to set parameters for a specific Z3 module.
+       This can be done by using <module-name>.<parameter-name>.
+       For example:
+       Z3_global_param_set('pp.decimal', 'true')
+       will set the parameter "decimal" in the module "pp" to true.
+
+       def_API('Z3_global_param_set', VOID, (_in(STRING), _in(STRING)))
+    */
+    void Z3_API Z3_global_param_set(__in Z3_string param_id, __in Z3_string param_value);
+    
+    /**
+       \brief Get a global (or module) parameter.
+       
+       Returns \mlonly \c None \endmlonly \conly \c Z3_FALSE
+       if the parameter value does not exist.
+
+       \sa Z3_global_param_set
+
+       The caller must invoke #Z3_global_param_del_value to delete the value returned at \c param_value.
+
+       \remark This function cannot be invoked simultaneously from different threads without synchronization.
+       The result string stored in param_value is stored in shared location.
+
+       def_API('Z3_global_param_get', BOOL, (_in(STRING), _out(STRING)))
+    */
+    Z3_bool_opt Z3_API Z3_global_param_get(__in Z3_string param_id, __out_opt Z3_string_ptr param_value);
+
+    /*@}*/
+
     /**
         @name Create configuration
     */
     /*@{*/
 
     /**
-       \brief Create a configuration.
+       \brief Create a configuration object for the Z3 context object.
 
        Configurations are created in order to assign parameters prior to creating 
-       contexts for Z3 interaction. For example, if the users wishes to use model
+       contexts for Z3 interaction. For example, if the users wishes to use proof
        generation, then call:
 
-       \ccode{Z3_set_param_value(cfg\, "MODEL"\, "true")}
+       \ccode{Z3_set_param_value(cfg\, "proof"\, "true")}
 
        \mlonly \remark Consider using {!mk_context_x} instead of using
        explicit configuration objects. The function {!mk_context_x}
        receives an array of string pairs. This array represents the
        configuration options. \endmlonly
 
+       \remark In previous versions of Z3, the \c Z3_config was used to store
+       global and module configurations. Now, we should use \c Z3_global_param_set.
+
+       The following parameters can be set:
+        
+          - proof  (Boolean)           Enable proof generation
+          - debug_ref_count (Boolean)  Enable debug support for Z3_ast reference counting 
+          - trace  (Boolean)           Tracing support for VCC
+          - trace_file_name (String)   Trace out file for VCC traces
+
        \sa Z3_set_param_value
        \sa Z3_del_config
 
@@ -1271,18 +1328,14 @@ extern "C" {
     /**
        \brief Set a configuration parameter.
 
-       The list of all configuration parameters can be obtained using the Z3 executable:
-
-       \verbatim
-       z3.exe -ini?
-       \endverbatim
+       The following parameters can be set for 
 
        \sa Z3_mk_config
 
        def_API('Z3_set_param_value', VOID, (_in(CONFIG), _in(STRING), _in(STRING)))
     */
     void Z3_API Z3_set_param_value(__in Z3_config c, __in Z3_string param_id, __in Z3_string param_value);
-
+    
     /*@}*/
 #endif
 
@@ -1367,33 +1420,19 @@ extern "C" {
 #endif
 
     /**
-       \brief Update a mutable configuration parameter.
+       \brief This is a deprecated function. This is a NOOP in the current version of Z3.
 
-       The list of all configuration parameters can be obtained using the Z3 executable:
-
-       \verbatim
-       z3.exe -ini?
-       \endverbatim
-
-       Only a few configuration parameters are mutable once the context is created.
-       The error handler is invoked when trying to modify an immutable parameter.
-
-       \conly \sa Z3_set_param_value
-       \mlonly \sa Z3_mk_context \endmlonly
+       \deprecated Use #Z3_global_param_set.
 
        def_API('Z3_update_param_value', VOID, (_in(CONTEXT), _in(STRING), _in(STRING)))
     */
     void Z3_API Z3_update_param_value(__in Z3_context c, __in Z3_string param_id, __in Z3_string param_value);
 
     /**
-       \brief Get a configuration parameter.
+       \brief This is a deprecated function. This is a NOOP in the current version of Z3.
+       It always return Z3_FALSE.
       
-       Returns \mlonly \c None \endmlonly \conly \c Z3_FALSE
-       if the parameter value does not exist.
-
-       \conly \sa Z3_mk_config
-       \conly \sa Z3_set_param_value
-       \mlonly \sa Z3_mk_context \endmlonly
+       \deprecated Use #Z3_global_param_get
 
        def_API('Z3_get_param_value', BOOL, (_in(CONTEXT), _in(STRING), _out(STRING)))
     */
diff --git a/src/ast/pattern/expr_pattern_match.cpp b/src/ast/pattern/expr_pattern_match.cpp
index 25be8dbf0..a446ae538 100644
--- a/src/ast/pattern/expr_pattern_match.cpp
+++ b/src/ast/pattern/expr_pattern_match.cpp
@@ -388,8 +388,7 @@ expr_pattern_match::initialize(char const * spec_string) {
     m_instrs.push_back(instr(BACKTRACK));
 
     std::istringstream is(spec_string);
-    front_end_params p;
-    cmd_context      ctx(&p, true, &m_manager);
+    cmd_context      ctx(true, &m_manager);
     VERIFY(parse_smt2_commands(ctx, is));
 
     ptr_vector<expr>::const_iterator it  = ctx.begin_assertions();
diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp
index 1960cd22a..43507ed3f 100644
--- a/src/cmd_context/basic_cmds.cpp
+++ b/src/cmd_context/basic_cmds.cpp
@@ -29,6 +29,7 @@ Notes:
 #include"eval_cmd.h"
 #include"front_end_params.h"
 #include"gparams.h"
+#include"model_params.hpp"
 
 class help_cmd : public cmd {
     svector<symbol> m_cmds;
@@ -104,9 +105,10 @@ ATOMIC_CMD(get_model_cmd, "get-model", "retrieve model for the last check-sat co
         throw cmd_exception("model is not available");
     model_ref m;
     ctx.get_check_sat_result()->get_model(m);
-    if (ctx.params().m_model_v1_pp || ctx.params().m_model_v2_pp) {
+    model_params p;
+    if (p.v1() || p.v2()) {
         std::ostringstream buffer;
-        model_v2_pp(buffer, *m, ctx.params().m_model_partial);
+        model_v2_pp(buffer, *m, p.partial());
         ctx.regular_stream() << "\"" << escaped(buffer.str().c_str(), true) << "\"" << std::endl;
     } else {
         ctx.regular_stream() << "(model " << std::endl;
diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index 5dcc4268c..cd8c81387 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -316,10 +316,9 @@ public:
     }
 };
 
-cmd_context::cmd_context(front_end_params * params, bool main_ctx, ast_manager * m, symbol const & l):
+cmd_context::cmd_context(bool main_ctx, ast_manager * m, symbol const & l):
     m_main_ctx(main_ctx),
-    m_params(params == 0 ? alloc(front_end_params) : params),
-    m_params_owner(params == 0),
+    m_fparams(alloc(front_end_params)),
     m_logic(l),
     m_interactive_mode(false),
     m_global_decls(false),  // :global-decls is false by default.
@@ -359,9 +358,7 @@ cmd_context::~cmd_context() {
     finalize_probes();
     m_solver = 0;
     m_check_sat_result = 0;
-    if (m_params_owner) {
-        dealloc(m_params);
-    }
+    dealloc(m_fparams);
 }
 
 void cmd_context::set_produce_models(bool f) {
@@ -382,10 +379,6 @@ void cmd_context::set_produce_proofs(bool f) {
     params().m_proof_mode = f ? PGM_FINE : PGM_DISABLED;
 }
 
-bool cmd_context::is_smtlib2_compliant() const { 
-    return params().m_smtlib2_compliant; 
-}
-
 bool cmd_context::produce_models() const { 
     return params().m_model; 
 }
@@ -599,8 +592,9 @@ void cmd_context::init_manager() {
     m_manager  = alloc(ast_manager, params().m_proof_mode, params().m_trace_stream);
     m_pmanager = alloc(pdecl_manager, *m_manager);
     init_manager_core(true);
-    if (params().m_smtlib2_compliant)
-        m_manager->enable_int_real_coercions(false);
+    // PARAM-TODO
+    // if (params().m_smtlib2_compliant)
+    //    m_manager->enable_int_real_coercions(false);
 }
 
 void cmd_context::init_external_manager() {
diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h
index 6688f66d9..1b15c0b60 100644
--- a/src/cmd_context/cmd_context.h
+++ b/src/cmd_context/cmd_context.h
@@ -138,8 +138,7 @@ public:
 
 protected:
     bool                         m_main_ctx;
-    front_end_params *           m_params;
-    bool                         m_params_owner;
+    front_end_params *           m_fparams;
     symbol                       m_logic;
     bool                         m_interactive_mode;
     bool                         m_global_decls;
@@ -251,9 +250,8 @@ protected:
     void print_unsupported_info(symbol const& s) { if (s != symbol::null) diagnostic_stream() << "; " << s << std::endl;}
 
 public:
-    cmd_context(front_end_params * params = 0, bool main_ctx = true, ast_manager * m = 0, symbol const & l = symbol::null);
+    cmd_context(bool main_ctx = true, ast_manager * m = 0, symbol const & l = symbol::null);
     ~cmd_context(); 
-    bool is_smtlib2_compliant() const;
     void set_logic(symbol const & s);
     bool has_logic() const { return m_logic != symbol::null; }
     symbol const & get_logic() const { return m_logic; }
@@ -290,7 +288,7 @@ public:
     virtual ast_manager & get_ast_manager() { return m(); }
     pdecl_manager & pm() const { if (!m_pmanager) const_cast<cmd_context*>(this)->init_manager(); return *m_pmanager; }
     sexpr_manager & sm() const { if (!m_sexpr_manager) const_cast<cmd_context*>(this)->m_sexpr_manager = alloc(sexpr_manager); return *m_sexpr_manager; }
-    front_end_params & params() const { return *m_params; }
+    front_end_params & params() const { return *m_fparams; }
  
     void set_solver(solver * s);
     solver * get_solver() const { return m_solver.get(); }
diff --git a/src/front_end_params/README b/src/front_end_params/README
new file mode 100644
index 000000000..1ab0a2463
--- /dev/null
+++ b/src/front_end_params/README
@@ -0,0 +1,9 @@
+This directory contains the "remains" of the old parameter setting
+infrastructure used by Z3. Old code (mostly `smt::context`) is still
+based on the front_end_params structure. However, we removed support
+for the old INI file infrastructure.  Instead, we have functions for
+setting the fields of front_end_params using parameter sets
+(params_ref).  Moreover, many of the parameters in front_end_params
+are now "hidden".  That is, they can't be set from the command line or
+using the command `set-option`.
+
diff --git a/src/front_end_params/front_end_params.cpp b/src/front_end_params/front_end_params.cpp
index 9d05a3fc3..d30ec825d 100644
--- a/src/front_end_params/front_end_params.cpp
+++ b/src/front_end_params/front_end_params.cpp
@@ -22,9 +22,7 @@ void front_end_params::register_params(ini_params & p) {
     p.register_param_vector(m_param_vector.get());
     preprocessor_params::register_params(p);
     smt_params::register_params(p);
-    parser_params::register_params(p);
     arith_simplifier_params::register_params(p);
-    model_params::register_params(p);
     p.register_bool_param("at_labels_cex", m_at_labels_cex, 
                           "only use labels that contain '@' when building multiple counterexamples");
     p.register_bool_param("check_at_labels", m_check_at_labels, 
@@ -33,14 +31,12 @@ void front_end_params::register_params(ini_params & p) {
     
     p.register_bool_param("type_check", m_well_sorted_check, "enable/disable type checker");
     p.register_bool_param("well_sorted_check", m_well_sorted_check, "enable/disable type checker");
-    p.register_bool_param("interactive", m_interactive, "enable interactive mode using Simplify input format");
     p.register_unsigned_param("soft_timeout", m_soft_timeout, "set approximate timeout for each solver query (milliseconds), the value 0 represents no timeout", true);
     p.register_double_param("instruction_max", m_instr_out, "set the (approximate) maximal number of instructions per invocation of check", true);
     p.register_bool_param("auto_config", m_auto_config, "use heuristics to set Z3 configuration parameters, it is only available for the SMT-LIB input format");
     p.register_int_param("proof_mode", 0, 2, reinterpret_cast<int&>(m_proof_mode), "select proof generation mode: 0 - disabled, 1 - coarse grain, 2 - fine grain");
     p.register_bool_param("trace", m_trace, "enable tracing for the Axiom Profiler tool");
     p.register_string_param("trace_file_name", m_trace_file_name, "tracing file name");
-    p.register_bool_param("async_commands", m_async_commands, "enable/disable support for asynchronous commands in the Simplify front-end.");
     p.register_bool_param("display_config", m_display_config, "display configuration used by Z3");
 
 #ifdef _WINDOWS
@@ -51,29 +47,10 @@ void front_end_params::register_params(ini_params & p) {
                               "set hard upper limit for memory consumption (in megabytes)");
 #endif
 
-#ifndef _EXTERNAL_RELEASE
-    // external users should not have access to it.
-    p.register_bool_param("preprocess", m_preprocess);
-#endif
-
-    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);
-
-    p.register_bool_param("smtlib2_compliant", m_smtlib2_compliant);    
-
-    p.register_bool_param("ignore_bad_patterns", m_ignore_bad_patterns);
 
     PRIVATE_PARAMS({
         p.register_bool_param("ignore_checksat", m_ignore_checksat);
         p.register_bool_param("debug_ref_count", m_debug_ref_count);
-        p.register_bool_param("ignore_user_patterns", m_ignore_user_patterns);
         p.register_bool_param("incremental_core_assert", m_incremental_core_assert);
         DEBUG_CODE(p.register_int_param("copy_params", m_copy_params););
     });
diff --git a/src/front_end_params/front_end_params.h b/src/front_end_params/front_end_params.h
index b87265c01..505052450 100644
--- a/src/front_end_params/front_end_params.h
+++ b/src/front_end_params/front_end_params.h
@@ -23,22 +23,15 @@ Revision History:
 #include"ast.h"
 #include"preprocessor_params.h"
 #include"smt_params.h"
-#include"parser_params.h"
 #include"arith_simplifier_params.h"
-#include"model_params.h"
 
-struct front_end_params : public preprocessor_params, public smt_params, public parser_params, 
-                          public arith_simplifier_params, public model_params
-                           {
+struct front_end_params : public preprocessor_params, public smt_params, 
+                          public arith_simplifier_params {
     ref<param_vector>   m_param_vector;
-    unsigned            m_max_num_cex; // maximum number of counterexamples
     bool                m_at_labels_cex; // only use labels which contains the @ symbol when building multiple counterexamples.
     bool                m_check_at_labels; // check that @ labels are inserted to generate unique counter-examples.
     bool                m_default_qid;
-    bool                m_interactive;
     bool                m_well_sorted_check;
-    bool                m_ignore_bad_patterns;
-    bool                m_ignore_user_patterns;
     bool                m_incremental_core_assert; // assert conditions to the core incrementally
     unsigned            m_soft_timeout;
     double              m_instr_out;
@@ -46,32 +39,26 @@ struct front_end_params : public preprocessor_params, public smt_params, public
     unsigned            m_memory_max_size;
     proof_gen_mode      m_proof_mode;
     bool                m_auto_config;
-    bool                m_smtlib2_compliant;
 #ifdef Z3DEBUG
     int                 m_copy_params; // used for testing copy params... Invoke method copy_params(m_copy_params) in main.cpp when diff -1.
 #endif
-    bool                m_preprocess;  // temporary hack for disabling all preprocessing..
+
     bool                m_ignore_checksat; // abort before checksat... for internal debugging
     bool                m_debug_ref_count;
     bool                m_trace;
     std::string         m_trace_file_name;
     std::fstream*       m_trace_stream;
-    bool                m_async_commands;
     bool                m_display_config;
-    bool                m_user_theory_preprocess_axioms;
-    bool                m_user_theory_persist_axioms;
     bool                m_nlsat; // temporary hack until strategic_solver is ported to new tactic framework
 
+    bool                m_dump_goal_as_smt;
+
     front_end_params():
         m_param_vector(alloc(param_vector, this)),
-        m_max_num_cex(1),
         m_at_labels_cex(false),
         m_check_at_labels(false),
         m_default_qid(false),
-        m_interactive(false),
         m_well_sorted_check(true),
-        m_ignore_bad_patterns(true),
-        m_ignore_user_patterns(false),
         m_incremental_core_assert(true),
         m_soft_timeout(0),
         m_instr_out(0.0),
@@ -83,25 +70,17 @@ struct front_end_params : public preprocessor_params, public smt_params, public
 #else
         m_auto_config(false), 
 #endif
-#if    0 
-        m_smtlib2_compliant(true),
-#else
-        m_smtlib2_compliant(false),        
-#endif
 #ifdef Z3DEBUG
         m_copy_params(-1),
 #endif
-        m_preprocess(true), // temporary hack for disabling all preprocessing..
         m_ignore_checksat(false),
         m_debug_ref_count(false),
         m_trace(false),
         m_trace_file_name("z3.log"),
         m_trace_stream(NULL),
-        m_async_commands(true),
         m_display_config(false),
-        m_user_theory_preprocess_axioms(false),
-        m_user_theory_persist_axioms(false),
-        m_nlsat(false) {
+        m_nlsat(false),
+        m_dump_goal_as_smt(false) {
     }
 
     void register_params(ini_params & p);
diff --git a/src/front_end_params/model_params.cpp b/src/front_end_params/model_params.cpp
deleted file mode 100644
index a859684d8..000000000
--- a/src/front_end_params/model_params.cpp
+++ /dev/null
@@ -1,35 +0,0 @@
-/*++
-Copyright (c) 2006 Microsoft Corporation
-
-Module Name:
-
-    model_params.cpp
-
-Abstract:
-
-    <abstract>
-
-Author:
-
-    Leonardo de Moura (leonardo) 2007-08-23.
-
-Revision History:
-
---*/
-
-#include"model_params.h"
-
-void model_params::register_params(ini_params & p) {
-    p.register_bool_param("model_partial", m_model_partial, "enable/disable partial function interpretations", true);
-    p.register_bool_param("model_v1", m_model_v1_pp, 
-                          "use Z3 version 1.x pretty printer", true);
-    p.register_bool_param("model_v2", m_model_v2_pp, 
-                          "use Z3 version 2.x (x <= 16) pretty printer", true);
-    p.register_bool_param("model_compact", m_model_compact, 
-                          "try to compact function graph (i.e., function interpretations that are lookup tables", true);
-    p.register_bool_param("model_completion", m_model_completion, 
-                          "assigns an interptetation to symbols that do not have one in the current model, when evaluating expressions in the current model", true);
-
-}
-
-
diff --git a/src/front_end_params/model_params.h b/src/front_end_params/model_params.h
deleted file mode 100644
index 2718d4e5f..000000000
--- a/src/front_end_params/model_params.h
+++ /dev/null
@@ -1,43 +0,0 @@
-/*++
-Copyright (c) 2006 Microsoft Corporation
-
-Module Name:
-
-    model_params.h
-
-Abstract:
-
-    <abstract>
-
-Author:
-
-    Leonardo de Moura (leonardo) 2007-08-23.
-
-Revision History:
-
---*/
-#ifndef _MODEL_PARAMS_H_
-#define _MODEL_PARAMS_H_
-
-#include"ini_file.h"
-
-struct model_params {
-    bool m_model_partial;
-    bool m_model_compact;
-    bool m_model_v1_pp;
-    bool m_model_v2_pp;
-    bool m_model_completion;
-
-    model_params():
-        m_model_partial(false),
-        m_model_compact(false),
-        m_model_v1_pp(false),
-        m_model_v2_pp(false),
-        m_model_completion(false) {
-    }
-
-    void register_params(ini_params & p);
-};
-
-#endif /* _MODEL_PARAMS_H_ */
-
diff --git a/src/front_end_params/parser_params.cpp b/src/front_end_params/parser_params.cpp
deleted file mode 100644
index 3edd03fb0..000000000
--- a/src/front_end_params/parser_params.cpp
+++ /dev/null
@@ -1,14 +0,0 @@
-#include "parser_params.h"
-
-parser_params::parser_params() :
-    m_dump_goal_as_smt(false),
-    m_display_error_for_vs(false) {
-}
-
-void parser_params::register_params(ini_params & p) {
-    p.register_bool_param("dump_goal_as_smt", m_dump_goal_as_smt, "write goal back to output in SMT format");
-    p.register_bool_param("display_error_for_visual_studio", m_display_error_for_vs, "display error messages in Visual Studio format");
-}
-
-
-
diff --git a/src/front_end_params/parser_params.h b/src/front_end_params/parser_params.h
deleted file mode 100644
index eaab4fd81..000000000
--- a/src/front_end_params/parser_params.h
+++ /dev/null
@@ -1,33 +0,0 @@
-/*++
-Copyright (c) 2008 Microsoft Corporation
-
-Module Name:
-
-    parser_params.h
-
-Abstract:
-
-    <abstract>
-
-Author:
-
-    Nikolaj Bjorner (nbjorner) 2008-04-21.
-
-Revision History:
-
---*/
-#ifndef _PARSER_PARAMS_H_
-#define _PARSER_PARAMS_H_
-
-#include"ini_file.h"
-
-struct parser_params {
-    bool        m_dump_goal_as_smt; // re-print goal as SMT benchmark.
-    bool        m_display_error_for_vs; // print error in vs format.
-
-    parser_params();
-    void register_params(ini_params & p);
-};
-
-#endif /* _PARSER_PARAMS_H_ */
-
diff --git a/src/front_end_params/smt_params.cpp b/src/front_end_params/smt_params.cpp
index 74e279ff8..737b369b4 100644
--- a/src/front_end_params/smt_params.cpp
+++ b/src/front_end_params/smt_params.cpp
@@ -103,5 +103,17 @@ void smt_params::register_params(ini_params & p) {
     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);
+
 }
 
diff --git a/src/front_end_params/smt_params.h b/src/front_end_params/smt_params.h
index 5c62c49e3..c6b34a2d3 100644
--- a/src/front_end_params/smt_params.h
+++ b/src/front_end_params/smt_params.h
@@ -169,6 +169,7 @@ struct smt_params : public dyn_ack_params, public qi_params, public theory_arith
     //
     // -----------------------------------
     bool             m_model; 
+    bool             m_model_compact;
     bool             m_model_validate;
     bool             m_model_on_timeout;
     bool             m_model_on_final_check;
@@ -187,6 +188,15 @@ struct smt_params : public dyn_ack_params, public qi_params, public theory_arith
     // -----------------------------------
     bool             m_display_installed_theories;
 
+    // -----------------------------------
+    //
+    // From front_end_params
+    //
+    // -----------------------------------
+    bool                m_preprocess;  // temporary hack for disabling all preprocessing..
+    bool                m_user_theory_preprocess_axioms;
+    bool                m_user_theory_persist_axioms;
+    
     smt_params():
         m_display_proof(false),
         m_display_dot_proof(false),
@@ -241,11 +251,17 @@ struct smt_params : public dyn_ack_params, public qi_params, public theory_arith
         m_display_ll_bool_var2expr(false),
         m_abort_after_preproc(false),
         m_model(true),
+        m_model_compact(false),
         m_model_validate(false),
         m_model_on_timeout(false),
         m_model_on_final_check(false),
         m_progress_sampling_freq(0),
-        m_display_installed_theories(false) {
+        m_display_installed_theories(false),
+        m_preprocess(true), // temporary hack for disabling all preprocessing..
+        m_user_theory_preprocess_axioms(false),
+        m_user_theory_persist_axioms(false)
+    {
+
     }
 
     void register_params(ini_params & p);
diff --git a/src/parsers/smt/smtlib_solver.cpp b/src/parsers/smt/smtlib_solver.cpp
index dd54de350..ddcdb56c8 100644
--- a/src/parsers/smt/smtlib_solver.cpp
+++ b/src/parsers/smt/smtlib_solver.cpp
@@ -28,6 +28,8 @@ Revision History:
 #include"solver.h"
 #include"smt_strategic_solver.h"
 #include"cmd_context.h"
+#include"model_params.hpp"
+#include"parser_params.hpp"
 
 namespace smtlib {
 
@@ -35,8 +37,9 @@ namespace smtlib {
         m_ast_manager(params.m_proof_mode, params.m_trace_stream),
         m_params(params),
         m_ctx(0),
-        m_parser(parser::create(m_ast_manager, params.m_ignore_user_patterns)), 
         m_error_code(0) {
+        parser_params ps;
+        m_parser = parser::create(m_ast_manager, ps.ignore_user_patterns());
         m_parser->initialize_smtlib();
     }
 
@@ -82,7 +85,7 @@ namespace smtlib {
             // Hack: it seems SMT-LIB allow benchmarks without any :formula
             benchmark.add_formula(m_ast_manager.mk_true());
         }
-        m_ctx = alloc(cmd_context, &m_params, true, &m_ast_manager, benchmark.get_logic());
+        m_ctx = alloc(cmd_context, true, &m_ast_manager, benchmark.get_logic());
         m_ctx->set_solver(mk_smt_strategic_solver(false));
         theory::expr_iterator fit  = benchmark.begin_formulas();
         theory::expr_iterator fend = benchmark.end_formulas();
@@ -105,7 +108,8 @@ namespace smtlib {
             model_ref md;
             if (r->status() != l_false) r->get_model(md);
             if (md.get() != 0 && m_params.m_model) {
-                model_v2_pp(std::cout, *(md.get()), m_params.m_model_partial);
+                model_params p;
+                model_v2_pp(std::cout, *(md.get()), p.partial());
             }
         }
         else {
diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp
index f288c526e..c0c8d5bc5 100644
--- a/src/parsers/smt2/smt2parser.cpp
+++ b/src/parsers/smt2/smt2parser.cpp
@@ -28,7 +28,7 @@ Revision History:
 #include"rewriter.h"
 #include"has_free_vars.h"
 #include"ast_smt2_pp.h"
-#include"front_end_params.h"
+#include"parser_params.hpp"
 
 namespace smt2 {
     typedef cmd_exception parser_exception;
@@ -106,9 +106,14 @@ namespace smt2 {
         ast_manager & m() const { return m_ctx.m(); }
         pdecl_manager & pm() const { return m_ctx.pm(); }
         sexpr_manager & sm() const { return m_ctx.sm(); }
+
+        bool m_ignore_user_patterns;
+        bool m_ignore_bad_patterns;
+        bool m_display_error_for_vs;
         
-        bool ignore_user_patterns() const { return m_ctx.params().m_ignore_user_patterns; }
-        bool ignore_bad_patterns() const { return m_ctx.params().m_ignore_bad_patterns; }
+        bool ignore_user_patterns() const { return m_ignore_user_patterns; }
+        bool ignore_bad_patterns() const  { return m_ignore_bad_patterns; }
+        bool use_vs_format() const        { return m_display_error_for_vs; }
 
         struct psort_frame {
             psort_decl *     m_decl;
@@ -383,8 +388,6 @@ namespace smt2 {
         void check_int(char const * msg) { if (!curr_is_int()) throw parser_exception(msg); }
         void check_float(char const * msg) { if (!curr_is_float()) throw parser_exception(msg); }
 
-        bool use_vs_format() const { return m_ctx.params().m_display_error_for_vs; }
-
         void error(unsigned line, unsigned pos, char const * msg) {
             if (use_vs_format()) {
                 m_ctx.diagnostic_stream() << "Z3(" << line << ", " << pos << "): ERROR: " << msg;
@@ -2354,9 +2357,9 @@ namespace smt2 {
         }
 
     public:
-        parser(cmd_context & ctx, std::istream & is, bool interactive):
+        parser(cmd_context & ctx, std::istream & is, bool interactive, params_ref const & _p):
             m_ctx(ctx), 
-            m_scanner(ctx, is, interactive), 
+            m_scanner(ctx, is, interactive, _p), 
             m_curr(scanner::NULL_TOKEN),
             m_curr_cmd(0),
             m_num_bindings(0),
@@ -2393,6 +2396,11 @@ namespace smt2 {
             m_num_open_paren(0) {
             // 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();
         }
         
         ~parser() {
@@ -2487,8 +2495,8 @@ namespace smt2 {
     };
 };
 
-bool parse_smt2_commands(cmd_context & ctx, std::istream & is, bool interactive) {
-    smt2::parser p(ctx, is, interactive);
+bool parse_smt2_commands(cmd_context & ctx, std::istream & is, bool interactive, params_ref const & ps) {
+    smt2::parser p(ctx, is, interactive, ps);
     return p();
 }
 
diff --git a/src/parsers/smt2/smt2parser.h b/src/parsers/smt2/smt2parser.h
index a7264ff63..d230e5ae0 100644
--- a/src/parsers/smt2/smt2parser.h
+++ b/src/parsers/smt2/smt2parser.h
@@ -21,6 +21,6 @@ Revision History:
 
 #include"cmd_context.h"
 
-bool parse_smt2_commands(cmd_context & ctx, std::istream & is, bool interactive = false);
+bool parse_smt2_commands(cmd_context & ctx, std::istream & is, bool interactive = false, params_ref const & p = params_ref());
 
 #endif
diff --git a/src/parsers/smt2/smt2scanner.cpp b/src/parsers/smt2/smt2scanner.cpp
index b350796fc..e2b2030ac 100644
--- a/src/parsers/smt2/smt2scanner.cpp
+++ b/src/parsers/smt2/smt2scanner.cpp
@@ -17,6 +17,7 @@ Revision History:
 
 --*/
 #include"smt2scanner.h"
+#include"parser_params.hpp"
 
 namespace smt2 {
 
@@ -241,7 +242,7 @@ namespace smt2 {
         }
     }
     
-    scanner::scanner(cmd_context & ctx, std::istream& stream, bool interactive):
+    scanner::scanner(cmd_context & ctx, std::istream& stream, bool interactive, params_ref const & _p):
         m_ctx(ctx),
         m_interactive(interactive), 
         m_spos(0),
@@ -253,6 +254,10 @@ namespace smt2 {
         m_bend(0),
         m_stream(stream),
         m_cache_input(false) {
+
+        parser_params p(_p);
+        m_smtlib2_compliant = p.smt2_compliant();
+
         for (int i = 0; i < 256; ++i) {
             m_normalized[i] = (char) i;
         }
@@ -325,7 +330,7 @@ namespace smt2 {
             case '#':
                 return read_bv_literal();
             case '-':
-                if (m_ctx.is_smtlib2_compliant())
+                if (m_smtlib2_compliant)
                     return read_symbol();
                 else
                     return read_signed_number();
diff --git a/src/parsers/smt2/smt2scanner.h b/src/parsers/smt2/smt2scanner.h
index 015f05fa1..c63a09ff1 100644
--- a/src/parsers/smt2/smt2scanner.h
+++ b/src/parsers/smt2/smt2scanner.h
@@ -55,6 +55,8 @@ namespace smt2 {
         svector<char>      m_cache;
         svector<char>      m_cache_result;
         
+        bool               m_smtlib2_compliant;
+        
         char curr() const { return m_curr; }
         void new_line() { m_line++; m_spos = 0; }
         void next();
@@ -74,7 +76,7 @@ namespace smt2 {
             EOF_TOKEN
         };
         
-        scanner(cmd_context & ctx, std::istream& stream, bool interactive = false);
+        scanner(cmd_context & ctx, std::istream& stream, bool interactive = false, params_ref const & p = params_ref());
         
         ~scanner() {}    
         
diff --git a/src/parsers/util/parser_params.pyg b/src/parsers/util/parser_params.pyg
new file mode 100644
index 000000000..fa8f17a00
--- /dev/null
+++ b/src/parsers/util/parser_params.pyg
@@ -0,0 +1,6 @@
+def_module_params('parser', 
+                  export=True,
+                  params=(('ignore_user_patterns', BOOL, False, 'ignore patterns provided by the user'),
+                          ('ignore_bad_patterns',  BOOL, True, 'ignore malformed patterns'),
+                          ('error_for_visual_studio', BOOL, False, 'display error messages in Visual Studio format'),
+                          ('smt2_compliant', BOOL, False, 'enable/disable SMT-LIB 2.0 compliance')))
diff --git a/src/shell/main.cpp b/src/shell/main.cpp
index 56882a02b..bc3953c1e 100644
--- a/src/shell/main.cpp
+++ b/src/shell/main.cpp
@@ -77,7 +77,7 @@ 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 << "params     display all available parameters.\n";
+    std::cout << "  " << OPT << "ps         display all available parameters.\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.
@@ -184,10 +184,7 @@ void parse_cmd_line_args(int argc, char ** argv) {
                 if (i < argc - 1)
                     g_aux_input_file += " ";
             }
-            if (g_front_end_params->m_interactive) {
-                warning_msg("ignoring input file in interactive mode.");
-            }
-            else if (g_input_file) {
+            if (g_input_file) {
                 warning_msg("input file was already specified.");
             }
             else {
@@ -284,7 +281,7 @@ void parse_cmd_line_args(int argc, char ** argv) {
             else if (strcmp(opt_name, "nw") == 0) {
                 enable_warning_messages(false);
             }
-            else if (strcmp(opt_name, "params") == 0) {
+            else if (strcmp(opt_name, "ps") == 0) {
                 gparams::display(std::cout);
                 exit(0);
             }
@@ -324,10 +321,7 @@ void parse_cmd_line_args(int argc, char ** argv) {
             gparams::set(key, value);
         }
         else {
-            if (g_front_end_params->m_interactive) {
-                warning_msg("ignoring input file in interactive mode.");
-            }
-            else if (g_input_file) {
+            if (g_input_file) {
                 warning_msg("input file was already specified.");
             }
             else {
@@ -389,7 +383,7 @@ int main(int argc, char ** argv) {
         if (g_input_file && g_standard_input) {
             error("using standard input to read formula.");
         }
-        if (!g_input_file && !g_front_end_params->m_interactive && !g_standard_input) {
+        if (!g_input_file && !g_standard_input) {
             error("input file was not specified.");
         }
         
diff --git a/src/shell/smtlib_frontend.cpp b/src/shell/smtlib_frontend.cpp
index 08b070183..c9dcc3fa2 100644
--- a/src/shell/smtlib_frontend.cpp
+++ b/src/shell/smtlib_frontend.cpp
@@ -97,7 +97,7 @@ unsigned read_smtlib2_commands(char const* file_name, front_end_params& front_en
     g_start_time = clock();
     register_on_timeout_proc(on_timeout);
     signal(SIGINT, on_ctrl_c);
-    cmd_context ctx(&front_end_params);
+    cmd_context ctx;
 
     // temporary hack until strategic_solver is ported to new tactic framework
     if (front_end_params.m_nlsat) {
diff --git a/src/smt/proto_model/proto_model.cpp b/src/smt/proto_model/proto_model.cpp
index 4cedea228..34742e3a0 100644
--- a/src/smt/proto_model/proto_model.cpp
+++ b/src/smt/proto_model/proto_model.cpp
@@ -17,6 +17,7 @@ Revision History:
 
 --*/
 #include"proto_model.h"
+#include"model_params.hpp"
 #include"ast_pp.h"
 #include"ast_ll_pp.h"
 #include"var_subst.h"
@@ -26,15 +27,16 @@ Revision History:
 #include"model_v2_pp.h"
 #include"basic_simplifier_plugin.h"
 
-proto_model::proto_model(ast_manager & m, simplifier & s, model_params const & p):
+proto_model::proto_model(ast_manager & m, simplifier & s, params_ref const & p):
     model_core(m),
-    m_params(p),
     m_asts(m),
     m_simplifier(s),
     m_afid(m.get_family_id(symbol("array"))) {
     register_factory(alloc(basic_factory, m));
     m_user_sort_factory = alloc(user_sort_factory, m);
     register_factory(m_user_sort_factory);
+    
+    m_model_partial = model_params(p).partial();
 }
 
 void proto_model::reset_finterp() {
@@ -620,7 +622,7 @@ void proto_model::complete_partial_func(func_decl * f) {
    \brief Set the (else) field of function interpretations... 
 */
 void proto_model::complete_partial_funcs() {
-    if (m_params.m_model_partial)
+    if (m_model_partial)
         return;
 
     // m_func_decls may be "expanded" when we invoke get_some_value.
diff --git a/src/smt/proto_model/proto_model.h b/src/smt/proto_model/proto_model.h
index bd5609f33..d16586698 100644
--- a/src/smt/proto_model/proto_model.h
+++ b/src/smt/proto_model/proto_model.h
@@ -29,16 +29,15 @@ Revision History:
 #define _PROTO_MODEL_H_
 
 #include"model_core.h"
-#include"model_params.h"
 #include"value_factory.h"
 #include"plugin_manager.h"
 #include"simplifier.h"
 #include"arith_decl_plugin.h"
 #include"func_decl_dependencies.h"
 #include"model.h"
+#include"params.h"
 
 class proto_model : public model_core {
-    model_params const &          m_params; 
     ast_ref_vector                m_asts;
     plugin_manager<value_factory> m_factories;
     user_sort_factory *           m_user_sort_factory;
@@ -47,6 +46,8 @@ class proto_model : public model_core {
     func_decl_set                 m_aux_decls;
     ptr_vector<expr>              m_tmp;
 
+    bool                          m_model_partial;
+
     void reset_finterp();
 
     expr * mk_some_interp_for(func_decl * d);
@@ -60,11 +61,9 @@ class proto_model : public model_core {
 
 
 public:
-    proto_model(ast_manager & m, simplifier & s, model_params const & p);
+    proto_model(ast_manager & m, simplifier & s, params_ref const & p = params_ref());
     virtual ~proto_model(); 
 
-    model_params const & get_model_params() const { return m_params; }
-
     void register_factory(value_factory * f) { m_factories.register_plugin(f); }
 
     bool eval(expr * e, expr_ref & result, bool model_completion = false);
diff --git a/src/smt/smt_model_generator.cpp b/src/smt/smt_model_generator.cpp
index 1c441ad11..d14abc31a 100644
--- a/src/smt/smt_model_generator.cpp
+++ b/src/smt/smt_model_generator.cpp
@@ -48,7 +48,8 @@ namespace smt {
 
     void model_generator::init_model() {
         SASSERT(!m_model);
-        m_model = alloc(proto_model, m_manager, m_context->get_simplifier(), m_context->get_fparams());
+        // PARAM-TODO
+        m_model = alloc(proto_model, m_manager, m_context->get_simplifier()); // , m_context->get_fparams());
         ptr_vector<theory>::const_iterator it  = m_context->begin_theories();
         ptr_vector<theory>::const_iterator end = m_context->end_theories();
         for (; it != end; ++it) {
diff --git a/src/util/gparams.cpp b/src/util/gparams.cpp
index 27fdd828b..426789bb4 100644
--- a/src/util/gparams.cpp
+++ b/src/util/gparams.cpp
@@ -26,7 +26,6 @@ struct gparams::imp {
     param_descrs              m_param_descrs;
     dictionary<params_ref *>  m_module_params;
     params_ref                m_params;
-    params_ref                m_empty;
 public:
     imp() {
     }
@@ -49,28 +48,37 @@ public:
     }
 
     void register_global(param_descrs & d) {
-        m_param_descrs.copy(d);
+        #pragma omp critical (gparams)
+        {
+           m_param_descrs.copy(d);
+        }
     }
 
     void register_module(char const * module_name, param_descrs * d) {
-        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);
+        #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);
+            }
         }
     }
 
     void display(std::ostream & out, unsigned indent, bool smt2_style) {
-        m_param_descrs.display(out, indent, smt2_style);
-        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 << "\n";
-            it->m_value->display(out, indent + 4, smt2_style);
+        #pragma omp critical (gparams)
+        {
+            m_param_descrs.display(out, indent, smt2_style);
+            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 << "\n";
+                it->m_value->display(out, indent + 4, smt2_style);
+            }
         }
     }
 
@@ -102,15 +110,13 @@ public:
             return m_params;
         }
         else {
-            params_ref * p;
-            if (m_module_params.find(mod_name, p)) {
-                return *p;
-            }
-            else {
+            params_ref * p = 0;
+            if (!m_module_params.find(mod_name, p)) {
                 p = alloc(params_ref);
                 m_module_params.insert(mod_name, p);
-                return *p;
             }
+            SASSERT(p != 0);
+            return *p;
         }
     }
 
@@ -119,9 +125,9 @@ public:
         params_ref & ps = get_params(mod_name);
         if (k == CPK_INVALID) {
             if (mod_name == symbol::null)
-                throw default_exception("unknown parameter '%s'", param_name.bare_str());
+                throw exception("unknown parameter '%s'", param_name.bare_str());
             else
-                throw default_exception("unknown parameter '%s' at module '%s'", param_name.bare_str(), mod_name.bare_str());
+                throw exception("unknown parameter '%s' at module '%s'", param_name.bare_str(), mod_name.bare_str());
         }
         else if (k == CPK_UINT) {
             long val = strtol(value, 0, 10);
@@ -136,9 +142,9 @@ public:
             }
             else {
                 if (mod_name == symbol::null)
-                    throw default_exception("invalid value '%s' for Boolean parameter '%s'", value, param_name.bare_str());
+                    throw exception("invalid value '%s' for Boolean parameter '%s'", value, param_name.bare_str());
                 else
-                    throw default_exception("invalid value '%s' for Boolean parameter '%s' at module '%s'", value, param_name.bare_str(), mod_name.bare_str());
+                    throw exception("invalid value '%s' for Boolean parameter '%s' at module '%s'", value, param_name.bare_str(), mod_name.bare_str());
             }
         }
         else if (k == CPK_SYMBOL) {
@@ -149,47 +155,125 @@ public:
         }
         else {
             if (mod_name == symbol::null)
-                throw default_exception("unsupported parameter type '%s'", param_name.bare_str());
+                throw exception("unsupported parameter type '%s'", param_name.bare_str());
             else
-                throw default_exception("unsupported parameter type '%s' at module '%s'", param_name.bare_str(), mod_name.bare_str());
+                throw exception("unsupported parameter type '%s' at module '%s'", param_name.bare_str(), mod_name.bare_str());
         }
     }
 
     void set(char const * name, char const * value) {
-        symbol m, p;
-        normalize(name, m, p);
-        if (m == symbol::null) {
-            set(m_param_descrs, p, value, m);
-        }
-        else {
-            param_descrs * d;
-            if (m_module_param_descrs.find(m, d)) {
-                set(*d, p, value, m);
+        bool error = false;
+        std::string error_msg;
+        #pragma omp critical (gparams)
+        {
+            try {
+                symbol m, p;
+                normalize(name, m, p);
+                if (m == symbol::null) {
+                    set(m_param_descrs, p, value, m);
+                }
+                else {
+                    param_descrs * d;
+                    if (m_module_param_descrs.find(m, d)) {
+                        set(*d, p, value, m);
+                    }
+                    else {
+                        throw exception("invalid parameter, unknown module '%s'", m.bare_str());
+                    }
+                }
             }
-            else {
-                throw default_exception("invalid parameter, unknown module '%s'", m.bare_str());
+            catch (exception & ex) {
+                // Exception cannot cross critical section boundaries.
+                error = true;
+                error_msg = ex.msg();
             }
         }
+        if (error)
+            throw exception(error_msg);
+    }
+
+    std::string get_value(params_ref const & ps, symbol const & p) {
+        std::ostringstream buffer;
+        ps.display(buffer, p);
+        return buffer.str();
+    }
+
+    std::string get_default(param_descrs const & d, symbol const & p, symbol const & m) {
+        if (!d.contains(p)) {
+            if (m == symbol::null)
+                throw exception("unknown parameter '%s'", p.bare_str());
+            else
+                throw exception("unknown parameter '%s' at module '%s'", p.bare_str(), m.bare_str());
+        }
+        char const * r = d.get_default(p);
+        if (r == 0) 
+            return "default";
+        return r;
     }
 
     std::string get_value(char const * name) {
-        // TODO
-        return "";
+        std::string r;
+        bool error = false;
+        std::string error_msg;
+        #pragma omp critical (gparams)
+        {
+            try {
+                symbol m, p;
+                normalize(name, m, p);
+                if (m == symbol::null) {
+                    if (m_params.contains(p)) {
+                        r = get_value(m_params, p);
+                    }
+                    else {
+                        r = get_default(m_param_descrs, p, m);
+                    }
+                }
+                else {
+                    params_ref * ps = 0;
+                    if (m_module_params.find(m, ps) && ps->contains(p)) {
+                        r = get_value(*ps, p);
+                    }
+                    else {
+                        param_descrs * d;
+                        if (m_module_param_descrs.find(m, d)) {
+                            r = get_default(*d, p, m);
+                        }
+                        else {
+                            throw exception("unknown module '%s'", m.bare_str());
+                        }
+                    }
+                }
+            }
+            catch (exception & ex) {
+                // Exception cannot cross critical section boundaries.
+                error = true;
+                error_msg = ex.msg();
+            }
+        }
+        if (error)
+            throw exception(error_msg);
+        return r;
     }
 
-
-    params_ref const & get_module(symbol const & module_name) {
+    params_ref get_module(symbol const & module_name) {
+        params_ref result;
         params_ref * ps = 0;
-        if (m_module_params.find(module_name, ps)) {
-            return *ps;
-        }
-        else {
-            return m_empty;
+        #pragma omp critical (gparams)
+        {
+            if (m_module_params.find(module_name, ps)) {
+                result = *ps;
+            }
         }
+        return result;
     }
     
-    params_ref const & get() { 
-        return m_params;
+    params_ref get() { 
+        params_ref result;
+        #pragma omp critical (gparams)
+        {
+            result = m_params;
+        }
+        return result;
     }
 
 };
@@ -226,16 +310,16 @@ void gparams::register_module(char const * module_name, param_descrs * d) {
     g_imp->register_module(module_name, d);
 }
 
-params_ref const & gparams::get_module(char const * module_name) {
+params_ref gparams::get_module(char const * module_name) {
     return get_module(symbol(module_name));
 }
 
-params_ref const & gparams::get_module(symbol const & module_name) {
+params_ref gparams::get_module(symbol const & module_name) {
     SASSERT(g_imp != 0);
     return g_imp->get_module(module_name);
 }
 
-params_ref const & gparams::get() {
+params_ref gparams::get() {
     SASSERT(g_imp != 0);
     return g_imp->get();
 }
diff --git a/src/util/gparams.h b/src/util/gparams.h
index 7112e67f9..04e1f6051 100644
--- a/src/util/gparams.h
+++ b/src/util/gparams.h
@@ -31,7 +31,7 @@ public:
        \brief Set a global parameter \c name with \c value.
        
        The name of parameter can be composed of characters [a-z][A-Z], digits [0-9], '-' and '_'. 
-       The character '.' is used a delimiter (more later).
+       The character '.' is a delimiter (more later).
        
        The parameter names are case-insensitive. The character '-' should be viewed as an "alias" for '_'.
        Thus, the following parameter names are considered equivalent: "auto-config"  and "AUTO_CONFIG".
@@ -90,13 +90,13 @@ public:
        // In this example "p" will contain "decimal" -> true after executing this function.
        params_ref const & p = get_module_params("pp")
     */
-    static params_ref const & get_module(char const * module_name);
-    static params_ref const & get_module(symbol const & module_name);
+    static params_ref get_module(char const * module_name);
+    static params_ref get_module(symbol const & module_name);
 
     /**
        \brief Return the global parameter set (i.e., parameters that are not associated with any particular module).
     */
-    static params_ref const & get();
+    static params_ref get();
 
     /**
        \brief Dump information about available parameters in the given output stream.
diff --git a/src/util/memory_manager.cpp b/src/util/memory_manager.cpp
index b6eb648d9..be08fe50f 100644
--- a/src/util/memory_manager.cpp
+++ b/src/util/memory_manager.cpp
@@ -1,9 +1,9 @@
 #include<iostream>
 #include<stdlib.h>
+#include<limits.h>
 #include"trace.h"
 #include"memory_manager.h"
 #include"error_codes.h"
-
 // The following two function are automatically generated by the mk_make.py script.
 // The script collects ADD_INITIALIZER and ADD_FINALIZER commands in the .h files.
 // For example, rational.h contains
@@ -27,6 +27,7 @@ out_of_memory_error::out_of_memory_error():z3_error(ERR_MEMOUT) {
 }
 
 volatile bool g_memory_out_of_memory  = false;
+bool       g_memory_initialized       = false;
 long long  g_memory_alloc_size        = 0;
 long long  g_memory_max_size          = 0;
 long long  g_memory_max_used_size     = 0;
@@ -70,8 +71,20 @@ mem_usage_report g_info;
 #endif
 
 void memory::initialize(size_t max_size) {
+    bool initialize = false;
+    #pragma omp critical (z3_memory_manager)
+    {
+        // only update the maximum size if max_size != UINT_MAX
+        if (max_size != UINT_MAX) 
+            g_memory_max_size       = max_size;
+        if (!g_memory_initialized) {
+            g_memory_initialized = true;
+            initialize = true;
+        }
+    }
+    if (!initialize)
+        return;
     g_memory_out_of_memory  = false;
-    g_memory_max_size       = max_size;
     mem_initialize();
 }
 
@@ -108,8 +121,12 @@ void memory::set_max_size(size_t max_size) {
 static bool g_finalizing = false;
 
 void memory::finalize() {
-    g_finalizing = true;
-    mem_finalize();
+    if (g_memory_initialized) {
+        g_finalizing = true;
+        mem_finalize();
+        g_memory_initialized = false;
+        g_finalizing = false;
+    }
 }
 
 unsigned long long memory::get_allocation_size() {
diff --git a/src/util/params.cpp b/src/util/params.cpp
index 264149e4b..4f2a73e99 100644
--- a/src/util/params.cpp
+++ b/src/util/params.cpp
@@ -57,6 +57,10 @@ struct param_descrs::imp {
     void erase(symbol const & name) {
         m_info.erase(name);
     }
+
+    bool contains(symbol const & name) const {
+        return m_info.contains(name);
+    }
                                     
     param_kind get_kind(symbol const & name) const {
         info i;
@@ -157,6 +161,14 @@ void param_descrs::insert(char const * name, param_kind k, char const * descr, c
     insert(symbol(name), k, descr, def);
 }
 
+bool param_descrs::contains(char const * name) const {
+    return contains(symbol(name));
+}
+
+bool param_descrs::contains(symbol const & name) const {
+    return m_imp->contains(name);
+}
+
 char const * param_descrs::get_descr(char const * name) const {
     return get_descr(symbol(name));
 }
@@ -345,7 +357,7 @@ public:
                 continue;
             switch (it->second.m_kind) {
             case CPK_BOOL:
-                out << it->second.m_bool_value;
+                out << (it->second.m_bool_value?"true":"false");
                 return;
             case CPK_UINT:
                 out << it->second.m_uint_value;
diff --git a/src/util/params.h b/src/util/params.h
index 747b23e39..68f4c967b 100644
--- a/src/util/params.h
+++ b/src/util/params.h
@@ -109,6 +109,8 @@ public:
     void copy(param_descrs & other);
     void insert(char const * name, param_kind k, char const * descr, char const * def = 0);
     void insert(symbol const & name, param_kind k, char const * descr, char const * def = 0);
+    bool contains(char const * name) const;
+    bool contains(symbol const & name) const;
     void erase(char const * name);
     void erase(symbol const & name);
     param_kind get_kind(char const * name) const;