[Bug]: Quantification over all char values implemented incorrectly in Java runtime

[robin-aws]

Dafny version

3.9.1

Code to produce this issue

method Main() {
  var allChars := set c: char | true;
  var allUTF16CodeUnits := set i: int | 0 <= i < 0x10000 :: i as char;
  assert forall c: char :: 0 <= c as int < 0x10000;
  assert allChars == allUTF16CodeUnits;
  
  if allChars != allUTF16CodeUnits {
    print 1/0;
  }
}

Command to run and results

dafny run Scratch.dfy -t:java

What happened?

Exception in thread "main" java.lang.ArithmeticException: BigInteger divide by zero

Root cause is a typo in Helpers.AllChars() (0x1000 instead of 0x1_0000).

Will fix in the upcoming --unicode-char implementation PR, just wanted to track the soundness bug.

Loving the new issue template! :)

What type of Operating System are you seeing the problem on?

Mac