z3 java api 使用 mkOptimize

Question

我通过 context.mkOptimize() 在 java api 中使用 z3 的优化选项。当我执行我的代码时，它会显示以下错误：

java.lang.UnsatisfiedLinkError: com.microsoft.z3.Native.INTERNALmkOptimize(J)J

我的代码：

Context context = new Context();
Optimize mkOptimize = context.mkOptimize();

IntExpr intTest = context.mkIntConst("test");
IntExpr intTen = context.mkInt(10);
BoolExpr assertInt = context.mkLe(intTest, intTen);

mkOptimize.Add(assertInt);
mkOptimize.MkMaximize(intTest);
mkOptimize.Check();

是我做错了什么还是 java api 中的错误？ （第二行创建优化对象时抛出异常）

Answer 1

发现问题。这是因为系统路径指向两个不同版本的 z3 库。