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