Fix CBMC output parser panic when using SMT solvers

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

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}")
     }

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 {
         ""

tests/expected/smt-solver-error-status/expected

@@ -0,0 +1,2 @@
+Running SMT2 QF_AUFBV (with FPA) using Bitwuzla
+VERIFICATION:- FAILED

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);
+}

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}")
     }