diff --git a/charon/src/transform/control_flow/ullbc_to_llbc.rs b/charon/src/transform/control_flow/ullbc_to_llbc.rs index 55f0ea469..242d16c6a 100644 --- a/charon/src/transform/control_flow/ullbc_to_llbc.rs +++ b/charon/src/transform/control_flow/ullbc_to_llbc.rs @@ -841,7 +841,7 @@ impl ExitInfo { } }) .collect(); - let num_possible_candidates = loop_exits.len(); + let num_possible_candidates = possible_candidates.len(); // If there is exactly one one best candidate, it is easy. // Otherwise we need to split further. diff --git a/charon/tests/ui/control-flow/loops.out b/charon/tests/ui/control-flow/loops.out index 41bd2088a..94589203f 100644 --- a/charon/tests/ui/control-flow/loops.out +++ b/charon/tests/ui/control-flow/loops.out @@ -2079,10 +2079,11 @@ where return }, _ => { - panic(core::panicking::panic) + break 0 }, } } + panic(core::panicking::panic) } // Full name: test_crate::loop_break_1 diff --git a/charon/tests/ui/demo.out b/charon/tests/ui/demo.out index 9d251208b..0c230e056 100644 --- a/charon/tests/ui/demo.out +++ b/charon/tests/ui/demo.out @@ -376,10 +376,11 @@ where return }, _ => { - panic(core::panicking::panic) + break 0 }, } } + panic(core::panicking::panic) } // Full name: test_crate::i32_id