From 318738b3093e2ad0c47945152cc0f81724c8fdf3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 28 Jul 2026 10:58:04 -0700 Subject: [PATCH] Fix #9063: avoid leaking internal seq skolem terms into models When building the model value of a sequence, an unresolved element such as (seq.nth_i k!0 0) over an internal sequence constant could be emitted verbatim, exposing internal skolem symbols (e.g. k!0) in the user-visible model returned by get-model / get-value. Such a term is not a proper value and is unconstrained at model-construction time, so replace it with a concrete fresh value from the sequence factory. This only affects model values that were already non-concrete (i.e. leaking internal terms); genuine concrete sequence values satisfy m.is_value and are left untouched, so sat/unsat verdicts and normal string/sequence models are unaffected. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: 57b9b87e-950a-49ea-bbb3-ed585646a5a9 --- src/smt/theory_seq.cpp | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index a7dee69d93..27b43a6f16 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -2205,6 +2205,16 @@ app* theory_seq::mk_value(expr* e) { else { m_rewrite(result); } + // Avoid leaking internal terms into the model. An unresolved sequence + // value (e.g. (seq.nth_i k!0 0) over an internal sequence constant k!0) + // is not a proper value and must not be exposed to the user. Since such a + // term is unconstrained at this point, replace it by a concrete fresh + // value from the factory. See issue #9063. + if (m_util.is_seq(result) && !m.is_value(result)) { + expr_ref fresh(m_factory->get_fresh_value(result->get_sort()), m); + if (fresh) + result = fresh; + } m_factory->add_trail(result); TRACE(seq, tout << mk_pp(e, m) << " -> " << result << "\n";); m_rep.update(e, result, nullptr);