From 34cb0a17fc544cdddbe0030f23d314d3c91e7a87 Mon Sep 17 00:00:00 2001
From: CEisenhofer <clemens.eisenhofer@tuwien.ac.at>
Date: Thu, 2 Apr 2026 18:33:44 +0200
Subject: [PATCH] str.at wants a special treatment...

---
 src/ast/euf/euf_sgraph.cpp  | 9 ++++-----
 src/ast/euf/euf_snode.h     | 1 +
 src/smt/seq/seq_nielsen.cpp | 5 ++++-
 src/smt/seq/seq_nielsen.h   | 1 +
 4 files changed, 10 insertions(+), 6 deletions(-)

diff --git a/src/ast/euf/euf_sgraph.cpp b/src/ast/euf/euf_sgraph.cpp
index ccadadc01..63a59ea1b 100644
--- a/src/ast/euf/euf_sgraph.cpp
+++ b/src/ast/euf/euf_sgraph.cpp
@@ -105,10 +105,10 @@ namespace euf {
             return snode_kind::s_in_re;
 
         // uninterpreted constants of string sort are variables
-        if (m_seq.is_seq(e->get_sort()) && (is_uninterp(e) || m_seq.is_skolem(e)))
+        if (m_seq.is_seq(e->get_sort()) && (is_uninterp(e) || m_seq.is_skolem(e) || m_seq.str.is_at(e)))
             return snode_kind::s_var;
 
-        return snode_kind::s_var;
+        return snode_kind::s_unknown; // it is an element of the seq
     }
 
     void sgraph::compute_metadata(snode* n) {
@@ -465,6 +465,8 @@ namespace euf {
     snode* sgraph::mk_concat(snode* a, snode* b) {
         if (a->is_empty()) return b;
         if (b->is_empty()) return a;
+        SASSERT(a->kind() != snode_kind::s_unknown);
+        SASSERT(b->kind() != snode_kind::s_unknown);
         if (m_seq.is_re(a->get_expr()))
             return mk(expr_ref(m_seq.re.mk_concat(a->get_expr(), b->get_expr()), m));
         return mk(expr_ref(m_seq.str.mk_concat(a->get_expr(), b->get_expr()), m));
@@ -520,9 +522,6 @@ namespace euf {
                 return mk_concat(s1, s2);
             return n;
         }
-        // substitution can also work for expressions under unit.
-        if (n->is_unit() && n->arg(0) == var)
-            return mk(m_seq.str.mk_unit(replacement->get_expr()));
         // for non-concat compound nodes (power, star, etc.), no substitution into children
         return n;
     }
diff --git a/src/ast/euf/euf_snode.h b/src/ast/euf/euf_snode.h
index c70eb18d9..b5f5b6a38 100644
--- a/src/ast/euf/euf_snode.h
+++ b/src/ast/euf/euf_snode.h
@@ -53,6 +53,7 @@ namespace euf {
         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_unknown,     // something else
     };
 
     class snode {
diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp
index 086eecc79..b86f110fc 100644
--- a/src/smt/seq/seq_nielsen.cpp
+++ b/src/smt/seq/seq_nielsen.cpp
@@ -1474,6 +1474,10 @@ namespace seq {
             bool ext = generate_extensions(node);
             IF_VERBOSE(1, display(verbose_stream(), node));
             CTRACE(seq, !ext, display(tout, node) << to_dot() << "\n");
+            if (!ext) {
+                node->to_html(std::cout, m);
+                std::cout << std::endl;
+            }
             VERIFY(ext);
             node->set_extended(true);
             ++m_stats.m_num_extensions;
@@ -1833,7 +1837,6 @@ namespace seq {
                 def = l->arg(0);
             }
 
-
             if (var) {
                 nielsen_node* child = mk_child(node);
                 nielsen_edge* e = mk_edge(node, child, true);
diff --git a/src/smt/seq/seq_nielsen.h b/src/smt/seq/seq_nielsen.h
index eeef89424..a17912f7c 100644
--- a/src/smt/seq/seq_nielsen.h
+++ b/src/smt/seq/seq_nielsen.h
@@ -432,6 +432,7 @@ namespace seq {
             SASSERT(repl != nullptr);
             // var may be s_var or s_power; sgraph::subst uses pointer identity matching
             SASSERT(var->is_var() || var->is_power() || var->is_unit());
+            SASSERT(!var->is_unit() || repl->is_char_or_unit());
         }
 
         // an eliminating substitution does not contain the variable in the replacement