diff --git a/src/muz/spacer/spacer_sat_answer.cpp b/src/muz/spacer/spacer_sat_answer.cpp
index 593d0d76d..98e93be1d 100644
--- a/src/muz/spacer/spacer_sat_answer.cpp
+++ b/src/muz/spacer/spacer_sat_answer.cpp
@@ -127,8 +127,14 @@ void ground_sat_answer_op::mk_children(frame &fr, vector<frame> &todo) {
     m_solver->assert_expr(fr.pt().transition());
     m_solver->assert_expr(fr.pt().rule2tag(&r));
 
+    TRACE("spacer_sat",
+          tout << "Solver in mk_children\n";
+          m_solver->display(tout) << "\n";);
+
     lbool res = m_solver->check_sat(0, nullptr);
     (void)res;
+    CTRACE("spacer_sat", res != l_true,
+           tout << "Result: " << res << "\n";);
     VERIFY(res == l_true);
 
     model_ref mdl;
diff --git a/src/muz/spacer/spacer_util.cpp b/src/muz/spacer/spacer_util.cpp
index dd7e2a6ab..825f5012c 100644
--- a/src/muz/spacer/spacer_util.cpp
+++ b/src/muz/spacer/spacer_util.cpp
@@ -496,15 +496,16 @@ namespace {
             SASSERT(m_todo.empty());
             if (m_visited.is_marked(e) || !is_app(e)) return;
 
+            m_todo.reset();
             m_todo.push_back(e);
-            for (unsigned i = 0; i < m_todo.size(); ++i) {
+            while(!m_todo.empty()) {
                 e = m_todo.back();
+                m_todo.pop_back();
                 if (!is_app(e)) continue;
                 app* a = to_app(e);
-                m_todo.pop_back();
                 process_app(a, out);
                 m_visited.mark(a, true);
-            } 
+            }
             m_todo.reset();
         }