nlopes added a comment. FWIW, I added support for constrained fadd/fsub/fmul/fdiv to Alive2 yesterday. Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://reviews.llvm.org/D118928/new/ https://reviews.llvm.org/D118928