Checking assembly with Z3 (opens in new tab)

Short post today. New ZJIT contributor dak2 to fix an overflow bug in fixnum division in ZJIT. We did the division fine, but lied about the type of the result in the case of dividing FIXNUM_MIN by -1. You can see how this is special-cased in CRuby: static inline void rb_fix_divmod_fix(VALUE a, VALUE b, VALUE *divp, VALUE *modp) { // ... if (x == FIXNUM_MIN && y == -1) { if (divp) *divp = LONG2NUM(-FIXNUM_MIN); if (modp) *modp = LONG2FIX(0); return; } // ... } Since -FIXNUM_MIN (note the negat...