From 11efe33aa0d02fad08e280b144b3ba599cd18f2f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 3 Mar 2021 11:19:03 -0800 Subject: [PATCH] fix #5061 --- src/ast/rewriter/seq_rewriter.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index f466f5cf1..a4e3cc8c9 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -2009,8 +2009,8 @@ br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) { } expr* b2 = nullptr, *b3 = nullptr; - if (str().is_replace(b, b1, b2, b3) && b2 == a1 && str().is_empty(b3)) { - result = str().mk_prefix(str().mk_concat(a1, a1), b1); + if (str().is_replace(b, b1, b2, b3) && b2 == a && str().is_empty(b3)) { + result = str().mk_prefix(str().mk_concat(a, a), b1); return BR_REWRITE2; }