#include <stdint.h>
#define UINT_LEAST64_MAX                               (18446744073709551616ULL)

/*
STDC(199901)
*/