buu上的一道z3题，记录一下z3奇怪的用法。
首先扔进ida，打开主函数，非常混乱的算法，大概发现两个关键点：
这里应该是对flag进行异或得到v6
而这里的比较应该就是求解flag的关键，可以看出来有四个未知数，求解也是非常简单，z3直接求解即可：
from z3 import *
x, y, z, w = BitVecs("x y z w", 64)
#2 1 0 3
s = Solver()
s.add(x & ~z == 0x11204161012)
s.add(((x & ~y) & z) | x & ((y & z) | y & ~z | ~(y | z)) == 0x8020717153E3013)
s.add((x & ~z) | (y & z) | (x & ~y) | (z & ~y) == 0x3E3A4717373E7F1F)
s.add((0x3E3A4717373E7F1F ^ w) == 0x3E3A4717050F791F)
s.add(((x & ~z) | (y & z) | y & x) == (~z & x | 0xC00020130082C0C) and 1)
if s.check() == unsat:
print("无解")
else:
m = s.model()
for i in m:
print(f"%s = 0x%x"%(i, m[i].as_long()))
注意这里的y应该是有不唯一解，但在比赛中好像给出了中间部分的结果，所以这里并无大碍
接下来就是看求出来的四个未知数和flag的关系了，这里看到有这么个函数：
可以看到每相隔8位有一个case，如果不满8位则将v17加上w并右移八位。不难猜想，该函数的作用是将encode的前24个字母每8个分成一组，并按序号从小到低拼成一个十六进制数，最后未满8个的字母在一组，然后存进数组里进行刚才的z3运算
因此我们只要按顺序将刚才的x,y,z,w两位两位提取出来即可得到encode的内容。然后encode与key异或即可得到flag。交叉应用key，非常容易发现key的值为i_will_check_is_debug_or_not
因此写出解密脚本:
key = "i_will_check_is_debug_or_not"
enc = [0x3E, 0x3A, 0x46, 0x05, 0x33, 0x28, 0x6F, 0x0D, 0x8C, 0x00, 0x8A, 0x09, 0x78, 0x49, 0x2C, 0xAC, 0x08, 0x02, 0x07, 0x17, 0x15, 0x3E, 0x30, 0x13, 0x32, 0x31, 0x06]
flag = ''
for i in range(len(enc)):
flag += chr(enc[i] ^ ord(key[i % len(key)]))
print(flag)
得出结果：We1l_D0näeéb' _ólgebra_am_i
将中间的y换成题目给的e!P0or_a即可
flag{We1l_D0ne!P0or_algebra_am_i}