Regression: Windows x64 DLL crashes for Z3 4.13.2 and 4.13.3

[kfriedberger]

There is a regression from Z3 v4.13.0 to v4.13.2: Executing the JavaExample with the released DLL crashes.

Input:

• download released version of Z3 for Windows x64 from https://github.com/Z3Prover/z3/releases and unpack
• set PATH to include the directory for libz3.dll and libz3java.dll, and make com.microsoft.z3.jar available
• use the JavaExample from https://github.com/Z3Prover/z3/blob/master/examples/java/JavaExample.java
• run java -cp ../lib/com.microsoft.z3.jar:. JavaExample

Output:

java -cp ../lib/com.microsoft.z3.jar:. JavaExample
Z3 Major Version: 4
Z3 Full Version: 4.13.3.0
Z3 Full Version String: Z3 4.13.3.0
String example
#
# A fatal error has been detected by the Java Runtime Environment:
#
#  EXCEPTION_ACCESS_VIOLATION (0xc0000005) at pc=0x00007ffbb40c3080, pid=17672, tid=17288
#
# JRE version: OpenJDK Runtime Environment Corretto-22.0.2.9.1 (22.0.2+9) (build 22.0.2+9-FR)
# Java VM: OpenJDK 64-Bit Server VM Corretto-22.0.2.9.1 (22.0.2+9-FR, mixed mode, sharing, tiered, compressed oops, compressed class ptrs, g1 gc, windows-amd64)
# Problematic frame:
# C  [msvcp140.dll+0x13080]
#
# No core dump will be written. Minidumps are not enabled by default on client versions of Windows
#
# An error report file with more information is saved as:
# C:\Users\<USERNAME>\workspace\z3-example\src\hs_err_pid17672.log
[0.201s][warning][os] Loading hsdis library failed
#
# If you would like to submit a bug report, please visit:
#   https://github.com/corretto/corretto-22/issues/
# The crash happened outside the Java Virtual Machine in native code.
# See problematic frame for where to report the bug.

I'm encountering a crash with versions v4.13.2 and v4.13.3 of the software. However, if I replace the Z3-related DLLs with those from v4.13.0, everything works as expected.

Have there been any updates to system requirements or changes in dependencies between Z3 versions v4.13.0 and v4.13.2 that I might have missed?

Can anyone else confirm this issue?
I've been able to reproduce it both locally on my Windows 11 laptop and in the Windows CI for JavaSMT. The CI run includes a tab labeled "artifacts", where coredumps are available if needed.

As I'm not very familiar with debugging DLL-related issues, any assistance from the developers would be appreciated.

[DavidRobb]

Came across your problem while looking for a solution for mine. Might be worth checking that the latest VC Redistributbales are present to provide compatibility with std::mutex handling in release builds of C++ exe and dll files.

Please see issue raised as
gabime/spdlog#3212

https://stackoverflow.com/questions/78598141/first-stdmutexlock-crashes-in-application-built-with-latest-visual-studio

adoptium/temurin-build#3887

[kfriedberger]

@DavidRobb : Thank you for your comment. It is really helpful. 👍

The issue stems from the msvcp140.dll 14.29.30153.0 file that comes with JDK Corretto 22.0.2_9. Removing msvcp140.dll from the JDK's bin directory resolved the problem, allowing the Z3 DLLs to work in version 4.13.2/4.13.3.

However, this step is not an ideal solution, as we cannot expect users to modify their JDK installations just for using Z3, especially given potential permission limitations.

@NikolajBjorner : Would it be possible to provide Z3 DLLs compatible with earlier versions of msvcp140.dll? Maybe use the _DISABLE_CONSTEXPR_MUTEX_CONSTRUCTOR preprocessor macro as mentioned in the StackOverflow reponse.

[NikolajBjorner]

Right, seems setting _DISABLE_CONSTEXPR_MUTEX_CONSTRUCTOR will be the way to go.
It would be set both for the CMAKE build system and the python build system, at least when creating Java dlls.
Other users will face this issue and it doesn't work well if everybody has to work around it.
There is a separate bug filed for it already.

[NikolajBjorner]

#7405

[kfriedberger]

Thank you for referencing the other issue.
It seems that this one is redundant, so it can be closed.
We look forward to the fix.

[NikolajBjorner]

It now works in my own tests.