Reachable `unwrap()` panic in statement codegen for function pointer returning `!`

[nuczyc]

I tried this code:

fn diverge() -> ! {
    loop {}
}

#[kani::proof]
fn check_fnptr_never() {
    let f: fn() -> ! = diverge;
    f();
}

using the following command line invocation:

 RUST_BACKTRACE=1 ./scripts/kani test.rs

with Kani version:bc27348476839097611ea4af25e2af06be8dce20

I expected to see this happen:

VERIFICATION:- SUCCESSFUL

Instead, this happened:

Kani Rust Verifier 0.67.0 (standalone)

thread 'rustc' (1757809) panicked at kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs:776:52:
called `Option::unwrap()` on a `None` value
stack backtrace:
   0: __rustc::rust_begin_unwind
   1: core::panicking::panic_fmt
   2: core::panicking::panic
   3: core::option::unwrap_failed
   4: <core::option::Option<usize>>::unwrap
             at /home/yuchen/.rustup/toolchains/nightly-2025-12-03-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/option.rs:1016:21
   5: <kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_funcall
             at ./kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs:776:52
   6: <kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_terminator
             at ./kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs:311:22
   7: <kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_block
             at ./kani-compiler/src/codegen_cprover_gotoc/codegen/block.rs:41:34
   8: <kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_function::{closure#0}
             at ./kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs:81:57
   9: core::iter::traits::iterator::Iterator::for_each::call::<usize, <kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_function::{closure#0}>::{closure#0}
             at /home/yuchen/.rustup/toolchains/nightly-2025-12-03-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/iter/traits/iterator.rs:825:29
  10: <alloc::vec::into_iter::IntoIter<usize> as core::iter::traits::double_ended::DoubleEndedIterator>::rfold::<(), core::iter::traits::iterator::Iterator::for_each::call<usize, <kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_function::{closure#0}>::{closure#0}>
             at /home/yuchen/.rustup/toolchains/nightly-2025-12-03-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/iter/traits/double_ended.rs:308:21
  11: <core::iter::adapters::rev::Rev<alloc::vec::into_iter::IntoIter<usize>> as core::iter::traits::iterator::Iterator>::fold::<(), core::iter::traits::iterator::Iterator::for_each::call<usize, <kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_function::{closure#0}>::{closure#0}>
             at /home/yuchen/.rustup/toolchains/nightly-2025-12-03-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/iter/adapters/rev.rs:83:19
  12: <core::iter::adapters::rev::Rev<alloc::vec::into_iter::IntoIter<usize>> as core::iter::traits::iterator::Iterator>::for_each::<<kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_function::{closure#0}>
             at /home/yuchen/.rustup/toolchains/nightly-2025-12-03-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/iter/traits/iterator.rs:828:14
  13: <kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_function
             at ./kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs:81:38
  14: <kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend>::codegen_items::{closure#4}::{closure#4}
             at ./kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs:167:43
  15: <kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::call_with_panic_debug_info::<rustc_public::mir::mono::InstanceDef, <kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend>::codegen_items::{closure#4}::{closure#4}, <kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend>::codegen_items::{closure#4}::{closure#5}>::{closure#0}
             at ./kani-compiler/src/codegen_cprover_gotoc/utils/debug.rs:74:13
  16: <std::thread::local::LocalKey<core::cell::RefCell<(core::option::Option<alloc::boxed::Box<dyn core::ops::function::Fn<(), Output = alloc::string::String>>>, core::option::Option<cprover_bindings::goto_program::location::Location>)>>>::try_with::<<kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::call_with_panic_debug_info<rustc_public::mir::mono::InstanceDef, <kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend>::codegen_items::{closure#4}::{closure#4}, <kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend>::codegen_items::{closure#4}::{closure#5}>::{closure#0}, ()>
             at /home/yuchen/.rustup/toolchains/nightly-2025-12-03-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/std/src/thread/local.rs:513:12
  17: <std::thread::local::LocalKey<core::cell::RefCell<(core::option::Option<alloc::boxed::Box<dyn core::ops::function::Fn<(), Output = alloc::string::String>>>, core::option::Option<cprover_bindings::goto_program::location::Location>)>>>::with::<<kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::call_with_panic_debug_info<rustc_public::mir::mono::InstanceDef, <kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend>::codegen_items::{closure#4}::{closure#4}, <kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend>::codegen_items::{closure#4}::{closure#5}>::{closure#0}, ()>
             at /home/yuchen/.rustup/toolchains/nightly-2025-12-03-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/std/src/thread/local.rs:477:20
  18: <kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::call_with_panic_debug_info::<rustc_public::mir::mono::InstanceDef, <kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend>::codegen_items::{closure#4}::{closure#4}, <kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend>::codegen_items::{closure#4}::{closure#5}>
             at ./kani-compiler/src/codegen_cprover_gotoc/utils/debug.rs:69:30
  19: <kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend>::codegen_items::{closure#4}
             at ./kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs:166:33
  20: kani_compiler::codegen_cprover_gotoc::compiler_interface::with_timer::<core::option::Option<kani_metadata::harness::AssignsContract>, <kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend>::codegen_items::{closure#4}>
             at ./kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs:900:15
  21: <kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend>::codegen_items
             at ./kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs:139:29
  22: <kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend as rustc_codegen_ssa::traits::backend::CodegenBackend>::codegen_crate::{closure#0}
             at ./kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs:408:72
  23: rustc_public::rustc_internal::run::<<kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend as rustc_codegen_ssa::traits::backend::CodegenBackend>::codegen_crate::{closure#0}, alloc::boxed::Box<dyn core::any::Any>>::{closure#0}
             at /home/yuchen/.rustup/toolchains/nightly-2025-12-03-x86_64-unknown-linux-gnu/lib/rustlib/rustc-src/rust/compiler/rustc_public/src/rustc_internal/mod.rs:79:60
  24: rustc_public::compiler_interface::run::<rustc_public::rustc_internal::run<<kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend as rustc_codegen_ssa::traits::backend::CodegenBackend>::codegen_crate::{closure#0}, alloc::boxed::Box<dyn core::any::Any>>::{closure#0}, alloc::boxed::Box<dyn core::any::Any>>::{closure#0}
             at /home/yuchen/.rustup/toolchains/nightly-2025-12-03-x86_64-unknown-linux-gnu/lib/rustlib/rustc-src/rust/compiler/rustc_public/src/compiler_interface.rs:856:40
  25: <scoped_tls::ScopedKey<core::cell::Cell<*const ()>>>::set::<rustc_public::compiler_interface::run<rustc_public::rustc_internal::run<<kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend as rustc_codegen_ssa::traits::backend::CodegenBackend>::codegen_crate::{closure#0}, alloc::boxed::Box<dyn core::any::Any>>::{closure#0}, alloc::boxed::Box<dyn core::any::Any>>::{closure#0}, core::result::Result<alloc::boxed::Box<dyn core::any::Any>, rustc_public::error::Error>>
             at /rust/deps/scoped-tls-1.0.1/src/lib.rs:137:9
  26: rustc_public::compiler_interface::run::<rustc_public::rustc_internal::run<<kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend as rustc_codegen_ssa::traits::backend::CodegenBackend>::codegen_crate::{closure#0}, alloc::boxed::Box<dyn core::any::Any>>::{closure#0}, alloc::boxed::Box<dyn core::any::Any>>
             at /home/yuchen/.rustup/toolchains/nightly-2025-12-03-x86_64-unknown-linux-gnu/lib/rustlib/rustc-src/rust/compiler/rustc_public/src/compiler_interface.rs:856:13
  27: rustc_public::rustc_internal::run::<<kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend as rustc_codegen_ssa::traits::backend::CodegenBackend>::codegen_crate::{closure#0}, alloc::boxed::Box<dyn core::any::Any>>
             at /home/yuchen/.rustup/toolchains/nightly-2025-12-03-x86_64-unknown-linux-gnu/lib/rustlib/rustc-src/rust/compiler/rustc_public/src/rustc_internal/mod.rs:79:5
  28: <kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend as rustc_codegen_ssa::traits::backend::CodegenBackend>::codegen_crate
             at ./kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs:330:23
  29: <rustc_interface::queries::Linker>::codegen_and_build_linker
  30: <rustc_interface::passes::create_and_enter_global_ctxt<core::option::Option<rustc_interface::queries::Linker>, rustc_driver_impl::run_compiler::{closure#0}::{closure#2}>::{closure#2} as core::ops::function::FnOnce<(&rustc_session::session::Session, rustc_middle::ty::context::CurrentGcx, alloc::sync::Arc<rustc_data_structures::jobserver::Proxy>, &std::sync::once_lock::OnceLock<rustc_middle::ty::context::GlobalCtxt>, &rustc_data_structures::sync::worker_local::WorkerLocal<rustc_middle::arena::Arena>, &rustc_data_structures::sync::worker_local::WorkerLocal<rustc_hir::Arena>, rustc_driver_impl::run_compiler::{closure#0}::{closure#2})>>::call_once::{shim:vtable#0}
  31: rustc_interface::interface::run_compiler::<(), rustc_driver_impl::run_compiler::{closure#0}>::{closure#1}
note: Some details are omitted, run with `RUST_BACKTRACE=full` for a verbose backtrace.

Kani unexpectedly panicked during compilation.
Please file an issue here: https://github.com/model-checking/kani/issues/new?labels=bug&template=bug_report.md

[Kani] current codegen item: codegen_function: check_fnptr_never
_RNvCsgdZa4Rj9F6O_1_717check_fnptr_never
[Kani] current codegen location: Loc { file: "test.rs", function: None, start_line: 9, start_col: Some(1), end_line: 9, end_col: Some(23), pragmas: [] }
error: kani/target/kani/bin/kani-compiler exited with status exit status: 101