diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h
index 291a0f0d8..6ebbbbf0d 100644
--- a/src/smt/theory_arith_core.h
+++ b/src/smt/theory_arith_core.h
@@ -721,6 +721,11 @@ namespace smt {
             return internalize_div(n);
         else if (m_util.is_idiv(n))
             return internalize_idiv(n);
+        else if (is_app_of(n, get_id(), OP_IDIV_0) || is_app_of(n, get_id(), OP_DIV_0)) {
+            ctx.internalize(n->get_arg(0), false);
+            enode * e = mk_enode(n);
+            return mk_var(e);
+        }
         else if (m_util.is_mod(n)) 
             return internalize_mod(n);
         else if (m_util.is_rem(n))