From 3e24cb7c10007b25b4659d98f058319d56ed03c1 Mon Sep 17 00:00:00 2001
From: CEisenhofer <clemens.eisenhofer@tuwien.ac.at>
Date: Tue, 7 Apr 2026 09:33:14 +0200
Subject: [PATCH] Bug

---
 src/smt/seq/seq_nielsen.cpp | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp
index 0f21ce64e..73ba8889a 100644
--- a/src/smt/seq/seq_nielsen.cpp
+++ b/src/smt/seq/seq_nielsen.cpp
@@ -295,10 +295,10 @@ namespace seq {
                  mem.m_dep = m_graph.dep_mgr().mk_join(mem.m_dep, s.m_dep);
             }
         }
-        if (s.m_var->get_expr() && !sg.get_seq_util().is_seq(s.m_var->get_expr()) && !sg.get_seq_util().is_re(s.m_var->get_expr())) {
+        if (s.is_char_subst()) {
             expr* v = s.m_var->get_expr();
             expr* repl = s.m_replacement->get_expr();
-            
+
             expr* eq = sg.get_manager().mk_eq(v, repl);
             add_constraint(constraint(eq, s.m_dep, sg.get_manager()));
         }