diff --git a/tests/ui/attr-invariant/double-attr-invariant/double-attr-invariant.rs b/tests/ui/attr-invariant/double-attr-invariant/double-attr-invariant.rs
new file mode 100644
index 000000000000..2782ad8280a7
--- /dev/null
+++ b/tests/ui/attr-invariant/double-attr-invariant/double-attr-invariant.rs
@@ -0,0 +1,17 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! 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 struct fields `x` and `y` are references in this context, we should
+// refer to `*x` and `*y` instead.
+#[kani::invariant(*x >= 0)]
+#[kani::invariant(*y >= 0)]
+struct Point {
+    x: i32,
+    y: i32,
+}
diff --git a/tests/ui/attr-invariant/double-attr-invariant/expected b/tests/ui/attr-invariant/double-attr-invariant/expected
new file mode 100644
index 000000000000..9817b2bea1e2
--- /dev/null
+++ b/tests/ui/attr-invariant/double-attr-invariant/expected
@@ -0,0 +1,6 @@
+error[E0119]: conflicting implementations of trait `kani::Invariant` for type `Point`
+   |
+12 | #[kani::invariant(*x >= 0)]
+   | --------------------------- first implementation here
+13 | #[kani::invariant(*y >= 0)]
+   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^ conflicting implementation for `Point`