mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity

fix bug exposed when running test-z3.exe /a in debug mode, #1159. Add assertions to heap interaction

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-07-25 16:26:45 -07:00
parent 9d6be286d0
commit 9f9c575451
4 changed files with 30 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

18
src/util/heap.h
View file

@ -43,6 +43,15 @@ class heap : private LT {
return i >> 1;
}
void display(std::ostream& out, unsigned indent, int idx) const {
if (idx < static_cast<int>(m_values.size())) {
for (unsigned i = 0; i < indent; ++i) out << " ";
out << m_values[idx] << "\n";
display(out, indent + 1, left(idx));
display(out, indent + 1, right(idx));
}
}
#ifdef Z3DEBUG
// Return true if the value can be inserted in the heap. That is, the vector m_value2indices is big enough to store this value.
bool is_valid_value(int v) const {
@ -59,10 +68,13 @@ class heap : private LT {
}
return true;
}
public:
bool check_invariant() const {
return check_invariant_core(1);
}
#endif
private:
@ -219,6 +231,7 @@ public:
void insert(int val) {
CASSERT("heap", check_invariant());
CASSERT("heap", !contains(val));
SASSERT(is_valid_value(val));
int idx = static_cast<int>(m_values.size());
m_value2indices[val] = idx;
@ -272,6 +285,11 @@ public:
}
}
}
void display(std::ostream& out) const {
display(out, 0, 1);
}
};