From c7878e384cb07a4040e383790af638987d5d7d3d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 22 Apr 2020 17:46:16 -0700 Subject: [PATCH] fix #4060 Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 5e9f66ece..f322f949f 100644 --- 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; }