by-clause ignored for assign-such-that statements

[RustanLeino]

Dafny version

4.9.1

Code to produce this issue

function F(x: int): int

method Works() {
  var a :| F(a) == 2 by {
    assume {:axiom} F(10) == 2;
  }
}

method ByClauseIsIgnored() {
  var a;
  a :| F(a) == 2 by { // this gives an error, but it should not
    assume {:axiom} F(10) == 2;
  }
}

Command to run and resulting output

% dafny verify test.dfy
test.dfy(11,4): Error: cannot establish the existence of LHS values that satisfy the such-that predicate
   |
11 |   a :| F(a) == 2 by { // this gives an error, but it should not
   |   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^


Dafny program verifier finished with 1 verified, 1 error

What happened?

The by clause in method Works works. The assumption contained therein proves the existence of an a.

Method ByClauseIgnored is similar, but uses just an assign-such-that statement with a by clause (rather than a statement that combines var and :=). Here, the assume statement does not help and the verifier cannot prove the existence of an a. Indeed, there is no trace of the assume statement in the Boogie that's generated.

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

Mac