Contract fails due to promoted constants being havocked #3228
Description
I tried this code:
extern crate kani;
#[derive(PartialEq, Eq)]
pub enum Foo {
A,
B,
}
#[kani::ensures(result == Foo::A)]
pub fn a() -> Foo {
Foo::A
}
#[kani::proof_for_contract(a)]
fn check() {
let _ = a();
}using the following command line invocation:
kani enum_ensures_bug.rs -Zfunction-contracts
with Kani version: 7bf23a2
I expected to see this happen: Verification succeeds
Instead, this happened:
SUMMARY:
** 1 of 1336 failed
Failed Checks: result == Foo::A
File: "enum_ensures_bug.rs", line 9, in a_check_7b31b
VERIFICATION:- FAILED
Verification Time: 1.9666983s