#include <inttypes.h>
#include <stdint.h>
#include <stdio.h>

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 ) );
}