Z3 and Eclipse IDE

Question

I am trying to using Z3 (http://z3.codeplex.com/) within Eclipse IDE. I installed PyDev and downloaded the Z3's pre-compiled Windows binaries. I also added the "bin" subdirectory to the environment variables PYTHONPATH and PATH.

In this very simple example,

from z3 import *

x = Real('x')
y = Real('y')
s = Solver()
s.add(x + y > 5, x > 1, y > 1)
print s.check()
print s.model()

Eclipse says that Real e Solver are undefined variables. Running this code I got this error msg:

"ImportError: Bad magic number in ...\bin\z3.pyc"

It seems that this is a problem of different version of python (usually later) than the interpreter (see: What's the bad magic number error?).

Any help? Do I need to compile and install Z3Py rather than using the pre-compiled Windows binaries?

Thanks.

Answer 1

I'm not very familiar with using Python from Eclipse, but it's very likely that this is indeed because of a mismatch of Python versions. The safest way is perhaps to install the 32-bit version of Python 2.7.x and to make sure that Eclipse also uses this version. Alternatively, you could compile Z3 yourself, using your favorite version of Python for the Python bindings. I'd advise to use the unstable branch as this contains many fixes that are not integrated in the master branch yet (for compilation instructions see the README). Note that there are also precompiled Windows binaries for the unstable branch in the `planned' section on Codeplex (see here), which may solve this problem.