fix #5061

NikolajBjorner · NikolajBjorner · commit 11efe33aa0d0 · 2021-03-03T11:19:03.000-08:00
diff --git 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;
     }
 

Original file line number	Diff line number	Diff line change
`@@ -2009,8 +2009,8 @@ br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) {`
`2009`	`2009`	`}`
`2010`	`2010`
`2011`	`2011`	`expr* b2 = nullptr, *b3 = nullptr;`
`2012`		`- if (str().is_replace(b, b1, b2, b3) && b2 == a1 && str().is_empty(b3)) {`
`2013`		`- result = str().mk_prefix(str().mk_concat(a1, a1), b1);`
	`2012`	`+ if (str().is_replace(b, b1, b2, b3) && b2 == a && str().is_empty(b3)) {`
	`2013`	`+ result = str().mk_prefix(str().mk_concat(a, a), b1);`
`2014`	`2014`	`return BR_REWRITE2;`
`2015`	`2015`	`}`
`2016`	`2016`