diff --git a/cprover_bindings/src/goto_program/expr.rs b/cprover_bindings/src/goto_program/expr.rs
index ccd30771a6ac..91d26f3f65be 100644
--- a/cprover_bindings/src/goto_program/expr.rs
+++ b/cprover_bindings/src/goto_program/expr.rs
@@ -282,13 +282,33 @@ impl Expr {
             _ => false,
         }
     }
+
+    /// Returns whether an expression causes side effects or not
     pub fn is_side_effect(&self) -> bool {
-        match *self.value {
+        match &*self.value {
+            // These expressions always cause side effects
             Assign { .. }
             | FunctionCall { .. }
             | Nondet
             | SelfOp { .. }
             | StatementExpression { .. } => true,
+            // These expressions do not cause side effects, but the expressions
+            // they contain may do. All we need to do are recursive calls.
+            AddressOf(e) => e.is_side_effect(),
+            Array { elems } => elems.iter().any(|e| e.is_side_effect()),
+            ArrayOf { elem } => elem.is_side_effect(),
+            BinOp { op: _, lhs, rhs } => lhs.is_side_effect() || rhs.is_side_effect(),
+            ByteExtract { e, offset: _ } => e.is_side_effect(),
+            Dereference(e) => e.is_side_effect(),
+            If { c, t, e } => c.is_side_effect() || t.is_side_effect() || e.is_side_effect(),
+            Index { array, index } => array.is_side_effect() || index.is_side_effect(),
+            Member { lhs, field: _ } => lhs.is_side_effect(),
+            Struct { values } => values.iter().any(|e| e.is_side_effect()),
+            Typecast(e) => e.is_side_effect(),
+            Union { value, field: _ } => value.is_side_effect(),
+            UnOp { op: _, e } => e.is_side_effect(),
+            Vector { elems } => elems.iter().any(|e| e.is_side_effect()),
+            // The rest of expressions (constants) do not cause side effects
             _ => false,
         }
     }
@@ -1080,6 +1100,15 @@ impl Expr {
     pub fn r_ok(self, e: Expr) -> Expr {
         self.binop(ROk, e)
     }
+
+    // Expressions defined on top of other expressions
+
+    /// `min(self, e)`
+    pub fn min(self, e: Expr) -> Expr {
+        assert!(!self.is_side_effect() && !e.is_side_effect());
+        let cmp = self.clone().lt(e.clone());
+        cmp.ternary(self, e)
+    }
 }
 
 /// Constructors for self operations
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
index 56eff147616d..d65f4148fad8 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
@@ -412,6 +412,11 @@ impl<'tcx> GotocCtx<'tcx> {
             "atomic_load_acq" => self.codegen_atomic_load(intrinsic, fargs, p, loc),
             "atomic_load_relaxed" => self.codegen_atomic_load(intrinsic, fargs, p, loc),
             "atomic_load_unordered" => self.codegen_atomic_load(intrinsic, fargs, p, loc),
+            "atomic_min" => codegen_atomic_binop!(min),
+            "atomic_min_acq" => codegen_atomic_binop!(min),
+            "atomic_min_acqrel" => codegen_atomic_binop!(min),
+            "atomic_min_rel" => codegen_atomic_binop!(min),
+            "atomic_min_relaxed" => codegen_atomic_binop!(min),
             "atomic_nand" => codegen_atomic_binop!(bitnand),
             "atomic_nand_acq" => codegen_atomic_binop!(bitnand),
             "atomic_nand_acqrel" => codegen_atomic_binop!(bitnand),
@@ -430,6 +435,11 @@ impl<'tcx> GotocCtx<'tcx> {
             "atomic_store_rel" => self.codegen_atomic_store(intrinsic, fargs, p, loc),
             "atomic_store_relaxed" => self.codegen_atomic_store(intrinsic, fargs, p, loc),
             "atomic_store_unordered" => self.codegen_atomic_store(intrinsic, fargs, p, loc),
+            "atomic_umin" => codegen_atomic_binop!(min),
+            "atomic_umin_acq" => codegen_atomic_binop!(min),
+            "atomic_umin_acqrel" => codegen_atomic_binop!(min),
+            "atomic_umin_rel" => codegen_atomic_binop!(min),
+            "atomic_umin_relaxed" => codegen_atomic_binop!(min),
             "atomic_xadd" => codegen_atomic_binop!(plus),
             "atomic_xadd_acq" => codegen_atomic_binop!(plus),
             "atomic_xadd_acqrel" => codegen_atomic_binop!(plus),
diff --git a/tests/kani/Intrinsics/Atomic/Unstable/AtomicMin/main.rs b/tests/kani/Intrinsics/Atomic/Unstable/AtomicMin/main.rs
new file mode 100644
index 000000000000..0091bfb54209
--- /dev/null
+++ b/tests/kani/Intrinsics/Atomic/Unstable/AtomicMin/main.rs
@@ -0,0 +1,47 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Check that `atomic_min` and other variants (unstable version) return the
+// expected result.
+
+#![feature(core_intrinsics)]
+use std::intrinsics::{
+    atomic_min, atomic_min_acq, atomic_min_acqrel, atomic_min_rel, atomic_min_relaxed,
+};
+
+#[kani::proof]
+fn main() {
+    let mut a1 = 1 as u8;
+    let mut a2 = 1 as u8;
+    let mut a3 = 1 as u8;
+    let mut a4 = 1 as u8;
+    let mut a5 = 1 as u8;
+
+    let ptr_a1: *mut u8 = &mut a1;
+    let ptr_a2: *mut u8 = &mut a2;
+    let ptr_a3: *mut u8 = &mut a3;
+    let ptr_a4: *mut u8 = &mut a4;
+    let ptr_a5: *mut u8 = &mut a5;
+
+    let b = 0 as u8;
+
+    unsafe {
+        let x1 = atomic_min(ptr_a1, b);
+        let x2 = atomic_min_acq(ptr_a2, b);
+        let x3 = atomic_min_acqrel(ptr_a3, b);
+        let x4 = atomic_min_rel(ptr_a4, b);
+        let x5 = atomic_min_relaxed(ptr_a5, b);
+
+        assert!(x1 == 1);
+        assert!(x2 == 1);
+        assert!(x3 == 1);
+        assert!(x4 == 1);
+        assert!(x5 == 1);
+
+        assert!(*ptr_a1 == b);
+        assert!(*ptr_a2 == b);
+        assert!(*ptr_a3 == b);
+        assert!(*ptr_a4 == b);
+        assert!(*ptr_a5 == b);
+    }
+}
diff --git a/tests/kani/Intrinsics/Atomic/Unstable/AtomicMin/min.rs b/tests/kani/Intrinsics/Atomic/Unstable/AtomicMin/min.rs
deleted file mode 100644
index 01cbffcd1691..000000000000
--- a/tests/kani/Intrinsics/Atomic/Unstable/AtomicMin/min.rs
+++ /dev/null
@@ -1,22 +0,0 @@
-// Copyright Kani Contributors
-// SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-verify-fail
-
-// Check that `atomic_min` is not supported.
-
-#![feature(core_intrinsics)]
-use std::intrinsics::atomic_min;
-
-#[kani::proof]
-fn main() {
-    let mut a1 = 1 as u8;
-    let ptr_a1: *mut u8 = &mut a1;
-
-    let b = 0 as u8;
-
-    unsafe {
-        let x1 = atomic_min(ptr_a1, b);
-        assert!(x1 == 1);
-        assert!(*ptr_a1 == 0);
-    }
-}
diff --git a/tests/kani/Intrinsics/Atomic/Unstable/AtomicMin/min_acq.rs b/tests/kani/Intrinsics/Atomic/Unstable/AtomicMin/min_acq.rs
deleted file mode 100644
index 4ba23a1feba8..000000000000
--- a/tests/kani/Intrinsics/Atomic/Unstable/AtomicMin/min_acq.rs
+++ /dev/null
@@ -1,22 +0,0 @@
-// Copyright Kani Contributors
-// SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-verify-fail
-
-// Check that `atomic_min_acq` is not supported.
-
-#![feature(core_intrinsics)]
-use std::intrinsics::atomic_min_acq;
-
-#[kani::proof]
-fn main() {
-    let mut a1 = 1 as u8;
-    let ptr_a1: *mut u8 = &mut a1;
-
-    let b = 0 as u8;
-
-    unsafe {
-        let x1 = atomic_min_acq(ptr_a1, b);
-        assert!(x1 == 1);
-        assert!(*ptr_a1 == 0);
-    }
-}
diff --git a/tests/kani/Intrinsics/Atomic/Unstable/AtomicMin/min_acqrel.rs b/tests/kani/Intrinsics/Atomic/Unstable/AtomicMin/min_acqrel.rs
deleted file mode 100644
index f55028c3744a..000000000000
--- a/tests/kani/Intrinsics/Atomic/Unstable/AtomicMin/min_acqrel.rs
+++ /dev/null
@@ -1,22 +0,0 @@
-// Copyright Kani Contributors
-// SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-verify-fail
-
-// Check that `atomic_min_acqrel` is not supported.
-
-#![feature(core_intrinsics)]
-use std::intrinsics::atomic_min_acqrel;
-
-#[kani::proof]
-fn main() {
-    let mut a1 = 1 as u8;
-    let ptr_a1: *mut u8 = &mut a1;
-
-    let b = 0 as u8;
-
-    unsafe {
-        let x1 = atomic_min_acqrel(ptr_a1, b);
-        assert!(x1 == 1);
-        assert!(*ptr_a1 == 0);
-    }
-}
diff --git a/tests/kani/Intrinsics/Atomic/Unstable/AtomicMin/min_rel.rs b/tests/kani/Intrinsics/Atomic/Unstable/AtomicMin/min_rel.rs
deleted file mode 100644
index 8d77357e0693..000000000000
--- a/tests/kani/Intrinsics/Atomic/Unstable/AtomicMin/min_rel.rs
+++ /dev/null
@@ -1,22 +0,0 @@
-// Copyright Kani Contributors
-// SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-verify-fail
-
-// Check that `atomic_min_rel` is not supported.
-
-#![feature(core_intrinsics)]
-use std::intrinsics::atomic_min_rel;
-
-#[kani::proof]
-fn main() {
-    let mut a1 = 1 as u8;
-    let ptr_a1: *mut u8 = &mut a1;
-
-    let b = 0 as u8;
-
-    unsafe {
-        let x1 = atomic_min_rel(ptr_a1, b);
-        assert!(x1 == 1);
-        assert!(*ptr_a1 == 0);
-    }
-}
diff --git a/tests/kani/Intrinsics/Atomic/Unstable/AtomicMin/min_relaxed.rs b/tests/kani/Intrinsics/Atomic/Unstable/AtomicMin/min_relaxed.rs
deleted file mode 100644
index 5280818a5e0c..000000000000
--- a/tests/kani/Intrinsics/Atomic/Unstable/AtomicMin/min_relaxed.rs
+++ /dev/null
@@ -1,22 +0,0 @@
-// Copyright Kani Contributors
-// SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-verify-fail
-
-// Check that `atomic_min_relaxed` is not supported.
-
-#![feature(core_intrinsics)]
-use std::intrinsics::atomic_min_relaxed;
-
-#[kani::proof]
-fn main() {
-    let mut a1 = 1 as u8;
-    let ptr_a1: *mut u8 = &mut a1;
-
-    let b = 0 as u8;
-
-    unsafe {
-        let x1 = atomic_min_relaxed(ptr_a1, b);
-        assert!(x1 == 1);
-        assert!(*ptr_a1 == 0);
-    }
-}
diff --git a/tests/kani/Intrinsics/Atomic/Unstable/AtomicUmin/main.rs b/tests/kani/Intrinsics/Atomic/Unstable/AtomicUmin/main.rs
new file mode 100644
index 000000000000..032413a1b64c
--- /dev/null
+++ b/tests/kani/Intrinsics/Atomic/Unstable/AtomicUmin/main.rs
@@ -0,0 +1,47 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Check that `atomic_umin` and other variants (unstable version) return the
+// expected result.
+
+#![feature(core_intrinsics)]
+use std::intrinsics::{
+    atomic_umin, atomic_umin_acq, atomic_umin_acqrel, atomic_umin_rel, atomic_umin_relaxed,
+};
+
+#[kani::proof]
+fn main() {
+    let mut a1 = 1 as u8;
+    let mut a2 = 1 as u8;
+    let mut a3 = 1 as u8;
+    let mut a4 = 1 as u8;
+    let mut a5 = 1 as u8;
+
+    let ptr_a1: *mut u8 = &mut a1;
+    let ptr_a2: *mut u8 = &mut a2;
+    let ptr_a3: *mut u8 = &mut a3;
+    let ptr_a4: *mut u8 = &mut a4;
+    let ptr_a5: *mut u8 = &mut a5;
+
+    let b = 0 as u8;
+
+    unsafe {
+        let x1 = atomic_umin(ptr_a1, b);
+        let x2 = atomic_umin_acq(ptr_a2, b);
+        let x3 = atomic_umin_acqrel(ptr_a3, b);
+        let x4 = atomic_umin_rel(ptr_a4, b);
+        let x5 = atomic_umin_relaxed(ptr_a5, b);
+
+        assert!(x1 == 1);
+        assert!(x2 == 1);
+        assert!(x3 == 1);
+        assert!(x4 == 1);
+        assert!(x5 == 1);
+
+        assert!(*ptr_a1 == b);
+        assert!(*ptr_a2 == b);
+        assert!(*ptr_a3 == b);
+        assert!(*ptr_a4 == b);
+        assert!(*ptr_a5 == b);
+    }
+}
diff --git a/tests/kani/Intrinsics/Atomic/Unstable/AtomicUmin/umin.rs b/tests/kani/Intrinsics/Atomic/Unstable/AtomicUmin/umin.rs
deleted file mode 100644
index 84d3e85a7d64..000000000000
--- a/tests/kani/Intrinsics/Atomic/Unstable/AtomicUmin/umin.rs
+++ /dev/null
@@ -1,22 +0,0 @@
-// Copyright Kani Contributors
-// SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-verify-fail
-
-// Check that `atomic_umin` is not supported.
-
-#![feature(core_intrinsics)]
-use std::intrinsics::atomic_umin;
-
-#[kani::proof]
-fn main() {
-    let mut a1 = 1 as u8;
-    let ptr_a1: *mut u8 = &mut a1;
-
-    let b = 0 as u8;
-
-    unsafe {
-        let x1 = atomic_umin(ptr_a1, b);
-        assert!(x1 == 1);
-        assert!(*ptr_a1 == 0);
-    }
-}
diff --git a/tests/kani/Intrinsics/Atomic/Unstable/AtomicUmin/umin_acq.rs b/tests/kani/Intrinsics/Atomic/Unstable/AtomicUmin/umin_acq.rs
deleted file mode 100644
index 5a2f3f14455b..000000000000
--- a/tests/kani/Intrinsics/Atomic/Unstable/AtomicUmin/umin_acq.rs
+++ /dev/null
@@ -1,22 +0,0 @@
-// Copyright Kani Contributors
-// SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-verify-fail
-
-// Check that `atomic_umin_acq` is not supported.
-
-#![feature(core_intrinsics)]
-use std::intrinsics::atomic_umin_acq;
-
-#[kani::proof]
-fn main() {
-    let mut a1 = 1 as u8;
-    let ptr_a1: *mut u8 = &mut a1;
-
-    let b = 0 as u8;
-
-    unsafe {
-        let x1 = atomic_umin_acq(ptr_a1, b);
-        assert!(x1 == 1);
-        assert!(*ptr_a1 == 0);
-    }
-}
diff --git a/tests/kani/Intrinsics/Atomic/Unstable/AtomicUmin/umin_acqrel.rs b/tests/kani/Intrinsics/Atomic/Unstable/AtomicUmin/umin_acqrel.rs
deleted file mode 100644
index e4a4b6c0edab..000000000000
--- a/tests/kani/Intrinsics/Atomic/Unstable/AtomicUmin/umin_acqrel.rs
+++ /dev/null
@@ -1,22 +0,0 @@
-// Copyright Kani Contributors
-// SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-verify-fail
-
-// Check that `atomic_umin_acqrel` is not supported.
-
-#![feature(core_intrinsics)]
-use std::intrinsics::atomic_umin_acqrel;
-
-#[kani::proof]
-fn main() {
-    let mut a1 = 1 as u8;
-    let ptr_a1: *mut u8 = &mut a1;
-
-    let b = 0 as u8;
-
-    unsafe {
-        let x1 = atomic_umin_acqrel(ptr_a1, b);
-        assert!(x1 == 1);
-        assert!(*ptr_a1 == 0);
-    }
-}
diff --git a/tests/kani/Intrinsics/Atomic/Unstable/AtomicUmin/umin_rel.rs b/tests/kani/Intrinsics/Atomic/Unstable/AtomicUmin/umin_rel.rs
deleted file mode 100644
index 8411f65475e1..000000000000
--- a/tests/kani/Intrinsics/Atomic/Unstable/AtomicUmin/umin_rel.rs
+++ /dev/null
@@ -1,22 +0,0 @@
-// Copyright Kani Contributors
-// SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-verify-fail
-
-// Check that `atomic_umin_rel` is not supported.
-
-#![feature(core_intrinsics)]
-use std::intrinsics::atomic_umin_rel;
-
-#[kani::proof]
-fn main() {
-    let mut a1 = 1 as u8;
-    let ptr_a1: *mut u8 = &mut a1;
-
-    let b = 0 as u8;
-
-    unsafe {
-        let x1 = atomic_umin_rel(ptr_a1, b);
-        assert!(x1 == 1);
-        assert!(*ptr_a1 == 0);
-    }
-}
diff --git a/tests/kani/Intrinsics/Atomic/Unstable/AtomicUmin/umin_relaxed.rs b/tests/kani/Intrinsics/Atomic/Unstable/AtomicUmin/umin_relaxed.rs
deleted file mode 100644
index 6f9f23488dc7..000000000000
--- a/tests/kani/Intrinsics/Atomic/Unstable/AtomicUmin/umin_relaxed.rs
+++ /dev/null
@@ -1,22 +0,0 @@
-// Copyright Kani Contributors
-// SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-verify-fail
-
-// Check that `atomic_umin_relaxed` is not supported.
-
-#![feature(core_intrinsics)]
-use std::intrinsics::atomic_umin_relaxed;
-
-#[kani::proof]
-fn main() {
-    let mut a1 = 1 as u8;
-    let ptr_a1: *mut u8 = &mut a1;
-
-    let b = 0 as u8;
-
-    unsafe {
-        let x1 = atomic_umin_relaxed(ptr_a1, b);
-        assert!(x1 == 1);
-        assert!(*ptr_a1 == 0);
-    }
-}