From ff7cbe94067843329e7857459d7cede68282ee94 Mon Sep 17 00:00:00 2001
From: CEisenhofer <clemens.eisenhofer@tuwien.ac.at>
Date: Fri, 26 Jun 2026 11:08:54 +0200
Subject: [PATCH] Copy elements from propagation queue before propagating them.
 The memory might get invalidated inbetween

---
 scripts/compare_seq_solvers.py |  2 +-
 src/smt/theory_nseq.cpp        | 23 ++++++++++++++++-------
 src/smt/theory_nseq.h          |  1 +
 3 files changed, 18 insertions(+), 8 deletions(-)

diff --git a/scripts/compare_seq_solvers.py b/scripts/compare_seq_solvers.py
index 8335b33be3..bc465a4254 100644
--- a/scripts/compare_seq_solvers.py
+++ b/scripts/compare_seq_solvers.py
@@ -38,7 +38,7 @@ COMMON_ARGS = ["model_validate=true"]
 SOLVERS = {
     "nseq_md": ["smt.string_solver=nseq", "smt.nseq.parikh=false",
                 "smt.nseq.regex_factorization_threshold=100", "smt.nseq.regex_factorization_eager=true"],
-    "nseq_pa": ["smt.string_solver=nseq", "smt.nseq.parikh=true",
+    "nseq_pa": ["smt.string_solver=nseq", "smt.nseq.parikh=false",
                 "smt.nseq.regex_factorization_threshold=0", "smt.nseq.regex_factorization_eager=false"],
     "seq":     ["smt.string_solver=seq"],
 }
diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp
index 1c963be421..e6442170e2 100644
--- a/src/smt/theory_nseq.cpp
+++ b/src/smt/theory_nseq.cpp
@@ -463,14 +463,23 @@ namespace smt {
             ctx.push_trail(value_trail(m_prop_qhead));
             while (m_prop_qhead < m_prop_queue.size() && !ctx.inconsistent()) {
                 auto const& item = m_prop_queue[m_prop_qhead++];
-                if (std::holds_alternative<eq_item>(item))
-                    propagate_eq(std::get<eq_item>(item));
-                else if (std::holds_alternative<deq_item>(item))
-                    propagate_deq(std::get<deq_item>(item));
-                else if (std::holds_alternative<mem_item>(item))
-                    propagate_pos_mem(std::get<mem_item>(item));
-                else if (std::holds_alternative<axiom_item>(item))
+                // don't pass arguments via reference. They might tigger internalization
+                // and so the references from the propagation queue might change
+                if (std::holds_alternative<eq_item>(item)) {
+                    const auto eq = std::get<eq_item>(item);
+                    propagate_eq(eq);
+                }
+                else if (std::holds_alternative<deq_item>(item)) {
+                    const auto deq = std::get<deq_item>(item);
+                    propagate_deq(deq);
+                }
+                else if (std::holds_alternative<mem_item>(item)) {
+                    const auto mem = std::get<mem_item>(item);
+                    propagate_pos_mem(mem);
+                }
+                else if (std::holds_alternative<axiom_item>(item)) {
                     dequeue_axiom(std::get<axiom_item>(item).e);
+                }
                 else {
                     UNREACHABLE();
                 }
diff --git a/src/smt/theory_nseq.h b/src/smt/theory_nseq.h
index b2c64f859d..499d2017c1 100644
--- a/src/smt/theory_nseq.h
+++ b/src/smt/theory_nseq.h
@@ -153,6 +153,7 @@ namespace smt {
         void propagate_eq(tracked_str_eq const& eq) const;
         void propagate_deq(tracked_str_deq const& deq) const;
         void propagate_pos_mem(tracked_str_mem const& mem);
+
         void enqueue_axiom(expr* e);
         void dequeue_axiom(expr* e);
         void ensure_length_var(expr* e) const;