diff --git a/tests/kani/BitManipulation/Stable/fixme_main.rs b/tests/kani/BitManipulation/Stable/fixme_main.rs
deleted file mode 100644
index 19b338a3dca0..000000000000
--- a/tests/kani/BitManipulation/Stable/fixme_main.rs
+++ /dev/null
@@ -1,15 +0,0 @@
-// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
-// SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-verify-fail
-
-fn main() {
-    // Intrinsics implemented as integer primitives
-    // https://doc.rust-lang.org/core/intrinsics/fn.cttz.html
-    // https://doc.rust-lang.org/core/intrinsics/fn.ctlz.html
-    let x = 0b0011_1000_u8;
-    let num_trailing = x.trailing_zeros();
-    let num_leading = x.leading_zeros();
-
-    assert!(num_trailing == 3); // fails because of https://github.com/model-checking/kani/issues/26
-    assert!(num_leading == 2);
-}
diff --git a/tests/kani/BitManipulation/Unstable/fixme_main.rs b/tests/kani/BitManipulation/Unstable/fixme_main.rs
deleted file mode 100644
index 7fed5c91b4b1..000000000000
--- a/tests/kani/BitManipulation/Unstable/fixme_main.rs
+++ /dev/null
@@ -1,25 +0,0 @@
-// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
-// SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-verify-fail
-
-#![feature(core_intrinsics)]
-use std::intrinsics::{ctlz, cttz, cttz_nonzero};
-
-fn main() {
-    let v8 = 0b0011_1000_u8;
-    let v16 = 0b0011_1000_0000_0000_u16;
-    let v32 = 0b0011_1000_0000_0000_0000_0000_0000_0000_u32;
-
-    let nttz8 = cttz(v8);
-    let nttz16 = cttz(v16);
-    let nttz32 = unsafe { cttz_nonzero(v32) };
-    let num_leading = ctlz(v8);
-    let num_trailing_nz = unsafe { cttz_nonzero(v8) };
-
-    // fail because of https://github.com/model-checking/kani/issues/26
-    assert!(nttz8 == 3);
-    assert!(nttz16 == 11);
-    assert!(nttz32 == 27);
-    assert!(num_trailing_nz == 3);
-    assert!(num_leading == 2);
-}
diff --git a/tests/kani/Intrinsics/Count/ctlz.rs b/tests/kani/Intrinsics/Count/ctlz.rs
new file mode 100644
index 000000000000..ab6117ff1d8d
--- /dev/null
+++ b/tests/kani/Intrinsics/Count/ctlz.rs
@@ -0,0 +1,67 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Check that `ctlz` and `ctlz_nonzero` are supported and return the expected
+// results
+
+#![feature(core_intrinsics)]
+use std::intrinsics::{ctlz, ctlz_nonzero};
+
+// Define a function for counting like `ctlz` and assert that their results are
+// the same for any value
+macro_rules! test_ctlz {
+    ( $fn_name:ident, $ty:ty ) => {
+        fn $fn_name(x: $ty) -> $ty {
+            let mut count = 0;
+            let num_bits = <$ty>::BITS;
+            for i in 0..num_bits {
+                // Get value at index `i`
+                let bitmask = 1 << (num_bits - i - 1);
+                let bit = x & bitmask;
+                if bit == 0 {
+                    count += 1;
+                } else {
+                    break;
+                }
+            }
+            count
+        }
+        let var: $ty = kani::any();
+        // Check that the result is correct
+        assert!($fn_name(var) == ctlz(var));
+        // Check that the stable version returns the same value
+        assert!(ctlz(var) as u32 == var.leading_zeros());
+    };
+}
+
+// Assert that the results of `ctlz` and `ctlz_nonzero` are the same if we
+// exclude zero
+macro_rules! test_ctlz_nonzero {
+    ($ty:ty) => {
+        let var_nonzero: $ty = kani::any();
+        kani::assume(var_nonzero != 0);
+        unsafe {
+            assert!(ctlz(var_nonzero) == ctlz_nonzero(var_nonzero));
+        }
+    };
+}
+
+fn main() {
+    test_ctlz!(my_ctlz_u8, u8);
+    test_ctlz!(my_ctlz_u16, u16);
+    test_ctlz!(my_ctlz_u32, u32);
+    test_ctlz!(my_ctlz_u64, u64);
+    test_ctlz!(my_ctlz_u128, u128);
+    test_ctlz!(my_ctlz_usize, usize);
+    test_ctlz_nonzero!(u8);
+    test_ctlz_nonzero!(u16);
+    test_ctlz_nonzero!(u32);
+    test_ctlz_nonzero!(u64);
+    test_ctlz_nonzero!(u128);
+    test_ctlz_nonzero!(usize);
+    // These intrinsics are also defined for signed integer types by casting the
+    // number into the corresponding unsigned type and then casting the result
+    // into the original signed type. This causes overflows unless we restrict
+    // their values, making the signed versions not very interesting to test
+    // here.
+}
diff --git a/tests/kani/Intrinsics/Count/ctlz_nonzero_panic.rs b/tests/kani/Intrinsics/Count/ctlz_nonzero_panic.rs
new file mode 100644
index 000000000000..e8211e33e8bf
--- /dev/null
+++ b/tests/kani/Intrinsics/Count/ctlz_nonzero_panic.rs
@@ -0,0 +1,25 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-verify-fail
+
+// Check that `ctlz_nonzero` fails if zero is passed as an argument
+
+#![feature(core_intrinsics)]
+use std::intrinsics::ctlz_nonzero;
+
+// Call `ctlz_nonzero` with an unconstrained symbolic argument
+macro_rules! test_ctlz_nonzero {
+    ($ty:ty) => {
+        let var_nonzero: $ty = kani::any();
+        let _ = unsafe { ctlz_nonzero(var_nonzero) };
+    };
+}
+
+fn main() {
+    test_ctlz_nonzero!(u8);
+    test_ctlz_nonzero!(u16);
+    test_ctlz_nonzero!(u32);
+    test_ctlz_nonzero!(u64);
+    test_ctlz_nonzero!(u128);
+    test_ctlz_nonzero!(usize);
+}
diff --git a/tests/kani/Intrinsics/Count/cttz.rs b/tests/kani/Intrinsics/Count/cttz.rs
new file mode 100644
index 000000000000..35a56603347c
--- /dev/null
+++ b/tests/kani/Intrinsics/Count/cttz.rs
@@ -0,0 +1,70 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Check that `cttz` and `cttz_nonzero` are supported and return the expected
+// results
+
+#![feature(core_intrinsics)]
+use std::intrinsics::{cttz, cttz_nonzero};
+
+// Define a function for counting like `cttz` and assert that their results are
+// the same for any value
+macro_rules! test_cttz {
+    ( $fn_name:ident, $ty:ty ) => {
+        fn $fn_name(x: $ty) -> $ty {
+            let mut count = 0;
+            let num_bits = <$ty>::BITS;
+            for i in 0..num_bits {
+                // Get value at index `i`
+                let bitmask = 1 << i;
+                let bit = x & bitmask;
+                if bit == 0 {
+                    count += 1;
+                } else {
+                    break;
+                }
+            }
+            count
+        }
+        let var: $ty = kani::any();
+        // FIXME: Remove the assumption below when CBMC returns the correct value for 0
+        // https://github.com/model-checking/kani/issues/881
+        kani::assume(var != 0);
+        // Check that the result is correct
+        assert!($fn_name(var) == cttz(var));
+        // Check that the stable version returns the same value
+        assert!(cttz(var) as u32 == var.trailing_zeros());
+    };
+}
+
+// Assert that the results of `cttz` and `cttz_nonzero` are the same if we
+// exclude zero
+macro_rules! test_cttz_nonzero {
+    ($ty:ty) => {
+        let var_nonzero: $ty = kani::any();
+        kani::assume(var_nonzero != 0);
+        unsafe {
+            assert!(cttz(var_nonzero) == cttz_nonzero(var_nonzero));
+        }
+    };
+}
+
+fn main() {
+    test_cttz!(my_cttz_u8, u8);
+    test_cttz!(my_cttz_u16, u16);
+    test_cttz!(my_cttz_u32, u32);
+    test_cttz!(my_cttz_u64, u64);
+    test_cttz!(my_cttz_u128, u128);
+    test_cttz!(my_cttz_usize, usize);
+    test_cttz_nonzero!(u8);
+    test_cttz_nonzero!(u16);
+    test_cttz_nonzero!(u32);
+    test_cttz_nonzero!(u64);
+    test_cttz_nonzero!(u128);
+    test_cttz_nonzero!(usize);
+    // These intrinsics are also defined for signed integer types by casting the
+    // number into the corresponding unsigned type and then casting the result
+    // into the original signed type. This causes overflows unless we restrict
+    // their values, making the signed versions not very interesting to test
+    // here.
+}
diff --git a/tests/kani/Intrinsics/Count/cttz_nonzero_panic.rs b/tests/kani/Intrinsics/Count/cttz_nonzero_panic.rs
new file mode 100644
index 000000000000..710758673fe0
--- /dev/null
+++ b/tests/kani/Intrinsics/Count/cttz_nonzero_panic.rs
@@ -0,0 +1,25 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-verify-fail
+
+// Check that `cttz_nonzero` fails if zero is passed as an argument
+
+#![feature(core_intrinsics)]
+use std::intrinsics::cttz_nonzero;
+
+// Call `cttz_nonzero` with an unconstrained symbolic argument
+macro_rules! test_cttz_nonzero {
+    ($ty:ty) => {
+        let var_nonzero: $ty = kani::any();
+        let _ = unsafe { cttz_nonzero(var_nonzero) };
+    };
+}
+
+fn main() {
+    test_cttz_nonzero!(u8);
+    test_cttz_nonzero!(u16);
+    test_cttz_nonzero!(u32);
+    test_cttz_nonzero!(u64);
+    test_cttz_nonzero!(u128);
+    test_cttz_nonzero!(usize);
+}