Negative coverage: borrow_check_loop / fixed-point / premise if state0 == state1

Premise at line 596. Observed failure causes: if_false.

3 tests failed proving this premise:

Source location: tests/borrowck.rs:3967 (all coverage from this test)

fn conditional() -> u32 {
    exists<'r0, 'r1, 'r2, 'r3> {
        let b: X = X { value: 0_u32 };
        let p: &'r0 mut X = &'r1 mut b;
        'l: loop {
            let now: &'r2 mut X = &'r2 mut *p;
            if true {
                if true {
                    let next: &'r3 mut X = next_of::<'r3>(&'r3 mut *now);
                    p = next;
                } else {
                }
            } else {
                break 'l;
            }
        }
        return 0_u32;
    }
}

Source location: tests/borrowck.rs:4233 (all coverage from this test)

fn next<'a>(d: &'a mut Decoder) -> &'a u32 {
    exists<'r0, 'r1> {
        'l: loop {
            let buf: &'r0 u32 = fill_buf::<'r0>(&'r0 mut (*d).buf_read);
            let s: &'r1 u32 = decode::<'r1>(buf);
            if true {
                return s;
            } else {
            }
        }
    }
}

Source location: tests/borrowck.rs:4356 (all coverage from this test)

fn next<'s>(f: &'s mut Filter) -> &'s mut u32 {
    exists<'r0, 'r1, 'r2> {
        'l: loop {
            let item: &'r0 mut u32 = iter_next::<'r0>(&'r0 mut (*f).iter);
            if true {
                let keep: bool = call_predicate::<'r1, 'r2>(&'r1 mut (*f).predicate, &'r2 *item);
                if keep {
                    return item;
                } else {
                }
            } else {
                break 'l;
            }
        }
        return no_item::<'s>();
    }
}