Kani incorrectly assumes that SwitchInts have at least one branch #4103
Description
I tried this code:
pub enum Reference {
ByName { alias: String },
}
#[kani::proof]
fn check_nontrivial_drop() {
let result: Reference = Reference::ByName { alias: "foo".into() };
drop(result)
}using the following command line invocation:
cargo kani
with Kani version: 0.62.0
I expected to see this happen: Verification succeeds
Instead, this happened:
Kani Rust Verifier 0.62.0 (cargo plugin)
Compiling playground v0.1.0 (/Users/cmzech/playground)
thread 'rustc' panicked at kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs:502:9:
assertion failed: targets.len() > 1
stack backtrace:
error: internal compiler error: Kani unexpectedly panicked at panicked at kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs:502:9:
assertion failed: targets.len() > 1.
0: __rustc::rust_begin_unwind
1: core::panicking::panic_fmt
2: core::panicking::panic
3: kani_compiler::codegen_cprover_gotoc::codegen::statement::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_switch_int
at /Users/cmzech/kani/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs:502:9
4: kani_compiler::codegen_cprover_gotoc::codegen::statement::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_terminator
at /Users/cmzech/kani/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs:207:17
5: kani_compiler::codegen_cprover_gotoc::codegen::block::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_block
at /Users/cmzech/kani/kani-compiler/src/codegen_cprover_gotoc/codegen/block.rs:41:29
6: kani_compiler::codegen_cprover_gotoc::codegen::function::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_function::{{closure}}
at /Users/cmzech/kani/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs:81:52
7: core::iter::traits::iterator::Iterator::for_each::call::{{closure}}
at /Users/cmzech/.rustup/toolchains/nightly-2025-05-24-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/iter/traits/iterator.rs:798:29
8: core::iter::traits::double_ended::DoubleEndedIterator::rfold
at /Users/cmzech/.rustup/toolchains/nightly-2025-05-24-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/iter/traits/double_ended.rs:308:21
9: <core::iter::adapters::rev::Rev<I> as core::iter::traits::iterator::Iterator>::fold
at /Users/cmzech/.rustup/toolchains/nightly-2025-05-24-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/iter/adapters/rev.rs:64:9
10: core::iter::traits::iterator::Iterator::for_each
at /Users/cmzech/.rustup/toolchains/nightly-2025-05-24-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/iter/traits/iterator.rs:801:9
11: kani_compiler::codegen_cprover_gotoc::codegen::function::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_function
at /Users/cmzech/kani/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs:81:13
12: kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend::codegen_items::{{closure}}::{{closure}}
at /Users/cmzech/kani/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs:162:39
13: kani_compiler::codegen_cprover_gotoc::utils::debug::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::call_with_panic_debug_info::{{closure}}
at /Users/cmzech/kani/kani-compiler/src/codegen_cprover_gotoc/utils/debug.rs:66:13
14: std::thread::local::LocalKey<T>::try_with
at /Users/cmzech/.rustup/toolchains/nightly-2025-05-24-aarch64-apple-darwin/lib/rustlib/src/rust/library/std/src/thread/local.rs:315:12
15: std::thread::local::LocalKey<T>::with
at /Users/cmzech/.rustup/toolchains/nightly-2025-05-24-aarch64-apple-darwin/lib/rustlib/src/rust/library/std/src/thread/local.rs:279:15
16: kani_compiler::codegen_cprover_gotoc::utils::debug::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::call_with_panic_debug_info
at /Users/cmzech/kani/kani-compiler/src/codegen_cprover_gotoc/utils/debug.rs:64:9
17: kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend::codegen_items::{{closure}}
at /Users/cmzech/kani/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs:161:29
18: kani_compiler::codegen_cprover_gotoc::compiler_interface::with_timer
at /Users/cmzech/kani/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs:838:15
19: kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend::codegen_items
at /Users/cmzech/kani/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs:134:29
20: <kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend as rustc_codegen_ssa::traits::backend::CodegenBackend>::codegen_crate::{{closure}}
at /Users/cmzech/kani/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs:323:63
21: rustc_smir::rustc_internal::init::{{closure}}
at /Users/cmzech/.rustup/toolchains/nightly-2025-05-24-aarch64-apple-darwin/lib/rustlib/src/rust/compiler/rustc_smir/src/rustc_internal/mod.rs:206:33
22: scoped_tls::ScopedKey<T>::set
at /rust/deps/scoped-tls-1.0.1/src/lib.rs:137:9
23: rustc_smir::rustc_internal::init
at /Users/cmzech/.rustup/toolchains/nightly-2025-05-24-aarch64-apple-darwin/lib/rustlib/src/rust/compiler/rustc_smir/src/rustc_internal/mod.rs:206:5
24: rustc_smir::rustc_internal::run::{{closure}}
at /Users/cmzech/.rustup/toolchains/nightly-2025-05-24-aarch64-apple-darwin/lib/rustlib/src/rust/compiler/rustc_smir/src/rustc_internal/mod.rs:242:56
25: rustc_smir::stable_mir::compiler_interface::run::{{closure}}
at /Users/cmzech/.rustup/toolchains/nightly-2025-05-24-aarch64-apple-darwin/lib/rustlib/src/rust/compiler/rustc_smir/src/stable_mir/compiler_interface.rs:482:40
26: scoped_tls::ScopedKey<T>::set
at /rust/deps/scoped-tls-1.0.1/src/lib.rs:137:9
27: rustc_smir::stable_mir::compiler_interface::run
at /Users/cmzech/.rustup/toolchains/nightly-2025-05-24-aarch64-apple-darwin/lib/rustlib/src/rust/compiler/rustc_smir/src/stable_mir/compiler_interface.rs:482:9
28: rustc_smir::rustc_internal::run
at /Users/cmzech/.rustup/toolchains/nightly-2025-05-24-aarch64-apple-darwin/lib/rustlib/src/rust/compiler/rustc_smir/src/rustc_internal/mod.rs:242:5
29: <kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend as rustc_codegen_ssa::traits::backend::CodegenBackend>::codegen_crate
at /Users/cmzech/kani/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs:279:23
30: <rustc_interface::queries::Linker>::codegen_and_build_linker
31: rustc_interface::passes::create_and_enter_global_ctxt::<core::option::Option<rustc_interface::queries::Linker>, rustc_driver_impl::run_compiler::{closure#0}::{closure#2}>
32: 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: std::ptr::drop_in_place::<Reference>
_RINvNtCsc7IzUIR3vjn_4core3ptr13drop_in_placeNtCsfNXD7nFlnMP_10playground9ReferenceEBI_
[Kani] current codegen location: Loc { file: "/Users/cmzech/.rustup/toolchains/nightly-2025-05-24-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/ptr/mod.rs", function: None, start_line: 797, start_col: Some(1), end_line: 797, end_col: Some(56), pragmas: [] }
error: could not compile `playground` (lib)
Caused by:
process didn't exit successfully: `/Users/cmzech/kani/target/kani/bin/kani-compiler --crate-name playground --edition=2024 src/lib.rs --error-format=json --json=diagnostic-rendered-ansi,artifacts,future-incompat --diagnostic-width=204 --crate-type lib --emit=dep-info,metadata,link -C embed-bitcode=no -C debuginfo=2 -C split-debuginfo=unpacked --check-cfg 'cfg(docsrs,test)' --check-cfg 'cfg(feature, values())' -C metadata=8c3b025410d851c8 -C extra-filename=-2ae3a27962318259 --out-dir /Users/cmzech/playground/target/kani/aarch64-apple-darwin/debug/deps --target aarch64-apple-darwin -C incremental=/Users/cmzech/playground/target/kani/aarch64-apple-darwin/debug/incremental -L dependency=/Users/cmzech/playground/target/kani/aarch64-apple-darwin/debug/deps -L dependency=/Users/cmzech/playground/target/kani/debug/deps -Cllvm-args=--reachability=harnesses -C overflow-checks=on -Z unstable-options -Z trim-diagnostic-paths=no -Z human_readable_cgu_names -Z always-encode-mir --cfg=kani -Z 'crate-attr=feature(register_tool)' -Z 'crate-attr=register_tool(kanitool)' --sysroot /Users/cmzech/kani/target/kani -L /Users/cmzech/kani/target/kani/lib --extern kani --extern 'noprelude:std=/Users/cmzech/kani/target/kani/lib/libstd.rlib' -C panic=abort -C symbol-mangling-version=v0 -Z panic_abort_tests=yes -Z mir-enable-passes=-RemoveStorageMarkers '--check-cfg=cfg(kani)' -Clinker=echo --kani-compiler '-Cllvm-args=--check-version=0.62.0 --log-level=warn --assertion-reach-checks'` (exit status: 101)
error: Failed to compile `playground` due to an internal compiler error.: error: internal compiler error: Kani unexpectedly panicked at panicked at kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs:502:9:
assertion failed: targets.len() > 1.