z3使用mkOptimize的java api

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库。