0

I'm trying to build Z3 newest version (v4.3.2) on Mac OS X 10.10.2.

Downloading the latest source from http://download-codeplex.sec.s-msft.com/Download/SourceControlFileDownload.ashx?he ProjectName=z3&changeSetId=cee7dd39444c9060186df79c2a2c7f8845de415b to follow the command in http://z3.codeplex.com/SourceControl/latest#README.

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

The build and installation seems to be OK, however, when I tried to run the example.py, I got this error. 

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

I added export Z3_LIBRARY_PATH=/Library/Python/2.7/site-packages/ in the environment variables, and tried 64 bit python with arch -x86_64 python example.py to get the same results.

From Using Z3Py With Python 3.3, I tried to copy the libz3.a/dylib/java.dylib files into the /Library/Python/2.7/site-packages, but without success.

What might be wrong?

Community
  • 1
  • 1
prosseek
  • 182,215
  • 215
  • 566
  • 871
  • Did you try setting `PYTHONPATH` to Z3's `bin` directory? You could also copy your `py`-file into Z3's `bin` directory (where `z3.pyc` etc. are), and run it from there. Does any of that help? – Malte Schwerhoff Mar 19 '15 at 09:14
  • @Malte Schwerhoff: I tried to set PYTHONPATH, but got the same results. – prosseek Mar 19 '15 at 13:13
  • I had a similar problem on Win 7 x64, which apparently was due to using x86 Python with x64 Z3. The error disappeared after using x86 builds of both. – Malte Schwerhoff Mar 20 '15 at 11:54
  • Yes, everything needs to be of the same bit-ness, i.e., Python 32-bit will refuse to load a 64-bit z3 and the other way around. In this particular case, did you also set DYLD_LIBRARY_PATH to include the z3 bin directory? Otherwise the system will not be able to find libz3.dylib. – Christoph Wintersteiger Mar 21 '15 at 17:17

1 Answers1

0

It has something to do with 64 bit python that Mac OS supports. From the hint Executing python in 64 bit mode on Mac OS X 10.10, I installed python with brew, and now it works fine. 

bin> /usr/local/Cellar/python/2.7.9/bin/python example.py 
sat
[y = 4, x = 2]
Community
  • 1
  • 1
prosseek
  • 182,215
  • 215
  • 566
  • 871