Support of Casts In Uniqueness Checker

[The-Ray-Man]

The following test is accepted by the Uniqueness Checker. However the consume should not succeed because current is partially moved.

class A(
    @Unique val next : A?
)

fun <!VIPER_TEXT!>consume<!>(@Unique a : A) {}

fun <!VIPER_TEXT!>test<!>(@Unique a: A) {
    val current = a.next
    if (current != null) {
        val local = current.next
        consume(current)

    }
}

I think the problem is, that the CFG node for the access of current is followed by a SmartCastExpressionExitNode which seems to lose some information.