diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index f172e5e93..acbdc0bcf 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -229,6 +229,28 @@ func_decl * func_decls::find(ast_manager & m, unsigned num_args, expr * const *
     return find(num_args, sorts.c_ptr(), range);
 }
 
+unsigned func_decls::get_num_entries() const {
+    if (!more_than_one())
+        return 1;
+
+    func_decl_set * fs = UNTAG(func_decl_set *, m_decls);
+    return fs->size();
+}
+
+func_decl * func_decls::get_entry(unsigned inx) {
+    if (!more_than_one()) {
+        SASSERT(inx == 0);
+        return first();
+    }
+    else {
+        func_decl_set * fs = UNTAG(func_decl_set *, m_decls);
+        auto b = fs->begin();
+        for (unsigned i = 0; i < inx; i++)
+            b++;
+        return *b;
+    }
+}
+
 void macro_decls::finalize(ast_manager& m) {
     for (auto v : *m_decls) m.dec_ref(v.m_body);
     dealloc(m_decls);
@@ -288,13 +310,13 @@ void cmd_context::insert_macro(symbol const& s, unsigned arity, sort*const* doma
     }
     else {
         VERIFY(decls.insert(m(), arity, domain, t));
-    }    
+    }
 }
 
 void cmd_context::erase_macro(symbol const& s) {
     macro_decls decls;
     VERIFY(m_macros.find(s, decls));
-    decls.erase_last(m());    
+    decls.erase_last(m());
 }
 
 bool cmd_context::macros_find(symbol const& s, unsigned n, expr*const* args, expr*& t) const {
@@ -870,11 +892,11 @@ void cmd_context::insert_rec_fun(func_decl* f, expr_ref_vector const& binding, s
     }
 
     //
-    // disable warning given the current way they are used 
-    // (Z3 will here silently assume and not check the definitions to be well founded, 
+    // disable warning given the current way they are used
+    // (Z3 will here silently assume and not check the definitions to be well founded,
     // and please use HSF for everything else).
     //
-    if (false && !ids.empty() && !m_rec_fun_declared) {        
+    if (false && !ids.empty() && !m_rec_fun_declared) {
         warning_msg("recursive function definitions are assumed well-founded");
         m_rec_fun_declared = true;
     }
@@ -953,7 +975,7 @@ func_decl * cmd_context::find_func_decl(symbol const & s, unsigned num_indices,
         return f;
     }
 
-    if (contains_macro(s, arity, domain)) 
+    if (contains_macro(s, arity, domain))
         throw cmd_exception("invalid function declaration reference, named expressions (aka macros) cannot be referenced ", s);
 
     if (num_indices > 0)
@@ -1316,7 +1338,7 @@ void cmd_context::push(unsigned n) {
         push();
 }
 
-void cmd_context::restore_func_decls(unsigned old_sz) {    
+void cmd_context::restore_func_decls(unsigned old_sz) {
     SASSERT(old_sz <= m_func_decls_stack.size());
     svector<sf_pair>::iterator it  = m_func_decls_stack.begin() + old_sz;
     svector<sf_pair>::iterator end = m_func_decls_stack.end();
@@ -1418,7 +1440,7 @@ void cmd_context::pop(unsigned n) {
     restore_assertions(s.m_assertions_lim);
     restore_psort_inst(s.m_psort_inst_stack_lim);
     m_scopes.shrink(new_lvl);
-    
+
 }
 
 void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions) {
@@ -1488,6 +1510,7 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
     }
     display_sat_result(r);
     if (r == l_true) {
+        complete_model();
         validate_model();
     }
     validate_check_sat_result(r);
@@ -1548,7 +1571,7 @@ void cmd_context::reset_assertions() {
         if (m_solver) m_solver->push();
     }
 }
-    
+
 
 void cmd_context::display_model(model_ref& mdl) {
     if (mdl) {
@@ -1632,6 +1655,60 @@ struct contains_array_op_proc {
     void operator()(quantifier * n) {}
 };
 
+/**
+    \brief Complete the model if necessary.
+*/
+void cmd_context::complete_model() {
+    if (!is_model_available() ||
+        gparams::get_value("model.completion") != "true")
+        return;
+
+    model_ref md;
+    get_check_sat_result()->get_model(md);
+    SASSERT(md.get() != 0);
+    params_ref p;
+    p.set_uint("max_degree", UINT_MAX); // evaluate algebraic numbers of any degree.
+    p.set_uint("sort_store", true);
+    p.set_bool("completion", true);
+    model_evaluator evaluator(*(md.get()), p);
+    evaluator.set_expand_array_equalities(false);
+
+    scoped_rlimit _rlimit(m().limit(), 0);
+    cancel_eh<reslimit> eh(m().limit());
+    expr_ref r(m());
+    scoped_ctrl_c ctrlc(eh);
+
+    for (auto kd : m_psort_decls) {
+        symbol const & k = kd.m_key;
+        psort_decl * v = kd.m_value;
+        if (v->is_user_decl()) {
+            SASSERT(!v->has_var_params());
+            IF_VERBOSE(12, verbose_stream() << "(model.completion " << k << ")\n"; );
+            ptr_vector<sort> param_sorts(v->get_num_params(), m().mk_bool_sort());
+            sort * srt = v->instantiate(*m_pmanager, param_sorts.size(), param_sorts.c_ptr());
+            if (!md->has_uninterpreted_sort(srt)) {
+                expr * singleton = m().get_some_value(srt);
+                md->register_usort(srt, 1, &singleton);
+            }
+        }
+    }
+
+    for (auto kd : m_func_decls) {
+        symbol const & k = kd.m_key;
+        func_decls & v = kd.m_value;
+        IF_VERBOSE(12, verbose_stream() << "(model.completion " << k << ")\n"; );
+        for (unsigned i = 0; i < v.get_num_entries(); i++) {
+            func_decl * f = v.get_entry(i);
+            if (!md->has_interpretation(f)) {
+                sort * range = f->get_range();
+                func_interp * fi = alloc(func_interp, m(), f->get_arity());
+                fi->set_else(m().get_some_value(range));
+                md->register_decl(f, fi);
+            }
+        }
+    }
+}
+
 /**
    \brief Check if the current model satisfies the quantifier free formulas.
 */
@@ -1918,7 +1995,7 @@ void cmd_context::dt_eh::operator()(sort * dt, pdecl* pd) {
     }
     if (m_owner.m_scopes.size() > 0) {
         m_owner.m_psort_inst_stack.push_back(pd);
-        
+
     }
 }
 
diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h
index 189863e58..5883a8d8e 100644
--- a/src/cmd_context/cmd_context.h
+++ b/src/cmd_context/cmd_context.h
@@ -8,7 +8,7 @@ Module Name:
 Abstract:
     Ultra-light command context.
     It provides a generic command pluging infrastructure.
-    A command context also provides names (aka symbols) to Z3 objects. 
+    A command context also provides names (aka symbols) to Z3 objects.
     These names are used to reference Z3 objects in commands.
 
 Author:
@@ -58,6 +58,8 @@ public:
     func_decl * first() const;
     func_decl * find(unsigned arity, sort * const * domain, sort * range) const;
     func_decl * find(ast_manager & m, unsigned num_args, expr * const * args, sort * range) const;
+    unsigned get_num_entries() const;
+    func_decl * get_entry(unsigned inx);
 };
 
 struct macro_decl {
@@ -66,18 +68,18 @@ struct macro_decl {
 
     macro_decl(unsigned arity, sort *const* domain, expr* body):
         m_domain(arity, domain), m_body(body) {}
-    
+
     void dec_ref(ast_manager& m) { m.dec_ref(m_body); }
-    
+
 };
 
 class macro_decls {
     vector<macro_decl>* m_decls;
-public:    
+public:
     macro_decls() { m_decls = 0; }
     void finalize(ast_manager& m);
     bool insert(ast_manager& m, unsigned arity, sort *const* domain, expr* body);
-    expr* find(unsigned arity, sort *const* domain) const;    
+    expr* find(unsigned arity, sort *const* domain) const;
     void erase_last(ast_manager& m);
     vector<macro_decl>::iterator begin() const { return m_decls->begin(); }
     vector<macro_decl>::iterator end() const { return m_decls->end(); }
@@ -158,11 +160,11 @@ public:
     enum status {
         UNSAT, SAT, UNKNOWN
     };
-    
+
     enum check_sat_state {
         css_unsat, css_sat, css_unknown, css_clear
     };
-    
+
     typedef std::pair<unsigned, expr*> macro;
 
     struct scoped_watch {
@@ -188,7 +190,7 @@ protected:
     bool                         m_ignore_check;      // used by the API to disable check-sat() commands when parsing SMT 2.0 files.
     bool                         m_processing_pareto; // used when re-entering check-sat for pareto front.
     bool                         m_exit_on_error;
-    
+
     static std::ostringstream    g_error_stream;
 
     ast_manager *                m_manager;
@@ -200,7 +202,7 @@ protected:
     check_logic                  m_check_logic;
     stream_ref                   m_regular;
     stream_ref                   m_diagnostic;
-    dictionary<cmd*>             m_cmds;    
+    dictionary<cmd*>             m_cmds;
     dictionary<builtin_decl>     m_builtin_decls;
     scoped_ptr_vector<builtin_decl> m_extra_builtin_decls; // make sure that dynamically allocated builtin_decls are deleted
     dictionary<object_ref*>      m_object_refs; // anything that can be named.
@@ -217,7 +219,7 @@ protected:
     svector<symbol>              m_macros_stack;
     ptr_vector<pdecl>            m_psort_inst_stack;
 
-    // 
+    //
     ptr_vector<pdecl>            m_aux_pdecls;
     ptr_vector<expr>             m_assertions;
     std::vector<std::string>     m_assertion_strings;
@@ -236,7 +238,7 @@ protected:
     svector<scope>               m_scopes;
     scoped_ptr<solver_factory>   m_solver_factory;
     scoped_ptr<solver_factory>   m_interpolating_solver_factory;
-    ref<solver>                  m_solver;    
+    ref<solver>                  m_solver;
     ref<check_sat_result>        m_check_sat_result;
     ref<opt_wrapper>             m_opt;
 
@@ -296,7 +298,7 @@ protected:
 
     bool contains_macro(symbol const& s) const;
     bool contains_macro(symbol const& s, func_decl* f) const;
-    bool contains_macro(symbol const& s, unsigned arity, sort *const* domain) const;    
+    bool contains_macro(symbol const& s, unsigned arity, sort *const* domain) const;
     void insert_macro(symbol const& s, unsigned arity, sort*const* domain, expr* t);
     void erase_macro(symbol const& s);
     bool macros_find(symbol const& s, unsigned n, expr*const* args, expr*& t) const;
@@ -304,7 +306,7 @@ protected:
 
 public:
     cmd_context(bool main_ctx = true, ast_manager * m = 0, symbol const & l = symbol::null);
-    ~cmd_context(); 
+    ~cmd_context();
     void set_cancel(bool f);
     context_params  & params() { return m_params; }
     solver_factory &get_solver_factory() { return *m_solver_factory; }
@@ -354,39 +356,40 @@ public:
     virtual ast_manager & get_ast_manager() { return m(); }
     pdecl_manager & pm() const { if (!m_pmanager) const_cast<cmd_context*>(this)->init_manager(); return *m_pmanager; }
     sexpr_manager & sm() const { if (!m_sexpr_manager) const_cast<cmd_context*>(this)->m_sexpr_manager = alloc(sexpr_manager); return *m_sexpr_manager; }
- 
+
     void set_solver_factory(solver_factory * s);
     void set_interpolating_solver_factory(solver_factory * s);
     void set_check_sat_result(check_sat_result * r) { m_check_sat_result = r; }
     check_sat_result * get_check_sat_result() const { return m_check_sat_result.get(); }
     check_sat_state cs_state() const;
+    void complete_model();
     void validate_model();
     void display_model(model_ref& mdl);
 
-    void register_plugin(symbol const & name, decl_plugin * p, bool install_names);    
+    void register_plugin(symbol const & name, decl_plugin * p, bool install_names);
     bool is_func_decl(symbol const & s) const;
     bool is_sort_decl(symbol const& s) const { return m_psort_decls.contains(s); }
     void insert(cmd * c);
-    void insert(symbol const & s, func_decl * f); 
+    void insert(symbol const & s, func_decl * f);
     void insert(func_decl * f) { insert(f->get_name(), f); }
     void insert(symbol const & s, psort_decl * p);
     void insert(psort_decl * p) { insert(p->get_name(), p); }
     void insert(symbol const & s, unsigned arity, sort *const* domain, expr * t);
     void insert(symbol const & s, object_ref *);
     void insert(tactic_cmd * c) { tactic_manager::insert(c); }
-    void insert(probe_info * p) { tactic_manager::insert(p); } 
-    void insert_user_tactic(symbol const & s, sexpr * d); 
+    void insert(probe_info * p) { tactic_manager::insert(p); }
+    void insert_user_tactic(symbol const & s, sexpr * d);
     void insert_aux_pdecl(pdecl * p);
     void insert_rec_fun(func_decl* f, expr_ref_vector const& binding, svector<symbol> const& ids, expr* e);
     func_decl * find_func_decl(symbol const & s) const;
-    func_decl * find_func_decl(symbol const & s, unsigned num_indices, unsigned const * indices, 
+    func_decl * find_func_decl(symbol const & s, unsigned num_indices, unsigned const * indices,
                                unsigned arity, sort * const * domain, sort * range) const;
     psort_decl * find_psort_decl(symbol const & s) const;
     cmd * find_cmd(symbol const & s) const;
     sexpr * find_user_tactic(symbol const & s) const;
     object_ref * find_object_ref(symbol const & s) const;
     void mk_const(symbol const & s, expr_ref & result) const;
-    void mk_app(symbol const & s, unsigned num_args, expr * const * args, unsigned num_indices, parameter const * indices, sort * range, 
+    void mk_app(symbol const & s, unsigned num_args, expr * const * args, unsigned num_indices, parameter const * indices, sort * range,
                 expr_ref & r) const;
     void erase_cmd(symbol const & s);
     void erase_func_decl(symbol const & s);
@@ -401,7 +404,7 @@ public:
     void reset_object_refs();
     void reset_user_tactics();
     void set_regular_stream(char const * name) { m_regular.set(name); }
-    void set_diagnostic_stream(char const * name); 
+    void set_diagnostic_stream(char const * name);
     virtual std::ostream & regular_stream() { return *m_regular; }
     virtual std::ostream & diagnostic_stream() { return *m_diagnostic; }
     char const * get_regular_stream_name() const { return m_regular.name(); }
@@ -429,7 +432,7 @@ public:
     // display the result produced by a check-sat or check-sat-using commands in the regular stream
     void display_sat_result(lbool r);
     // check if result produced by check-sat or check-sat-using matches the known status
-    void validate_check_sat_result(lbool r); 
+    void validate_check_sat_result(lbool r);
     unsigned num_scopes() const { return m_scopes.size(); }
 
     dictionary<macro_decls> const & get_macros() const { return m_macros; }
diff --git a/src/cmd_context/pdecl.cpp b/src/cmd_context/pdecl.cpp
index 983dbbc78..f255c8353 100644
--- a/src/cmd_context/pdecl.cpp
+++ b/src/cmd_context/pdecl.cpp
@@ -25,11 +25,11 @@ class psort_inst_cache {
     sort *                m_const;
     obj_map<sort, void *> m_map; // if m_num_params == 1 value is a sort, otherwise it is a reference to another inst_cache
 public:
-    psort_inst_cache(unsigned num_params):m_num_params(num_params), m_const(0) { 
+    psort_inst_cache(unsigned num_params):m_num_params(num_params), m_const(0) {
     }
 
     ~psort_inst_cache() { SASSERT(m_map.empty()); SASSERT(m_const == 0); }
-    
+
     void finalize(pdecl_manager & m) {
         if (m_num_params == 0) {
             SASSERT(m_map.empty());
@@ -85,7 +85,7 @@ public:
             curr = static_cast<psort_inst_cache*>(next);
         }
     }
-    
+
     sort * find(sort * const * s) const {
         if (m_num_params == 0)
             return m_const;
@@ -138,8 +138,8 @@ class psort_sort : public psort {
     friend class pdecl_manager;
     sort * m_sort;
     psort_sort(unsigned id, pdecl_manager & m, sort * s):psort(id, 0), m_sort(s) { m.m().inc_ref(m_sort); }
-    virtual void finalize(pdecl_manager & m) { 
-        m.m().dec_ref(m_sort); 
+    virtual void finalize(pdecl_manager & m) {
+        m.m().dec_ref(m_sort);
         psort::finalize(m);
     }
     virtual bool check_num_params(pdecl * other) const { return true; }
@@ -152,7 +152,7 @@ public:
     virtual char const * hcons_kind() const { return "psort_sort"; }
     virtual unsigned hcons_hash() const { return m_sort->get_id(); }
     virtual bool hcons_eq(psort const * other) const {
-        if (other->hcons_kind() != hcons_kind()) 
+        if (other->hcons_kind() != hcons_kind())
             return false;
         return m_sort == static_cast<psort_sort const *>(other)->m_sort;
     }
@@ -172,10 +172,10 @@ public:
     virtual char const * hcons_kind() const { return "psort_var"; }
     virtual unsigned hcons_hash() const { return hash_u_u(m_num_params, m_idx); }
     virtual bool hcons_eq(psort const * other) const {
-        if (other->hcons_kind() != hcons_kind()) 
+        if (other->hcons_kind() != hcons_kind())
             return false;
         return get_num_params() == other->get_num_params() && m_idx == static_cast<psort_var const *>(other)->m_idx;
-    }    
+    }
     virtual void display(std::ostream & out) const {
         out << "s_" << m_idx;
     }
@@ -197,7 +197,7 @@ class psort_app : public psort {
         DEBUG_CODE(if (num_args == num_params) { for (unsigned i = 0; i < num_params; i++) args[i]->check_num_params(this); });
     }
 
-    virtual void finalize(pdecl_manager & m) { 
+    virtual void finalize(pdecl_manager & m) {
         m.lazy_dec_ref(m_decl);
         m.lazy_dec_ref(m_args.size(), m_args.c_ptr());
         psort::finalize(m);
@@ -208,14 +208,14 @@ class psort_app : public psort {
     struct khasher {
         unsigned operator()(psort_app const * d) const { return d->m_decl->hash(); }
     };
-    
+
     struct chasher {
         unsigned operator()(psort_app const * d, unsigned idx) const { return d->m_args[idx]->hash(); }
     };
 
-    virtual sort * instantiate(pdecl_manager & m, sort * const * s) { 
+    virtual sort * instantiate(pdecl_manager & m, sort * const * s) {
         sort * r = find(s);
-        if (r) 
+        if (r)
             return r;
         sort_ref_buffer args_i(m.m());
         unsigned sz = m_args.size();
@@ -231,11 +231,11 @@ class psort_app : public psort {
 public:
     virtual ~psort_app() {}
     virtual char const * hcons_kind() const { return "psort_app"; }
-    virtual unsigned hcons_hash() const { 
+    virtual unsigned hcons_hash() const {
         return get_composite_hash<psort_app*, khasher, chasher>(const_cast<psort_app*>(this), m_args.size());
     }
     virtual bool hcons_eq(psort const * other) const {
-        if (other->hcons_kind() != hcons_kind()) 
+        if (other->hcons_kind() != hcons_kind())
             return false;
         if (get_num_params() != other->get_num_params())
             return false;
@@ -268,6 +268,7 @@ public:
 
 psort_decl::psort_decl(unsigned id, unsigned num_params, pdecl_manager & m, symbol const & n):
     pdecl(id, num_params),
+    m_psort_kind(PSORT_BASE),
     m_name(n),
     m_inst_cache(0) {
 }
@@ -295,7 +296,7 @@ sort * psort_decl::find(sort * const * s) {
 
 #if 0
 psort_dt_decl::psort_dt_decl(unsigned id, unsigned num_params, pdecl_manager& m, symbol const& n):
-    psort_decl(id, num_params, m, n) { 
+    psort_decl(id, num_params, m, n) {
 }
 
 void psort_dt_decl::finalize(pdecl_manager& m) {
@@ -314,9 +315,10 @@ void psort_dt_decl::display(std::ostream & out) const {
 #endif
 
 
-psort_user_decl::psort_user_decl(unsigned id, unsigned num_params, pdecl_manager & m, symbol const & n, psort * p):
+psort_user_decl::psort_user_decl(unsigned id, unsigned num_params, pdecl_manager & m, symbol const & n, psort * p) :
     psort_decl(id, num_params, m, n),
     m_def(p) {
+    m_psort_kind = PSORT_USER;
     m.inc_ref(p);
     SASSERT(p == 0 || num_params == p->get_num_params());
 }
@@ -369,6 +371,7 @@ psort_builtin_decl::psort_builtin_decl(unsigned id, pdecl_manager & m, symbol co
     psort_decl(id, PSORT_DECL_VAR_PARAMS, m, n),
     m_fid(fid),
     m_kind(k) {
+    m_psort_kind = PSORT_BUILTIN;
 }
 
 sort * psort_builtin_decl::instantiate(pdecl_manager & m, unsigned n, sort * const * s) {
@@ -417,16 +420,16 @@ void ptype::display(std::ostream & out, pdatatype_decl const * const * dts) cons
 
 paccessor_decl::paccessor_decl(unsigned id, unsigned num_params, pdecl_manager & m, symbol const & n, ptype const & r):
     pdecl(id, num_params),
-    m_name(n), 
+    m_name(n),
     m_type(r) {
     if (m_type.kind() == PTR_PSORT) {
         m.inc_ref(r.get_psort());
     }
 }
 
-void paccessor_decl::finalize(pdecl_manager & m) { 
+void paccessor_decl::finalize(pdecl_manager & m) {
     if (m_type.kind() == PTR_PSORT) {
-        m.lazy_dec_ref(m_type.get_psort());	
+        m.lazy_dec_ref(m_type.get_psort());
     }
 }
 
@@ -439,7 +442,7 @@ bool paccessor_decl::has_missing_refs(symbol & missing) const {
 }
 
 bool paccessor_decl::fix_missing_refs(dictionary<int> const & symbol2idx, symbol & missing) {
-    TRACE("fix_missing_refs", tout << "m_type.kind(): " << m_type.kind() << "\n"; 
+    TRACE("fix_missing_refs", tout << "m_type.kind(): " << m_type.kind() << "\n";
           if (m_type.kind() == PTR_MISSING_REF) tout << m_type.get_missing_ref() << "\n";);
     if (m_type.kind() != PTR_MISSING_REF)
         return true;
@@ -470,7 +473,7 @@ void paccessor_decl::display(std::ostream & out, pdatatype_decl const * const *
     out << ")";
 }
 
-pconstructor_decl::pconstructor_decl(unsigned id, unsigned num_params, pdecl_manager & m, 
+pconstructor_decl::pconstructor_decl(unsigned id, unsigned num_params, pdecl_manager & m,
                                      symbol const & n, symbol const & r, unsigned num_accessors, paccessor_decl * const * accessors):
     pdecl(id, num_params),
     m_name(n),
@@ -508,7 +511,7 @@ constructor_decl * pconstructor_decl::instantiate_decl(pdecl_manager & m, sort *
     ptr_buffer<accessor_decl> as;
     ptr_vector<paccessor_decl>::iterator it  = m_accessors.begin();
     ptr_vector<paccessor_decl>::iterator end = m_accessors.end();
-    for (; it != end; ++it) 
+    for (; it != end; ++it)
         as.push_back((*it)->instantiate_decl(m, s));
     return mk_constructor_decl(m_name, m_recogniser_name, as.size(), as.c_ptr());
 }
@@ -524,7 +527,7 @@ void pconstructor_decl::display(std::ostream & out, pdatatype_decl const * const
     out << ")";
 }
 
-pdatatype_decl::pdatatype_decl(unsigned id, unsigned num_params, pdecl_manager & m, 
+pdatatype_decl::pdatatype_decl(unsigned id, unsigned num_params, pdecl_manager & m,
                                symbol const & n, unsigned num_constructors, pconstructor_decl * const * constructors):
     psort_decl(id, num_params, m, n),
     m_constructors(num_constructors, constructors),
@@ -641,7 +644,7 @@ void pdatatype_decl::display(std::ostream & out) const {
     out << ")";
 }
 
-pdatatypes_decl::pdatatypes_decl(unsigned id, unsigned num_params, pdecl_manager & m, 
+pdatatypes_decl::pdatatypes_decl(unsigned id, unsigned num_params, pdecl_manager & m,
                                  unsigned num_datatypes, pdatatype_decl * const * dts):
     pdecl(id, num_params),
     m_datatypes(num_datatypes, dts) {
@@ -714,22 +717,22 @@ struct pdecl_manager::sort_info {
 
 struct pdecl_manager::app_sort_info : public pdecl_manager::sort_info {
     ptr_vector<sort> m_args;
-    
+
     app_sort_info(pdecl_manager & m, psort_decl * d, unsigned n, sort * const * s):
         sort_info(m, d),
         m_args(n, s) {
         m.m().inc_array_ref(n, s);
     }
-    
+
     virtual ~app_sort_info() {}
-    
+
     virtual unsigned obj_size() const { return sizeof(app_sort_info); }
-    
+
     virtual void finalize(pdecl_manager & m) {
         sort_info::finalize(m);
         m.m().dec_array_ref(m_args.size(), m_args.c_ptr());
     }
-    
+
     virtual void display(std::ostream & out, pdecl_manager const & m) const {
         if (m_args.empty()) {
             out << m_decl->get_name();
@@ -743,7 +746,7 @@ struct pdecl_manager::app_sort_info : public pdecl_manager::sort_info {
             out << ")";
         }
     }
-    
+
     virtual format * pp(pdecl_manager const & m) const {
         if (m_args.empty()) {
             return mk_string(m.m(), m_decl->get_name().str().c_str());
@@ -755,7 +758,7 @@ struct pdecl_manager::app_sort_info : public pdecl_manager::sort_info {
             return mk_seq1(m.m(), b.begin(), b.end(), f2f(), m_decl->get_name().str().c_str());
         }
     }
-}; 
+};
 
 struct pdecl_manager::indexed_sort_info : public pdecl_manager::sort_info {
     svector<unsigned> m_indices;
@@ -781,7 +784,7 @@ struct pdecl_manager::indexed_sort_info : public pdecl_manager::sort_info {
             out << ")";
         }
     }
-    
+
     virtual format * pp(pdecl_manager const & m) const {
         if (m_indices.empty()) {
             return mk_string(m.m(), m_decl->get_name().str().c_str());
@@ -801,7 +804,7 @@ void pdecl_manager::init_list() {
     psort * v   = mk_psort_var(1, 0);
     ptype T(v);
     ptype ListT(0);
-    paccessor_decl * as[2]    = { mk_paccessor_decl(1, symbol("head"), T), 
+    paccessor_decl * as[2]    = { mk_paccessor_decl(1, symbol("head"), T),
                                   mk_paccessor_decl(1, symbol("tail"), ListT) };
     pconstructor_decl * cs[2] = { mk_pconstructor_decl(1, symbol("nil"), symbol("is-nil"), 0, 0),
                                   mk_pconstructor_decl(1, symbol("insert"), symbol("is-insert"), 2, as) };
@@ -851,8 +854,8 @@ psort * pdecl_manager::mk_psort_var(unsigned num_params, unsigned vidx) {
 paccessor_decl * pdecl_manager::mk_paccessor_decl(unsigned num_params, symbol const & s, ptype const & p) {
     return new (a().allocate(sizeof(paccessor_decl))) paccessor_decl(m_id_gen.mk(), num_params, *this, s, p);
 }
- 
-pconstructor_decl * pdecl_manager::mk_pconstructor_decl(unsigned num_params, 
+
+pconstructor_decl * pdecl_manager::mk_pconstructor_decl(unsigned num_params,
                                                         symbol const & s, symbol const & r, unsigned num, paccessor_decl * const * as) {
     return new (a().allocate(sizeof(pconstructor_decl))) pconstructor_decl(m_id_gen.mk(), num_params, *this,
                                                                            s, r, num, as);
@@ -901,9 +904,9 @@ sort * pdecl_manager::instantiate(psort * p, unsigned num, sort * const * args)
 
 
 void pdecl_manager::del_decl_core(pdecl * p) {
-    TRACE("pdecl_manager", 
+    TRACE("pdecl_manager",
           tout << "del_decl_core:\n";
-          if (p->is_psort()) static_cast<psort*>(p)->display(tout); 
+          if (p->is_psort()) static_cast<psort*>(p)->display(tout);
           else static_cast<psort_decl*>(p)->display(tout);
           tout << "\n";);
     size_t sz = p->obj_size();
@@ -921,7 +924,7 @@ void pdecl_manager::del_decl(pdecl * p) {
         else
             m_table.erase(_p);
     }
-    del_decl_core(p); 
+    del_decl_core(p);
 }
 
 void pdecl_manager::del_decls() {
diff --git a/src/cmd_context/pdecl.h b/src/cmd_context/pdecl.h
index 2dfbb93ae..a32a42413 100644
--- a/src/cmd_context/pdecl.h
+++ b/src/cmd_context/pdecl.h
@@ -86,10 +86,13 @@ typedef ptr_hashtable<psort, psort_hash_proc, psort_eq_proc> psort_table;
 
 #define PSORT_DECL_VAR_PARAMS UINT_MAX
 
+typedef enum { PSORT_BASE = 0, PSORT_USER, PSORT_BUILTIN } psort_decl_kind;
+
 class psort_decl : public pdecl {
 protected:
     friend class pdecl_manager;
     symbol                        m_name;
+    psort_decl_kind               m_psort_kind;
     psort_inst_cache *            m_inst_cache;
     void cache(pdecl_manager & m, sort * const * s, sort * r);
     sort * find(sort * const * s);
@@ -105,6 +108,8 @@ public:
     bool has_var_params() const { return m_num_params == PSORT_DECL_VAR_PARAMS; }
     symbol const & get_name() const { return m_name; }
     virtual void reset_cache(pdecl_manager& m);
+    bool is_user_decl() const { return m_psort_kind == PSORT_USER; }
+    bool is_builtin_decl() const { return m_psort_kind == PSORT_BUILTIN; }
 };
 
 class psort_user_decl : public psort_decl {
@@ -209,7 +214,7 @@ class pconstructor_decl : public pdecl {
     symbol                     m_name;
     symbol                     m_recogniser_name;
     ptr_vector<paccessor_decl> m_accessors;
-    pconstructor_decl(unsigned id, unsigned num_params, pdecl_manager & m, 
+    pconstructor_decl(unsigned id, unsigned num_params, pdecl_manager & m,
                       symbol const & n, symbol const & r, unsigned num_accessors, paccessor_decl * const * accessors);
     virtual void finalize(pdecl_manager & m);
     virtual size_t obj_size() const { return sizeof(pconstructor_decl); }
@@ -229,7 +234,7 @@ class pdatatype_decl : public psort_decl {
     friend class pdatatypes_decl;
     ptr_vector<pconstructor_decl> m_constructors;
     pdatatypes_decl *             m_parent;
-    pdatatype_decl(unsigned id, unsigned num_params, pdecl_manager & m, symbol const & n, 
+    pdatatype_decl(unsigned id, unsigned num_params, pdecl_manager & m, symbol const & n,
                    unsigned num_constructors, pconstructor_decl * const * constructors);
     virtual void finalize(pdecl_manager & m);
     virtual size_t obj_size() const { return sizeof(pdatatype_decl); }
@@ -282,7 +287,7 @@ class pdecl_manager {
     struct indexed_sort_info;
 
     obj_map<sort, sort_info *>   m_sort2info; // for pretty printing sorts
-    
+
     void init_list();
     void del_decl_core(pdecl * p);
     void del_decl(pdecl * p);
@@ -296,7 +301,7 @@ public:
     small_object_allocator & a() const { return m_allocator; }
     family_id get_datatype_fid() const { return m_datatype_fid; }
     void set_new_datatype_eh(new_datatype_eh * eh) { m_new_dt_eh = eh; }
-    psort * mk_psort_cnst(sort * s);    
+    psort * mk_psort_cnst(sort * s);
     psort * mk_psort_var(unsigned num_params, unsigned vidx);
     psort * mk_psort_app(unsigned num_params, psort_decl * d, unsigned num_args, psort * const * args);
     psort * mk_psort_app(psort_decl * d);
diff --git a/src/model/model_params.pyg b/src/model/model_params.pyg
index 14e83952c..58337e863 100644
--- a/src/model/model_params.pyg
+++ b/src/model/model_params.pyg
@@ -1,8 +1,9 @@
-def_module_params('model', 
+def_module_params('model',
                   export=True,
                   params=(('partial', BOOL, False, 'enable/disable partial function interpretations'),
                           ('v1', BOOL, False, 'use Z3 version 1.x pretty printer'),
                           ('v2', BOOL, False, 'use Z3 version 2.x (x <= 16) pretty printer'),
                           ('compact', BOOL, False, 'try to compact function graph (i.e., function interpretations that are lookup tables)'),
+                          ('completion', BOOL, False, 'enable/disable model completion'),
                           ))