From 472d9bde6cef1bab075ed56dc97891cff8f1571b Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Tue, 10 Mar 2026 18:52:40 +0000
Subject: [PATCH] Fix unused variable build warnings in theory_finite_set,
 theory_finite_set_size, theory_nseq

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
 src/smt/theory_finite_set.cpp      | 5 +----
 src/smt/theory_finite_set_size.cpp | 1 -
 src/smt/theory_nseq.cpp            | 7 ++-----
 3 files changed, 3 insertions(+), 10 deletions(-)

diff --git a/src/smt/theory_finite_set.cpp b/src/smt/theory_finite_set.cpp
index 44c51d7dc..845914427 100644
--- a/src/smt/theory_finite_set.cpp
+++ b/src/smt/theory_finite_set.cpp
@@ -171,7 +171,6 @@ namespace smt {
     void theory_finite_set::add_in_axioms(enode *in, var_data *d) {
         SASSERT(u.is_in(in->get_expr()));
         auto e = in->get_arg(0)->get_expr();
-        auto set1 = in->get_arg(1);
         for (enode *setop : d->m_parent_setops) {
             SASSERT(
                 any_of(enode::args(setop), [&](enode *arg) { return in->get_arg(1)->get_root() == arg->get_root(); }));
@@ -437,12 +436,11 @@ namespace smt {
                     return lit == arg;
             };
             auto lit1 = clause.get(0);
-            auto lit2 = clause.get(1);
             auto position = 0;
             if (is_complement_to(is_true, lit1, e))
                 position = 0;
             else {
-                SASSERT(is_complement_to(is_true, lit2, e));
+                SASSERT(is_complement_to(is_true, clause.get(1), e));
                 position = 1;
             }
             
@@ -833,7 +831,6 @@ namespace smt {
         }
 
         app *mk_range_value(model_generator &mg, expr_ref_vector const &values) {
-            unsigned i = 0;
             arith_value av(th.m);
             av.init(&th.ctx);
             vector<std::tuple<rational, enode *, bool>> elems;
diff --git a/src/smt/theory_finite_set_size.cpp b/src/smt/theory_finite_set_size.cpp
index 2bae076d6..d9c4a9ddf 100644
--- a/src/smt/theory_finite_set_size.cpp
+++ b/src/smt/theory_finite_set_size.cpp
@@ -201,7 +201,6 @@ namespace smt {
         for (auto [a, b] : th.m_diseqs) {
             auto x = th.get_enode(a);
             auto y = th.get_enode(b);
-            diseq d = {a, b};
             if (n2b.contains(x) && n2b.contains(y)) {
                 arith_util a(m);
                 auto d1 = mk_diff(x, y);
diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp
index 5e11fe7cf..46673e91f 100644
--- a/src/smt/theory_nseq.cpp
+++ b/src/smt/theory_nseq.cpp
@@ -54,7 +54,6 @@ namespace smt {
 
     bool theory_nseq::internalize_atom(app* atom, bool /*gate_ctx*/) {
         context& ctx = get_context();
-        ast_manager& m = get_manager();
 
         // str.in_re atoms are boolean predicates: register as bool_var
         // so that assign_eh fires when the SAT solver assigns them.
@@ -761,7 +760,6 @@ namespace smt {
 
     bool theory_nseq::propagate_length_lemma(literal lit, seq::length_constraint const& lc) {
         context& ctx = get_context();
-        ast_manager& m = get_manager();
 
         // unconditional constraints: assert as theory axiom
         if (lc.m_kind == seq::length_kind::nonneg) {
@@ -783,7 +781,7 @@ namespace smt {
                 lit));
         ctx.assign(lit, js);
 
-        TRACE(seq, tout << "nseq length propagation: " << mk_pp(lc.m_expr, m)
+        TRACE(seq, tout << "nseq length propagation: " << mk_pp(lc.m_expr, get_manager())
                         << " (" << eqs.size() << " eqs, " << lits.size() << " lits)\n";);
         ++m_num_length_axioms;
         return true;
@@ -813,7 +811,6 @@ namespace smt {
     }
 
     bool theory_nseq::assert_length_constraints() {
-        ast_manager& m = get_manager();
         context& ctx = get_context();
         vector<seq::length_constraint> constraints;
         m_nielsen.generate_length_constraints(constraints);
@@ -825,7 +822,7 @@ namespace smt {
                 ctx.internalize(e, true);
             literal lit = ctx.get_literal(e);
             if (ctx.get_assignment(lit) != l_true) {
-                TRACE(seq, tout << "nseq length lemma: " << mk_pp(e, m) << "\n";);
+                TRACE(seq, tout << "nseq length lemma: " << mk_pp(e, get_manager()) << "\n";);
                 propagate_length_lemma(lit, lc);
                 new_axiom = true;
             }