From 9a237d55ca46e92487d3aa55ffb50ed35d09817e Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 11 Jan 2025 17:41:24 -0800
Subject: [PATCH] fix misc build warnings

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/sls/sls_arith_base.cpp | 4 +---
 src/math/lp/lar_solver.cpp     | 2 +-
 src/smt/smt_internalizer.cpp   | 2 --
 3 files changed, 2 insertions(+), 6 deletions(-)

diff --git a/src/ast/sls/sls_arith_base.cpp b/src/ast/sls/sls_arith_base.cpp
index 1e6eef3a3..12b00c5a8 100644
--- a/src/ast/sls/sls_arith_base.cpp
+++ b/src/ast/sls/sls_arith_base.cpp
@@ -724,7 +724,6 @@ namespace sls {
 
         for (auto idx : vi.m_adds) {
             auto const& ad = m_adds[idx];
-            auto w = ad.m_var;
             num_t sum(ad.m_coeff);
             for (auto const& [coeff, w] : ad.m_args)
                 sum += coeff * value(w);
@@ -2265,7 +2264,7 @@ namespace sls {
             return value(v) == (value(od.m_arg2) == 0 ? num_t(0) : mod(value(od.m_arg1), value(od.m_arg2)));
         }
         case arith_op_kind::OP_POWER: {
-            auto od = m_ops[vi.m_def_idx];
+            //auto od = m_ops[vi.m_def_idx];
             NOT_IMPLEMENTED_YET();
             break;
         }
@@ -2333,7 +2332,6 @@ namespace sls {
                 display(out, ad) << "\n";
             }
         };
-        auto& out = verbose_stream();
         for (var_t v = 0; v < m_vars.size(); ++v) {
             if (!eval_is_correct(v)) {
                 report_error(verbose_stream(), v);
diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp
index 16d851e87..3d8a18386 100644
--- a/src/math/lp/lar_solver.cpp
+++ b/src/math/lp/lar_solver.cpp
@@ -699,7 +699,7 @@ namespace lp {
             return;
         
         lar_term t;
-        auto const& col = m_columns[j];
+        //auto const& col = m_columns[j];
         auto const& r = basic2row(j);
         for (auto const& c : r) {
             if (c.var() != j)       
diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp
index f19144b62..17c0033f0 100644
--- a/src/smt/smt_internalizer.cpp
+++ b/src/smt/smt_internalizer.cpp
@@ -1433,12 +1433,10 @@ namespace smt {
             return nullptr;
         case 1: {
             literal unit = lits[0];
-            expr* atom = m_bool_var2expr[unit.var()];
             if (j && !j->in_region())
                 m_justifications.push_back(j);
             assign(unit, j);
             inc_ref(unit);
-            // m_units_to_reassert.push_back({ expr_ref(atom, m), unit.sign(), is_relevant(unit) });
             return nullptr;
         }
         case 2: