p4c: More questions on setInvalid

Hello. I have another clarification question on setInvalid, this is a follow-up to #2212. This issue is quite esoteric but has given me some trouble recently.

So for a program like this:

control ingress(inout Headers h, inout Meta m, inout standard_metadata_t sm) {
    apply {
        h.h.setInvalid();
        h.h.a = 16w2;
        h.eth_hdr.eth_type = h.h.a * h.eth_hdr.eth_type;
    }
}

the LocalCopyPropagation pass collapses the values into

control ingress(inout Headers h, inout Meta m, inout standard_metadata_t sm) {
    apply {
        h.h.setInvalid();
        h.eth_hdr.eth_type = 16w2 * h.eth_hdr.eth_type;
    }
}

h.eth_hdr is a valid header and its value is now always 16w2 * h.eth_hdr.eth_type after the pass instead of being undefined. However, since the alternative is undefined behaviour does it matter? The only case I can think of where this may affect the output is something like

control ingress(inout Headers h, inout Meta m, inout standard_metadata_t sm) {
    apply {
        h.h.setInvalid();
        h.h.a = 1;
        h.eth_hdr.src_addr = h.h.a;
        if (h.eth_hdr.src_addr != 1) {
            h.h.setValid();
            h.h.a = 1;
        }
    }
}

which is eventually turned into

control ingress(inout Headers h, inout Meta m, inout standard_metadata_t sm) {
    apply {
        h.h.setInvalid();
        h.h.a = 48w1;
        h.eth_hdr.src_addr = 48w1;
    }
}

because the assumption is that h.eth_hdr.src_addr is always 1. There may be undefined cases where the inequality is true, however. Or can this be treated as a case where all bets are off?

strange_set_valid.p4.txt strange_set_valid.stf.txt