https://gcc.gnu.org/bugzilla/show_bug.cgi?id=67070
--- Comment #8 from Andrew Sutton <andrew.n.sutton at gmail dot com> --- And as an afterthought, adding negation makes the subsumption solver more complex, since determining implications in the presence of negation would mean decomposition of both the left and right sides of the implication, and modifying those term lists whenever negation is encountered. It's certainly doable, but it's going to add a *lot* of overhead: decomposing conjunctions on the RHS is the same as disjunctions on the LHS. That gets us into ways to heuristically simplify constraints by identifying and removing tautologies or reducing to contradiction where possible. I don't know what the overhead of those algorithms are.
