#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;
}