一开始以为是z3可解，就直接上z3，后来上angr，浪费很多时间，仔细看了一下源码发现是大整数乘积，a*a-7*b*b=8，再加上其他限制可解Pell's equation.
[招生]科锐逆向工程师培训(2024年11月15日实地，远程教学同时开班, 第51期)
