mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 05:18:44 +00:00
Code Activity

Fixed various signed/unsigned conversion warnings.

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2015-05-23 17:30:19 +01:00
parent f1cc1842e1
commit 4da7286a7b
2 changed files with 5 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/math/simplex/sparse_matrix.h
View file

@ -79,7 +79,7 @@ namespace simplex {
};
col_entry(int r, int i): m_row_id(r), m_row_idx(i) {}
col_entry(): m_row_id(0), m_row_idx(0) {}
bool is_dead() const { return m_row_id == dead_id; }
bool is_dead() const { return (unsigned) m_row_id == dead_id; }
};
struct column;

8
src/math/simplex/sparse_matrix_def.h
View file

@ -79,7 +79,7 @@ namespace simplex {
void sparse_matrix<Ext>::_row::del_row_entry(unsigned idx) {
_row_entry & t = m_entries[idx];
SASSERT(!t.is_dead());
t.m_next_free_row_entry_idx = m_first_free_idx;
t.m_next_free_row_entry_idx = (unsigned)m_first_free_idx;
t.m_var = dead_id;
m_size--;
m_first_free_idx = idx;
@ -513,8 +513,8 @@ namespace simplex {
SASSERT(!m.is_zero(e.m_coeff));
SASSERT(e.m_var != dead_id);
col_entry const& c = m_columns[e.m_var].m_entries[e.m_col_idx];
SASSERT(c.m_row_id == row_id);
SASSERT(c.m_row_idx == i);
SASSERT((unsigned)c.m_row_id == row_id);
SASSERT((unsigned)c.m_row_idx == i);
vars.insert(e.m_var);
}
int idx = r.m_first_free_idx;
@ -544,7 +544,7 @@ namespace simplex {
_row const& row = m_rows[c.m_row_id];
_row_entry const& r = row.m_entries[c.m_row_idx];
SASSERT(r.m_var == v);
SASSERT(r.m_col_idx == i);
SASSERT((unsigned)r.m_col_idx == i);
rows.insert(c.m_row_id);
}
int idx = col.m_first_free_idx;