From 233184944ca5e32c669ed5c7f10bef67109b303e Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 26 Nov 2025 09:43:52 -0800
Subject: [PATCH] fix build warnings

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/euf/euf_arith_plugin.cpp       | 1 -
 src/ast/euf/ho_matcher.cpp             | 3 +--
 src/ast/simplifiers/euf_completion.cpp | 2 +-
 src/nlsat/nlsat_solver.cpp             | 3 +--
 src/smt/smt_parallel.cpp               | 2 +-
 src/smt/smt_relevancy.cpp              | 1 -
 6 files changed, 4 insertions(+), 8 deletions(-)

diff --git a/src/ast/euf/euf_arith_plugin.cpp b/src/ast/euf/euf_arith_plugin.cpp
index 487cc1392..82ce7f2a9 100644
--- a/src/ast/euf/euf_arith_plugin.cpp
+++ b/src/ast/euf/euf_arith_plugin.cpp
@@ -59,7 +59,6 @@ namespace euf {
         expr* e = n->get_expr(), * x, * y;
         // x - y = x + (* -1 y)
         if (a.is_sub(e, x, y)) {
-            auto& m = g.get_manager();
             auto e1 = a.mk_numeral(rational(-1), a.is_int(x));
             auto n1 = g.find(e1) ? g.find(e1) : g.mk(e1, 0, 0, nullptr);
             auto e2 = a.mk_mul(e1, y);
diff --git a/src/ast/euf/ho_matcher.cpp b/src/ast/euf/ho_matcher.cpp
index 4a313ee61..696f868b2 100644
--- a/src/ast/euf/ho_matcher.cpp
+++ b/src/ast/euf/ho_matcher.cpp
@@ -293,8 +293,7 @@ namespace euf {
         // v - offset |-> t
         if (is_meta_var(p, wi.pat_offset()) && is_closed(t, 0, wi.term_offset())) {
             auto v = to_var(p);
-            auto idx = v->get_idx() - wi.pat_offset();
-            SASSERT(!m_subst.get(idx)); // reduce ensures meta variables are not in substitutions
+            SASSERT(!m_subst.get(v->get_idx() - wi.pat_offset()));  // reduce ensures meta variables are not in substitutions
             add_binding(v, wi.pat_offset(), t);
             wi.set_done();
             return true;
diff --git a/src/ast/simplifiers/euf_completion.cpp b/src/ast/simplifiers/euf_completion.cpp
index a78338226..1c33b63ba 100644
--- a/src/ast/simplifiers/euf_completion.cpp
+++ b/src/ast/simplifiers/euf_completion.cpp
@@ -1088,7 +1088,7 @@ namespace euf {
             verbose_stream() << mk_pp(s->get_expr(), m) << "\n";
         }
 #endif
-        auto n = m_egraph.find(q);
+        // auto n = m_egraph.find(q);
 #if 0
         verbose_stream() << "class of " << mk_pp(q, m) << "\n";
         for (auto s : euf::enode_class(n)) {
diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp
index 1283b20fe..1f1e21c93 100644
--- a/src/nlsat/nlsat_solver.cpp
+++ b/src/nlsat/nlsat_solver.cpp
@@ -984,8 +984,7 @@ namespace nlsat {
 
                 lbool val = l_undef;
                 // Arithmetic atom: evaluate directly
-                var max = a->max_var();
-                SASSERT(debug_assignment.is_assigned(max));
+                SASSERT(debug_assignment.is_assigned(a->max_var()));
                 val = to_lbool(debug_evaluator.eval(a, l.sign()));
                 SASSERT(val != l_undef);
                 if (val == l_true)
diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp
index 46b883b1e..3785d3738 100644
--- a/src/smt/smt_parallel.cpp
+++ b/src/smt/smt_parallel.cpp
@@ -131,7 +131,7 @@ namespace smt {
     }
 
     parallel::worker::worker(unsigned id, parallel &p, expr_ref_vector const &_asms)
-        : id(id), p(p), b(p.m_batch_manager), m_smt_params(p.ctx.get_fparams()), asms(m), m_g2l(p.ctx.m, m),
+        : id(id), p(p), b(p.m_batch_manager), asms(m), m_smt_params(p.ctx.get_fparams()), m_g2l(p.ctx.m, m),
           m_l2g(m, p.ctx.m) {
         for (auto e : _asms)
             asms.push_back(m_g2l(e));
diff --git a/src/smt/smt_relevancy.cpp b/src/smt/smt_relevancy.cpp
index 48fa3657d..80fc9bc8d 100644
--- a/src/smt/smt_relevancy.cpp
+++ b/src/smt/smt_relevancy.cpp
@@ -385,7 +385,6 @@ namespace smt {
             case l_undef:
                 break;
             case l_true: {
-                expr* true_arg = nullptr;
                 auto arg0 = n->get_arg(0);
                 auto arg1 = n->get_arg(1);
                 if (m_context.find_assignment(arg0) == l_false) {