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

remove some warnings

Browse source
This commit is contained in:
Lev Nachmanson 2024-12-20 13:59:43 -10:00 committed by Lev Nachmanson
parent 9a96aa94e6
commit fd3bd088a4
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

@ -305,7 +305,7 @@ namespace lp {
void fill_entry(const lar_term& t) { void fill_entry(const lar_term& t) {
TRACE("dioph_eq", print_lar_term_L(t, tout) << std::endl;); TRACE("dioph_eq", print_lar_term_L(t, tout) << std::endl;);
entry te = {lar_term(t.j()), mpq(0), entry_status::F}; entry te = {lar_term(t.j()), mpq(0), entry_status::F};
unsigned entry_index = m_entries.size(); unsigned entry_index = (unsigned) m_entries.size();
m_f.push_back(entry_index); m_f.push_back(entry_index);
m_entries.push_back(te); m_entries.push_back(te);
entry& e = m_entries.back(); entry& e = m_entries.back();
@ -1029,7 +1029,7 @@ namespace lp {
} }
unsigned get_number_of_int_inf() const { unsigned get_number_of_int_inf() const {
return std::count_if( return (unsigned) std::count_if(
lra.r_basis().begin(), lra.r_basis().end(), lra.r_basis().begin(), lra.r_basis().end(),
[this](unsigned j) { [this](unsigned j) {
return lia.column_is_int_inf(j); return lia.column_is_int_inf(j);
@ -1170,7 +1170,7 @@ namespace lp {
[ei](const auto& cell) { [ei](const auto& cell) {
return cell.var() == ei; return cell.var() == ei;
}); });
unsigned pivot_col_cell_index = std::distance(column.begin(), it); unsigned pivot_col_cell_index = (unsigned) std::distance(column.begin(), it);
if (pivot_col_cell_index != 0) { if (pivot_col_cell_index != 0) {
// swap the pivot column cell with the head cell // swap the pivot column cell with the head cell
auto c = column[0]; auto c = column[0];