RKSimon wrote: > Sadly alive2 times out on this test... But if you have better luck, [try it out](https://alive2.llvm.org/ce/z/GBbJ-F) You should be able to get it to work using smaller types - i4 operands usually works for binary ops https://github.com/llvm/llvm-project/pull/171865