mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-11 19:53:34 +00:00
Code Activity

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

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-06-23 19:18:03 +02:00
parent 0eaaafc79d
commit 108d76270e
2 changed files with 7 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/smt/smt_relevancy.cpp
View file

@ -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);

6
src/util/memory_manager.cpp
View file

@ -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();
}