vonaka

@carolynzech I added some basic tests. Regarding PR itself, defining `force_fn_once` to later replace it with literarily the same function feels suboptimal. Maybe at the very least, the body of...

> Remove the compiler & kani_core changes entirely and just do the transformations entirely in the macro expansion logic. I would think you could just change the macro logic to...

> Thanks! Before merging, can you check if we can indeed get rid of `kani_register_contract`? We can't, we still need this workaround to call closures from const functions.

Just for the record, I believe this boils down to the following: ```rust #[derive(PartialEq)] enum Enum { First, Second, } #[kani::ensures(|result| *result == Enum::First)] const fn first() -> Enum {...