Hacker News Reader

Yeah I'm pretty sure Z3 can do all the examples easily. Nice simple interface though!

Yep, Z3 can do exactly this using BitVec and passed to prove() or just compare the expressions directly..