Dafny fails to verify identical universal statements

[tjhance]

The following code fails to verify in Dafny 2.3.0. In particular, Dafny fails to verify a 'forall' statement even though the identical statement is directly available in the context.

predicate method {:opaque} foo(a: int, b: int)
{
  a == 5
}

lemma fooLemma(a: int, b: int, c: int)
ensures foo(a, b) ==> foo(a, c);
{
  reveal_foo();
}

lemma forallFooLemma()
// This post-condition fails to verify
ensures forall a, b, c | foo(a, b) :: foo(a, c);
{
  forall a, b, c | foo(a, b) 
  ensures foo(a, c)
  {
    fooLemma(a, b, c);
  }

  // This fails to verify, even though it ought to follow from the forall-body.
  assert forall a, b, c | foo(a, b) :: foo(a, c);

  // This fails to verify, even though it is identical to the above assertion.
  assert forall a, b, c | foo(a, b) :: foo(a, c);
}

which fails with these errors:

Dafny 2.3.0.10506
total_order.dfy(15,0): Error BP5003: A postcondition might not hold on this return path.
total_order.dfy(14,8): Related location: This is the postcondition that might not hold.
total_order.dfy(14,38): Related location
Execution trace:
    (0,0): anon0
    (0,0): anon8_Else
    (0,0): anon9_Then
    (0,0): anon5
    (0,0): anon10_Then
    (0,0): anon7
total_order.dfy(23,9): Error: assertion violation
total_order.dfy(23,39): Related location
Execution trace:
    (0,0): anon0
    (0,0): anon8_Else
    (0,0): anon9_Then
    (0,0): anon5
total_order.dfy(26,9): Error: assertion violation
total_order.dfy(26,39): Related location
Execution trace:
    (0,0): anon0
    (0,0): anon8_Else
    (0,0): anon9_Then
    (0,0): anon5
    (0,0): anon10_Then
    (0,0): anon7

Dafny program verifier finished with 1 verified, 3 errors

[RustanLeino]

The bug lies in the encoding of {:opaque} functions. Internally, the assumed quantifiers pass a parameter StartFuel__module._default.foo to foo, whereas the asserted quantifiers pass StartFuelAssert__module._default.foo. No relation between these two is known, unless reveal foo(); is called (in which case StartFuelAssert is known to be one more than StartFuel). To fix this issue, some relation between StartFuelAssert and StartFuel needs to always be encoded.

Here is a slightly shorter repro:

predicate method {:opaque} foo(a: int)

lemma Test()
{
  assume forall a :: foo(a);

  // This fails to verify, even though it is identical to the above assertion.
  assert forall a :: foo(a);
}