pin expressions to fix unsound behavior

Z3Prover · Dec 19, 2023 · dff419a · dff419a
1 parent 5d4c18d
commit dff419a
Showing 1 changed file with 2 additions and 0 deletions.
diff --git 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);