From d556fe7dfad5473761b7c13a7848ce7d887d30ff Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 11 Feb 2026 13:41:54 +0000 Subject: [PATCH 1/2] Fix CBMC output parser panic when using SMT solvers 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 --- kani-driver/src/call_cbmc.rs | 7 +++++++ kani-driver/src/cbmc_output_parser.rs | 3 +++ kani-driver/src/cbmc_property_renderer.rs | 1 + tests/expected/smt-solver-error-status/expected | 2 ++ tests/expected/smt-solver-error-status/test.rs | 13 +++++++++++++ tools/kani-cov/src/coverage.rs | 3 +++ 6 files changed, 29 insertions(+) create mode 100644 tests/expected/smt-solver-error-status/expected create mode 100644 tests/expected/smt-solver-error-status/test.rs diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs index 3eeede9f68e4..4728c2064de6 100644 --- a/kani-driver/src/call_cbmc.rs +++ b/kani-driver/src/call_cbmc.rs @@ -46,6 +46,8 @@ pub enum FailedProperties { PanicsOnly, // One or more failures that aren't panic-related Other, + // One or more properties resulted in an ERROR rather than a failing/successful verification + Error, } /// The possible CBMC exit statuses @@ -440,11 +442,13 @@ fn verification_outcome_from_properties( let failed_properties = determine_failed_properties(properties); let status = if should_panic { match failed_properties { + FailedProperties::Error => VerificationStatus::Failure, FailedProperties::None | FailedProperties::Other => VerificationStatus::Failure, FailedProperties::PanicsOnly => VerificationStatus::Success, } } else { match failed_properties { + FailedProperties::Error => VerificationStatus::Failure, FailedProperties::None => VerificationStatus::Success, FailedProperties::PanicsOnly | FailedProperties::Other => VerificationStatus::Failure, } @@ -454,6 +458,9 @@ fn verification_outcome_from_properties( /// Determines the `FailedProperties` variant that corresponds to an array of properties fn determine_failed_properties(properties: &[Property]) -> FailedProperties { + if properties.iter().any(|prop| prop.status == CheckStatus::Error) { + return FailedProperties::Error; + }; let failed_properties: Vec<&Property> = properties.iter().filter(|prop| prop.status == CheckStatus::Failure).collect(); // Return `FAILURE` if there isn't at least one failed property diff --git a/kani-driver/src/cbmc_output_parser.rs b/kani-driver/src/cbmc_output_parser.rs index 749bb9abec1e..686ced189311 100644 --- a/kani-driver/src/cbmc_output_parser.rs +++ b/kani-driver/src/cbmc_output_parser.rs @@ -341,6 +341,7 @@ pub enum CheckStatus { Unreachable, Uncovered, // for `code_coverage` properties only Unsatisfiable, // for `cover` properties only + Error, // returned by CBMC when using SMT solvers } impl std::fmt::Display for CheckStatus { @@ -357,6 +358,8 @@ impl std::fmt::Display for CheckStatus { // impossible to definitively conclude whether other properties hold or not. CheckStatus::Unknown => style("UNDETERMINED").yellow(), CheckStatus::Unsatisfiable => style("UNSATISFIABLE").yellow(), + // CBMC returns ERROR when using SMT solvers and the solver encounters an error. + CheckStatus::Error => style("ERROR").red(), }; write!(f, "{check_str}") } diff --git a/kani-driver/src/cbmc_property_renderer.rs b/kani-driver/src/cbmc_property_renderer.rs index a64562d51162..3506910ce43e 100644 --- a/kani-driver/src/cbmc_property_renderer.rs +++ b/kani-driver/src/cbmc_property_renderer.rs @@ -395,6 +395,7 @@ pub fn format_result( FailedProperties::Other => { " (encountered failures other than panics, which were unexpected)" } + FailedProperties::Error => " (encountered a solver error)", } } else { "" diff --git a/tests/expected/smt-solver-error-status/expected b/tests/expected/smt-solver-error-status/expected new file mode 100644 index 000000000000..1ab893adb188 --- /dev/null +++ b/tests/expected/smt-solver-error-status/expected @@ -0,0 +1,2 @@ +Running SMT2 QF_AUFBV using Z3 +VERIFICATION:- FAILED diff --git a/tests/expected/smt-solver-error-status/test.rs b/tests/expected/smt-solver-error-status/test.rs new file mode 100644 index 000000000000..c0c1f3d7f396 --- /dev/null +++ b/tests/expected/smt-solver-error-status/test.rs @@ -0,0 +1,13 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Regression test for issue #4519. +//! Ensures that Kani properly handles the ERROR status returned by CBMC +//! when using SMT solvers (z3, bitwuzla, cvc5) instead of panicking with: +//! "unknown variant `ERROR`, expected one of `FAILURE`, `COVERED`, ..." + +#[kani::proof] +#[kani::solver(bitwuzla)] +pub fn check_smt_solver_error_status() { + assert!(false); +} diff --git a/tools/kani-cov/src/coverage.rs b/tools/kani-cov/src/coverage.rs index 0898010ea2d0..88f13d5c1995 100644 --- a/tools/kani-cov/src/coverage.rs +++ b/tools/kani-cov/src/coverage.rs @@ -33,6 +33,7 @@ pub enum CheckStatus { Unreachable, Uncovered, // for `code_coverage` properties only Unsatisfiable, // for `cover` properties only + Error, // returned by CBMC when using SMT solvers } /// Kani coverage check. @@ -60,6 +61,8 @@ impl std::fmt::Display for CheckStatus { CheckStatus::Unreachable => style("UNREACHABLE").yellow(), CheckStatus::Undetermined => style("UNDETERMINED").yellow(), CheckStatus::Unsatisfiable => style("UNSATISFIABLE").yellow(), + // CBMC returns ERROR when using SMT solvers and the solver encounters an error. + CheckStatus::Error => style("ERROR").red(), }; write!(f, "{check_str}") } From f9d590ef15682d5ba28e297e61478c8d2902459c Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 11 Feb 2026 15:27:24 +0100 Subject: [PATCH 2/2] Update tests/expected/smt-solver-error-status/expected Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com> --- tests/expected/smt-solver-error-status/expected | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/expected/smt-solver-error-status/expected b/tests/expected/smt-solver-error-status/expected index 1ab893adb188..4f88f34e76a2 100644 --- a/tests/expected/smt-solver-error-status/expected +++ b/tests/expected/smt-solver-error-status/expected @@ -1,2 +1,2 @@ -Running SMT2 QF_AUFBV using Z3 +Running SMT2 QF_AUFBV (with FPA) using Bitwuzla VERIFICATION:- FAILED