Kani crashes when coverage is enabled and an unwind assertion fails

I tried this code:

#[kani::proof]
#[kani::unwind(1)]
fn foo() {
    let mut sum = 0;
    for i in 0..5 {
        sum += i;
    }
    sum = sum + 1;
}

using the following command line invocation:

kani cov_bug.rs --coverage -Zline-coverage

with Kani version: 0.47.0

I expected to see this happen: Kani doesn't crash

Instead, this happened:

$ kani cov_bug.rs --coverage -Zline-coverage
Kani Rust Verifier 0.47.0 (standalone)
warning: value assigned to `sum` is never read
 --> cov_bug.rs:8:5
  |
8 |     sum = sum + 1;
  |     ^^^
  |
  = help: maybe it is overwritten before being read?
  = note: `#[warn(unused_assignments)]` on by default

warning: 1 warning emitted

Checking harness foo...
CBMC 5.95.1 (cbmc-5.95.1)
CBMC version 5.95.1 (cbmc-5.95.1) 64-bit x86_64 linux
Reading GOTO program from file /home/zyadh/examples/cov_bug__RNvCsiBZXatwW6dG_7cov_bug3foo.out
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 16 object bits, 48 offset bits (user-specified)
Starting Bounded Model Checking
Not unwinding loop _RNvCsiBZXatwW6dG_7cov_bug3foo.0 iteration 1 file cov_bug.rs line 5 column 5 function foo thread 0
aborting path on assume(false) at file cov_bug.rs line 5 column 14 function foo thread 0
Runtime Symex: 0.0173246s
size of program expression: 198 steps
slicing removed 121 assignments
Generated 65 VCC(s), 39 remaining after simplification
Runtime Postprocess Equation: 0.0001281s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 0.0015949s
Running propositional reduction
Post-processing
Runtime Post-process: 3.54e-05s
Solving with CaDiCaL 1.7.2
325 variables, 330 clauses
SAT checker: instance is SATISFIABLE
Runtime Solver: 0.0001701s
Runtime decision procedure: 0.002079s
thread '<unnamed>' panicked at kani-driver/src/cbmc_property_renderer.rs:712:22:
internal error: entered unreachable code: status for coverage checks should be either `SUCCESS` or `FAILURE` prior to postprocessing
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

model-checking / kani

Kani crashes when coverage is enabled and an unwind assertion fails #3070