diff --git a/tests/charon_llbc/src/lib.rs b/tests/charon_llbc/src/lib.rs index eb40e9f..b5193b4 100644 --- a/tests/charon_llbc/src/lib.rs +++ b/tests/charon_llbc/src/lib.rs @@ -1,9 +1,13 @@ //! Minimal Rust crate used to smoke-test the charon_llbc Bazel rule. //! Kept deliberately small: `charon rustc --preset=aeneas` should translate //! this without hitting any unsupported features. +//! +//! MUTANT #2 (mutation-testing spike, rules_lean#23): `add` drops the `y` +//! term entirely. Expect: KILLED — add.spec requires z.val = x.val + y.val. pub fn add(x: u32, y: u32) -> u32 { - x + y + let _ = y; + x } pub fn identity(x: u64) -> u64 {