#include <stdint.h>

extern uint64_t mytime ();