You should definitely check AdrenSys writeup as it covers details about the challenge and the binary, I don't want to repeat what is already done. (Thank you for a great writeup!)
What I would like to add is how I solved this challenge, in a slightly different way, without involving Z3(although it's a great tool, and you should
try it :) ).
The key idea is that all 4 parts of the license key must not be equal to 0, but we know that (email_checksum ^ license_checksum ^ 0xaecbcc2) == 0.
The email checksum is 0xaed12f1, so the license_checksum should be 0x01ae33. Keeping in mind that all 4 parts of the license key
should not be equal to 0, we can create a license key with 3 parts having value 1 and the 4th part having value 0x42b0.