From cdf13e8f1bae5f5ccb6733e2305457324f5f8149 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Mon, 4 Dec 2023 22:59:55 +0000
Subject: [PATCH] Revert "Also drop unit test of our stub that uses ToBitMask"

This reverts commit ba6b95e20b3e3add97d9c40a1462f5524a7ae6f5.
---
 library/kani/src/models/mod.rs | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

diff --git a/library/kani/src/models/mod.rs b/library/kani/src/models/mod.rs
index e44323f355cb..8b3f771756dc 100644
--- a/library/kani/src/models/mod.rs
+++ b/library/kani/src/models/mod.rs
@@ -184,6 +184,20 @@ mod test {
         check_bitmask::<_, [u8; 9], i128, 70>(CustomMask([-1i128; 70]));
     }
 
+    /// Compare the value returned by our model and the portable simd representation.
+    fn check_portable_bitmask<T, E, const LANES: usize>(mask: T)
+    where
+        T: ToBitMask + Clone,
+        T::BitMask: Debug + PartialEq,
+        E: kani_intrinsic::MaskElement,
+        [u8; kani_intrinsic::mask_len(LANES)]: Sized,
+    {
+        assert_eq!(
+            unsafe { kani_intrinsic::simd_bitmask::<_, T::BitMask, E, LANES>(mask.clone()) },
+            mask.to_bitmask()
+        );
+    }
+
     /// Compare the value returned by our model and the simd_bitmask intrinsic.
     fn check_bitmask<T, U, E, const LANES: usize>(mask: T)
     where