diff --git a/src/smt/proto_model/proto_model.cpp b/src/smt/proto_model/proto_model.cpp
index 688ded834..493948f32 100644
--- a/src/smt/proto_model/proto_model.cpp
+++ b/src/smt/proto_model/proto_model.cpp
@@ -342,10 +342,16 @@ void proto_model::compress() {
    \brief Complete the interpretation fi of f if it is partial.
    If f does not have an interpretation in the given model, then this is a noop.
 */
-void proto_model::complete_partial_func(func_decl * f) {
+void proto_model::complete_partial_func(func_decl * f, bool use_fresh) {
     func_interp * fi = get_func_interp(f);
     if (fi && fi->is_partial()) {
-        expr * else_value = fi->get_max_occ_result();
+        expr * else_value;
+        if (use_fresh) {
+            else_value = get_fresh_value(f->get_range());
+        }
+        else {
+            else_value = fi->get_max_occ_result();
+        }
         if (else_value == nullptr)
             else_value = get_some_value(f->get_range());
         fi->set_else(else_value);
@@ -355,14 +361,14 @@ void proto_model::complete_partial_func(func_decl * f) {
 /**
    \brief Set the (else) field of function interpretations...
 */
-void proto_model::complete_partial_funcs() {
+void proto_model::complete_partial_funcs(bool use_fresh) {
     if (m_model_partial)
         return;
 
     // m_func_decls may be "expanded" when we invoke get_some_value.
     // So, we must not use iterators to traverse it.
-    for (unsigned i = 0; i < m_func_decls.size(); i++) {
-        complete_partial_func(m_func_decls[i]);
+    for (func_decl* f : m_func_decls) {
+        complete_partial_func(f, use_fresh);
     }
 }
 
diff --git a/src/smt/proto_model/proto_model.h b/src/smt/proto_model/proto_model.h
index d92d459e4..04e3a90fe 100644
--- a/src/smt/proto_model/proto_model.h
+++ b/src/smt/proto_model/proto_model.h
@@ -100,8 +100,8 @@ public:
     //
     // Complete partial function interps
     //
-    void complete_partial_func(func_decl * f);
-    void complete_partial_funcs();
+    void complete_partial_func(func_decl * f, bool use_fresh);
+    void complete_partial_funcs(bool use_fresh);
 
     //
     // Create final model object. 
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index b2adfff8d..48033f9b5 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -4364,7 +4364,7 @@ namespace smt {
             m_proto_model = m_model_generator->mk_model();
             m_qmanager->adjust_model(m_proto_model.get());
             TRACE("mbqi_bug", tout << "before complete_partial_funcs:\n"; model_pp(tout, *m_proto_model););
-            m_proto_model->complete_partial_funcs();
+            m_proto_model->complete_partial_funcs(false);
             TRACE("mbqi_bug", tout << "before cleanup:\n"; model_pp(tout, *m_proto_model););
             m_proto_model->cleanup();
             if (m_fparams.m_model_compact)
diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp
index 4307d3fdf..73f85faf6 100644
--- a/src/smt/smt_model_finder.cpp
+++ b/src/smt/smt_model_finder.cpp
@@ -1028,7 +1028,7 @@ namespace smt {
             void complete_partial_funcs(func_decl_set const & partial_funcs) {
                 for (func_decl * f : partial_funcs) {
                     // Complete the current interpretation
-                    m_model->complete_partial_func(f);
+                    m_model->complete_partial_func(f, true);
 
                     unsigned arity   = f->get_arity();
                     func_interp * fi = m_model->get_func_interp(f);