From 97683bd48a00d51d0c8deeaff1adaaeae41400de Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 8 Dec 2020 12:12:16 -0800
Subject: [PATCH] fix #4876

---
 src/ast/rewriter/seq_rewriter.cpp | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index 6725c263c..0c581b296 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -1712,8 +1712,9 @@ br_status seq_rewriter::mk_seq_replace_all(expr* a, expr* b, expr* c, expr_ref&
             return BR_DONE;
         }
         expr_ref_vector strs(m());
-        for (unsigned i = 0; i < s1.length() - s2.length(); ++i) {
-            if (s2 == s1.extract(0, s2.length()-1)) {
+        for (unsigned i = 0; i < s1.length(); ++i) {
+            if (s1.length() >= s2.length() + i && 
+                s2 == s1.extract(i, s2.length())) {
                 strs.push_back(c);
                 i += s2.length();
             }