diff --git a/tests/ui/fail-uncoverable/all-covered/test.rs b/tests/ui/fail-uncoverable/all-covered/test.rs index a9f5be67aa66..2708c2870590 100644 --- a/tests/ui/fail-uncoverable/all-covered/test.rs +++ b/tests/ui/fail-uncoverable/all-covered/test.rs @@ -2,8 +2,8 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT // kani-flags: --enable-unstable --fail-uncoverable -//! Checks that all cover statements are satisfied and `--fail-uncoverable` -//! doesn't cause failures. +//! Checks that all cover statements are satisfied and enabling +//! `--fail-uncoverable` doesn't cause unexpected failures. #[kani::proof] fn harness1() { diff --git a/tests/ui/fail-uncoverable/uncoverable/test.rs b/tests/ui/fail-uncoverable/uncoverable/test.rs index 386f5bf45ad3..dfde7f6eedb3 100644 --- a/tests/ui/fail-uncoverable/uncoverable/test.rs +++ b/tests/ui/fail-uncoverable/uncoverable/test.rs @@ -2,8 +2,10 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT // kani-flags: --enable-unstable --fail-uncoverable -//! Checks that the `--fail-uncoverable` option causes a failure due to a cover -//! statement not being covered. +//! Checks that enabling the `--fail-uncoverable` option triggers a +//! condition-based failure due to a `cover` statement not being satisfied. +//! +//! Note: The `cover` statement isn't satisfied because it's unreachable. #[kani::proof] fn harness_uncoverable() { diff --git a/tests/ui/fail-uncoverable/unsatisfied/test.rs b/tests/ui/fail-uncoverable/unsatisfied/test.rs index e79b426c9426..a8e2bb689510 100644 --- a/tests/ui/fail-uncoverable/unsatisfied/test.rs +++ b/tests/ui/fail-uncoverable/unsatisfied/test.rs @@ -2,8 +2,11 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT // kani-flags: --enable-unstable --fail-uncoverable -//! Checks that the `--fail-uncoverable` option causes a failure due to a cover -//! statement not being satisfied. +//! Checks that enabling the `--fail-uncoverable` option triggers a +//! condition-based failure due to a `cover` statement not being satisfied. +//! +//! Note: The `cover` statement isn't satisfied because the condition `x == -1` +//! cannot be satisfied. #[kani::proof] fn harness_unsatisfied() {