diff --git a/src/ast/euf/euf_sgraph.cpp b/src/ast/euf/euf_sgraph.cpp
index 2fc385688..8242ca35e 100644
--- a/src/ast/euf/euf_sgraph.cpp
+++ b/src/ast/euf/euf_sgraph.cpp
@@ -96,6 +96,9 @@ namespace euf {
         if (m_seq.re.is_full_seq(e))
             return snode_kind::s_full_seq;
 
+        if (m_seq.re.is_range(e))
+            return snode_kind::s_range;
+
         if (m_seq.re.is_to_re(e))
             return snode_kind::s_to_re;
 
@@ -252,8 +255,16 @@ namespace euf {
             n->m_length = 1;
             break;
 
+        case snode_kind::s_range:
+            SASSERT(n->num_args() == 2);
+            n->m_ground = n->arg(0)->is_ground() && n->arg(1)->is_ground();
+            n->m_regex_free = false;
+            n->m_nullable = false;
+            n->m_level = 1;
+            n->m_length = 1;
+            break;
+
         case snode_kind::s_to_re:
-            // NSB review: are strings nullable or just empty
             SASSERT(n->num_args() == 1);
             n->m_ground = n->arg(0)->is_ground();
             n->m_regex_free = false;
@@ -746,6 +757,7 @@ namespace euf {
             case snode_kind::s_fail:       return "fail";
             case snode_kind::s_full_char:  return "full_char";
             case snode_kind::s_full_seq:   return "full_seq";
+            case snode_kind::s_range:      return "range";
             case snode_kind::s_to_re:      return "to_re";
             case snode_kind::s_in_re:      return "in_re";
             case snode_kind::s_other:      return "other";
diff --git a/src/ast/euf/euf_sgraph.h b/src/ast/euf/euf_sgraph.h
index a3d52a403..0da7f69c0 100644
--- a/src/ast/euf/euf_sgraph.h
+++ b/src/ast/euf/euf_sgraph.h
@@ -17,7 +17,7 @@ Abstract:
 
     -- snode classification: empty, char, variable, unit, concat, power,
        star, loop, union, intersection, complement, fail, full_char,
-       full_seq, to_re, in_re, other.
+       full_seq, range, to_re, in_re, other.
     -- Metadata computation: ground, regex_free, nullable, level, length.
     -- Expression registration via mk(expr*), lookup via find(expr*).
     -- Scope management: push/pop with backtracking.
diff --git a/src/ast/euf/euf_snode.h b/src/ast/euf/euf_snode.h
index d0be50946..a67644168 100644
--- a/src/ast/euf/euf_snode.h
+++ b/src/ast/euf/euf_snode.h
@@ -50,6 +50,7 @@ namespace euf {
         s_fail,        // empty language (OP_RE_EMPTY_SET)
         s_full_char,   // full character set (OP_RE_FULL_CHAR_SET)
         s_full_seq,    // full sequence set r=.* (OP_RE_FULL_SEQ_SET)
+        s_range,       // character range [lo,hi] (OP_RE_RANGE)
         s_to_re,       // string to regex (OP_SEQ_TO_RE)
         s_in_re,       // regex membership (OP_SEQ_IN_RE)
         s_other,       // other sequence expression not directly classified
@@ -125,6 +126,7 @@ namespace euf {
         bool is_fail()       const { return m_kind == snode_kind::s_fail; }
         bool is_full_char()  const { return m_kind == snode_kind::s_full_char; }
         bool is_full_seq()   const { return m_kind == snode_kind::s_full_seq; }
+        bool is_range()      const { return m_kind == snode_kind::s_range; }
         bool is_to_re()      const { return m_kind == snode_kind::s_to_re; }
         bool is_in_re()      const { return m_kind == snode_kind::s_in_re; }