From d70bfd8250f30a12c0147163eaecdd25441c3bb3 Mon Sep 17 00:00:00 2001
From: Ralf Anton Beier <ralf_beier@me.com>
Date: Wed, 29 Jul 2026 21:34:39 +0200
Subject: [PATCH] experiment(mutant-4): add() commutes operands (expect:
 survives, equivalent)

---
 tests/charon_llbc/src/lib.rs | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/tests/charon_llbc/src/lib.rs b/tests/charon_llbc/src/lib.rs
index eb40e9f..60300c2 100644
--- a/tests/charon_llbc/src/lib.rs
+++ b/tests/charon_llbc/src/lib.rs
@@ -1,9 +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 #4 (mutation-testing spike, rules_lean#23): operands commuted in
+//! `add`. Expect: SURVIVES, as an EQUIVALENT MUTANT (u32 addition is
+//! commutative) — control case to validate the bucketing methodology itself,
+//! not a real spec gap.
 
 pub fn add(x: u32, y: u32) -> u32 {
-    x + y
+    y + x
 }
 
 pub fn identity(x: u64) -> u64 {