Fix CBMC output parser panic when using SMT solvers

[tautschnig]

Add Error variant to CheckStatus enum to handle the ERROR status returned by CBMC when using SMT solvers (z3, bitwuzla, cvc5). Previously this caused a deserialization panic.

Resolves #4519

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[Copilot]

Pull request overview

This PR fixes a panic in the CBMC output parser when using SMT solvers (z3, bitwuzla, cvc5) by adding a new Error variant to the CheckStatus enum. When SMT solvers encounter errors, CBMC returns an "ERROR" status that was not previously handled, causing deserialization to panic.

Changes:

• Added Error variant to CheckStatus enum in both kani-driver and kani-cov modules
• Added Error variant to FailedProperties enum and updated verification logic to treat ERROR status as a verification failure
• Added regression test to ensure ERROR status is properly handled

Reviewed changes

Copilot reviewed 6 out of 6 changed files in this pull request and generated 1 comment.

Show a summary per file

File	Description
kani-driver/src/cbmc_output_parser.rs	Added Error variant to CheckStatus enum with appropriate display formatting (red color)
tools/kani-cov/src/coverage.rs	Added Error variant to CheckStatus enum (duplicate maintained for issue #3541) with matching display implementation
kani-driver/src/call_cbmc.rs	Added Error variant to FailedProperties enum and updated logic to prioritize ERROR status and treat it as verification failure
kani-driver/src/cbmc_property_renderer.rs	Added message for solver errors in should_panic case
tests/expected/smt-solver-error-status/test.rs	Added regression test using bitwuzla solver with failing assertion
tests/expected/smt-solver-error-status/expected	Added expected output pattern for the regression test

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.