为什么z3方程失败了?

2024-03-29 05:44:21 发布

您现在位置:Python中文网/ 问答频道 /正文

我需要解这个代码(C中的代码)

if ( ((0xAAAAAAAAAAAAAAABLL * len_input_serial >> 64) >> 1)+ len_input_serial- 3 * ((0xAAAAAAAAAAAAAAABLL * len_input_serial >> 64) >> 1) != 14)
    return 0xFFFFFFFFLL;

这是我的python脚本

from z3 import *
len_input_serial = BitVec("serial_len",64)
solve(LShR(LShR(0xAAAAAAAAAAAAAAABL * len_input_serial,64),1) + len_input_serial - 3 * LShR(LShR(0xAAAAAAAAAAAAAAABL * len_input_serial,64),1) == 14)

但是这给了我[serial_len = 14]

我知道解决方案应该在[42,38,40]左右,那么这里出了什么问题?你知道吗


Tags: 代码fromimport脚本inputlenreturnif
1条回答
网友
1楼 · 发布于 2024-03-29 05:44:21

此表达式:

(0xAAAAAAAAAAAAAAABLL * len_input_serial >> 64) >> 1

总是等价于0。如果将64位量右移64位,则得到0。(请注意,您使用的是LShr,它将其输入视为无符号量。)

因此,整个过程简化为求解len_input_serial == 14,这就是Z3产生的答案。你知道吗

请注意,在Python中编写长整数(即0x123L等)时,可以获得无限精度。(参见此处:Maximum value for long integer)。在C语言中,很可能是64位整数。因此,您的Z3代码实际上是正确的;是Python在这里使用了更高的精度,因此造成了混乱。你知道吗

相关问题 更多 >