Z3でアセンブリをチェックする

ZJITのfixnum除算におけるオーバーフローバグ修正のため、分岐なしテスト（xor, xor, or, test, je）が提案された。このコードが元のC条件（left == FIXNUM_MIN && right == -1）と等価であることを、SMTソルバーZ3を用いて証明した。条件を否定して反例を探索させる手法により、等価性が確認された。