> Branchless (left == FIXNUM_MIN && right == -1): (left ^ MIN) | (right ^ -1) == 0.

> I didn’t understand why those were equivalent.

Well, it's, uh, the same reason why "xor eax, eax" zeros eax. So "a ^ b" is zero only when a is equal to b; and "a | b" is zero only when both a and b are zero.

> The core trick to use Z3 as a “proof engine” that I learned from CF [They note that this is a “standard technique” and they did not come up with it] is to make Z3 search for counter-examples by negating the condition

Isn't that how Prolog's resolution works, technically? All the facts, plus the negation of the query, are conjuncted together, and then the resolution rule is applied, until you derive falsity; that means that the negation of the query is false or, equivalently, that the query is true.