You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Creating a Z3 Context through the java API is causing a fatal error. I traced the problem to a call to the com.microsoft.z3.Context() constructor in a larger project. Below is a distilled example which reproduces the issue in my environment.
Installation
I downloaded latest yesterday, and installed via the 64-bit Windows compilation pathway.
In x64 Native Tools Command Prompt for VS 2022:
python3 scripts/mk-make.py -x --java
cd build
nmake
Then, I added the build directory to my PATH user environment variable.
Reproducing
Then, in the build directory, I created the following class with a small snippet from the JavaExample class.
importcom.microsoft.z3.*;
classSimple {
// / "Hello world" example: create a Z3 logical context, and delete it.publicstaticvoidsimpleExample()
{
System.out.println("SimpleExample");
{
Contextctx = newContext();
/* do something with the context *//* be kind to dispose manually and not wait for the GC. */ctx.close();
}
}
publicstaticvoidmain(String[] args) {
simpleExample();
}
}
Still in the build directory, I compiled and ran, as per the instructions in #7000.
SimpleExample
#
# A fatal error has been detected by the Java Runtime Environment:
#
# EXCEPTION_ACCESS_VIOLATION (0xc0000005) at pc=0x00007fff57e22f58, pid=5064, tid=17680
#
# JRE version: Java(TM) SE Runtime Environment (17.0.12+8) (build 17.0.12+8-LTS-286)
# Java VM: Java HotSpot(TM) 64-Bit Server VM (17.0.12+8-LTS-286, mixed mode, sharing, tiered, compressed oops, compressed class ptrs, g1 gc, windows-amd64)
# Problematic frame:
# C [msvcp140.dll+0x12f58]
#
# 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\wagne\software\z3-master\z3-master\build\hs_err_pid5064.log
#
# If you would like to submit a bug report, please visit:
# https://bugreport.java.com/bugreport/crash.jsp
# The crash happened outside the Java Virtual Machine in native code.
# See problematic frame for where to report the bug.
#
The text was updated successfully, but these errors were encountered:
Based on my tests this is not a new bug. But I am not sure what is going on.
At this point I can observe that it crashes when taking an std::mutex.
The following steps do build a working binary:
Creating a Z3 Context through the java API is causing a fatal error. I traced the problem to a call to the com.microsoft.z3.Context() constructor in a larger project. Below is a distilled example which reproduces the issue in my environment.
Installation
I downloaded latest yesterday, and installed via the 64-bit Windows compilation pathway.
In x64 Native Tools Command Prompt for VS 2022:
Then, I added the build directory to my PATH user environment variable.
Reproducing
Then, in the build directory, I created the following class with a small snippet from the JavaExample class.
Still in the build directory, I compiled and ran, as per the instructions in #7000.
This produced the following output.
The text was updated successfully, but these errors were encountered: