diff --git a/src/ast/arith_decl_plugin.h b/src/ast/arith_decl_plugin.h
index 5d6f102f1..45f04fd58 100644
--- a/src/ast/arith_decl_plugin.h
+++ b/src/ast/arith_decl_plugin.h
@@ -287,6 +287,8 @@ public:
     bool is_idiv0(expr const * n) const { return is_app_of(n, m_afid, OP_IDIV0); }
     bool is_mod(expr const * n) const { return is_app_of(n, m_afid, OP_MOD); }
     bool is_rem(expr const * n) const { return is_app_of(n, m_afid, OP_REM); }
+    bool is_mod0(expr const * n) const { return is_app_of(n, m_afid, OP_MOD0); }
+    bool is_rem0(expr const * n) const { return is_app_of(n, m_afid, OP_REM0); }
     bool is_to_real(expr const * n) const { return is_app_of(n, m_afid, OP_TO_REAL); }
     bool is_to_int(expr const * n) const { return is_app_of(n, m_afid, OP_TO_INT); }
     bool is_is_int(expr const * n) const { return is_app_of(n, m_afid, OP_IS_INT); }
diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h
index 59b7a6a0e..08c060f89 100644
--- a/src/smt/theory_arith_core.h
+++ b/src/smt/theory_arith_core.h
@@ -848,7 +848,9 @@ namespace smt {
             return mk_var(e);
         }
         if (m_util.get_family_id() == n->get_family_id()) {
-            found_unsupported_op(n);
+            if (!m_util.is_div0(n) && !m_util.is_mod0(n) && !m_util.is_idiv0(n) && !m_util.is_rem0(n)) {
+                found_unsupported_op(n);
+            }
             if (ctx.e_internalized(n))
                 return expr2var(n);
             for (unsigned i = 0; i < n->get_num_args(); ++i) {