Add test case from #1257 to reproduce behaviour

1 files changed, 24 insertions, 0 deletions

diff --git a/test/regression/2020-04-27-stp-array-names.c b/test/regression/2020-04-27-stp-array-names.c
new file mode 100644
index 00000000..f06e1b1a
--- /dev/null
+++ b/test/regression/2020-04-27-stp-array-names.c
@@ -0,0 +1,24 @@
+// RUN: %clang %s -emit-llvm %O0opt -g -c -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee -output-dir=%t.klee-out --search=bfs --max-instructions=1000 %t.bc
+b;
+a(c) {
+  if (!c)
+    abort();
+}
+main() {
+  int e;
+  short d;
+  klee_make_symbolic(&d, sizeof(d), "__sym___VERIFIER_nondet_short");
+  b = d;
+  a(b > 0);
+  int f[b];
+  int g[b];
+  for (;;) {
+    short d;
+    klee_make_symbolic(&d, sizeof(d), "__sym___VERIFIER_nondet_short");
+    a(d >= 0 && d < b);
+    f[d];
+    g[b - 1 - d];
+  }
+}