Finding a Magic Square with KLEE

#include <klee/klee.h>

#define N 3

unsigned char square[N * N];

unsigned int line(int i, int j) { return i * N + j; }

unsigned int col(int i, int j) { return i + j * N; }

unsigned int sum_line_col(unsigned int (*f)(int i, int j))
{
    int i, j;
    unsigned int sum, csum;

    for (i = 0; i < N; i++) {
        csum = 0;
        for (j = 0; j < N; j++) {
            csum += square[ f(i, j) ];
        }
        if (0 == i) {
            sum = csum;
        }
        if (sum != csum) {
            return 0;
        }
    }
    return csum;
}

unsigned int sum_diag()
{
    int i;
    unsigned int main_sum = 0, sec_sum = 0;
    for (i = 0; i < N; i++) {
        main_sum += square[ line(i, i) ];
    }

    unsigned int sum = 0;
    for (i = 0; i < N; i++) {
        sec_sum += square[ line(i, i) ];
    }

    if (main_sum != sec_sum) {
        return 0;
    }
    return main_sum;
}

int each_once()
{
    unsigned char all_nums[N * N] = { 0 };
    int i, j;
    for (i = 0; i < N; i++) {
        for (j = 0; j < N; j++) {
            unsigned cell = square[ line(i, j) ];
            if (cell > N * N || cell < 1) {
                return 0;
            }
            all_nums[cell - 1]++;
        }
    }
    for(i = 0; i < N * N; i++) {
        if (all_nums[i] > 1) {
            return 0;
        }
    }
    return 1;
}

int magic()
{
    unsigned int s_line = sum_line_col(&line);
    unsigned int s_col = sum_line_col(&col);
    unsigned int s_diag = sum_diag();
    if (each_once() && s_line == s_col && s_col == s_diag) {
        return 1;
    }
    return 0;
}

int main(int argc, char *argv[])
{
    klee_make_symbolic(&square[0], sizeof(unsigned char) * N * N, "square");
    klee_assert(!magic());
    return 0;
}