Checking assembly with Z3

A Ruby ZJIT contributor fixed an overflow bug in fixnum division when dividing FIXNUM_MIN by -1, which produces a bignum instead of a fixnum. The patch used a branchless test using xor, or, test, and je instructions in the JIT's low-level IR. The author used the Z3 SMT solver to prove the equivalence of the original C condition and the new branchless assembly code.