1 files changed, 16 insertions, 0 deletions
diff --git a/test/Concrete/ackermann.c b/test/Concrete/ackermann.c
new file mode 100644
index 00000000..0f21a3ab
--- /dev/null
+++ b/test/Concrete/ackermann.c
@@ -0,0 +1,16 @@
+// llvm-gcc -O2 --emit-llvm -c ackermann.c && ../../Debug/bin/klee ackermann.o 2 2
+
+#include <stdio.h>
+
+int ackermann(int m, int n) {
+   if (m == 0)
+     return n+1;
+   else
+     return ackermann(m-1, (n==0) ? 1 : ackermann(m, n-1));
+ }
+
+int main() {
+  printf("ackerman(%d, %d) = %d\n", 2, 2, ackermann(2, 2));
+
+  return 0;
+}