mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 11:42:28 +00:00
Code Activity

remove one invariant

Browse source
This commit is contained in:
Chuyue Sun 2024-08-01 23:50:39 +00:00
parent 56f216644e
commit a57b74bd58
1 changed files with 6 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/util/heap.h
View file

@ -61,12 +61,12 @@ class heap : private LT {
return false; return false;
} }
// All indices in m_value2indices that are not used in m_values should be 0 // // All indices in m_value2indices that are not used in m_values should be 0
for (int val = 0; val < static_cast<int>(m_value2indices.size()); ++val) { // for (int val = 0; val < static_cast<int>(m_value2indices.size()); ++val) {
if (std::find(m_values.begin(), m_values.end(), val) == m_values.end() && m_value2indices[val] != 0) { // if (std::find(m_values.begin(), m_values.end(), val) == m_values.end() && m_value2indices[val] != 0) {
return false; // Unused indices should have a 0 value // return false; // Unused indices should have a 0 value
} // }
} // }
if (idx < static_cast<int>(m_values.size())) { if (idx < static_cast<int>(m_values.size())) {
SASSERT(m_value2indices[m_values[idx]] == idx); SASSERT(m_value2indices[m_values[idx]] == idx);