From 18b4a86740142ec1999003f3597f5abb1aced709 Mon Sep 17 00:00:00 2001
From: Copilot <198982749+Copilot@users.noreply.github.com>
Date: Fri, 24 Jul 2026 13:11:08 -0700
Subject: [PATCH] ci: add MinGW build/test job to Windows.yml (#10211)

MinGW silently ignores `#pragma comment(lib, ...)` (MSVC-only), so
linker errors like missing `dbghelp` symbols go undetected until a
downstream user hits them. No CI coverage existed for MinGW on Windows.

## Changes

- **`.github/workflows/Windows.yml`**: New `mingw-build` job using MSYS2
UCRT64 (`mingw-w64-ucrt-x86_64-gcc`) that builds Z3 via `cmake -G Ninja`
and runs `test-z3 /a`, exercising the full link step under MinGW on
every push/PR to master.

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
---
 .github/workflows/Windows.yml | 27 +++++++++++++++++++++++++++
 src/test/hwf.cpp              |  1 +
 src/test/quant_elim.cpp       |  3 +--
 3 files changed, 29 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/Windows.yml b/.github/workflows/Windows.yml
index 728925fde6..e91e4edbf6 100644
--- a/.github/workflows/Windows.yml
+++ b/.github/workflows/Windows.yml
@@ -11,6 +11,33 @@ concurrency:
   cancel-in-progress: true     
 
 jobs:               
+  mingw-build:
+    runs-on: windows-latest
+    steps:
+      - name: Checkout code
+        uses: actions/checkout@v7.0.1
+      - name: Setup MSYS2 (UCRT64 / MinGW-w64)
+        uses: msys2/setup-msys2@v2
+        with:
+          msystem: UCRT64
+          update: true
+          install: >-
+            mingw-w64-ucrt-x86_64-gcc
+            mingw-w64-ucrt-x86_64-cmake
+            mingw-w64-ucrt-x86_64-ninja
+            python3
+      - name: Build Z3 with MinGW
+        shell: msys2 {0}
+        run: |
+          mkdir build && cd build
+          cmake -G Ninja -DCMAKE_BUILD_TYPE=Release ..
+          ninja -j$(nproc) shell test-z3
+      - name: Run unit tests
+        shell: msys2 {0}
+        run: |
+          cd build
+          ./test-z3.exe /a
+
   build:
     strategy:
       matrix:
diff --git a/src/test/hwf.cpp b/src/test/hwf.cpp
index b81a9cef30..8ed3155d5d 100644
--- a/src/test/hwf.cpp
+++ b/src/test/hwf.cpp
@@ -19,6 +19,7 @@ Revision History:
 #include "util/hwf.h"
 #include "util/f2n.h"
 #include "util/rational.h"
+#include <cfloat>
 #include <iostream>
 
 static void bug_set_double() {
diff --git a/src/test/quant_elim.cpp b/src/test/quant_elim.cpp
index cd3b52553e..cd03273448 100644
--- a/src/test/quant_elim.cpp
+++ b/src/test/quant_elim.cpp
@@ -497,10 +497,9 @@ void tst_quant_elim() {
    
 
     memory::finalize();
-#ifdef _WINDOWS
+#if defined(_WINDOWS) && defined(_MSC_VER)
     _CrtDumpMemoryLeaks();
 #endif
     exit(0);
 }
 
-