mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-27 00:18:45 +00:00
Code Activity

fix index cases

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-07-12 19:01:39 +01:00
parent 84990ffa27
commit 559af09b07
1 changed files with 7 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/ast/rewriter/seq_rewriter.cpp
View file

@ -704,7 +704,7 @@ br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& resu
get_lengths(b, lens, other, pos); get_lengths(b, lens, other, pos);
unsigned rsz = lens.size(); unsigned rsz = lens.size();
unsigned i = 0; unsigned i = 0;
for (; i < rsz; ++i) { for (; i < m_lhs.size(); ++i) {
expr* lhs = m_lhs.get(i); expr* lhs = m_lhs.get(i);
if (lens.contains(lhs)) { if (lens.contains(lhs)) {
lens.erase(lhs); lens.erase(lhs);
@ -718,7 +718,12 @@ br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& resu
} }
if (i == 0) return BR_FAILED; if (i == 0) return BR_FAILED;
expr_ref t1(m()), t2(m()); expr_ref t1(m()), t2(m());
t1 = m_util.str.mk_concat(m_lhs.size() - i, m_lhs.c_ptr() + i); if (m_lhs.size() == i) {
t1 = m_util.str.mk_empty(m().get_sort(a));
}
else {
t1 = m_util.str.mk_concat(m_lhs.size() - i, m_lhs.c_ptr() + i);
}
t2 = m_autil.mk_int(pos); t2 = m_autil.mk_int(pos);
for (expr* rhs : lens) { for (expr* rhs : lens) {
t2 = m_autil.mk_add(t2, m_util.str.mk_length(rhs)); t2 = m_autil.mk_add(t2, m_util.str.mk_length(rhs));