how to solve the undetermined issue in a let-such-that expression in Dafny?

Question

here is an example:

function intsetmax(s:set<int>):int
  requires |s| > 0
  ensures  var m := intsetmax(s);
           m in s && forall i :: i in s ==> m >= i
{
  var x :| x in s;
  if |s| == 1 then
    assert |s - {x}| == 0;
    x
  else
    var sy := s - {x};
    var y := intsetmax(sy);
    assert forall i :: i in s ==> i in sy || i == x;
    if x > y then x else y
}

function 'intsetmax' wants to find the max element in a set, but it shows an error "to be compilable, the value of a let-such-that expression must be uniquely determined", because of the statement "var x :| x in s".

This code works with Dafny versions that are less than 4.0, but it reports an error with 4.0.

So, how to solve it? Do I have to set the function as 'ghost'? Is there any way to get an element in a set?

Answer 1

Personally, I consider this to be a bug in the Dafny compiler (i.e. as you can compile such a statement in a method). I'm assuming the bug was introduced in the switch from Dafny 3 to Dafny 4. See more details here.

Answer 2

In versions of Dafny less than 4.0, function means ghost function. So you should just mark the function as ghost.