Stack overflow for mutually recursive specifications

[vfukala]

On

use prusti_contracts::*;

#[pure]
#[requires(g())]
fn f() -> bool {
    unreachable!()
}

#[pure]
#[requires(f())]
fn g() -> bool {
    unreachable!()
}

fn main() {}

, Prusti overflows the stack:

  __          __        __  ___             
 |__)  _\/_  |__) |  | /__`  |   ____\/_  | 
 |      /\   |  \ \__/ .__/  |       /\   | 

Prusti version: 0.2.2, commit d3dc99990e2 2023-06-26 14:59:58 UTC, built on 2023-07-01 23:37:13 UTC
Verification of 3 items...

thread 'rustc' has overflowed its stack
fatal runtime error: stack overflow

Note that Prusti also produces an unexpected internal error on

use prusti_contracts::*;

#[pure]
#[requires(f())]
fn f() -> bool {
    unreachable!()
}

fn main() {}

, but I think this is the same kind of error as the one expected in prusti-tests/tests/verify_partial/fail/issues/issues-769.rs.