From dff419a7cb5cadc46fc29b99cb4b9d748ad7621f Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 18 Dec 2023 13:51:29 -0800
Subject: [PATCH] pin expressions to fix unsound behavior

---
 src/solver/simplifier_solver.cpp | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/solver/simplifier_solver.cpp b/src/solver/simplifier_solver.cpp
index 7debe6bc0..ed645dae0 100644
--- a/src/solver/simplifier_solver.cpp
+++ b/src/solver/simplifier_solver.cpp
@@ -80,8 +80,10 @@ class simplifier_solver : public solver {
         void flatten_suffix() override {
             expr_mark seen;
             unsigned j = qhead();
+            expr_ref_vector pinned(s.m);
             for (unsigned i = qhead(); i < qtail(); ++i) {
                 expr* f = s.m_fmls[i].fml(), *g = nullptr;
+                pinned.push_back(f);
                 if (seen.is_marked(f))
                     continue;
                 seen.mark(f, true);