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