diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp
index 1503b387f..45892bac3 100644
--- a/src/api/api_ast.cpp
+++ b/src/api/api_ast.cpp
@@ -36,6 +36,7 @@ Revision History:
 #include"scoped_ctrl_c.h"
 #include"cancel_eh.h"
 #include"scoped_timer.h"
+#include"pp_params.hpp"
 
 extern "C" {
 
@@ -833,7 +834,8 @@ extern "C" {
             break;
         case Z3_PRINT_SMTLIB_COMPLIANT: {
             ast_smt_pp pp(mk_c(c)->m());
-            pp.set_simplify_implies(get_pp_default_params().m_pp_simplify_implies);
+            pp_params params;
+            pp.set_simplify_implies(params.simplify_implies());
             ast* a1 = to_ast(a);
             pp.set_logic(mk_c(c)->fparams().m_smtlib_logic.c_str());
             if (!is_expr(a1)) {
@@ -886,7 +888,8 @@ extern "C" {
         pp.set_logic(logic);
         pp.set_status(status);
         pp.add_attributes(attributes);
-        pp.set_simplify_implies(get_pp_default_params().m_pp_simplify_implies);
+        pp_params params;
+        pp.set_simplify_implies(params.simplify_implies());
         for (unsigned i = 0; i < num_assumptions; ++i) {
             pp.add_assumption(to_expr(assumptions[i]));
         }
diff --git a/src/ast/ast_pp.h b/src/ast/ast_pp.h
index d99fb7670..7e7bdfc4e 100644
--- a/src/ast/ast_pp.h
+++ b/src/ast/ast_pp.h
@@ -24,7 +24,7 @@ Revision History:
 #include"ast_smt2_pp.h"
 
 struct mk_pp : public mk_ismt2_pp {
-    mk_pp(ast * t, ast_manager & m, pp_params const & p, unsigned indent = 0, unsigned num_vars = 0, char const * var_prefix = 0):
+    mk_pp(ast * t, ast_manager & m, params_ref const & p, unsigned indent = 0, unsigned num_vars = 0, char const * var_prefix = 0):
         mk_ismt2_pp(t, m, p, indent, num_vars, var_prefix) {
     }
     mk_pp(ast * t, ast_manager & m, unsigned indent = 0, unsigned num_vars = 0, char const * var_prefix = 0):
diff --git a/src/ast/ast_printer.cpp b/src/ast/ast_printer.cpp
index 33ddcb709..8d6ed91f7 100644
--- a/src/ast/ast_printer.cpp
+++ b/src/ast/ast_printer.cpp
@@ -33,14 +33,14 @@ public:
     virtual void display(std::ostream & out, func_decl * f, unsigned indent = 0) const {
         out << f->get_name();
     }
-    virtual void pp(sort * s, format_ns::format_ref & r) const { mk_smt2_format(s, env(), get_pp_default_params(), r); }
-    virtual void pp(func_decl * f, format_ns::format_ref & r) const { mk_smt2_format(f, env(), get_pp_default_params(), r); }
+    virtual void pp(sort * s, format_ns::format_ref & r) const { mk_smt2_format(s, env(), params_ref(), r); }
+    virtual void pp(func_decl * f, format_ns::format_ref & r) const { mk_smt2_format(f, env(), params_ref(), r); }
     virtual void pp(expr * n, format_ns::format_ref & r) const { 
         sbuffer<symbol> buf;
-        mk_smt2_format(n, env(), get_pp_default_params(), 0, 0, r, buf); 
+        mk_smt2_format(n, env(), params_ref(), 0, 0, r, buf); 
     }
     virtual void pp(expr * n, unsigned num_vars, char const * var_prefix, format_ns::format_ref & r, sbuffer<symbol> & var_names) const {
-        mk_smt2_format(n, env(), get_pp_default_params(), num_vars, var_prefix, r, var_names);
+        mk_smt2_format(n, env(), params_ref(), num_vars, var_prefix, r, var_names);
     }
     virtual void display(std::ostream & out, expr * n, unsigned indent, unsigned num_vars, char const * var_prefix, sbuffer<symbol> & var_names) const {
         NOT_IMPLEMENTED_YET();
diff --git a/src/ast/ast_smt2_pp.cpp b/src/ast/ast_smt2_pp.cpp
index dcc7a1a0d..afe301ddf 100644
--- a/src/ast/ast_smt2_pp.cpp
+++ b/src/ast/ast_smt2_pp.cpp
@@ -24,6 +24,7 @@ Revision History:
 #include"ast_ll_pp.h"
 #include"ast_pp.h"
 #include"algebraic_numbers.h"
+#include"pp_params.hpp"
 using namespace format_ns;
 
 #define ALIAS_PREFIX "a"
@@ -376,7 +377,6 @@ typedef app_ref_vector format_ref_vector;
 
 class smt2_printer {
     ast_manager &                         m_manager;
-    pp_params const &                     m_params;
     smt2_pp_environment &                 m_env;
 
     shared_occs                           m_soccs;
@@ -421,6 +421,16 @@ class smt2_printer {
 
     string_buffer<> m_next_name_buffer;
 
+    // Config
+    bool     m_pp_decimal;
+    unsigned m_pp_decimal_precision;
+    bool     m_pp_bv_lits;
+    bool     m_pp_bv_neg;
+    unsigned m_pp_max_depth;
+    unsigned m_pp_min_alias_size;
+    bool     m_pp_flat_assoc;
+
+
     symbol next_name(char const * prefix, unsigned & idx) {
         while (true) {
             m_next_name_buffer.reset();
@@ -508,10 +518,10 @@ class smt2_printer {
     void pp_const(app * c) {
         format * f;
         if (m_env.get_autil().is_numeral(c) || m_env.get_autil().is_irrational_algebraic_numeral(c)) {
-            f = m_env.pp_arith_literal(c, m_params.m_pp_decimal, m_params.m_pp_decimal_precision);
+            f = m_env.pp_arith_literal(c, m_pp_decimal, m_pp_decimal_precision);
         }
         else if (m_env.get_bvutil().is_numeral(c)) {
-            f = m_env.pp_bv_literal(c, m_params.m_pp_bv_lits, m_params.m_pp_bv_neg);
+            f = m_env.pp_bv_literal(c, m_pp_bv_lits, m_pp_bv_neg);
         }
         else if (m_env.get_futil().is_value(c)) {
             f = m_env.pp_float_literal(c);
@@ -584,8 +594,8 @@ class smt2_printer {
         m_format_stack.shrink(fr.m_spos);
         m_info_stack.shrink(fr.m_spos);
         if (fr.m_use_alias && m_root != t &&
-            ((f_info.m_depth >= m_params.m_pp_max_depth) || 
-             ((f_info.m_weight >= m_params.m_pp_min_alias_size || is_quantifier(t)) && m_soccs.is_shared(t)))) {
+            ((f_info.m_depth >= m_pp_max_depth) || 
+             ((f_info.m_weight >= m_pp_min_alias_size || is_quantifier(t)) && m_soccs.is_shared(t)))) {
             symbol a = next_alias();
             TRACE("smt2_pp", tout << "a: " << a << " depth: " << f_info.m_depth << ", weight: " << f_info.m_weight 
                   << ", lvl: " << f_info.m_lvl << " t: #" << t->get_id() << "\n" << mk_ll_pp(t, m()) 
@@ -602,7 +612,7 @@ class smt2_printer {
     }
 
     bool flat_assoc(app * t, frame const & fr) {
-        if (!m_params.m_pp_flat_assoc)
+        if (!m_pp_flat_assoc)
             return false;
         func_decl * f = t->get_decl();
         if (f->is_associative() && m_frame_stack.size() >= 2 && !m_soccs.is_shared(t)) {
@@ -943,9 +953,8 @@ class smt2_printer {
     }
 
 public:
-    smt2_printer(smt2_pp_environment & env, pp_params const & params):
+    smt2_printer(smt2_pp_environment & env, params_ref const & params):
         m_manager(env.get_manager()),
-        m_params(params),
         m_env(env),
         m_soccs(m_manager),
         m_root(0),
@@ -953,6 +962,15 @@ public:
         m_next_alias_idx(1),
         m_format_stack(fm()) {
         init_expr2alias_stack();
+
+        pp_params p(params);
+        m_pp_decimal = p.decimal();
+        m_pp_decimal_precision = p.decimal_precision();
+        m_pp_bv_lits = p.bv_literals();
+        m_pp_bv_neg  = p.bv_neg();
+        m_pp_max_depth = p.max_depth();
+        m_pp_min_alias_size = p.min_alias_size();
+        m_pp_flat_assoc = p.flat_assoc();
     }
 
     ~smt2_printer() {
@@ -1003,24 +1021,24 @@ public:
 
 };
 
-void mk_smt2_format(expr * n, smt2_pp_environment & env, pp_params const & p, 
+void mk_smt2_format(expr * n, smt2_pp_environment & env, params_ref const & p, 
                     unsigned num_vars, char const * var_prefix,
                     format_ref & r, sbuffer<symbol> & var_names) {
     smt2_printer pr(env, p);
     pr(n, num_vars, var_prefix, r, var_names);
 }
 
-void mk_smt2_format(sort * s, smt2_pp_environment & env, pp_params const & p, format_ref & r) {
+void mk_smt2_format(sort * s, smt2_pp_environment & env, params_ref const & p, format_ref & r) {
     smt2_printer pr(env, p);
     pr(s, r);
 }
 
-void mk_smt2_format(func_decl * f, smt2_pp_environment & env, pp_params const & p, format_ref & r) {
+void mk_smt2_format(func_decl * f, smt2_pp_environment & env, params_ref const & p, format_ref & r) {
     smt2_printer pr(env, p);
     pr(f, r);
 }
 
-std::ostream & ast_smt2_pp(std::ostream & out, expr * n, smt2_pp_environment & env, pp_params const & p, unsigned indent, 
+std::ostream & ast_smt2_pp(std::ostream & out, expr * n, smt2_pp_environment & env, params_ref const & p, unsigned indent, 
                             unsigned num_vars, char const * var_prefix) {
     ast_manager & m = env.get_manager();
     format_ref r(fm(m));
@@ -1032,7 +1050,7 @@ std::ostream & ast_smt2_pp(std::ostream & out, expr * n, smt2_pp_environment & e
     return out;
 }
 
-std::ostream & ast_smt2_pp(std::ostream & out, sort * s, smt2_pp_environment & env, pp_params const & p, unsigned indent) {
+std::ostream & ast_smt2_pp(std::ostream & out, sort * s, smt2_pp_environment & env, params_ref const & p, unsigned indent) {
     ast_manager & m = env.get_manager();
     format_ref r(fm(m));
     sbuffer<symbol> var_names;
@@ -1043,7 +1061,7 @@ std::ostream & ast_smt2_pp(std::ostream & out, sort * s, smt2_pp_environment & e
     return out;
 }
 
-std::ostream & ast_smt2_pp(std::ostream & out, func_decl * f, smt2_pp_environment & env, pp_params const & p, unsigned indent) {
+std::ostream & ast_smt2_pp(std::ostream & out, func_decl * f, smt2_pp_environment & env, params_ref const & p, unsigned indent) {
     ast_manager & m = env.get_manager();
     format_ref r(fm(m));
     sbuffer<symbol> var_names;
@@ -1054,7 +1072,7 @@ std::ostream & ast_smt2_pp(std::ostream & out, func_decl * f, smt2_pp_environmen
     return out;
 }
 
-mk_ismt2_pp::mk_ismt2_pp(ast * t, ast_manager & m, pp_params const & p, unsigned indent, unsigned num_vars, char const * var_prefix):
+mk_ismt2_pp::mk_ismt2_pp(ast * t, ast_manager & m, params_ref const & p, unsigned indent, unsigned num_vars, char const * var_prefix):
     m_ast(t),
     m_manager(m),
     m_params(p),
@@ -1066,7 +1084,7 @@ mk_ismt2_pp::mk_ismt2_pp(ast * t, ast_manager & m, pp_params const & p, unsigned
 mk_ismt2_pp::mk_ismt2_pp(ast * t, ast_manager & m, unsigned indent, unsigned num_vars, char const * var_prefix):
     m_ast(t),
     m_manager(m),
-    m_params(get_pp_default_params()),
+    m_params(m_empty),
     m_indent(indent),
     m_num_vars(num_vars),
     m_var_prefix(var_prefix) {
diff --git a/src/ast/ast_smt2_pp.h b/src/ast/ast_smt2_pp.h
index 048dd8d67..aa84d6e03 100644
--- a/src/ast/ast_smt2_pp.h
+++ b/src/ast/ast_smt2_pp.h
@@ -23,7 +23,7 @@ Revision History:
 #define _AST_SMT2_PP_H_
 
 #include"format.h"
-#include"pp_params.h"
+#include"params.h"
 #include"arith_decl_plugin.h"
 #include"bv_decl_plugin.h"
 #include"array_decl_plugin.h"
@@ -82,28 +82,29 @@ public:
     virtual bool uses(symbol const & s) const { return false; }
 };
 
-void mk_smt2_format(expr * n, smt2_pp_environment & env, pp_params const & p, 
+void mk_smt2_format(expr * n, smt2_pp_environment & env, params_ref const & p, 
                     unsigned num_vars, char const * var_prefix,
                     format_ns::format_ref & r, sbuffer<symbol> & var_names);
-void mk_smt2_format(sort * s, smt2_pp_environment & env, pp_params const & p, format_ns::format_ref & r);
-void mk_smt2_format(func_decl * f, smt2_pp_environment & env, pp_params const & p, format_ns::format_ref & r);
+void mk_smt2_format(sort * s, smt2_pp_environment & env, params_ref const & p, format_ns::format_ref & r);
+void mk_smt2_format(func_decl * f, smt2_pp_environment & env, params_ref const & p, format_ns::format_ref & r);
 
-std::ostream & ast_smt2_pp(std::ostream & out, expr * n, smt2_pp_environment & env, pp_params const & p, unsigned indent = 0, 
+std::ostream & ast_smt2_pp(std::ostream & out, expr * n, smt2_pp_environment & env, params_ref const & p = params_ref(), unsigned indent = 0, 
                            unsigned num_vars = 0, char const * var_prefix = 0);
-std::ostream & ast_smt2_pp(std::ostream & out, sort * s, smt2_pp_environment & env, pp_params const & p, unsigned indent = 0);
-std::ostream & ast_smt2_pp(std::ostream & out, func_decl * f, smt2_pp_environment & env, pp_params const & p, unsigned indent = 0);
+std::ostream & ast_smt2_pp(std::ostream & out, sort * s, smt2_pp_environment & env, params_ref const & p = params_ref(), unsigned indent = 0);
+std::ostream & ast_smt2_pp(std::ostream & out, func_decl * f, smt2_pp_environment & env, params_ref const & p = params_ref(), unsigned indent = 0);
 
 /**
    \brief Internal wrapper (for debugging purposes only)
 */
 struct mk_ismt2_pp {
-    ast *             m_ast;
-    ast_manager &     m_manager;
-    pp_params const & m_params;
-    unsigned          m_indent;
-    unsigned          m_num_vars;
-    char const *      m_var_prefix;
-    mk_ismt2_pp(ast * t, ast_manager & m, pp_params const & p, unsigned indent = 0, unsigned num_vars = 0, char const * var_prefix = 0);
+    ast *              m_ast;
+    ast_manager &      m_manager;
+    params_ref         m_empty;
+    params_ref const & m_params;
+    unsigned           m_indent;
+    unsigned           m_num_vars;
+    char const *       m_var_prefix;
+    mk_ismt2_pp(ast * t, ast_manager & m, params_ref const & p, unsigned indent = 0, unsigned num_vars = 0, char const * var_prefix = 0);
     mk_ismt2_pp(ast * t, ast_manager & m, unsigned indent = 0, unsigned num_vars = 0, char const * var_prefix = 0);
 };
 
diff --git a/src/ast/pp.cpp b/src/ast/pp.cpp
index d05776e78..13247127d 100644
--- a/src/ast/pp.cpp
+++ b/src/ast/pp.cpp
@@ -17,40 +17,9 @@ Revision History:
 
 --*/
 #include"pp.h"
+#include"pp_params.hpp"
 using namespace format_ns;
 
-void pp_param_descrs(param_descrs & p) {
-    p.insert("max_indent", CPK_UINT, "max. indentation in pretty printer");
-    p.insert("max_num_lines", CPK_UINT, "max. number of lines to be displayed in pretty printer");
-    p.insert("max_width", CPK_UINT, "max. width in pretty printer");
-    p.insert("max_ribbon", CPK_UINT, "max. ribbon (width - indentation) in pretty printer");
-    p.insert("max_depth", CPK_UINT, "max. term depth (when pretty printing SMT2 terms/formulas)");
-    p.insert("min_alias_size", CPK_UINT, "min. size for creating an alias for a shared term (when pretty printing SMT2 terms/formulas)");
-    p.insert("decimal", CPK_BOOL, "pretty print real numbers using decimal notation (the output may be truncated). Z3 adds a '?' if the value is not precise");
-    p.insert("decimal_precision", CPK_BOOL, "maximum number of decimal places to be used when pp.decimal=true");
-    p.insert("bv_literals", CPK_BOOL, "use Bit-Vector literals (e.g, #x0F and #b0101) during pretty printing");
-    p.insert("bv_neg", CPK_BOOL, "use bvneg when displaying Bit-Vector literals where the most significant bit is 1");
-    p.insert("flat_assoc", CPK_BOOL, "flat associative operators (when pretty printing SMT2 terms/formulas)");
-    p.insert("fixed_indent", CPK_BOOL, "use a fixed indentation for applications");
-    p.insert("single_line", CPK_BOOL, "ignore line breaks when true");
-    p.insert("bounded", CPK_BOOL, "ignore characters exceeding max widht");
-    p.insert("simplify_implies", CPK_BOOL, "simplify nested implications for pretty printing");
-}
-
-pp_params g_pp_params;
-
-void set_pp_default_params(pp_params const & p) {
-    g_pp_params = p;
-}
-
-void register_pp_params(ini_params & p) {
-    g_pp_params.register_params(p);
-}
-
-pp_params const & get_pp_default_params() {
-    return g_pp_params;
-}
-
 static std::pair<unsigned, bool> space_upto_line_break(ast_manager & m, format * f) {
     unsigned r;
     SASSERT(f->get_family_id() == fm(m).get_family_id("format"));
@@ -87,7 +56,15 @@ inline bool fits(ast_manager & m, format * f, unsigned space_left) {
     return s <= space_left;
 }
 
-void pp(std::ostream & out, format * f, ast_manager & m, pp_params const & p) {
+void pp(std::ostream & out, format * f, ast_manager & m, params_ref const & _p) {
+    pp_params p(_p);
+    unsigned max_width     = p.max_width();
+    unsigned max_ribbon    = p.max_ribbon(); 
+    unsigned max_num_lines = p.max_num_lines();
+    unsigned max_indent    = p.max_indent();
+    bool     bounded       = p.bounded();
+    bool     single_line   = p.single_line();
+
     unsigned pos = 0;
     unsigned ribbon_pos = 0;
     unsigned line = 0;
@@ -98,7 +75,7 @@ void pp(std::ostream & out, format * f, ast_manager & m, pp_params const & p) {
     todo.push_back(std::make_pair(f, 0));
     app_ref  space(mk_string(m, " "), fm(m));
     while (!todo.empty()) {
-        if (line >= p.m_pp_max_num_lines)
+        if (line >= max_num_lines)
             return;
         std::pair<format *, unsigned> pair = todo.back();
         format * f = pair.first;
@@ -107,10 +84,10 @@ void pp(std::ostream & out, format * f, ast_manager & m, pp_params const & p) {
         SASSERT(f->get_family_id() == fm(m).get_family_id("format"));
         switch (f->get_decl_kind()) {
         case OP_STRING:
-            if (p.m_pp_bounded && pos > p.m_pp_max_width)
+            if (bounded && pos > max_width)
                 break;
             len = static_cast<unsigned>(strlen(f->get_decl()->get_parameter(0).get_symbol().bare_str()));
-            if (p.m_pp_bounded && pos + len > p.m_pp_max_width) {
+            if (bounded && pos + len > max_width) {
                 out << "...";
                 break;
             }
@@ -121,7 +98,7 @@ void pp(std::ostream & out, format * f, ast_manager & m, pp_params const & p) {
         case OP_INDENT:
             todo.push_back(std::make_pair(to_app(f->get_arg(0)), 
                                           std::min(indent + f->get_decl()->get_parameter(0).get_int(),
-                                                   p.m_pp_max_indent)));
+                                                   max_indent)));
             break;
         case OP_COMPOSE:
             i = f->get_num_args();
@@ -131,7 +108,7 @@ void pp(std::ostream & out, format * f, ast_manager & m, pp_params const & p) {
             }
             break;
         case OP_CHOICE:
-            space_left = std::min(p.m_pp_max_width - pos, p.m_pp_max_ribbon - pos);
+            space_left = std::min(max_width - pos, max_ribbon - pos);
             if (space_left > 0 && fits(m, to_app(f->get_arg(0)), space_left)) 
                 todo.push_back(std::make_pair(to_app(f->get_arg(0)), indent));
             else
@@ -139,14 +116,14 @@ void pp(std::ostream & out, format * f, ast_manager & m, pp_params const & p) {
             break;
         case OP_LINE_BREAK:
         case OP_LINE_BREAK_EXT:
-            if (p.m_pp_single_line) {
+            if (single_line) {
                 todo.push_back(std::make_pair(space, indent));
                 break;
             }
             pos = indent;
             ribbon_pos = 0;
             line++;
-            if (line < p.m_pp_max_num_lines) {
+            if (line < max_num_lines) {
                 out << "\n";
                 for (unsigned i = 0; i < indent; i++) 
                     out << " ";
@@ -160,7 +137,3 @@ void pp(std::ostream & out, format * f, ast_manager & m, pp_params const & p) {
     }
 }
 
-void pp(std::ostream & out, format_ns::format * f, ast_manager & m) {
-    pp(out, f, m, g_pp_params);
-}
-
diff --git a/src/ast/pp.h b/src/ast/pp.h
index 13afcb07c..f567afa4a 100644
--- a/src/ast/pp.h
+++ b/src/ast/pp.h
@@ -20,21 +20,9 @@ Revision History:
 #define _PP_H_
 
 #include"format.h"
-#include"pp_params.h"
 #include"params.h"
 
-/*
-  REG_MODULE_PARAMS('pp', 'pp_param_descrs')
-*/
-void pp_param_descrs(param_descrs & d);
-
-void set_pp_default_params(pp_params const & p);
-void register_pp_params(ini_params & p);
-
-pp_params const & get_pp_default_params();
-
-void pp(std::ostream & out, format_ns::format * f, ast_manager & m, pp_params const & p);
-void pp(std::ostream & out, format_ns::format * f, ast_manager & m);
+void pp(std::ostream & out, format_ns::format * f, ast_manager & m, params_ref const & p = params_ref());
 
 #endif /* _PP_H_ */
 
diff --git a/src/ast/pp_params.cpp b/src/ast/pp_params.cpp
deleted file mode 100644
index 0cf3e455d..000000000
--- a/src/ast/pp_params.cpp
+++ /dev/null
@@ -1,57 +0,0 @@
-/*++
-Copyright (c) 2006 Microsoft Corporation
-
-Module Name:
-
-    pp_params.cpp
-
-Abstract:
-
-    <abstract>
-
-Author:
-
-    Leonardo de Moura (leonardo) 2008-01-20.
-
-Revision History:
-
---*/
-
-#include"pp_params.h"
-
-pp_params::pp_params():
-    m_pp_max_indent(UINT_MAX),
-    m_pp_max_num_lines(UINT_MAX),
-    m_pp_max_width(80),
-    m_pp_max_ribbon(80),
-    m_pp_max_depth(5),
-    m_pp_min_alias_size(10),
-    m_pp_decimal(false),
-    m_pp_decimal_precision(10),
-    m_pp_bv_lits(true),
-    m_pp_bv_neg(false),
-    m_pp_flat_assoc(true),
-    m_pp_fixed_indent(false),
-    m_pp_single_line(false),
-    m_pp_bounded(false),
-    m_pp_simplify_implies(false) {
-}
-
-void pp_params::register_params(ini_params & p) {
-    p.register_unsigned_param("PP_MAX_INDENT", m_pp_max_indent, "max. indentation in pretty printer", true);
-    p.register_unsigned_param("PP_MAX_NUM_LINES", m_pp_max_num_lines, "max. number of lines to be displayed in pretty printer", true);
-    p.register_unsigned_param("PP_MAX_WIDTH", m_pp_max_width, "max. width in pretty printer", true);
-    p.register_unsigned_param("PP_MAX_RIBBON", m_pp_max_ribbon, "max. ribbon (width - indentation) in pretty printer", true);
-    p.register_unsigned_param("PP_MAX_DEPTH", m_pp_max_depth, "max. term depth (when pretty printing SMT2 terms/formulas)", true);
-    p.register_unsigned_param("PP_MIN_ALIAS_SIZE", m_pp_min_alias_size, "min. size for creating an alias for a shared term (when pretty printing SMT2 terms/formulas)", true);
-    p.register_bool_param("PP_DECIMAL", m_pp_decimal, "pretty print real numbers using decimal notation (the output may be truncated). Z3 adds a '?' if the value is not precise", true);
-    p.register_unsigned_param("PP_DECIMAL_PRECISION", m_pp_decimal_precision, "maximum number of decimal places to be used when PP_DECIMAL=true", true);
-    p.register_bool_param("PP_BV_LITERALS", m_pp_bv_lits, "use Bit-Vector literals (e.g, #x0F and #b0101) during pretty printing", true);
-    p.register_bool_param("PP_BV_NEG", m_pp_bv_neg, "use bvneg when displaying Bit-Vector literals where the most significant bit is 1", true);
-    p.register_bool_param("PP_FLAT_ASSOC", m_pp_flat_assoc, "flat associative operators (when pretty printing SMT2 terms/formulas)", true);
-    p.register_bool_param("PP_FIXED_INDENT", m_pp_fixed_indent, "use a fixed indentation for applications", true);
-    p.register_bool_param("PP_SINGLE_LINE", m_pp_single_line, "ignore line breaks when true", true);
-    p.register_bool_param("PP_BOUNDED", m_pp_bounded, "ignore characters exceeding max widht", true);
-    p.register_bool_param("PP_SIMPLIFY_IMPLIES", m_pp_simplify_implies, "simplify nested implications for pretty printing", true);
-}
-
diff --git a/src/ast/pp_params.h b/src/ast/pp_params.h
deleted file mode 100644
index 970f97968..000000000
--- a/src/ast/pp_params.h
+++ /dev/null
@@ -1,46 +0,0 @@
-/*++
-Copyright (c) 2006 Microsoft Corporation
-
-Module Name:
-
-    pp_params.h
-
-Abstract:
-
-    <abstract>
-
-Author:
-
-    Leonardo de Moura (leonardo) 2008-01-20.
-
-Revision History:
-
---*/
-#ifndef _PP_PARAMS_H_
-#define _PP_PARAMS_H_
-
-#include"ini_file.h"
-
-struct pp_params {
-    unsigned  m_pp_max_indent; // max. indentation
-    unsigned  m_pp_max_num_lines; // max. num. lines
-    unsigned  m_pp_max_width;  // max. width
-    unsigned  m_pp_max_ribbon; // max. ribbon: width - indentation
-    unsigned  m_pp_max_depth;
-    unsigned  m_pp_min_alias_size; 
-    bool      m_pp_decimal; // display reals using decimals
-    unsigned  m_pp_decimal_precision; // max. number of decimal places
-    bool      m_pp_bv_lits;
-    bool      m_pp_bv_neg; // use bvneg to display bit-vector literals which the most significant bit is 1
-    bool      m_pp_flat_assoc;
-    bool      m_pp_fixed_indent; 
-    bool      m_pp_single_line; // ignore line breaks if true
-    bool      m_pp_bounded; // ignore characters exceeding max width.
-    bool      m_pp_simplify_implies; // simplify nested implications during pretty printing
-
-    pp_params();
-    void register_params(ini_params & p);
-};
-
-#endif /* _PP_PARAMS_H_ */
-
diff --git a/src/ast/pp_params.pyg b/src/ast/pp_params.pyg
new file mode 100644
index 000000000..57d6e185d
--- /dev/null
+++ b/src/ast/pp_params.pyg
@@ -0,0 +1,17 @@
+def_module_params('pp', 
+                  export=True,
+                  params=(('max_indent', UINT, UINT_MAX, 'max. indentation in pretty printer'),
+                          ('max_num_lines', UINT, UINT_MAX, 'max. number of lines to be displayed in pretty printer'),
+                          ('max_width', UINT, 80, 'max. width in pretty printer'),
+                          ('max_ribbon', UINT, 80, 'max. ribbon (width - indentation) in pretty printer'),
+                          ('max_depth', UINT, 5, 'max. term depth (when pretty printing SMT2 terms/formulas)'),
+                          ('min_alias_size', UINT, 10, 'min. size for creating an alias for a shared term (when pretty printing SMT2 terms/formulas)'),
+                          ('decimal', BOOL, False, 'pretty print real numbers using decimal notation (the output may be truncated). Z3 adds a ? if the value is not precise'),
+                          ('decimal_precision', UINT, 10, 'maximum number of decimal places to be used when pp.decimal=true'),
+                          ('bv_literals', BOOL, True, 'use Bit-Vector literals (e.g, #x0F and #b0101) during pretty printing'),
+                          ('bv_neg', BOOL, False, 'use bvneg when displaying Bit-Vector literals where the most significant bit is 1'),
+                          ('flat_assoc', BOOL, True, 'flat associative operators (when pretty printing SMT2 terms/formulas)'),
+                          ('fixed_indent', BOOL, False, 'use a fixed indentation for applications'),
+                          ('single_line', BOOL, False, 'ignore line breaks when true'),
+                          ('bounded', BOOL, False, 'ignore characters exceeding max widht'),
+                          ('simplify_implies', BOOL, True, 'simplify nested implications for pretty printing')))
diff --git a/src/ast/substitution/substitution_tree.cpp b/src/ast/substitution/substitution_tree.cpp
index 81b2f7be6..037d51e32 100644
--- a/src/ast/substitution/substitution_tree.cpp
+++ b/src/ast/substitution/substitution_tree.cpp
@@ -607,8 +607,8 @@ void substitution_tree::display(std::ostream & out, node * n, unsigned delta) co
         out << "  ";
     display(out, n->m_subst);
     if (n->m_leaf) {
-        pp_params p;
-        p.m_pp_single_line = true;
+        params_ref p;
+        p.set_bool("single_line", true);
         out << "  ==> ";
         out << mk_pp(n->m_expr, m_manager, p);
         out << "\n";
diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index d14ce3076..5dcc4268c 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -1536,8 +1536,7 @@ cmd_context::pp_env & cmd_context::get_pp_env() const {
 }
 
 void cmd_context::pp(expr * n, unsigned num_vars, char const * var_prefix, format_ns::format_ref & r, sbuffer<symbol> & var_names) const {
-    mk_smt2_format(n, get_pp_env(), get_pp_default_params(),
-                   num_vars, var_prefix, r, var_names);
+    mk_smt2_format(n, get_pp_env(), params_ref(), num_vars, var_prefix, r, var_names);
 }
 
 void cmd_context::pp(expr * n, format_ns::format_ref & r) const {
@@ -1546,7 +1545,7 @@ void cmd_context::pp(expr * n, format_ns::format_ref & r) const {
 }
 
 void cmd_context::pp(func_decl * f, format_ns::format_ref & r) const {
-    mk_smt2_format(f, get_pp_env(), get_pp_default_params(), r);
+    mk_smt2_format(f, get_pp_env(), params_ref(), r);
 }
 
 void cmd_context::display(std::ostream & out, sort * s, unsigned indent) const {
@@ -1554,7 +1553,7 @@ void cmd_context::display(std::ostream & out, sort * s, unsigned indent) const {
     f = pp(s);
     if (indent > 0) 
         f = format_ns::mk_indent(m(), indent, f);
-    ::pp(out, f.get(), m(), get_pp_default_params());
+    ::pp(out, f.get(), m());
 }
 
 void cmd_context::display(std::ostream & out, expr * n, unsigned indent, unsigned num_vars, char const * var_prefix, sbuffer<symbol> & var_names) const {
@@ -1562,7 +1561,7 @@ void cmd_context::display(std::ostream & out, expr * n, unsigned indent, unsigne
     pp(n, num_vars, var_prefix, f, var_names);
     if (indent > 0) 
         f = format_ns::mk_indent(m(), indent, f);
-    ::pp(out, f.get(), m(), get_pp_default_params());
+    ::pp(out, f.get(), m());
 }
 
 void cmd_context::display(std::ostream & out, expr * n, unsigned indent) const {
@@ -1575,7 +1574,7 @@ void cmd_context::display(std::ostream & out, func_decl * d, unsigned indent) co
     pp(d, f);
     if (indent > 0) 
         f = format_ns::mk_indent(m(), indent, f);
-    ::pp(out, f.get(), m(), get_pp_default_params());
+    ::pp(out, f.get(), m());
 }
 
 void cmd_context::dump_assertions(std::ostream & out) const {
diff --git a/src/cmd_context/extra_cmds/polynomial_cmds.cpp b/src/cmd_context/extra_cmds/polynomial_cmds.cpp
index 7b37b750e..e68789dac 100644
--- a/src/cmd_context/extra_cmds/polynomial_cmds.cpp
+++ b/src/cmd_context/extra_cmds/polynomial_cmds.cpp
@@ -26,10 +26,10 @@ Notes:
 #include"parametric_cmd.h"
 #include"mpq.h"
 #include"algebraic_numbers.h"
-#include"pp.h"
-#include"pp_params.h"
 #include"polynomial_var2value.h"
 #include"expr2var.h"
+#include"pp.h"
+#include"pp_params.hpp"
 
 static void to_poly(cmd_context & ctx, expr * t) {
     polynomial::numeral_manager nm;
@@ -145,9 +145,11 @@ class poly_isolate_roots_cmd : public cmd {
             scoped_anum_vector rs(m_am);
             m_am.isolate_roots(m_p, m_x2v, rs);
             ctx.regular_stream() << "(roots";
+            pp_params params;
+            bool pp_decimal = params.decimal();
             for (unsigned i = 0; i < rs.size(); i++) {
                 ctx.regular_stream() << std::endl;
-                if (!get_pp_default_params().m_pp_decimal)
+                if (!pp_decimal)
                     m_am.display_root_smt2(ctx.regular_stream(), rs[i]);
                 else
                     m_am.display_decimal(ctx.regular_stream(), rs[i]);
diff --git a/src/front_end_params/front_end_params.h b/src/front_end_params/front_end_params.h
index f9e62cd01..b87265c01 100644
--- a/src/front_end_params/front_end_params.h
+++ b/src/front_end_params/front_end_params.h
@@ -23,7 +23,6 @@ Revision History:
 #include"ast.h"
 #include"preprocessor_params.h"
 #include"smt_params.h"
-#include"pp_params.h"
 #include"parser_params.h"
 #include"arith_simplifier_params.h"
 #include"model_params.h"
diff --git a/src/model/model_pp.cpp b/src/model/model_pp.cpp
index a8e8a0880..b968c7184 100644
--- a/src/model/model_pp.cpp
+++ b/src/model/model_pp.cpp
@@ -85,8 +85,7 @@ static void display_functions(std::ostream & out, model_core const & md) {
         if (fi->is_partial())
             out << "  #unspecified";
         else {
-            pp_params const & params = get_pp_default_params();
-            out << "  " << mk_ismt2_pp(fi->get_else(), m, params, 5, arity, "x");
+            out << "  " << mk_ismt2_pp(fi->get_else(), m, params_ref(), 5, arity, "x");
         }
         for (unsigned j = 0; j < num_entries; j++)
             out << ")";
diff --git a/src/model/model_smt2_pp.cpp b/src/model/model_smt2_pp.cpp
index 1a639b5f1..929668638 100644
--- a/src/model/model_smt2_pp.cpp
+++ b/src/model/model_smt2_pp.cpp
@@ -128,7 +128,7 @@ static void pp_uninterp_sorts(std::ostream & out, ast_printer_context & ctx, mod
         format_ref f_card(fm(m));
         f_card = mk_indent(m, indent, mk_seq1<format**, f2f>(m, f_args, f_args+2, f2f(), "forall"));
         pp_indent(out, indent);
-        pp(out, f_card, m, get_pp_default_params());
+        pp(out, f_card, m);
         out << "\n";
         pp_indent(out, indent);
         out << ";; -----------\n";
@@ -284,7 +284,7 @@ static void pp_funs(std::ostream & out, ast_printer_context & ctx, model_core co
                                                                               body.get(),
                                                                               mk_string(m, ")")))));
         pp_indent(out, indent);
-        pp(out, def.get(), m, get_pp_default_params());
+        pp(out, def.get(), m);
         out << "\n";
     }
 }
diff --git a/src/muz_qe/dl_context.cpp b/src/muz_qe/dl_context.cpp
index 4a9bba27c..3a2844964 100644
--- a/src/muz_qe/dl_context.cpp
+++ b/src/muz_qe/dl_context.cpp
@@ -1672,12 +1672,11 @@ namespace datalog {
         bool print_low_level = m_params.get_bool("print_low_level_smt2", false);
         bool do_declare_vars = m_params.get_bool("print_with_variable_declarations", true);
 
-#define PP(_e_) if (print_low_level) out << mk_smt_pp(_e_, m); else ast_smt2_pp(out, _e_, env, params);
+#define PP(_e_) if (print_low_level) out << mk_smt_pp(_e_, m); else ast_smt2_pp(out, _e_, env);
 
         get_rules_as_formulas(rules, names);
 
         smt2_pp_environment_dbg env(m);
-        pp_params params;
         mk_fresh_name fresh_names;
         collect_free_funcs(num_axioms,  axioms,  visited, visitor, fresh_names);
         collect_free_funcs(rules.size(), rules.c_ptr(),   visited, visitor, fresh_names);
@@ -1719,7 +1718,7 @@ namespace datalog {
             func_decl* f = *it;
             out << "(declare-rel " << f->get_name() << " (";
             for (unsigned i = 0; i < f->get_arity(); ++i) {                
-                ast_smt2_pp(out, f->get_domain(i), env, params);
+                ast_smt2_pp(out, f->get_domain(i), env);
                 if (i + 1 < f->get_arity()) {
                     out << " ";
                 }
@@ -1796,7 +1795,6 @@ namespace datalog {
         // 
         smt2_pp_environment_dbg env(m);
         var_subst vsubst(m, false);
-        pp_params param;
         
         expr_ref_vector fresh_vars(m), subst(m);
         expr_ref res(m);
@@ -1839,7 +1837,7 @@ namespace datalog {
                     symbol name = fresh_names.next();
                     fresh_vars.push_back(m.mk_const(name, s));
                     out << "(declare-var " << name << " ";
-                    ast_smt2_pp(out, s, env, param);
+                    ast_smt2_pp(out, s, env);
                     out << ")\n"; 
                 }
                 subst.push_back(fresh_vars[vars[max_var]].get());
diff --git a/src/muz_qe/pdr_manager.cpp b/src/muz_qe/pdr_manager.cpp
index ad53f45db..9536d8f36 100644
--- a/src/muz_qe/pdr_manager.cpp
+++ b/src/muz_qe/pdr_manager.cpp
@@ -29,7 +29,6 @@ Revision History:
 #include "model_smt2_pp.h"
 #include "model_converter.h"
 
-
 namespace pdr {
 
     class collect_decls_proc {
@@ -143,11 +142,10 @@ namespace pdr {
             }
         }
         smt2_pp_environment_dbg env(m);
-        pp_params params;
         func_decl_set::iterator it = aux_decls.begin(), end = aux_decls.end();
         for (; it != end; ++it) {
             func_decl* f = *it;
-            ast_smt2_pp(out, f, env, params);
+            ast_smt2_pp(out, f, env);
             out << "\n";
         }
 
diff --git a/src/shell/main.cpp b/src/shell/main.cpp
index d6e7b1bf1..56882a02b 100644
--- a/src/shell/main.cpp
+++ b/src/shell/main.cpp
@@ -127,7 +127,6 @@ void init_params() {
         g_extra_params = new extra_params();
         register_verbosity_level(*g_params);
         register_warning(*g_params);
-        register_pp_params(*g_params);
         g_front_end_params->register_params(*g_params);
         g_extra_params->register_params(*g_params);
         g_params_initialized = true;
diff --git a/src/tactic/fpa/fpa2bv_converter.cpp b/src/tactic/fpa/fpa2bv_converter.cpp
index 77ff50e9b..62cc76266 100644
--- a/src/tactic/fpa/fpa2bv_converter.cpp
+++ b/src/tactic/fpa/fpa2bv_converter.cpp
@@ -105,7 +105,7 @@ void fpa2bv_converter::mk_value(func_decl * f, unsigned num, expr * const * args
 
         mk_triple(bv_sgn, bv_sig, biased_exp, result);
         TRACE("fpa2bv_dbg", tout << "value of [" << sign << " " << m_mpz_manager.to_string(sig) << " " << exp << "] is " 
-                                 << mk_ismt2_pp(result, m) << std::endl;);
+              << mk_ismt2_pp(result, m) << std::endl;);
                         
     }
 }