mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

Merge branch 'master' of https://github.com/z3prover/z3

Browse source
This commit is contained in:
Nikolaj Bjorner 2018-12-11 09:38:44 -08:00
parent bfcea7a819 271e86020a
commit c1b03e8ca6
3 changed files with 13 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/api/api_context.cpp
View file

@ -109,13 +109,10 @@ namespace api {
context::~context() { context::~context() {
m_last_obj = nullptr; m_last_obj = nullptr;
u_map<api::object*>::iterator it = m_allocated_objects.begin(); for (auto& kv : m_allocated_objects) {
while (it != m_allocated_objects.end()) { api::object* val = kv.m_value;
api::object* val = it->m_value; DEBUG_CODE(warning_msg("Uncollected memory: %d: %s", kv.m_key, typeid(*val).name()););
DEBUG_CODE(warning_msg("Uncollected memory: %d: %s", it->m_key, typeid(*val).name()););
m_allocated_objects.remove(it->m_key);
dealloc(val); dealloc(val);
it = m_allocated_objects.begin();
} }
} }

2
src/api/ml/z3native_stubs.c.pre
View file

@ -458,7 +458,7 @@ CAMLprim DLL_PUBLIC value n_mk_config() {
z3rv = Z3_mk_config(); z3rv = Z3_mk_config();
if (z3rv == NULL) { if (z3rv == NULL) {
caml_raise_with_string(*caml_named_value("Z3EXCEPTION"), "internal error"); caml_raise_with_string(*caml_named_value("Z3EXCEPTION"), "Object allocation failed");
} }
/* construct simple return value */ /* construct simple return value */

10
src/nlsat/nlsat_solver.cpp
View file

@ -190,7 +190,7 @@ namespace nlsat {
} }
~imp() { ~imp() {
reset(); clear();
} }
void mk_true_bvar() { void mk_true_bvar() {
@ -230,6 +230,14 @@ namespace nlsat {
m_assignment.reset(); m_assignment.reset();
} }
void clear() {
m_explain.reset();
m_lemma.reset();
m_lazy_clause.reset();
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());