How did you find the z3 lib?
We also managed to figure out all those equations but then didn't know how to go on.
Neither matlab nor mathematica wanted to help us and by googling terms like "equation system xor", "solve plus minus xor" and similar words we weren't able to find something that can actually solve that.