From 596f158e44049775fece2c9156c5878873750d03 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 25 Jun 2026 21:39:54 -0700 Subject: [PATCH] change back coalesce_chars to true, a regression Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.cpp | 3 +++ src/ast/rewriter/seq_rewriter.h | 2 +- 2 files changed, 4 insertions(+), 1 deletion(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index daa2714e4a..e7981566a2 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -470,6 +470,7 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con */ br_status seq_rewriter::mk_seq_unit(expr* e, expr_ref& result) { unsigned ch; + verbose_stream() << "mk_seq_unit: " << mk_ismt2_pp(e, m()) << " " << m_coalesce_chars << "\n"; // specifically we want (_ BitVector 8) if (m_util.is_const_char(e, ch) && m_coalesce_chars) { // convert to string constant @@ -500,6 +501,8 @@ br_status seq_rewriter::mk_seq_concat(expr* a, expr* b, expr_ref& result) { expr* c, *d; bool isc1 = str().is_string(a, s1) && m_coalesce_chars; bool isc2 = str().is_string(b, s2) && m_coalesce_chars; + + verbose_stream() << "mk_seq_concat: a = " << mk_ismt2_pp(a, m()) << ", b = " << mk_ismt2_pp(b, m()) << "\n"; if (isc1 && isc2) { result = str().mk_string(s1 + s2); return BR_DONE; diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h index d20e4f50ee..45821c8042 100644 --- a/src/ast/rewriter/seq_rewriter.h +++ b/src/ast/rewriter/seq_rewriter.h @@ -139,7 +139,7 @@ class seq_rewriter { // re2automaton m_re2aut; op_cache m_op_cache; expr_ref_vector m_es, m_lhs, m_rhs; - bool m_coalesce_chars = false; + bool m_coalesce_chars = true; bool m_in_bisim { false }; unsigned m_re_deriv_depth { 0 }; static const unsigned m_max_re_deriv_depth = 512;