#include <klee/klee.h>

typedef unsigned char byte;

#define N 5

byte a[N * N]=
{
/*   A B C D E*/
/*A*/1,1,1,1,1,
/*B*/1,1,0,0,1,
/*C*/1,0,1,1,1,
/*D*/1,0,1,1,0,
/*E*/1,1,1,0,1
};

int ham_cycle(byte *path)
{
        byte i;
        byte visited[N + 1] = { 0 };

        if (path[N] != path[0]) {
                return 0;
        }

        for (i = 0; i < N; i++) {
                if (path[i] >= N) {
                        return 0;
                }
                if (visited[path[i]]) {
                        return 0;
                }
                visited[path[i]]++;
        }

        for (i = 0; i < N; i++) {
                byte x = path[i];
                byte y = path[i + 1];
                if (!a[x + y * N]) {
                        return 0;
                }
        }
        return 1;
}

int main(int argc, char *argv[])
{
        byte i;
        byte cycle[N + 1];

        klee_make_symbolic(&cycle[0], sizeof(byte) * (N + 1), "cycle");
        klee_assert(!ham_cycle(cycle));
        return 0;
}