diff --git a/src/ast/euf/euf_sgraph.cpp b/src/ast/euf/euf_sgraph.cpp
index b332cd2a4..c167f16ce 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)) {
@@ -201,13 +201,17 @@ namespace euf {
             break;
 
         case snode_kind::s_loop: {
-            bool body_nullable = n->num_args() > 0 && n->arg(0)->is_nullable();
-            unsigned lo = 0, hi = 0;
-            expr* body = nullptr;
-            bool lo_zero = n->get_expr() && m_seq.re.is_loop(n->get_expr(), body, lo, hi) && lo == 0;
             n->m_ground = n->num_args() > 0 ? n->arg(0)->is_ground() : true;
             n->m_regex_free = false;
-            n->m_nullable = lo_zero || body_nullable;
+            // nullable iff lower bound is 0: r{0,n} accepts the empty string
+            // 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);
+            n->m_nullable = (lo == 0);
             n->m_level = 1;
             n->m_length = 1;
             break;