Inconsistent casting results for nested structures

[celinval]

CBMC version: 5.59.0 (cbmc-5.59.0)
Operating system: Ubuntu 18.04
Exact command line resulting in the issue: cbmc casting.c
What behaviour did you expect: The test should succeed.
What happened instead: The property fn.assertion.2 fails.

For the following test case:

// casting.c
#include<assert.h>

struct PtrWrapperInner {
    int* value;
};

struct PtrWrapper {
    int* value;
    struct PtrWrapperInner inner;
};

struct AltPtrWrapperInner {
    int* value;
};

struct AltPtrWrapper {
    unsigned int* value;
    // A) Doesn't work
    struct AltPtrWrapperInner inner;
    // B) Works
    //struct PtrWrapperInner inner;
};


void fn(struct PtrWrapper wrapper) {
    assert(*wrapper.value == 10);
    assert(*wrapper.inner.value == 10);
}

int main() {
    int ret = 10;
    int* ptr = &ret;

    struct AltPtrWrapper alt;
    alt.inner.value = ptr;
    alt.value = ptr;

    // Casting the structure itself works.
    struct PtrWrapper wrapper = *(struct PtrWrapper*) &alt;
    assert(*wrapper.value == 10);
    assert(*wrapper.inner.value == 10);

    // This only works if there is one level of casting.
    int (*alias) (struct AltPtrWrapper) = (int (*) (struct AltPtrWrapper)) fn;
    alias(alt);
}

The casting between AltPtrWrapper and PtrWrapper is successful when done explicitly but not due to calling the function alias, it seems that CBMC is casting the outer structure members, but not the inner ones. Note that if the inner structures have the same type (by commenting A and uncommenting B), the test succeeds.

[tautschnig]

Thank you for the nice reproducer! I've created #6959 to fix the issue.

[celinval]

That's amazing! Thank you for fixing this so fast.