From 12ecc4b5d7b6f99790bb4460106b823d4b477e4c Mon Sep 17 00:00:00 2001
From: Adrian Palacios <accorell@amazon.com>
Date: Wed, 10 Jan 2024 23:09:17 +0000
Subject: [PATCH] Minor improvements in test descriptions

---
 tests/ui/fail-uncoverable/all-covered/test.rs | 4 ++--
 tests/ui/fail-uncoverable/uncoverable/test.rs | 6 ++++--
 tests/ui/fail-uncoverable/unsatisfied/test.rs | 7 +++++--
 3 files changed, 11 insertions(+), 6 deletions(-)

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() {