From 14312ef8a33991aa4ac460225fc5fe42e7afc2b1 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Thu, 2 Nov 2023 15:34:41 -0700
Subject: [PATCH] remove some warnings with clang
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
src/math/grobner/pdd_solver.cpp | 3 +--
src/math/lp/lar_solver.cpp | 3 +--
2 files changed, 2 insertions(+), 4 deletions(-)
diff --git a/src/math/grobner/pdd_solver.cpp b/src/math/grobner/pdd_solver.cpp
index 3f41d07cf..10f1eb88f 100644
--- a/src/math/grobner/pdd_solver.cpp
+++ b/src/math/grobner/pdd_solver.cpp
@@ -122,8 +122,7 @@ namespace dd {
solver::scoped_process::~scoped_process() {
if (e) {
- pdd const& p = e->poly();
- SASSERT(!p.is_val());
+ SASSERT(!e->poly().is_val());
g.push_equation(processed, e);
}
}
diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp
index d7d3a684a..5795e1665 100644
--- a/src/math/lp/lar_solver.cpp
+++ b/src/math/lp/lar_solver.cpp
@@ -316,7 +316,6 @@ namespace lp {
// get dependencies of the corresponding bounds from max_coeffs
u_dependency* lar_solver::get_dependencies_of_maximum(const vector<std::pair<mpq,lpvar>>& max_coeffs) {
- const auto& s = this->m_mpq_lar_core_solver.m_r_solver;
// The linear combinations of d_j*x[j] = the term that got maximized, where (d_j, j) is in max_coeffs
// Every j with positive coeff is at its upper bound,
// and every j with negative coeff is at its lower bound: so the sum cannot be increased.
@@ -326,7 +325,7 @@ namespace lp {
SASSERT (!d_j.is_zero());
TRACE("lar_solver_improve_bounds", tout << "d[" << j << "] = " << d_j << "\n";
- s.print_column_info(j, tout););
+ this->m_mpq_lar_core_solver.m_r_solver.print_column_info(j, tout););
const ul_pair& ul = m_columns_to_ul_pairs[j];
u_dependency * bound_dep;
if (d_j.is_pos())