diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp
index 1f2e9e2e9..4dfd69ddd 100644
--- a/src/ast/rewriter/arith_rewriter.cpp
+++ b/src/ast/rewriter/arith_rewriter.cpp
@@ -681,8 +681,6 @@ br_status arith_rewriter::mk_div_core(expr * arg1, expr * arg2, expr_ref & resul
         SASSERT(!is_int);
         if (v2.is_zero()) {
             return BR_FAILED;
-            //result = m_util.mk_div0(arg1);
-            //return BR_REWRITE1;
         }
         else if (m_util.is_numeral(arg1, v1, is_int)) {
             result = m_util.mk_numeral(v1/v2, false);
@@ -735,10 +733,6 @@ br_status arith_rewriter::mk_idiv_core(expr * arg1, expr * arg2, expr_ref & resu
         result = m_util.mk_numeral(div(v1, v2), is_int);
         return BR_DONE;
     }
-    if (m_util.is_numeral(arg2, v2, is_int) && v2.is_zero()) {
-        //result = m_util.mk_idiv0(arg1);
-        //return BR_REWRITE1;
-    }
     return BR_FAILED;
 }
 
diff --git a/src/ast/simplifier/arith_simplifier_plugin.cpp b/src/ast/simplifier/arith_simplifier_plugin.cpp
index 8410ce143..bfe72b232 100644
--- a/src/ast/simplifier/arith_simplifier_plugin.cpp
+++ b/src/ast/simplifier/arith_simplifier_plugin.cpp
@@ -405,8 +405,6 @@ bool arith_simplifier_plugin::reduce(func_decl * f, unsigned num_args, expr * co
     case OP_POWER:                    return false;
     case OP_ABS:      SASSERT(num_args == 1); mk_abs(args[0], result); break;
     case OP_IRRATIONAL_ALGEBRAIC_NUM: return false;
-    case OP_DIV_0: return false;
-    case OP_IDIV_0: return false;
     default:
         return false;
     }
diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h
index 13aba9686..aa512a2be 100644
--- a/src/smt/theory_arith_core.h
+++ b/src/smt/theory_arith_core.h
@@ -407,7 +407,8 @@ namespace smt {
 
     template<typename Ext>
     theory_var theory_arith<Ext>::internalize_idiv(app * n) {
-        found_underspecified_op(n);
+        rational r;
+        if (!m_util.is_numeral(n->get_arg(1), r) || r.is_zero()) found_underspecified_op(n);
         theory_var s      = mk_binary_op(n);
         context & ctx     = get_context();
         app * mod         = m_util.mk_mod(n->get_arg(0), n->get_arg(1));
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index dd044b78a..a09005b7e 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -377,7 +377,12 @@ namespace smt {
                 }
                 else if (is_app(n) && a.get_family_id() == to_app(n)->get_family_id()) {
                     app* t = to_app(n);
-                    found_not_handled(n);
+                    if (a.is_div(n, n1, n2) && is_numeral(n2, r)) {
+                        // skip
+                    }
+                    else {
+                        found_not_handled(n);
+                    }
                     internalize_args(t);
                     mk_enode(t);
                     theory_var v = mk_var(n);