From ea33b426094652b25914628f16434007380e4323 Mon Sep 17 00:00:00 2001
From: Adrian Palacios <accorell@amazon.com>
Date: Tue, 9 Jul 2024 21:08:14 +0000
Subject: [PATCH] Add double-attr-invariant test

---
 .../double-attr-invariant.rs                    | 17 +++++++++++++++++
 .../double-attr-invariant/expected              |  6 ++++++
 2 files changed, 23 insertions(+)
 create mode 100644 tests/ui/attr-invariant/double-attr-invariant/double-attr-invariant.rs
 create mode 100644 tests/ui/attr-invariant/double-attr-invariant/expected

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`