Error: (error "line 66 column 36: Sort mismatch at argument #1 for function (declare-fun or (Bool Bool) Bool) supplied sort is Int") sat

[ghost]

I have just started workign with Z3 for my bachelors computer science and engineering. One of the assignments was to provide solutions for the 8 queens problem.

The logic behind the solutions can be found below:

The text file attaches is the logic written out for Z3 but I can't seem to figure out what causes the error. I was hoping someone could give me some insight since I am still a novice.

8queens.txt

[NikolajBjorner]

The error message suggests that you are passing an integer expression to "or".
Your text file declares the variables as Int. You should try to declare them as Bool.

[NikolajBjorner]

See also https://github.com/Z3Prover/z3/tree/master/examples/userPropagator
for a tuned version of 8 queens enumeration