From 44c221b690cd254ac4c09831bafca8c93def3176 Mon Sep 17 00:00:00 2001
From: Copilot <198982749+Copilot@users.noreply.github.com>
Date: Thu, 23 Jul 2026 10:25:58 -0700
Subject: [PATCH] Fix MinGW linker errors: explicitly link dbghelp on Windows
 (#10203)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Building Z3 on Windows with MinGW (`mingw-w64-ucrt-x86_64-gcc`) fails
with undefined references to `SymSetOptions`, `SymInitialize`,
`SymFromAddr`, and `SymGetLineFromAddr64` from the DbgHelp library used
in `src/util/debug.cpp` for stack backtraces.

The existing `#pragma comment(lib, "dbghelp.lib")` in `debug.cpp` is an
MSVC-only extension — MinGW silently ignores it, so `dbghelp` is never
passed to the linker.

## Changes

- **`CMakeLists.txt`**: Append `dbghelp` to `Z3_DEPENDENT_LIBS` in the
`WIN32` platform block. This feeds the library to both the `libz3` and
`shell` link steps regardless of compiler.
- **`src/util/debug.cpp`**: Guard the `#pragma comment` with `#ifdef
_MSC_VER` to make the MSVC-only intent explicit.

<!-- START COPILOT CODING AGENT SUFFIX -->

- Fixes #10171

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
---
 CMakeLists.txt     | 6 +++++-
 src/util/debug.cpp | 2 ++
 2 files changed, 7 insertions(+), 1 deletion(-)

diff --git a/CMakeLists.txt b/CMakeLists.txt
index ae57d5b2f4..aa9bfcad9c 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -197,7 +197,11 @@ elseif (WIN32)
   message(STATUS "Platform: Windows")
   list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_WINDOWS")
   # workaround for #7420
-  list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_DISABLE_CONSTEXPR_MUTEX_CONSTRUCTOR")  
+  list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_DISABLE_CONSTEXPR_MUTEX_CONSTRUCTOR")
+  # dbghelp is used in debug.cpp for stack backtraces on Windows.
+  # With MSVC this is handled by #pragma comment(lib, "dbghelp.lib") in debug.cpp,
+  # but MinGW does not support that pragma, so we add it explicitly here.
+  list(APPEND Z3_DEPENDENT_LIBS dbghelp)
 elseif (EMSCRIPTEN)
   message(STATUS "Platform: Emscripten")
   list(APPEND Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS
diff --git a/src/util/debug.cpp b/src/util/debug.cpp
index 4a2141c024..a95b8358d4 100644
--- a/src/util/debug.cpp
+++ b/src/util/debug.cpp
@@ -39,7 +39,9 @@ bool assertions_enabled() {
 #if defined(_WINDOWS)
 #include <windows.h>
 #include <dbghelp.h>
+#ifdef _MSC_VER
 #pragma comment(lib, "dbghelp.lib")
+#endif
 static void print_windows_backtrace() {
     HANDLE process = GetCurrentProcess();
     SymSetOptions(SYMOPT_LOAD_LINES | SYMOPT_DEFERRED_LOADS | SYMOPT_UNDNAME);