mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-21 02:30:23 +00:00
Code Activity

remove all loop invariants

Browse source
This commit is contained in:
Chuyue Sun 2024-08-02 23:26:51 +00:00
parent 079db69b93
commit b6e9091385
1 changed files with 21 additions and 21 deletions
Download patch file Download diff file Expand all files Collapse all files

42
src/util/scoped_vector.h
View file

@ -188,32 +188,32 @@ private:
if (m_src_lim.size() != m_sizes.size() || m_src.size() != m_dst.size()) if (m_src_lim.size() != m_sizes.size() || m_src.size() != m_dst.size())
return false; return false;
// m_elems_lim stores the past sizes of m_elems for each scope. Each element in m_elems_lim should be // // m_elems_lim stores the past sizes of m_elems for each scope. Each element in m_elems_lim should be
// within bounds and in non-decreasing order. // // within bounds and in non-decreasing order.
for (unsigned i = 1; i < m_elems_lim.size(); ++i) { // for (unsigned i = 1; i < m_elems_lim.size(); ++i) {
if (m_elems_lim[i - 1] > m_elems_lim[i]) return false; // if (m_elems_lim[i - 1] > m_elems_lim[i]) return false;
} // }
// m_sizes tracks the size of the vector at each scope level. // // m_sizes tracks the size of the vector at each scope level.
// Each element in m_sizes should be non-decreasing and within the size of m_elems. // // Each element in m_sizes should be non-decreasing and within the size of m_elems.
for (unsigned i = 1; i < m_sizes.size(); ++i) { // for (unsigned i = 1; i < m_sizes.size(); ++i) {
if (m_sizes[i - 1] > m_sizes[i]) // if (m_sizes[i - 1] > m_sizes[i])
return false; // return false;
} // }
// The m_src and m_dst vectors should have the same size and should contain valid indices. // // The m_src and m_dst vectors should have the same size and should contain valid indices.
if (m_src.size() != m_dst.size()) return false; // if (m_src.size() != m_dst.size()) return false;
for (unsigned i = 0; i < m_src.size(); ++i) { // for (unsigned i = 0; i < m_src.size(); ++i) {
if (m_src[i] >= m_index.size() || m_dst[i] >= m_elems.size()) return false; // if (m_src[i] >= m_index.size() || m_dst[i] >= m_elems.size()) return false;
} // }
// The size of m_src_lim should be less than or equal to the size of m_sizes and store valid indices. // // The size of m_src_lim should be less than or equal to the size of m_sizes and store valid indices.
if (m_src_lim.size() > m_sizes.size()) return false; // if (m_src_lim.size() > m_sizes.size()) return false;
for (unsigned elem : m_src_lim) { // for (unsigned elem : m_src_lim) {
if (elem > m_src.size()) return false; // if (elem > m_src.size()) return false;
} // }
return true; return true;