Skip to content

Instantly share code, notes, and snippets.

@Mr-Slippery
Created November 19, 2020 22:06
Show Gist options
  • Save Mr-Slippery/7cf6fbdcb6b8786912f2dbf866043535 to your computer and use it in GitHub Desktop.
Save Mr-Slippery/7cf6fbdcb6b8786912f2dbf866043535 to your computer and use it in GitHub Desktop.
Finding Ramanujan's taxicab number 1729 with KLEE
#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;
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment