蓝帽杯半决Re-babynim
0x1 分析
输入
长度要求42 flag格式要求
取flag里面的十进制值
相乘然后和一个值对比
0x2 动调取值
取出要乘的值
取出密文
0x3 解密
import z3
a = z3.IntVal(56006392793428440965060594343955737638876552919041519193476344215226028549209672868995436445345986471)
b = z3.IntVal(51748409119571493927314047697799213641286278894049840228804594223988372501782894889443165173295123444031074892600769905627166718788675801)
s = z3.Solver()
flag =z3.Int("flag")
s.add(a*flag == b)
if s.check()==z3.sat:
print(s.model())
# [flag = 923973256239481267349126498121231231]
