#include <inttypes.h>

int64_t dbl(int64_t x) {
  return x + x;
}