From d902ce166e4dd521aca853dc03c2ed1ce7eb0839 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Tue, 3 Mar 2026 05:17:55 +0000
Subject: [PATCH 1/3] Initial plan


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 2/3] 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);

From c0ed79c93b74b645deb3e6d1e8c5fb70ea5f5836 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Tue, 3 Mar 2026 05:40:16 +0000
Subject: [PATCH 3/3] improve s_loop nullable extraction: clearer comments and
 sentinel values

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
 src/ast/euf/euf_sgraph.cpp | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/ast/euf/euf_sgraph.cpp b/src/ast/euf/euf_sgraph.cpp
index b1c232ef6..0434fe239 100644
--- a/src/ast/euf/euf_sgraph.cpp
+++ b/src/ast/euf/euf_sgraph.cpp
@@ -204,8 +204,10 @@ namespace euf {
             n->m_ground = n->num_args() > 0 ? n->arg(0)->is_ground() : true;
             n->m_regex_free = false;
             // nullable iff lower bound is 0: r{0,n} accepts the empty string
-            unsigned lo = 1, hi = 0;
+            // default lo=1 (non-nullable) in case extraction fails
+            unsigned lo = 1, hi = 1;
             expr* loop_body = nullptr;
+            // try bounded r{lo,hi} first; fall back to unbounded r{lo,}
             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);