Make labelled separation logic asserts preserve labels (#8671)

Make labelled separation logic asserts preserve labels (#8671)

This is a first step towards fixing #8659.

The issue is that when two labels are equal, we assume they refer to subheaps of the same heap. This is incorrect for magic wand. This ensures we preserve labels, a further PR will ensure that syntactic equality on labels (instead of semantic equality) is used for knowing when two pto constraints must be unified. This means that SEP_LABEL nodes should never be rewritten.