mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 09:34:08 +00:00
parent
886f4cbee0
commit
c7878e384c
|
@ -1262,7 +1262,7 @@ br_status seq_rewriter::mk_seq_index(expr* a, expr* b, expr* c, expr_ref& result
|
|||
unsigned i = 0;
|
||||
if (m_autil.is_numeral(c, r)) {
|
||||
i = 0;
|
||||
while (r.is_pos() && m_util.str.is_unit(as.get(i))) {
|
||||
while (r.is_pos() && i < as.size() && m_util.str.is_unit(as.get(i))) {
|
||||
r -= rational(1);
|
||||
++i;
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue