mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

fix some warnings

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-01-20 14:58:24 -08:00 committed by Lev Nachmanson
parent 7bba8bc0c9
commit 0e71adfa35
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/math/lp/dioph_eq.cpp
View file

@ -289,7 +289,7 @@ namespace lp {
if (!contains(m_active_terms, t)) { if (!contains(m_active_terms, t)) {
for (int i = m_added_terms.size() - 1; i >= 0; --i) { for (int i = m_added_terms.size() - 1; i >= 0; --i) {
if (m_added_terms[i] != t) continue; if (m_added_terms[i] != t) continue;
if (i != m_added_terms.size() -1) if ((unsigned)i != m_added_terms.size() -1)
m_added_terms[i] = m_added_terms.back(); m_added_terms[i] = m_added_terms.back();
m_added_terms.pop_back(); m_added_terms.pop_back();
break; // all is done since the term has not made it to m_active_terms break; // all is done since the term has not made it to m_active_terms
@ -350,7 +350,7 @@ namespace lp {
make_sure_j_is_in_the_last_row_of_l_matrix(); make_sure_j_is_in_the_last_row_of_l_matrix();
const auto &last_e_row = m_l_matrix.m_rows.back(); const auto &last_e_row = m_l_matrix.m_rows.back();
mpq alpha; mpq alpha;
for (const auto p: last_e_row) { for (const auto& p: last_e_row) {
if (p.var() == j) { if (p.var() == j) {
alpha = p.coeff(); alpha = p.coeff();
break; break;
@ -396,7 +396,7 @@ namespace lp {
unsigned j = m_l_matrix.column_count() - 1; unsigned j = m_l_matrix.column_count() - 1;
const auto &last_e_row = m_l_matrix.m_rows.back(); const auto &last_e_row = m_l_matrix.m_rows.back();
mpq alpha; mpq alpha;
for (const auto p: last_e_row) { for (const auto& p: last_e_row) {
if (p.var() == j) { if (p.var() == j) {
return; return;
} }