C# Wrong Result: Multi-level Multisets

[alex-usher]

Dafny version

4.1.0

Code to produce this issue

method Main() {
	var a: multiset<bool> := multiset{false, true};
	var b: multiset<multiset<bool>> := multiset{a[true := 0]};

	print b == multiset{multiset{false}}, "\n";
}

Command to run and resulting output

$ dafny /compile:4 main.dfy

Dafny program verifier finished with 1 verified, 0 errors
Running...

false

$ dafny /compile:4 /compileTarget:js main.dfy

Dafny program verifier finished with 1 verified, 0 errors
Running...

true

What happened?

The above program verifies and compiles successfully to all backends, but the C# backend will print false while all others will print true (where true would be the expected case).

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

Linux, Mac

[alex-usher]

Hi, just wanted to ping this issue as I believe it may be a soundness wrong result :)

[robin-aws]

Reopening because we had to revert the PR to fix nightly: https://github.com/dafny-lang/dafny/pull/5492