From 068f65c8ac7dcb89e71f7535f5c4f6a89b345c01 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 15 Apr 2020 10:36:33 -0700
Subject: [PATCH] fix #3967 regression from using rewriter mode that splits
 strings

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/theory_seq.cpp | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 0aab00b23..dfa9353bd 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -4320,6 +4320,7 @@ public:
                     dependency* deps = nullptr;
                     expr_ref tmp(th.m);
                     if (!th.canonize(m_strings[k], deps, tmp)) tmp = m_strings[k];
+                    th.m_str_rewrite(tmp);
                     zstring zs;
                     if (th.m_util.str.is_string(tmp, zs)) {
                         add_buffer(sbuffer, zs);