Unsatisfiable公式？也許錯誤的語法？

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最右邊的位零

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

如果更改爲0xfffffffc常量，那麼你會得到一個解。

Answer 2

C程序不會爲我打印任何東西。而Z3說「沒有解決方案」。所以，這是一致的。

您的C程序是否打印「是啊！」？如果是這樣，你不是在一個大型機器上？我在x86機器上試過你的例子。