[Python] z3 solver Xor issue?

Is there a potential issue with z3 solver library. Sprecifically on Xor operator?

Running the following code in python would return 'unsat' while I believe the answer should be sat. Is this a potential issue with z3, or is my z3 library corrupted?


from z3 import *

l1 = Bool('l1')
l2 = Bool('l2')
l3 = Bool('l3')

s = Solver()
s.add(Xor(l1, l2, l3))
s.add(l3)
s.add(Not(l1))
s.add(Not(l2))
print(s.check())

Continue reading...