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

int main()
{
uint64_t x;
int y = 0xfd000000;

x = 3;
x <<= 32;
x |= y;
printf("0x%016llx\n", x);
return 0;
}