A simplified example that triggers issue 6230, from @SaswatPadhi

regression/cbmc/array-bug-6230/main.c

@@ -0,0 +1,19 @@
+#include <stdint.h>
+#include <stdlib.h>
+
+struct inner
+{
+  uint32_t exts[32]; // 32 is the minimum to crash
+};
+
+struct outer
+{
+  struct inner ctx; // Nesting is necessary
+};
+
+int main()
+{
+  struct outer *s = malloc(sizeof(struct outer));
+  if(s != NULL)
+    s->ctx.exts[0] = 0;
+}

regression/cbmc/array-bug-6230/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--malloc-may-fail --malloc-fail-null --pointer-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+A simplified test case that triggers issue #6230