diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
index 96f757e22aeb..4b8a5751a28c 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
@@ -805,16 +805,15 @@ impl GotocCtx<'_, '_> {
     /// its primary argument and returns a tuple that contains:
     ///  * the previous value
     ///  * a boolean value indicating whether the operation was successful or not
-    ///
-    /// In a sequential context, the update is always sucessful so we assume the
-    /// second value to be true.
     /// -------------------------
     /// var = atomic_cxchg(var1, var2, var3)
     /// -------------------------
     /// unsigned char tmp;
+    /// bool success;
     /// tmp = *var1;
-    /// if (*var1 == var2) *var1 = var3;
-    /// var = (tmp, true);
+    /// success = (*var1 == var2);
+    /// if (success) *var1 = var3;
+    /// var = (tmp, success);
     /// -------------------------
     fn codegen_atomic_cxchg(
         &mut self,
@@ -830,16 +829,21 @@ impl GotocCtx<'_, '_> {
             self.decl_temp_variable(var1.typ().clone(), Some(var1.to_owned()), loc);
         let var2 = fargs.remove(0).with_location(loc);
         let var3 = fargs.remove(0).with_location(loc);
-        let eq_expr = (var1.clone()).eq(var2);
+        let eq_expr = var1.clone().eq(var2);
+        // Store the comparison result so we can use it both for the condition and the return value
+        let (success, success_decl) = self.decl_temp_variable(Type::bool(), Some(eq_expr), loc);
         let assign_stmt = var1.assign(var3, loc);
-        let cond_update_stmt = Stmt::if_then_else(eq_expr, assign_stmt, None, loc);
+        let cond_update_stmt = Stmt::if_then_else(success.clone(), assign_stmt, None, loc);
         let place_type = self.place_ty_stable(p);
         let res_type = self.codegen_ty_stable(place_type);
-        let tuple_expr =
-            Expr::struct_expr_from_values(res_type, vec![tmp, Expr::c_true()], &self.symbol_table)
-                .with_location(loc);
+        let tuple_expr = Expr::struct_expr_from_values(
+            res_type,
+            vec![tmp, success.cast_to(Type::c_bool())],
+            &self.symbol_table,
+        )
+        .with_location(loc);
         let res_stmt = self.codegen_expr_to_place_stable(p, tuple_expr, loc);
-        Stmt::atomic_block(vec![decl_stmt, cond_update_stmt, res_stmt], loc)
+        Stmt::atomic_block(vec![decl_stmt, success_decl, cond_update_stmt, res_stmt], loc)
     }
 
     /// An atomic store updates the value referenced in
diff --git a/tests/kani/Intrinsics/Atomic/Stable/CompareExchange/compare_exchange_failure.rs b/tests/kani/Intrinsics/Atomic/Stable/CompareExchange/compare_exchange_failure.rs
new file mode 100644
index 000000000000..dfb19d2c1dad
--- /dev/null
+++ b/tests/kani/Intrinsics/Atomic/Stable/CompareExchange/compare_exchange_failure.rs
@@ -0,0 +1,44 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Check that `compare_exchange` and `compare_exchange_weak` return `Err` when
+// the expected value doesn't match the current value.
+
+use std::sync::atomic::{AtomicU8, Ordering};
+
+#[kani::proof]
+fn check_compare_exchange_failure() {
+    // Create an atomic with initial value 0
+    let a = AtomicU8::new(0);
+
+    // Try to compare_exchange with expected value 1 (but current is 0)
+    // This should fail and return Err(0)
+    let result = a.compare_exchange(1, 2, Ordering::SeqCst, Ordering::SeqCst);
+    assert!(result == Err(0), "compare_exchange should return Err when expected doesn't match");
+
+    // The value should remain unchanged
+    assert!(
+        a.load(Ordering::SeqCst) == 0,
+        "value should remain unchanged after failed compare_exchange"
+    );
+}
+
+#[kani::proof]
+fn check_compare_exchange_weak_failure() {
+    // Create an atomic with initial value 0
+    let a = AtomicU8::new(0);
+
+    // Try to compare_exchange_weak with expected value 1 (but current is 0)
+    // This should fail and return Err(0)
+    let result = a.compare_exchange_weak(1, 2, Ordering::SeqCst, Ordering::SeqCst);
+    assert!(
+        result == Err(0),
+        "compare_exchange_weak should return Err when expected doesn't match"
+    );
+
+    // The value should remain unchanged
+    assert!(
+        a.load(Ordering::SeqCst) == 0,
+        "value should remain unchanged after failed compare_exchange_weak"
+    );
+}