Malformed Boogie for if-then-else with non-reference traits

[RustanLeino]

Dafny version

4.6.0

Code to produce this issue

trait Parent { }

class Record extends Parent {}

function Pick(b: bool, r: Record, d: Parent): Parent {
  if b then r else d
}

Command to run and resulting output

% dafny run test.dfy --type-system-refresh --general-traits=datatype
test.dfy(6,4): Error: branches of if-then-else have incompatible types ref and Box
test.dfy(6,4): Error: branches of if-then-else have incompatible types ref and Box
test.dfy(6,4): Error: branches of if-then-else have incompatible types ref and Box
3 type checking errors detected in /tmp/test__module.bpl

*** Encountered internal translation error - re-running Boogie to get better debug information

/tmp/test__module.bpl(3372,53): Error: branches of if-then-else have incompatible types ref and Box
/tmp/test__module.bpl(3382,63): Error: branches of if-then-else have incompatible types ref and Box
/tmp/test__module.bpl(3393,13): Error: branches of if-then-else have incompatible types ref and Box
3 type checking errors detected in /tmp/test__module.bpl

What happened?

The verifier generates malformed Boogie. In particular, one of the branches of the generated Boogie if-then-else expression is missing a $Box conversion.

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

Mac