[lifthrasiir]

Not the author, but it is large enough to generalize to any other big bitvectors and small enough to handle. The use of SAT solver of course means that 32-bit is not a hard limit, but humans can't easily look at them.