2026-09-17 10:44 UTC
Thought I had just discovered my first LLVM bug while working on the Lean runtime, but someone beat me to it: https://github.com/llvm/llvm-project/issues/217376 The good news is that the fix is already released, so I'm not blocked on the work I'm actually supposed to do, but I wouldn't have said no to the experience of reporting a bug to LLVM either 🙂
Replies (1)
-
@juhi@hachyderm.io 2026-09-17 10:47
Also interesting: the faulty optimization apparently had an alive2 (LLVM's formal verification tool for their optimization passes) proof attached to it, but due to a typo in an assertion it didn't actually prove anything. A nice example of one of the pitfalls of formal verification. https://github.com/llvm/llvm-project/issues/217376#issuecomment-5348043980