Why is Z3 optimization in Java segfaulting?

Question

In a Java project I'm working on, I have a wrapper class around Z3. When I was testing optimization, my program crashed with a segfault. After some experimentation, I was able to find this minimum reproducible example, which simply creates a context and optimizer, and checks the optimizer:

import com.microsoft.z3.*;

public class Z3Test {

  public static void main(String[] args) {
    try (Context ctx = new Context()) {
      Optimize opt = ctx.mkOptimize();
      System.out.println("Check: " + opt.Check());
    }
  }
}

Note that the program still segfaults without the try block, i.e.

Context ctx = new Context();
Optimize opt = ctx.mkOptimize();
System.out.println("Check: " + opt.Check());

Solving without optimizing, on the other hand, runs just fine:

try (Context ctx = new Context()) {
  Solver opt = ctx.mkSolver();
  System.out.println("Check: " + opt.check());
}

Check: SATISFIABLE

What could I be doing wrong? Some potentially relevant information:

OS:

macOS 10.15.3

Java Version:

openjdk 14 2020-03-17
OpenJDK Runtime Environment (build 14+36-1461)
OpenJDK 64-Bit Server VM (build 14+36-1461, mixed mode, sharing)

I have libz3.dylib and libz3java.dylib in the directory where I'm running the code.

Stack trace from log file:

Native frames: (J=compiled Java code, A=aot compiled Java code, j=interpreted, Vv=VM code, C=native code)
C  [libz3.dylib+0x79f96]  Z3_optimize_check+0x76
C  [libz3java.dylib+0x8425]  Java_com_microsoft_z3_Native_INTERNALoptimizeCheck+0x45
j  com.microsoft.z3.Native.INTERNALoptimizeCheck(JJ)I+0
j  com.microsoft.z3.Native.optimizeCheck(JJ)I+2
j  com.microsoft.z3.Optimize.Check()Lcom/microsoft/z3/Status;+11
j  jaedmax.Main.main([Ljava/lang/String;)V+17
v  ~StubRoutines::call_stub
V  [libjvm.dylib+0x34b082]  JavaCalls::call_helper(JavaValue*, methodHandle const&, JavaCallArguments*, Thread*)+0x256
V  [libjvm.dylib+0x38f7f1]  jni_invoke_static(JNIEnv_*, JavaValue*, _jobject*, JNICallType, _jmethodID*, JNI_ArgumentPusher*, Thread*)+0x11c
V  [libjvm.dylib+0x3930d4]  jni_CallStaticVoidMethod+0x1b3
C  [libjli.dylib+0x4ac2]  JavaMain+0xab4
C  [libjli.dylib+0x6d6a]  ThreadJavaMain+0x9
C  [libsystem_pthread.dylib+0x5e65]  _pthread_start+0x94
C  [libsystem_pthread.dylib+0x183b]  thread_start+0xf

Project directory structure:

.
├── build.xml
├── lib
│   └── com.microsoft.z3-4.7.1.jar
├── libz3.dylib
├── libz3java.dylib
└── src
    └── Z3Test.java

Ant build file:

<project name="Z3Test" basedir="." default="run">

  <path id="lib.path">
    <pathelement location="lib/com.microsoft.z3-4.7.1.jar"/>
  </path>

  <path id="class.path">
    <path refid="lib.path"/>
    <pathelement location="build"/>
  </path>

  <target name="clean">
    <delete dir="build"/>
    <delete>
      <fileset dir="." includes="**/*.log"/>
    </delete>
  </target>

  <target name="compile" depends="clean">
    <mkdir dir="build"/>
    <javac srcdir="src" destdir="build" classpathref="lib.path" includeantruntime="no"/>
  </target>

  <target name="run" depends="compile">
    <java classname="Z3Test" classpathref="class.path" fork="yes"/>
  </target>

</project>

Answer 1

It appears you might have a problem with your z3 and/or Java installation. To keep everything simple, I did the following:

$ cat Z3Test.java
import com.microsoft.z3.*;

public class Z3Test {

  public static void main(String[] args) {
    try (Context ctx = new Context()) {
      Optimize opt = ctx.mkOptimize();
      System.out.println("Check: " + opt.Check());
    }
  }
}

Then:

$ javac -cp /usr/local/z3/build/com.microsoft.z3.jar:. Z3Test.java
$ java -Djava.library.path=/usr/local/z3/build -cp /usr/local/z3/build/com.microsoft.z3.jar:. Z3Test
Check: SATISFIABLE

So it all worked out just fine. See if you can replicate this on your command line. If so, issue must be somewhere else in your build system. If it fails, perhaps your best bet is to reinstall z3 with java bindings from scratch.