1  ==== Average, rounded down
 2  
 3  .Implementation
 4  [source]
 5  ----
 6  template<class T> T average_round_down(T x, T y) {
 7      return (x & y) + ((x ^ y) >> 1);
 8  }
 9  ----
10  
11  .Proof
12  [source]
13  ----
14  int main() {
15      unsigned x = nondet_unsigned();
16      unsigned y = nondet_unsigned();
17      unsigned z = average_round_down(x, y);
18      unsigned w = (uint64_t(x) + y) / 2;
19      assert(z == w);
20      return 0;
21  }
22  ----