This patch handles the following case: turn
if (x <u Invariant1) {
if (zext(x) <u Invariant2) {
...
}
}into
if (x <u Invariant1) {
if (zext(Invariant1) <=u Invariant2) { // Unswitch here
// No check needed
} else {
if (zext(x) <u Invariant2) {
...
}
}
}
wile you are here. intro -> into