Function precondition might not hold without hint

[MikaelMayer]

predicate problem(x: nat) {
  x > 2
}
function callProblem(x: nat): (j: nat)
  requires problem(x) {
  1
}
method Main() {
  var _ := callProblem(1);
}

We get the too simple error message in the IDE.

On the command line it's fine, it correctly reports two more locations.