Error: function precondition might not hold

This error can occur when trying to write a sequence comprehension expression like

function f(i: int): int
  requires i < 10 
{
  i
}

method test() {
  var s := seq(5, i => f(i));
}

which produces

ERROR_SeqComp.dfy(8,23): Error: function precondition might not hold
ERROR_SeqComp.dfy(2,13): Related location

Dafny program verifier finished with 0 verified, 1 error

The problem is that current Dafny does not implicitly impose the condition that the function used to initialize the sequence elements is only called with nat values less than the size of the new sequence. That condition has to be made explicit:

function f(i: int): int
  requires i < 10 
{
  i
}

method test() {
  var s := seq(5, i requires i < 10 => f(i));
}