Failing test to demonstrate renaming inconsistencies

The mapping from L1 names to types is not in line with the different types used
across loop iterations.

Author: tautschnig

regression/cbmc/vla3/main.c

@@ -0,0 +1,30 @@
+#include <assert.h>
+
+int main(int argc, char *argv[])
+{
+  unsigned char x = argc;
+
+  for(int i = 0; i < 3; ++i)
+  {
+    struct S
+    {
+      int a;
+      int b[x + i + 1];
+      int *c;
+    } __attribute((packed));
+
+    struct S s;
+
+    for(int j = 0; j < i; ++j)
+      s.b[x + j] = j;
+
+    for(int j = 0; j < i; ++j)
+      assert(s.b[x + j] == j);
+
+    assert(
+      sizeof(struct S) ==
+      sizeof(int *) + ((unsigned char)argc + i + 2) * sizeof(int));
+  }
+
+  return 0;
+}

regression/cbmc/vla3/test.desc

@@ -0,0 +1,11 @@
+KNOWNBUG
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Renaming is inconsistent across loop iterations as we map L1 names to types, but
+do not actually introduce new L1 ids each time we declare an object.