Possibly faulty "Contract might not be well-formed error"

[bobismijnnaam]

Via https://github.com/viperproject/silicon/issues/537:

Carbon and Silicon both disapprove of the following:

method m(last: Seq[Seq[Bool]], l: Int, k: Int)
  requires (forall z: Int :: { last[z] } 0 <= z && z < |last| ==> 0 <= l && l < |last[z]| /* && last[z][l] == false */)
  requires (forall z: Int :: 0 <= z && z < |last| ==> last[z][l] == false) 
{ }

Output:

Contract might not be well-formed. Index l into last[z] might be negative. ([email protected])

The verification failure disappears if I move the statement that's not well-formed into the previous forall:

method m(last: Seq[Seq[Bool]], l: Int, k: Int)
  requires (forall z: Int :: { last[z] } 0 <= z && z < |last| ==> 0 <= l && l < |last[z]| && last[z][l] == false )
  // requires (forall z: Int :: 0 <= z && z < |last| ==> last[z][l] == false) 
{ }

[mschwerhoff]

A cursory inspection suggests a triggering problem, as explained in Silicon issue #537.