thread 'main' panicked at ...kani-verifier-0.54.0/src/lib.rs:156:38: No exit code?

[weaversa]

I'm not able to provide an example here, but a proof is causing Kani version 0.54 to panic with the message above and references the following line:

https://github.com/model-checking/kani/blob/e6f8a62d689d0b0ebcbabe3661be6273c5ab9be8/src/lib.rs#L156

There were no issues w/ version 0.53 or prior.

[jaisnan]

Hi @weaversa , is there any information about your invocation that you can provide that could help us reproduce this crash? Some details that would be useful are

1. The command that you invoked that caused the crash.
2. The OS that you are running the command on
3. Did verification fail or succeed before this crash?
4. Did you go through the setup process by running cargo-kani setup for example.

[weaversa]

Thank you @jaisnan --

1. cargo kani --output-format terse
2. Ubuntu 22.04
3. I see that Kani is Checking harness ... then Compiling ... and then thread 'main' panicked...
4. Kani is installed in the container via

    RUN curl https://sh.rustup.rs -sSf | bash -s -- -y \
     && cargo install --locked kani-verifier \
     && cargo kani setup
   

   I am using Kani in a CI job and many theorems are checked just fine. One in particular is now failing with version 0.54.0 with the panic message above.

[jaisnan]

Would it be possible to share a synthetic example that might have caused the crash?

[weaversa]

I'm sorry that I don't have such an example.

[celinval]

Hi @weaversa, sorry for the late reply. May I ask you to run kani with RUST_BACKTRACE and send us information about the stack trace you are getting (if any). Thanks!