Issues building 4.12.0 for MinGW-w64 target

[brechtsanders]

When building natively in Windows 11 with MinGW-w64 GCC 12.2.0 for Windows 64-bit the link step fails with the following output:

[846/847] Linking CXX executable z3.exe
FAILED: z3.exe
cmd.exe /C "cd . && D:\Prog\winlibs64-12.2.0msvcrt\mingw64\bin\c++.exe -Werror=odr  -O3 -DNDEBUG  @CMakeFiles\shell.rsp -o z3.exe -Wl,--out-implib,libz3.dll.a -Wl,--major-image-version,0,--minor-image-version,0  && cd ."
d:/prog/winlibs64-12.2.0msvcrt/mingw64/bin/../lib/gcc/x86_64-w64-mingw32/12.2.0/../../../../x86_64-w64-mingw32/bin/ld.exe: src/ast/simplifiers/CMakeFiles/simplifiers.dir/max_bv_sharing.cpp.obj:max_bv_sharing:(.text+0x5a): undefined reference to `rewriter_tpl<maximize_bv_sharing>::rewriter_tpl(ast_manager&, bool, maximize_bv_sharing&)'
d:/prog/winlibs64-12.2.0msvcrt/mingw64/bin/../lib/gcc/x86_64-w64-mingw32/12.2.0/../../../../x86_64-w64-mingw32/bin/ld.exe: src/sat/sat_solver/CMakeFiles/sat_solver.dir/sat_smt_preprocess.cpp.obj:sat_smt_preprocess.cpp:(.text+0x2ba): undefined reference to `rewriter_tpl<elim_term_ite_cfg>::rewriter_tpl(ast_manager&, bool, elim_term_ite_cfg&)'
d:/prog/winlibs64-12.2.0msvcrt/mingw64/bin/../lib/gcc/x86_64-w64-mingw32/12.2.0/../../../../x86_64-w64-mingw32/bin/ld.exe: src/sat/sat_solver/CMakeFiles/sat_solver.dir/sat_smt_preprocess.cpp.obj:sat_smt_preprocess.cpp:(.text+0x390): undefined reference to `rewriter_tpl<ng_push_app_ite_cfg>::rewriter_tpl(ast_manager&, bool, ng_push_app_ite_cfg&)'
d:/prog/winlibs64-12.2.0msvcrt/mingw64/bin/../lib/gcc/x86_64-w64-mingw32/12.2.0/../../../../x86_64-w64-mingw32/bin/ld.exe: src/sat/sat_solver/CMakeFiles/sat_solver.dir/sat_smt_preprocess.cpp.obj:sat_smt_preprocess.cpp:(.text+0x70d): undefined reference to `rewriter_tpl<bv_elim_cfg>::rewriter_tpl(ast_manager&, bool, bv_elim_cfg&)'
d:/prog/winlibs64-12.2.0msvcrt/mingw64/bin/../lib/gcc/x86_64-w64-mingw32/12.2.0/../../../../x86_64-w64-mingw32/bin/ld.exe: src/sat/sat_solver/CMakeFiles/sat_solver.dir/sat_smt_preprocess.cpp.obj:sat_smt_preprocess.cpp:(.text+0x7a1): undefined reference to `rewriter_tpl<push_app_ite_cfg>::rewriter_tpl(ast_manager&, bool, push_app_ite_cfg&)'
d:/prog/winlibs64-12.2.0msvcrt/mingw64/bin/../lib/gcc/x86_64-w64-mingw32/12.2.0/../../../../x86_64-w64-mingw32/bin/ld.exe: src/sat/sat_solver/CMakeFiles/sat_solver.dir/sat_smt_preprocess.cpp.obj:sat_smt_preprocess.cpp:(.text+0x8ab): undefined reference to `rewriter_tpl<elim_bounds_cfg>::rewriter_tpl(ast_manager&, bool, elim_bounds_cfg&)'
collect2.exe: error: ld returned 1 exit status
ninja: build stopped: subcommand failed.

When building for Windows 32-bit there is a compiler error earlier on:

FAILED: src/util/CMakeFiles/util.dir/hwf.cpp.obj
D:\Prog\winlibs32-12.2.0msvcrt\mingw32\bin\c++.exe -D_EXTERNAL_RELEASE -D_MP_GMP -D_WINDOWS -IR:/winlibs32-12.2.0msvcrt/z3-z3-4.12.0/build_static/src -IR:/winlibs32-12.2.0msvcrt/z3-z3-4.12.0/src -Werror=odr  -O3 -DNDEBUG -fvisibility=hidden -fno-keep-inline-dllexport -Wall -std=gnu++17 -MD -MT src/util/CMakeFiles/util.dir/hwf.cpp.obj -MF src\util\CMakeFiles\util.dir\hwf.cpp.obj.d -o src/util/CMakeFiles/util.dir/hwf.cpp.obj -c R:/winlibs32-12.2.0msvcrt/z3-z3-4.12.0/src/util/hwf.cpp
R:/winlibs32-12.2.0msvcrt/z3-z3-4.12.0/src/util/hwf.cpp: In member function 'void hwf_manager::add(mpf_rounding_mode, const hwf&, const hwf&, hwf&)':
R:/winlibs32-12.2.0msvcrt/z3-z3-4.12.0/src/util/hwf.cpp:223:17: warning: SSE vector return without SSE enabled changes the ABI [-Wpsabi]
  223 |     _mm_store_sd(&o.value, _mm_add_sd(_mm_set_sd(x.value), _mm_set_sd(y.value)));
      |     ~~~~~~~~~~~~^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In file included from R:/winlibs32-12.2.0msvcrt/z3-z3-4.12.0/src/util/hwf.cpp:56:
d:\prog\winlibs32-12.2.0msvcrt\mingw32\lib\gcc\i686-w64-mingw32\12.2.0\include\emmintrin.h: In member function 'void hwf_manager::maximum(const hwf&, const hwf&, hwf&)':
d:\prog\winlibs32-12.2.0msvcrt\mingw32\lib\gcc\i686-w64-mingw32\12.2.0\include\emmintrin.h:178:1: error: inlining failed in call to 'always_inline' 'void _mm_store_sd(double*, __m128d)': target specific option mismatch
  178 | _mm_store_sd (double *__P, __m128d __A)
      | ^~~~~~~~~~~~
R:/winlibs32-12.2.0msvcrt/z3-z3-4.12.0/src/util/hwf.cpp:320:17: note: called from here
  320 |     _mm_store_sd(&o.value, _mm_max_sd(_mm_set_sd(x.value), _mm_set_sd(y.value)));
      |     ~~~~~~~~~~~~^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
d:\prog\winlibs32-12.2.0msvcrt\mingw32\lib\gcc\i686-w64-mingw32\12.2.0\include\emmintrin.h:326:1: error: inlining failed in call to 'always_inline' '__m128d _mm_max_sd(__m128d, __m128d)': target specific option mismatch
  326 | _mm_max_sd (__m128d __A, __m128d __B)
      | ^~~~~~~~~~
R:/winlibs32-12.2.0msvcrt/z3-z3-4.12.0/src/util/hwf.cpp:320:17: note: called from here
  320 |     _mm_store_sd(&o.value, _mm_max_sd(_mm_set_sd(x.value), _mm_set_sd(y.value)));
      |     ~~~~~~~~~~~~^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
d:\prog\winlibs32-12.2.0msvcrt\mingw32\lib\gcc\i686-w64-mingw32\12.2.0\include\emmintrin.h:66:1: error: inlining failed in call to 'always_inline' '__m128d _mm_set_sd(double)': target specific option mismatch
   66 | _mm_set_sd (double __F)
      | ^~~~~~~~~~
R:/winlibs32-12.2.0msvcrt/z3-z3-4.12.0/src/util/hwf.cpp:320:17: note: called from here
  320 |     _mm_store_sd(&o.value, _mm_max_sd(_mm_set_sd(x.value), _mm_set_sd(y.value)));
      |     ~~~~~~~~~~~~^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
d:\prog\winlibs32-12.2.0msvcrt\mingw32\lib\gcc\i686-w64-mingw32\12.2.0\include\emmintrin.h:66:1: error: inlining failed in call to 'always_inline' '__m128d _mm_set_sd(double)': target specific option mismatch
   66 | _mm_set_sd (double __F)
      | ^~~~~~~~~~
R:/winlibs32-12.2.0msvcrt/z3-z3-4.12.0/src/util/hwf.cpp:320:17: note: called from here
  320 |     _mm_store_sd(&o.value, _mm_max_sd(_mm_set_sd(x.value), _mm_set_sd(y.value)));
      |     ~~~~~~~~~~~~^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
ninja: build stopped: subcommand failed.

[NikolajBjorner]

these are two different things.
I pushed a commit to address the first. Can you try it out?

The second has to be a configuration option for the build. It enables/disables SSE based on some platform environment flags. Looks like these are not right for your build.

[brechtsanders]

I tried current master and it builds fine with MinGW-w64 targeting Windows 64-bit.

As for the 32-bit SSE issue, something must have changed since 4.11.2, because that built fine (so did earlier versions).
My CMake flags are: -DZ3_USE_LIB_GMP:BOOL=ON -DSINGLE_THREADED:BOOL=OFF -DZ3_BUILD_DOTNET_BINDINGS:BOOL=OFF -DZ3_BUILD_JAVA_BINDINGS:BOOL=OFF -DZ3_INCLUDE_GIT_DESCRIBE:BOOL=OFF -DZ3_INCLUDE_GIT_HASH:BOOL=OFF -DZ3_ENABLE_EXAMPLE_TARGETS:BOOL=OFF -DZ3_BUILD_DOCUMENTATION:BOOL=OFF

[NikolajBjorner]

your pull request from Jan 10 is the only change to hwf.cpp

#if (defined(clang) && !defined(MINGW32)) || defined(_M_ARM) && defined(_M_ARM64)

[brechtsanders]

My Windows 32-bit build issue is resolved when I use this CMake flag: -DCMAKE_CXX_FLAGS:STRING="-msse4.1"