20-Apr-2015: Using Z3 theorem prover to prove equivalence of some bizarre alternative to XOR operation.

(The following text has been copypasted to the SAT/SMT by example.)

Update2: some of discussions:

http://www.reddit.com/r/programming/comments/33830f/using_z3_theorem_prover_to_prove_equivalence_of/

http://www.reddit.com/r/ReverseEngineering/comments/33815w/using_z3_theorem_prover_to_prove_equivalence_of/

http://www.reddit.com/r/Python/comments/3384bt/using_z3_theorem_prover_to_prove_equivalence_of/

https://news.ycombinator.com/item?id=9407366

http://vk.com/wall-30666517_1127706 (Russian social networking site)

This open sourced site and this page in particular is hosted on GitHub. Patches, suggestions and comments are welcome.

→ [list of blog posts]