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.
% 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-18.104.22.168.tar.gz % tar -zxvf z3-solver-22.214.171.124.tar.gz % cd z3-solver-126.96.36.199 % python setup.py build % python setup.py install
>>> 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( x2*x1-x4*x3 == 0x24CDF2E7C953DA56) # constraints can be added using the method add() >>> s.add( 3*x3+4*x4-x2-2*x1 == 0x17B85F06) >>> s.add( 3*x1*x4-x3*x2 == 0x2E6E497E6415CF3E) >>> 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]