From 1510b3112ef0d9689ef04121258cb056803e5aba Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 14 Apr 2025 10:33:14 -0700
Subject: [PATCH] fix build warnings

---
 src/ast/sls/sls_bv_fixed.cpp           | 1 -
 src/ast/sls/sls_bv_fixed.h             | 1 -
 src/ast/sls/sls_bv_terms.cpp           | 1 -
 src/ast/sls/sls_bv_terms.h             | 1 -
 src/ast/sls/sls_context.h              | 1 -
 src/qe/mbp/mbp_arrays_tg.cpp           | 1 -
 src/tactic/arith/fix_dl_var_tactic.cpp | 1 -
 7 files changed, 7 deletions(-)

diff --git a/src/ast/sls/sls_bv_fixed.cpp b/src/ast/sls/sls_bv_fixed.cpp
index 34e45ee4f..7a4c852ef 100644
--- a/src/ast/sls/sls_bv_fixed.cpp
+++ b/src/ast/sls/sls_bv_fixed.cpp
@@ -21,7 +21,6 @@ namespace sls {
 
     bv_fixed::bv_fixed(bv_eval& ev, bv_terms& terms, sls::context& ctx) :
         ev(ev),
-        terms(terms),
         m(ev.m),
         bv(ev.bv),
         ctx(ctx)
diff --git a/src/ast/sls/sls_bv_fixed.h b/src/ast/sls/sls_bv_fixed.h
index d175e9d6a..96799111d 100644
--- a/src/ast/sls/sls_bv_fixed.h
+++ b/src/ast/sls/sls_bv_fixed.h
@@ -29,7 +29,6 @@ namespace sls {
     
     class bv_fixed {
         bv_eval&        ev;
-        bv_terms&       terms;
         ast_manager&    m;
         bv_util&        bv;
         sls::context&   ctx;
diff --git a/src/ast/sls/sls_bv_terms.cpp b/src/ast/sls/sls_bv_terms.cpp
index fe44d109b..a88b16cb3 100644
--- a/src/ast/sls/sls_bv_terms.cpp
+++ b/src/ast/sls/sls_bv_terms.cpp
@@ -24,7 +24,6 @@ Author:
 namespace sls {
 
     bv_terms::bv_terms(sls::context& ctx):
-        ctx(ctx),
         m(ctx.get_manager()), 
         bv(m),
         m_axioms(m) {}
diff --git a/src/ast/sls/sls_bv_terms.h b/src/ast/sls/sls_bv_terms.h
index 5dbf8d72f..062cfaec0 100644
--- a/src/ast/sls/sls_bv_terms.h
+++ b/src/ast/sls/sls_bv_terms.h
@@ -29,7 +29,6 @@ Author:
 namespace sls {
 
     class bv_terms {
-        context&            ctx;
         ast_manager&        m;
         bv_util             bv;
         expr_ref_vector     m_axioms;
diff --git a/src/ast/sls/sls_context.h b/src/ast/sls/sls_context.h
index 818f2a9f3..4178c9d05 100644
--- a/src/ast/sls/sls_context.h
+++ b/src/ast/sls/sls_context.h
@@ -125,7 +125,6 @@ namespace sls {
         random_gen m_rand;
         bool m_initialized = false;
         bool m_new_constraint = false;
-        bool m_dirty = false;
         expr_ref_vector m_input_assertions;
         expr_ref_vector m_allterms;
         ptr_vector<expr> m_subterms;
diff --git a/src/qe/mbp/mbp_arrays_tg.cpp b/src/qe/mbp/mbp_arrays_tg.cpp
index 40c3360f4..3d1c825f5 100644
--- a/src/qe/mbp/mbp_arrays_tg.cpp
+++ b/src/qe/mbp/mbp_arrays_tg.cpp
@@ -414,7 +414,6 @@ struct mbp_array_tg::impl {
             expr* a1 = e1->get_arg(0);
             for (unsigned j = i + 1; j < rdTerms.size(); j++) {
                 app* e2 = rdTerms.get(j);
-                expr* a2 = e2->get_arg(0);
                 if (!is_seen(e1, e2) && a1 == e2) {
                     mark_seen(e1, e2);
                     progress = true;
diff --git a/src/tactic/arith/fix_dl_var_tactic.cpp b/src/tactic/arith/fix_dl_var_tactic.cpp
index 7a51d01fe..015108cc3 100644
--- a/src/tactic/arith/fix_dl_var_tactic.cpp
+++ b/src/tactic/arith/fix_dl_var_tactic.cpp
@@ -245,7 +245,6 @@ class fix_dl_var_tactic : public tactic {
         void operator()(goal_ref const & g, 
                         goal_ref_buffer & result) {
             tactic_report report("fix-dl-var", *g);
-            bool produce_proofs = g->proofs_enabled();
             m_produce_models    = g->models_enabled();
             TRACE("fix_dl_var", g->display(tout););