diff --git a/src/sat/smt/arith_internalize.cpp b/src/sat/smt/arith_internalize.cpp
index 09352e147..30eab0b53 100644
--- a/src/sat/smt/arith_internalize.cpp
+++ b/src/sat/smt/arith_internalize.cpp
@@ -98,6 +98,7 @@ namespace arith {
     void solver::found_underspecified(expr* n) {
         if (a.is_underspecified(n)) {
             TRACE("arith", tout << "Unhandled: " << mk_pp(n, m) << "\n";);
+            ctx.push(push_back_vector(m_underspecified));
             m_underspecified.push_back(to_app(n));
         }
         expr* e = nullptr, * x = nullptr, * y = nullptr;
@@ -243,6 +244,7 @@ namespace arith {
                     mk_abs_axiom(t);                
                 else if (a.is_idiv(n, n1, n2)) {
                     if (!a.is_numeral(n2, r) || r.is_zero()) found_underspecified(n);
+                    ctx.push(push_back_vector(m_idiv_terms));
                     m_idiv_terms.push_back(n);
                     app_ref mod(a.mk_mod(n1, n2), m);
                     internalize(mod, m_is_redundant);
diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp
index 7d3578dc5..883773988 100644
--- a/src/sat/smt/arith_solver.cpp
+++ b/src/sat/smt/arith_solver.cpp
@@ -681,10 +681,7 @@ namespace arith {
         scope& sc = m_scopes.back();
         sc.m_bounds_lim = m_bounds_trail.size();
         sc.m_asserted_qhead = m_asserted_qhead;
-        sc.m_idiv_lim = m_idiv_terms.size();
         sc.m_asserted_lim = m_asserted.size();
-        sc.m_not_handled = m_not_handled;
-        sc.m_underspecified_lim = m_underspecified.size();
         lp().push();
         if (m_nla)
             m_nla->push();
@@ -696,11 +693,8 @@ namespace arith {
         TRACE("arith", tout << "pop " << num_scopes << "\n";);
         unsigned old_size = m_scopes.size() - num_scopes;
         del_bounds(m_scopes[old_size].m_bounds_lim);
-        m_idiv_terms.shrink(m_scopes[old_size].m_idiv_lim);
         m_asserted.shrink(m_scopes[old_size].m_asserted_lim);
         m_asserted_qhead = m_scopes[old_size].m_asserted_qhead;
-        m_underspecified.shrink(m_scopes[old_size].m_underspecified_lim);
-        m_not_handled = m_scopes[old_size].m_not_handled;
         m_scopes.resize(old_size);
         lp().pop(num_scopes);
         m_new_bounds.reset();
@@ -1117,7 +1111,7 @@ namespace arith {
         if (m_delayed_eqs.empty())
             return true;
         force_push();
-        for (unsigned i; i < m_delayed_eqs.size(); ++i) {
+        for (unsigned i = 0; i < m_delayed_eqs.size(); ++i) {
             auto p = m_delayed_eqs[i];
             auto const& e = p.first;
             if (p.second)
diff --git a/src/sat/smt/arith_solver.h b/src/sat/smt/arith_solver.h
index cf21e13b8..83c91ac05 100644
--- a/src/sat/smt/arith_solver.h
+++ b/src/sat/smt/arith_solver.h
@@ -105,11 +105,8 @@ namespace arith {
 
         struct scope {
             unsigned m_bounds_lim;
-            unsigned m_idiv_lim;
             unsigned m_asserted_qhead;
             unsigned m_asserted_lim;
-            unsigned m_underspecified_lim;
-            expr* m_not_handled;
         };
 
         class resource_limit : public lp::lp_resource_limit {
@@ -220,7 +217,7 @@ namespace arith {
         svector<std::pair<euf::th_eq, bool>>          m_delayed_eqs;
 
         literal_vector  m_asserted;
-        expr* m_not_handled{ nullptr };
+        expr* m_not_handled = nullptr;
         ptr_vector<app>        m_underspecified;
         ptr_vector<expr>       m_idiv_terms;
         vector<ptr_vector<api_bound> > m_use_list;        // bounds where variables are used.