I've installed Microsoft Z3 (Z3 [version 4.3.0 - 64 bit]. (C) 2006
) and it's pyc
binaries for Python2.
I've written an Python3 package which needs access to z3
functionality.
In order to be able to use the pyc
binaries with my Python3 package, I decompyle
the z3
binaries and applied 2to3
.
Int('string')
doesn't work because Z3Py isn't able to handle the new <class 'str'>
used as 'string'
argument:
>>> import z3; z3.Int('abc')
Traceback (most recent call last):
File "<stdin>", line 1, in <module>
File ".\bin\z3.py", line 2931, in Int
return ArithRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), IntSort(ctx).ast), ctx)
File ".\bin\z3.py", line 72, in to_symbol
return Z3_mk_string_symbol(_get_ctx(ctx).ref(), s)
File ".\bin\z3core.py", line 1430, in Z3_mk_string_symbol
r = lib().Z3_mk_string_symbol(a0, a1)
ctypes.ArgumentError: argument 2: <class 'TypeError'>: wrong type
decompyle
Z3's *.pyc
files first. So, are there any Z3Py source codes available?Thanks. - If anything's unclear, please leave a question comment.
The unstable
(work-in-progress) has support for Python 3. This feature will be available in the next Z3 release (v4.3.2). In the meantime, you can build the unstable
branch using the instructions found here.