mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-07 11:41:22 +00:00
Code Activity

disable assertion notification during shutdown

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-04-01 14:59:35 -07:00
parent 7b60c37ad8
commit dcc87a682c
3 changed files with 12 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/util/debug.cpp
View file

@ -36,7 +36,16 @@ bool assertions_enabled() {
return g_enable_assertions; return g_enable_assertions;
} }
static atomic<bool> g_enable_notify_assertion_violation(true);
void disable_notify_assertion_violation() {
g_enable_notify_assertion_violation = false;
}
void notify_assertion_violation(const char * fileName, int line, const char * condition) { void notify_assertion_violation(const char * fileName, int line, const char * condition) {
if (!g_enable_notify_assertion_violation)
return;
std::cerr << "ASSERTION VIOLATION\n" std::cerr << "ASSERTION VIOLATION\n"
"File: " << fileName << "\n" "File: " << fileName << "\n"
"Line: " << line << '\n' "Line: " << line << '\n'

1
src/util/debug.h
View file

@ -67,6 +67,7 @@ void invoke_gdb();
#endif #endif
void notify_assertion_violation(const char * file_name, int line, const char * condition); void notify_assertion_violation(const char * file_name, int line, const char * condition);
void disable_notify_assertion_violation();
void enable_debug(const char * tag); void enable_debug(const char * tag);
void disable_debug(const char * tag); void disable_debug(const char * tag);
bool is_debug_enabled(const char * tag); bool is_debug_enabled(const char * tag);

2
src/util/timeout.cpp
View file

@ -25,6 +25,7 @@ Revision History:
#include "util/event_handler.h" #include "util/event_handler.h"
#include "util/scoped_timer.h" #include "util/scoped_timer.h"
#include "util/debug.h"
static scoped_timer * g_timeout = nullptr; static scoped_timer * g_timeout = nullptr;
static void (* g_on_timeout)() = nullptr; static void (* g_on_timeout)() = nullptr;
@ -36,6 +37,7 @@ public:
m_caller_id = caller_id; m_caller_id = caller_id;
std::cout << "timeout\n"; std::cout << "timeout\n";
std::cout.flush(); std::cout.flush();
disable_notify_assertion_violation();
if (g_on_timeout) if (g_on_timeout)
g_on_timeout(); g_on_timeout();
throw z3_error(ERR_TIMEOUT); throw z3_error(ERR_TIMEOUT);