use std::fmt::Display;

enum Foo {
    A(String),
    B(String),
}

impl Display for Foo {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        let s = match self {
            Foo::A(s) => format!("A.{s}"),
            Foo::B(s) => format!("B.{s}"),
        };
        write!(f, "{s}")?;
        Ok(())
    }
}

#[kani::proof]
#[kani::unwind(6)]
fn fast() {
    let a = Foo::A(String::from("foo"));
    let s = match a {
        Foo::A(s) => format!("A.{s}"),
        Foo::B(s) => format!("B.{s}"),
    };
    assert_eq!(s, "A.foo");
}

#[kani::proof]
#[kani::unwind(6)]
fn slow() {
    let a = Foo::A(String::from("foo"));
    let s = a.to_string();
    assert_eq!(s, "A.foo");
}