Create a gist now

Instantly share code, notes, and snippets.

@integeruser /amadhj.py Secret
Last active Feb 12, 2017

What would you like to do?
Collection of z3 scripts
#!/usr/bin/env python2
import struct
import z3
def s264(s):
return struct.unpack('<Q', s)[0]
def to8(i):
return i & 0xff
def to16(i):
return i & 0xffff
def to32(i):
return i & 0xffffffff
################################################################################
def f_a(a1, a2):
return a1 ^ a2
def f_b(a1, a2, a3):
return (to8(z3.LShR(a1, 8 * a2)) << 8 * a3) | (to8(z3.LShR(a1, 8 * a3)) << 8 * a2) | ~(
255 << 8 * a2) & ~(255 << 8 * a3) & a1
def f_c(a1, a2):
return (a1 << (a2 & 0x3F)) | (z3.LShR(a1, (64 - (a2 & 0x3F))))
def f_d(a1, a2):
return (a1 << (64 - (a2 & 0x3F))) | z3.LShR(a1, (a2 & 0x3F))
def f_e(a1):
return (a1 << 56) ^ a1 & 0xFF00000000000000 | z3.LShR(
(to16(a1) & 0xFF00), 8) ^ to8(a1) | z3.LShR(
(a1 & 0xFF0000), 8) ^ to16(a1) & 0xFF00 | z3.LShR(
(to32(a1) & 0xFF000000), 8) ^ a1 & 0xFF0000 | z3.LShR(
(a1 & 0xFF00000000), 8) ^ to32(a1) & 0xFF000000 | z3.LShR(
(a1 & 0xFF0000000000), 8) ^ a1 & 0xFF00000000 | z3.LShR(
(a1 & 0xFF000000000000), 8) ^ a1 & 0xFF0000000000 | z3.LShR(
(a1 & 0xFF00000000000000), 8) ^ a1 & 0xFF000000000000
def f_f(a1):
return z3.LShR((a1 & 0xFF00000000000000), 8) | z3.LShR((a1 & 0xFF000000000000), 40) | z3.LShR(
(a1 & 0xFF0000000000), 40) | z3.LShR((a1 & 0xFF00000000), 16) | (
(to32(a1) & 0xFF000000) << 16) | ((a1 & 0xFF0000) << 40) | (
(to16(a1) & 0xFF00) << 24) | (to16(a1) << 24)
def check1(i):
v1 = f_a(i, 3861390726976975706)
v2 = f_b(v1, 2, 0)
v3 = f_a(v2, 0x89FDAF6604952DF1)
v4 = f_a(v3, 0xE9F30F0CE704876A)
v5 = f_b(v4, 2, 3)
v6 = f_a(v5, 0xBDC5026D3C0B56E6)
v7 = f_c(v6, 16)
v8 = f_c(v7, 35)
v9 = f_d(v8, 19)
v10 = f_e(v9)
v11 = f_c(v10, 36)
v12 = f_d(v11, 40)
v13 = f_b(v12, 1, 0)
v14 = f_a(v13, 6765015749217278743)
v15 = f_f(v14)
v16 = f_f(v15)
v17 = f_b(v16, 2, 1)
v18 = f_a(v17, 7686949068708848117)
v19 = f_b(v18, 3, 0)
v20 = f_f(v19)
v21 = f_a(v20, 6401935715922169987)
v22 = f_d(v21, 22)
v23 = f_e(v22)
v24 = f_a(v23, 5166993816397978483)
v25 = f_e(v24)
v26 = f_e(v25)
v27 = f_b(v26, 6, 5)
v28 = f_c(v27, 59)
v29 = f_b(v28, 5, 2)
v30 = f_b(v29, 2, 3)
v31 = f_c(v30, 12)
v32 = f_a(v31, 0xAD25307F8E364B17)
v33 = f_a(v32, 5234710379464860866)
v34 = f_c(v33, 6)
v35 = f_b(v34, 6, 5)
v36 = f_d(v35, 11)
v37 = f_f(v36)
v38 = f_a(v37, 0x869365DB4C9F3CB6)
v39 = f_f(v38)
v40 = f_d(v39, 2)
v41 = f_a(v40, 4649309708712362587)
v42 = f_c(v41, 35)
v43 = f_c(v42, 9)
v44 = f_e(v43)
v45 = f_c(v44, 7)
v46 = f_c(v45, 38)
v47 = f_e(v46)
v48 = f_a(v47, 0xDEF2D72447EF4E1B)
v49 = f_f(v48)
v50 = f_f(v49)
v51 = f_b(v50, 2, 7)
v52 = f_d(v51, 51)
v53 = f_f(v52)
v54 = f_d(v53, 19)
v55 = f_a(v54, 0x95DE49591A44EE21)
v56 = f_e(v55)
v57 = f_f(v56)
return f_d(v57, 16)
def check2(i):
v1 = f_c(i, 22)
v2 = f_f(v1)
v3 = f_b(v2, 4, 1)
v4 = f_f(v3)
v5 = f_e(v4)
v6 = f_c(v5, 35)
v7 = f_b(v6, 2, 6)
v8 = f_a(v7, 0x80A9EA4F90944FEA)
v9 = f_c(v8, 3)
v10 = f_b(v9, 0, 1)
v11 = f_b(v10, 1, 2)
v12 = f_f(v11)
v13 = f_e(v12)
v14 = f_b(v13, 5, 1)
v15 = f_d(v14, 24)
v16 = f_c(v15, 39)
v17 = f_b(v16, 2, 4)
v18 = f_a(v17, 7462025471038891063)
v19 = f_b(v18, 4, 3)
v20 = f_b(v19, 0, 7)
v21 = f_c(v20, 62)
v22 = f_f(v21)
v23 = f_b(v22, 7, 6)
v24 = f_b(v23, 2, 6)
v25 = f_f(v24)
v26 = f_e(v25)
v27 = f_b(v26, 5, 2)
v28 = f_e(v27)
v29 = f_b(v28, 1, 7)
v30 = f_a(v29, 4749710960471120103)
v31 = f_f(v30)
v32 = f_e(v31)
v33 = f_b(v32, 1, 4)
v34 = f_c(v33, 10)
v35 = f_f(v34)
v36 = f_f(v35)
v37 = f_d(v36, 24)
v38 = f_b(v37, 0, 4)
v39 = f_d(v38, 61)
v40 = f_b(v39, 3, 4)
v41 = f_d(v40, 35)
v42 = f_c(v41, 55)
v43 = f_c(v42, 34)
v44 = f_e(v43)
v45 = f_e(v44)
v46 = f_d(v45, 23)
v47 = f_c(v46, 59)
v48 = f_d(v47, 20)
v49 = f_c(v48, 28)
v50 = f_a(v49, 0xC26499379C0927CD)
v51 = f_e(v50)
return f_d(v51, 13)
def check3(i):
v1 = f_c(i, 18)
v2 = f_c(v1, 29)
v3 = f_b(v2, 5, 3)
v4 = f_b(v3, 0, 7)
v5 = f_c(v4, 18)
v6 = f_a(v5, 0xC9AB604BB92038AD)
v7 = f_d(v6, 33)
v8 = f_b(v7, 0, 4)
v9 = f_e(v8)
v10 = f_b(v9, 6, 2)
v11 = f_d(v10, 13)
v12 = f_d(v11, 20)
v13 = f_a(v12, 6368261268581873766)
v14 = f_e(v13)
v15 = f_f(v14)
v16 = f_d(v15, 46)
v17 = f_b(v16, 2, 3)
v18 = f_d(v17, 44)
v19 = f_d(v18, 3)
v20 = f_b(v19, 4, 3)
v21 = f_e(v20)
v22 = f_b(v21, 7, 6)
v23 = f_d(v22, 59)
v24 = f_d(v23, 38)
v25 = f_f(v24)
v26 = f_b(v25, 1, 5)
v27 = f_f(v26)
v28 = f_c(v27, 27)
v29 = f_a(v28, 0xBED577A97EB7966F)
v30 = f_d(v29, 14)
v31 = f_c(v30, 7)
v32 = f_c(v31, 18)
v33 = f_c(v32, 57)
v34 = f_a(v33, 0xB44427BE7889C31B)
v35 = f_a(v34, 929788566303591270)
v36 = f_a(v35, 0x94B1608ADB7F7221)
v37 = f_a(v36, 0x85BEF139817EBC4A)
v38 = f_b(v37, 5, 1)
v39 = f_c(v38, 20)
v40 = f_c(v39, 24)
v41 = f_d(v40, 46)
v42 = f_d(v41, 13)
v43 = f_a(v42, 0xC95E5C35034B9775)
v44 = f_c(v43, 7)
v45 = f_a(v44, 641209893495219690)
v46 = f_a(v45, 6473287570272602621)
v47 = f_e(v46)
v48 = f_b(v47, 4, 7)
v49 = f_e(v48)
v50 = f_d(v49, 22)
v51 = f_d(v50, 50)
return f_e(v51)
def check4(i):
v1 = f_b(i, 1, 7)
v2 = f_c(v1, 6)
v3 = f_b(v2, 2, 5)
v4 = f_d(v3, 57)
v5 = f_a(v4, 902179681853661902)
v6 = f_b(v5, 5, 1)
v7 = f_c(v6, 1)
v8 = f_e(v7)
v9 = f_a(v8, 6764338754798371998)
v10 = f_e(v9)
v11 = f_c(v10, 6)
v12 = f_e(v11)
v13 = f_c(v12, 33)
v14 = f_d(v13, 25)
v15 = f_e(v14)
v16 = f_a(v15, 762415417889401952)
v17 = f_b(v16, 6, 2)
v18 = f_e(v17)
v19 = f_a(v18, -3724318961155856981)
v20 = f_a(v19, -8646321147571282756)
v21 = f_e(v20)
v22 = f_a(v21, -8802313616937474543)
v23 = f_d(v22, 8)
v24 = f_d(v23, 43)
v25 = f_a(v24, 7150187182015826299)
v26 = f_b(v25, 3, 1)
v27 = f_b(v26, 5, 7)
v28 = f_f(v27)
v29 = f_e(v28)
v30 = f_d(v29, 59)
v31 = f_d(v30, 10)
v32 = f_e(v31)
v33 = f_b(v32, 2, 1)
v34 = f_b(v33, 7, 2)
v35 = f_e(v34)
v36 = f_a(v35, 7246290916701591349)
v37 = f_a(v36, -243320396905423181)
v38 = f_a(v37, -43605043069428557)
v39 = f_b(v38, 2, 4)
v40 = f_b(v39, 5, 4)
v41 = f_d(v40, 11)
v42 = f_e(v41)
v43 = f_c(v42, 39)
v44 = f_f(v43)
v45 = f_e(v44)
v46 = f_a(v45, -4064264580452746468)
v47 = f_f(v46)
v48 = f_e(v47)
v49 = f_c(v48, 35)
v50 = f_b(v49, 3, 5)
v51 = f_e(v50)
v52 = f_f(v51)
return f_e(v52)
if __name__ == '__main__':
s = z3.Solver()
i1 = z3.BitVec('i1', 64)
i2 = z3.BitVec('i2', 64)
i3 = z3.BitVec('i3', 64)
i4 = z3.BitVec('i4', 64)
for v in [i1, i2, i3, i4]:
for i in range(8):
mask = 0xff << (i * 8)
s.add(z3.Or(v & mask == (32 << (i * 8)), v & mask > (0x40 << (i * 8))))
s.add(v & mask <= (0x7a << (i * 8)))
s.add(v & mask != (91 << (i * 8)))
s.add(v & mask != (92 << (i * 8)))
s.add(v & mask != (93 << (i * 8)))
s.add(v & mask != (94 << (i * 8)))
s.add(v & mask != (96 << (i * 8)))
r1 = check1(i1)
r2 = check2(i2)
r3 = check3(i3)
r4 = check4(i4)
res = r1 ^ r2 ^ r3 ^ r4
s.add(res == 0xB101124831C0110A)
assert s.check() == z3.sat
model = s.model()
print repr(''.join(struct.pack('<Q', model[v].as_long()) for v in [i1, i2, i3, i4]))
# V YYVZj iyVFvxPDalGHWT aLw YT
# $ nc amadhj_b76a229964d83e06b7978d0237d4d2b0.quals.shallweplayaga.me 4567
# V YYVZj iyVFvxPDalGHWT aLw YT
# The flag is: Da robats took err jerbs.
#!/usr/bin/env python2
from z3 import *
solver = Solver()
s = [BitVec('v%02d' % i, 8) for i in range(20)]
LOBYTE_off_606018_0 = 0
LOBYTE_off_606020_0 = 0
BYTE2_off_606020_0 = 0
BYTE1_off_606028_0 = 0x60
off_606038 = 0x90
BYTE1_off_606038 = 0x60
BYTE2_off_606038 = 0x60
BYTE3_off_606038 = 0x90
v8 = s[0] ^ s[1]
solver.add(Not((s[0] ^ s[1]) <= 15))
v8 = s[0] & s[1]
solver.add(Not((s[0] & s[1]) > 80))
v8 = s[18] & s[1]
solver.add(Not((s[18] & s[1]) > 48))
v8 = s[7] & s[4] ^ s[0]
solver.add(Not(v8 > 44))
v8 = s[0] & s[2]
solver.add(Not((s[0] & s[2]) <= 72))
v8 = s[11] & s[17]
solver.add(Not((s[11] & s[17]) <= 72))
v8 = s[0] ^ s[13]
solver.add(Not((s[0] ^ s[13]) <= 43))
v8 = s[13] ^ s[10]
solver.add(Not((s[13] ^ s[10]) <= 66))
v8 = s[11] ^ s[16]
solver.add(Not((s[11] ^ s[16]) > 16))
v8 = s[10] ^ s[8]
solver.add(Not((s[10] ^ s[8]) > 83))
v8 = s[19] ^ s[5]
solver.add(Not((s[19] ^ s[5]) <= 117))
v8 = s[0] | s[1]
solver.add(Not((s[0] | s[1]) <= 16))
v8 = s[17] & s[3]
solver.add(Not((s[17] & s[3]) <= 80))
v8 = off_606038 ^ s[1]
solver.add(Not((off_606038 ^ s[1]) > 23))
v8 = ~s[14]
solver.add(Not(~s[14] > 1))
v8 = s[13] | s[15]
solver.add(Not((s[13] | s[15]) <= 116))
v8 = s[0] >> 5
solver.add(Not((s[0] >> 5) <= 0))
v8 = ~s[19]
solver.add(Not(~s[19] > 1))
v8 = s[1] ^ s[11]
solver.add(Not((s[1] ^ s[11]) <= 28))
v8 = s[12] ^ s[15]
solver.add(Not((s[12] ^ s[15]) > 18))
v8 = s[13] & s[1]
solver.add(Not((s[13] & s[1]) <= 47))
v8 = (s[10] ^ s[19]) & s[12]
solver.add(Not(v8 > 108))
v8 = ~s[6]
solver.add(Not(~s[6] > 1))
v8 = s[1] ^ s[9]
solver.add(Not((s[1] ^ s[9]) <= 7))
v8 = s[16] >> 1
solver.add(Not((s[16] >> 1) <= 25))
v8 = LOBYTE_off_606018_0 ^ s[8]
solver.add(Not((LOBYTE_off_606018_0 ^ s[8]) <= 99))
v8 = ~s[6]
solver.add(Not(~s[6] > 1))
v8 = s[4] & s[12]
solver.add(Not((s[4] & s[12]) <= 41))
v8 = s[16] >> 1
solver.add(Not((s[16] >> 1) <= 14))
v8 = ~s[14]
solver.add(Not(~s[14] > 1))
v8 = s[0] >> 5
solver.add(Not((s[0] >> 5) > 48))
v8 = ~s[19]
solver.add(Not(~s[19] > 1))
v8 = s[0] ^ s[1]
solver.add(Not((s[0] ^ s[1]) > 45))
v8 = s[0] & s[1]
solver.add(Not((s[0] & s[1]) <= 0))
v8 = ~s[14]
solver.add(Not(~s[14] > 1))
v8 = s[0] ^ s[19]
solver.add(Not((s[0] ^ s[19]) <= 95))
v8 = s[0] >> 5
solver.add(Not((s[0] >> 5) > 12))
v8 = LOBYTE_off_606020_0 ^ s[13]
solver.add(Not((LOBYTE_off_606020_0 ^ s[13]) <= 29))
v8 = s[16] | s[7]
solver.add(Not((s[16] | s[7]) <= 121))
v8 = s[7] ^ s[17]
solver.add(Not((s[7] ^ s[17]) > 42))
v8 = ~s[19]
solver.add(Not(~s[19] > 1))
v8 = s[15] & s[3]
solver.add(Not((s[15] & s[3]) <= 61))
v8 = s[19] ^ s[15]
solver.add(Not((s[19] ^ s[15]) > 94))
v8 = s[0] ^ s[1]
solver.add(Not((s[0] ^ s[1]) > 125))
v8 = s[18] & s[1]
solver.add(Not((s[18] & s[1]) <= 0))
v8 = (s[16] ^ s[5]) & s[1]
solver.add(Not(v8 > 66))
v8 = ~s[14]
solver.add(Not(~s[14] > 1))
v8 = s[0] >> 5
solver.add(Not((s[0] >> 5) <= 0))
v8 = BYTE1_off_606028_0 ^ s[17]
solver.add(Not(v8 <= 46))
v8 = ~s[19]
solver.add(Not(~s[19] > 1))
v8 = s[4] ^ s[19]
solver.add(Not((s[4] ^ s[19]) > 106))
v8 = s[8] & s[7]
solver.add(Not((s[8] & s[7]) <= 33))
v8 = s[6] | s[7]
solver.add(Not((s[6] | s[7]) <= 118))
v8 = s[18] & s[1]
solver.add(Not((s[18] & s[1]) > 58))
v8 = s[2] ^ s[8]
solver.add(Not((s[2] ^ s[8]) <= 42))
v8 = s[2] ^ s[13]
solver.add(Not((s[2] ^ s[13]) <= 46))
v8 = s[3] & s[8]
solver.add(Not((s[3] & s[8]) <= 94))
v8 = s[16] ^ s[18]
solver.add(Not((s[16] ^ s[18]) <= 66))
v8 = BYTE2_off_606020_0 ^ s[15]
solver.add(Not(v8 <= 35))
v8 = s[10] ^ s[9]
solver.add(Not((s[10] ^ s[9]) <= 23))
v8 = s[18] & s[1]
solver.add(Not((s[18] & s[1]) <= 17))
v8 = s[0] & s[1]
solver.add(Not((s[0] & s[1]) > 90))
v8 = s[16] ^ s[1]
solver.add(Not((s[16] ^ s[1]) > 63))
v8 = s[18] & s[1]
solver.add(Not((s[18] & s[1]) > 102))
v8 = s[18] & s[3]
solver.add(Not((s[18] & s[3]) <= 49))
v8 = s[9] ^ s[1]
solver.add(Not((s[9] ^ s[1]) > 26))
v8 = off_606038 ^ s[15]
solver.add(Not((off_606038 ^ s[15]) > 40))
v8 = s[0] ^ s[1]
solver.add(Not((s[0] ^ s[1]) > 55))
v8 = s[13] & s[1]
solver.add(Not((s[13] & s[1]) > 103))
v8 = s[18] & s[1]
solver.add(Not((s[18] & s[1]) <= 0))
v8 = s[0] ^ s[1]
solver.add(Not((s[0] ^ s[1]) <= 34))
v8 = s[0] & s[1]
solver.add(Not((s[0] & s[1]) > 90))
v8 = s[11] ^ s[14]
solver.add(Not((s[11] ^ s[14]) > 4))
v8 = s[5] ^ s[11]
solver.add(Not((s[5] ^ s[11]) > 50))
v8 = s[18] & s[1]
solver.add(Not((s[18] & s[1]) <= 37))
v8 = s[0] ^ s[6]
solver.add(Not((s[0] ^ s[6]) > 48))
v8 = s[2] << 6
solver.add(Not((s[2] << 6) > 1))
v8 = s[0] | s[1]
solver.add(Not((s[0] | s[1]) <= 85))
v8 = s[9] ^ s[10]
solver.add(Not((s[9] ^ s[10]) <= 66))
v8 = s[10] & s[8]
solver.add(Not((s[10] & s[8]) <= 30))
v8 = s[19] ^ s[17]
solver.add(Not((s[19] ^ s[17]) > 118))
v8 = s[0] & s[17] | s[8]
solver.add(Not(v8 <= 59))
v8 = s[17] ^ s[18]
solver.add(Not((s[17] ^ s[18]) <= 94))
v8 = s[18] & s[9]
solver.add(Not((s[18] & s[9]) <= 30))
v8 = s[3] ^ s[6]
solver.add(Not((s[3] ^ s[6]) > 32))
v8 = 16 * s[16]
solver.add(Not((16 * s[16]) > 1))
v8 = s[7] ^ s[3] | s[17]
solver.add(Not(v8 <= 94))
v8 = s[0] | s[1]
solver.add(Not((s[0] | s[1]) > 120))
v8 = s[10] & s[18]
solver.add(Not((s[10] & s[18]) > 81))
v8 = s[6] | s[7]
solver.add(Not((s[6] | s[7]) > 119))
v8 = s[0] ^ s[6]
solver.add(Not((s[0] ^ s[6]) <= 16))
v8 = 2 * s[12]
solver.add(Not((2 * s[12]) > 1))
v8 = s[0] | s[1]
solver.add(Not((s[0] | s[1]) <= 66))
v8 = s[6] & s[1]
solver.add(Not((s[6] & s[1]) <= 84))
v8 = s[18] & s[1]
solver.add(Not((s[18] & s[1]) > 118))
v8 = s[0] ^ s[6]
solver.add(Not((s[0] ^ s[6]) > 47))
v8 = s[0] | s[1]
solver.add(Not((s[0] | s[1]) <= 60))
v8 = s[18] & s[1]
solver.add(Not((s[18] & s[1]) <= 13))
v8 = s[0] ^ s[6]
solver.add(Not((s[0] ^ s[6]) <= 38))
v8 = s[13] ^ s[10]
solver.add(Not((s[13] ^ s[10]) > 67))
v8 = 16 * s[2]
solver.add(Not((16 * s[2]) > 1))
v8 = s[0] | s[1]
solver.add(Not((s[0] | s[1]) <= 94))
v8 = s[0] & s[11]
solver.add(Not((s[0] & s[11]) > 67))
v8 = s[18] & s[1]
solver.add(Not((s[18] & s[1]) > 48))
v8 = s[0] ^ s[6]
solver.add(Not((s[0] ^ s[6]) > 102))
v8 = s[0] ^ s[19]
solver.add(Not((s[0] ^ s[19]) > 96))
v8 = s[14] ^ s[18] | s[3]
solver.add(Not(v8 != 127))
v8 = 4 * s[14]
solver.add(Not((4 * s[14]) > 1))
v8 = BYTE3_off_606038 ^ s[11]
solver.add(Not(v8 > 97))
v8 = s[6] | s[1]
solver.add(Not((s[6] | s[1]) <= 43))
v8 = s[5] & s[1]
solver.add(Not((s[5] & s[1]) > 95))
v8 = (s[14] ^ s[3]) & s[10]
solver.add(Not(v8 <= 2))
v8 = s[18] & s[1]
solver.add(Not((s[18] & s[1]) > 65))
v8 = s[0] ^ s[6]
solver.add(Not((s[0] ^ s[6]) <= 24))
v8 = ~s[6]
solver.add(Not(~s[6] > 1))
v8 = s[9] ^ s[10]
solver.add(Not((s[9] ^ s[10]) > 67))
v8 = 2 * s[7]
solver.add(Not((2 * s[7]) > 1))
v8 = s[9] & s[17]
solver.add(Not((s[9] & s[17]) > 101))
v8 = s[16] & s[15] | s[18]
solver.add(Not(v8 <= 121))
v8 = s[0] ^ s[16]
solver.add(Not((s[0] ^ s[16]) <= 40))
v8 = s[18] & s[3]
solver.add(Not((s[18] & s[3]) > 50))
v8 = s[3] << 6
solver.add(Not((s[3] << 6) > 1))
v8 = s[0] | s[1]
solver.add(Not((s[0] | s[1]) <= 12))
v8 = ~s[14]
solver.add(Not(~s[14] > 1))
v8 = s[0] >> 5
solver.add(Not((s[0] >> 5) > 79))
v8 = ~s[19]
solver.add(Not(~s[19] > 1))
v8 = s[0] ^ s[6]
solver.add(Not((s[0] ^ s[6]) > 44))
v8 = s[9] & s[5] | s[0]
solver.add(Not(v8 <= 28))
v8 = s[0] | s[1]
solver.add(Not((s[0] | s[1]) <= 93))
v8 = s[12] | s[4]
solver.add(Not((s[12] | s[4]) <= 40))
v8 = ~s[14]
solver.add(Not(~s[14] > 1))
v8 = s[0] >> 5
solver.add(Not((s[0] >> 5) <= 0))
v8 = ~s[19]
solver.add(Not(~s[19] > 1))
v8 = ~s[14]
solver.add(Not(~s[14] > 1))
v8 = s[1] ^ s[9]
solver.add(Not((s[1] ^ s[9]) > 8))
v8 = ~s[19]
solver.add(Not(~s[19] > 1))
v8 = s[11] ^ s[14]
solver.add(Not((s[11] ^ s[14]) <= 3))
v8 = s[11] | s[9]
solver.add(Not((s[11] | s[9]) <= 102))
v8 = s[12] ^ s[15]
solver.add(Not((s[12] ^ s[15]) > 68))
v8 = s[0] & s[2]
solver.add(Not((s[0] & s[2]) > 73))
v8 = s[13] & s[1]
solver.add(Not((s[13] & s[1]) <= 68))
v8 = 16 * s[7]
solver.add(Not((16 * s[7]) > 125))
v8 = s[13] ^ s[5]
solver.add(Not((s[13] ^ s[5]) > 79))
v8 = s[12] ^ s[14]
solver.add(Not((s[12] ^ s[14]) > 6))
v8 = s[9] & s[4]
solver.add(Not((s[9] & s[4]) <= 16))
v8 = ~s[6]
solver.add(Not(~s[6] > 1))
v8 = ~s[14]
solver.add(Not(~s[14] > 1))
v8 = s[0] >> 5
solver.add(Not((s[0] >> 5) > 74))
v8 = ~s[19]
solver.add(Not(~s[19] > 1))
v8 = s[11] | s[9]
solver.add(Not((s[11] | s[9]) <= 89))
v8 = s[12] ^ s[15]
solver.add(Not((s[12] ^ s[15]) > 46))
v8 = 16 * s[7]
solver.add(Not((16 * s[7]) <= 29))
v8 = s[19] | s[7]
solver.add(Not((s[19] | s[7]) <= 77))
v8 = s[4] ^ s[6]
solver.add(Not((s[4] ^ s[6]) > 12))
v8 = ~s[6]
solver.add(Not(~s[6] > 1))
v8 = ~s[14]
solver.add(Not(~s[14] > 1))
v8 = s[0] >> 5
solver.add(Not((s[0] >> 5) > 27))
v8 = ~s[19]
solver.add(Not(~s[19] > 1))
v8 = s[11] | s[9]
solver.add(Not((s[11] | s[9]) > 122))
v8 = s[12] ^ s[15]
solver.add(Not((s[12] ^ s[15]) <= 3))
v8 = s[13] & s[1]
solver.add(Not((s[13] & s[1]) <= 56))
v8 = 16 * s[7]
solver.add(Not((16 * s[7]) <= 3))
v8 = s[2] ^ s[8]
solver.add(Not((s[2] ^ s[8]) > 43))
v8 = s[13] ^ s[5]
solver.add(Not((s[13] ^ s[5]) <= 16))
v8 = ~s[6]
solver.add(Not(~s[6] > 1))
v8 = ~s[6]
solver.add(Not(~s[6] > 1))
v8 = ~s[14]
solver.add(Not(~s[14] > 1))
v8 = s[0] >> 5
solver.add(Not((s[0] >> 5) > 88))
v8 = ~s[19]
solver.add(Not(~s[19] > 33))
v8 = s[12] ^ s[15]
solver.add(Not((s[12] ^ s[15]) > 46))
v8 = ~s[5]
solver.add(Not(~s[5] > 1))
v8 = s[6] & s[7] | s[3]
solver.add(Not(v8 <= 9))
v8 = s[13] ^ s[5]
solver.add(Not((s[13] ^ s[5]) > 96))
v8 = ~s[6]
solver.add(Not(~s[6] > 1))
v8 = ~s[14]
solver.add(Not(~s[14] > 1))
v8 = s[0] >> 5
solver.add(Not((s[0] >> 5) > 91))
v8 = ~s[19]
solver.add(Not(~s[19] > 1))
v8 = s[11] | s[9]
solver.add(Not((s[11] | s[9]) <= 32))
v8 = s[9] & s[11]
solver.add(Not((s[9] & s[11]) <= 32))
v8 = ~s[6]
solver.add(Not(~s[6] > 1))
v8 = ~s[14]
solver.add(Not(~s[14] > 1))
v8 = ~s[19]
solver.add(Not(~s[19] > 1))
v8 = s[11] | s[9]
solver.add(Not((s[11] | s[9]) <= 90))
v8 = BYTE2_off_606038 ^ s[5]
solver.add(Not(v8 > 120))
v8 = s[12] ^ s[15]
solver.add(Not((s[12] ^ s[15]) > 32))
v8 = 16 * s[7]
solver.add(Not((16 * s[7]) <= 61))
v8 = s[13] ^ s[5]
solver.add(Not((s[13] ^ s[5]) <= 33))
v8 = s[0] >> 5
solver.add(Not((s[0] >> 5) > 16))
v8 = ~s[19]
solver.add(Not(~s[19] > 64))
v8 = s[11] | s[9]
solver.add(Not((s[11] | s[9]) <= 95))
v8 = s[12] ^ s[15]
solver.add(Not((s[12] ^ s[15]) > 48))
v8 = s[13] & s[1]
solver.add(Not((s[13] & s[1]) > 113))
v8 = s[7] ^ s[17]
solver.add(Not((s[7] ^ s[17]) <= 41))
v8 = 16 * s[7]
solver.add(Not((16 * s[7]) <= 63))
v8 = ~s[6]
solver.add(Not(~s[6] > 1))
v8 = s[4] & s[12]
solver.add(Not((s[4] & s[12]) <= 94))
v8 = s[2] ^ s[8]
solver.add(Not((s[2] ^ s[8]) > 43))
v8 = s[16] >> 1
solver.add(Not((s[16] >> 1) <= 57))
v8 = ~s[6]
solver.add(Not(~s[6] > 1))
v8 = s[4] & s[12]
solver.add(Not((s[4] & s[12]) > 103))
v8 = s[16] >> 1
solver.add(Not((s[16] >> 1) > 92))
v8 = BYTE1_off_606038 ^ s[4]
solver.add(Not(v8 > 57))
v8 = ~s[19]
solver.add(Not(~s[19] > 1))
v8 = s[19] & s[4] | s[2]
solver.add(Not(v8 <= 16))
v8 = s[11] | s[9]
solver.add(Not((s[11] | s[9]) <= 20))
v8 = s[12] ^ s[15]
solver.add(Not((s[12] ^ s[15]) > 82))
v8 = s[13] | s[15]
solver.add(Not((s[13] | s[15]) > 117))
v8 = s[13] & s[1]
solver.add(Not((s[13] & s[1]) <= 50))
v8 = s[19] ^ s[5]
solver.add(Not((s[19] ^ s[5]) > 118))
v8 = s[13] ^ s[5]
solver.add(Not((s[13] ^ s[5]) == 127))
v8 = ~s[6]
solver.add(Not(~s[6] > 1))
v8 = s[4] & s[12]
solver.add(Not((s[4] & s[12]) <= 67))
v8 = s[5] & s[17]
solver.add(Not((s[5] & s[17]) <= 56))
v8 = s[16] >> 1
solver.add(Not((s[16] >> 1) > 95))
v8 = ~s[6]
solver.add(Not(~s[6] > 1))
v8 = s[7] ^ s[3] | s[17]
solver.add(Not(v8 > 95))
v8 = s[4] & s[12]
solver.add(Not((s[4] & s[12]) <= 78))
v8 = s[16] >> 1
solver.add(Not((s[16] >> 1) <= 7))
v8 = s[0] >> 5
solver.add(Not((s[0] >> 5) > 123))
v8 = ~s[19]
solver.add(Not(~s[19] > 1))
v8 = s[11] | s[9]
solver.add(Not((s[11] | s[9]) <= 101))
v8 = s[13] & s[1]
solver.add(Not((s[13] & s[1]) <= 61))
v8 = 16 * s[7]
solver.add(Not((16 * s[7]) <= 73))
v8 = s[13] ^ s[5]
solver.add(Not((s[13] ^ s[5]) <= 34))
v8 = ~s[6]
solver.add(Not(~s[6] > 1))
v8 = s[4] & s[12]
solver.add(Not((s[4] & s[12]) <= 5))
v8 = ~s[6]
solver.add(Not(~s[6] > 85))
v8 = s[4] & s[12]
solver.add(Not((s[4] & s[12]) > 113))
v8 = s[16] >> 1
solver.add(Not((s[16] >> 1) > 61))
v8 = s[16] >> 1
solver.add(Not((s[16] >> 1) > 90))
v8 = s[0] >> 5
solver.add(Not((s[0] >> 5) > 106))
v8 = ~s[19]
solver.add(Not(~s[19] > 1))
v8 = s[0] ^ s[1]
solver.add(Not((s[0] ^ s[1]) > 84))
v8 = s[0] & s[1]
solver.add(Not((s[0] & s[1]) > 81))
v8 = ~s[14]
solver.add(Not(~s[14] > 1))
v8 = s[0] >> 5
solver.add(Not((s[0] >> 5) > 49))
v8 = ~s[19]
solver.add(Not(~s[19] > 1))
v8 = s[0] ^ s[1]
solver.add(Not((s[0] ^ s[1]) > 66))
v8 = s[0] & s[1]
solver.add(Not((s[0] & s[1]) > 81))
v8 = s[18] & s[1]
solver.add(Not((s[18] & s[1]) > 41))
v8 = s[0] ^ s[1]
solver.add(Not((s[0] ^ s[1]) > 82))
v8 = s[17] & s[3]
solver.add(Not((s[17] & s[3]) > 84))
v8 = s[0] & s[1]
solver.add(Not((s[0] & s[1]) <= 34))
v8 = s[18] & s[1]
solver.add(Not((s[18] & s[1]) > 66))
v8 = s[0] & s[1]
solver.add(Not((s[0] & s[1]) > 90))
v8 = s[18] & s[4]
solver.add(Not((s[18] & s[4]) > 73))
v8 = s[18] & s[1]
solver.add(Not((s[18] & s[1]) <= 12))
v8 = s[0] ^ s[1]
solver.add(Not((s[0] ^ s[1]) <= 9))
v8 = s[2] ^ s[8]
solver.add(Not((s[2] ^ s[8]) <= 42))
v8 = s[13] ^ s[0]
solver.add(Not((s[13] ^ s[0]) > 44))
v8 = s[0] & s[1]
solver.add(Not((s[0] & s[1]) <= 14))
v8 = s[0] & s[1]
solver.add(Not((s[0] & s[1]) <= 16))
v8 = s[18] & s[1]
solver.add(Not((s[18] & s[1]) > 74))
v8 = s[0] ^ s[6]
solver.add(Not((s[0] ^ s[6]) > 102))
v8 = 4 * s[2]
solver.add(Not((4 * s[2]) <= 16))
v8 = s[0] | s[1]
solver.add(Not((s[0] | s[1]) <= 87))
v8 = s[1] ^ s[11]
solver.add(Not((s[1] ^ s[11]) > 29))
v8 = s[18] & s[1]
solver.add(Not((s[18] & s[1]) > 51))
v8 = s[0] ^ s[6]
solver.add(Not((s[0] ^ s[6]) > 74))
v8 = 4 * s[2]
solver.add(Not((4 * s[2]) <= 103))
v8 = s[0] | s[1]
solver.add(Not((s[0] | s[1]) <= 56))
v8 = s[4] ^ s[6]
solver.add(Not((s[4] ^ s[6]) <= 11))
v8 = s[0] & s[1]
solver.add(Not((s[0] & s[1]) <= 16))
v8 = s[18] & s[1]
solver.add(Not((s[18] & s[1]) <= 22))
v8 = s[16] & s[15] | s[18]
solver.add(Not(v8 > 122))
v8 = s[0] ^ s[6]
solver.add(Not((s[0] ^ s[6]) > 74))
v8 = 4 * s[2]
solver.add(Not((4 * s[2]) <= 16))
v8 = s[16] ^ s[18]
solver.add(Not((s[16] ^ s[18]) > 67))
v8 = s[0] & s[1]
solver.add(Not((s[0] & s[1]) > 102))
v8 = s[0] ^ s[6]
solver.add(Not((s[0] ^ s[6]) > 74))
v8 = s[9] | s[13]
solver.add(Not((s[9] | s[13]) <= 27))
v8 = 4 * s[2]
solver.add(Not((4 * s[2]) <= 58))
v8 = 4 * s[2]
solver.add(Not((4 * s[2]) <= 77))
v8 = s[0] | s[1]
solver.add(Not((s[0] | s[1]) <= 3))
v8 = s[0] & s[1]
solver.add(Not((s[0] & s[1]) <= 13))
v8 = s[0] ^ s[6]
solver.add(Not((s[0] ^ s[6]) > 47))
v8 = s[7] & s[4]
solver.add(Not((s[7] & s[4]) <= 39))
v8 = s[16] | s[7]
solver.add(Not((s[16] | s[7]) == 127))
v8 = s[0] | s[1]
solver.add(Not((s[0] | s[1]) <= 66))
v8 = s[0] & s[1]
solver.add(Not((s[0] & s[1]) <= 47))
v8 = s[18] & s[1]
solver.add(Not((s[18] & s[1]) > 63))
v8 = s[13] & s[3]
solver.add(Not((s[13] & s[3]) > 122))
v8 = 4 * s[2]
solver.add(Not((4 * s[2]) <= 65))
v8 = s[0] & s[1]
solver.add(Not((s[0] & s[1]) > 120))
v8 = 4 * s[2]
solver.add(Not((4 * s[2]) <= 83))
v8 = s[0] | s[1]
solver.add(Not((s[0] | s[1]) <= 99))
v8 = ~s[14]
solver.add(Not(~s[14] > 1))
v8 = s[0] >> 5
solver.add(Not((s[0] >> 5) > 42))
v8 = ~s[19]
solver.add(Not(~s[19] > 1))
v8 = s[0] ^ s[6]
solver.add(Not((s[0] ^ s[6]) > 110))
v8 = 4 * s[2]
solver.add(Not((4 * s[2]) <= 92))
v8 = s[0] | s[1]
solver.add(Not((s[0] | s[1]) <= 59))
v8 = s[8] | s[0]
solver.add(Not((s[8] | s[0]) <= 1))
v8 = ~s[14]
solver.add(Not(~s[14] > 1))
v8 = ~s[19]
solver.add(Not(~s[19] > 1))
v8 = ~s[14]
solver.add(Not(~s[14] > 17))
v8 = ~s[19]
solver.add(Not(~s[19] > 1))
v8 = s[11] | s[9]
solver.add(Not((s[11] | s[9]) <= 78))
v8 = s[12] ^ s[15]
solver.add(Not((s[12] ^ s[15]) > 47))
v8 = s[13] & s[1]
solver.add(Not((s[13] & s[1]) <= 90))
v8 = 16 * s[7]
solver.add(Not((16 * s[7]) <= 78))
v8 = s[13] ^ s[5]
solver.add(Not((s[13] ^ s[5]) <= 30))
v8 = ~s[6]
solver.add(Not(~s[6] > 1))
v8 = ~s[14]
solver.add(Not(~s[14] > 1))
v8 = ~s[19]
solver.add(Not(~s[19] > 1))
v8 = s[11] | s[9]
solver.add(Not((s[11] | s[9]) <= 17))
v8 = s[12] ^ s[15]
solver.add(Not((s[12] ^ s[15]) > 86))
v8 = s[12] & s[4]
solver.add(Not((s[12] & s[4]) > 120))
v8 = 16 * s[7]
solver.add(Not((16 * s[7]) <= 46))
v8 = s[13] ^ s[5]
solver.add(Not((s[13] ^ s[5]) > 63))
v8 = s[12] ^ s[14]
solver.add(Not((s[12] ^ s[14]) <= 5))
v8 = ~s[6]
solver.add(Not(~s[6] > 17))
v8 = ~s[14]
solver.add(Not(~s[14] > 113))
v8 = ~s[19]
solver.add(Not(~s[19] > 1))
v8 = s[11] | s[9]
solver.add(Not((s[11] | s[9]) <= 73))
v8 = s[12] ^ s[15]
solver.add(Not((s[12] ^ s[15]) > 60))
v8 = s[13] & s[1]
solver.add(Not((s[13] & s[1]) > 119))
v8 = ~s[6]
solver.add(Not(~s[6] > 21))
v8 = ~s[19]
solver.add(Not(~s[19] > 107))
v8 = s[12] ^ s[15]
solver.add(Not((s[12] ^ s[15]) > 44))
v8 = s[13] & s[1]
solver.add(Not((s[13] & s[1]) <= 57))
v8 = s[13] ^ s[5]
solver.add(Not((s[13] ^ s[5]) > 59))
v8 = ~s[6]
solver.add(Not(~s[6] > 1))
v8 = ~s[14]
solver.add(Not(~s[14] > 1))
v8 = s[0] >> 5
solver.add(Not((s[0] >> 5) > 58))
v8 = ~s[9]
solver.add(Not(~s[9] > 1))
v8 = s[11] | s[9]
solver.add(Not((s[11] | s[9]) <= 101))
v8 = s[13] & s[1]
solver.add(Not((s[13] & s[1]) <= 99))
v8 = 16 * s[7]
solver.add(Not((16 * s[7]) <= 78))
v8 = s[13] ^ s[4]
solver.add(Not((s[13] ^ s[4]) > 16))
v8 = ~s[16]
solver.add(Not(~s[16] > 10))
v8 = ~s[4]
solver.add(Not(~s[4] > 1))
v8 = s[0] >> 5
solver.add(Not((s[0] >> 5) > 3))
v8 = ~s[19]
solver.add(Not(~s[19] > 1))
v8 = s[11] | s[9]
solver.add(Not((s[11] | s[9]) > 118))
v8 = s[12] ^ s[15]
solver.add(Not((s[12] ^ s[15]) <= 1))
v8 = 16 * s[7]
solver.add(Not((16 * s[7]) <= 0))
v8 = s[13] ^ s[5]
solver.add(Not((s[13] ^ s[5]) > 101))
v8 = s[0] >> 5
solver.add(Not((s[0] >> 5) > 18))
v8 = ~s[19]
solver.add(Not(~s[19] > 1))
v8 = s[11] | s[9]
solver.add(Not((s[11] | s[9]) <= 0))
v8 = s[12] ^ s[15]
solver.add(Not((s[12] ^ s[15]) > 67))
v8 = s[13] & s[1]
solver.add(Not((s[13] & s[1]) > 103))
v8 = 16 * s[4]
solver.add(Not((16 * s[4]) > 1))
v8 = s[13] ^ s[5]
solver.add(Not((s[13] ^ s[5]) <= 38))
v8 = ~s[6]
solver.add(Not(~s[6] > 1))
v8 = s[4] & s[12]
solver.add(Not((s[4] & s[12]) <= 94))
v8 = s[16] >> 1
solver.add(Not((s[16] >> 1) > 63))
v8 = ~s[6]
solver.add(Not(~s[6] > 1))
v8 = s[16] >> 1
solver.add(Not((s[16] >> 1) <= 47))
v8 = s[0] >> 5
solver.add(Not((s[0] >> 5) <= 0))
v8 = ~s[19]
solver.add(Not(~s[19] > 1))
v8 = s[11] | s[9]
solver.add(Not((s[11] | s[9]) > 118))
v8 = s[12] ^ s[15]
solver.add(Not((s[12] ^ s[15]) > 58))
v8 = s[13] & s[1]
solver.add(Not((s[13] & s[1]) <= 91))
v8 = 16 * s[7]
solver.add(Not((16 * s[7]) <= 72))
v8 = s[13] ^ s[5]
solver.add(Not((s[13] ^ s[5]) > 63))
v8 = ~s[6]
solver.add(Not(~s[6] > 1))
v8 = s[4] & s[12]
solver.add(Not((s[4] & s[12]) <= 94))
v8 = s[16] >> 1
solver.add(Not((s[16] >> 1) <= 57))
v8 = ~s[6]
solver.add(Not(~s[6] > 1))
v8 = s[4] & s[12]
solver.add(Not((s[4] & s[12]) > 99))
v8 = s[16] >> 1
solver.add(Not((s[16] >> 1) > 63))
v8 = s[0] >> 5
solver.add(Not((s[0] >> 5) > 81))
v8 = ~s[19]
solver.add(Not(~s[19] > 1))
v8 = s[11] | s[9]
solver.add(Not((s[11] | s[9]) > 118))
v8 = s[8] ^ s[15]
solver.add(Not((s[8] ^ s[15]) > 1))
v8 = s[7] & s[1]
solver.add(Not((s[7] & s[1]) <= 72))
v8 = 16 * s[17]
solver.add(Not((16 * s[17]) > 1))
v8 = s[3] ^ s[5]
solver.add(Not((s[3] ^ s[5]) > 110))
v8 = ~s[6]
solver.add(Not(~s[6] > 1))
v8 = s[4] & s[12]
solver.add(Not((s[4] & s[12]) <= 68))
v8 = s[16] >> 1
solver.add(Not((s[16] >> 1) > 91))
v8 = ~s[6]
solver.add(Not(~s[6] > 1))
v8 = s[4] & s[12]
solver.add(Not((s[4] & s[12]) > 99))
v8 = s[16] >> 1
solver.add(Not((s[16] >> 1) <= 40))
v8 = s[16] >> 1
solver.add(Not((s[16] >> 1) <= 31))
v8 = ~s[14]
solver.add(Not(~s[14] > 1))
v8 = s[0] >> 5
solver.add(Not((s[0] >> 5) > 96))
v8 = ~s[19]
solver.add(Not(~s[19] > 1))
v8 = s[3] ^ s[1]
solver.add(Not((s[3] ^ s[1]) > 42))
v8 = s[4] & s[1]
solver.add(Not((s[4] & s[1]) > 118))
v8 = s[16] >> 1
solver.add(Not((s[16] >> 1) > 94))
v8 = ~s[14]
solver.add(Not(~s[14] > 1))
v8 = ~s[19]
solver.add(Not(~s[19] > 1))
v8 = s[0] ^ s[1]
solver.add(Not((s[0] ^ s[1]) > 64))
v8 = s[0] & s[1]
solver.add(Not((s[0] & s[1]) > 110))
v8 = 4 * s[2]
solver.add(Not((4 * s[2]) <= 104))
v8 = s[0] | s[1]
solver.add(Not((s[0] | s[1]) > 112))
v8 = s[0] & s[1]
solver.add(Not((s[0] & s[1]) <= 62))
v8 = s[18] & s[1]
solver.add(Not((s[18] & s[1]) > 48))
v8 = s[0] ^ s[6]
solver.add(Not((s[0] ^ s[6]) > 58))
v8 = 4 * s[2]
solver.add(Not((4 * s[2]) <= 104))
v8 = s[8] | s[1]
solver.add(Not((s[8] | s[1]) <= 50))
v8 = s[5] & s[1]
solver.add(Not((s[5] & s[1]) <= 38))
v8 = s[18] & s[1]
solver.add(Not((s[18] & s[1]) > 85))
v8 = s[0] ^ s[6]
solver.add(Not((s[0] ^ s[6]) <= 18))
v8 = 4 * s[2]
solver.add(Not((4 * s[2]) <= 97))
v8 = s[0] | s[1]
solver.add(Not((s[0] | s[1]) <= 94))
v8 = s[18] & s[1]
solver.add(Not((s[18] & s[1]) <= 26))
v8 = s[0] ^ s[6]
solver.add(Not((s[0] ^ s[6]) > 67))
v8 = 4 * s[2]
solver.add(Not((4 * s[2]) <= 103))
v8 = s[18] & s[1]
solver.add(Not((s[18] & s[1]) > 50))
v8 = s[0] ^ s[6]
solver.add(Not((s[0] ^ s[6]) <= 22))
v8 = 4 * s[2]
solver.add(Not((4 * s[2]) <= 103))
v8 = s[0] | s[1]
solver.add(Not((s[0] | s[1]) <= 38))
v8 = s[0] & s[1]
solver.add(Not((s[0] & s[1]) <= 52))
v8 = s[18] & s[1]
solver.add(Not((s[18] & s[1]) <= 17))
v8 = 4 * s[9]
solver.add(Not((4 * s[9]) > 1))
v8 = s[0] | s[1]
solver.add(Not((s[0] | s[1]) <= 92))
v8 = s[0] & s[1]
solver.add(Not((s[0] & s[1]) <= 55))
v8 = s[8] ^ s[6]
solver.add(Not((s[8] ^ s[6]) > 81))
v8 = 4 * s[12]
solver.add(Not((4 * s[12]) > 1))
v8 = s[0] | s[1]
solver.add(Not((s[0] | s[1]) <= 94))
v8 = ~s[12]
solver.add(Not(~s[12] > 1))
v8 = ~s[1]
solver.add(Not(~s[1] > 1))
v8 = s[0] ^ s[6]
solver.add(Not((s[0] ^ s[6]) > 101))
v8 = 4 * s[4]
solver.add(Not((4 * s[4]) > 1))
v8 = s[0] | s[1]
solver.add(Not((s[0] | s[1]) <= 44))
v8 = ~s[14]
solver.add(Not(~s[14] > 1))
v8 = ~s[14]
solver.add(Not(~s[14] > 1))
v8 = ~s[19]
solver.add(Not(~s[19] > 120))
assert solver.check() == sat
model = solver.model()
print ''.join(chr(model[c].as_long()) for c in s)
# Im_so_cute&pretty_:)
#!/usr/bin/python
# Math is hard!
import struct
import sys
import z3
def LODWORD(n):
return n & 0xffffffff
solver = z3.Solver()
table = [0x926d, 0x5475, 0x0752, 0xb4c1, 0xc5c9, 0xa89e, 0x7372, 0x4004, 0xe15d, 0x3922, 0x5262,
0x99ae, 0xd5e5, 0xc6f8, 0x12c9, 0x1783, 0x9832, 0x39ca, 0x5847, 0x0345, 0x8f77, 0xc5a0,
0x2e35, 0x4e4e, 0x2428, 0xcfec, 0x974a, 0xcecf, 0x41f2, 0x691b, 0xad9e, 0x48a9, 0xfec5,
0xb9b7, 0x4526, 0x8476, 0xa69e, 0x14fb, 0x2ccd, 0xe193, 0x5d51, 0x65a0, 0x6252, 0xd42d,
0x7e51, 0x2999, 0x87f5, 0x23d3, 0x5947, 0x21ad, 0x027a, 0x2e58, 0x36b5, 0x3fc3, 0xabbc,
0x876e, 0xd669, 0x17fd, 0x8a63, 0xf219, 0x6de6, 0xa8b2, 0xe91c, 0x3cda, 0xc3a2, 0x9f38,
0x55fe, 0x3528, 0x1352, 0x687e, 0x7bdc, 0x9ab3, 0x3522, 0xe6af, 0x7fe2, 0x729d, 0x2841,
0x3d22, 0xb98b, 0xe200, 0x34a5, 0x27eb, 0x13a8, 0x522f, 0x73a7, 0xd7c9, 0x17b1, 0x3eaf,
0x11ca, 0x08d6, 0x49d7, 0xff8b, 0x4317, 0x24c2, 0x57f2, 0xcc99, 0x2413, 0xd03d, 0xbb25,
0xe6e7, 0xa149, 0x5f66, 0xa0da, 0x5b97, 0x070d, 0x1027, 0x4204, 0x8265, 0xb6af, 0xe4b7,
0x8546, 0xaf78, 0x2e9d, 0x5032, 0x3d53, 0x8ef5, 0x4737, 0xa7bd, 0xee80, 0xb071, 0xa144,
0x06ba, 0x6737, 0xb7cc, 0xa57b, 0x3ab9, 0x4a1f, 0x2a24, 0x8227, 0xf8c0, 0x90dd, 0xc986,
0x4586, 0x278f, 0xcca4, 0x31ca, 0x312b, 0xe5a2, 0x204d, 0x5855, 0x7821, 0x5175, 0x7dd8,
0x8f2a, 0xb9ce, 0x8202, 0xe72c, 0xfeac, 0x240c, 0xe8cf, 0xf5a8, 0xbe4f, 0xb8f4, 0x92d8,
0xe10c, 0x9e3e, 0xca17, 0x8c27, 0xf992, 0x1006, 0xe877, 0x538a, 0x5121, 0x6795, 0x6df9,
0x62a4, 0xab0d, 0x6421, 0x1c92]
func = [
lambda inp: LODWORD(LODWORD(LODWORD((inp[0x30/4])) * LODWORD(table[(0x2b0-0x280)/4])) + LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(table[(0x2b0-0x2B0)/4]) * LODWORD(inp[0])) - LODWORD(LODWORD((inp[0x4/4])) * LODWORD(table[(0x2b0-0x2AC)/4]))) - LODWORD(LODWORD((inp[0x8/4])) * LODWORD(table[(0x2b0-0x2A8)/4]))) - LODWORD(LODWORD((inp[0xc/4])) * LODWORD(table[(0x2b0-0x2A4)/4]))) + LODWORD(LODWORD((inp[0x10/4])) * LODWORD(table[(0x2b0-0x2A0)/4]))) + LODWORD(LODWORD((inp[0x14/4])) * LODWORD(table[(0x2b0-0x29C)/4]))) + LODWORD(LODWORD((inp[0x18/4])) * LODWORD(table[(0x2b0-0x298)/4]))) + LODWORD(LODWORD((inp[0x1c/4])) * LODWORD(table[(0x2b0-0x294)/4]))) + LODWORD(LODWORD((inp[0x20/4])) * LODWORD(table[(0x2b0-0x290)/4]))) + LODWORD(LODWORD((inp[0x24/4])) * LODWORD(table[(0x2b0-0x28C)/4]))) + LODWORD(LODWORD((inp[0x28/4])) * LODWORD(table[(0x2b0-0x288)/4]))) + LODWORD(LODWORD((inp[0x2c/4])) * LODWORD(table[(0x2b0-0x284)/4])))),
lambda inp: LODWORD(LODWORD(LODWORD((inp[0x30/4])) * LODWORD(table[(0x2b0-0x24C)/4])) + LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(table[(0x2b0-0x27C)/4]) * LODWORD(inp[0]) + LODWORD((inp[0x4/4])) * LODWORD(table[(0x2b0-0x278)/4])) - LODWORD(LODWORD((inp[0x8/4])) * LODWORD(table[(0x2b0-0x274)/4]))) + LODWORD(LODWORD((inp[0xc/4])) * LODWORD(table[(0x2b0-0x270)/4]))) + LODWORD(LODWORD((inp[0x10/4])) * LODWORD(table[(0x2b0-0x26C)/4]))) + LODWORD(LODWORD((inp[0x14/4])) * LODWORD(table[(0x2b0-0x268)/4]))) - LODWORD(LODWORD((inp[0x18/4])) * LODWORD(table[(0x2b0-0x264)/4]))) - LODWORD(LODWORD((inp[0x1c/4])) * LODWORD(table[(0x2b0-0x260)/4]))) - LODWORD(LODWORD((inp[0x20/4])) * LODWORD(table[(0x2b0-0x25C)/4]))) - LODWORD(LODWORD((inp[0x24/4])) * LODWORD(table[(0x2b0-0x258)/4]))) - LODWORD(LODWORD((inp[0x28/4])) * LODWORD(table[(0x2b0-0x254)/4]))) - LODWORD(LODWORD((inp[0x2c/4])) * LODWORD(table[(0x2b0-0x250)/4])))),
lambda inp: LODWORD(LODWORD(LODWORD((inp[0x30/4])) * LODWORD(table[(0x2b0-0x218)/4])) + LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(-LODWORD(table[(0x2b0-0x248)/4])) * LODWORD(inp[0]) + LODWORD((inp[0x4/4])) * LODWORD(table[(0x2b0-0x244)/4])) - LODWORD(LODWORD((inp[0x8/4])) * LODWORD(table[(0x2b0-0x240)/4]))) + LODWORD(LODWORD((inp[0xc/4])) * LODWORD(table[(0x2b0-0x23C)/4]))) - LODWORD(LODWORD((inp[0x10/4])) * LODWORD(table[(0x2b0-0x238)/4]))) - LODWORD(LODWORD((inp[0x14/4])) * LODWORD(table[(0x2b0-0x234)/4]))) - LODWORD(LODWORD((inp[0x18/4])) * LODWORD(table[(0x2b0-0x230)/4]))) - LODWORD(LODWORD((inp[0x1c/4])) * LODWORD(table[(0x2b0-0x22C)/4]))) + LODWORD(LODWORD((inp[0x20/4])) * LODWORD(table[(0x2b0-0x228)/4]))) - LODWORD(LODWORD((inp[0x24/4])) * LODWORD(table[(0x2b0-0x224)/4]))) + LODWORD(LODWORD((inp[0x28/4])) * LODWORD(table[(0x2b0-0x220)/4]))) + LODWORD(LODWORD((inp[0x2c/4])) * LODWORD(table[(0x2b0-0x21C)/4])))),
lambda inp: LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(table[(0x2b0-0x214)/4]) * LODWORD(inp[0])) - LODWORD(LODWORD((inp[0x4/4])) * LODWORD(table[(0x2b0-0x210)/4]))) - LODWORD(LODWORD((inp[0x8/4])) * LODWORD(table[(0x2b0-0x20C)/4]))) - LODWORD(LODWORD((inp[0xc/4])) * LODWORD(table[(0x2b0-0x208)/4]))) + LODWORD(LODWORD((inp[0x10/4])) * LODWORD(table[(0x2b0-0x204)/4]))) - LODWORD(LODWORD((inp[0x14/4])) * LODWORD(table[(0x2b0-0x200)/4]))) + LODWORD(LODWORD((inp[0x18/4])) * LODWORD(table[(0x2b0-0x1FC)/4]))) + LODWORD(LODWORD((inp[0x1c/4])) * LODWORD(table[(0x2b0-0x1F8)/4]))) - LODWORD(LODWORD((inp[0x20/4])) * LODWORD(table[(0x2b0-0x1F4)/4]))) - LODWORD(LODWORD((inp[0x24/4])) * LODWORD(table[(0x2b0-0x1F0)/4]))) + LODWORD(LODWORD((inp[0x28/4])) * LODWORD(table[(0x2b0-0x1EC)/4]))) - LODWORD(LODWORD((inp[0x2c/4])) * LODWORD(table[(0x2b0-0x1E8)/4]))) - LODWORD(LODWORD((inp[0x30/4])) * LODWORD(table[(0x2b0-0x1E4)/4]))),
lambda inp: LODWORD(LODWORD(LODWORD((inp[0x30/4])) * LODWORD(table[(0x2b0-0x1B0)/4])) + LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(-LODWORD(table[(0x2b0-0x1E0)/4])) * LODWORD(inp[0]) + LODWORD((inp[0x4/4])) * LODWORD(table[(0x2b0-0x1DC)/4])) + LODWORD(LODWORD((inp[0x8/4])) * LODWORD(table[(0x2b0-0x1D8)/4]))) + LODWORD(LODWORD((inp[0xc/4])) * LODWORD(table[(0x2b0-0x1D4)/4]))) + LODWORD(LODWORD((inp[0x10/4])) * LODWORD(table[(0x2b0-0x1D0)/4]))) - LODWORD(LODWORD((inp[0x14/4])) * LODWORD(table[(0x2b0-0x1CC)/4]))) - LODWORD(LODWORD((inp[0x18/4])) * LODWORD(table[(0x2b0-0x1C8)/4]))) - LODWORD(LODWORD((inp[0x1c/4])) * LODWORD(table[(0x2b0-0x1C4)/4]))) + LODWORD(LODWORD((inp[0x20/4])) * LODWORD(table[(0x2b0-0x1C0)/4]))) + LODWORD(LODWORD((inp[0x24/4])) * LODWORD(table[(0x2b0-0x1BC)/4]))) - LODWORD(LODWORD((inp[0x28/4])) * LODWORD(table[(0x2b0-0x1B8)/4]))) + LODWORD(LODWORD((inp[0x2c/4])) * LODWORD(table[(0x2b0-0x1B4)/4])))),
lambda inp: LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(-LODWORD(table[(0x2b0-0x1AC)/4])) * LODWORD(inp[0])) - LODWORD(LODWORD((inp[0x4/4])) * LODWORD(table[(0x2b0-0x1A8)/4]))) + LODWORD(LODWORD((inp[0x8/4])) * LODWORD(table[(0x2b0-0x1A4)/4]))) - LODWORD(LODWORD((inp[0xc/4])) * LODWORD(table[(0x2b0-0x1A0)/4]))) - LODWORD(LODWORD((inp[0x10/4])) * LODWORD(table[(0x2b0-0x19C)/4]))) - LODWORD(LODWORD((inp[0x14/4])) * LODWORD(table[(0x2b0-0x198)/4]))) + LODWORD(LODWORD((inp[0x18/4])) * LODWORD(table[(0x2b0-0x194)/4]))) + LODWORD(LODWORD((inp[0x1c/4])) * LODWORD(table[(0x2b0-0x190)/4]))) - LODWORD(LODWORD((inp[0x20/4])) * LODWORD(table[(0x2b0-0x18C)/4]))) - LODWORD(LODWORD((inp[0x24/4])) * LODWORD(table[(0x2b0-0x188)/4]))) + LODWORD(LODWORD((inp[0x28/4])) * LODWORD(table[(0x2b0-0x184)/4]))) + LODWORD(LODWORD((inp[0x2c/4])) * LODWORD(table[(0x2b0-0x180)/4]))) - LODWORD(LODWORD((inp[0x30/4])) * LODWORD(table[(0x2b0-0x17C)/4]))),
lambda inp: LODWORD(LODWORD(LODWORD((inp[0x30/4])) * LODWORD(table[(0x2b0-0x148)/4])) + LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(-LODWORD(table[(0x2b0-0x178)/4])) * LODWORD(inp[0]) + LODWORD((inp[0x4/4])) * LODWORD(table[(0x2b0-0x174)/4])) + LODWORD(LODWORD((inp[0x8/4])) * LODWORD(table[(0x2b0-0x170)/4]))) - LODWORD(LODWORD((inp[0xc/4])) * LODWORD(table[(0x2b0-0x16C)/4]))) - LODWORD(LODWORD((inp[0x10/4])) * LODWORD(table[(0x2b0-0x168)/4]))) - LODWORD(LODWORD((inp[0x14/4])) * LODWORD(table[(0x2b0-0x164)/4]))) - LODWORD(LODWORD((inp[0x18/4])) * LODWORD(table[(0x2b0-0x160)/4]))) + LODWORD(LODWORD((inp[0x1c/4])) * LODWORD(table[(0x2b0-0x15C)/4]))) - LODWORD(LODWORD((inp[0x20/4])) * LODWORD(table[(0x2b0-0x158)/4]))) + LODWORD(LODWORD((inp[0x24/4])) * LODWORD(table[(0x2b0-0x154)/4]))) - LODWORD(LODWORD((inp[0x28/4])) * LODWORD(table[(0x2b0-0x150)/4]))) - LODWORD(LODWORD((inp[0x2c/4])) * LODWORD(table[(0x2b0-0x14C)/4])))),
lambda inp: LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(-LODWORD(table[(0x2b0-0x144)/4])) * LODWORD(inp[0]) + LODWORD((inp[0x4/4])) * LODWORD(table[(0x2b0-0x140)/4])) - LODWORD(LODWORD((inp[0x8/4])) * LODWORD(table[(0x2b0-0x13C)/4]))) - LODWORD(LODWORD((inp[0xc/4])) * LODWORD(table[(0x2b0-0x138)/4]))) - LODWORD(LODWORD((inp[0x10/4])) * LODWORD(table[(0x2b0-0x134)/4]))) - LODWORD(LODWORD((inp[0x14/4])) * LODWORD(table[(0x2b0-0x130)/4]))) + LODWORD(LODWORD((inp[0x18/4])) * LODWORD(table[(0x2b0-0x12C)/4]))) + LODWORD(LODWORD((inp[0x1c/4])) * LODWORD(table[(0x2b0-0x128)/4]))) - LODWORD(LODWORD((inp[0x20/4])) * LODWORD(table[(0x2b0-0x124)/4]))) - LODWORD(LODWORD((inp[0x24/4])) * LODWORD(table[(0x2b0-0x120)/4]))) - LODWORD(LODWORD((inp[0x28/4])) * LODWORD(table[(0x2b0-0x11C)/4]))) + LODWORD(LODWORD((inp[0x2c/4])) * LODWORD(table[(0x2b0-0x118)/4]))) - LODWORD(LODWORD((inp[0x30/4])) * LODWORD(table[(0x2b0-0x114)/4]))),
lambda inp: LODWORD(LODWORD(LODWORD((inp[0x30/4])) * LODWORD(table[(0x2b0-0xE0)/4])) + LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(table[(0x2b0-0x110)/4]) * LODWORD(inp[0]) + LODWORD((inp[0x4/4])) * LODWORD(table[(0x2b0-0x10C)/4])) - LODWORD(LODWORD((inp[0x8/4])) * LODWORD(table[(0x2b0-0x108)/4]))) + LODWORD(LODWORD((inp[0xc/4])) * LODWORD(table[(0x2b0-0x104)/4]))) + LODWORD(LODWORD((inp[0x10/4])) * LODWORD(table[(0x2b0-0x100)/4]))) + LODWORD(LODWORD((inp[0x14/4])) * LODWORD(table[(0x2b0-0xFC)/4]))) - LODWORD(LODWORD((inp[0x18/4])) * LODWORD(table[(0x2b0-0xF8)/4]))) - LODWORD(LODWORD((inp[0x1c/4])) * LODWORD(table[(0x2b0-0xF4)/4]))) - LODWORD(LODWORD((inp[0x20/4])) * LODWORD(table[(0x2b0-0xF0)/4]))) - LODWORD(LODWORD((inp[0x24/4])) * LODWORD(table[(0x2b0-0xEC)/4]))) + LODWORD(LODWORD((inp[0x28/4])) * LODWORD(table[(0x2b0-0xE8)/4]))) - LODWORD(LODWORD((inp[0x2c/4])) * LODWORD(table[(0x2b0-0xE4)/4])))),
lambda inp: LODWORD(LODWORD(LODWORD((inp[0x30/4])) * LODWORD(table[(0x2b0-0xAC)/4])) + LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(-LODWORD(table[(0x2b0-0xDC)/4])) * LODWORD(inp[0]) + LODWORD((inp[0x4/4])) * LODWORD(table[(0x2b0-0xD8)/4])) - LODWORD(LODWORD((inp[0x8/4])) * LODWORD(table[(0x2b0-0xD4)/4]))) + LODWORD(LODWORD((inp[0xc/4])) * LODWORD(table[(0x2b0-0xD0)/4]))) - LODWORD(LODWORD((inp[0x10/4])) * LODWORD(table[(0x2b0-0xCC)/4]))) - LODWORD(LODWORD((inp[0x14/4])) * LODWORD(table[(0x2b0-0xC8)/4]))) + LODWORD(LODWORD((inp[0x18/4])) * LODWORD(table[(0x2b0-0xC4)/4]))) + LODWORD(LODWORD((inp[0x1c/4])) * LODWORD(table[(0x2b0-0xC0)/4]))) + LODWORD(LODWORD((inp[0x20/4])) * LODWORD(table[(0x2b0-0xBC)/4]))) + LODWORD(LODWORD((inp[0x24/4])) * LODWORD(table[(0x2b0-0xB8)/4]))) + LODWORD(LODWORD((inp[0x28/4])) * LODWORD(table[(0x2b0-0xB4)/4]))) - LODWORD(LODWORD((inp[0x2c/4])) * LODWORD(table[(0x2b0-0xB0)/4])))),
lambda inp: LODWORD(LODWORD(LODWORD((inp[0x30/4])) * LODWORD(table[(0x2b0-0x78)/4])) + LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(-LODWORD(table[(0x2b0-0xA8)/4])) * LODWORD(inp[0])) - LODWORD(LODWORD((inp[0x4/4])) * LODWORD(table[(0x2b0-0xA4)/4]))) - LODWORD(LODWORD((inp[0x8/4])) * LODWORD(table[(0x2b0-0xA0)/4]))) - LODWORD(LODWORD((inp[0xc/4])) * LODWORD(table[(0x2b0-0x9C)/4]))) - LODWORD(LODWORD((inp[0x10/4])) * LODWORD(table[(0x2b0-0x98)/4]))) + LODWORD(LODWORD((inp[0x14/4])) * LODWORD(table[(0x2b0-0x94)/4]))) + LODWORD(LODWORD((inp[0x18/4])) * LODWORD(table[(0x2b0-0x90)/4]))) + LODWORD(LODWORD((inp[0x1c/4])) * LODWORD(table[(0x2b0-0x8C)/4]))) - LODWORD(LODWORD((inp[0x20/4])) * LODWORD(table[(0x2b0-0x88)/4]))) + LODWORD(LODWORD((inp[0x24/4])) * LODWORD(table[(0x2b0-0x84)/4]))) + LODWORD(LODWORD((inp[0x28/4])) * LODWORD(table[(0x2b0-0x80)/4]))) - LODWORD(LODWORD((inp[0x2c/4])) * LODWORD(table[(0x2b0-0x7C)/4])))),
lambda inp: LODWORD(LODWORD(LODWORD((inp[0x30/4])) * LODWORD(table[(0x2b0-0x44)/4])) + LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(table[(0x2b0-0x74)/4]) * LODWORD(inp[0]) + LODWORD((inp[0x4/4])) * LODWORD(table[(0x2b0-0x70)/4])) - LODWORD(LODWORD((inp[0x8/4])) * LODWORD(table[(0x2b0-0x6C)/4]))) - LODWORD(LODWORD((inp[0xc/4])) * LODWORD(table[(0x2b0-0x68)/4]))) + LODWORD(LODWORD((inp[0x10/4])) * LODWORD(table[(0x2b0-0x64)/4]))) + LODWORD(LODWORD((inp[0x14/4])) * LODWORD(table[(0x2b0-0x60)/4]))) - LODWORD(LODWORD((inp[0x18/4])) * LODWORD(table[(0x2b0-0x5C)/4]))) - LODWORD(LODWORD((inp[0x1c/4])) * LODWORD(table[(0x2b0-0x58)/4]))) + LODWORD(LODWORD((inp[0x20/4])) * LODWORD(table[(0x2b0-0x54)/4]))) + LODWORD(LODWORD((inp[0x24/4])) * LODWORD(table[(0x2b0-0x50)/4]))) - LODWORD(LODWORD((inp[0x28/4])) * LODWORD(table[(0x2b0-0x4C)/4]))) + LODWORD(LODWORD((inp[0x2c/4])) * LODWORD(table[(0x2b0-0x48)/4])))),
lambda inp: LODWORD(LODWORD(LODWORD((inp[0x30/4])) * LODWORD(table[(0x2b0-0x10)/4])) + LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(LODWORD(table[(0x2b0-0x40)/4]) * LODWORD(inp[0]) + LODWORD((inp[0x4/4])) * LODWORD(table[(0x2b0-0x3C)/4])) - LODWORD(LODWORD((inp[0x8/4])) * LODWORD(table[(0x2b0-0x38)/4]))) + LODWORD(LODWORD((inp[0xc/4])) * LODWORD(table[(0x2b0-0x34)/4]))) + LODWORD(LODWORD((inp[0x10/4])) * LODWORD(table[(0x2b0-0x30)/4]))) - LODWORD(LODWORD((inp[0x14/4])) * LODWORD(table[(0x2b0-0x2C)/4]))) - LODWORD(LODWORD((inp[0x18/4])) * LODWORD(table[(0x2b0-0x28)/4]))) + LODWORD(LODWORD((inp[0x1c/4])) * LODWORD(table[(0x2b0-0x24)/4]))) + LODWORD(LODWORD((inp[0x20/4])) * LODWORD(table[(0x2b0-0x20)/4]))) + LODWORD(LODWORD((inp[0x24/4])) * LODWORD(table[(0x2b0-0x1C)/4]))) - LODWORD(LODWORD((inp[0x28/4])) * LODWORD(table[(0x2b0-0x18)/4]))) + LODWORD(LODWORD((inp[0x2c/4])) * LODWORD(table[(0x2b0-0x14)/4])))),
]
constraints = [
0x1468753,
0x162f30,
0xffb2939c,
0xffac90e3,
0x76d288,
0xff78bf99,
0xfff496e3,
0xff525e90,
0xfffd7704,
0x897cbb,
0xffc05f9f,
0x3e4761,
0x1b4945,
]
input_array = [z3.BitVec('i%d' % i, 32) for i in range(len(constraints))]
print input_array
for f, c in zip(func, constraints):
solver.add(f(input_array) == c)
assert solver.check() == z3.sat
print(solver.model())
from z3 import *
def transform_char(c):
return If(And(c > 64, c <= 70), c - 55, If(And(c > 47, c <= 57), c - 48, -1))
solver = Solver()
vars = [z3.BitVec("i{}".format(i), 64) for i in range(8)]
for v in vars:
solver.add(Or(And(48 <= v, v <= 57), And(65 <= v, v <= 70)))
res = BitVec("res", 64)
for v in vars:
res = res * 16
res = res | transform_char(v)
solver.add(res == 2502586916)
print solver.check()
m = solver.model()
print "The input string is:"
print "".join(chr(m[v].as_long()) for v in vars)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment