fix #4060

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Apr 23, 2020 · c7878e3 · c7878e3
1 parent 886f4cb
commit c7878e3
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
@@ -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;
         }