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 out of bounds bug

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-01-23 16:12:12 -10:00 committed by Lev Nachmanson
parent 3990df6d91
commit ef55de1646
3 changed files with 10 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -63,7 +63,7 @@ namespace lp {
return m_rev_map.find(b)->second; return m_rev_map.find(b)->second;
} }
unsigned size() const {return m_map.size();} unsigned size() const {return static_cast<unsigned>(m_map.size());}
void erase_val(unsigned b) { void erase_val(unsigned b) {
SASSERT(contains(m_rev_map, b) && contains(m_map, m_rev_map[b])); SASSERT(contains(m_rev_map, b) && contains(m_map, m_rev_map[b]));
@ -340,7 +340,7 @@ namespace lp {
TRACE("d_undo", tout << "t:"<< t<<", t->j():"<< t->j() << std::endl;); TRACE("d_undo", tout << "t:"<< t<<", t->j():"<< t->j() << std::endl;);
TRACE("dioph_eq", lra.print_term(*t, tout); tout << ", t->j() =" << t->j() << std::endl;); TRACE("dioph_eq", lra.print_term(*t, tout); tout << ", t->j() =" << t->j() << std::endl;);
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 = static_cast<int>(m_added_terms.size() - 1); i >= 0; --i) {
if (m_added_terms[i] != t) continue; if (m_added_terms[i] != t) continue;
if ((unsigned)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();
@ -388,7 +388,7 @@ namespace lp {
}; };
void remove_last_entry() { void remove_last_entry() {
unsigned ei = m_entries.size() - 1; unsigned ei = static_cast<unsigned>(m_entries.size() - 1);
if (m_k2s.has_val(ei)) { if (m_k2s.has_val(ei)) {
remove_from_S(ei); remove_from_S(ei);
@ -487,7 +487,7 @@ namespace lp {
void remove_last_row_in_matrix(static_matrix<mpq, mpq>& m) { void remove_last_row_in_matrix(static_matrix<mpq, mpq>& m) {
auto & last_row = m.m_rows.back(); auto & last_row = m.m_rows.back();
for (unsigned k = last_row.size(); k-- > 0;) { for (unsigned k = static_cast<unsigned>(last_row.size()); k-- > 0;) {
m.remove_element(last_row, last_row[k]); m.remove_element(last_row, last_row[k]);
} }
m.m_rows.pop_back(); m.m_rows.pop_back();
@ -609,6 +609,7 @@ namespace lp {
SASSERT(entry_invariant(entry_index)); SASSERT(entry_invariant(entry_index));
} }
void subs_entry(unsigned ei) { void subs_entry(unsigned ei) {
if (ei >= m_entries.size()) return;
std::queue<unsigned> q; std::queue<unsigned> q;
for (const auto& p: m_e_matrix.m_rows[ei]) { for (const auto& p: m_e_matrix.m_rows[ei]) {
if (can_substitute(p.var())) if (can_substitute(p.var()))
@ -754,9 +755,9 @@ namespace lp {
fresh_entries_to_remove.pop_back(); fresh_entries_to_remove.pop_back();
const fresh_definition & fd = m_fresh_definitions[xt]; const fresh_definition & fd = m_fresh_definitions[xt];
TRACE("d_once", print_entry(fd.m_ei, tout) << std::endl; tout << "xt:" << xt << std::endl;); TRACE("d_once", print_entry(fd.m_ei, tout) << std::endl; tout << "xt:" << xt << std::endl;);
unsigned last_ei = m_entries.size() - 1; unsigned last_ei = static_cast<unsigned>(m_entries.size() - 1);
if (fd.m_ei != last_ei) { // not the last entry if (fd.m_ei != last_ei) { // not the last entry
transpose_entries(fd.m_ei, m_entries.size() -1 ); transpose_entries(fd.m_ei, static_cast<unsigned>(m_entries.size() - 1));
// we are not going to recalculate fd.m_ei // we are not going to recalculate fd.m_ei
// but we might need to recalculate last_ei, which becomes fd.m_ei // but we might need to recalculate last_ei, which becomes fd.m_ei
if (contains(entries_to_recalculate, last_ei )) { if (contains(entries_to_recalculate, last_ei )) {
@ -1786,7 +1787,7 @@ namespace lp {
pivot_col_cell_index; pivot_col_cell_index;
} }
unsigned cell_to_process = column.size() - 1; unsigned cell_to_process = static_cast<unsigned>(column.size() - 1);
while (cell_to_process > 0) { while (cell_to_process > 0) {
auto& c = column[cell_to_process]; auto& c = column[cell_to_process];
if (belongs_to_s(c.var())) { if (belongs_to_s(c.var())) {

2
src/math/lp/indexed_vector.h
View file

@ -80,7 +80,7 @@ public:
void resize(unsigned data_size); void resize(unsigned data_size);
unsigned data_size() const { unsigned data_size() const {
return m_data.size(); return static_cast<unsigned>(m_data.size());
} }
unsigned size() const { unsigned size() const {

2
src/math/lp/indexed_vector_def.h
View file

@ -51,7 +51,7 @@ void indexed_vector<T>::clear() {
} }
template <typename T> template <typename T>
void indexed_vector<T>::clear_all() { void indexed_vector<T>::clear_all() {
unsigned i = m_data.size(); unsigned i = static_cast<unsigned>(m_data.size());
while (i--) m_data[i] = numeric_traits<T>::zero(); while (i--) m_data[i] = numeric_traits<T>::zero();
m_index.resize(0); m_index.resize(0);
} }