diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp
index c5730c19c..7d3578dc5 100644
--- a/src/sat/smt/arith_solver.cpp
+++ b/src/sat/smt/arith_solver.cpp
@@ -1114,12 +1114,11 @@ namespace arith {
 
     bool solver::check_delayed_eqs() {
         bool found_diseq = false;
-        if (m_delayed_eqs_qhead == m_delayed_eqs.size())
+        if (m_delayed_eqs.empty())
             return true;
         force_push();
-        ctx.push(value_trail<unsigned>(m_delayed_eqs_qhead));
-        for (; m_delayed_eqs_qhead < m_delayed_eqs.size(); ++ m_delayed_eqs_qhead) {
-            auto p = m_delayed_eqs[m_delayed_eqs_qhead];
+        for (unsigned i; i < m_delayed_eqs.size(); ++i) {
+            auto p = m_delayed_eqs[i];
             auto const& e = p.first;
             if (p.second)
                 new_eq_eh(e);
diff --git a/src/sat/smt/arith_solver.h b/src/sat/smt/arith_solver.h
index a1c89af76..cf21e13b8 100644
--- a/src/sat/smt/arith_solver.h
+++ b/src/sat/smt/arith_solver.h
@@ -218,7 +218,6 @@ namespace arith {
         svector<euf::enode_pair>                      m_equalities;      // asserted rows corresponding to equalities.
         svector<theory_var>                           m_definitions;     // asserted rows corresponding to definitions
         svector<std::pair<euf::th_eq, bool>>          m_delayed_eqs;
-        unsigned                                      m_delayed_eqs_qhead = 0;
 
         literal_vector  m_asserted;
         expr* m_not_handled{ nullptr };