diff --git a/regression/cbmc/Struct_Initialization/flexible_array_member.c b/regression/cbmc/Struct_Initialization/flexible_array_member.c
new file mode 100644
index 00000000000..158c13586cf
--- /dev/null
+++ b/regression/cbmc/Struct_Initialization/flexible_array_member.c
@@ -0,0 +1,16 @@
+#include <assert.h>
+
+struct f
+{
+  int w;
+  int x[];
+};
+
+struct f f = {4, {0, 1, 2, 3}};
+
+int main()
+{
+  assert(sizeof(f) == sizeof(int));
+  assert(f.x[1] == 1);
+  return 0;
+}
diff --git a/regression/cbmc/Struct_Initialization/flexible_array_member.desc b/regression/cbmc/Struct_Initialization/flexible_array_member.desc
new file mode 100644
index 00000000000..b08c8c05a87
--- /dev/null
+++ b/regression/cbmc/Struct_Initialization/flexible_array_member.desc
@@ -0,0 +1,10 @@
+KNOWNBUG
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Based on issue #3653.