Add another test

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());
+}

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