From ae5a713e815eb884a7f60d54ac489b14689b90e8 Mon Sep 17 00:00:00 2001
From: Arie Gurfinkel <arie.gurfinkel@uwaterloo.ca>
Date: Sat, 11 Apr 2020 00:18:25 -0400
Subject: [PATCH] fix #3906 by fixing a regression from today

---
 src/muz/spacer/spacer_util.cpp | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

diff --git a/src/muz/spacer/spacer_util.cpp b/src/muz/spacer/spacer_util.cpp
index 825f5012c..606c19e7c 100644
--- a/src/muz/spacer/spacer_util.cpp
+++ b/src/muz/spacer/spacer_util.cpp
@@ -496,13 +496,17 @@ namespace {
             SASSERT(m_todo.empty());
             if (m_visited.is_marked(e) || !is_app(e)) return;
 
+            // -- keep track of all created expressions to
+            // -- make sure that expression ids are stable
+            expr_ref_vector pinned(m);
+
             m_todo.reset();
             m_todo.push_back(e);
             while(!m_todo.empty()) {
-                e = m_todo.back();
+                pinned.push_back(m_todo.back());
                 m_todo.pop_back();
-                if (!is_app(e)) continue;
-                app* a = to_app(e);
+                if (!is_app(pinned.back())) continue;
+                app* a = to_app(pinned.back());
                 process_app(a, out);
                 m_visited.mark(a, true);
             }