Generate valid input (printable) for pwnable.kr's collision

collision.py

import struct
from z3 import *

p = [BitVec('p{}'.format(i), 32) for i in range(5)]
s = Solver()

for a in p:
    for i in range(4):
        s.add(((a >> i*8) & 0xff) >= 0x30)
        s.add(((a >> i*8) & 0xff) <= 0x7a)
        s.add(((a >> i*8) & 0xff) != 0x60)

s.add(p[0] + p[1] + p[2] + p[3] + p[4] == 0x21DD09EC)

if s.check() == sat:
    m = s.model()
    print(''.join(struct.pack("<I", m[a].as_long()).decode() for a in p))
else:
    print("Unsat")