From cf3002c2937d5845fa51b9071d46392898440374 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 3 Mar 2021 23:13:56 -0800
Subject: [PATCH] fix #5071

---
 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 a4e3cc8c9..c196d99b4 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -1869,7 +1869,7 @@ br_status seq_rewriter::mk_seq_replace_all(expr* a, expr* b, expr* c, expr_ref&
             if (s1.length() >= s2.length() + i && 
                 s2 == s1.extract(i, s2.length())) {
                 strs.push_back(c);
-                i += s2.length();
+                i += s2.length() - 1;
             }
             else 
                 strs.push_back(str().mk_unit(str().mk_char(s1, i)));