1  ==== Unsigned division by 3
 2  
 3  .Implementation
 4  [source]
 5  ----
 6  inline unsigned udiv3(uint32_t dividend, unsigned *remainder) {
 7      uint32_t q = (dividend * (uint64_t)0xAAAAAAABu) >> 33;
 8      if(remainder) *remainder = dividend - q * 3;
 9      return q;
10  }
11  ----
12  
13  .Proof
14  [source]
15  ----
16  int main() {
17      unsigned n = nondet_unsigned();
18      unsigned r;
19      unsigned q = udiv3(n, &r);
20  
21      assert(q * 3 + r == n);
22      // cbmc is not able to prove this, or anything else I could come up with to
23      // fully prove division-by-3, in a reasonable period of time
24      //assert(r < 3);
25  }
26  ----