mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

fix #4146

Browse source
This commit is contained in:
Nikolaj Bjorner 2020-04-28 13:28:46 -07:00
parent c5550e4385
commit b571e43f85
1 changed files with 6 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/math/polynomial/polynomial.cpp
View file

@ -794,11 +794,15 @@ namespace polynomial {
~monomial_manager() { ~monomial_manager() {
dec_ref(m_unit); dec_ref(m_unit);
CTRACE("polynomial", !m_monomials.empty(), CTRACE("polynomial", !m_monomials.empty(),
tout << "monomials leaked\n"; tout << "monomials leaked (can happen during cancelation)\n";
for (auto * m : m_monomials) { for (auto * m : m_monomials) {
m->display(tout << m->id() << " " << m->ref_count() << " ") << "\n"; m->display(tout << m->id() << " " << m->ref_count() << " ") << "\n";
}); });
SASSERT(m_monomials.empty()); for (monomial* m : m_monomials) {
unsigned obj_sz = monomial::get_obj_size(m->size());
m_allocator->deallocate(obj_sz, m);
}
m_monomials.reset();
if (m_own_allocator) if (m_own_allocator)
dealloc(m_allocator); dealloc(m_allocator);
} }