#include <stdio.h>

int __VERIFIER_nondet_getInt() {
  int x;
  scanf("%d", &x);
  return x;
}

void printInt(int x) {
  printf("answer=%d\n", x);
}