From be65e9a2418910821b109d2764981e9e1196062e Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 9 Mar 2020 17:37:38 +0100
Subject: [PATCH] fix #3218

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/tactic/core/solve_eqs_tactic.cpp | 3 +++
 1 file changed, 3 insertions(+)

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);