OpenSMT 2

int nondet();

int f (int a ){

  if (a < 10)

    return f (a + 1);

  return a - 10;

}

void main(){

  int y = 0;

  int x = nondet();

  __CPROVER_assume(x > 8 && x < 100);

  if (x > 0) y = f (x);

  assert (y >= 0);

}