我正在尝试使用Z3的Java绑定，尤其是尝试运行在Z3的4.4.2版本中分发的Java示例JavaExample.java。
当我使用4.4.2 com.microsoft.z3.jar文件时，JavaExample.java编译正常。但是，由于默认libz3java.dll是32位并且我的环境是64位，因此它无法运行。我尝试为其Makefile制造商-x用scripts/mk_make.py标志构建一个64位Z3，但是当我运行nmake时会产生错误（关于here的帖子）。
无论如何，然后我下载了Z3 4.3.2版本的二进制文件，其中包含一个64位的libz3java.dll。但是，现在JavaExample.java无法编译，从而产生大量错误，例如：
FiniteDomainNum cannot be resolved to a type Z3Example.java line 2222
线
FiniteDomainNum s1 = (FiniteDomainNum)ctx.mkNumeral(1, s);
有数百个这样的错误。
jar文件已正确包含在Eclipse项目中，就像
JavaExample.java编译时的4.4.2一样。有什么帮助吗？谢谢。
最佳答案
这些错误很可能是由于com.microsoft.z3.jar丢失或不完整而引起的。您需要先整理另一篇文章中描述的编译问题，然后Java API才能正常工作。
关于java - Z3的Java绑定(bind)的JavaExample.java测试的编译错误，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/35286636/