mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
ensure limit children are safe for race conditions
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
4132fc2d91
commit
54ac71cada
|
@ -217,10 +217,7 @@ namespace nlsat {
|
|||
}
|
||||
|
||||
void checkpoint() {
|
||||
if (!m_rlimit.inc()) {
|
||||
if (m_rlimit.cancel_flag_set()) throw solver_exception(Z3_CANCELED_MSG);
|
||||
throw solver_exception(Z3_MAX_RESOURCE_MSG);
|
||||
}
|
||||
if (!m_rlimit.inc()) throw solver_exception(m_rlimit.get_cancel_msg());
|
||||
if (memory::get_allocation_size() > m_max_memory) throw solver_exception(Z3_MAX_MEMORY_MSG);
|
||||
}
|
||||
|
||||
|
|
|
@ -17,6 +17,7 @@ Revision History:
|
|||
|
||||
--*/
|
||||
#include "rlimit.h"
|
||||
#include "common_msgs.h"
|
||||
|
||||
reslimit::reslimit():
|
||||
m_cancel(false),
|
||||
|
@ -57,7 +58,7 @@ void reslimit::pop() {
|
|||
m_cancel = false;
|
||||
}
|
||||
|
||||
char const* get_cancel_msg() const {
|
||||
char const* reslimit::get_cancel_msg() const {
|
||||
if (m_cancel) {
|
||||
return Z3_CANCELED_MSG;
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue