diff --git a/src/tactic/core/solve_eqs_tactic.cpp b/src/tactic/core/solve_eqs_tactic.cpp
index 005d1b2e6..ade601951 100644
--- a/src/tactic/core/solve_eqs_tactic.cpp
+++ b/src/tactic/core/solve_eqs_tactic.cpp
@@ -516,6 +516,9 @@ class solve_eqs_tactic : public tactic {
                         occ.mark(e, occ.is_marked(body));
                         m_todo.pop_back();
                     }
+					else {
+						m_todo.push_back(body);
+					}
                 }
                 else {
                     visited.mark(e, true);