In the examples, 0x3bffffffffffffffff decodes to -18446744073709551616, which doesn't fit into int64_t. Why didn't they switch to bignums after INT64_MIN (-9223372036854775808) instead? Seems a bit asymmetric.