1 files changed, 12 insertions, 0 deletions
diff --git a/test/regression/2008-04-10-bad-alloca-free.c b/test/regression/2008-04-10-bad-alloca-free.c
new file mode 100644
index 00000000..46e2b0cf
--- /dev/null
+++ b/test/regression/2008-04-10-bad-alloca-free.c
@@ -0,0 +1,12 @@
+// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc
+// RUN: %klee --exit-on-error %t1.bc
+
+void f(int *addr) {
+  klee_make_symbolic_name(addr, sizeof *addr, "moo");
+}
+
+int main() {
+  int x;
+  f(&x);
+  return x;
+}