Context Instantiation Causing Access Violation - Java API

[wagne279]

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.
#

[NikolajBjorner]

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:

md build cd build cmake -DZ3_BUILD_JAVA_BINDINGS=True -G "Ninja" ..\ ninja javac -cp com.microsoft.z3.jar Simple.java java -cp "com.microsoft.z3.jar;." Simple

[kris7t]

I get a working binary when I build z3-4.13.2 with

cmake -DZ3_BUILD_JAVA_BINDINGS=True -G "Ninja" ..

but a broken one when I build with

cmake -DCMAKE_BUILD_TYPE=Release -DZ3_BUILD_JAVA_BINDINGS=True -G "Ninja" ..

so something must be broken with the optimized builds with MSVC. The bug is likely not in the Java API itself: I can reproduce it even by combining a debug z3java.dll with a release libz3.dll.

---

Interestingly, compiling z3-4.12.6 also in Release mode also produces a crashing binary, but the binaries released on Github do work. So perhaps cmake uses different build flags for release build than mk_make.py, and the binaries only recently broke with the mk_make.py flags, but have been broken since a longer time with the cmake flags?