在使用使用 Z3(我在 Visual Studio 命令提示符中构建)的 python 脚本 (oyente) 时，我遇到了以下错误:

File "C:\Python27\Lib\site-packages\oyente\z3\z3core.py", line 23, in lib
    raise Z3Exception("init(Z3_LIBRARY_PATH) must be invoked before using Z3-python")
z3.z3types.Z3Exception: init(Z3_LIBRARY_PATH) must be invoked before using Z3-python
Exception AttributeError: "Context instance has no attribute 'lib'" in <bound method Context.__del__ of <z3.z3.Context instance at 0x0000000003A5AC48>> ignored

我在 z3 和 oyente 目录中有 libz3.dll 文件，在我的 PYTHONPATH 系统变量中，我添加了可能需要存在的每个目录，例如:

最佳答案

这是从 64 位版本的 python 或其他方式调用 32 位版本的 Z3 时的常见错误。

关于python - window : Z3Exception ("init(Z3_LIBRARY_PATH) must be invoked before using Z3-python")，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/46010223/