Hacker News new | ask | show | jobs
by Randor 947 days ago
Yep, Z3 can do exactly this using BitVec and passed to prove() or just compare the expressions directly..