diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index 1df3c082e..277a7e702 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -1784,7 +1784,7 @@ def mk_gparams_register_modules(cnames, path):
                     mod_cmds.append((m.group(1), m.group(2)))
     fout.write('void gparams_register_modules() {\n')
     for code in cmds:
-        fout.write('{ param_descrs d; %s(*d); gparams::register_global(d); }\n' % code)
+        fout.write('{ param_descrs d; %s(d); gparams::register_global(d); }\n' % code)
     for (mod, code) in mod_cmds:
         fout.write('{ param_descrs * d = alloc(param_descrs); %s(*d); gparams::register_module("%s", d); }\n' % (code, mod))
     fout.write('}\n')
diff --git a/src/api/api_config_params.cpp b/src/api/api_config_params.cpp
index 6adcced44..c14e68919 100644
--- a/src/api/api_config_params.cpp
+++ b/src/api/api_config_params.cpp
@@ -24,6 +24,7 @@ Revision History:
 #include"cmd_context.h"
 #include"symbol.h"
 #include"gparams.h"
+#include"env_params.h"
 
 namespace api {
 
@@ -41,6 +42,7 @@ extern "C" {
         LOG_Z3_global_param_set(param_id, param_value);
         try { 
             gparams::set(param_id, param_value);
+            env_params::updt_params();
         }
         catch (z3_exception & ex) {
             // The error handler is only available for contexts
diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index 7a06f30bf..984a535c7 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -1309,7 +1309,7 @@ void cmd_context::pop(unsigned n) {
 void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions) {
     if (m_ignore_check)
         return;
-    IF_VERBOSE(100, verbose_stream() << "check-sat..." << std::endl;);
+    IF_VERBOSE(100, verbose_stream() << "(started \"check-sat\")" << std::endl;);
     TRACE("before_check_sat", dump_assertions(tout););
     if (!has_manager())
         init_manager();
diff --git a/src/shell/main.cpp b/src/shell/main.cpp
index b08d02812..90473c21f 100644
--- a/src/shell/main.cpp
+++ b/src/shell/main.cpp
@@ -33,6 +33,7 @@ Revision History:
 #include"z3_exception.h"
 #include"error_codes.h"
 #include"gparams.h"
+#include"env_params.h"
 
 typedef enum { IN_UNSPECIFIED, IN_SMTLIB, IN_SMTLIB_2, IN_DATALOG, IN_DIMACS, IN_Z3_LOG } input_kind;
 
@@ -106,12 +107,6 @@ public:
     }
 
     virtual ~extra_params() {}
-
-    // PARAM-TODO
-    // virtual void register_params(ini_params & p) {
-        // datalog_params::register_params(p);
-        // p.register_bool_param("STATISTICS", m_statistics, "display statistics");
-    // }
 };
 
 extra_params*       g_extra_params = 0;
@@ -123,8 +118,6 @@ void init_params() {
         g_front_end_params = new front_end_params();
         // g_params = new ini_params();
         g_extra_params = new extra_params();
-        // register_verbosity_level(*g_params);
-        // register_warning(*g_params);
         // g_front_end_params->register_params(*g_params);
         // g_extra_params->register_params(*g_params);
         g_params_initialized = true;
@@ -304,9 +297,6 @@ class global_state_initialiser {
 public:
     global_state_initialiser() {
         memory::initialize(0);
-#if defined(_WINDOWS) && defined(_Z3_BUILD_PARALLEL_SMT)
-        memory::mem->set_threaded_mode(true);
-#endif
         init_params();
     }
 
@@ -326,8 +316,8 @@ int main(int argc, char ** argv) {
         global_state_initialiser global_state;
         memory::exit_when_out_of_memory(true, "ERROR: out of memory");
         parse_cmd_line_args(argc, argv);
-        memory::set_high_watermark(static_cast<size_t>(g_front_end_params->m_memory_high_watermark) * 1024 * 1024);
-        memory::set_max_size(static_cast<size_t>(g_front_end_params->m_memory_max_size) * 1024 * 1024);
+        env_params::updt_params();
+
         g_front_end_params->open_trace_file();
         if (g_input_file && g_standard_input) {
             error("using standard input to read formula.");
diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp
index c548eca94..513aa7634 100644
--- a/src/smt/asserted_formulas.cpp
+++ b/src/smt/asserted_formulas.cpp
@@ -248,7 +248,6 @@ void asserted_formulas::reduce() {
     if (m_macro_manager.has_macros())
         expand_macros();
     TRACE("before_reduce", display(tout););
-    IF_VERBOSE(10000, verbose_stream() << "total size: " << get_total_size() << "\n";);
     CASSERT("well_sorted", check_well_sorted());
 
 #define INVOKE(COND, FUNC) if (COND) { FUNC; IF_VERBOSE(10000, verbose_stream() << "total size: " << get_total_size() << "\n";); }  TRACE("reduce_step_ll", ast_mark visited; display_ll(tout, visited);); TRACE("reduce_step", display(tout << #FUNC << " ");); CASSERT("well_sorted",check_well_sorted()); if (inconsistent() || canceled()) { TRACE("after_reduce", display(tout);); TRACE("after_reduce_ll", ast_mark visited; display_ll(tout, visited);); return;  }
@@ -280,7 +279,7 @@ void asserted_formulas::reduce() {
 
     CASSERT("well_sorted",check_well_sorted());
 
-    IF_VERBOSE(10, verbose_stream() << "simplifier done.\n";);
+    IF_VERBOSE(10, verbose_stream() << "(smt.simplifier-done)\n";);
     TRACE("after_reduce", display(tout););
     TRACE("after_reduce_ll", ast_mark visited; display_ll(tout, visited););
     TRACE("macros", m_macro_manager.display(tout););
@@ -288,7 +287,7 @@ void asserted_formulas::reduce() {
 }
 
 void asserted_formulas::eliminate_and() {
-    IF_IVERBOSE(10, verbose_stream() << "eliminating and...\n";);
+    IF_IVERBOSE(10, verbose_stream() << "(smt.eliminating-and)\n";);
     set_eliminate_and(true);
     reduce_asserted_formulas();    
     TRACE("after_elim_and", display(tout););
@@ -393,19 +392,19 @@ void asserted_formulas::find_macros_core() {
 }
 
 void asserted_formulas::find_macros() {
-    IF_IVERBOSE(10, verbose_stream() << "trying to find macros...\n";);
+    IF_IVERBOSE(10, verbose_stream() << "(smt.find-macros)\n";);
     TRACE("before_find_macros", display(tout););
     find_macros_core();
     TRACE("after_find_macros", display(tout););
 }
 
 void asserted_formulas::expand_macros() {
-    IF_IVERBOSE(10, verbose_stream() << "expanding macros...\n";);
+    IF_IVERBOSE(10, verbose_stream() << "(smt.expand-macros)\n";);
     find_macros_core();
 }
 
 void asserted_formulas::apply_quasi_macros() {
-    IF_IVERBOSE(10, verbose_stream() << "finding quasi macros...\n";);
+    IF_IVERBOSE(10, verbose_stream() << "(smt.find-quasi-macros)\n";);
     TRACE("before_quasi_macros", display(tout););
     expr_ref_vector  new_exprs(m_manager);
     proof_ref_vector new_prs(m_manager);      
@@ -423,7 +422,7 @@ void asserted_formulas::apply_quasi_macros() {
 }
 
 void asserted_formulas::nnf_cnf() {
-    IF_IVERBOSE(10, verbose_stream() << "applying nnf...\n";);
+    IF_IVERBOSE(10, verbose_stream() << "(smt.nnf)\n";);
     nnf              apply_nnf(m_manager, m_defined_names);
     expr_ref_vector  new_exprs(m_manager);
     proof_ref_vector new_prs(m_manager);
@@ -471,7 +470,7 @@ void asserted_formulas::nnf_cnf() {
 
 #define MK_SIMPLE_SIMPLIFIER(NAME, FUNCTOR_DEF, LABEL, MSG)                                                             \
 void asserted_formulas::NAME() {                                                                                        \
-    IF_IVERBOSE(10, verbose_stream() << MSG << "...\n";);                                                                      \
+    IF_IVERBOSE(10, verbose_stream() << "(smt." << MSG << ")\n";);     \
     TRACE(LABEL, tout << "before:\n"; display(tout););                                                                  \
     FUNCTOR_DEF;                                                                                                        \
     expr_ref_vector  new_exprs(m_manager);                                                                              \
@@ -503,16 +502,16 @@ void asserted_formulas::NAME() {
     TRACE(LABEL, display(tout););                                                                                       \
 }
 
-MK_SIMPLE_SIMPLIFIER(apply_distribute_forall, distribute_forall functor(m_manager, *m_bsimp), "distribute_forall", "distribute forall");
+MK_SIMPLE_SIMPLIFIER(apply_distribute_forall, distribute_forall functor(m_manager, *m_bsimp), "distribute_forall", "distribute-forall");
 
 void asserted_formulas::reduce_and_solve() {
-    IF_IVERBOSE(10, verbose_stream() << "reducing...\n";);
+    IF_IVERBOSE(10, verbose_stream() << "(smt.reducing)\n";);
     flush_cache(); // collect garbage
     reduce_asserted_formulas();
 }
 
 void asserted_formulas::infer_patterns() {
-    IF_IVERBOSE(10, verbose_stream() << "pattern inference...\n";);
+    IF_IVERBOSE(10, verbose_stream() << "(smt.pattern-inference)\n";);
     TRACE("before_pattern_inference", display(tout););
     pattern_inference infer(m_manager, m_params);
     expr_ref_vector  new_exprs(m_manager);
@@ -546,7 +545,7 @@ void asserted_formulas::commit() {
 }
 
 void asserted_formulas::eliminate_term_ite() {
-    IF_IVERBOSE(10, verbose_stream() << "eliminating ite term...\n";);
+    IF_IVERBOSE(10, verbose_stream() << "(smt.eliminating-ite-term)\n";);
     TRACE("before_elim_term_ite", display(tout););
     elim_term_ite   elim(m_manager, m_defined_names);
     expr_ref_vector  new_exprs(m_manager);
@@ -583,7 +582,7 @@ void asserted_formulas::eliminate_term_ite() {
 }
 
 void asserted_formulas::propagate_values() {
-    IF_IVERBOSE(10, verbose_stream() << "constant propagation...\n";);
+    IF_IVERBOSE(10, verbose_stream() << "(smt.constant-propagation)\n";);
     TRACE("propagate_values", tout << "before:\n"; display(tout););
     flush_cache();
     bool found = false;
@@ -661,7 +660,7 @@ void asserted_formulas::propagate_booleans() {
     flush_cache();
     while (cont) {
         TRACE("propagate_booleans", tout << "before:\n"; display(tout););
-        IF_IVERBOSE(10, verbose_stream() << "boolean propagation...\n";);
+        IF_IVERBOSE(10, verbose_stream() << "(smt.propagate-booleans)\n";);
         cont        = false;
         unsigned i  = m_asserted_qhead;
         unsigned sz = m_asserted_formulas.size();
@@ -704,7 +703,7 @@ void asserted_formulas::propagate_booleans() {
 
 #define MK_SIMPLIFIER(NAME, FUNCTOR, TAG, MSG, REDUCE)                  \
 bool asserted_formulas::NAME() {                                        \
-    IF_IVERBOSE(10, verbose_stream() << MSG << "...\n";);               \
+    IF_IVERBOSE(10, verbose_stream() << "(smt." << MSG << ")\n";);     \
     TRACE(TAG, ast_mark visited; display_ll(tout, visited););           \
     FUNCTOR;                                                            \
     bool changed = false;                                               \
@@ -741,9 +740,9 @@ bool asserted_formulas::NAME() {                                        \
     return changed;                                                     \
 }
 
-MK_SIMPLIFIER(pull_cheap_ite_trees, pull_cheap_ite_tree_star functor(m_manager, m_simplifier), "pull_cheap_ite_trees", "pull cheap ite trees", false);
+MK_SIMPLIFIER(pull_cheap_ite_trees, pull_cheap_ite_tree_star functor(m_manager, m_simplifier), "pull_cheap_ite_trees", "pull-cheap-ite-trees", false);
 
-MK_SIMPLIFIER(pull_nested_quantifiers, pull_nested_quant functor(m_manager), "pull_nested_quantifiers", "pull nested quantifiers", false);
+MK_SIMPLIFIER(pull_nested_quantifiers, pull_nested_quant functor(m_manager), "pull_nested_quantifiers", "pull-nested-quantifiers", false);
 
 proof * asserted_formulas::get_inconsistency_proof() const {
     if (!inconsistent())
@@ -761,7 +760,7 @@ proof * asserted_formulas::get_inconsistency_proof() const {
 }
 
 void asserted_formulas::refine_inj_axiom() {
-    IF_IVERBOSE(10, verbose_stream() << "refining injectivity...\n";);
+    IF_IVERBOSE(10, verbose_stream() << "(smt.refine-injectivity)\n";);
     TRACE("inj_axiom", display(tout););
     unsigned i  = m_asserted_qhead;
     unsigned sz = m_asserted_formulas.size();
@@ -783,9 +782,9 @@ void asserted_formulas::refine_inj_axiom() {
     TRACE("inj_axiom", display(tout););
 }
 
-MK_SIMPLIFIER(apply_bit2int, bit2int& functor = m_bit2int, "bit2int", "propagate bit-vector over integers", true);
+MK_SIMPLIFIER(apply_bit2int, bit2int& functor = m_bit2int, "bit2int", "propagate-bit-vector-over-integers", true);
 
-MK_SIMPLIFIER(cheap_quant_fourier_motzkin, elim_bounds_star functor(m_manager), "elim_bounds", "cheap fourier-motzkin", true);
+MK_SIMPLIFIER(cheap_quant_fourier_motzkin, elim_bounds_star functor(m_manager), "elim_bounds", "cheap-fourier-motzkin", true);
 
 // MK_SIMPLIFIER(quant_elim, qe::expr_quant_elim_star1 &functor = m_quant_elim, 
 //              "quantifiers", "quantifier elimination procedures", true);
@@ -795,11 +794,11 @@ bool asserted_formulas::quant_elim() {
     return false;
 }
 
-MK_SIMPLIFIER(elim_bvs_from_quantifiers, bv_elim_star functor(m_manager), "bv_elim", "eliminate bit-vectors from quantifiers", true);
+MK_SIMPLIFIER(elim_bvs_from_quantifiers, bv_elim_star functor(m_manager), "bv_elim", "eliminate-bit-vectors-from-quantifiers", true);
 
 #define LIFT_ITE(NAME, FUNCTOR, MSG)                                                                                            \
 void asserted_formulas::NAME() {                                                                                                \
-    IF_IVERBOSE(10, verbose_stream() << MSG;);                                                                                         \
+    IF_IVERBOSE(10, verbose_stream() << "(smt." << MSG << ")\n";);            \
     TRACE("lift_ite", display(tout););                                                                                          \
     FUNCTOR;                                                                                                                    \
     unsigned i  = m_asserted_qhead;                                                                                             \
@@ -822,8 +821,8 @@ void asserted_formulas::NAME() {
     reduce_and_solve();                                                                                                         \
 }
 
-LIFT_ITE(lift_ite, push_app_ite functor(m_simplifier, m_params.m_lift_ite == LI_CONSERVATIVE), "lifting ite...\n");
-LIFT_ITE(ng_lift_ite, ng_push_app_ite functor(m_simplifier, m_params.m_ng_lift_ite == LI_CONSERVATIVE), "lifting ng ite...\n");
+LIFT_ITE(lift_ite, push_app_ite functor(m_simplifier, m_params.m_lift_ite == LI_CONSERVATIVE), "lifting ite");
+LIFT_ITE(ng_lift_ite, ng_push_app_ite functor(m_simplifier, m_params.m_ng_lift_ite == LI_CONSERVATIVE), "lifting ng ite");
 
 unsigned asserted_formulas::get_total_size() const {
     expr_mark visited;
@@ -835,7 +834,7 @@ unsigned asserted_formulas::get_total_size() const {
 }
 
 void asserted_formulas::max_bv_sharing() {
-    IF_IVERBOSE(10, verbose_stream() << "maximizing bv sharing...\n";);
+    IF_IVERBOSE(10, verbose_stream() << "(smt.maximizing-bv-sharing)\n";);
     TRACE("bv_sharing", display(tout););
     unsigned i  = m_asserted_qhead;
     unsigned sz = m_asserted_formulas.size();
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index c51a1ebc1..1aae1c62a 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -2488,7 +2488,7 @@ namespace smt {
         SASSERT(check_clauses(m_lemmas));
         SASSERT(check_clauses(m_aux_clauses));
 
-        IF_VERBOSE(2, verbose_stream() << "simplifying clause set... "; verbose_stream().flush(););
+        IF_VERBOSE(2, verbose_stream() << "(smt.simplifying-clause-set"; verbose_stream().flush(););
 
         // m_simp_counter is used to balance the cost of simplify_clause.
         //
@@ -2503,8 +2503,7 @@ namespace smt {
         // the field m_simp_qhead is used to check whether there are 
         // new assigned literals at the base level.
         m_simp_qhead = m_assigned_literals.size();
-        
-        unsigned num_clauses     = m_aux_clauses.size() + m_lemmas.size();
+
         unsigned num_del_clauses = 0;
 
         SASSERT(m_scope_lvl == m_base_lvl);
@@ -2519,7 +2518,7 @@ namespace smt {
             num_del_clauses += simplify_clauses(m_lemmas, bs.m_lemmas_lim);
         }
         TRACE("simp_counter", tout << "simp_counter: " << m_simp_counter << " scope_lvl: " << m_scope_lvl << "\n";);
-        IF_VERBOSE(2, verbose_stream() << "num. deleted clauses: " << num_del_clauses << " (out of " << num_clauses << ")" << std::endl;);
+        IF_VERBOSE(2, verbose_stream() << " :num-deleted-clauses " << num_del_clauses << ")" << std::endl;);
         TRACE("simplify_clauses_detail", tout << "after:\n"; display_clauses(tout, m_lemmas););
         SASSERT(check_clauses(m_lemmas) && check_clauses(m_aux_clauses));
     }
@@ -2551,7 +2550,7 @@ namespace smt {
         SASSERT(start_at <= sz);
         if (start_at + m_fparams.m_recent_lemmas_size >= sz)
             return;
-        IF_VERBOSE(2, verbose_stream() << "deleting inactive lemmas... "; verbose_stream().flush(););
+        IF_VERBOSE(2, verbose_stream() << "(smt.delete-inactive-lemmas"; verbose_stream().flush(););
         SASSERT (m_fparams.m_recent_lemmas_size < sz);
         unsigned end_at        = sz - m_fparams.m_recent_lemmas_size;
         SASSERT(start_at < end_at);
@@ -2595,7 +2594,7 @@ namespace smt {
                 cls->set_activity(cls->get_activity() / m_fparams.m_clause_decay);
             }
         }
-        IF_VERBOSE(2, verbose_stream() << "num. deleted clauses: " << num_del_cls << " (out of " << sz << ")" << std::endl;);
+        IF_VERBOSE(2, verbose_stream() << " :num-deleted-clauses " << num_del_cls << ")" << std::endl;);
     }
 
     /**
@@ -2606,7 +2605,7 @@ namespace smt {
        depends on which group the clauses is in.
     */
     void context::del_inactive_lemmas2() {
-        IF_VERBOSE(2, verbose_stream() << "deleting inactive clauses... "; verbose_stream().flush(););
+        IF_VERBOSE(2, verbose_stream() << "(smt.delete-inactive-clauses "; verbose_stream().flush(););
         unsigned sz            = m_lemmas.size();
         unsigned start_at      = m_base_lvl == 0 ? 0 : m_base_scopes[m_base_lvl - 1].m_lemmas_lim;
         SASSERT(start_at <= sz);
@@ -2645,7 +2644,7 @@ namespace smt {
         }
         SASSERT(j <= sz);
         m_lemmas.shrink(j);
-        IF_VERBOSE(2, verbose_stream() << "num. deleted clauses: " << num_del_cls << " (out of " << sz << ")" << std::endl;);
+        IF_VERBOSE(2, verbose_stream() << " :num-deleted-clauses " << num_del_cls << ")" << std::endl;);
     }
 
     /**
@@ -2786,7 +2785,7 @@ namespace smt {
     }
 
     void context::assert_expr(expr * e, proof * pr) {
-        timeit tt(get_verbosity_level() >= 100, "simplifying");
+        timeit tt(get_verbosity_level() >= 100, "smt.simplifying");
         assert_expr_core(e, pr);
     }
 
@@ -2800,7 +2799,7 @@ namespace smt {
 
     void context::internalize_assertions() {
         TRACE("internalize_assertions", tout << "internalize_assertions()...\n";);
-        timeit tt(get_verbosity_level() >= 100, "preprocessing");
+        timeit tt(get_verbosity_level() >= 100, "smt.preprocessing");
         reduce_assertions();
         if (!m_asserted_formulas.inconsistent()) {
             unsigned sz    = m_asserted_formulas.get_num_formulas();
@@ -3158,7 +3157,7 @@ namespace smt {
             exit(1);
         }
 #endif
-        timeit tt(get_verbosity_level() >= 100, "searching");
+        timeit tt(get_verbosity_level() >= 100, "smt.stats");
         scoped_mk_model smk(*this);
         SASSERT(at_search_level());
         TRACE("search", display(tout); display_enodes_lbls(tout););
@@ -3166,7 +3165,7 @@ namespace smt {
         init_search();
         flet<bool> l(m_searching, true);
         TRACE("after_init_search", display(tout););
-        IF_VERBOSE(2, verbose_stream() << "searching...\n";);
+        IF_VERBOSE(2, verbose_stream() << "(smt.searching)\n";);
         TRACE("search_lite", tout << "searching...\n";);
         lbool    status            = l_undef;
         unsigned curr_lvl          = m_scope_lvl;
@@ -3215,16 +3214,16 @@ namespace smt {
             inc_limits();
             if (force_restart || !m_fparams.m_restart_adaptive || m_agility < m_fparams.m_restart_agility_threshold) {
                 SASSERT(!inconsistent());
-                IF_VERBOSE(1, verbose_stream() << "restarting... propagations: " << m_stats.m_num_propagations 
-                           << ", decisions: " << m_stats.m_num_decisions
-                           << ", conflicts: " << m_stats.m_num_conflicts << ", restart: " << m_restart_threshold;
+                IF_VERBOSE(1, verbose_stream() << "(smt.restarting :propagations " << m_stats.m_num_propagations 
+                           << " :decisions " << m_stats.m_num_decisions
+                           << " :conflicts " << m_stats.m_num_conflicts << " :restart " << m_restart_threshold;
                            if (m_fparams.m_restart_strategy == RS_IN_OUT_GEOMETRIC) {
-                               verbose_stream() << ", restart-outer: " << m_restart_outer_threshold;
+                               verbose_stream() << " :restart-outer " << m_restart_outer_threshold;
                            }
                            if (m_fparams.m_restart_adaptive) {
-                               verbose_stream() << ", agility: " << m_agility;
+                               verbose_stream() << " :agility " << m_agility;
                            }
-                           verbose_stream() << std::endl; verbose_stream().flush(););
+                           verbose_stream() << ")" << std::endl; verbose_stream().flush(););
                 // execute the restart
                 m_stats.m_num_restarts++;
                 if (m_scope_lvl > curr_lvl) {
@@ -3259,12 +3258,12 @@ namespace smt {
     void context::tick(unsigned & counter) const {
         counter++;
         if (counter > m_fparams.m_tick) {
-            IF_VERBOSE(3, verbose_stream() << "working...";
-                       verbose_stream() << " num. conflicts: " << m_num_conflicts;
+            IF_VERBOSE(3, verbose_stream() << "(smt.working";
+                       verbose_stream() << " :conflicts " << m_num_conflicts;
                        // verbose_stream() << " lemma avg. activity: " << get_lemma_avg_activity();
                        if (m_fparams.m_restart_adaptive)
-                       verbose_stream() << " agility: " << m_agility;
-                       verbose_stream() << std::endl; verbose_stream().flush(););
+                       verbose_stream() << " :agility " << m_agility;
+                       verbose_stream() << ")" << std::endl; verbose_stream().flush(););
             TRACE("assigned_literals_per_lvl", display_num_assigned_literals_per_lvl(tout); tout << "\n";);
             counter = 0;
         }
@@ -3410,7 +3409,7 @@ namespace smt {
             final_check_status ok;
             if (m_final_check_idx < num_th) {
                 theory * th = m_theory_set[m_final_check_idx];
-                IF_VERBOSE(100, verbose_stream() << "final check '" << th->get_name() << "' ...\n";);
+                IF_VERBOSE(100, verbose_stream() << "(smt.final-check \"" << th->get_name() << "\")\n";);
                 ok = th->final_check_eh();
                 TRACE("final_check_step", tout << "final check '" << th->get_name() << " ok: " << ok << " inconsistent " << inconsistent() << "\n";);
                 if (ok == FC_GIVEUP) {
diff --git a/src/smt/smt_quantifier.cpp b/src/smt/smt_quantifier.cpp
index c11f226ed..e6d81d3d2 100644
--- a/src/smt/smt_quantifier.cpp
+++ b/src/smt/smt_quantifier.cpp
@@ -211,7 +211,7 @@ namespace smt {
 
         final_check_status final_check_eh(bool full) {
             if (full) {
-                IF_VERBOSE(100, verbose_stream() << "final check 'quantifiers'...\n";);
+                IF_VERBOSE(100, verbose_stream() << "(smt.final-check \"quantifiers\")\n";);
                 final_check_status result  = m_qi_queue.final_check_eh() ? FC_DONE : FC_CONTINUE;
                 final_check_status presult = m_plugin->final_check_eh(full);
                 if (presult != FC_DONE)
diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp
index 67c94808e..ac080ccaa 100644
--- a/src/smt/smt_setup.cpp
+++ b/src/smt/smt_setup.cpp
@@ -118,7 +118,7 @@ namespace smt {
 
     void setup::setup_auto_config() {
         static_features    st(m_manager);
-        IF_VERBOSE(100, verbose_stream() << "configuring...\n";);
+        IF_VERBOSE(100, verbose_stream() << "(smt.configuring)\n";);
         TRACE("setup", tout << "setup, logic: " << m_logic << "\n";);
         // HACK: do not collect features for QF_BV and QF_AUFBV... since they do not use them...
         if (m_logic == "QF_BV") {
@@ -128,7 +128,7 @@ namespace smt {
             setup_QF_AUFBV();
         }
         else {
-            IF_VERBOSE(100, verbose_stream() << "collecting features...\n";);
+            IF_VERBOSE(100, verbose_stream() << "(smt.collecting-features)\n";);
             st.collect(m_context.get_num_asserted_formulas(), m_context.get_asserted_formulas());
             IF_VERBOSE(1000, st.display_primitive(verbose_stream()););
             if (m_logic == "QF_UF") 
diff --git a/src/util/env_params.cpp b/src/util/env_params.cpp
new file mode 100644
index 000000000..cf1d31b85
--- /dev/null
+++ b/src/util/env_params.cpp
@@ -0,0 +1,36 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    env_params.cpp
+
+Abstract:
+
+    Goodies for updating environment parameters.
+
+Author:
+
+    Leonardo (leonardo) 2012-12-01
+
+Notes:
+
+--*/
+#include"env_params.h"
+#include"params.h"
+#include"gparams.h"
+#include"util.h"
+#include"memory_manager.h"
+
+void env_params::updt_params() {
+    params_ref p = gparams::get();
+    set_verbosity_level(p.get_uint("verbose", 0));
+    enable_warning_messages(p.get_bool("warning", true));
+    memory::set_max_size(p.get_uint("memory_max_size", 0));
+}
+
+void env_params::collect_param_descrs(param_descrs & d) {
+    d.insert("verbose", CPK_UINT, "be verbose, where the value is the verbosity level", "0");
+    d.insert("warning", CPK_BOOL, "enable/disable warning messages", "true");
+    d.insert("memory_max_size", CPK_UINT, "set hard upper limit for memory consumption (in megabytes), if 0 then there is no bound.", "0");
+}
diff --git a/src/util/env_params.h b/src/util/env_params.h
new file mode 100644
index 000000000..8b5fa7005
--- /dev/null
+++ b/src/util/env_params.h
@@ -0,0 +1,32 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    env_params.h
+
+Abstract:
+
+    Goodies for updating environment parameters.
+
+Author:
+
+    Leonardo (leonardo) 2012-12-01
+
+Notes:
+
+--*/
+#ifndef _ENV_PARAMS_H_
+#define _ENV_PARAMS_H_
+
+class param_descrs;
+
+struct env_params {
+    static void updt_params();
+    static void collect_param_descrs(param_descrs & p);
+    /*
+      REG_PARAMS('env_params::collect_param_descrs')
+    */
+};
+
+#endif
diff --git a/src/util/gparams.cpp b/src/util/gparams.cpp
index e7b2a52eb..29377eb8d 100644
--- a/src/util/gparams.cpp
+++ b/src/util/gparams.cpp
@@ -18,6 +18,7 @@ Notes:
 --*/
 #include"gparams.h"
 #include"dictionary.h"
+#include"trace.h"
 
 extern void gparams_register_modules();
 
@@ -291,6 +292,7 @@ public:
     
     params_ref get() { 
         params_ref result;
+        TRACE("gparams", tout << "get() m_params: " << m_params << "\n";);
         #pragma omp critical (gparams)
         {
             result = m_params;
@@ -303,6 +305,7 @@ public:
 gparams::imp * gparams::g_imp = 0;
 
 void gparams::set(char const * name, char const * value) {
+    TRACE("gparams", tout << "setting [" << name << "] <- '" << value << "'\n";);
     SASSERT(g_imp != 0);
     g_imp->set(name, value);
 }
@@ -342,6 +345,7 @@ params_ref gparams::get_module(symbol const & module_name) {
 }
 
 params_ref gparams::get() {
+    TRACE("gparams", tout << "gparams::get()\n";);
     SASSERT(g_imp != 0);
     return g_imp->get();
 }
@@ -352,11 +356,13 @@ void gparams::display(std::ostream & out, unsigned indent, bool smt2_style) {
 }
 
 void gparams::init() {
+    TRACE("gparams", tout << "gparams::init()\n";);
     g_imp = alloc(imp);
     gparams_register_modules();
 }
 
 void gparams::finalize() {
+    TRACE("gparams", tout << "gparams::finalize()\n";);
     if (g_imp != 0) {
         dealloc(g_imp);
         g_imp = 0;
diff --git a/src/util/timeit.cpp b/src/util/timeit.cpp
index 975dd3127..5246beced 100644
--- a/src/util/timeit.cpp
+++ b/src/util/timeit.cpp
@@ -38,9 +38,9 @@ struct timeit::imp {
     ~imp() {
         m_watch.stop();
         double end_memory = static_cast<double>(memory::get_allocation_size())/static_cast<double>(1024*1024);
-        m_out << m_msg << ", time: " << std::fixed << std::setprecision(2) << m_watch.get_seconds() 
-              << " secs, memory: (before " << std::fixed << std::setprecision(2) << m_start_memory 
-              << ", after " << std::fixed << std::setprecision(2) << end_memory << ")" 
+        m_out << "(" << m_msg << " :time " << std::fixed << std::setprecision(2) << m_watch.get_seconds() 
+              << " :before-memory " << std::fixed << std::setprecision(2) << m_start_memory 
+              << " :after-memory " << std::fixed << std::setprecision(2) << end_memory << ")" 
               << std::endl;
     }
 };
diff --git a/src/util/util.cpp b/src/util/util.cpp
index 3e5ced813..eb9acb385 100644
--- a/src/util/util.cpp
+++ b/src/util/util.cpp
@@ -29,11 +29,6 @@ unsigned get_verbosity_level() {
     return g_verbosity_level;
 }
 
-void register_verbosity_level() {
-    // PARAM-TODO
-    // p.register_unsigned_param("VERBOSE", g_verbosity_level, "be verbose, where the value is the verbosity level", true);
-}
-
 static std::ostream* g_verbose_stream = &std::cerr;
 
 void set_verbose_stream(std::ostream& str) {
diff --git a/src/util/util.h b/src/util/util.h
index 5e51d8ef1..945d259f9 100644
--- a/src/util/util.h
+++ b/src/util/util.h
@@ -157,8 +157,6 @@ struct delete_proc {
 
 void set_verbosity_level(unsigned lvl);
 unsigned get_verbosity_level();
-class ini_params;
-void register_verbosity_level(ini_params & p);
 std::ostream& verbose_stream();
 void set_verbose_stream(std::ostream& str);
 
diff --git a/src/util/warning.h b/src/util/warning.h
index 6800c1f95..a556bfb60 100644
--- a/src/util/warning.h
+++ b/src/util/warning.h
@@ -21,8 +21,6 @@ Revision History:
 #include<iostream>
 #include<stdarg.h>
 
-class ini_params;
-
 void send_warnings_to_stdout(bool flag);
 
 void enable_warning_messages(bool flag);
@@ -33,8 +31,6 @@ void set_warning_stream(std::ostream* strm);
 
 void warning_msg(const char * msg, ...);
 
-void register_warning(ini_params & p);
-
 void disable_error_msg_prefix();
 
 void format2ostream(std::ostream& out, char const* fmt, va_list args);