Soundness issue when variable present in function postcondition with recursive call with same arguments

[samuelchassot]

Dafny version

4.10.1

Code to produce this issue

function example(elements: int) : (r: int)
    ensures 
        var i := 1;
        example(elements) == 0
   
{
    1
}

Command to run and resulting output

❯ dafny verify dbug.dfy

Dafny program verifier finished with 1 verified, 0 errors

What happened?

When defining a variable in a function postcondition that contain recursive calls with same arguments, we are able to prove false.
When we remove either the variable definition or replace the recursive call by the named output variable, the verification fails as intended.

While analyzing the produced boogie, we could see that in the procedure for well-formedness, the free postcondition is:

free ensures {:always_assume} _module.__default.example#canCall(elements#0);

when the variable is present but is:

free ensures {:always_assume} elements#0 == elements#0 || _module.__default.example#canCall(elements#0);

when it is not.

This only difference makes the verification pass or fail.

This bug was discovered by @Brandon-Rozek.

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

Mac