diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index b6f678fea..c8e58cc14 100644
--- a/src/ast/ast.cpp
+++ b/src/ast/ast.cpp
@@ -2284,6 +2284,7 @@ void ast_manager::check_args(func_decl* f, unsigned n, expr* const* es) {
                    << " for function " << mk_pp(f,*this)
                    << " supplied sort is "
                    << mk_pp(actual_sort, *this);
+            SASSERT(false);
             throw ast_exception(buffer.str());
         }
     }
diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp
index 66d828b94..b1614bc8a 100644
--- a/src/parsers/smt2/smt2parser.cpp
+++ b/src/parsers/smt2/smt2parser.cpp
@@ -2034,7 +2034,8 @@ namespace smt2 {
             process_last_symbol(fr);
             TRACE("consume_attributes", tout << "pop_attr_expr_frame, expr_stack.size(): " << expr_stack().size() << "\n";);
             // the resultant expression is already on the top of the stack.
-            SASSERT(expr_stack().size() == fr->m_expr_spos + 1);
+            if (expr_stack().size() != fr->m_expr_spos + 1)
+                throw parser_exception("invalid expression");
             m_stack.deallocate(fr);
             m_num_expr_frames--;
         }
diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h
index afeb9dd99..41bb3753e 100644
--- a/src/smt/theory_arith.h
+++ b/src/smt/theory_arith.h
@@ -1000,7 +1000,7 @@ namespace smt {
         bool is_mixed_real_integer(row const & r) const;
         bool is_integer(row const & r) const;
         typedef std::pair<rational, expr *> coeff_expr; 
-        void get_polynomial_info(sbuffer<coeff_expr> const & p, sbuffer<var_num_occs> & vars);
+        bool get_polynomial_info(sbuffer<coeff_expr> const & p, sbuffer<var_num_occs> & vars);
         expr * p2expr(sbuffer<coeff_expr> & p);
         expr * power(expr * var, unsigned power);
         expr * mk_nary_mul(unsigned sz, expr * const * args, bool is_int);
diff --git a/src/smt/theory_arith_nl.h b/src/smt/theory_arith_nl.h
index 50ba60d06..b009380f0 100644
--- a/src/smt/theory_arith_nl.h
+++ b/src/smt/theory_arith_nl.h
@@ -1209,7 +1209,7 @@ void theory_arith<Ext>::display_coeff_exprs(std::ostream & out, sbuffer<coeff_ex
    occurrences is also stored.
 */
 template<typename Ext>
-void theory_arith<Ext>::get_polynomial_info(sbuffer<coeff_expr> const & p, sbuffer<var_num_occs> & varinfo) {
+bool theory_arith<Ext>::get_polynomial_info(sbuffer<coeff_expr> const & p, sbuffer<var_num_occs> & varinfo) {
     context & ctx = get_context();
     varinfo.reset();
     m_var2num_occs.reset();
@@ -1222,10 +1222,8 @@ void theory_arith<Ext>::get_polynomial_info(sbuffer<coeff_expr> const & p, sbuff
         m_var2num_occs.insert(VAR, occs);                               \
     }
 
-    typename sbuffer<coeff_expr>::const_iterator it  = p.begin();
-    typename sbuffer<coeff_expr>::const_iterator end = p.end();
-    for (; it != end; ++it) {
-        expr * m = it->second;
+    for (auto const& ce : p) {
+        expr * m = ce.second;
         if (is_pure_monomial(m)) {
             unsigned num_vars = get_num_vars_in_monomial(m);
             for (unsigned i = 0; i < num_vars; i++) {
@@ -1242,6 +1240,7 @@ void theory_arith<Ext>::get_polynomial_info(sbuffer<coeff_expr> const & p, sbuff
         else {
             TRACE("non_linear", tout << mk_pp(m, get_manager()) << "\n";);
             UNREACHABLE();
+            return false;
         }
     }
 
@@ -1250,6 +1249,7 @@ void theory_arith<Ext>::get_polynomial_info(sbuffer<coeff_expr> const & p, sbuff
         if (vn.m_value > 1)
             varinfo.push_back(var_num_occs(vn.m_key, vn.m_value));
     }
+    return true;
 }
 
 /**
@@ -1519,7 +1519,8 @@ expr * theory_arith<Ext>::cross_nested(sbuffer<coeff_expr> & p, expr * var) {
     TRACE("non_linear", tout << "p.size: " << p.size() << "\n";);
     if (var == nullptr) {
         sbuffer<var_num_occs> varinfo;
-        get_polynomial_info(p, varinfo);
+        if (!get_polynomial_info(p, varinfo))
+            return nullptr;
         if (varinfo.empty())
             return p2expr(p);
         sbuffer<var_num_occs>::const_iterator it  = varinfo.begin();
@@ -1608,7 +1609,8 @@ expr * theory_arith<Ext>::cross_nested(sbuffer<coeff_expr> & p, expr * var) {
 template<typename Ext>
 bool theory_arith<Ext>::is_cross_nested_consistent(sbuffer<coeff_expr> & p) {
     sbuffer<var_num_occs> varinfo;
-    get_polynomial_info(p, varinfo);
+    if (!get_polynomial_info(p, varinfo))
+        return true;
     if (varinfo.empty())
         return true;
     std::stable_sort(varinfo.begin(), varinfo.end(), var_num_occs_lt());