diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index 22c82c0c9..44503c40e 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -1674,6 +1674,7 @@ void cmd_context::display_model(model_ref& mdl) {
     if (mdl) {
         if (m_mc0) (*m_mc0)(mdl);
         if (m_params.m_model_compress) mdl->compress();
+        add_declared_functions(*mdl);
         model_params p;
         if (p.v1() || p.v2()) {
             std::ostringstream buffer;
@@ -1687,6 +1688,23 @@ void cmd_context::display_model(model_ref& mdl) {
     }
 }
 
+void cmd_context::add_declared_functions(model& mdl) {
+    for (auto const& kv : m_func_decls) {
+        func_decl* f = kv.m_value.first();
+        if (!mdl.has_interpretation(f)) {
+            expr* val = mdl.get_some_value(f->get_range());
+            if (f->get_arity() == 0) {
+                mdl.register_decl(f, val);
+                }
+            else {
+                func_interp* fi = alloc(func_interp, m(), f->get_arity());
+                fi->set_else(val);
+                mdl.register_decl(f, fi);
+            }
+        }
+    }
+}
+
 void cmd_context::display_sat_result(lbool r) {
     switch (r) {
     case l_true:
diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h
index 55ea65cb5..384cfb04e 100644
--- a/src/cmd_context/cmd_context.h
+++ b/src/cmd_context/cmd_context.h
@@ -273,6 +273,7 @@ protected:
     void init_external_manager();
     void reset_cmds();
     void finalize_cmds();
+    void add_declared_functions(model& mdl);
 
     void restore_func_decls(unsigned old_sz);
     void restore_psort_decls(unsigned old_sz);