Cannot verify postcondition in lambda

[alexstaeding]

Dafny version

4.10.0

Code to produce this issue

function Foo(x: int): int requires x > 4 { x + 1 }
type F1 = f: int --> int | forall x :: f.requires(x) ==> f(x) > 5 witness Foo
type F2 = f: int --> int | forall x :: f.requires(x) ==> f(x) > 5 witness x requires x > 4 => x + 1

Command to run and resulting output

dafny verify Test.dfy
Test.dfy(20,74): Error: the given witness expression might not satisfy constraint
   |
20 | type F2 = f: int --> int | forall x :: f.requires(x) ==> f(x) > 5 witness x requires x > 4 => x + 1

What happened?

Dafny seems to be unable to verify that the postcondition f(x) > 5 holds, but only when the type is instantiated by a lambda. Instantiating the type with Foo verifies as expected.

I asked on zulip first, but this does now seem to be a bug.

What type of operating system are you experiencing the problem on?

Mac