Bug in loop fixed-point computation

[sonmarcho]

trafficstars

This triggers a bug (comes from investigating https://github.com/AeneasVerif/aeneas/issues/270 - it is a different bug):

pub enum List<T> {
    Cons(T, Box<List<T>>),
    Nil,
}

fn foo(h : &u8, mut t: &List<u8>) {
    let mut last = h;
    while let List::Cons(ht, tt) = t
    {
        last = ht;
        t = &*tt;
    }
}

The error is:

[Error] In file InterpreterLoopsFixedPoint.ml, line 680:
The sets of abstractions we need to end per region group are not pairwise disjoint

If we use the same lifetime for the two shared borrows, the translation succeeds:

pub enum List<T> {
    Cons(T, Box<List<T>>),
    Nil,
}

fn foo<'a>(h : &'a u8, mut t: &'a List<u8>) {
    let mut last = h;
    while let List::Cons(ht, tt) = t
    {
        last = ht;
        t = &*tt;
    }
}

The issue will be solved once we finish generalizing the support for loops (to add nested loops for instance).