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] 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);