From 087b22b4a88db26a94b7940ac0d0daba8ab13710 Mon Sep 17 00:00:00 2001
From: Adrian Palacios <accorell@amazon.com>
Date: Tue, 9 Jul 2024 21:35:11 +0000
Subject: [PATCH] Add another test

---
 .../check_arbitrary/check_arbitrary.rs        | 23 +++++++++++++++++++
 .../attr-invariant/check_arbitrary/expected   | 11 +++++++++
 2 files changed, 34 insertions(+)
 create mode 100644 tests/expected/attr-invariant/check_arbitrary/check_arbitrary.rs
 create mode 100644 tests/expected/attr-invariant/check_arbitrary/expected

diff --git a/tests/expected/attr-invariant/check_arbitrary/check_arbitrary.rs b/tests/expected/attr-invariant/check_arbitrary/check_arbitrary.rs
new file mode 100644
index 000000000000..8c59f2cc1701
--- /dev/null
+++ b/tests/expected/attr-invariant/check_arbitrary/check_arbitrary.rs
@@ -0,0 +1,23 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Check that the `kani::invariant` attribute automatically generates the
+//! `Arbitrary` implementation, and also that the values it generates respect
+//! the type invariant.
+
+extern crate kani;
+use kani::Invariant;
+
+#[kani::invariant(*x >= 0 && *y >= 0)]
+struct Point {
+    x: i32,
+    y: i32,
+}
+
+#[kani::proof]
+fn check_arbitrary() {
+    let point: Point = kani::any();
+    assert!(point.x >= 0);
+    assert!(point.y >= 0);
+    assert!(point.is_safe());
+}
diff --git a/tests/expected/attr-invariant/check_arbitrary/expected b/tests/expected/attr-invariant/check_arbitrary/expected
new file mode 100644
index 000000000000..ee1e13bb726d
--- /dev/null
+++ b/tests/expected/attr-invariant/check_arbitrary/expected
@@ -0,0 +1,11 @@
+Check 1: check_arbitrary.assertion.1\
+         - Status: SUCCESS\
+         - Description: "assertion failed: point.x >= 0"
+
+Check 2: check_arbitrary.assertion.2\
+         - Status: SUCCESS\
+         - Description: "assertion failed: point.y >= 0"
+
+Check 3: check_arbitrary.assertion.3\
+         - Status: SUCCESS\
+         - Description: "assertion failed: point.is_safe()"