More precise bitwise AND

[elazarg]

x & K can at least be inferred to be <= K. This is not the case currently.

[caballa]

I'm assuming you mean that y = x & k implies that y <= k

E.g., given x = 10, k = -3 and bitwdith=4 we get y = 1010 & 1101 = 1000

which in decimal, y = 8. Thus, we cannot infer here that y <= -3