Initializing assignments make iset/imap auto-ghost

[RustanLeino]

Dafny version

4.4.0

Code to produce this issue

method Test() {
  var s := {3, 3, 3, 5};
  var u := iset x | x in s; // BOGUS: this is making "u" auto-ghost

  var m := map[3 := true, 5 := false];
  var w := imap x | x in m :: true; // BOGUS: this is making "w" auto-ghost

  print u, w;
}

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

Command to run and resulting output

% dafny test.dfy
test.dfy(9,8): Error: ghost variables such as u are allowed only in specification contexts. u was inferred to be ghost based on its declaration or initialization. (ID: r_ghost_var_only_in_specifications)
test.dfy(9,11): Error: ghost variables such as w are allowed only in specification contexts. w was inferred to be ghost based on its declaration or initialization. (ID: r_ghost_var_only_in_specifications)
2 resolution/type errors detected in test.dfy

What happened?

The program should be compilable. However, the RHSs of the initializing assignments to u and w (which use iset/imap comprehensions where the "bounded pool" is coming from a collection, namely a set) are making those variables auto-ghost. This results in the errors shown above.

If the RHS expressions above are used in places other than initializing assignments, then Dafny correctly determines that they are compilable. This indicates that the bug lies in UsesSpecFeatures and that the similar (but different) method CheckIsCompilable is implemented correctly.

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

Mac