fix #3967 regression from using rewriter mode that splits strings

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Apr 15, 2020 · 068f65c · 068f65c
1 parent 79a2b52
commit 068f65c
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
@@ -4320,6 +4320,7 @@ class theory_seq::seq_value_proc : public model_value_proc {
                     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);