##
#include
#include
#include
int main( void ) {
double x = 9007199254740992;
printf( "%"PRIu64"\n", (uint64_t)( x ) );
printf( "%"PRIu64"\n", (uint64_t)( x + 1 ) );
printf( "%"PRIu64"\n", (uint64_t)( (uint64_t)x + 1 ) );
}
## ##
9007199254740992
9007199254740992
9007199254740993