From 927b03615cd6bdbc89c19d74867f4260d4da4296 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Tue, 3 Mar 2026 21:53:55 +0000 Subject: [PATCH] Fix dangling pointer in fresh variable name construction in generate_extensions() Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/smt/seq/seq_nielsen.cpp | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp index 6b3a3efe5..2cdf8877e 100644 --- a/src/smt/seq/seq_nielsen.cpp +++ b/src/smt/seq/seq_nielsen.cpp @@ -552,7 +552,8 @@ namespace seq { // Const Nielsen modifier: lhs starts with char, rhs starts with var // -> substitute rhs_var = char . fresh_var if (lhead->is_char() && rhead->is_var()) { - symbol fresh_name(("v!" + std::to_string(node->id())).c_str()); + std::string fresh_str = "v!" + std::to_string(node->id()); + symbol fresh_name(fresh_str.c_str()); euf::snode* fresh = m_sg.mk_var(fresh_name); euf::snode* replacement = m_sg.mk_concat(lhead, fresh); @@ -565,7 +566,8 @@ namespace seq { } if (rhead->is_char() && lhead->is_var()) { - symbol fresh_name(("v!" + std::to_string(node->id())).c_str()); + std::string fresh_str = "v!" + std::to_string(node->id()); + symbol fresh_name(fresh_str.c_str()); euf::snode* fresh = m_sg.mk_var(fresh_name); euf::snode* replacement = m_sg.mk_concat(rhead, fresh);