diff --git a/src/ast/arith_decl_plugin.h b/src/ast/arith_decl_plugin.h
index beb227c33..6d6da9ed5 100644
--- a/src/ast/arith_decl_plugin.h
+++ b/src/ast/arith_decl_plugin.h
@@ -275,7 +275,9 @@ public:
     bool is_uminus(expr const * n) const { return is_app_of(n, m_afid, OP_UMINUS); }
     bool is_mul(expr const * n) const { return is_app_of(n, m_afid, OP_MUL); }
     bool is_div(expr const * n) const { return is_app_of(n, m_afid, OP_DIV); }
+    bool is_div0(expr const * n) const { return is_app_of(n, m_afid, OP_DIV_0); }
     bool is_idiv(expr const * n) const { return is_app_of(n, m_afid, OP_IDIV); }
+    bool is_idiv0(expr const * n) const { return is_app_of(n, m_afid, OP_IDIV_0); }
     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_to_real(expr const * n) const { return is_app_of(n, m_afid, OP_TO_REAL); }
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 2bd4844e8..9e4f544c1 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -292,6 +292,9 @@ namespace smt {
         }
 
         void found_not_handled(expr* n) {
+            if (a.is_div0(n)) {
+                return;
+            }
             m_not_handled = n;
             if (is_app(n) && is_underspecified(to_app(n))) {
                 m_underspecified.push_back(to_app(n));