web1.py

from z3 import *
import struct

a = [BitVec("a{}".format(i), 8) for i in range(5)]
s = Solver()

def is_valid(x):
    return Or(
        And(x >= ord('1'), x <= ord('9')),
        And(x >= ord('a'), x <= ord('z')),
        And(x >= ord('A'), x <= ord('Z'))
    )

s.add(
    22 == (88 ^ a[4]),
    a[3] % 65 == 0,
    a[2] + 30 >= 130,
    a[1] + a[2] == 161,
    2 == (a[0] ^ a[4]),
    26 == (a[0] ^ a[1] ^ a[2] ^ a[3] ^ a[4]),
    is_valid(a[1]),
    is_valid(a[2])
)

if s.check() == sat:
    m = s.model()
    p = ""
    for x in a:
        p += chr(m[x].as_long())
    print(p)
else:
    print("Unsat")