1  ==== Counting 1-bits in a word
 2  .Implementation
 3  [source]
 4  ----
 5  int pop(unsigned x) {
 6     x = x - ((x >> 1) & 0x55555555);
 7     x = (x & 0x33333333) + ((x >> 2) & 0x33333333);
 8     x = (x + (x >> 4)) & 0x0F0F0F0F;
 9     x = x + (x >> 8);
10     x = x + (x >> 16);
11     return x & 0x0000003F;
12  }
13  ----
14  
15  .Proof
16  [source]
17  ----
18  int main() {
19      unsigned u = nondet_unsigned();
20      int i = pop(u);
21      assert(i == proof_popcnt(u));
22  }
23  ----