Internetwache CTF 2016: EquationSolver (exp 60)

Description

I created a program for an unsolveable equation system. My friend somehow forced it to solve the equations. Can you tell me how he did it?

Exploit

This challenge asks us to solve the following equations.

Solve the following equations:
X > 1337
X * 7 + 4 = 1337

Obviously, the solution exists only if the integer overflow exists. I use Z3 to solve this problem.

1
2
3
4
5
6
7
8
9
10

from z3 import Solver, BitVec

s = Solver()
x = BitVec('x', 32)

s.add(x > 1337)
s.add(x*7 + 4 == 1337)

s.check()
print s.model()

$ python solve.py
[x = 613566947]

Flag: IW{Y4Y_0verfl0w}