From 7dcebcdb0a23c371bd830100d36cdd07d04af426 Mon Sep 17 00:00:00 2001
From: CEisenhofer <clemens.eisenhofer@tuwien.ac.at>
Date: Thu, 5 Mar 2026 17:14:54 +0100
Subject: [PATCH] A bit cleanup

---
 src/ast/euf/euf_sgraph.cpp  | 2 +-
 src/smt/seq/seq_nielsen.cpp | 4 ----
 src/smt/seq/seq_nielsen.h   | 8 --------
 3 files changed, 1 insertion(+), 13 deletions(-)

diff --git a/src/ast/euf/euf_sgraph.cpp b/src/ast/euf/euf_sgraph.cpp
index 1bd2a8d8b..d12e16d7c 100644
--- a/src/ast/euf/euf_sgraph.cpp
+++ b/src/ast/euf/euf_sgraph.cpp
@@ -575,7 +575,7 @@ namespace euf {
         if (!re || !re->get_expr())
             return;
         expr* e = re->get_expr();
-        expr* ch = nullptr, *lo = nullptr, *hi = nullptr;
+        expr* lo = nullptr, *hi = nullptr;
         // leaf regex predicates: character ranges and single characters
         if (m_seq.re.is_range(e, lo, hi)) {
             preds.push_back(e);
diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp
index 23c1ce0d3..e4a6daa75 100644
--- a/src/smt/seq/seq_nielsen.cpp
+++ b/src/smt/seq/seq_nielsen.cpp
@@ -868,10 +868,6 @@ namespace seq {
         return search_result::unknown;
     }
 
-    simplify_result nielsen_graph::simplify_node(nielsen_node* node) {
-        return node->simplify_and_init(*this);
-    }
-
     bool nielsen_graph::apply_det_modifier(nielsen_node* node) {
         for (str_eq const& eq : node->str_eqs()) {
             if (eq.is_trivial())
diff --git a/src/smt/seq/seq_nielsen.h b/src/smt/seq/seq_nielsen.h
index 9f7735699..0251e47e5 100644
--- a/src/smt/seq/seq_nielsen.h
+++ b/src/smt/seq/seq_nielsen.h
@@ -594,12 +594,7 @@ namespace seq {
         ptr_vector<nielsen_node> const& nodes() const { return m_nodes; }
         unsigned num_nodes() const { return m_nodes.size(); }
 
-        // depth bound for iterative deepening
-        unsigned depth_bound() const { return m_depth_bound; }
-        void set_depth_bound(unsigned d) { m_depth_bound = d; }
-
         // maximum overall search depth (0 = unlimited)
-        unsigned max_search_depth() const { return m_max_search_depth; }
         void set_max_search_depth(unsigned d) { m_max_search_depth = d; }
 
         // generate next unique regex membership id
@@ -626,9 +621,6 @@ namespace seq {
         // main search entry point: iterative deepening DFS
         search_result solve();
 
-        // simplify a node's constraints (delegate to node)
-        simplify_result simplify_node(nielsen_node* node);
-
         // generate child nodes by applying modifier rules
         // returns true if at least one child was generated
         bool generate_extensions(nielsen_node *node);