diff --git a/src/ast/euf/euf_sgraph.cpp b/src/ast/euf/euf_sgraph.cpp
index a080ab3fa..eff926004 100644
--- a/src/ast/euf/euf_sgraph.cpp
+++ b/src/ast/euf/euf_sgraph.cpp
@@ -289,6 +289,10 @@ namespace euf {
 
     static const unsigned HASH_BASE = 31;
 
+    // Compute a 2x2 polynomial hash matrix for associativity-respecting hashing.
+    // Unsigned overflow is intentional and well-defined (mod 2^32).
+    // M[0][0] tracks HASH_BASE^(num_leaves), which is always nonzero since
+    // HASH_BASE is odd. M[0][1] is the actual hash value.
     void sgraph::compute_hash_matrix(snode* n) {
         if (n->is_empty()) {
             // identity matrix: concat with empty is identity
@@ -310,6 +314,7 @@ namespace euf {
         }
         else {
             // leaf/token: [[HASH_BASE, value], [0, 1]]
+            // +1 avoids zero hash values; wraps safely on unsigned overflow
             unsigned v = n->get_expr() ? n->get_expr()->get_id() + 1 : n->id() + 1;
             n->m_hash_matrix[0][0] = HASH_BASE;
             n->m_hash_matrix[0][1] = v;
diff --git a/src/ast/euf/euf_snode.h b/src/ast/euf/euf_snode.h
index bf9ce293e..955dd3788 100644
--- a/src/ast/euf/euf_snode.h
+++ b/src/ast/euf/euf_snode.h
@@ -109,7 +109,9 @@ namespace euf {
         unsigned level()     const { return m_level; }
         unsigned length()    const { return m_length; }
 
-        // associativity-respecting hash: cached if the 2x2 matrix is non-zero
+        // associativity-respecting hash: cached if the 2x2 matrix is non-zero.
+        // M[0][0] = HASH_BASE^(num_leaves) which is always nonzero since HASH_BASE
+        // is odd and gcd(odd, 2^32) = 1, so the check is safe.
         bool has_cached_hash() const { return m_hash_matrix[0][0] != 0; }
         unsigned assoc_hash()  const { return m_hash_matrix[0][1]; }