diff --git a/src/ast/euf/euf_sgraph.cpp b/src/ast/euf/euf_sgraph.cpp
index 36eb25dcb..3af0fa955 100644
--- a/src/ast/euf/euf_sgraph.cpp
+++ b/src/ast/euf/euf_sgraph.cpp
@@ -104,11 +104,7 @@ namespace euf {
         if (m_seq.str.is_in_re(e))
             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) || m_seq.str.is_at(e)))
-            return snode_kind::s_var;
-
-        return snode_kind::s_unknown; // it is an element of the seq
+        return snode_kind::s_var;
     }
 
     void sgraph::compute_metadata(snode* n) {
@@ -473,8 +469,6 @@ 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));
diff --git a/src/ast/euf/euf_snode.h b/src/ast/euf/euf_snode.h
index 85bbbc4fe..b2241f0ee 100644
--- a/src/ast/euf/euf_snode.h
+++ b/src/ast/euf/euf_snode.h
@@ -52,8 +52,7 @@ namespace euf {
         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_unknown,     // something else
+        s_in_re        // regex membership (OP_SEQ_IN_RE)
     };
 
     class snode {