Internal error: Location bb6[1] has not yet been encoded

[nishanthkarthik]

extern crate prusti_contracts;
use prusti_contracts::*;

fn main() {
    let xs: [u8; 10] = Default::default();
    let mut v: std::vec::Vec<&u8> = std::vec::Vec::new();

    let mut i = 0;
    while i < 10 {
        v.push(&xs[i]); // error
        i += 1;
    }
}

mir dump showing bb6

// WARNING: This output format is intended for human consumers only
// and is subject to change without notice. Knock yourself out.
fn main() -> () {
    let mut _0: ();
    let _1: [u8; 10];
    let mut _4: bool;
    let mut _5: usize;
    let _6: ();
    let mut _7: &mut std::vec::Vec<&u8>;
    let _8: &u8;
    let _9: usize;
    let mut _10: usize;
    let mut _11: bool;
    let mut _12: (usize, bool);
    scope 1 {
        debug xs => _1;
        let mut _2: std::vec::Vec<&u8>;
        scope 2 {
            debug v => _2;
            let mut _3: usize;
            scope 3 {
                debug i => _3;
            }
        }
    }

    bb0: {
        _1 = <[u8; 10] as Default>::default() -> [return: bb1, unwind continue];
    }

    bb1: {
        _2 = Vec::<&u8>::new() -> [return: bb2, unwind continue];
    }

    bb2: {
        _3 = const 0_usize;
        goto -> bb3;
    }

    bb3: {
        _5 = _3;
        _4 = Lt(move _5, const 10_usize);
        switchInt(move _4) -> [0: bb8, otherwise: bb4];
    }

    bb4: {
        _7 = &mut _2;
        _9 = _3;
        _10 = const 10_usize;
        _11 = Lt(_9, _10);
        assert(move _11, "index out of bounds: the length is {} but the index is {}", move _10, _9) -> [success: bb5, unwind: bb10];
    }

    bb5: {
        _8 = &_1[_9];
        _6 = Vec::<&u8>::push(move _7, _8) -> [return: bb6, unwind: bb10];
    }

    bb6: {
        _12 = CheckedAdd(_3, const 1_usize);
        assert(!move (_12.1: bool), "attempt to compute `{} + {}`, which would overflow", _3, const 1_usize) -> [success: bb7, unwind: bb10];
    }

    bb7: {
        _3 = move (_12.0: usize);
        goto -> bb3;
    }

    bb8: {
        drop(_2) -> [return: bb9, unwind continue];
    }

    bb9: {
        return;
    }

    bb10 (cleanup): {
        drop(_2) -> [return: bb11, unwind terminate(cleanup)];
    }

    bb11 (cleanup): {
        resume;
    }
}

main::{constant#0}: usize = {
    let mut _0: usize;

    bb0: {
        _0 = const 10_usize;
        return;
    }
}

Prusti version: 0.2.2, commit 0d4a8d4 2024-03-26 13:08:03 UTC, built on 2024-03-26 13:20:57 UTC