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