(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/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.