This patch enable following transform
(x + (~(y & c) + 1) --> x - (y & c) (x + (~((y >> z) & c) + 1) --> x - ((y>>z) & c) (x + (~(y | c) + 1) --> x - (y | c) if c is odd (x + (~((y >> z) | c) + 1) --> x - ((y>>z) | c) if c is odd
Z3 verification code:
http://rise4fun.com/Z3/ZA06
"atleast" --> "at least"