diff --git a/src/util/debug.cpp b/src/util/debug.cpp index 4434cb19f..3e40e412c 100644 --- a/src/util/debug.cpp +++ b/src/util/debug.cpp @@ -69,7 +69,7 @@ bool is_debug_enabled(const char * tag) { return g_enabled_debug_tags->contains(const_cast(tag)); } -#ifndef _WINDOWS +#if !defined(_WINDOWS) && !defined(NO_Z3_DEBUGGER) void invoke_gdb() { char buffer[1024]; int * x = nullptr;