diff --git a/library/kani_macros/src/sysroot/contracts/bootstrap.rs b/library/kani_macros/src/sysroot/contracts/bootstrap.rs
index 7c35cc469254..6a48bab08070 100644
--- a/library/kani_macros/src/sysroot/contracts/bootstrap.rs
+++ b/library/kani_macros/src/sysroot/contracts/bootstrap.rs
@@ -85,7 +85,7 @@ impl<'a> ContractConditionsHandler<'a> {
 
         let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site());
         self.output.extend(quote!(
-            #[allow(dead_code, unused_variables)]
+            #[allow(dead_code, unused_variables, unused_mut)]
             #[kanitool::is_contract_generated(recursion_wrapper)]
             #wrapper_sig {
                 static mut REENTRY: bool = false;
diff --git a/library/kani_macros/src/sysroot/contracts/shared.rs b/library/kani_macros/src/sysroot/contracts/shared.rs
index b0f5804824ad..b0d323b12ca3 100644
--- a/library/kani_macros/src/sysroot/contracts/shared.rs
+++ b/library/kani_macros/src/sysroot/contracts/shared.rs
@@ -50,7 +50,7 @@ impl<'a> ContractConditionsHandler<'a> {
     pub fn emit_common_header(&mut self) {
         if self.function_state.emit_tag_attr() {
             self.output.extend(quote!(
-                #[allow(dead_code, unused_variables)]
+                #[allow(dead_code, unused_variables, unused_mut)]
             ));
         }
         self.output.extend(self.annotated_fn.attrs.iter().flat_map(Attribute::to_token_stream));
diff --git a/tests/expected/function-contract/gcd_success.rs b/tests/expected/function-contract/gcd_success.rs
index 3b983a230b60..61d8fea8ec80 100644
--- a/tests/expected/function-contract/gcd_success.rs
+++ b/tests/expected/function-contract/gcd_success.rs
@@ -1,28 +1,22 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // kani-flags: -Zfunction-contracts
+#![deny(warnings)]
 type T = u8;
 
 /// Euclid's algorithm for calculating the GCD of two numbers
 #[kani::requires(x != 0 && y != 0)]
 #[kani::ensures(|result : &T| *result != 0 && x % *result == 0 && y % *result == 0)]
-fn gcd(x: T, y: T) -> T {
-    let mut max = x;
-    let mut min = y;
-    if min > max {
-        let val = max;
-        max = min;
-        min = val;
-    }
-
+fn gcd(mut x: T, mut y: T) -> T {
+    (x, y) = (if x > y { x } else { y }, if x > y { y } else { x });
     loop {
-        let res = max % min;
+        let res = x % y;
         if res == 0 {
-            return min;
+            return y;
         }
 
-        max = min;
-        min = res;
+        x = y;
+        y = res;
     }
 }