mirror of
https://github.com/Z3Prover/z3
synced 2025-04-12 12:08:18 +00:00
free memory the clean way
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
d32dcfc4a4
commit
910b3023c2
|
@ -180,7 +180,7 @@ namespace algebraic_numbers {
|
||||||
return m_upmanager;
|
return m_upmanager;
|
||||||
}
|
}
|
||||||
|
|
||||||
void del(basic_cell * c) {
|
void del_basic(basic_cell * c) {
|
||||||
qm().del(c->m_value);
|
qm().del(c->m_value);
|
||||||
m_allocator.deallocate(sizeof(basic_cell), c);
|
m_allocator.deallocate(sizeof(basic_cell), c);
|
||||||
}
|
}
|
||||||
|
@ -207,7 +207,7 @@ namespace algebraic_numbers {
|
||||||
if (a.is_null())
|
if (a.is_null())
|
||||||
return;
|
return;
|
||||||
if (a.is_basic())
|
if (a.is_basic())
|
||||||
del(a.to_basic());
|
del_basic(a.to_basic());
|
||||||
else
|
else
|
||||||
del(a.to_algebraic());
|
del(a.to_algebraic());
|
||||||
a.clear();
|
a.clear();
|
||||||
|
@ -795,7 +795,7 @@ namespace algebraic_numbers {
|
||||||
// root was found
|
// root was found
|
||||||
scoped_mpq r(qm());
|
scoped_mpq r(qm());
|
||||||
to_mpq(qm(), lower(c), r);
|
to_mpq(qm(), lower(c), r);
|
||||||
del(c);
|
del(a);
|
||||||
a = mk_basic_cell(r);
|
a = mk_basic_cell(r);
|
||||||
return false;
|
return false;
|
||||||
}
|
}
|
||||||
|
|
Loading…
Reference in a new issue