From 7502e3c4092a1683d98101c6d35291f1c66801a5 Mon Sep 17 00:00:00 2001
From: davedets <daviddetlefs@gmail.com>
Date: Thu, 30 Jul 2026 13:41:20 -0700
Subject: [PATCH] Remove new instances of unused local vars and functions
 (#10309)

A few seem to have crept in.  Verified with both dbg and release builds.
---
 src/ast/pattern/pattern_inference.cpp   | 1 -
 src/ast/rewriter/seq_range_collapse.cpp | 4 ----
 src/cmd_context/tptp_frontend.cpp       | 1 -
 3 files changed, 6 deletions(-)

diff --git a/src/ast/pattern/pattern_inference.cpp b/src/ast/pattern/pattern_inference.cpp
index ff0ab73160..7eda82f75a 100644
--- a/src/ast/pattern/pattern_inference.cpp
+++ b/src/ast/pattern/pattern_inference.cpp
@@ -195,7 +195,6 @@ void pattern_inference_cfg::collect::save_candidate(expr * n, unsigned delta) {
     }
     case AST_APP: {
         app *       c    = to_app(n);
-        func_decl * decl = c->get_decl();
         if (m_owner.is_forbidden(c)) {
             save(n, delta, nullptr);
             return;
diff --git a/src/ast/rewriter/seq_range_collapse.cpp b/src/ast/rewriter/seq_range_collapse.cpp
index 4ddcf1048b..2a657aaebe 100644
--- a/src/ast/rewriter/seq_range_collapse.cpp
+++ b/src/ast/rewriter/seq_range_collapse.cpp
@@ -202,10 +202,6 @@ namespace seq {
         return false;
     }
 
-    static expr_ref mk_unit_string_from_char(seq_util& u, unsigned c) {
-        return expr_ref(u.str.mk_string(zstring(c)), u.get_manager());
-    }
-
     static expr_ref mk_single_range_regex(seq_util& u, unsigned lo, unsigned hi, sort* re_sort) {
         ast_manager& m = u.get_manager();
         return expr_ref(u.re.mk_range(re_sort, lo, hi), m);
diff --git a/src/cmd_context/tptp_frontend.cpp b/src/cmd_context/tptp_frontend.cpp
index 9409614b50..0149de1128 100644
--- a/src/cmd_context/tptp_frontend.cpp
+++ b/src/cmd_context/tptp_frontend.cpp
@@ -2952,7 +2952,6 @@ static unsigned read_tptp_stream(std::istream& in, char const* current_file) {
         if (char const* dump_path = getenv("Z3_TPTP_DUMP_SMT2")) {
             std::ofstream dout(dump_path);
             if (dout) {
-                ast_manager& m = ctx.m();
                 dout << "; Auto-generated from TPTP input: "
                      << (current_file ? current_file : "?") << "\n";
                 dout << "(set-logic ALL)\n";