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.
- 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.