Mismatch reported for nan values for promotion of half operation to float

[arsenm]

This testcase reports a mismatch in a resultant nan value, despite only consisting of canonicalizing operations:

define half @src0(half noundef %x, half noundef %y, half noundef %z) {
  %mul = fmul half %x, %y
  %result = fadd half %mul, %z
  ret half %result
}

define half @tgt0(half %x, half %y, half %z) {
  %x.ext = fpext half %x to float
  %y.ext = fpext half %y to float
  %z.ext = fpext half %z to float
  %mul = fmul float %x.ext, %y.ext
  %add = fadd float %mul, %z.ext
  %result = fptrunc float %add to half
  ret half %result
}

$alive-tv --smt-to=0 /tmp/mac-alive.ll

----------------------------------------
define half @src0(half noundef %x, half noundef %y, half noundef %z) {
#0:
  %mul = fmul half noundef %x, noundef %y
  %result = fadd half %mul, noundef %z
  ret half %result
}
=>
define half @tgt0(half %x, half %y, half %z) {
#0:
  %x.ext = fpext half %x to float
  %y.ext = fpext half %y to float
  %z.ext = fpext half %z to float
  %mul = fmul float %x.ext, %y.ext
  %add = fadd float %mul, %z.ext
  %result = fptrunc float %add to half
  ret half %result
}
Transformation doesn't verify!

ERROR: Value mismatch

Example:
half noundef %x = #x7c04 (SNaN)
half noundef %y = #x0000 (+0.0)
half noundef %z = #x0000 (+0.0)

Source:
half %mul = #xfe00 (QNaN)
half %result = #xfe00 (QNaN)

Target:
float %x.ext = #x7f808000 (SNaN)
float %y.ext = #x00000000 (+0.0)
float %z.ext = #x00000000 (+0.0)
float %mul = #x7f808000 (SNaN)
float %add = #x7ffd6000 (QNaN)
half %result = #x7feb (QNaN)
Source value: #xfe00 (QNaN)
Target value: #x7feb (QNaN)