From e4f9a517e4407fbe5fd6e56fbd3e839d9b3b4bae Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Sun, 1 Mar 2026 20:25:18 +0000
Subject: [PATCH] Address code review: fix const-correctness, improve child
 registration, add comments

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
 src/ast/euf/euf_sgraph.cpp | 12 +++++++-----
 src/ast/euf/euf_snode.h    | 24 +++++++++++++++++++-----
 2 files changed, 26 insertions(+), 10 deletions(-)

diff --git a/src/ast/euf/euf_sgraph.cpp b/src/ast/euf/euf_sgraph.cpp
index b35b65b1a..919bb0e0d 100644
--- a/src/ast/euf/euf_sgraph.cpp
+++ b/src/ast/euf/euf_sgraph.cpp
@@ -142,6 +142,8 @@ namespace euf {
         }
 
         case snode_kind::s_power: {
+            // s^n: nullable follows base, consistent with ZIPT's PowerToken
+            // the exponent n is assumed to be a symbolic integer, may or may not be zero
             SASSERT(n->num_args() >= 1);
             snode* base = n->arg(0);
             n->m_ground = base->is_ground();
@@ -278,14 +280,14 @@ namespace euf {
         app* a = to_app(e);
         unsigned arity = a->get_num_args();
 
-        // recursively register children that are sequences or regexes
+        // recursively register children
+        // for seq/re children, create classified snodes
+        // for other children (e.g. integer exponents), create s_other snodes
         snode_vector child_nodes;
         for (unsigned i = 0; i < arity; ++i) {
             expr* ch = a->get_arg(i);
-            if (m_seq.is_seq(ch) || m_seq.is_re(ch)) {
-                snode* cn = mk(ch);
-                child_nodes.push_back(cn);
-            }
+            snode* cn = mk(ch);
+            child_nodes.push_back(cn);
         }
 
         return mk_snode(e, k, child_nodes.size(), child_nodes.data());
diff --git a/src/ast/euf/euf_snode.h b/src/ast/euf/euf_snode.h
index d87a4382d..149ebbdcf 100644
--- a/src/ast/euf/euf_snode.h
+++ b/src/ast/euf/euf_snode.h
@@ -67,7 +67,7 @@ namespace euf {
         unsigned    m_level      = 0;      // tree depth/level (0 for empty, 1 for singletons)
         unsigned    m_length     = 0;      // token count, number of leaf tokens in the tree
 
-        snode*      m_args[0];
+        snode*      m_args[0]; // variable-length array, allocated via get_snode_size(num_args)
 
         friend class sgraph;
 
@@ -129,18 +129,32 @@ namespace euf {
         }
 
         // analogous to ZIPT's Str.First / Str.Last
-        snode* first() const {
+        snode const* first() const {
             snode const* s = this;
             while (s->is_concat())
                 s = s->arg(0);
-            return const_cast<snode*>(s);
+            return s;
         }
 
-        snode* last() const {
+        snode const* last() const {
             snode const* s = this;
             while (s->is_concat())
                 s = s->arg(1);
-            return const_cast<snode*>(s);
+            return s;
+        }
+
+        snode* first() {
+            snode* s = this;
+            while (s->is_concat())
+                s = s->arg(0);
+            return s;
+        }
+
+        snode* last() {
+            snode* s = this;
+            while (s->is_concat())
+                s = s->arg(1);
+            return s;
         }
     };