Z3 v4.3.2 Mac OS X上的example.py执行错误10.10

Question

我试图在Mac OS X 10.10.2上构建Z3最新版本（v4.3.2）。

下载从http://download-codeplex.sec.s-msft.com/Download/SourceControlFileDownload.ashx?he项目名= Z3 & changeSetId = cee7dd39444c9060186df79c2a2c7f8845de415b最新的源在http://z3.codeplex.com/SourceControl/latest#README跟随命令。

CXX=clang++ CC=clang python scripts/mk_make.py 
cd build 
make 
sudo make install 

构建和安装似乎没问题，但是，当我尝试运行example.py时，出现此错误。

Traceback (most recent call last): 
    File "example.py", line 3, in <module> 
    x = Real('x') 
    File "/Library/Python/2.7/site-packages/z3.py", line 2774, in Real 
    ctx = _get_ctx(ctx) 
    File "/Library/Python/2.7/site-packages/z3.py", line 210, in _get_ctx 
    return main_ctx() 
    File "/Library/Python/2.7/site-packages/z3.py", line 205, in main_ctx 
    _main_ctx = Context() 
    File "/Library/Python/2.7/site-packages/z3.py", line 151, in __init__ 
    conf = Z3_mk_config() 
    File "/Library/Python/2.7/site-packages/z3core.py", line 1036, in Z3_mk_config 
    r = lib().Z3_mk_config() 
    File "/Library/Python/2.7/site-packages/z3core.py", line 24, in lib 
    raise Z3Exception("init(Z3_LIBRARY_PATH) must be invoked before using Z3-python") 
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.Context instance at 0x227800>> ignored 

我在环境变量中添加export Z3_LIBRARY_PATH=/Library/Python/2.7/site-packages/，并尝试64位蟒蛇与arch -x86_64 python example.py得到相同的结果。

从Using Z3Py With Python 3.3，我试图将libz3.a/dylib/java.dylib文件复制到/Library/Python/2.7/site-packages，但没有成功。

什么可能是错误的？

Answer 1

它与Mac OS支持的64位python有关。 从提示Executing python in 64 bit mode on Mac OS X 10.10，我安装了Python与brew，现在它工作正常。

bin> /usr/local/Cellar/python/2.7.9/bin/python example.py 
sat 
[y = 4, x = 2]