From 0fa1e75f3f5a356520d4e32eb78e89a57964632f Mon Sep 17 00:00:00 2001
From: CEisenhofer <clemens.eisenhofer@tuwien.ac.at>
Date: Wed, 27 May 2026 17:27:48 +0200
Subject: [PATCH] Remove redundant function

---
 src/smt/seq/seq_nielsen.cpp | 3 +--
 src/smt/seq/seq_nielsen.h   | 4 ----
 2 files changed, 1 insertion(+), 6 deletions(-)

diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp
index 5d7c5166e..70aa963bf 100644
--- a/src/smt/seq/seq_nielsen.cpp
+++ b/src/smt/seq/seq_nielsen.cpp
@@ -336,8 +336,7 @@ namespace seq {
         }
         m_constraints.push_back(c);
     }
-    euf::snode *nielsen_graph::mk_fresh_char_var() {}
-
+    
     void nielsen_node::apply_subst(euf::sgraph& sg, nielsen_subst const& s) {
         SASSERT(!s.m_var->is_char_or_unit() || s.m_replacement->is_char_or_unit());
         SASSERT(s.m_var);
diff --git a/src/smt/seq/seq_nielsen.h b/src/smt/seq/seq_nielsen.h
index 9c7f2cced..de5c17bec 100644
--- a/src/smt/seq/seq_nielsen.h
+++ b/src/smt/seq/seq_nielsen.h
@@ -1195,10 +1195,6 @@ namespace seq {
         // create a fresh variable with a unique name and the given sequence sort
         euf::snode* mk_fresh_var(sort* s);
 
-        // create a fresh symbolic character: seq.unit(fresh_char_const)
-        // analogous to ZIPT's SymCharToken creation
-        euf::snode* mk_fresh_char_var();
-
         // deterministic modifier: var = ε, same-head cancel
         bool apply_det_modifier(nielsen_node* node);