Windows: Z3Exception("init(Z3_LIBRARY_PATH) 必须在使用 Z3-python 之前调用")

Posted 2023-02-25

【中文标题】Windows: Z3Exception("init(Z3_LIBRARY_PATH) 必须在使用 Z3-python 之前调用")

【英文标题】：Windows: Z3Exception("init(Z3_LIBRARY_PATH) must be invoked before using Z3-python")

【发布时间】：2018-02-11 02:35:45

【问题描述】：

在使用使用 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 中，我添加了每个可能需要存在的目录，例如：

【参考方案1】：

你见过Installing Z3 + Python on Windows吗？正如 Nikolaj 指出的那样，在 Z3 或 Python 或您的机器本身中似乎是 32/64 位混淆。

【讨论】：

是的。我使用的是 64 位版本的 Z3 和 python。

【参考方案2】：

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

【讨论】：

我正在使用 64 位版本的 python（在 python 控制台中由import platform 和platform.architecture()[0] 验证）并尝试在github.com/Z3Prover/z3/releases/tag/z3-4.5.0 使用 Windows 的 64 位版本的 z3（而不是下载源代码和编译）。我已将“C:\Python27\Lib\site-packages\oyente\z3-4.5.0-x64-win\bin”（包含 libz3.dll）添加到我的 PYTHONPATH 系统变量中，但仍然出现相同的错误。跨度>

您是否也将该路径添加到您的 PATH 中？ （系统需要查看 .dll；Python 需要查看 .py 文件。）