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

Question

当使用使用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

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

Answer 1

这是从 64 位版本的 python 调用 32 位版本的 Z3 时的常见错误，反之亦然。