From ef55de16461d5079804c14e80cd2af3349d8e95a Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Thu, 23 Jan 2025 16:12:12 -1000
Subject: [PATCH] fix out of bounds bug
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
src/math/lp/dioph_eq.cpp | 15 ++++++++-------
src/math/lp/indexed_vector.h | 2 +-
src/math/lp/indexed_vector_def.h | 2 +-
3 files changed, 10 insertions(+), 9 deletions(-)
diff --git a/src/math/lp/dioph_eq.cpp b/src/math/lp/dioph_eq.cpp
index 1318a38d0..36a81a9d8 100644
--- a/src/math/lp/dioph_eq.cpp
+++ b/src/math/lp/dioph_eq.cpp
@@ -63,7 +63,7 @@ namespace lp {
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) {
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("dioph_eq", lra.print_term(*t, tout); tout << ", t->j() =" << t->j() << std::endl;);
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 ((unsigned)i != m_added_terms.size() -1)
m_added_terms[i] = m_added_terms.back();
@@ -388,7 +388,7 @@ namespace lp {
};
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)) {
remove_from_S(ei);
@@ -487,7 +487,7 @@ namespace lp {
void remove_last_row_in_matrix(static_matrix<mpq, mpq>& m) {
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.m_rows.pop_back();
@@ -609,6 +609,7 @@ namespace lp {
SASSERT(entry_invariant(entry_index));
}
void subs_entry(unsigned ei) {
+ if (ei >= m_entries.size()) return;
std::queue<unsigned> q;
for (const auto& p: m_e_matrix.m_rows[ei]) {
if (can_substitute(p.var()))
@@ -754,9 +755,9 @@ namespace lp {
fresh_entries_to_remove.pop_back();
const fresh_definition & fd = m_fresh_definitions[xt];
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
- 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
// but we might need to recalculate last_ei, which becomes fd.m_ei
if (contains(entries_to_recalculate, last_ei )) {
@@ -1786,7 +1787,7 @@ namespace lp {
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) {
auto& c = column[cell_to_process];
if (belongs_to_s(c.var())) {
diff --git a/src/math/lp/indexed_vector.h b/src/math/lp/indexed_vector.h
index 4451a1428..66208fdba 100644
--- a/src/math/lp/indexed_vector.h
+++ b/src/math/lp/indexed_vector.h
@@ -80,7 +80,7 @@ public:
void resize(unsigned data_size);
unsigned data_size() const {
- return m_data.size();
+ return static_cast<unsigned>(m_data.size());
}
unsigned size() const {
diff --git a/src/math/lp/indexed_vector_def.h b/src/math/lp/indexed_vector_def.h
index 55faaf555..1bb05ce84 100644
--- a/src/math/lp/indexed_vector_def.h
+++ b/src/math/lp/indexed_vector_def.h
@@ -51,7 +51,7 @@ void indexed_vector<T>::clear() {
}
template <typename T>
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();
m_index.resize(0);
}