一开始以为是z3可解，就直接上z3，后来上angr，浪费很多时间，仔细看了一下源码发现是大整数乘积，a*a-7*b*b=8，再加上其他限制可解Pell's equation.
[培训]内核驱动高级班，冲击BAT一流互联网大厂工作，每周日13:00-18:00直播授课
