mirror of
https://github.com/Z3Prover/z3
synced 2025-04-10 19:27:06 +00:00
parent
e1b52c323c
commit
6af6617e36
|
@ -117,6 +117,7 @@ namespace smt {
|
|||
}
|
||||
if (u.is_seq(s, ch)) {
|
||||
expr* v = m_model.get_fresh_value(ch);
|
||||
if (!v) return nullptr;
|
||||
return u.str.mk_unit(v);
|
||||
}
|
||||
UNREACHABLE();
|
||||
|
|
Loading…
Reference in a new issue