// fichier validé par le plugin EVA de Frama-C

#include <assert.h>

int binary_search(long t[], int len, long v) {
  int l = 0, u = len-1 ;
  while (l <= u ) {
    int m = (u + l) / 2;  // <- débordement arithmétique inatteignable pour le "main" fourni 
    if (t[m] < v) l = m + 1;
    else if (t[m] > v) u = m - 1;
    else return m;
  }
  return -1;
}

void init(long t[], int len) {
  for (int i = 0; i < len; i++) {
    t[i] = i;
  }
}
  
#define N 100000

long a[N];

/*@assigns \result \from \nothing;*/
extern int input();

int main() {
  int x = input();
  init(a, N);
  int i = binary_search(a, N, x);
  assert (-1 <= i && i <= N);
  if (i >= 0) { assert (0 <= a[i] && a[i] <= N); }
}