From 108d76270e52a9861bf8e8ee801b54dfd32cfb54 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 23 Jun 2015 19:18:03 +0200 Subject: [PATCH] set undo trail after set-watches to avoid crash during exception handling (the relevancy trail is scoped so ends up traversing the trail if allocating the watch throws an exception). Fixes crash.smt in issue #56 Signed-off-by: Nikolaj Bjorner --- src/smt/smt_relevancy.cpp | 2 +- src/util/memory_manager.cpp | 6 ++++++ 2 files changed, 7 insertions(+), 1 deletion(-) diff --git a/src/smt/smt_relevancy.cpp b/src/smt/smt_relevancy.cpp index 47e3e3ef4..b7a2b4011 100644 --- a/src/smt/smt_relevancy.cpp +++ b/src/smt/smt_relevancy.cpp @@ -212,8 +212,8 @@ namespace smt { return; case l_undef: SASSERT(eh); - push_trail(eh_trail(n, val)); set_watches(n, val, new (get_region()) relevancy_ehs(eh, get_watches(n, val))); + push_trail(eh_trail(n, val)); break; case l_true: eh->operator()(*this, n, val); diff --git a/src/util/memory_manager.cpp b/src/util/memory_manager.cpp index 88bd6b92e..f207fa969 100644 --- a/src/util/memory_manager.cpp +++ b/src/util/memory_manager.cpp @@ -69,6 +69,12 @@ static void throw_out_of_memory() { } static void throw_alloc_counts_exceeded() { + #pragma omp critical (z3_memory_manager) + { + // reset the count to avoid re-throwing while + // the exception is being thrown. + g_memory_alloc_count = 0; + } throw exceeded_memory_allocations(); }