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 #2595

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-09-28 17:43:35 -07:00
parent a424ab918b
commit 98c3887460
2 changed files with 9 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -2184,10 +2184,16 @@ namespace polynomial {
}
~som_buffer_vector() {
clear();
}
void clear() {
reset();
unsigned sz = m_buffers.size();
for (unsigned i = 0; i < sz; i++) {
dealloc(m_buffers[i]);
}
m_buffers.reset();
}
void set_owner(imp * owner) {
@ -2372,11 +2378,14 @@ namespace polynomial {
m_polynomials.reset();
});
SASSERT(m_polynomials.empty());
m_iccp_ZpX_buffers.clear();
m_monomial_manager->dec_ref();
}
void checkpoint() {
if (!m_limit.inc()) {
m_som_buffer.reset();
m_som_buffer2.reset();
throw polynomial_exception(Z3_CANCELED_MSG);
}
}