diff --git a/src/ast/arith_decl_plugin.cpp b/src/ast/arith_decl_plugin.cpp
index fa169316b..01b671c99 100644
--- a/src/ast/arith_decl_plugin.cpp
+++ b/src/ast/arith_decl_plugin.cpp
@@ -81,8 +81,9 @@ app * arith_decl_plugin::mk_numeral(algebraic_numbers::anum const & val, bool is
         return mk_numeral(rval, is_int);
     }
     else {
-        if (is_int)
+        if (is_int) {            
             m_manager->raise_exception("invalid irrational value passed as an integer");
+        }
         unsigned idx = aw().mk_id(val);
         parameter p(idx, true);
         SASSERT(p.is_external());
diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h
index 6b8abcdbc..e10395d31 100644
--- a/src/smt/theory_arith_core.h
+++ b/src/smt/theory_arith_core.h
@@ -1224,7 +1224,9 @@ namespace smt {
         app * rhs      = to_app(n->get_arg(1));
         expr * rhs2;
         if (m_util.is_to_real(rhs, rhs2) && is_app(rhs2)) { rhs = to_app(rhs2); }
-        SASSERT(m_util.is_numeral(rhs));
+        if (!m_util.is_numeral(rhs)) {
+            throw default_exception("malformed atomic constraint");
+        }
         theory_var v   = internalize_term_core(lhs);
         if (v == null_theory_var) {
             TRACE("arith_internalize", tout << "failed to internalize: #" << n->get_id() << "\n";);