Python binding to Z3

This is a Python binding to the SMT solver Z3. Since it is based on Python's dynamic foreign function interface ctypes, no compilation is required. For additions, corrections or suggestions, please contact me.

Download

• Python binding: z3-python-2.0.1.tar.gz

Please make sure the C header file provided along with the Python binding matches the header file you received along with Z3. For using the Python binding, the C header file is not required.

Please set the path to your Z3 library file in line 10 of the Python binding file:

_z3 = CDLL("PATH_TO_Z3_LIB")

This Python binding was tested with Python version 2.5.1 and 2.5.2.