#include <klee/klee.h>

#define N 8
unsigned char queens[N];

int abs(int x)
{
  return x >= 0 ? x: -x;
}

int attack()
{
  int i, j;
  for (i = 0; i < N; i++) {
    for (j = i + 1; j < N; j++) {
      if ((queens[i] == queens[j]) ||
          (abs(queens[i] - queens[j]) == j - i)) {
        return 1;
      }
    }
  }
  return 0;
}

int main(int argc, char *argv[])
{
  int i;
  klee_make_symbolic(&queens[0], sizeof(unsigned char) * N, "queens");
  for (i = 0; i < N; i++) {
    queens[i] %= N;
  }
  klee_assert(attack());
  return 0;
}