Bitwise operators

&

(& x y)

(& x y)

• takes x: integer
• takes y: integer
• produces integer

Bitwise and

Supported in either invariants or properties.

|

(| x y)

(| x y)

• takes x: integer
• takes y: integer
• produces integer

Bitwise or

Supported in either invariants or properties.

xor

(xor x y)

(xor x y)

• takes x: integer
• takes y: integer
• produces integer

Bitwise exclusive-or

Supported in either invariants or properties.

shift

(shift x y)

(shift x y)

• takes x: integer
• takes y: integer
• produces integer

Shift x y bits left if y is positive, or right by -y bits otherwise.

Supported in either invariants or properties.

~

(~ x)

(~ x)

• takes x: integer
• produces integer

Reverse all bits in x

Supported in either invariants or properties.