#pragma CIVL ACSL

/*@ predicate gt(int x, int y) = x > y;
  @*/

int main() {
  $assert(gt(1, 0));
}