From 69da8f02c25a651281b60cb0eecb2e9c8a79a40e Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Tue, 3 Mar 2026 05:19:06 +0000 Subject: [PATCH] fix re.concat classification and loop nullability in euf_sgraph.cpp Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/ast/euf/euf_sgraph.cpp | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) diff --git a/src/ast/euf/euf_sgraph.cpp b/src/ast/euf/euf_sgraph.cpp index eff926004..b1c232ef6 100644 --- a/src/ast/euf/euf_sgraph.cpp +++ b/src/ast/euf/euf_sgraph.cpp @@ -80,7 +80,7 @@ namespace euf { return snode_kind::s_other; } - if (m_seq.str.is_concat(e)) + if (m_seq.str.is_concat(e) || m_seq.re.is_concat(e)) return snode_kind::s_concat; if (m_seq.str.is_unit(e)) { @@ -200,13 +200,20 @@ namespace euf { n->m_length = 1; break; - case snode_kind::s_loop: + case snode_kind::s_loop: { n->m_ground = n->num_args() > 0 ? n->arg(0)->is_ground() : true; n->m_regex_free = false; - n->m_nullable = false; // depends on lower bound + // nullable iff lower bound is 0: r{0,n} accepts the empty string + unsigned lo = 1, hi = 0; + expr* loop_body = nullptr; + if (n->get_expr() && + !m_seq.re.is_loop(n->get_expr(), loop_body, lo, hi)) + m_seq.re.is_loop(n->get_expr(), loop_body, lo); + n->m_nullable = (lo == 0); n->m_level = 1; n->m_length = 1; break; + } case snode_kind::s_union: SASSERT(n->num_args() == 2);