mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-29 02:03:49 +00:00
Code Activity

Fix #9063: avoid leaking internal seq skolem terms into models

Browse source 
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
This commit is contained in:
Nikolaj Bjorner 2026-07-28 10:58:04 -07:00
parent 06824e7f5a
commit 318738b309
1 changed files with 10 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/smt/theory_seq.cpp
View file

@ -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);