无法满足的公式？也许语法错误？

Question

我想解决的公式在 C 中如下所示：

#define foo(w,x,y) ((((w)*(x)*(y)+31) & ~31) / 8)  
WORD w,x,y,z;  
y = 24;  
if( (foo(w,x,y) * z) == -1 )  
    printf("yeah!");  

我通过以下方式将其重写为z3py：

from z3 import *
w= BitVec('w',16)
x= BitVec('x',16)
z= BitVec('z',16)
y= BitVecVal(24,16)
solve( (UDiv( (w*x*y+31) & ~31, 8 )) * z == 0xffffffff)

有什么建议吗？
PS：请注意尝试以该形式求解公式：
solve( (UDiv( (w*x*y+31), 8 )) * z == 0xffffffff)
是可能的，所以我无法相信按位运算会导致这个公式无法满足。

Answer 1

我认为 Z3 的行为没有任何问题。为什么你认为公式应该是可满足的？

A = (w*x*y+31) & ~31 -- 暗示最右边的 5 位将始终为零

B = UDiv( A & ~31, 8 )（等于逻辑右移 3）——意味着最右边的 2 位将始终为零。

C = B * z -- 这将始终有 2 个最右边的位为零

c == 0xffffffff -- 那是不可能的

如果你把常数改成0xfffffffc，那么你会得到一个解决方案。

Answer 2

C 程序不会为我打印任何内容。 Z3说“没有解决方案”。所以，它是一致的。

您的 C 程序是否打印“是的！”？如果是这样，你不是在大端机器上吗？我在 x86 机器上试过你的例子。