Skip to content

Instantly share code, notes, and snippets.

@lionaneesh

lionaneesh/katy_csaw_2016_solution.py

Created November 13, 2016 11:41
Show Gist options
  • Save lionaneesh/c777ed8e7d9257f4f997961b2bfbb8fb to your computer and use it in GitHub Desktop.
Save lionaneesh/c777ed8e7d9257f4f997961b2bfbb8fb to your computer and use it in GitHub Desktop.
Download ZIP
Raw
katy_csaw_2016_solution.py
#!/usr/bin/env python
from z3 import *
s = Solver()
ret = BitVecVal(0, 32)
seed = BitVec('seed', 32)
ret = 25214903917 * seed + 11
ret = ret & 0xFFFFFFFFFFFF
s.add(ret == 1364650861) # 1364650861, 1208101748
if s.check() == sat:
model = s.model()
print model[seed]
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment