From 559af09b0756fb68629dc9463e7ff27994566d5f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 12 Jul 2019 19:01:39 +0100 Subject: [PATCH] fix index cases Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.cpp | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 020ca748f..b9cb5f8d7 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -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); unsigned rsz = lens.size(); unsigned i = 0; - for (; i < rsz; ++i) { + for (; i < m_lhs.size(); ++i) { expr* lhs = m_lhs.get(i); if (lens.contains(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; 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); for (expr* rhs : lens) { t2 = m_autil.mk_add(t2, m_util.str.mk_length(rhs));