mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 09:55:19 +00:00
Code Activity

remove some warnings with clang

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2023-11-02 15:34:41 -07:00
parent 08d3a82ce0
commit 14312ef8a3
2 changed files with 2 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/math/grobner/pdd_solver.cpp
View file

@ -122,8 +122,7 @@ namespace dd {
solver::scoped_process::~scoped_process() { solver::scoped_process::~scoped_process() {
if (e) { if (e) {
pdd const& p = e->poly(); SASSERT(!e->poly().is_val());
SASSERT(!p.is_val());
g.push_equation(processed, e); g.push_equation(processed, e);
} }
} }

3
src/math/lp/lar_solver.cpp
View file

@ -316,7 +316,6 @@ namespace lp {
// get dependencies of the corresponding bounds from max_coeffs // 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) { 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 // 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, // 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. // 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()); SASSERT (!d_j.is_zero());
TRACE("lar_solver_improve_bounds", tout << "d[" << j << "] = " << d_j << "\n"; 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]; const ul_pair& ul = m_columns_to_ul_pairs[j];
u_dependency * bound_dep; u_dependency * bound_dep;
if (d_j.is_pos()) if (d_j.is_pos())