将约束放入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!
[注意]传递专业知识、拓宽行业人脉——看雪讲师团队等你加入！
