CBMC version: 5.95.1
Operating system: Ubuntu 22.04
Exact command line resulting in the issue: cbmc --trace <example program below>
What behaviour did you expect: The size of the second struct should be 16 bytes.
What happened instead: CBMC thought the size is 6 bytes and reported a false alarm.

Example program:

#include <assert.h>
#include <stdio.h>

typedef struct Example_packed_s {
  char c;
  int i;
} __attribute__((packed)) Example_packed_t;

typedef struct Example_aligned_s {
  char c;
  Example_packed_t i __attribute__((aligned(8)));
} Example_aligned_t;

int main() {
  printf("Size of example packed struct = %ld\n", sizeof(Example_packed_t));
  printf("Size of example aligned struct = %ld\n", sizeof(Example_aligned_t));
  assert(sizeof(Example_packed_t) == 5);
  assert(sizeof(Example_aligned_t) == 16);
  return 0;
}

It seems the packed attribute in the first struct also influenced the second struct and caused CBMC to pack the second member i in Example_aligned_t. (Therefore, the size is 1 + 5 = 6 bytes).

Violated property:
  file compiler_atrribute_nested.c function main line 18 thread 0
  assertion sizeof(Example_aligned_t) == 16
  sizeof(Example_aligned_t) /*6ul*/  == (unsigned long int)16

GCC version gcc (Ubuntu 11.4.0-1ubuntu1~22.04) 11.4.0 confirms that the size of the second struct is 16 bytes.