将约束放入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!
[CTF入门培训]顶尖高校博士及硕士团队亲授《30小时教你玩转CTF》，视频+靶场+题目！助力进入CTF世界
