From 9d6728aa718b003adda909a7147533f18ea222fe Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 2 Aug 2019 01:14:31 +0800
Subject: [PATCH] fix unsound rewrite

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 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 d61af5057..967ecdc0b 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -960,7 +960,7 @@ br_status seq_rewriter::mk_seq_at(expr* a, expr* b, expr_ref& result) {
             result = m_util.str.mk_empty(m().get_sort(a));
         }
         else {
-            result = a2;
+            result = a;
         }
         return BR_DONE;            
     }