C# and Go Backends: Incorrect finite map semantics

[khemichew]

Dafny version

4.6.0

Code to produce this issue

method Main() {
 var result := map numerator: int | 8 <= numerator && numerator < 12 :: numerator / 5 := false;
 print result;
}

Command to run and resulting output

dotnet dafny/Binaries/Dafny.dll build --target:cs main.dfy
dotnet main.dll
map[1 := false, 2 := false]

dotnet dafny/Binaries/Dafny.dll build --target:py main.dfy
python main-py/__main__.py
map[1 := false, 2 := false]

dotnet dafny/Binaries/Dafny.dll build --target:java main.dfy
java -jar main.jar
map[1 := false, 2 := false]

-------------------------------------
dotnet dafny/Binaries/Dafny.dll build --target:js main.dfy
node main.js
map[1 := false, 1 := false, 2 := false, 2 := false]

dotnet dafny/Binaries/Dafny.dll build --target:go main.dfy
./main
map[1 := false, 1 := false, 2 := false, 2 := false]

What happened?

The example showcases the map comprehension expression which assigns the false value to the keys 1 and 2.

The entries should be unique for each key but are duplicated in the C# and Go backends.

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

Linux

[stefan-aws]

I can confirm the problem, but believe the issue contains a typo: the problematic backends are js and go.

[kbuaaaaaa]

Not sure if this will be helpful, but the issue in Go started from here ffbee004e08628c430c1f56bf3a87318afcba992