// kani-codegen-fail