Incorrect right shift operation for byte in Java

[MikaelMayer]

Dafny version

4.0.0

Code to produce this issue

newtype uint8 = x : int | 0 <= x < 256

method Main() {
  var y := 0x80 as bv8;
  var x := (y >> 4) as uint8;
  assert x != 248; // What Java obtains
  assert x == 0x8;
  if x == 248 {
    var x := 1/0;
  }
  print "All right";
}

Command to run and resulting output

dafny run --target java file.dfy

What happened?

This is a minimum reproductible example for #3724

Dafny program verifier finished with 2 verified, 0 errors
Exception in thread "main" java.lang.ArithmeticException: BigInteger divide by z
ero
        at java.base/java.math.MutableBigInteger.divideKnuth(MutableBigInteger.j
ava:1184)
        at java.base/java.math.BigInteger.divideKnuth(BigInteger.java:2318)
        at java.base/java.math.BigInteger.divide(BigInteger.java:2299)
        at dafny.DafnyEuclidean.EuclideanDivision(DafnyEuclidean.java:90)
        at _System.__default.Main(__default.java:22)
        at _System.__default.__Main(__default.java:27)
        at git_issu_3724bis.lambda$main$0(git_issu_3724bis.java:10)
        at dafny.Helpers.withHaltHandling(Helpers.java:279)
        at git_issu_3724bis.main(git_issu_3724bis.java:10

Looks like the generated Java code is the following:

    byte _0_y;
    _0_y = (byte) 128;
    byte _1_x;
    _1_x = ((byte) (byte)  ((byte)((_0_y) >>> ((byte) 4))));
    if ((_1_x) == ((byte) 248)) {
      java.math.BigInteger _2_x = java.math.BigInteger.ZERO;
      _2_x = dafny.DafnyEuclidean.EuclideanDivision(java.math.BigInteger.ONE, java.math.BigInteger.ZERO);
    }
    System.out.print((dafny.DafnySequence.asUnicodeString("All right")).verbatimString());

Transforming "4" in "3" and "0x80" in "0x40" does not trigger the stack overflow, so it's really the last byte.

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

Windows, Mac