mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
parent
a9a26e5f2e
commit
aff4b3022a
|
@ -731,6 +731,7 @@ br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& resu
|
|||
t2 = m_autil.mk_add(t2, m_util.str.mk_length(rhs));
|
||||
}
|
||||
result = m_util.str.mk_substr(t1, t2, c);
|
||||
TRACE("seq", tout << result << "\n";);
|
||||
return BR_REWRITE2;
|
||||
}
|
||||
|
||||
|
@ -798,7 +799,7 @@ bool seq_rewriter::get_lengths(expr* e, expr_ref_vector& lens, rational& pos) {
|
|||
else {
|
||||
return false;
|
||||
}
|
||||
return true;
|
||||
return !pos.is_neg();
|
||||
}
|
||||
|
||||
bool seq_rewriter::cannot_contain_suffix(expr* a, expr* b) {
|
||||
|
|
Loading…
Reference in a new issue