// #include <stdio.h>

/*@ requires x >= 0;
    ensures \result == \floor(x/2);
 */
int myfloor(int x) {
    return x >> 1;
}

/*
void main( void ) {
    for(int i = 0; i < 20; i++)
        printf("%d\t%d\n",i,myfloor(i));
}
*/