Finding Ramanujan's taxicab number 1729 with KLEE

taxi.c

#include <klee/klee.h>
#include <assert.h>

#define N (15)

#define SYM(x) { \
  klee_make_symbolic(&x, sizeof x, #x); \
}

int main() {
  unsigned int a, b, c, d, r;
  SYM(a); SYM(b); SYM(c); SYM(d); SYM(r);
  klee_assert(!(a < N && b < N && c < N && d < N &&
                a * a * a + b * b * b == r &&
                c * c * c + d * d * d == r &&
                a != c && a != d));
  return 0;
}