The refinement that is done when encountering branching uses UnionDomain.meet, which currently causes unsound behavior and crashes.

In the following example, Goblint considers both branches of the if to be dead:

The reason is that the meet of a: $(field: x, value: 12)$ and b: $(field: f, value: 129.0)$ yields $(field: \bot, value: \bot)$.

In an example where the union type contains either a char or an int, Goblint crashes with a IncompatibleIkind-exception, because the abstract values with ikinds of Char and Int are passed to a meet.