diff --git a/tests/expected/attr-invariant/check_invariant/check_invariant.rs b/tests/expected/attr-invariant/check_invariant/check_invariant.rs
index 38e10a730b99..ffbeab5af619 100644
--- a/tests/expected/attr-invariant/check_invariant/check_invariant.rs
+++ b/tests/expected/attr-invariant/check_invariant/check_invariant.rs
@@ -1,7 +1,8 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-//! Check that Kani can automatically derive `Invariant` for structs with named fields.
+//! Check that the `kani::invariant` attribute is applied and the associated
+//! invariant can be checked through an `is_safe` call.
 
 extern crate kani;
 use kani::Invariant;
diff --git a/tests/ui/attr-invariant/invalid-pred-error/invalid-pred-error.rs b/tests/ui/attr-invariant/invalid-pred-error/invalid-pred-error.rs
index 7182a4cab3eb..0c69b7e76eb3 100644
--- a/tests/ui/attr-invariant/invalid-pred-error/invalid-pred-error.rs
+++ b/tests/ui/attr-invariant/invalid-pred-error/invalid-pred-error.rs
@@ -1,11 +1,14 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-//! Check that Kani can automatically derive `Invariant` for structs with named fields.
+//! Check that there is a compilation error when the predicate passed to
+//! `kani::invariant` attribute would result in a compiler error.
 
 extern crate kani;
 use kani::Invariant;
 
+// Note: The `x.is_safe() && y.is_safe()` requires `self` before each struct
+// field to be evaluated in the `is_safe` function body.
 #[derive(kani::Arbitrary)]
 #[kani::invariant(x.is_safe() && y.is_safe())]
 struct Point {
diff --git a/tests/ui/attr-invariant/no-struct-error/no-struct-error.rs b/tests/ui/attr-invariant/no-struct-error/no-struct-error.rs
index a01a2dc33d0d..6e317ce22ec8 100644
--- a/tests/ui/attr-invariant/no-struct-error/no-struct-error.rs
+++ b/tests/ui/attr-invariant/no-struct-error/no-struct-error.rs
@@ -1,7 +1,8 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-//! Check that Kani can automatically derive `Invariant` for structs with named fields.
+//! Check that Kani raises an error when the `kani::invariant` attribute is
+//! applied to items which is not a struct.
 
 extern crate kani;
 use kani::Invariant;