Loop contracts in closure run too slow

[thanhnguyen-aws]

I tried this code:

#![feature(proc_macro_hygiene)]
#![feature(stmt_expr_attributes)] 

fn simple_while_loops(x: &mut u8, y: &mut u8) {
    let mut closure_with_loop = || 
    {
        #[kani::loop_invariant(*x >= 2)]
        #[kani::loop_modifies(x as *const _, y as *const _)]
        while *x > 2 {
            *x = *x - 1;
            #[kani::loop_invariant(*y >= 2)]
            #[kani::loop_modifies(y as *const _)]
            while *y > 2 {
                *y = *y - 1;
            }
        }
    };
    closure_with_loop();
}

#[kani::proof]
fn multiple_loops_harness() {
    let mut x: u8 = kani::any_where(|i| *i >= 10);
    let mut y: u8 = kani::any_where(|i| *i >= 10);
    simple_while_loops(&mut x, &mut y);
}

using the following command line invocation:

kani src/closureloop.rs -Z loop-contracts

with Kani version: 0.65.0

I expected to see this happen: VERIFICATION:- SUCCESSFUL

Instead, this happened: Kani runs forever. Some of the output:

Starting Bounded Model Checking
Unwinding loop _RNCNvCsgkQR1KaHvr3_11closureloop18simple_while_loops0B3_.0 iteration 1 file src/closureloop.rs line 12 column 13 function simple_while_loops::{closure#0} thread 0
Unwinding loop __CPROVER_contracts_write_set_check_assigns_clause_inclusion.0 iteration 1 file <builtin-library-__CPROVER_contracts_library> line 986 function __CPROVER_contracts_write_set_check_assigns_clause_inclusion thread 0
aborting path on assume(false) at file src/closureloop.rs line 12 column 13 function simple_while_loops::{closure#0} thread 0
Unwinding loop _RNCNvCsgkQR1KaHvr3_11closureloop18simple_while_loops0B3_.1 iteration 1 file src/closureloop.rs line 8 column 9 function simple_while_loops::{closure#0} thread 0
Unwinding loop _RNCNvCsgkQR1KaHvr3_11closureloop18simple_while_loops0B3_.0 iteration 1 file src/closureloop.rs line 12 column 13 function simple_while_loops::{closure#0} thread 0
Unwinding loop __CPROVER_contracts_write_set_check_assigns_clause_inclusion.0 iteration 1 file <builtin-library-__CPROVER_contracts_library> line 986 function __CPROVER_contracts_write_set_check_assigns_clause_inclusion thread 0
aborting path on assume(false) at file src/closureloop.rs line 12 column 13 function simple_while_loops::{closure#0} thread 0
...
size of program expression: 4290 steps
slicing removed 1514 assignments
Generated 626 VCC(s), 192 remaining after simplification

For reference, Kani very quickly returns VERIFICATION:- SUCCESSFUL for the following equivalent function:

fn simple_while_loops(x: &mut u8, y: &mut u8) {
        #[kani::loop_invariant(*x >= 2)]
        #[kani::loop_modifies(x as *const _, y as *const _)]
        while *x > 2 {
            *x = *x - 1;
            #[kani::loop_invariant(*y >= 2)]
            #[kani::loop_modifies(y as *const _)]
            while *y > 2 {
                *y = *y - 1;
            }
        }
}

I think the reason is that CBMC add more VCCs for inferring the loop_assigns clauses. I don't know if it is possible to fix it from CBMC side.