From f27a5ed1426c705ec6faa181f080579b90983436 Mon Sep 17 00:00:00 2001
From: "Celina G. Val" <celinval@amazon.com>
Date: Thu, 15 Aug 2024 07:18:06 -0700
Subject: [PATCH] Add test related to issue 3432 (#3439)

In some cases, Kani would report a spurious counter example for cases
where a match arm contained more than one pattern. This was fixed by
changing how we handle storage lifecycle in #2995. This PR is only
adding the related test to the regression.

Resolves #3432

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
---
 tests/kani/Match/match_pattern.rs | 57 +++++++++++++++++++++++++++++++
 1 file changed, 57 insertions(+)
 create mode 100644 tests/kani/Match/match_pattern.rs

diff --git a/tests/kani/Match/match_pattern.rs b/tests/kani/Match/match_pattern.rs
new file mode 100644
index 000000000000..1b8689aee881
--- /dev/null
+++ b/tests/kani/Match/match_pattern.rs
@@ -0,0 +1,57 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//! Test that Kani can correctly handle match patterns joined with the `|` operator.
+//! It contains two equivalent methods that only differ by grouping march patterns.
+//! Kani used to only be able to verify one as reported in:
+//! <https://github.com/model-checking/kani/issues/3432>
+
+#[derive(Debug, Clone, Copy, PartialEq, Eq)]
+#[cfg_attr(kani, derive(kani::Arbitrary))]
+pub enum AbstractInt {
+    Bottom = 0,
+    Zero = 1,
+    Top = 2,
+}
+
+impl AbstractInt {
+    /// Code with exhausive match expression where each arm contains one pattern.
+    pub fn merge(self, other: Self) -> Self {
+        use AbstractInt::*;
+        match (self, other) {
+            (Bottom, x) => x,
+            (x, Bottom) => x,
+            (Zero, Zero) => Zero,
+            (Top, _) => Top,
+            (_, Top) => Top,
+        }
+    }
+
+    /// Code with exhausive match expression where an arm may contain multiple patterns.
+    pub fn merge_joined(self, other: Self) -> Self {
+        use AbstractInt::*;
+        match (self, other) {
+            (Bottom, x) | (x, Bottom) => x,
+            (Zero, Zero) => Zero,
+            (Top, _) | (_, Top) => Top,
+        }
+    }
+}
+
+#[cfg(kani)]
+mod test {
+    use super::*;
+
+    #[kani::proof]
+    fn merge_with_bottom() {
+        let x: AbstractInt = kani::any();
+        assert!(x.merge(AbstractInt::Bottom) == x);
+        assert!(AbstractInt::Bottom.merge(x) == x)
+    }
+
+    #[kani::proof]
+    fn check_equivalence() {
+        let x: AbstractInt = kani::any();
+        let y: AbstractInt = kani::any();
+        assert_eq!(x.merge(y), x.merge_joined(y));
+    }
+}