1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
| from z3 import *
s = Solver()
a = [BitVec(f"a{i:02}",16) for i in range(26)]
for i in range(26):
s.add(And(a[i]>=40, a[i]<=126))
s.add(a[0] + a[1] == 210 and a[1] | (a[0] == (a[1] | a[0])))
s.add(a[1] * a[2] == 10476)
s.add(a[1] + a[0] + a[2] == 307)
s.add(a[3] - a[2] == 6)
s.add(a[4] != If(a[5] == 15, BitVecVal(1, 16), BitVecVal(0, 16)))
s.add(a[7] * a[4] == 6273)
s.add((a[5] | If(a[11] == 119, BitVecVal(1, 16), BitVecVal(0, 16) )) != 0)
s.add(a[6] - a[17] == 53)
s.add(a[6] + a[5] + a[7] == 271)
s.add(a[8] - a[9] == 13)
s.add(a[8] + a[9] - a[10] == 125)
s.add(a[9] - a[11] == 31)
s.add(a[10] - a[11] == 1)
s.add(a[13] * a[12] == 10260)
s.add(a[13] + a[14] == 177)
s.add(And(If(a[17] == 69, a[16] != 1, a[16] != 0), ((a[17] | a[16]) & 1) != 0))
s.add(a[16] + a[18] == 219)
s.add(a[17] + a[16] + a[23] == 220)
s.add(a[14] - a[15] == 31)
s.add(a[14] + a[12] + a[15] == 241 and (a[14] ^ a[12]) != (a[12] == a[14]) )
s.add(a[17] - a[18] == -50)
s.add(a[19] + a[18] + a[20] == 316)
s.add(a[22] + a[21] + a[23] == 248)
s.add(a[22] - a[23] == 64)
s.add(a[24] + a[25] == 207)
s.add(a[24] - a[20] == -32)
s.add(a[25] - a[21] == 43)
s.add(a[0] + a[3] == 205)
s.add(a[13] + a[12] + a[14] == 285)
flag_list = []
result = set()
while s.check() == sat:
model = s.model()
flag = "".join([chr(model[a[i]].as_long()) for i in range(26)])
if flag not in result:
result.add(flag)
s.add(Or([a[i] != model[a[i]].as_long() for i in range(26)]))
for flag in result:
print(flag)
|