diff --git a/src/ast/arith_decl_plugin.cpp b/src/ast/arith_decl_plugin.cpp
index a1d067a32..ba2b4b4a7 100644
--- a/src/ast/arith_decl_plugin.cpp
+++ b/src/ast/arith_decl_plugin.cpp
@@ -801,6 +801,29 @@ expr_ref arith_util::mk_add_simplify(unsigned sz, expr* const* args) {
     return result;
 }
 
+bool arith_util::is_considered_partially_interpreted(func_decl* f, unsigned n, expr* const* args, func_decl_ref& f_out) {
+    if (is_decl_of(f, arith_family_id, OP_DIV) && n == 2 && !is_numeral(args[1])) {
+        f_out = mk_div0();
+        return true;
+    }
+    if (is_decl_of(f, arith_family_id, OP_IDIV) && n == 2 && !is_numeral(args[1])) {
+        sort* rs[2] = { mk_int(), mk_int() };
+        f_out = m_manager.mk_func_decl(arith_family_id, OP_IDIV0, 0, nullptr, 2, rs, mk_int());
+        return true;
+    }
+    if (is_decl_of(f, arith_family_id, OP_MOD) && n == 2 && !is_numeral(args[1])) {
+        sort* rs[2] = { mk_int(), mk_int() };
+        f_out = m_manager.mk_func_decl(arith_family_id, OP_MOD0, 0, nullptr, 2, rs, mk_int());
+        return true;
+    }
+    if (is_decl_of(f, arith_family_id, OP_REM) && n == 2 && !is_numeral(args[1])) {
+        sort* rs[2] = { mk_int(), mk_int() };
+        f_out = m_manager.mk_func_decl(arith_family_id, OP_MOD0, 0, nullptr, 2, rs, mk_int());
+        return true;
+    }
+    return false;
+}
+
 bool arith_util::is_considered_uninterpreted(func_decl* f, unsigned n, expr* const* args, func_decl_ref& f_out) {
     rational r;
     if (is_decl_of(f, arith_family_id, OP_DIV) && n == 2 && is_numeral(args[1], r) && r.is_zero()) {
diff --git a/src/ast/arith_decl_plugin.h b/src/ast/arith_decl_plugin.h
index 5dbf3e8cf..fa359a9a7 100644
--- a/src/ast/arith_decl_plugin.h
+++ b/src/ast/arith_decl_plugin.h
@@ -517,6 +517,8 @@ public:
 
     bool is_considered_uninterpreted(func_decl* f, unsigned n, expr* const* args, func_decl_ref& f_out);
 
+    bool is_considered_partially_interpreted(func_decl* f, unsigned n, expr* const* args, func_decl_ref& f_out);
+
     bool is_underspecified(expr* e) const;
 
     bool is_bounded(expr* e) const;
diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp
index 0c2a09e78..125380930 100644
--- a/src/model/model_evaluator.cpp
+++ b/src/model/model_evaluator.cpp
@@ -421,6 +421,15 @@ struct evaluator_cfg : public default_rewriter_cfg {
                 return BR_DONE;
             }
         }
+        else if (!fi && m_au.is_considered_partially_interpreted(f, num, args, f_ui)) {
+            fi = m_model.get_func_interp(f_ui);
+            if (fi) {
+                var_subst vs(m, false);
+                result = vs(fi->get_interp(), num, args);
+                result = m.mk_ite(m.mk_eq(m_au.mk_real(rational(0)), args[1]), result, m.mk_app(f, num, args));
+                return BR_DONE;
+            }
+        }
         else if (!fi && m_fpau.is_considered_uninterpreted(f, num, args)) {
             result = m.get_some_value(f->get_range());
             return BR_DONE;