1  ==== Turn off rightmost one
 2  
 3  .Implementation
 4  [source]
 5  ----
 6  template<class T> T turn_off_rightmost_one(T x) { return x & (x - 1); }
 7  ----
 8  
 9  .Proof
10  [source]
11  ----
12  int main() {
13      unsigned x = nondet_unsigned() | 1;
14      unsigned y = nondet_unsigned() & 31;
15      unsigned z = x << y;
16      assert(turn_off_rightmost_one(z) == (z ^ (1u<<y)));
17  }
18  ----