str.at wants a special treatment...

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;
     }

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 {

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);

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