mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 02:15:19 +00:00
Code Activity

smt_context: we can't assert that the resource limits were exceeded on cancel_exception

Browse source 
It happens sometimes that e.g. the internalizer goes above the soft memory limit
But since it's only by a small amount, when the exception propagates back to the context, some stuff
has been freed already and we are not longer above the memory threshold
Just delete these asserts
This commit is contained in:
Nuno Lopes 2023-08-20 10:34:28 +01:00
parent 5d33805c8b
commit 3b546b2348
1 changed files with 0 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/smt/smt_context.cpp
View file

@ -3565,7 +3565,6 @@ namespace smt {
try {
internalize_assertions();
} catch (cancel_exception&) {
VERIFY(resource_limits_exceeded());
return l_undef;
}
expr_ref_vector theory_assumptions(m);
@ -3637,7 +3636,6 @@ namespace smt {
TRACE("unsat_core_bug", tout << asms << '\n';);
init_assumptions(asms);
} catch (cancel_exception&) {
VERIFY(resource_limits_exceeded());
return l_undef;
}
TRACE("before_search", display(tout););
@ -3664,7 +3662,6 @@ namespace smt {
for (auto const& clause : clauses) if (!validate_assumptions(clause)) return l_undef;
init_assumptions(asms);
} catch (cancel_exception&) {
VERIFY(resource_limits_exceeded());
return l_undef;
}
for (auto const& clause : clauses) init_clause(clause);