diff --git a/src/sat/smt/q_mbi.cpp b/src/sat/smt/q_mbi.cpp
index 582911222..39218d612 100644
--- a/src/sat/smt/q_mbi.cpp
+++ b/src/sat/smt/q_mbi.cpp
@@ -114,6 +114,8 @@ namespace q {
                 args.push_back(replace_model_value(arg));
             return expr_ref(m.mk_app(to_app(e)->get_decl(), args), m);
         }
+        if (m.is_model_value(e))
+            return expr_ref(m.mk_model_value(0, e->get_sort()), m);
         return expr_ref(e, m);
     }