void f2(int n) {
  $assert n>=0;
}