在我正在进行的一个Java项目中,我有一个围绕Z3的包装类。当我测试优化时,我的程序崩溃了并出现了段错误。经过一些实验,我能够找到这个最小可重现的示例,它只是创建一个上下文和优化器,并检查优化器:
请注意,没有try块时程序仍会发生段错误,即:
不进行优化的解决方案,另一方面,运行良好。
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());
}
}
}
请注意,没有try块时程序仍会发生段错误,即:
Context ctx = new Context();
Optimize opt = ctx.mkOptimize();
System.out.println("Check: " + opt.Check());
不进行优化的解决方案,另一方面,运行良好。
try (Context ctx = new Context()) {
Solver opt = ctx.mkSolver();
System.out.println("Check: " + opt.check());
}
检查:可满足
我可能做错了什么?以下是一些可能相关的信息:
操作系统:
macOS 10.15.3
Java 版本:
openjdk 14 2020-03-17
OpenJDK Runtime Environment (build 14+36-1461)
OpenJDK 64-Bit Server VM (build 14+36-1461, mixed mode, sharing)
我在运行代码的目录中有libz3.dylib和libz3java.dylib。
来自日志文件的堆栈跟踪:
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
项目目录结构:
.
├── build.xml
├── lib
│ └── com.microsoft.z3-4.7.1.jar
├── libz3.dylib
├── libz3java.dylib
└── src
└── Z3Test.java
Ant 构建文件:
<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>
main
函数等),其中包括您用于编译它的命令行标志。 - alias