Writing to a value via a pointer fails in some circumstances

[DanielG]

CBMC version: 9ee5b9d (develop), also reproducible on 5.11 and 5.10 (from Debian) to an extent
Operating system: Debian amd64

The program below is a minimal reproducer of a problem I encountered while trying to verify a uC program of mine. I have found three "fixes" to get the program to verify one of which only works on develop, see the comments.

Test program:

typedef void (*callback_t)(void);

struct xfer {
        union { /*< FIX: union -> struct */
                struct {
                        int * buf;
                        callback_t callback; /*< FIX: remove */
                } a;
        };
} g_xfer;

int g_buf;

int main()
{
        g_xfer = (struct xfer) {{{ &g_buf }}};

        /* FIX, uncomment (only on cbmc develop 9ee5b9d6): */
        // g_xfer.a.buf = &g_buf;

        /* check the pointer was initialized properly */
        assert(g_xfer.a.buf == &g_buf);

        g_xfer.a.buf[0] = 42; /* write a value via the pointer */
        assert(g_xfer.a.buf[0] == 42); /* check it was written */
        assert(g_buf == 42); /* the underlying value should also be updated */
}

Exact command line resulting in the issue: cbmc test.c
What behaviour did you expect: All three properties should succeed.
What happened instead: The last two assertions fail. Doing what any one of the "FIX" comments say will get all properties to succeed.