Regression: Windows x64 DLL crashes for Z3 4.13.2 and 4.13.3 #7420
Description
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.dllandlibz3java.dll, and makecom.microsoft.z3.jaravailable - 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.