From 597df194218f2de174ead6b8a1abb2555f8bef4b Mon Sep 17 00:00:00 2001
From: Martin Nowack <m.nowack@imperial.ac.uk>
Date: Mon, 27 Apr 2020 17:45:25 +0100
Subject: Add test case from #1257 to reproduce behaviour

---
 test/regression/2020-04-27-stp-array-names.c | 24 ++++++++++++++++++++++++
 1 file changed, 24 insertions(+)
 create mode 100644 test/regression/2020-04-27-stp-array-names.c

(limited to 'test')

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];
+  }
+}
-- 
cgit 1.4.1