From 3c1a2df2308a1f4ce288e08afd52e387d6084465 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 29 Jul 2026 21:34:28 +0200 Subject: [PATCH] experiment(mutant-3): identity() returns x+1 instead of x (expect: killed) --- tests/charon_llbc/src/lib.rs | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/tests/charon_llbc/src/lib.rs b/tests/charon_llbc/src/lib.rs index eb40e9f..d030903 100644 --- a/tests/charon_llbc/src/lib.rs +++ b/tests/charon_llbc/src/lib.rs @@ -1,11 +1,14 @@ //! 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 #3 (mutation-testing spike, rules_lean#23): `identity` adds a +//! constant. Expect: KILLED — identity.spec requires y = x exactly. pub fn add(x: u32, y: u32) -> u32 { x + y } pub fn identity(x: u64) -> u64 { - x + x + 1 }