test/Concrete/ackermann.c


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
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;
}