Unsatisfiable formula ? maybe wrong syntax?

Question

Formula which I wanna solve looks like this in 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!");  

I rewrite it to z3py in the following way:

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)

Any suggestions ?
PS: Please notice that trying to solve formula in that form:
solve( (UDiv( (w*x*y+31), 8 )) * z == 0xffffffff)
is possible, so I can't belive that bit-wise operation causes this formula Unsatisfiable.

Answer 1

I don't see anything wrong in Z3 behavior. Why do you think the formula should be satisfiable?

A = (w*x*y+31) & ~31 -- imply that the 5 rightmost bits will be always zero

B = UDiv( A & ~31, 8 ) (equal to a logical shift right by 3) -- imply that the 2 rightmost bits will be always zero.

C = B * z -- this will always have the 2 rightmost bits zero

c == 0xffffffff -- that's impossible

If you change the constant to 0xfffffffc, then you'll get a solution.

Answer 2

The C program doesn't print anything for me. And Z3 says "no solution". So, it's consistent.

Does your C program prints "yeah!"? If so, aren't you on a big-endian machine? I've tried your example in an x86 machine.