mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
typing error
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
7f22eb594e
commit
bc03ffb800
|
@ -1972,7 +1972,7 @@ bool seq_rewriter::get_head_tail(expr* s, expr_ref& head, expr_ref& tail) {
|
|||
return true;
|
||||
}
|
||||
if (m_util.str.is_string(s, s1) && s1.length() > 0) {
|
||||
head = m_util.str.mk_string(s1.extract(0, 1));
|
||||
head = m_util.mk_char(s1[0]);
|
||||
tail = m_util.str.mk_string(s1.extract(1, s1.length()));
|
||||
return true;
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue