From 26440ed3d807cc5134ceefef28a3bd7d9ac367c4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 29 Nov 2023 15:45:19 -0800 Subject: [PATCH] deal with ubuntu/clang warnings Signed-off-by: Nikolaj Bjorner --- src/ast/euf/euf_egraph.cpp | 1 - src/math/lp/bound_analyzer_on_row.h | 1 + src/math/lp/int_solver.cpp | 2 +- 3 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/ast/euf/euf_egraph.cpp b/src/ast/euf/euf_egraph.cpp index d370ceed3c4..6c8cbda0690 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 576f1459968..b4d587bec2d 100644 --- a/src/math/lp/bound_analyzer_on_row.h +++ b/src/math/lp/bound_analyzer_on_row.h @@ -286,6 +286,7 @@ public : 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 b619b1c8a12..c324af5b600 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;