From e172aa370d5bc25bf4ce10cfd49119c21ade487c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 20 Apr 2026 18:19:16 +0200 Subject: [PATCH] add simplification rule to concatentations of regex to avoid stack overflow in derivatives of very long expressions Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.cpp | 5 +++++ src/smt/seq/seq_nielsen.cpp | 2 ++ 2 files changed, 7 insertions(+) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index e70168498..044ee4523 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -4539,6 +4539,11 @@ br_status seq_rewriter::mk_re_concat(expr* a, expr* b, expr_ref& result) { result = re().mk_plus(b); return BR_DONE; } + expr *x = nullptr, *y = nullptr; + if (re().is_concat(a, x, y) && re().is_full_seq(y) && re().is_full_seq(b)) { + result = a; + return BR_DONE; + } expr_ref a_str(m()); expr_ref b_str(m()); if (lift_str_from_to_re(a, a_str) && lift_str_from_to_re(b, b_str)) { diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp index fdf2e8c0f..ee8eda179 100644 --- a/src/smt/seq/seq_nielsen.cpp +++ b/src/smt/seq/seq_nielsen.cpp @@ -1502,6 +1502,8 @@ namespace seq { IF_VERBOSE(1, display(verbose_stream(), node)); CTRACE(seq, !ext, display(tout, node) << to_dot() << "\n"); if (!ext) { + std::cout << "No extensions generated for node " << node->id() << ", but not satisfied or conflict?!" + << std::endl; node->to_html(std::cout, m); std::cout << std::endl; display(std::cout, node);