就记录个z3顺序输出
1
2
3
4
5
6
7
8
9
10
| from z3 import *
s = Solver()
flag = [BitVec("{}".format(i), 8) for i in range(23)]
if s.check() == sat:
m = s.model()
result = [int(str(m[each]), 10) for each in flag]
print(bytes(result))
|
BitVec类型不能直接转int，但是可以通过转str再转int。。。。。
真sb