diff --git a/src/ast/euf/euf_snode.h b/src/ast/euf/euf_snode.h
index 955dd3788..e54d276f6 100644
--- a/src/ast/euf/euf_snode.h
+++ b/src/ast/euf/euf_snode.h
@@ -178,9 +178,8 @@ namespace euf {
                 arg(0)->collect_tokens(tokens);
                 arg(1)->collect_tokens(tokens);
             }
-            else if (!is_empty()) {
+            else if (!is_empty())
                 tokens.push_back(const_cast<snode*>(this));
-            }
         }
 
         // access the i-th token (0-based, left-to-right order)
diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp
index 010a06a8c..d6d7de50c 100644
--- a/src/smt/seq/seq_nielsen.cpp
+++ b/src/smt/seq/seq_nielsen.cpp
@@ -879,6 +879,19 @@ namespace seq {
         return search_result::unknown;
     }
 
+    // Returns true if variable snode `var` appears anywhere in the token list of `n`.
+    static bool snode_contains_var(euf::snode const* n, euf::snode const* var) {
+        if (!n || !var)
+            return false;
+        euf::snode_vector tokens;
+        n->collect_tokens(tokens);
+        for (const euf::snode* t : tokens) {
+            if (t == var)
+                return true;
+        }
+        return false;
+    }
+
     bool nielsen_graph::apply_det_modifier(nielsen_node* node) {
         for (str_eq const& eq : node->str_eqs()) {
             if (eq.is_trivial())
@@ -886,28 +899,23 @@ namespace seq {
             if (!eq.m_lhs || !eq.m_rhs)
                 continue;
 
-            euf::snode_vector lhs_toks, rhs_toks;
-            eq.m_lhs->collect_tokens(lhs_toks);
-            eq.m_rhs->collect_tokens(rhs_toks);
-            if (lhs_toks.empty() || rhs_toks.empty())
-                continue;
-
-            euf::snode* lhead = lhs_toks[0];
-            euf::snode* rhead = rhs_toks[0];
-
-            // variable definition: x = t where x ∉ vars(t) → subst x → t
-            if (lhead->is_var() && eq.m_rhs->is_empty()) {
-                nielsen_node* child = mk_child(node);
-                nielsen_edge* e = mk_edge(node, child, true);
-                nielsen_subst s(lhead, m_sg.mk_empty(), eq.m_dep);
-                e->add_subst(s);
-                child->apply_subst(m_sg, s);
-                return true;
+            // variable definition: x = t where x is a single var and x ∉ vars(t)
+            // → deterministically substitute x → t throughout the node
+            euf::snode* var = nullptr;
+            euf::snode* def;
+            if (eq.m_lhs->is_var() && !snode_contains_var(eq.m_rhs, eq.m_lhs)) {
+                var = eq.m_lhs;
+                def = eq.m_rhs;
             }
-            if (rhead->is_var() && eq.m_lhs->is_empty()) {
+            else if (eq.m_rhs->is_var() && !snode_contains_var(eq.m_lhs, eq.m_rhs)) {
+                var = eq.m_rhs;
+                def = eq.m_lhs;
+            }
+
+            if (var) {
                 nielsen_node* child = mk_child(node);
                 nielsen_edge* e = mk_edge(node, child, true);
-                nielsen_subst s(rhead, m_sg.mk_empty(), eq.m_dep);
+                nielsen_subst s(var, def, eq.m_dep);
                 e->add_subst(s);
                 child->apply_subst(m_sg, s);
                 return true;
diff --git a/src/smt/seq/seq_nielsen.h b/src/smt/seq/seq_nielsen.h
index 0251e47e5..a892cbadb 100644
--- a/src/smt/seq/seq_nielsen.h
+++ b/src/smt/seq/seq_nielsen.h
@@ -349,7 +349,11 @@ namespace seq {
 
         nielsen_subst(): m_var(nullptr), m_replacement(nullptr) {}
         nielsen_subst(euf::snode* var, euf::snode* repl, dep_tracker const& dep):
-            m_var(var), m_replacement(repl), m_dep(dep) {}
+            m_var(var), m_replacement(repl), m_dep(dep) {
+            SASSERT(var != nullptr);
+            SASSERT(repl != nullptr);
+            SASSERT(var->is_var());
+        }
 
         // an eliminating substitution does not contain the variable in the replacement
         bool is_eliminating() const;