diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index 1e053fe1b3c..97cc4d1a694 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -4221,7 +4221,7 @@ bool seq_rewriter::reduce_eq_empty(expr* l, expr* r, expr_ref& result) {
         expr_ref_vector fmls(m());
         fmls.push_back(m_autil.mk_lt(offset, m_autil.mk_int(0)));
         fmls.push_back(m().mk_eq(s, l));
-        fmls.push_back(m_autil.mk_lt(len, m_autil.mk_int(0)));
+        fmls.push_back(m_autil.mk_le(len, m_autil.mk_int(0)));
         fmls.push_back(m_autil.mk_le(len_s, offset));
         result = m().mk_or(fmls);
         return true;
diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h
index 88696629a28..bbbade83ff5 100644
--- a/src/smt/theory_arith_core.h
+++ b/src/smt/theory_arith_core.h
@@ -1251,6 +1251,7 @@ namespace smt {
         expr * rhs2;
         if (m_util.is_to_real(rhs, rhs2) && is_app(rhs2)) { rhs = to_app(rhs2); }
         if (!m_util.is_numeral(rhs)) {
+            SASSERT(false);
             throw default_exception("malformed atomic constraint");
         }
         theory_var v   = internalize_term_core(lhs);