mirror of
https://github.com/Z3Prover/z3
synced 2025-06-06 06:03:23 +00:00
#1948 remove memory allocation in nlsat::solver::~solver
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
b40c2b2926
commit
796689f708
1 changed files with 6 additions and 1 deletions
|
@ -190,7 +190,7 @@ namespace nlsat {
|
||||||
}
|
}
|
||||||
|
|
||||||
~imp() {
|
~imp() {
|
||||||
reset();
|
clear();
|
||||||
}
|
}
|
||||||
|
|
||||||
void mk_true_bvar() {
|
void mk_true_bvar() {
|
||||||
|
@ -230,6 +230,11 @@ namespace nlsat {
|
||||||
m_assignment.reset();
|
m_assignment.reset();
|
||||||
}
|
}
|
||||||
|
|
||||||
|
void clear() {
|
||||||
|
undo_until_size(0);
|
||||||
|
del_clauses();
|
||||||
|
del_unref_atoms();
|
||||||
|
}
|
||||||
|
|
||||||
void checkpoint() {
|
void checkpoint() {
|
||||||
if (!m_rlimit.inc()) throw solver_exception(m_rlimit.get_cancel_msg());
|
if (!m_rlimit.inc()) throw solver_exception(m_rlimit.get_cancel_msg());
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue