SAT Brute Force solver isn't correct

[wrigjl]

The default instance for SAT is:

(x1 | !x2 | x3) & (!x1 | x3 | x1) & (x2 | !x3 | x1) & (!x3 | x4 | !x2 | x1) & (!x4 | !x1) & (x4 | x3 | !x1)

and the solver produces:

Solution: (x1:True,x2:False,x3:True,x4:True)

Which is NOT a solution. One of the conjunctions is (!x4 | !x1) which would be (!T | !T) => (F | F) => F

This particular problem appears to have 5 solutions (in order x1 to x4): 0000, 0101, 0111, 1000, 1110.

I suspect, but have not verified, that is has to do with how the bits are assigned to the variables. There is a solution with exactly three bits set (actually 2), but 1011 isn't one of them.