/* q18_a.h */

/*@ requires p <= 10;
    ensures \result == p + 1;
 */
int f(int p);