运行 Z3 java绑定时出错

Question

我运行 JavaExample.java 随 Z3 4.4.2 提供，但我得到以下输出然后出现错误：

Z3 Major Version: 4
Z3 Full Version: 4.3.2.0
SimpleExample
Opt
Exception in thread "main" java.lang.UnsatisfiedLinkError: com.microsoft.z3.Native.INTERNALmkOptimize(J)J
    at com.microsoft.z3.Native.INTERNALmkOptimize(Native Method)
    at com.microsoft.z3.Native.mkOptimize(Native.java:5208)
    at com.microsoft.z3.Optimize.<init>(Optimize.java:262)
    at com.microsoft.z3.Context.mkOptimize(Context.java:3043)
    at Z3Example.optimizeExample(Z3Example.java:2323)
    at Z3Example.main(Z3Example.java:2362)

公平地说，我使用的是 4.3.2 提供的 64 位 libz3java.dll，同时使用版本 4.4 的 jar 文件 com.microsoft.z3.jar .2，因为那是我设法开始工作的唯一组合（详细说明了这些问题）。可能是版本差异导致此错误的原因，还是有其他原因？

Answer 1

是的，版本差异是导致此问题的原因：4.3.2 不支持优化，因此 mkOptimize 不附带。其他问题我再单独看看

运行 Z3 java绑定时出错

Error when running Z3 java binding

java

z3