[thaunatos]

It's worth noting that the author of the arcicle doesn't think it's worth integrating a SAT solver:

> Does this mean that rustc should integrate an industrial-strength SAT solver? As hilarious as that would be, I'm advocating no such thing. This will only be a performance issue on pathological examples crafted by bored nerds, and I don't think precious engineering time should be spent on that. Besides, generalizing a SAT algorithm to handle the full expressive power of Rust's patterns might be, to borrow some language from mathematicians, non-trivial.