z3 4.8.11 fails to build on MinGW-w64

[brechtsanders]

When building z3 v4.8.11 for Windows with MinGW-w64 compilation fails with the following output:

FAILED: src/util/CMakeFiles/util.dir/mpz.cpp.obj
E:\Prog\winlibs32-11.1.0-9.0.0\mingw32\bin\c++.exe -D_EXTERNAL_RELEASE -D_MP_GMP -D_WINDOWS -Isrc -I../src -march=pentium4 -Werror=odr  -O3 -DNDEBUG -Wall -fvisibility=hidden -fvisibility-inlines-hidden -std=gnu++17 -MD -MT src/util/CMakeFiles/util.dir/mpz.cpp.obj -MF src\util\CMakeFiles\util.dir\mpz.cpp.obj.d -o src/util/CMakeFiles/util.dir/mpz.cpp.obj -c ../src/util/mpz.cpp
In file included from e:\prog\winlibs32-11.1.0-9.0.0\mingw32\lib\gcc\i686-w64-mingw32\10.3.0\include\immintrin.h:107,
                 from ../src/util/mpz.cpp:53:
e:\prog\winlibs32-11.1.0-9.0.0\mingw32\lib\gcc\i686-w64-mingw32\10.3.0\include\bmiintrin.h: In function 'unsigned int u_gcd(unsigned int, unsigned int)':
e:\prog\winlibs32-11.1.0-9.0.0\mingw32\lib\gcc\i686-w64-mingw32\10.3.0\include\bmiintrin.h:104:1: error: inlining failed in call to 'always_inline' 'unsigned int _tzcnt_u32(unsigned int)': target specific option mismatch
  104 | _tzcnt_u32 (unsigned int __X)
      | ^~~~~~~~~~
../src/util/mpz.cpp:54:40: note: called from here
   54 | #define _trailing_zeros32(X) _tzcnt_u32(X)
      |                              ~~~~~~~~~~^~~
../src/util/mpz.cpp:88:11: note: in expansion of macro '_trailing_zeros32'
   88 |     u >>= _trailing_zeros32(u);
      |           ^~~~~~~~~~~~~~~~~
In file included from e:\prog\winlibs32-11.1.0-9.0.0\mingw32\lib\gcc\i686-w64-mingw32\10.3.0\include\immintrin.h:107,
                 from ../src/util/mpz.cpp:53:
e:\prog\winlibs32-11.1.0-9.0.0\mingw32\lib\gcc\i686-w64-mingw32\10.3.0\include\bmiintrin.h:104:1: error: inlining failed in call to 'always_inline' 'unsigned int _tzcnt_u32(unsigned int)': target specific option mismatch
  104 | _tzcnt_u32 (unsigned int __X)
      | ^~~~~~~~~~
../src/util/mpz.cpp:54:40: note: called from here
   54 | #define _trailing_zeros32(X) _tzcnt_u32(X)
      |                              ~~~~~~~~~~^~~
../src/util/mpz.cpp:87:22: note: in expansion of macro '_trailing_zeros32'
   87 |     unsigned shift = _trailing_zeros32(u | v);
      |                      ^~~~~~~~~~~~~~~~~
In file included from e:\prog\winlibs32-11.1.0-9.0.0\mingw32\lib\gcc\i686-w64-mingw32\10.3.0\include\immintrin.h:107,
                 from ../src/util/mpz.cpp:53:
e:\prog\winlibs32-11.1.0-9.0.0\mingw32\lib\gcc\i686-w64-mingw32\10.3.0\include\bmiintrin.h:104:1: error: inlining failed in call to 'always_inline' 'unsigned int _tzcnt_u32(unsigned int)': target specific option mismatch
  104 | _tzcnt_u32 (unsigned int __X)
      | ^~~~~~~~~~
../src/util/mpz.cpp:54:40: note: called from here
   54 | #define _trailing_zeros32(X) _tzcnt_u32(X)
      |                              ~~~~~~~~~~^~~
../src/util/mpz.cpp:92:15: note: in expansion of macro '_trailing_zeros32'
   92 |         v >>= _trailing_zeros32(v);
      |               ^~~~~~~~~~~~~~~~~
ninja: build stopped: subcommand failed.

The issue is in src/util/mpz.cpp:

#if defined(_WINDOWS) && !defined(_M_ARM) && !defined(_M_ARM64)
// This is needed for _tzcnt_u32 and friends.
#include <immintrin.h>
#define _trailing_zeros32(X) _tzcnt_u32(X)
#elif defined(__GNUC__)
#define _trailing_zeros32(X) __builtin_ctz(X)
#else
static uint32_t _trailing_zeros32(uint32_t x) {
    uint32_t r = 0;
    for (; 0 == (x & 1) && r < 32; ++r, x >>= 1);
    return r;
}
#endif

Possible solutions:
Build succeeds after adding && !defined(__MINGW32__) after defined(_WINDOWS), or even better when putting the #if defined(__GNUC__) block before #elif defined(_WINDOWS) && !defined(_M_ARM) && !defined(_M_ARM64).

[NikolajBjorner]

Is the push OK?

Bonus favor: add a pipeline define to the CI build for this platform.

[brechtsanders]

It works, though technically if you put #if defined(__GNUC__) first then you no longer need to add && !defined(__MINGW32__) after #elif defined(_WINDOWS) && !defined(_M_ARM) && !defined(_M_ARM64) as __GNUC__ is always defined when building against MinGW (both when using MinGW gcc or clang).