Context Instantiation Causing Access Violation - Java API #7405
Open
Description
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.
import com.microsoft.z3.*;
class Simple {
// / "Hello world" example: create a Z3 logical context, and delete it.
public static void simpleExample()
{
System.out.println("SimpleExample");
{
Context ctx = new Context();
/* do something with the context */
/* be kind to dispose manually and not wait for the GC. */
ctx.close();
}
}
public static void main(String[] args) {
simpleExample();
}
}Still in the build directory, I compiled and ran, as per the instructions in #7000.
javac -cp com.microsoft.z3.jar Simple.java
java -cp "com.microsoft.z3.jar;." Simple
This produced the following output.
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.
#
Metadata
Assignees
Labels
No labels