import
binascii
import
z3
z
=
z3.Solver()
right
=
binascii.unhexlify(
"612a725f7e736dda72df43ab72bf4de96bc965"
)
flag
=
[z3.BitVec(
"a%d"
%
_,
32
)
for
_
in
range
(
0x13
)]
buff
=
[]
temp
=
flag[
0
]
for
_
in
range
(
len
(flag)):
try
:
temp
=
temp
*
3
+
flag[_
+
1
]
except
IndexError:
temp
=
temp
*
3
temp
%
=
(
0x1000
+
1
)
temp &
=
0xFF
buff.append(flag[
0
] ^ temp ^
len
(flag))
temp1
=
temp
+
len
(flag)
for
_
in
range
(
1
,
len
(flag)):
buff.append(flag[_] ^ temp1 ^ buff[_
-
1
])
temp1
+
=
len
(flag)
-
_
temp1 &
=
0xFF
for
p, i
in
enumerate
(buff):
z.add(z3.simplify(i
=
=
right[p]))
if
z.check()
=
=
z3.sat:
for
i
in
flag:
print
(
chr
(z.model()[i].as_long()), end
=
"")