diff --git a/src/ast/euf/euf_egraph.cpp b/src/ast/euf/euf_egraph.cpp
index d370ceed3..6c8cbda06 100644
--- a/src/ast/euf/euf_egraph.cpp
+++ b/src/ast/euf/euf_egraph.cpp
@@ -582,7 +582,6 @@ namespace euf {
 
     bool egraph::propagate() {
         force_push();
-        unsigned j = 0;
         for (unsigned i = 0; i < m_to_merge.size() && m.limit().inc() && !inconsistent(); ++i) {
             auto const& w = m_to_merge[i];
             switch (w.t) {
diff --git a/src/math/lp/bound_analyzer_on_row.h b/src/math/lp/bound_analyzer_on_row.h
index 576f14599..b4d587bec 100644
--- a/src/math/lp/bound_analyzer_on_row.h
+++ b/src/math/lp/bound_analyzer_on_row.h
@@ -286,6 +286,7 @@ private:
         unsigned row_index = this->m_row_index;
         auto* lar = &m_bp.lp();
         auto explain = [bound_j, coeff_before_j_is_pos, is_lower_bound, strict, row_index, lar]() {
+            (void) strict;
             TRACE("bound_analyzer", tout << "explain_bound_on_var_on_coeff, bound_j = " << bound_j << ", coeff_before_j_is_pos = " << coeff_before_j_is_pos << ", is_lower_bound = " << is_lower_bound << ", strict = " << strict << ", row_index = " << row_index << "\n";);
             int bound_sign = (is_lower_bound ? 1 : -1);
             int j_sign = (coeff_before_j_is_pos ? 1 : -1) * bound_sign;
diff --git a/src/math/lp/int_solver.cpp b/src/math/lp/int_solver.cpp
index b619b1c8a..c324af5b6 100644
--- a/src/math/lp/int_solver.cpp
+++ b/src/math/lp/int_solver.cpp
@@ -884,7 +884,7 @@ namespace lp {
         };
 
         auto _check_feasible = [&](void) {
-            auto st = lra.find_feasible_solution();
+            lra.find_feasible_solution();
             if (!lra.is_feasible() && !settings().get_cancel_flag()) {
                 lra.get_infeasibility_explanation(*m_ex);
                 return false;