Assign-such-that drawing from iset/imap collection is reported as non-compilable

[RustanLeino]

Dafny version

4.4.0

Code to produce this issue

method Test(u: iset<int>, w: imap<int, bool>)
  requires 3 in u && 3 in w.Keys
{
  // BOGUS: these assign-such-that statements are reported as non-compilable
  var y :| y in u && LessThanFour(y); // but an iset is enumerable, so it is compilable
  var z :| z in w && LessThanFour(z); // and an imap is enumerable, so it is compilable

  print y, z;
}

predicate LessThanFour(x: int) {
  x < 4
}

method Main() {
  var s := {3, 3, 3, 5};
  var m := map[3 := true, 5 := false];
  Test(iset x | x in s, imap x | x in m :: true);
}

Command to run and resulting output

% dafny test.dfy

Dafny program verifier finished with 2 verified, 0 errors
test.dfy(22,8): Error: this assign-such-that statement is too advanced for the current compiler; Dafny's heuristics cannot find any bound for variable 'y' (ID: c_assign_such_that_is_too_complex)

To compile an assign-such-that statement, Dafny needs to find some appropriate bounds for each variable.
However, in this case the expression is too complex for Dafny's heuristics.
test.dfy(23,8): Error: this assign-such-that statement is too advanced for the current compiler; Dafny's heuristics cannot find any bound for variable 'z' (ID: c_assign_such_that_is_too_complex)

To compile an assign-such-that statement, Dafny needs to find some appropriate bounds for each variable.
However, in this case the expression is too complex for Dafny's heuristics.

What happened?

The program should be compilable, in the same way as if u and w were a finite set and finite map, respectively. However, Dafny whines that the expressions are too advanced to be compiled.

The problem is that the CollectionBoundedPool reports the Enumerable virtue only for finite collections.

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

Mac