将约束放入z3求解即可
>>>
from
z3
import
*
>>> a
=
Int
(
'a'
)
>>> b
'b'
>>> s
Solver()
>>> s.add(a
+
b
117738
0xCE1B5379
>>> s.add(a<
b)
>>> s.check()
sat
>>> s.model()
[a
56101
, b
61637
]
然后验证
C:\Users\4qwer\Desktop>KanXueCTF_Simple.exe
Please input: 56101-61637
Accepted!
[培训]内核驱动高级班，冲击BAT一流互联网大厂工作，每周日13:00-18:00直播授课
