I do thank you for saying something since I found the claim so unbelievable I bookmarked it with a note to run every model checker and test generator I know of on those two components. All prior results Ive seen on compiler tech mean good QA tools usually find something. If the tool finds nothing, it's often a defective tool or a component already analyzed/tested to death by other tools. Now folks know it's better to invest effort in other parts of LLVM codebase.