diff --git a/regression/cbmc/array-bug-6230/main.c b/regression/cbmc/array-bug-6230/main.c
new file mode 100644
index 00000000000..5dc539954b7
--- /dev/null
+++ b/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;
+}
diff --git a/regression/cbmc/array-bug-6230/test.desc b/regression/cbmc/array-bug-6230/test.desc
new file mode 100644
index 00000000000..dc07bc8a3f3
--- /dev/null
+++ b/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