Another reply (can't edit my original reply now): what I have not done, though will if I ever have the chance again, is to prove correctness of bit-arithmetic l

Another reply (can't edit my original reply now): what I have not done, though will if I ever have the chance again, is to prove correctness of bit-arithmetic libraries (e.g. for use with symbolic execution). So long as you can represent your function in the SMT-LIB language (easy for this class of problem), you can prove properties of your code by asserting their respective negations in Z3 and asking it to prove satisfiability. If one of these properties doesn't hold, Z3 will tell you, and it will give you an example.