diff --git a/src/ast/ast_pp_util.cpp b/src/ast/ast_pp_util.cpp
index bbd1d0f41..43dccac02 100644
--- a/src/ast/ast_pp_util.cpp
+++ b/src/ast/ast_pp_util.cpp
@@ -45,10 +45,10 @@ void ast_pp_util::display_decls(std::ostream& out) {
     for (unsigned i = 0; i < n; ++i) {
         func_decl* f = coll.get_func_decls()[i];
         if (f->get_family_id() == null_family_id) {
-            ast_smt2_pp(out, f, m_env);
-            out << "\n";
+            ast_smt2_pp(out, f, m_env) << "\n";
         }
     }
+    SASSERT(coll.get_num_preds() == 0);
 }
 
 void ast_pp_util::display_asserts(std::ostream& out, expr_ref_vector const& fmls, bool neat) {
diff --git a/src/ast/ast_smt2_pp.cpp b/src/ast/ast_smt2_pp.cpp
index db66d9097..87ca5652a 100644
--- a/src/ast/ast_smt2_pp.cpp
+++ b/src/ast/ast_smt2_pp.cpp
@@ -599,9 +599,9 @@ class smt2_printer {
             return f;
         ptr_buffer<format> buf;
         buf.push_back(f);
-        for (unsigned i = 0; i < names.size(); i++) {
-            buf.push_back(pp_simple_attribute(is_pos ? ":lblpos " : ":lblneg ", names[i]));
-        }
+        for (symbol const& n : names) 
+            buf.push_back(pp_simple_attribute(is_pos ? ":lblpos " : ":lblneg ", n));
+
         return mk_seq1(m(), buf.begin(), buf.end(), f2f(), "!");
     }
 
@@ -1244,6 +1244,15 @@ std::ostream & ast_smt2_pp(std::ostream & out, unsigned sz, expr * const* es, sm
     return out;
 }
 
+std::ostream & ast_smt2_pp(std::ostream & out, symbol const& s, bool is_skolem, smt2_pp_environment & env, params_ref const& p) {
+    unsigned len;
+    ast_manager & m = env.get_manager();
+    format_ref r(fm(m));
+    r = env.pp_fdecl_name(s, len, is_skolem);
+    pp(out, r.get(), m, p);
+    return out;
+}
+
 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),
@@ -1262,6 +1271,8 @@ mk_ismt2_pp::mk_ismt2_pp(ast * t, ast_manager & m, unsigned indent, unsigned num
     m_var_prefix(var_prefix) {
 }
 
+
+
 std::ostream& operator<<(std::ostream& out, mk_ismt2_pp const & p) {
     smt2_pp_environment_dbg env(p.m_manager);    
     if (p.m_ast == 0) {
@@ -1309,14 +1320,14 @@ std::ostream& operator<<(std::ostream& out, app_ref_vector const&  e) {
 }
 
 std::ostream& operator<<(std::ostream& out, func_decl_ref_vector const&  e) {
-    for (unsigned i = 0; i < e.size(); ++i)
-        out << mk_ismt2_pp(e[i], e.get_manager()) << "\n";
+    for (func_decl* f : e) 
+        out << mk_ismt2_pp(f, e.get_manager()) << "\n";
     return out;
 }
 
 std::ostream& operator<<(std::ostream& out, sort_ref_vector const&  e) {
-    for (unsigned i = 0; i < e.size(); ++i)
-        out << mk_ismt2_pp(e[i], e.get_manager()) << "\n";
+    for (sort* s : e) 
+        out << mk_ismt2_pp(s, e.get_manager()) << "\n";
     return out;
 }
 
diff --git a/src/ast/ast_smt2_pp.h b/src/ast/ast_smt2_pp.h
index 8a4b3d80a..a1a457916 100644
--- a/src/ast/ast_smt2_pp.h
+++ b/src/ast/ast_smt2_pp.h
@@ -104,6 +104,7 @@ std::ostream & ast_smt2_pp(std::ostream & out, expr * n, smt2_pp_environment & e
 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, char const* cmd = "declare-fun");
 std::ostream & ast_smt2_pp(std::ostream & out, func_decl * f, expr* e, smt2_pp_environment & env, params_ref const & p = params_ref(), unsigned indent = 0, char const* cmd = "define-fun");
+std::ostream & ast_smt2_pp(std::ostream & out, symbol const& s, bool is_skolem, smt2_pp_environment & env, params_ref const& p = params_ref());
 
 /**
    \brief Internal wrapper (for debugging purposes only)
diff --git a/src/ast/ast_smt_pp.cpp b/src/ast/ast_smt_pp.cpp
index f8501824a..59b66d082 100644
--- a/src/ast/ast_smt_pp.cpp
+++ b/src/ast/ast_smt_pp.cpp
@@ -45,14 +45,6 @@ symbol smt_renaming::fix_symbol(symbol s, int k) {
     std::ostringstream buffer;
     char const * data = s.is_numerical() ? "" : s.bare_str();
 
-    if (data[0] && !data[1]) {
-        switch (data[0]) {
-        case '/': data = "op_div"; break;
-        case '%': data = "op_mod"; break;
-        default: break;
-        }
-    }
-
     if (k == 0 && *data) {
         if (s.is_numerical()) {
             return s;
@@ -80,7 +72,7 @@ symbol smt_renaming::fix_symbol(symbol s, int k) {
         buffer << s;
     }
     if (k > 0) {
-        buffer << k;
+        buffer << "!" << k;
     }
 
     return symbol(buffer.str().c_str());
@@ -139,6 +131,9 @@ symbol smt_renaming::get_symbol(symbol s0, bool is_skolem) {
     if (m_translate.find(s0, sb)) {
         if (is_skolem == sb.is_skolem)
             return sb.name;
+        if (sb.name_aux != symbol::null) {
+            return sb.name_aux;
+        }
         int k = 0;
         symbol s1;
         do {
@@ -146,6 +141,8 @@ symbol smt_renaming::get_symbol(symbol s0, bool is_skolem) {
         }
         while (s == s0 || (m_rev_translate.find(s, s1) && s1 != s0));
         m_rev_translate.insert(s, s0);
+        sb.name_aux = s;
+        m_translate.insert(s, sb);
         return s;
     }
 
diff --git a/src/ast/ast_smt_pp.h b/src/ast/ast_smt_pp.h
index 766c8530c..fd2cd186b 100644
--- a/src/ast/ast_smt_pp.h
+++ b/src/ast/ast_smt_pp.h
@@ -24,7 +24,7 @@ Revision History:
 #include "util/map.h"
 
 class smt_renaming {
-    struct sym_b { symbol name; bool is_skolem; sym_b(symbol n, bool s): name(n), is_skolem(s) {} sym_b():name(),is_skolem(false) {}};
+    struct sym_b { symbol name; bool is_skolem; symbol name_aux; sym_b(symbol n, bool s): name(n), is_skolem(s) {} sym_b():name(),is_skolem(false) {}};
     typedef map<symbol, symbol, symbol_hash_proc, symbol_eq_proc> symbol2symbol;
     typedef map<symbol, sym_b, symbol_hash_proc, symbol_eq_proc> symbol2sym_b;
     symbol2sym_b   m_translate;
diff --git a/src/ast/decl_collector.cpp b/src/ast/decl_collector.cpp
index e000f43df..0df4b0fc5 100644
--- a/src/ast/decl_collector.cpp
+++ b/src/ast/decl_collector.cpp
@@ -45,12 +45,14 @@ bool decl_collector::is_bool(sort * s) {
 }
 
 void decl_collector::visit_func(func_decl * n) {
-    family_id fid = n->get_family_id();
-    if (fid == null_family_id) {
-        if (m_sep_preds && is_bool(n->get_range()))
-            m_preds.push_back(n);
-        else
-            m_decls.push_back(n);
+    if (!m_visited.is_marked(n)) {
+        family_id fid = n->get_family_id();
+        if (fid == null_family_id) {
+            if (m_sep_preds && is_bool(n->get_range()))
+                m_preds.push_back(n);
+            else
+                m_decls.push_back(n);
+        }
     }
 }
 
@@ -63,31 +65,29 @@ decl_collector::decl_collector(ast_manager & m, bool preds):
 }
 
 void decl_collector::visit(ast* n) {
-    ptr_vector<ast> todo;
-    todo.push_back(n);
-    while (!todo.empty()) {
-        n = todo.back();
-        todo.pop_back();
+    m_todo.push_back(n);
+    while (!m_todo.empty()) {
+        n = m_todo.back();
+        m_todo.pop_back();
         if (!m_visited.is_marked(n)) {
-            m_visited.mark(n, true);
             switch(n->get_kind()) {
             case AST_APP: {
                 app * a = to_app(n);
                 for (unsigned i = 0; i < a->get_num_args(); ++i) {
-                    todo.push_back(a->get_arg(i));
+                    m_todo.push_back(a->get_arg(i));
                 }
-                todo.push_back(a->get_decl());
+                m_todo.push_back(a->get_decl());
                 break;
             }
             case AST_QUANTIFIER: {
                 quantifier * q = to_quantifier(n);
                 unsigned num_decls = q->get_num_decls();
                 for (unsigned i = 0; i < num_decls; ++i) {
-                    todo.push_back(q->get_decl_sort(i));
+                    m_todo.push_back(q->get_decl_sort(i));
                 }
-                todo.push_back(q->get_expr());
+                m_todo.push_back(q->get_expr());
                 for (unsigned i = 0; i < q->get_num_patterns(); ++i) {
-                    todo.push_back(q->get_pattern(i));
+                    m_todo.push_back(q->get_pattern(i));
                 }
                 break;
             }
@@ -97,9 +97,9 @@ void decl_collector::visit(ast* n) {
             case AST_FUNC_DECL: {
                 func_decl * d = to_func_decl(n);
                 for (unsigned i = 0; i < d->get_arity(); ++i) {
-                    todo.push_back(d->get_domain(i));
+                    m_todo.push_back(d->get_domain(i));
                 }
-                todo.push_back(d->get_range());
+                m_todo.push_back(d->get_range());
                 visit_func(d);
                 break;
             }
@@ -108,6 +108,7 @@ void decl_collector::visit(ast* n) {
             default:
                 UNREACHABLE();
             }
+            m_visited.mark(n, true);
         }
     }
 }
diff --git a/src/ast/decl_collector.h b/src/ast/decl_collector.h
index 053d6df41..0a812bb2c 100644
--- a/src/ast/decl_collector.h
+++ b/src/ast/decl_collector.h
@@ -36,7 +36,7 @@ class decl_collector {
 
     void visit_sort(sort* n);
     bool is_bool(sort* s);
-    void visit_func(func_decl* n);
+    ptr_vector<ast>      m_todo;
 
 
 public:
@@ -44,6 +44,7 @@ public:
     decl_collector(ast_manager & m, bool preds=true);
     ast_manager & m() { return m_manager; }
 
+    void visit_func(func_decl* n);
     void visit(ast * n);
     void visit(unsigned n, expr* const* es);
     void visit(expr_ref_vector const& es);
diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index 97c53d423..ee36468a5 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -868,6 +868,9 @@ void cmd_context::insert(symbol const & s, object_ref * r) {
 void cmd_context::model_add(symbol const & s, unsigned arity, sort *const* domain, expr * t) {
     if (!m_mc0) m_mc0 = alloc(generic_model_converter, m());
     func_decl_ref fn(m().mk_func_decl(s, arity, domain, m().get_sort(t)), m());
+    dictionary<func_decls>::entry * e = m_func_decls.insert_if_not_there2(s, func_decls());
+    func_decls & fs = e->get_data().m_value;
+    fs.insert(m(), fn);
     m_mc0->add(fn, t);
 }
 
diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h
index 48dd17cb0..abf19a487 100644
--- a/src/cmd_context/cmd_context.h
+++ b/src/cmd_context/cmd_context.h
@@ -304,7 +304,7 @@ protected:
     void erase_macro(symbol const& s);
     bool macros_find(symbol const& s, unsigned n, expr*const* args, expr*& t) const;
 
-    ref<generic_model_converter> m_mc0;
+    generic_model_converter_ref m_mc0;
 
 public:
     cmd_context(bool main_ctx = true, ast_manager * m = 0, symbol const & l = symbol::null);
@@ -324,6 +324,7 @@ public:
     void set_numeral_as_real(bool f) { m_numeral_as_real = f; }
     void set_interactive_mode(bool flag) { m_interactive_mode = flag; }
     void set_ignore_check(bool flag) { m_ignore_check = flag; }
+    bool ignore_check() const { return m_ignore_check; }
     void set_exit_on_error(bool flag) { m_exit_on_error = flag; }
     bool exit_on_error() const { return m_exit_on_error; }
     bool interactive_mode() const { return m_interactive_mode; }
diff --git a/src/cmd_context/tactic_cmds.cpp b/src/cmd_context/tactic_cmds.cpp
index 20a2b1c11..cd5eff9a6 100644
--- a/src/cmd_context/tactic_cmds.cpp
+++ b/src/cmd_context/tactic_cmds.cpp
@@ -200,6 +200,8 @@ public:
         if (!m_tactic) {
             throw cmd_exception("check-sat-using needs a tactic argument");
         }
+        if (ctx.ignore_check())
+            return;
         params_ref p = ctx.params().merge_default_params(ps());
         tactic_ref tref = using_params(sexpr2tactic(ctx, m_tactic), p);
         tref->set_logic(ctx.get_logic());
diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp
index 446059227..d73580323 100644
--- a/src/parsers/smt2/smt2parser.cpp
+++ b/src/parsers/smt2/smt2parser.cpp
@@ -2222,11 +2222,13 @@ namespace smt2 {
         }
 
         void parse_model_del() {
-            func_decl* f = parse_func_decl_ref();
-            check_rparen("invalid model-del, ')' expected");
-            m_ctx.model_del(f);
-            m_ctx.print_success();
             next();
+            symbol id = curr_id();
+            func_decl * f = m_ctx.find_func_decl(id);
+            m_ctx.model_del(f);
+            next();
+            check_rparen_next("invalid model-del, ')' expected");
+            m_ctx.print_success();
         }
 
         void parse_define_fun_rec() {
diff --git a/src/sat/sat_model_converter.cpp b/src/sat/sat_model_converter.cpp
index 7339f966d..d46063455 100644
--- a/src/sat/sat_model_converter.cpp
+++ b/src/sat/sat_model_converter.cpp
@@ -59,7 +59,7 @@ namespace sat {
         vector<entry>::const_iterator begin = m_entries.begin();
         vector<entry>::const_iterator it    = m_entries.end();
         bool first = true;
-        VERIFY(!m_solver || m_solver->check_clauses(m));
+        //VERIFY(!m_solver || m_solver->check_clauses(m));
         while (it != begin) {
             --it;
             SASSERT(it->get_kind() != ELIM_VAR || m[it->var()] == l_undef);
@@ -80,7 +80,7 @@ namespace sat {
                         process_stack(m, clause, st->stack());
                     }
                     sat = false;
-                    if (first && m_solver && !m_solver->check_clauses(m)) {
+                    if (false && first && m_solver && !m_solver->check_clauses(m)) {
                         display(std::cout, *it) << "\n";
                         first = false;
                     }
@@ -94,6 +94,8 @@ namespace sat {
                     continue;
                 bool sign  = l.sign();
                 bool_var v = l.var();
+                if (v >= m.size()) std::cout << v << " model size: " << m.size() << "\n";
+                VERIFY(v < m.size());
                 if (v == it->var())
                     var_sign = sign;
                 if (value_at(l, m) == l_true)
@@ -103,7 +105,7 @@ namespace sat {
                     m[v] = sign ? l_false : l_true;
                     // if (first) std::cout << "set: " << l << "\n";
                     sat = true;
-                    if (first && m_solver && !m_solver->check_clauses(m)) {
+                    if (false && first && m_solver && !m_solver->check_clauses(m)) {
                         display(std::cout, *it)  << "\n";;
                         first = false;
                     }
@@ -289,7 +291,7 @@ namespace sat {
         out << ")";
         for (literal l : entry.m_clauses) {
             if (l != null_literal) {
-                if (m_solver && m_solver->was_eliminated(l.var())) out << "\neliminated: " << l;
+                if (false && m_solver && m_solver->was_eliminated(l.var())) out << "\neliminated: " << l;
             }
         }
         return out;
@@ -317,12 +319,12 @@ namespace sat {
         return result;
     }
 
-    void model_converter::expand(vector<literal_vector>& update_stack) {
-        literal_vector clause;
+    void model_converter::expand(literal_vector& update_stack) {
+        sat::literal_vector clause;
         for (entry const& e : m_entries) {
-            clause.reset();
             unsigned index = 0;
             bool var_sign = false;
+            clause.reset();
             for (literal l : e.m_clauses) {
                 if (l == null_literal) {
                     elim_stack* st = e.m_elim_stack[index];                    
@@ -343,10 +345,12 @@ namespace sat {
                                 }
                             }
                             SASSERT(found);
-                            update_stack.push_back(literal_vector(csz, clause.c_ptr()));
+                            update_stack.append(csz, clause.c_ptr());
+                            update_stack.push_back(null_literal);
                         }
                     }
-                    update_stack.push_back(clause);
+                    update_stack.append(clause);
+                    update_stack.push_back(null_literal);
                     clause.reset();
                     continue;
                 }
diff --git a/src/sat/sat_model_converter.h b/src/sat/sat_model_converter.h
index a6f1f0bbe..8f8b1a41b 100644
--- a/src/sat/sat_model_converter.h
+++ b/src/sat/sat_model_converter.h
@@ -39,39 +39,47 @@ namespace sat {
 
     class solver;
 
+    static unsigned counter = 0;
+
     class model_converter {
         
     public:
         typedef svector<std::pair<unsigned, literal>> elim_stackv;
 
+
         class elim_stack {
-            unsigned       m_refcount;
+            unsigned        m_counter;
+            unsigned        m_refcount;
             elim_stackv     m_stack;
+            elim_stack(elim_stack const& );
         public:
             elim_stack(elim_stackv const& stack): 
+                m_counter(0),
                 m_refcount(0), 
                 m_stack(stack) {
+                m_counter = ++counter;
             }
             ~elim_stack() { }
             void inc_ref() { ++m_refcount; }
-            void dec_ref() { if (0 == --m_refcount) dealloc(this); }
+            void dec_ref() { if (0 == --m_refcount) { dealloc(this); } }
             elim_stackv const& stack() const { return m_stack; }
+            unsigned ref_count() const { return m_refcount; }
         };
 
         enum kind { ELIM_VAR = 0, BLOCK_LIT, CCE, ACCE };
         class entry {
             friend class model_converter;
-            unsigned           m_var:30;
-            unsigned           m_kind:2;
-            literal_vector     m_clauses; // the different clauses are separated by null_literal
-            sref_vector<elim_stack>  m_elim_stack;
-            entry(kind k, bool_var v):m_var(v), m_kind(k) {}
+            unsigned                m_var:30;
+            unsigned                m_kind:2;
+            literal_vector          m_clauses; // the different clauses are separated by null_literal
+            sref_vector<elim_stack> m_elim_stack;
+            entry(kind k, bool_var v): m_var(v), m_kind(k) {}
         public:
             entry(entry const & src):
                 m_var(src.m_var),
                 m_kind(src.m_kind),
-                m_clauses(src.m_clauses),
-                m_elim_stack(src.m_elim_stack) {
+                m_clauses(src.m_clauses) {
+                m_elim_stack.append(src.m_elim_stack);
             }
             bool_var var() const { return m_var; }
             kind get_kind() const { return static_cast<kind>(m_kind); }
@@ -115,7 +123,7 @@ namespace sat {
          *     lit0 := lit0 or (~lit1 & ~lit2 & ... & ~lit_k)
          *  
          */
-        void expand(vector<literal_vector>& update_stack);
+        void expand(literal_vector& update_stack);
     };
 
 };
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 0fb4dce93..6a9d1d5bb 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -61,6 +61,7 @@ namespace sat {
         m_num_checkpoints         = 0;
         m_simplifications         = 0;
         m_cuber                   = nullptr;
+        m_mc.set_solver(nullptr);
     }
 
     solver::~solver() {
@@ -1550,7 +1551,7 @@ namespace sat {
         
         if (m_config.m_drat) m_drat.check_model(m_model);
 
-        // m_mc.set_solver(this);
+        m_mc.set_solver(nullptr);
         m_mc(m_model);
 
         
diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp
index 218646de3..59f1a4a71 100644
--- a/src/sat/sat_solver/inc_sat_solver.cpp
+++ b/src/sat/sat_solver/inc_sat_solver.cpp
@@ -61,6 +61,7 @@ class inc_sat_solver : public solver {
     proof_converter_ref m_pc;
     model_converter_ref m_mc;
     model_converter_ref m_mc0;
+    model_converter_ref m_sat_mc;
     expr_dependency_ref m_dep_core;
     svector<double>     m_weights;
     std::string         m_unknown;
@@ -444,10 +445,11 @@ public:
     }
 
     virtual model_converter_ref get_model_converter() const {
-        if (m_internalized && m_internalized_converted) {
-            NOT_IMPLEMENTED_YET();
+        const_cast<inc_sat_solver*>(this)->convert_internalized();
+        if (m_internalized && m_internalized_converted) {            
             model_converter_ref mc = concat(m_mc0.get(), mk_bit_blaster_model_converter(m, m_bb_rewriter->const2bits()));
             mc = concat(solver::get_model_converter().get(), mc.get());
+            mc = concat(mc.get(), m_sat_mc.get());
             return mc;
         }
         else {
@@ -456,28 +458,14 @@ public:
     }
 
     void convert_internalized() {
-        if (!m_internalized) return;
+        if (!m_internalized || m_internalized_converted) return;
         sat2goal s2g;
-        model_converter_ref mc;
-        goal g(m, false, false, false);
-        s2g(m_solver, m_map, m_params, g, mc);
-        extract_model();
-        if (!m_model) {
-            m_model = alloc(model, m);
-        }
-        model_ref mdl = m_model;
-        if (m_mc) (*m_mc)(mdl);
-        for (unsigned i = 0; i < mdl->get_num_constants(); ++i) {
-            func_decl* c = mdl->get_constant(i);
-            expr_ref eq(m.mk_eq(m.mk_const(c), mdl->get_const_interp(c)), m);
-            g.assert_expr(eq);
-        }
+        m_sat_mc = nullptr;
+        goal g(m, false, true, false);
+        s2g(m_solver, m_map, m_params, g, m_sat_mc);
         m_internalized_fmls.reset();
         g.get_formulas(m_internalized_fmls);
         m_internalized_converted = true;
-        // if (mc) mc->display(std::cout << "mc");
-        // if (m_mc) m_mc->display(std::cout << "m_mc\n");
-        // if (m_mc0) m_mc0->display(std::cout << "m_mc0\n");
     }
 
     void init_preprocess() {
diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp
index 8daeb7ec0..48de6d600 100644
--- a/src/sat/tactic/goal2sat.cpp
+++ b/src/sat/tactic/goal2sat.cpp
@@ -52,7 +52,7 @@ struct goal2sat::imp {
     };
     ast_manager &               m;
     pb_util                     pb;
-    sat::ba_solver*        m_ext;
+    sat::ba_solver*             m_ext;
     svector<frame>              m_frame_stack;
     svector<sat::literal>       m_result_stack;
     obj_map<app, sat::literal>  m_cache;
@@ -896,20 +896,34 @@ struct sat2goal::imp {
     public:
         sat_model_converter(ast_manager & m, sat::solver const & s):m_var2expr(m) {
             m_mc.copy(s.get_model_converter());
-            m_mc.set_solver(&s);
             m_fmc = alloc(filter_model_converter, m);
         }
         
         ast_manager & m() { return m_var2expr.get_manager(); }
-        
-        void insert(expr * atom, bool aux) {
-            m_var2expr.push_back(atom);
+       
+        void init(unsigned num_vars) {
+            m_var2expr.resize(num_vars);
+        }
+
+        void insert(unsigned v, expr * atom, bool aux) {
+            VERIFY(!m_var2expr.get(v));
+            m_var2expr[v] = atom;
             if (aux) {
                 SASSERT(is_uninterp_const(atom));
                 SASSERT(m().is_bool(atom));
                 m_fmc->insert(to_app(atom)->get_decl());
             }
         }
+
+        void finish() {
+            sat::literal_vector updates;
+            m_mc.expand(updates);
+            for (sat::literal l : updates) {
+                if (l != sat::null_literal && !m_var2expr.get(l.var())) {
+                    insert(l.var(), m().mk_fresh_const(0, m().mk_bool_sort()), true);
+                }
+            }
+        }
         
         virtual void operator()(model_ref & md, unsigned goal_idx) {
             SASSERT(goal_idx == 0);
@@ -929,6 +943,10 @@ struct sat2goal::imp {
             sat::model sat_md;
             expr_ref val(m());
             for (expr * atom : m_var2expr) {
+                if (!atom) {
+                    sat_md.push_back(l_undef);
+                    continue;
+                }
                 ev(atom, val);
                 if (m().is_true(val)) 
                     sat_md.push_back(l_true);
@@ -945,7 +963,7 @@ struct sat2goal::imp {
             unsigned sz = m_var2expr.size();
             for (sat::bool_var v = 0; v < sz; v++) {
                 expr * atom = m_var2expr.get(v);
-                if (is_uninterp_const(atom)) {
+                if (atom && is_uninterp_const(atom)) {
                     func_decl * d = to_app(atom)->get_decl();
                     lbool new_val = sat_md[v];
                     if (new_val == l_true)
@@ -964,11 +982,12 @@ struct sat2goal::imp {
             sat_model_converter * res = alloc(sat_model_converter, translator.to());
             res->m_fmc = static_cast<filter_model_converter*>(m_fmc->translate(translator));
             for (expr* e : m_var2expr) 
-                res->m_var2expr.push_back(translator(e));
+                res->m_var2expr.push_back(e ? translator(e) : nullptr);
             return res;
         }
         
         expr_ref lit2expr(sat::literal l) {
+            VERIFY(m_var2expr.get(l.var()));
             expr_ref result(m_var2expr.get(l.var()), m());
             if (l.sign()) {
                 result = m().mk_not(result);
@@ -977,25 +996,43 @@ struct sat2goal::imp {
         }
 
         void display(std::ostream & out) {
-            vector<sat::literal_vector> updates;
+            sat::literal_vector updates;
             m_mc.expand(updates);
-            for (sat::literal_vector const& clause : updates) {
-                expr_ref_vector tail(m());
-                sat::literal lit0 = clause[0];
-                for (unsigned i = 1; i < clause.size(); ++i) {
-                    tail.push_back(lit2expr(~clause[i]));
+            sat::literal_vector clause;
+            expr_ref_vector tail(m());
+            expr_ref def(m());
+            for (sat::literal l : updates) {
+                if (l == sat::null_literal) {
+                    sat::literal lit0 = clause[0];
+                    for (unsigned i = 1; i < clause.size(); ++i) {
+                        tail.push_back(lit2expr(~clause[i]));
+                    }
+                    def = m().mk_or(lit2expr(lit0), mk_and(tail));            
+                    if (lit0.sign()) {
+                        lit0.neg();
+                        def = m().mk_not(def);
+                    }
+                    display_add(out, m(), to_app(lit2expr(lit0))->get_decl(), def);
+                    clause.reset();
+                    tail.reset();
                 }
-                expr_ref def(m().mk_or(lit2expr(lit0), mk_and(tail)), m());
-                if (lit0.sign()) {
-                    lit0.neg();
-                    def = m().mk_not(def);
+                else {
+                    clause.push_back(l);
                 }
-                display_add(out, m(), to_app(lit2expr(lit0))->get_decl(), def);
             }
             m_fmc->display(out);
         }
+        
+        virtual void collect(ast_pp_util& visitor) { 
+            m_env = &visitor.env();
+            for (expr* e : m_var2expr) if (e) visitor.coll.visit(e);
+            if (m_fmc) m_fmc->collect(visitor);
+        }
+
     };
 
+    typedef ref<sat_model_converter> sat_model_converter_ref;
+
     ast_manager &           m;
     expr_ref_vector         m_lit2expr;
     unsigned long long      m_max_memory;
@@ -1019,83 +1056,80 @@ struct sat2goal::imp {
             throw tactic_exception(TACTIC_MAX_MEMORY_MSG);
     }
 
-    void init_lit2expr(sat::solver const & s, atom2bool_var const & map, model_converter_ref & mc, bool produce_models) {
-        ref<sat_model_converter> _mc;
-        if (produce_models)
-            _mc = alloc(sat_model_converter, m, s);
+    void init_lit2expr(sat::solver const & s, atom2bool_var const & map, sat_model_converter_ref & mc) {
         unsigned num_vars = s.num_vars();
         m_lit2expr.resize(num_vars * 2);
         map.mk_inv(m_lit2expr);
-        sort * b = m.mk_bool_sort();
-        for (sat::bool_var v = 0; v < num_vars; v++) {
-            checkpoint();
-            sat::literal l(v, false);
-            if (m_lit2expr.get(l.index()) == 0) {
-                SASSERT(m_lit2expr.get((~l).index()) == 0);
-                app * aux = m.mk_fresh_const(0, b);
-                if (_mc)
-                    _mc->insert(aux, true);
-                m_lit2expr.set(l.index(), aux);
-                m_lit2expr.set((~l).index(), m.mk_not(aux));
-            }
-            else {
-                if (_mc)
-                    _mc->insert(m_lit2expr.get(l.index()), false);
-                SASSERT(m_lit2expr.get((~l).index()) != 0);
+        if (mc) {
+            mc->init(num_vars);
+            for (sat::bool_var v = 0; v < num_vars; v++) {
+                checkpoint();
+                sat::literal l(v, false);
+                if (m_lit2expr.get(l.index())) {
+                    mc->insert(v, m_lit2expr.get(l.index()), false);
+                    SASSERT(m_lit2expr[(~l).index()]);
+                }
             }
         }
-        mc = _mc.get();
     }
 
-    expr * lit2expr(sat::literal l) {
+    expr * lit2expr(sat_model_converter_ref& mc, sat::literal l) {
+        if (!m_lit2expr.get(l.index())) {
+            SASSERT(m_lit2expr.get((~l).index()) == 0);
+            app * aux = m.mk_fresh_const(0, m.mk_bool_sort());
+            if (mc)
+                mc->insert(l.var(), aux, true);
+            m_lit2expr.set(l.index(), aux);
+            m_lit2expr.set((~l).index(), m.mk_not(aux));
+        }        
         return m_lit2expr.get(l.index());
     }
 
-    void assert_pb(goal& r, sat::ba_solver::pb const& p) {
+    void assert_pb(sat_model_converter_ref& mc, goal& r, sat::ba_solver::pb const& p) {
         pb_util pb(m);
         ptr_buffer<expr> lits;
         vector<rational> coeffs;
         for (auto const& wl : p) {
-            lits.push_back(lit2expr(wl.second));
+            lits.push_back(lit2expr(mc, wl.second));
             coeffs.push_back(rational(wl.first));
         }
         rational k(p.k());
         expr_ref fml(pb.mk_ge(p.size(), coeffs.c_ptr(), lits.c_ptr(), k), m);
         
         if (p.lit() != sat::null_literal) {
-            fml = m.mk_eq(lit2expr(p.lit()), fml);            
+            fml = m.mk_eq(lit2expr(mc, p.lit()), fml);            
         }
         r.assert_expr(fml);
     }
 
-    void assert_card(goal& r, sat::ba_solver::card const& c) {
+    void assert_card(sat_model_converter_ref& mc, goal& r, sat::ba_solver::card const& c) {
         pb_util pb(m);
         ptr_buffer<expr> lits;
         for (sat::literal l : c) {
-            lits.push_back(lit2expr(l));
+            lits.push_back(lit2expr(mc, l));
         }
         expr_ref fml(pb.mk_at_least_k(c.size(), lits.c_ptr(), c.k()), m);
         
         if (c.lit() != sat::null_literal) {
-            fml = m.mk_eq(lit2expr(c.lit()), fml);            
+            fml = m.mk_eq(lit2expr(mc, c.lit()), fml);            
         }
         r.assert_expr(fml);
     }
 
-    void assert_xor(goal & r, sat::ba_solver::xor const& x) {
+    void assert_xor(sat_model_converter_ref& mc, goal & r, sat::ba_solver::xor const& x) {
         ptr_buffer<expr> lits;
         for (sat::literal l : x) {
-            lits.push_back(lit2expr(l));
+            lits.push_back(lit2expr(mc, l));
         }
         expr_ref fml(m.mk_xor(x.size(), lits.c_ptr()), m);
         
         if (x.lit() != sat::null_literal) {
-            fml = m.mk_eq(lit2expr(x.lit()), fml);            
+            fml = m.mk_eq(lit2expr(mc, x.lit()), fml);            
         }
         r.assert_expr(fml);
     }
 
-    void assert_clauses(sat::solver const & s, sat::clause_vector const& clauses, goal & r, bool asserted) {
+    void assert_clauses(sat_model_converter_ref& mc, sat::solver const & s, sat::clause_vector const& clauses, goal & r, bool asserted) {
         ptr_buffer<expr> lits;
         for (sat::clause* cp : clauses) {
             checkpoint();
@@ -1104,7 +1138,7 @@ struct sat2goal::imp {
             unsigned sz = c.size();
             if (asserted || m_learned || c.glue() <= s.get_config().m_gc_small_lbd) {
                 for (sat::literal l : c) {
-                    lits.push_back(lit2expr(l));
+                    lits.push_back(lit2expr(mc, l));
                 }
                 r.assert_expr(m.mk_or(lits.size(), lits.c_ptr()));
             }
@@ -1121,17 +1155,22 @@ struct sat2goal::imp {
             r.assert_expr(m.mk_false());
             return;
         }
-        init_lit2expr(s, map, mc, r.models_enabled());
+        ref<sat_model_converter> _mc;
+        if (r.models_enabled()) {
+            _mc = alloc(sat_model_converter, m, s);
+        }
+        mc = _mc.get();
+        init_lit2expr(s, map, _mc);
         // collect units
         unsigned num_vars = s.num_vars();
         for (sat::bool_var v = 0; v < num_vars; v++) {
             checkpoint();
             switch (s.value(v)) {
             case l_true:
-                r.assert_expr(lit2expr(sat::literal(v, false)));
+                r.assert_expr(lit2expr(_mc, sat::literal(v, false)));
                 break;
             case l_false:
-                r.assert_expr(lit2expr(sat::literal(v, true)));
+                r.assert_expr(lit2expr(_mc, sat::literal(v, true)));
                 break;
             case l_undef:
                 break;
@@ -1142,96 +1181,50 @@ struct sat2goal::imp {
         s.collect_bin_clauses(bin_clauses, m_learned);
         for (sat::solver::bin_clause const& bc : bin_clauses) {
             checkpoint();
-            r.assert_expr(m.mk_or(lit2expr(bc.first), lit2expr(bc.second)));
+            r.assert_expr(m.mk_or(lit2expr(_mc, bc.first), lit2expr(_mc, bc.second)));
         }
         // collect clauses
-        assert_clauses(s, s.clauses(), r, true);
+        assert_clauses(_mc, s, s.clauses(), r, true);
 
         sat::ba_solver* ext = get_ba_solver(s);
         if (ext) {
             for (auto* c : ext->constraints()) {
                 switch (c->tag()) {
                 case sat::ba_solver::card_t: 
-                    assert_card(r, c->to_card());
+                    assert_card(_mc, r, c->to_card());
                     break;
                 case sat::ba_solver::pb_t: 
-                    assert_pb(r, c->to_pb());
+                    assert_pb(_mc, r, c->to_pb());
                     break;
                 case sat::ba_solver::xor_t: 
-                    assert_xor(r, c->to_xor());
+                    assert_xor(_mc, r, c->to_xor());
                     break;
                 }
             }
         }
-        //s.display(std::cout);
-        //r.display(std::cout);
+        if (_mc) _mc->finish();
     }
 
-    void add_clause(sat::literal_vector const& lits, expr_ref_vector& lemmas) {
+    void add_clause(sat_model_converter_ref& mc, sat::literal_vector const& lits, expr_ref_vector& lemmas) {
         expr_ref_vector lemma(m);
         for (sat::literal l : lits) {
-            expr* e = m_lit2expr.get(l.index(), 0);
+            expr* e = lit2expr(mc, l);
             if (!e) return;
             lemma.push_back(e);
         }
         lemmas.push_back(mk_or(lemma));
     }
 
-    void add_clause(sat::clause const& c, expr_ref_vector& lemmas) {
+    void add_clause(sat_model_converter_ref& mc, sat::clause const& c, expr_ref_vector& lemmas) {
         expr_ref_vector lemma(m);
         for (sat::literal l : c) {
-            expr* e = m_lit2expr.get(l.index(), 0);
+            expr* e = lit2expr(mc, l);
             if (!e) return;
             lemma.push_back(e);
         }
         lemmas.push_back(mk_or(lemma));
     }
 
-    void get_learned(sat::solver const& s, atom2bool_var const& map, expr_ref_vector& lemmas) {
-        if (s.inconsistent()) {
-            lemmas.push_back(m.mk_false());
-            return;
-        }
-
-        unsigned num_vars = s.num_vars();
-        m_lit2expr.resize(num_vars * 2);
-        map.mk_inv(m_lit2expr);
-
-        sat::literal_vector lits;
-        // collect units
-        for (sat::bool_var v = 0; v < num_vars; v++) {
-            checkpoint();
-            lits.reset();
-            switch (s.value(v)) {
-            case l_true:
-                lits.push_back(sat::literal(v, false));
-                add_clause(lits, lemmas);
-                break;
-            case l_false:
-                lits.push_back(sat::literal(v, false));
-                add_clause(lits, lemmas);
-                break;
-            case l_undef:
-                break;
-            }
-        }
-        // collect learned binary clauses
-        svector<sat::solver::bin_clause> bin_clauses;
-        s.collect_bin_clauses(bin_clauses, true, true);
-        for (sat::solver::bin_clause const& bc : bin_clauses) {
-            checkpoint();
-            lits.reset();
-            lits.push_back(bc.first);
-            lits.push_back(bc.second);
-            add_clause(lits, lemmas);
-        }
-        // collect clauses
-        for (sat::clause const* c : s.learned()) {
-            add_clause(*c, lemmas);
-        }
-    }
-
-
 };
 
 sat2goal::sat2goal():m_imp(0) {
@@ -1260,9 +1253,4 @@ void sat2goal::operator()(sat::solver const & t, atom2bool_var const & m, params
     proc(t, m, g, mc);
 }
 
-void sat2goal::get_learned(sat::solver const & t, atom2bool_var const & m, params_ref const& p, expr_ref_vector& lemmas) {
-    imp proc(lemmas.get_manager(), p);
-    scoped_set_imp set(this, &proc);
-    proc.get_learned(t, m, lemmas);
-}
 
diff --git a/src/solver/solver.cpp b/src/solver/solver.cpp
index 122bb2933..c7f385416 100644
--- a/src/solver/solver.cpp
+++ b/src/solver/solver.cpp
@@ -37,16 +37,26 @@ expr * solver::get_assertion(unsigned idx) const {
 
 std::ostream& solver::display(std::ostream & out) const {
     expr_ref_vector fmls(get_manager());
+    std::cout << "display 1\n";
     get_assertions(fmls);
+    std::cout << "display 2\n";
     ast_pp_util visitor(get_manager());
-    visitor.collect(fmls);
-    visitor.display_decls(out);
-    visitor.display_asserts(out, fmls, true);
     model_converter_ref mc = get_model_converter();
+    std::cout << "display 3\n";
+    if (mc.get()) { 
+        mc->collect(visitor); 
+    }
+    std::cout << "display 4\n";
+    visitor.collect(fmls);
+    std::cout << "display 5\n";
+    visitor.display_decls(out);
+    std::cout << "display 6\n";
+    visitor.display_asserts(out, fmls, true);
+    std::cout << "display 7\n";
     if (mc.get()) {
-        mc->set_pp_env(&visitor.env());
         mc->display(out);
     }
+    std::cout << "display 8\n";
     return out;
 }
 
diff --git a/src/solver/tactic2solver.cpp b/src/solver/tactic2solver.cpp
index 1dd48fb9c..b9f269b6d 100644
--- a/src/solver/tactic2solver.cpp
+++ b/src/solver/tactic2solver.cpp
@@ -83,7 +83,7 @@ public:
         return expr_ref(m.mk_true(), m);
     }
 
-    virtual model_converter* get_model_converter() { return m_mc.get(); }
+    virtual model_converter_ref get_model_converter() const { return m_mc; }
 
 };
 
diff --git a/src/tactic/bv/bit_blaster_model_converter.cpp b/src/tactic/bv/bit_blaster_model_converter.cpp
index b21defd44..d8dbb77a4 100644
--- a/src/tactic/bv/bit_blaster_model_converter.cpp
+++ b/src/tactic/bv/bit_blaster_model_converter.cpp
@@ -34,11 +34,9 @@ struct bit_blaster_model_converter : public model_converter {
     ast_manager & m() const { return m_vars.get_manager(); }
     
     bit_blaster_model_converter(ast_manager & m, obj_map<func_decl, expr*> const & const2bits):m_vars(m), m_bits(m) {
-        obj_map<func_decl, expr*>::iterator it  = const2bits.begin();
-        obj_map<func_decl, expr*>::iterator end = const2bits.end();
-        for (; it != end; ++it) {
-            func_decl * v = it->m_key;
-            expr * bits   = it->m_value;
+        for (auto const& kv : const2bits) {
+            func_decl * v = kv.m_key;
+            expr * bits   = kv.m_value;
             SASSERT(!TO_BOOL || is_app_of(bits, m.get_family_id("bv"), OP_MKBV));
             SASSERT(TO_BOOL  || is_app_of(bits, m.get_family_id("bv"), OP_CONCAT));
             m_vars.push_back(v);
@@ -155,17 +153,11 @@ struct bit_blaster_model_converter : public model_converter {
         unsigned bv_sz = to_app(bs)->get_num_args();
         expr_ref_vector args(m());
         app_ref result(m());
-        for (unsigned j = 0; j < bv_sz; ++j) {
-            expr * bit = to_app(bs)->get_arg(j);
+        for (expr * bit : *to_app(bs)) {
             SASSERT(is_uninterp_const(bit));
             func_decl * bit_decl = to_app(bit)->get_decl();
             expr * bit_val = old_model.get_const_interp(bit_decl);
-            if (bit_val != 0) {
-                args.push_back(bit_val);
-            }
-            else {
-                args.push_back(bit);
-            }
+            args.push_back(bit_val ? bit_val : bit);
         }
 
         if (TO_BOOL) {
@@ -194,14 +186,10 @@ struct bit_blaster_model_converter : public model_converter {
     }
     
     virtual void display(std::ostream & out) {
-        out << "(bit-blaster-model-converter";
         unsigned sz = m_vars.size();
         for (unsigned i = 0; i < sz; i++) {
-            out << "\n  (" << m_vars.get(i)->get_name() << " ";
-            unsigned indent = m_vars.get(i)->get_name().size() + 4;
-            out << mk_ismt2_pp(m_bits.get(i), m(), indent) << ")";
-        }   
-        out << ")" << std::endl;
+            display_add(out, m(), m_vars.get(i), m_bits.get(i));
+        }
     }
 
 protected:
@@ -210,10 +198,10 @@ public:
 
     virtual model_converter * translate(ast_translation & translator) {
         bit_blaster_model_converter * res = alloc(bit_blaster_model_converter, translator.to());
-        for (unsigned i = 0; i < m_vars.size(); i++)
-            res->m_vars.push_back(translator(m_vars[i].get()));
-        for (unsigned i = 0; i < m_bits.size(); i++)
-            res->m_bits.push_back(translator(m_bits[i].get()));
+        for (func_decl * v : m_vars) 
+            res->m_vars.push_back(translator(v));
+        for (expr* b : m_bits)
+            res->m_bits.push_back(translator(b));
         return res;
     }
 };
diff --git a/src/tactic/bv/bit_blaster_tactic.cpp b/src/tactic/bv/bit_blaster_tactic.cpp
index 5c6c43778..308b775a4 100644
--- a/src/tactic/bv/bit_blaster_tactic.cpp
+++ b/src/tactic/bv/bit_blaster_tactic.cpp
@@ -81,7 +81,7 @@ class bit_blaster_tactic : public tactic {
                     new_pr     = m().mk_modus_ponens(pr, new_pr);
                 }
                 if (curr != new_curr) {
-                    change = true;
+                    change = true;                    
                     TRACE("bit_blaster", tout << mk_pp(curr, m()) << " -> " << mk_pp(new_curr, m()) << "\n";);
                     g->update(idx, new_curr, new_pr, g->dep(idx));
                 }
diff --git a/src/tactic/converter.h b/src/tactic/converter.h
index 84df02c94..7fa118e4b 100644
--- a/src/tactic/converter.h
+++ b/src/tactic/converter.h
@@ -29,11 +29,13 @@ public:
     converter():m_ref_count(0) {}
     virtual ~converter() {}
 
-    void inc_ref() { ++m_ref_count; }
+	void inc_ref() { ++m_ref_count; std::cout << "inc_ref " << m_ref_count << " " << this << "\n"; }
     void dec_ref() { 
         --m_ref_count;
-        if (m_ref_count == 0)
-            dealloc(this);
+		if (m_ref_count == 0) {
+			std::cout << "dec_ref " << this << "\n";
+			dealloc(this);
+		}
     }
 
     virtual void cancel() {}
diff --git a/src/tactic/filter_model_converter.cpp b/src/tactic/filter_model_converter.cpp
index 40de848be..4041e9275 100644
--- a/src/tactic/filter_model_converter.cpp
+++ b/src/tactic/filter_model_converter.cpp
@@ -62,7 +62,14 @@ void filter_model_converter::display(std::ostream & out) {
 
 model_converter * filter_model_converter::translate(ast_translation & translator) {
     filter_model_converter * res = alloc(filter_model_converter, translator.to());
-    for (unsigned i = 0; i < m_decls.size(); i++)
-        res->m_decls.push_back(translator(m_decls[i].get()));
+    for (func_decl* f : m_decls) 
+        res->m_decls.push_back(translator(f));
     return res;
 }
+
+void filter_model_converter::collect(ast_pp_util& visitor) { 
+    m_env = &visitor.env(); 
+    std::cout << "collect filter: " << m_decls.size() << "\n";
+    for (func_decl* f : m_decls) visitor.coll.visit_func(f);
+}
+
diff --git a/src/tactic/filter_model_converter.h b/src/tactic/filter_model_converter.h
index 1cb6ec056..2c3361808 100644
--- a/src/tactic/filter_model_converter.h
+++ b/src/tactic/filter_model_converter.h
@@ -20,6 +20,7 @@ Notes:
 #define FILTER_MODEL_CONVERTER_H_
 
 #include "tactic/model_converter.h"
+#include "ast/ast_pp_util.h"
 
 class filter_model_converter : public model_converter {
     func_decl_ref_vector  m_decls;
@@ -37,7 +38,7 @@ public:
     virtual void operator()(model_ref & md) { operator()(md, 0); } // TODO: delete
 
     virtual void cancel() {}
-
+    
     virtual void display(std::ostream & out);
 
     void insert(func_decl * d) {
@@ -45,6 +46,9 @@ public:
     }
 
     virtual model_converter * translate(ast_translation & translator);
+
+    virtual void collect(ast_pp_util& visitor);
+
 };
 
 typedef ref<filter_model_converter> filter_model_converter_ref;
diff --git a/src/tactic/model_converter.cpp b/src/tactic/model_converter.cpp
index 6984c0536..01c7a16bb 100644
--- a/src/tactic/model_converter.cpp
+++ b/src/tactic/model_converter.cpp
@@ -24,26 +24,16 @@ Notes:
  * Add or overwrite value in model.
  */
 void model_converter::display_add(std::ostream& out, ast_manager& m, func_decl* f, expr* e) const {
-    // TBD: for arity > 0, requires signature of arguments.
-    if (m_env) {
-        ast_smt2_pp(out, f, e, *m_env, params_ref(), 0, "model-add");        
-    }
-    else {
-        unsigned indent = f->get_name().size() + 4;
-        out << "(model-add " << f->get_name() << " " << mk_ismt2_pp(e, m, indent) << ")\n";
-    }
+    VERIFY(m_env);
+    ast_smt2_pp(out, f, e, *m_env, params_ref(), 0, "model-add") << "\n";
 }
 
 /*
  * A value is removed from the model.
  */
 void model_converter::display_del(std::ostream& out, func_decl* f) const {
-    if (m_env) {
-        ast_smt2_pp(out, f, *m_env, params_ref(), 0, "model-del");
-    }
-    else {
-        out << "(model-del " << f->get_name() << ")\n";
-    }
+    VERIFY(m_env);
+    ast_smt2_pp(out << "(model-del ", f->get_name(), f->is_skolem(), *m_env) << ")\n";    
 }
 
 void model_converter::display_add(std::ostream& out, ast_manager& m) {
@@ -64,7 +54,9 @@ void model_converter::display_add(std::ostream& out, ast_manager& m) {
 
 class concat_model_converter : public concat_converter<model_converter> {
 public:
-    concat_model_converter(model_converter * mc1, model_converter * mc2): concat_converter<model_converter>(mc1, mc2) {}
+    concat_model_converter(model_converter * mc1, model_converter * mc2): concat_converter<model_converter>(mc1, mc2) {
+        VERIFY(m_c1 && m_c2);
+    }
 
     virtual void operator()(model_ref & m) {
         this->m_c2->operator()(m);
@@ -86,6 +78,11 @@ public:
     virtual model_converter * translate(ast_translation & translator) {
         return this->translate_core<concat_model_converter>(translator);
     }
+
+    virtual void collect(ast_pp_util& visitor) { 
+        this->m_c1->collect(visitor);
+        this->m_c2->collect(visitor);
+    }
 };
 
 model_converter * concat(model_converter * mc1, model_converter * mc2) {
diff --git a/src/tactic/model_converter.h b/src/tactic/model_converter.h
index 02e59f6d5..f7597be07 100644
--- a/src/tactic/model_converter.h
+++ b/src/tactic/model_converter.h
@@ -19,6 +19,7 @@ Notes:
 #ifndef MODEL_CONVERTER_H_
 #define MODEL_CONVERTER_H_
 
+#include "ast/ast_pp_util.h"
 #include "model/model.h"
 #include "tactic/converter.h"
 #include "util/ref.h"
@@ -48,8 +49,8 @@ public:
 
     
     virtual model_converter * translate(ast_translation & translator) = 0;
-
-    void set_pp_env(smt2_pp_environment* env) { m_env = env; }
+    
+    virtual void collect(ast_pp_util& visitor) { m_env = &visitor.env(); }
 };
 
 typedef ref<model_converter> model_converter_ref;
diff --git a/src/tactic/portfolio/bounded_int2bv_solver.cpp b/src/tactic/portfolio/bounded_int2bv_solver.cpp
index 9e4a0c547..bb8bb463b 100644
--- a/src/tactic/portfolio/bounded_int2bv_solver.cpp
+++ b/src/tactic/portfolio/bounded_int2bv_solver.cpp
@@ -157,6 +157,7 @@ public:
             filter_model(mdl);
         }
     }
+    virtual model_converter_ref get_model_converter() const { return m_solver->get_model_converter(); }
     virtual proof * get_proof() { return m_solver->get_proof(); }
     virtual std::string reason_unknown() const { return m_solver->reason_unknown(); }
     virtual void set_reason_unknown(char const* msg) { m_solver->set_reason_unknown(msg); }
diff --git a/src/tactic/portfolio/enum2bv_solver.cpp b/src/tactic/portfolio/enum2bv_solver.cpp
index 1df7a000c..c74d729b5 100644
--- a/src/tactic/portfolio/enum2bv_solver.cpp
+++ b/src/tactic/portfolio/enum2bv_solver.cpp
@@ -102,6 +102,7 @@ public:
             filter_model(mdl);            
         }
     } 
+    virtual model_converter_ref get_model_converter() const { return m_solver->get_model_converter(); }
     virtual proof * get_proof() { return m_solver->get_proof(); }
     virtual std::string reason_unknown() const { return m_solver->reason_unknown(); }
     virtual void set_reason_unknown(char const* msg) { m_solver->set_reason_unknown(msg); }
diff --git a/src/tactic/portfolio/pb2bv_solver.cpp b/src/tactic/portfolio/pb2bv_solver.cpp
index 44898a578..4998cdecf 100644
--- a/src/tactic/portfolio/pb2bv_solver.cpp
+++ b/src/tactic/portfolio/pb2bv_solver.cpp
@@ -93,6 +93,7 @@ public:
             filter_model(mdl);            
         }
     } 
+    virtual model_converter_ref get_model_converter() const { return m_solver->get_model_converter(); }
     virtual proof * get_proof() { return m_solver->get_proof(); }
     virtual std::string reason_unknown() const { return m_solver->reason_unknown(); }
     virtual void set_reason_unknown(char const* msg) { m_solver->set_reason_unknown(msg); }