[Python] XOR with Z3 Python API - only returns a single solution

I am testing a single XOR statement using the Python API for Z3.

This is the output I get:

[B_L = True, A_L = False, C_L = False]


However, I should have 3 solutions, where two of the variables are false and the last is true. Where do I go wrong?

from z3 import *

A_L = Bool('A_L')
A_M = Bool('A_M')
A_R = Bool('A_R')

B_L = Bool('B_L')
B_M = Bool('B_M')
B_R = Bool('B_R')

C_L = Bool('C_L')
C_M = Bool('C_M')
C_R = Bool('C_R')

def OnlyA(a,b,c):
return And(a,Not(b),Not(c))

def XOR(a,b,c):
return Or(OnlyA(a,b,c),OnlyA(b,c,a),OnlyA(c,b,a))

s = Solver()

s.add(XOR(A_L,B_L,C_L))

if s.check() == sat:
m = s.model()
print(m)
else:
print("invalid installation profile")

Continue reading...