mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-07 13:54:53 +00:00
Code Activity

Fixed nseq model construction

Browse source
This commit is contained in:
CEisenhofer 2026-03-04 19:15:50 +01:00
parent b2838b472d
commit b935394aaf
1 changed files with 4 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/smt/nseq_model.cpp
View file

@ -86,8 +86,8 @@ namespace smt {
val = snode_to_value(sn);
if (!val) {
// no assignment found — generate fresh value
val = m_factory->get_fresh_value(e->get_sort());
// no assignment found — default to empty string
val = m_seq.str.mk_empty(e->get_sort());
}
if (val) {
@ -254,11 +254,11 @@ namespace smt {
}
}
// no regex constraint or witness generation failed: plain fresh value
// no regex constraint or witness generation failed: use empty string
sort* srt = m_seq.str.mk_string_sort();
if (var->get_expr())
srt = var->get_expr()->get_sort();
return m_factory->get_fresh_value(srt);
return m_seq.str.mk_empty(srt);
}
void nseq_model::collect_var_regex_constraints(nseq_state const& state) {