const int not_five = 18446744073709551621; // actually 0x10000000000000005

/*%%*
integer is too large: 18446744073709551621
*%%*/