Speaking as a compiler user, how much longer until we can expect better support for Mixed Boolean Arithmetic (MBA) simplification from compilers? For example, it's problematic that GCC and Clang aren't able to tell that `((((x ^ y) | (~(x ^ y) + 1)) >> 63) - 1)` is equivalent to `x==y` or that `(((x ^ ((x ^ y) | ((x - y) ^ y))) >> 63) - 1)` is equivalent to `x>=y`. We need MBA simplification because the algebra engines don't support it and malware authors frequently use it to obfuscate programs. But if we could plug it into a C compiler that shows us in assembly what the code is actually doing, then it would help a lot with software analysis.