Verus panics because rlimit-count is not in the map

[WeetHet]

@edwin1729 seems to have the same problem. It's not present on the verus playground

verus --record

Code:

use vstd::prelude::*;
verus! {
pub open spec fn nesting_level(input: Seq<char>) -> int
    decreases input.len(),
{
    if input.len() == 0 {
        0
    } else {
        let prev_nesting_level = nesting_level(input.drop_last());
        let c = input.last();
        if c == '(' {
            prev_nesting_level + 1
        } else if c == ')' {
            prev_nesting_level - 1
        } else {
            prev_nesting_level
        }
    }
}

pub open spec fn is_paren_char(c: char) -> bool {
    c == '(' || c == ')'
}

pub open spec fn is_balanced_group(input: Seq<char>) -> bool {
    &&& input.len() > 0
    &&& nesting_level(input) == 0
    &&& forall|i| 0 <= i < input.len() ==> is_paren_char(#[trigger] input[i])
}

pub open spec fn is_sequence_of_balanced_groups(input: Seq<char>) -> bool {
    &&& nesting_level(input) == 0
    &&& forall|i| 0 < i < input.len() ==> nesting_level(#[trigger] input.take(i)) >= 0
}

pub open spec fn vecs_to_seqs<T>(s: Seq<Vec<T>>) -> Seq<Seq<T>> {
    s.map(|_i, ss: Vec<T>| ss@)
}

pub open spec fn remove_nonparens(s: Seq<char>) -> Seq<char> {
    s.filter(|c| is_paren_char(c))
}

fn separate_paren_groups(input: &Vec<char>) -> (groups: Vec<Vec<char>>)
    requires
        is_sequence_of_balanced_groups(input@),
    ensures
        forall|i: int|
            #![trigger groups[i]]
            0 <= i < groups.len() ==> is_balanced_group(groups[i]@),
{
    let mut groups: Vec<Vec<char>> = Vec::new();
    let mut current_group: Vec<char> = Vec::new();
    let mut current_nesting_level: usize = 0;
    
    for i in 0..input.len()
        invariant
            0 <= i <= input.len(),
            current_nesting_level == nesting_level(current_group@) as usize,
            forall|j: int| 0 <= j < groups.len() ==> is_balanced_group(groups[j]@),
    {
        let c = input[i];
        if c == '(' {
            current_nesting_level += 1;
            current_group.push(c);
        } else if c == ')' {
            current_nesting_level -= 1;
            current_group.push(c);
            if current_nesting_level == 0 {
                groups.push(current_group);
                current_group = Vec::new();
            }
        }
    }
    
    groups
}
}
fn main() {}
// ==== verifiers ==== 
verus!{
fn separate_paren_groups_valid(input: &Vec<char>) -> (groups: Vec<Vec<char>>)
    // pre-conditions-start
    requires
        is_sequence_of_balanced_groups(input@),
    // pre-conditions-end
    // post-conditions-start
    ensures
        forall|i: int|
            #![trigger groups[i]]
            0 <= i < groups.len() ==> is_balanced_group(groups[i]@),
        vecs_to_seqs(groups@).flatten() == remove_nonparens(input@),
    // post-conditions-end
{ let ret = separate_paren_groups(input); ret }
}