From 06fc94818f477cd143fb114e9cde26ccc08320b1 Mon Sep 17 00:00:00 2001 From: Nicola Mometto Date: Tue, 11 Dec 2018 12:09:22 +0000 Subject: [PATCH 1/4] Change error message from "internal failure" to "Object allocation failed" For consistency with https://github.com/Z3Prover/z3/commit/ad49c3269a7a0e238d27e06532eb15482e285de2 and Java/dotNet APIs --- src/api/ml/z3native_stubs.c.pre | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/ml/z3native_stubs.c.pre b/src/api/ml/z3native_stubs.c.pre index 4d221aac3..5c1a3bd06 100644 --- a/src/api/ml/z3native_stubs.c.pre +++ b/src/api/ml/z3native_stubs.c.pre @@ -458,7 +458,7 @@ CAMLprim DLL_PUBLIC value n_mk_config() { z3rv = Z3_mk_config(); 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 */ From 796689f708a8248a46cc080cb1b8cdb1b816f283 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 11 Dec 2018 09:08:53 -0800 Subject: [PATCH 2/4] #1948 remove memory allocation in nlsat::solver::~solver Signed-off-by: Nikolaj Bjorner --- src/nlsat/nlsat_solver.cpp | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index f430f3a0c..882025024 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -190,7 +190,7 @@ namespace nlsat { } ~imp() { - reset(); + clear(); } void mk_true_bvar() { @@ -230,6 +230,11 @@ namespace nlsat { m_assignment.reset(); } + void clear() { + undo_until_size(0); + del_clauses(); + del_unref_atoms(); + } void checkpoint() { if (!m_rlimit.inc()) throw solver_exception(m_rlimit.get_cancel_msg()); From a3f9e3168dfee8f2be7491022c8e89a7adb8cb6c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 11 Dec 2018 09:29:59 -0800 Subject: [PATCH 3/4] simplify ~context #1948 Signed-off-by: Nikolaj Bjorner --- src/api/api_context.cpp | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index 2de93677d..a2492cb1a 100644 --- a/src/api/api_context.cpp +++ b/src/api/api_context.cpp @@ -109,13 +109,10 @@ namespace api { context::~context() { m_last_obj = nullptr; - u_map::iterator it = m_allocated_objects.begin(); - while (it != m_allocated_objects.end()) { - api::object* val = it->m_value; - DEBUG_CODE(warning_msg("Uncollected memory: %d: %s", it->m_key, typeid(*val).name());); - m_allocated_objects.remove(it->m_key); + for (auto& kv : m_allocated_objects) { + api::object* val = kv.m_value; + DEBUG_CODE(warning_msg("Uncollected memory: %d: %s", kv.m_key, typeid(*val).name());); dealloc(val); - it = m_allocated_objects.begin(); } } From 045fef35ed379628a65c5bf325270bd8518b05de Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 11 Dec 2018 09:35:27 -0800 Subject: [PATCH 4/4] fix build break Signed-off-by: Nikolaj Bjorner --- src/nlsat/nlsat_solver.cpp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index 882025024..6ea764a0a 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -231,6 +231,9 @@ namespace nlsat { } void clear() { + m_explain.reset(); + m_lemma.reset(); + m_lazy_clause.reset(); undo_until_size(0); del_clauses(); del_unref_atoms();