Error: cannot generate fold-unfold Viper statements

[nishanthkarthik]

Details: cannot generate fold-unfold Viper statements. The required permission Acc(_1.val_int, read) cannot be obtained.

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

Removing the #[ensures(!u32::is_s(&1u32))] below makes verification succeed.

extern crate prusti_contracts;
use prusti_contracts::*;

struct S;

trait SFind {
    #[pure]
    fn is_s(&self) -> bool;
}

impl SFind for S {
    #[pure]
    fn is_s(&self) -> bool {
        true
    }
}

impl SFind for u32 {
    #[pure]
    fn is_s(&self) -> bool { false }
}

#[requires(T::is_s(&t))]
#[ensures(T::is_s(&t))]
#[ensures(!u32::is_s(&1u32))]
fn foo<T: SFind>(t: T) {

}

fn main() {
    foo::<S>(S);
}