# Z3Py for CTF

## TL; DR

Z3 is a high performace theorem prover developed by Microsoft. And Z3Py is Z3 API in Python.

In some reverse or crypto questions in CTF, Z3 is a powerful tool to solve your euqations and return the answer to you.

## Install

``% sudo pip install z3 z3-solver``

If it doesn't work, maybe you can try to install z3 from the source code:

``````% wget https://files.pythonhosted.org/packages/7c/65/2656e6157f921cb3b28999d2441997d069f6e94b9e077a614064702f09df/z3-solver-4.8.6.0.tar.gz
% tar -zxvf z3-solver-4.8.6.0.tar.gz
% cd z3-solver-4.8.6.0
% python setup.py build
% python setup.py install``````

## Getting started

``````>>> from z3 import *
>>> x = Int('x') # create an interger variable in Z3 named x
>>> y = Int('y') # create an interger variable in Z3 named y
>>> solve(x > 2, y < 10, x + 2*y == 7) # solve a system of constraints
[y = 0, x = 7]``````
``````>>> from z3 import *
>>> x1 = Int('x1')
>>> x2 = Int('x2')
>>> x3 = Int('x3')
>>> x4 = Int('x4')
>>> s = Solver() # create a general purpose solver
>>> s.add( 27*x2+x1-11*x4 - x3 == 0x95AE13337)
>>> print s.check() # solve the asserted constraints
sat # the result is sat(satisifable) or unsat(unsatisfiable)
>>> m = s.model() # final solution. we say the solution is a "model" for the set of asserted constrains
>>> print m
[x2 = 1801073242,
x4 = 862734414,
x3 = 829124174,
x1 = 1869639009]
>>> for d in m.decls():
...     print "%s = %s" % (d.name(), m[d])
...
x2 = 1801073242
x4 = 862734414
x3 = 829124174
x1 = 1869639009``````
``````>>> from z3 import *
>>> a = Int('a') # declare single interger variable at once
>>> b, c, d = Ints('b c d') # declare multiple interger variables at once
>>> e = Real('e') # create the real variable e
>>> f, g, h = Reals('f g h')
>>> i, j, k = BitVecs('i, j, k', 8) # declare three bit-vectors variables with 8 bits
>>> solve(i^j&k == 12, j&i>>3 == 3, k^j == 4) # it works like this
[j, = 23, k = 19, i, = 31] ``````
• • 