diff --git a/kani-compiler/src/codegen_cprover_gotoc/archive.rs b/kani-compiler/src/codegen_cprover_gotoc/archive.rs
index ae865cf86086..53df0135766d 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/archive.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/archive.rs
@@ -44,47 +44,16 @@ pub(crate) struct ArArchiveBuilder<'a> {
 }
 
 impl<'a> ArchiveBuilder<'a> for ArArchiveBuilder<'a> {
-    fn new(sess: &'a Session, output: &Path, input: Option<&Path>) -> Self {
-        let (src_archives, entries) = if let Some(input) = input {
-            let read_cache = ReadCache::new(File::open(input).unwrap());
-            let archive = ArchiveFile::parse(&read_cache).unwrap();
-            let mut entries = Vec::new();
-
-            for entry in archive.members() {
-                let entry = entry.unwrap();
-                entries.push((
-                    entry.name().to_vec(),
-                    ArchiveEntry::FromArchive { archive_index: 0, file_range: entry.file_range() },
-                ));
-            }
-
-            (vec![read_cache.into_inner()], entries)
-        } else {
-            (vec![], Vec::new())
-        };
-
+    fn new(sess: &'a Session, output: &Path) -> Self {
         ArArchiveBuilder {
             sess,
             dst: output.to_path_buf(),
             use_gnu_style_archive: sess.target.archive_format == "gnu",
-            src_archives,
-            entries,
+            src_archives: vec![],
+            entries: vec![],
         }
     }
 
-    fn src_files(&mut self) -> Vec<String> {
-        self.entries.iter().map(|(name, _)| String::from_utf8(name.clone()).unwrap()).collect()
-    }
-
-    fn remove_file(&mut self, name: &str) {
-        let index = self
-            .entries
-            .iter()
-            .position(|(entry_name, _)| entry_name == name.as_bytes())
-            .expect("Tried to remove file not existing in src archive");
-        self.entries.remove(index);
-    }
-
     fn add_file(&mut self, file: &Path) {
         self.entries.push((
             file.file_name().unwrap().to_str().unwrap().to_string().into_bytes(),
@@ -116,7 +85,7 @@ impl<'a> ArchiveBuilder<'a> for ArArchiveBuilder<'a> {
         Ok(())
     }
 
-    fn build(mut self) {
+    fn build(mut self) -> bool {
         enum BuilderKind {
             Bsd(ar::Builder<File>),
             Gnu(ar::GnuBuilder<File>),
@@ -168,6 +137,7 @@ impl<'a> ArchiveBuilder<'a> for ArArchiveBuilder<'a> {
         };
 
         // Add all files
+        let any_members = !entries.is_empty();
         for (entry_name, data) in entries.into_iter() {
             let header = ar::Header::new(entry_name, data.len() as u64);
             match builder {
@@ -178,6 +148,7 @@ impl<'a> ArchiveBuilder<'a> for ArArchiveBuilder<'a> {
 
         // Finalize archive
         std::mem::drop(builder);
+        any_members
     }
 
     fn inject_dll_import_lib(
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
index 2ec2278dd44e..83dacec015f0 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
@@ -396,79 +396,79 @@ impl<'tcx> GotocCtx<'tcx> {
                 "assumption failed",
                 loc,
             ),
-            "atomic_and" => codegen_atomic_binop!(bitand),
-            "atomic_and_acq" => codegen_atomic_binop!(bitand),
+            "atomic_and_seqcst" => codegen_atomic_binop!(bitand),
+            "atomic_and_acquire" => codegen_atomic_binop!(bitand),
             "atomic_and_acqrel" => codegen_atomic_binop!(bitand),
-            "atomic_and_rel" => codegen_atomic_binop!(bitand),
+            "atomic_and_release" => codegen_atomic_binop!(bitand),
             "atomic_and_relaxed" => codegen_atomic_binop!(bitand),
             name if name.starts_with("atomic_cxchg") => {
                 self.codegen_atomic_cxchg(intrinsic, fargs, p, loc)
             }
-            "atomic_fence" => self.codegen_atomic_noop(intrinsic, loc),
-            "atomic_fence_acq" => self.codegen_atomic_noop(intrinsic, loc),
+            "atomic_fence_seqcst" => self.codegen_atomic_noop(intrinsic, loc),
+            "atomic_fence_acquire" => self.codegen_atomic_noop(intrinsic, loc),
             "atomic_fence_acqrel" => self.codegen_atomic_noop(intrinsic, loc),
-            "atomic_fence_rel" => self.codegen_atomic_noop(intrinsic, loc),
-            "atomic_load" => self.codegen_atomic_load(intrinsic, fargs, p, loc),
-            "atomic_load_acq" => self.codegen_atomic_load(intrinsic, fargs, p, loc),
+            "atomic_fence_release" => self.codegen_atomic_noop(intrinsic, loc),
+            "atomic_load_seqcst" => self.codegen_atomic_load(intrinsic, fargs, p, loc),
+            "atomic_load_acquire" => 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_max" => codegen_atomic_binop!(max),
-            "atomic_max_acq" => codegen_atomic_binop!(max),
+            "atomic_max_seqcst" => codegen_atomic_binop!(max),
+            "atomic_max_acquire" => codegen_atomic_binop!(max),
             "atomic_max_acqrel" => codegen_atomic_binop!(max),
-            "atomic_max_rel" => codegen_atomic_binop!(max),
+            "atomic_max_release" => codegen_atomic_binop!(max),
             "atomic_max_relaxed" => codegen_atomic_binop!(max),
-            "atomic_min" => codegen_atomic_binop!(min),
-            "atomic_min_acq" => codegen_atomic_binop!(min),
+            "atomic_min_seqcst" => codegen_atomic_binop!(min),
+            "atomic_min_acquire" => codegen_atomic_binop!(min),
             "atomic_min_acqrel" => codegen_atomic_binop!(min),
-            "atomic_min_rel" => codegen_atomic_binop!(min),
+            "atomic_min_release" => 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_seqcst" => codegen_atomic_binop!(bitnand),
+            "atomic_nand_acquire" => codegen_atomic_binop!(bitnand),
             "atomic_nand_acqrel" => codegen_atomic_binop!(bitnand),
-            "atomic_nand_rel" => codegen_atomic_binop!(bitnand),
+            "atomic_nand_release" => codegen_atomic_binop!(bitnand),
             "atomic_nand_relaxed" => codegen_atomic_binop!(bitnand),
-            "atomic_or" => codegen_atomic_binop!(bitor),
-            "atomic_or_acq" => codegen_atomic_binop!(bitor),
+            "atomic_or_seqcst" => codegen_atomic_binop!(bitor),
+            "atomic_or_acquire" => codegen_atomic_binop!(bitor),
             "atomic_or_acqrel" => codegen_atomic_binop!(bitor),
-            "atomic_or_rel" => codegen_atomic_binop!(bitor),
+            "atomic_or_release" => codegen_atomic_binop!(bitor),
             "atomic_or_relaxed" => codegen_atomic_binop!(bitor),
-            "atomic_singlethreadfence" => self.codegen_atomic_noop(intrinsic, loc),
-            "atomic_singlethreadfence_acq" => self.codegen_atomic_noop(intrinsic, loc),
+            "atomic_singlethreadfence_seqcst" => self.codegen_atomic_noop(intrinsic, loc),
+            "atomic_singlethreadfence_acquire" => self.codegen_atomic_noop(intrinsic, loc),
             "atomic_singlethreadfence_acqrel" => self.codegen_atomic_noop(intrinsic, loc),
-            "atomic_singlethreadfence_rel" => self.codegen_atomic_noop(intrinsic, loc),
-            "atomic_store" => self.codegen_atomic_store(intrinsic, fargs, p, loc),
-            "atomic_store_rel" => self.codegen_atomic_store(intrinsic, fargs, p, loc),
+            "atomic_singlethreadfence_release" => self.codegen_atomic_noop(intrinsic, loc),
+            "atomic_store_seqcst" => self.codegen_atomic_store(intrinsic, fargs, p, loc),
+            "atomic_store_release" => 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_umax" => codegen_atomic_binop!(max),
-            "atomic_umax_acq" => codegen_atomic_binop!(max),
+            "atomic_umax_seqcst" => codegen_atomic_binop!(max),
+            "atomic_umax_acquire" => codegen_atomic_binop!(max),
             "atomic_umax_acqrel" => codegen_atomic_binop!(max),
-            "atomic_umax_rel" => codegen_atomic_binop!(max),
+            "atomic_umax_release" => codegen_atomic_binop!(max),
             "atomic_umax_relaxed" => codegen_atomic_binop!(max),
-            "atomic_umin" => codegen_atomic_binop!(min),
-            "atomic_umin_acq" => codegen_atomic_binop!(min),
+            "atomic_umin_seqcst" => codegen_atomic_binop!(min),
+            "atomic_umin_acquire" => codegen_atomic_binop!(min),
             "atomic_umin_acqrel" => codegen_atomic_binop!(min),
-            "atomic_umin_rel" => codegen_atomic_binop!(min),
+            "atomic_umin_release" => 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_seqcst" => codegen_atomic_binop!(plus),
+            "atomic_xadd_acquire" => codegen_atomic_binop!(plus),
             "atomic_xadd_acqrel" => codegen_atomic_binop!(plus),
-            "atomic_xadd_rel" => codegen_atomic_binop!(plus),
+            "atomic_xadd_release" => codegen_atomic_binop!(plus),
             "atomic_xadd_relaxed" => codegen_atomic_binop!(plus),
-            "atomic_xchg" => self.codegen_atomic_store(intrinsic, fargs, p, loc),
-            "atomic_xchg_acq" => self.codegen_atomic_store(intrinsic, fargs, p, loc),
+            "atomic_xchg_seqcst" => self.codegen_atomic_store(intrinsic, fargs, p, loc),
+            "atomic_xchg_acquire" => self.codegen_atomic_store(intrinsic, fargs, p, loc),
             "atomic_xchg_acqrel" => self.codegen_atomic_store(intrinsic, fargs, p, loc),
-            "atomic_xchg_rel" => self.codegen_atomic_store(intrinsic, fargs, p, loc),
+            "atomic_xchg_release" => self.codegen_atomic_store(intrinsic, fargs, p, loc),
             "atomic_xchg_relaxed" => self.codegen_atomic_store(intrinsic, fargs, p, loc),
-            "atomic_xor" => codegen_atomic_binop!(bitxor),
-            "atomic_xor_acq" => codegen_atomic_binop!(bitxor),
+            "atomic_xor_seqcst" => codegen_atomic_binop!(bitxor),
+            "atomic_xor_acquire" => codegen_atomic_binop!(bitxor),
             "atomic_xor_acqrel" => codegen_atomic_binop!(bitxor),
-            "atomic_xor_rel" => codegen_atomic_binop!(bitxor),
+            "atomic_xor_release" => codegen_atomic_binop!(bitxor),
             "atomic_xor_relaxed" => codegen_atomic_binop!(bitxor),
-            "atomic_xsub" => codegen_atomic_binop!(sub),
-            "atomic_xsub_acq" => codegen_atomic_binop!(sub),
+            "atomic_xsub_seqcst" => codegen_atomic_binop!(sub),
+            "atomic_xsub_acquire" => codegen_atomic_binop!(sub),
             "atomic_xsub_acqrel" => codegen_atomic_binop!(sub),
-            "atomic_xsub_rel" => codegen_atomic_binop!(sub),
+            "atomic_xsub_release" => codegen_atomic_binop!(sub),
             "atomic_xsub_relaxed" => codegen_atomic_binop!(sub),
             "bitreverse" => self.codegen_expr_to_place(p, fargs.remove(0).bitreverse()),
             // black_box is an identity function that hints to the compiler
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs
index 610dff983f09..83e759f87c61 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs
@@ -57,7 +57,7 @@ impl<'tcx> GotocCtx<'tcx> {
         debug!("found literal: {:?}", lit);
         let lit = self.monomorphize(lit);
 
-        match lit.val() {
+        match lit.kind() {
             // evaluate constant if it has no been evaluated yet
             ConstKind::Unevaluated(unevaluated) => {
                 debug!("The literal was a Unevaluated");
@@ -68,14 +68,15 @@ impl<'tcx> GotocCtx<'tcx> {
                 self.codegen_const_value(const_val, lit.ty(), span)
             }
 
-            ConstKind::Value(v) => {
-                debug!("The literal was a ConstValue {:?}", v);
-                self.codegen_const_value(v, lit.ty(), span)
+            ConstKind::Value(valtree) => {
+                let value = self.tcx.valtree_to_const_val((lit.ty(), valtree));
+                debug!("The literal was a ConstValue {:?}", value);
+                self.codegen_const_value(value, lit.ty(), span)
             }
             _ => {
                 unreachable!(
                     "monomorphized item shouldn't have this constant value: {:?}",
-                    lit.val()
+                    lit.kind()
                 )
             }
         }
@@ -104,8 +105,6 @@ impl<'tcx> GotocCtx<'tcx> {
                 ty::Slice(slice_ty) => {
                     if let Uint(UintTy::U8) = slice_ty.kind() {
                         // The case where we have a slice of u8 is easy enough: make an array of u8
-                        // TODO: Handle cases with larger int types by making an array of bytes,
-                        // then using byte-extract on it.
                         let slice =
                             data.inspect_with_uninit_and_ptr_outside_interpreter(start..end);
                         let vec_of_bytes: Vec<Expr> = slice
@@ -123,12 +122,22 @@ impl<'tcx> GotocCtx<'tcx> {
                             len_expr,
                             &self.symbol_table,
                         );
+                    } else {
+                        // TODO: Handle cases with other types such as tuples and larger integers.
+                        let loc = self.codegen_span_option(span.cloned());
+                        let typ = self.codegen_ty(lit_ty);
+                        return self.codegen_unimplemented(
+                            "Constant slice value with 2+ bytes",
+                            typ,
+                            loc,
+                            "https://github.com/model-checking/kani/issues/1339",
+                        );
                     }
                 }
                 _ => {}
             }
         }
-        unimplemented!("\nv {:?}\nlit_ty {:?}\nspan {:?}", v, lit_ty, span);
+        unimplemented!("\nv {:?}\nlit_ty {:?}\nspan {:?}", v, lit_ty.kind(), span);
     }
 
     pub fn codegen_const_value(
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs
index 40051137ff19..d35e6e6d8bf3 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs
@@ -446,7 +446,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 // https://rust-lang.github.io/rfcs/2359-subslice-pattern-syntax.html
                 match before.mir_typ().kind() {
                     ty::Array(ty, len) => {
-                        let len = len.val().try_to_machine_usize(self.tcx).unwrap();
+                        let len = len.kind().try_to_machine_usize(self.tcx).unwrap();
                         let subarray_len = if from_end {
                             // `to` counts from the end of the array
                             len - to - from
@@ -578,7 +578,7 @@ impl<'tcx> GotocCtx<'tcx> {
         match before.mir_typ().kind() {
             //TODO, ask on zulip if we can ever have from_end here?
             ty::Array(elemt, length) => {
-                let length = length.val().try_to_machine_usize(self.tcx).unwrap();
+                let length = length.kind().try_to_machine_usize(self.tcx).unwrap();
                 assert!(length >= min_length);
                 let idx = if from_end { length - offset } else { offset };
                 let idxe = Expr::int_constant(idx, Type::ssize_t());
diff --git a/kani-compiler/src/codegen_cprover_gotoc/utils/debug.rs b/kani-compiler/src/codegen_cprover_gotoc/utils/debug.rs
index 590e6b078523..92af99445146 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/utils/debug.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/utils/debug.rs
@@ -10,8 +10,8 @@ use rustc_middle::ty::print::with_no_trimmed_paths;
 use rustc_middle::ty::Instance;
 use rustc_span::def_id::DefId;
 use std::cell::RefCell;
-use std::lazy::SyncLazy;
 use std::panic;
+use std::sync::LazyLock;
 use tracing::debug;
 
 // Use a thread-local global variable to track the current codegen item for debugging.
@@ -21,12 +21,12 @@ thread_local!(static CURRENT_CODEGEN_ITEM: RefCell<(Option<String>, Option<Locat
 
 pub fn init() {
     // Install panic hook
-    SyncLazy::force(&DEFAULT_HOOK); // Install ice hook
+    LazyLock::force(&DEFAULT_HOOK); // Install ice hook
 }
 
 // Custom panic hook to add more information when panic occurs during goto-c codegen.
-static DEFAULT_HOOK: SyncLazy<Box<dyn Fn(&panic::PanicInfo<'_>) + Sync + Send + 'static>> =
-    SyncLazy::new(|| {
+static DEFAULT_HOOK: LazyLock<Box<dyn Fn(&panic::PanicInfo<'_>) + Sync + Send + 'static>> =
+    LazyLock::new(|| {
         let hook = panic::take_hook();
         panic::set_hook(Box::new(|info| {
             // Invoke the default handler, which prints the actual panic message and
diff --git a/kani-compiler/src/session.rs b/kani-compiler/src/session.rs
index 37d3f87343f3..f577d251ee56 100644
--- a/kani-compiler/src/session.rs
+++ b/kani-compiler/src/session.rs
@@ -5,9 +5,9 @@
 
 use crate::parser;
 use clap::ArgMatches;
-use std::lazy::SyncLazy;
 use std::panic;
 use std::str::FromStr;
+use std::sync::LazyLock;
 use tracing_subscriber::{filter::Directive, layer::SubscriberExt, EnvFilter, Registry};
 use tracing_tree::HierarchicalLayer;
 
@@ -19,8 +19,8 @@ const BUG_REPORT_URL: &str =
     "https://github.com/model-checking/kani/issues/new?labels=bug&template=bug_report.md";
 
 // Custom panic hook.
-static PANIC_HOOK: SyncLazy<Box<dyn Fn(&panic::PanicInfo<'_>) + Sync + Send + 'static>> =
-    SyncLazy::new(|| {
+static PANIC_HOOK: LazyLock<Box<dyn Fn(&panic::PanicInfo<'_>) + Sync + Send + 'static>> =
+    LazyLock::new(|| {
         let hook = panic::take_hook();
         panic::set_hook(Box::new(|info| {
             // Print stack trace.
@@ -92,5 +92,5 @@ fn hier_logs(args: &ArgMatches, filter: EnvFilter) {
 
 fn init_panic_hook() {
     // Install panic hook
-    SyncLazy::force(&PANIC_HOOK); // Install ice hook
+    LazyLock::force(&PANIC_HOOK); // Install ice hook
 }
diff --git a/rust-toolchain.toml b/rust-toolchain.toml
index de3911297898..468e8286bdab 100644
--- a/rust-toolchain.toml
+++ b/rust-toolchain.toml
@@ -2,5 +2,5 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 [toolchain]
-channel = "nightly-2022-06-09"
+channel = "nightly-2022-07-05"
 components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]
diff --git a/tests/kani/Intrinsics/Atomic/Unstable/AtomicAdd/main.rs b/tests/kani/Intrinsics/Atomic/Unstable/AtomicAdd/main.rs
index 95a466f27888..2f85653b0631 100644
--- a/tests/kani/Intrinsics/Atomic/Unstable/AtomicAdd/main.rs
+++ b/tests/kani/Intrinsics/Atomic/Unstable/AtomicAdd/main.rs
@@ -6,7 +6,8 @@
 
 #![feature(core_intrinsics)]
 use std::intrinsics::{
-    atomic_xadd, atomic_xadd_acq, atomic_xadd_acqrel, atomic_xadd_rel, atomic_xadd_relaxed,
+    atomic_xadd_acqrel, atomic_xadd_acquire, atomic_xadd_relaxed, atomic_xadd_release,
+    atomic_xadd_seqcst,
 };
 
 #[kani::proof]
@@ -27,10 +28,10 @@ fn main() {
     let c = 1 as u8;
 
     unsafe {
-        let x1 = atomic_xadd(ptr_a1, b);
-        let x2 = atomic_xadd_acq(ptr_a2, b);
+        let x1 = atomic_xadd_seqcst(ptr_a1, b);
+        let x2 = atomic_xadd_acquire(ptr_a2, b);
         let x3 = atomic_xadd_acqrel(ptr_a3, b);
-        let x4 = atomic_xadd_rel(ptr_a4, b);
+        let x4 = atomic_xadd_release(ptr_a4, b);
         let x5 = atomic_xadd_relaxed(ptr_a5, b);
 
         assert!(x1 == 0);
diff --git a/tests/kani/Intrinsics/Atomic/Unstable/AtomicAnd/main.rs b/tests/kani/Intrinsics/Atomic/Unstable/AtomicAnd/main.rs
index 913b66c72ecd..6be83c2eaa2b 100644
--- a/tests/kani/Intrinsics/Atomic/Unstable/AtomicAnd/main.rs
+++ b/tests/kani/Intrinsics/Atomic/Unstable/AtomicAnd/main.rs
@@ -1,12 +1,13 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-// Check that `atomic_and` and other variants (unstable version) return the
+// Check that `atomic_and_seqcst` and other variants (unstable version) return the
 // expected result.
 
 #![feature(core_intrinsics)]
 use std::intrinsics::{
-    atomic_and, atomic_and_acq, atomic_and_acqrel, atomic_and_rel, atomic_and_relaxed,
+    atomic_and_acqrel, atomic_and_acquire, atomic_and_relaxed, atomic_and_release,
+    atomic_and_seqcst,
 };
 
 #[kani::proof]
@@ -26,10 +27,10 @@ fn main() {
     let b = 0 as u8;
 
     unsafe {
-        let x1 = atomic_and(ptr_a1, b);
-        let x2 = atomic_and_acq(ptr_a2, b);
+        let x1 = atomic_and_seqcst(ptr_a1, b);
+        let x2 = atomic_and_acquire(ptr_a2, b);
         let x3 = atomic_and_acqrel(ptr_a3, b);
-        let x4 = atomic_and_rel(ptr_a4, b);
+        let x4 = atomic_and_release(ptr_a4, b);
         let x5 = atomic_and_relaxed(ptr_a5, b);
 
         assert!(x1 == 1);
diff --git a/tests/kani/Intrinsics/Atomic/Unstable/AtomicCxchg/main.rs b/tests/kani/Intrinsics/Atomic/Unstable/AtomicCxchg/main.rs
index 19293b3a9151..898ad26dd514 100644
--- a/tests/kani/Intrinsics/Atomic/Unstable/AtomicCxchg/main.rs
+++ b/tests/kani/Intrinsics/Atomic/Unstable/AtomicCxchg/main.rs
@@ -6,9 +6,9 @@
 
 #![feature(core_intrinsics)]
 use std::intrinsics::{
-    atomic_cxchg, atomic_cxchg_acq, atomic_cxchg_acq_failrelaxed, atomic_cxchg_acqrel,
-    atomic_cxchg_acqrel_failrelaxed, atomic_cxchg_failacq, atomic_cxchg_failrelaxed,
-    atomic_cxchg_rel, atomic_cxchg_relaxed,
+    atomic_cxchg_acqrel_acquire, atomic_cxchg_acqrel_relaxed, atomic_cxchg_acquire_acquire,
+    atomic_cxchg_acquire_relaxed, atomic_cxchg_relaxed_relaxed, atomic_cxchg_release_relaxed,
+    atomic_cxchg_seqcst_acquire, atomic_cxchg_seqcst_relaxed, atomic_cxchg_seqcst_seqcst,
 };
 
 #[kani::proof]
@@ -38,15 +38,15 @@ fn main() {
         // Returns (val, ok) where
         //  * val: the old value
         //  * ok:  bool indicating whether the operation was successful or not
-        let x1 = atomic_cxchg(ptr_a1, 0, 1);
-        let x2 = atomic_cxchg_acq(ptr_a2, 0, 1);
-        let x3 = atomic_cxchg_acq_failrelaxed(ptr_a3, 0, 1);
-        let x4 = atomic_cxchg_acqrel(ptr_a4, 0, 1);
-        let x5 = atomic_cxchg_acqrel_failrelaxed(ptr_a5, 0, 1);
-        let x6 = atomic_cxchg_failacq(ptr_a6, 0, 1);
-        let x7 = atomic_cxchg_failrelaxed(ptr_a7, 0, 1);
-        let x8 = atomic_cxchg_rel(ptr_a8, 0, 1);
-        let x9 = atomic_cxchg_relaxed(ptr_a9, 0, 1);
+        let x1 = atomic_cxchg_seqcst_seqcst(ptr_a1, 0, 1);
+        let x2 = atomic_cxchg_acquire_acquire(ptr_a2, 0, 1);
+        let x3 = atomic_cxchg_acquire_relaxed(ptr_a3, 0, 1);
+        let x4 = atomic_cxchg_acqrel_acquire(ptr_a4, 0, 1);
+        let x5 = atomic_cxchg_acqrel_relaxed(ptr_a5, 0, 1);
+        let x6 = atomic_cxchg_seqcst_acquire(ptr_a6, 0, 1);
+        let x7 = atomic_cxchg_seqcst_relaxed(ptr_a7, 0, 1);
+        let x8 = atomic_cxchg_release_relaxed(ptr_a8, 0, 1);
+        let x9 = atomic_cxchg_relaxed_relaxed(ptr_a9, 0, 1);
 
         assert!(x1 == (0, true));
         assert!(x2 == (0, true));
@@ -58,15 +58,15 @@ fn main() {
         assert!(x8 == (0, true));
         assert!(x9 == (0, true));
 
-        let y1 = atomic_cxchg(ptr_a1, 1, 1);
-        let y2 = atomic_cxchg_acq(ptr_a2, 1, 1);
-        let y3 = atomic_cxchg_acq_failrelaxed(ptr_a3, 1, 1);
-        let y4 = atomic_cxchg_acqrel(ptr_a4, 1, 1);
-        let y5 = atomic_cxchg_acqrel_failrelaxed(ptr_a5, 1, 1);
-        let y6 = atomic_cxchg_failacq(ptr_a6, 1, 1);
-        let y7 = atomic_cxchg_failrelaxed(ptr_a7, 1, 1);
-        let y8 = atomic_cxchg_rel(ptr_a8, 1, 1);
-        let y9 = atomic_cxchg_relaxed(ptr_a9, 1, 1);
+        let y1 = atomic_cxchg_seqcst_seqcst(ptr_a1, 1, 1);
+        let y2 = atomic_cxchg_acquire_acquire(ptr_a2, 1, 1);
+        let y3 = atomic_cxchg_acqrel_relaxed(ptr_a3, 1, 1);
+        let y4 = atomic_cxchg_acqrel_acquire(ptr_a4, 1, 1);
+        let y5 = atomic_cxchg_acqrel_relaxed(ptr_a5, 1, 1);
+        let y6 = atomic_cxchg_seqcst_acquire(ptr_a6, 1, 1);
+        let y7 = atomic_cxchg_seqcst_relaxed(ptr_a7, 1, 1);
+        let y8 = atomic_cxchg_release_relaxed(ptr_a8, 1, 1);
+        let y9 = atomic_cxchg_relaxed_relaxed(ptr_a9, 1, 1);
 
         assert!(y1 == (1, true));
         assert!(y2 == (1, true));
diff --git a/tests/kani/Intrinsics/Atomic/Unstable/AtomicCxchgWeak/main.rs b/tests/kani/Intrinsics/Atomic/Unstable/AtomicCxchgWeak/main.rs
index e83359b9eefa..f3a615c07c7b 100644
--- a/tests/kani/Intrinsics/Atomic/Unstable/AtomicCxchgWeak/main.rs
+++ b/tests/kani/Intrinsics/Atomic/Unstable/AtomicCxchgWeak/main.rs
@@ -1,14 +1,16 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-// Check that `atomic_cxchgweak` and other variants (unstable version) return
+// Check that `atomic_cxchgweak_seqcst` and other variants (unstable version) return
 // the expected result.
 
 #![feature(core_intrinsics)]
 use std::intrinsics::{
-    atomic_cxchgweak, atomic_cxchgweak_acq, atomic_cxchgweak_acq_failrelaxed,
-    atomic_cxchgweak_acqrel, atomic_cxchgweak_acqrel_failrelaxed, atomic_cxchgweak_failacq,
-    atomic_cxchgweak_failrelaxed, atomic_cxchgweak_rel, atomic_cxchgweak_relaxed,
+    atomic_cxchgweak_acqrel_acquire, atomic_cxchgweak_acqrel_relaxed,
+    atomic_cxchgweak_acquire_acquire, atomic_cxchgweak_acquire_relaxed,
+    atomic_cxchgweak_relaxed_relaxed, atomic_cxchgweak_release_seqcst,
+    atomic_cxchgweak_seqcst_acquire, atomic_cxchgweak_seqcst_relaxed,
+    atomic_cxchgweak_seqcst_seqcst,
 };
 
 #[kani::proof]
@@ -38,15 +40,15 @@ fn main() {
         // Returns (val, ok) where
         //  * val: the old value
         //  * ok:  bool indicating whether the operation was successful or not
-        let x1 = atomic_cxchgweak(ptr_a1, 0, 1);
-        let x2 = atomic_cxchgweak_acq(ptr_a2, 0, 1);
-        let x3 = atomic_cxchgweak_acq_failrelaxed(ptr_a3, 0, 1);
-        let x4 = atomic_cxchgweak_acqrel(ptr_a4, 0, 1);
-        let x5 = atomic_cxchgweak_acqrel_failrelaxed(ptr_a5, 0, 1);
-        let x6 = atomic_cxchgweak_failacq(ptr_a6, 0, 1);
-        let x7 = atomic_cxchgweak_failrelaxed(ptr_a7, 0, 1);
-        let x8 = atomic_cxchgweak_rel(ptr_a8, 0, 1);
-        let x9 = atomic_cxchgweak_relaxed(ptr_a9, 0, 1);
+        let x1 = atomic_cxchgweak_seqcst_seqcst(ptr_a1, 0, 1);
+        let x2 = atomic_cxchgweak_acquire_acquire(ptr_a2, 0, 1);
+        let x3 = atomic_cxchgweak_acquire_relaxed(ptr_a3, 0, 1);
+        let x4 = atomic_cxchgweak_acqrel_acquire(ptr_a4, 0, 1);
+        let x5 = atomic_cxchgweak_acqrel_relaxed(ptr_a5, 0, 1);
+        let x6 = atomic_cxchgweak_seqcst_acquire(ptr_a6, 0, 1);
+        let x7 = atomic_cxchgweak_seqcst_relaxed(ptr_a7, 0, 1);
+        let x8 = atomic_cxchgweak_release_seqcst(ptr_a8, 0, 1);
+        let x9 = atomic_cxchgweak_relaxed_relaxed(ptr_a9, 0, 1);
 
         assert!(x1 == (0, true));
         assert!(x2 == (0, true));
@@ -58,15 +60,15 @@ fn main() {
         assert!(x8 == (0, true));
         assert!(x9 == (0, true));
 
-        let y1 = atomic_cxchgweak(ptr_a1, 1, 1);
-        let y2 = atomic_cxchgweak_acq(ptr_a2, 1, 1);
-        let y3 = atomic_cxchgweak_acq_failrelaxed(ptr_a3, 1, 1);
-        let y4 = atomic_cxchgweak_acqrel(ptr_a4, 1, 1);
-        let y5 = atomic_cxchgweak_acqrel_failrelaxed(ptr_a5, 1, 1);
-        let y6 = atomic_cxchgweak_failacq(ptr_a6, 1, 1);
-        let y7 = atomic_cxchgweak_failrelaxed(ptr_a7, 1, 1);
-        let y8 = atomic_cxchgweak_rel(ptr_a8, 1, 1);
-        let y9 = atomic_cxchgweak_relaxed(ptr_a9, 1, 1);
+        let y1 = atomic_cxchgweak_seqcst_seqcst(ptr_a1, 1, 1);
+        let y2 = atomic_cxchgweak_acquire_acquire(ptr_a2, 1, 1);
+        let y3 = atomic_cxchgweak_acquire_relaxed(ptr_a3, 1, 1);
+        let y4 = atomic_cxchgweak_acqrel_acquire(ptr_a4, 1, 1);
+        let y5 = atomic_cxchgweak_acqrel_relaxed(ptr_a5, 1, 1);
+        let y6 = atomic_cxchgweak_seqcst_acquire(ptr_a6, 1, 1);
+        let y7 = atomic_cxchgweak_seqcst_relaxed(ptr_a7, 1, 1);
+        let y8 = atomic_cxchgweak_release_seqcst(ptr_a8, 1, 1);
+        let y9 = atomic_cxchgweak_relaxed_relaxed(ptr_a9, 1, 1);
 
         assert!(y1 == (1, true));
         assert!(y2 == (1, true));
diff --git a/tests/kani/Intrinsics/Atomic/Unstable/AtomicFence/main.rs b/tests/kani/Intrinsics/Atomic/Unstable/AtomicFence/main.rs
index 5eb770563819..44cddd82e7dc 100644
--- a/tests/kani/Intrinsics/Atomic/Unstable/AtomicFence/main.rs
+++ b/tests/kani/Intrinsics/Atomic/Unstable/AtomicFence/main.rs
@@ -5,14 +5,16 @@
 // processed.
 
 #![feature(core_intrinsics)]
-use std::intrinsics::{atomic_fence, atomic_fence_acq, atomic_fence_acqrel, atomic_fence_rel};
+use std::intrinsics::{
+    atomic_fence_acqrel, atomic_fence_acquire, atomic_fence_release, atomic_fence_seqcst,
+};
 
 #[kani::proof]
 fn main() {
     unsafe {
-        atomic_fence();
-        atomic_fence_acq();
+        atomic_fence_seqcst();
+        atomic_fence_acquire();
         atomic_fence_acqrel();
-        atomic_fence_rel();
+        atomic_fence_release();
     }
 }
diff --git a/tests/kani/Intrinsics/Atomic/Unstable/AtomicLoad/main.rs b/tests/kani/Intrinsics/Atomic/Unstable/AtomicLoad/main.rs
index f326cdb7c091..b646c8326229 100644
--- a/tests/kani/Intrinsics/Atomic/Unstable/AtomicLoad/main.rs
+++ b/tests/kani/Intrinsics/Atomic/Unstable/AtomicLoad/main.rs
@@ -1,11 +1,11 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-// Check that `atomic_load` and other variants (unstable version) return the
+// Check that `atomic_load_seqcst` and other variants (unstable version) return the
 // expected result.
 
 #![feature(core_intrinsics)]
-use std::intrinsics::{atomic_load, atomic_load_acq, atomic_load_relaxed};
+use std::intrinsics::{atomic_load_acquire, atomic_load_relaxed, atomic_load_seqcst};
 
 #[kani::proof]
 fn main() {
@@ -18,8 +18,8 @@ fn main() {
     let ptr_a3: *const u8 = &a3;
 
     unsafe {
-        let x1 = atomic_load(ptr_a1);
-        let x2 = atomic_load_acq(ptr_a2);
+        let x1 = atomic_load_seqcst(ptr_a1);
+        let x2 = atomic_load_acquire(ptr_a2);
         let x3 = atomic_load_relaxed(ptr_a3);
 
         assert!(x1 == 1);
diff --git a/tests/kani/Intrinsics/Atomic/Unstable/AtomicMax/main.rs b/tests/kani/Intrinsics/Atomic/Unstable/AtomicMax/main.rs
index a8fed921ceae..9d5d850fe1c0 100644
--- a/tests/kani/Intrinsics/Atomic/Unstable/AtomicMax/main.rs
+++ b/tests/kani/Intrinsics/Atomic/Unstable/AtomicMax/main.rs
@@ -1,12 +1,13 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-// Check that `atomic_max` and other variants (unstable version) return the
+// Check that `atomic_max_seqcst` and other variants (unstable version) return the
 // expected result.
 
 #![feature(core_intrinsics)]
 use std::intrinsics::{
-    atomic_max, atomic_max_acq, atomic_max_acqrel, atomic_max_rel, atomic_max_relaxed,
+    atomic_max_acqrel, atomic_max_acquire, atomic_max_relaxed, atomic_max_release,
+    atomic_max_seqcst,
 };
 
 #[kani::proof]
@@ -26,10 +27,10 @@ fn main() {
     let b = 1 as u8;
 
     unsafe {
-        let x1 = atomic_max(ptr_a1, b);
-        let x2 = atomic_max_acq(ptr_a2, b);
+        let x1 = atomic_max_seqcst(ptr_a1, b);
+        let x2 = atomic_max_acquire(ptr_a2, b);
         let x3 = atomic_max_acqrel(ptr_a3, b);
-        let x4 = atomic_max_rel(ptr_a4, b);
+        let x4 = atomic_max_release(ptr_a4, b);
         let x5 = atomic_max_relaxed(ptr_a5, b);
 
         assert!(x1 == 0);
diff --git a/tests/kani/Intrinsics/Atomic/Unstable/AtomicMin/main.rs b/tests/kani/Intrinsics/Atomic/Unstable/AtomicMin/main.rs
index 0091bfb54209..ea9caf5971de 100644
--- a/tests/kani/Intrinsics/Atomic/Unstable/AtomicMin/main.rs
+++ b/tests/kani/Intrinsics/Atomic/Unstable/AtomicMin/main.rs
@@ -1,12 +1,13 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-// Check that `atomic_min` and other variants (unstable version) return the
+// Check that `atomic_min_seqcst` 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,
+    atomic_min_acqrel, atomic_min_acquire, atomic_min_relaxed, atomic_min_release,
+    atomic_min_seqcst,
 };
 
 #[kani::proof]
@@ -26,10 +27,10 @@ fn main() {
     let b = 0 as u8;
 
     unsafe {
-        let x1 = atomic_min(ptr_a1, b);
-        let x2 = atomic_min_acq(ptr_a2, b);
+        let x1 = atomic_min_seqcst(ptr_a1, b);
+        let x2 = atomic_min_acquire(ptr_a2, b);
         let x3 = atomic_min_acqrel(ptr_a3, b);
-        let x4 = atomic_min_rel(ptr_a4, b);
+        let x4 = atomic_min_release(ptr_a4, b);
         let x5 = atomic_min_relaxed(ptr_a5, b);
 
         assert!(x1 == 1);
diff --git a/tests/kani/Intrinsics/Atomic/Unstable/AtomicNand/main.rs b/tests/kani/Intrinsics/Atomic/Unstable/AtomicNand/main.rs
index 342886ca0837..c058dadfd0a1 100644
--- a/tests/kani/Intrinsics/Atomic/Unstable/AtomicNand/main.rs
+++ b/tests/kani/Intrinsics/Atomic/Unstable/AtomicNand/main.rs
@@ -1,12 +1,13 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-// Check that `atomic_nand` and other variants (unstable version) return the
+// Check that `atomic_nand_seqcst` and other variants (unstable version) return the
 // expected result.
 
 #![feature(core_intrinsics)]
 use std::intrinsics::{
-    atomic_nand, atomic_nand_acq, atomic_nand_acqrel, atomic_nand_rel, atomic_nand_relaxed,
+    atomic_nand_acqrel, atomic_nand_acquire, atomic_nand_relaxed, atomic_nand_release,
+    atomic_nand_seqcst,
 };
 
 #[kani::proof]
@@ -26,10 +27,10 @@ fn main() {
     let b = u8::MAX as u8;
 
     unsafe {
-        let x1 = atomic_nand(ptr_a1, b);
-        let x2 = atomic_nand_acq(ptr_a2, b);
+        let x1 = atomic_nand_seqcst(ptr_a1, b);
+        let x2 = atomic_nand_acquire(ptr_a2, b);
         let x3 = atomic_nand_acqrel(ptr_a3, b);
-        let x4 = atomic_nand_rel(ptr_a4, b);
+        let x4 = atomic_nand_release(ptr_a4, b);
         let x5 = atomic_nand_relaxed(ptr_a5, b);
 
         assert!(x1 == 0);
@@ -44,10 +45,10 @@ fn main() {
         assert!(*ptr_a4 == b);
         assert!(*ptr_a5 == b);
 
-        let x1 = atomic_nand(ptr_a1, b);
-        let x2 = atomic_nand_acq(ptr_a2, b);
+        let x1 = atomic_nand_seqcst(ptr_a1, b);
+        let x2 = atomic_nand_acquire(ptr_a2, b);
         let x3 = atomic_nand_acqrel(ptr_a3, b);
-        let x4 = atomic_nand_rel(ptr_a4, b);
+        let x4 = atomic_nand_release(ptr_a4, b);
         let x5 = atomic_nand_relaxed(ptr_a5, b);
 
         assert!(x1 == b);
diff --git a/tests/kani/Intrinsics/Atomic/Unstable/AtomicOr/main.rs b/tests/kani/Intrinsics/Atomic/Unstable/AtomicOr/main.rs
index ce2332458d4f..9eba4396b560 100644
--- a/tests/kani/Intrinsics/Atomic/Unstable/AtomicOr/main.rs
+++ b/tests/kani/Intrinsics/Atomic/Unstable/AtomicOr/main.rs
@@ -1,12 +1,12 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-// Check that `atomic_or` and other variants (unstable version) return the
+// Check that `atomic_or_seqcst` and other variants (unstable version) return the
 // expected result.
 
 #![feature(core_intrinsics)]
 use std::intrinsics::{
-    atomic_or, atomic_or_acq, atomic_or_acqrel, atomic_or_rel, atomic_or_relaxed,
+    atomic_or_acqrel, atomic_or_acquire, atomic_or_relaxed, atomic_or_release, atomic_or_seqcst,
 };
 
 #[kani::proof]
@@ -27,10 +27,10 @@ fn main() {
     let c = 1 as u8;
 
     unsafe {
-        let x1 = atomic_or(ptr_a1, b);
-        let x2 = atomic_or_acq(ptr_a2, b);
+        let x1 = atomic_or_seqcst(ptr_a1, b);
+        let x2 = atomic_or_acquire(ptr_a2, b);
         let x3 = atomic_or_acqrel(ptr_a3, b);
-        let x4 = atomic_or_rel(ptr_a4, b);
+        let x4 = atomic_or_release(ptr_a4, b);
         let x5 = atomic_or_relaxed(ptr_a5, b);
 
         assert!(x1 == 1);
diff --git a/tests/kani/Intrinsics/Atomic/Unstable/AtomicSingleThreadFence/main.rs b/tests/kani/Intrinsics/Atomic/Unstable/AtomicSingleThreadFence/main.rs
index d2367f987498..1b5b7df8bd34 100644
--- a/tests/kani/Intrinsics/Atomic/Unstable/AtomicSingleThreadFence/main.rs
+++ b/tests/kani/Intrinsics/Atomic/Unstable/AtomicSingleThreadFence/main.rs
@@ -1,21 +1,21 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-// Check that `atomic_singlethreadfence` and other variants (unstable version)
+// Check that `atomic_singlethreadfence_seqcst` and other variants (unstable version)
 // can be processed.
 
 #![feature(core_intrinsics)]
 use std::intrinsics::{
-    atomic_singlethreadfence, atomic_singlethreadfence_acq, atomic_singlethreadfence_acqrel,
-    atomic_singlethreadfence_rel,
+    atomic_singlethreadfence_acqrel, atomic_singlethreadfence_acquire,
+    atomic_singlethreadfence_release, atomic_singlethreadfence_seqcst,
 };
 
 #[kani::proof]
 fn main() {
     unsafe {
-        atomic_singlethreadfence();
-        atomic_singlethreadfence_acq();
+        atomic_singlethreadfence_seqcst();
+        atomic_singlethreadfence_acquire();
         atomic_singlethreadfence_acqrel();
-        atomic_singlethreadfence_rel();
+        atomic_singlethreadfence_release();
     }
 }
diff --git a/tests/kani/Intrinsics/Atomic/Unstable/AtomicStore/main.rs b/tests/kani/Intrinsics/Atomic/Unstable/AtomicStore/main.rs
index 815076381719..fd73c1c863eb 100644
--- a/tests/kani/Intrinsics/Atomic/Unstable/AtomicStore/main.rs
+++ b/tests/kani/Intrinsics/Atomic/Unstable/AtomicStore/main.rs
@@ -1,11 +1,11 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-// Check that `atomic_store` and other variants (unstable version) return the
+// Check that `atomic_store_seqcst` and other variants (unstable version) return the
 // expected result.
 
 #![feature(core_intrinsics)]
-use std::intrinsics::{atomic_store, atomic_store_rel, atomic_store_relaxed};
+use std::intrinsics::{atomic_store_relaxed, atomic_store_release, atomic_store_seqcst};
 
 #[kani::proof]
 fn main() {
@@ -18,8 +18,8 @@ fn main() {
     let ptr_a3: *mut u8 = &mut a3;
 
     unsafe {
-        atomic_store(ptr_a1, 0);
-        atomic_store_rel(ptr_a2, 0);
+        atomic_store_seqcst(ptr_a1, 0);
+        atomic_store_release(ptr_a2, 0);
         atomic_store_relaxed(ptr_a3, 0);
 
         assert!(*ptr_a1 == 0);
diff --git a/tests/kani/Intrinsics/Atomic/Unstable/AtomicSub/main.rs b/tests/kani/Intrinsics/Atomic/Unstable/AtomicSub/main.rs
index 474dae07ca23..3f205068948c 100644
--- a/tests/kani/Intrinsics/Atomic/Unstable/AtomicSub/main.rs
+++ b/tests/kani/Intrinsics/Atomic/Unstable/AtomicSub/main.rs
@@ -1,12 +1,13 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-// Check that `atomic_xsub` and other variants (unstable version) return the
+// Check that `atomic_xsub_seqcst` and other variants (unstable version) return the
 // expected result.
 
 #![feature(core_intrinsics)]
 use std::intrinsics::{
-    atomic_xsub, atomic_xsub_acq, atomic_xsub_acqrel, atomic_xsub_rel, atomic_xsub_relaxed,
+    atomic_xsub_acqrel, atomic_xsub_acquire, atomic_xsub_relaxed, atomic_xsub_release,
+    atomic_xsub_seqcst,
 };
 
 #[kani::proof]
@@ -27,10 +28,10 @@ fn main() {
     let c = 0 as u8;
 
     unsafe {
-        let x1 = atomic_xsub(ptr_a1, b);
-        let x2 = atomic_xsub_acq(ptr_a2, b);
+        let x1 = atomic_xsub_seqcst(ptr_a1, b);
+        let x2 = atomic_xsub_acquire(ptr_a2, b);
         let x3 = atomic_xsub_acqrel(ptr_a3, b);
-        let x4 = atomic_xsub_rel(ptr_a4, b);
+        let x4 = atomic_xsub_release(ptr_a4, b);
         let x5 = atomic_xsub_relaxed(ptr_a5, b);
 
         assert!(x1 == 1);
diff --git a/tests/kani/Intrinsics/Atomic/Unstable/AtomicUmax/main.rs b/tests/kani/Intrinsics/Atomic/Unstable/AtomicUmax/main.rs
index be35b59ad2b7..ee05691da839 100644
--- a/tests/kani/Intrinsics/Atomic/Unstable/AtomicUmax/main.rs
+++ b/tests/kani/Intrinsics/Atomic/Unstable/AtomicUmax/main.rs
@@ -1,12 +1,13 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-// Check that `atomic_umax` and other variants (unstable version) return the
+// Check that `atomic_umax_seqcst` and other variants (unstable version) return the
 // expected result.
 
 #![feature(core_intrinsics)]
 use std::intrinsics::{
-    atomic_umax, atomic_umax_acq, atomic_umax_acqrel, atomic_umax_rel, atomic_umax_relaxed,
+    atomic_umax_acqrel, atomic_umax_acquire, atomic_umax_relaxed, atomic_umax_release,
+    atomic_umax_seqcst,
 };
 
 #[kani::proof]
@@ -26,10 +27,10 @@ fn main() {
     let b = 1 as u8;
 
     unsafe {
-        let x1 = atomic_umax(ptr_a1, b);
-        let x2 = atomic_umax_acq(ptr_a2, b);
+        let x1 = atomic_umax_seqcst(ptr_a1, b);
+        let x2 = atomic_umax_acquire(ptr_a2, b);
         let x3 = atomic_umax_acqrel(ptr_a3, b);
-        let x4 = atomic_umax_rel(ptr_a4, b);
+        let x4 = atomic_umax_release(ptr_a4, b);
         let x5 = atomic_umax_relaxed(ptr_a5, b);
 
         assert!(x1 == 0);
diff --git a/tests/kani/Intrinsics/Atomic/Unstable/AtomicUmin/main.rs b/tests/kani/Intrinsics/Atomic/Unstable/AtomicUmin/main.rs
index 032413a1b64c..69aea2493c85 100644
--- a/tests/kani/Intrinsics/Atomic/Unstable/AtomicUmin/main.rs
+++ b/tests/kani/Intrinsics/Atomic/Unstable/AtomicUmin/main.rs
@@ -1,12 +1,13 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-// Check that `atomic_umin` and other variants (unstable version) return the
+// Check that `atomic_umin_seqcst` 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,
+    atomic_umin_acqrel, atomic_umin_acquire, atomic_umin_relaxed, atomic_umin_release,
+    atomic_umin_seqcst,
 };
 
 #[kani::proof]
@@ -26,10 +27,10 @@ fn main() {
     let b = 0 as u8;
 
     unsafe {
-        let x1 = atomic_umin(ptr_a1, b);
-        let x2 = atomic_umin_acq(ptr_a2, b);
+        let x1 = atomic_umin_seqcst(ptr_a1, b);
+        let x2 = atomic_umin_acquire(ptr_a2, b);
         let x3 = atomic_umin_acqrel(ptr_a3, b);
-        let x4 = atomic_umin_rel(ptr_a4, b);
+        let x4 = atomic_umin_release(ptr_a4, b);
         let x5 = atomic_umin_relaxed(ptr_a5, b);
 
         assert!(x1 == 1);
diff --git a/tests/kani/Intrinsics/Atomic/Unstable/AtomicXchg/main.rs b/tests/kani/Intrinsics/Atomic/Unstable/AtomicXchg/main.rs
index 28f75728b7bf..e91027f61b5a 100644
--- a/tests/kani/Intrinsics/Atomic/Unstable/AtomicXchg/main.rs
+++ b/tests/kani/Intrinsics/Atomic/Unstable/AtomicXchg/main.rs
@@ -1,12 +1,13 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-// Check that `atomic_xchg` and other variants (unstable version) return the
+// Check that `atomic_xchg_seqcst` and other variants (unstable version) return the
 // expected result.
 
 #![feature(core_intrinsics)]
 use std::intrinsics::{
-    atomic_xchg, atomic_xchg_acq, atomic_xchg_acqrel, atomic_xchg_rel, atomic_xchg_relaxed,
+    atomic_xchg_acqrel, atomic_xchg_acquire, atomic_xchg_relaxed, atomic_xchg_release,
+    atomic_xchg_seqcst,
 };
 
 #[kani::proof]
@@ -28,14 +29,14 @@ fn main() {
         // Returns (val, ok) where
         //  * val: the old value
         //  * ok:  bool indicating whether the operation was successful or not
-        assert!(atomic_xchg(ptr_a1, 1) == 0);
-        assert!(atomic_xchg(ptr_a1, 0) == 1);
-        assert!(atomic_xchg_acq(ptr_a2, 1) == 0);
-        assert!(atomic_xchg_acq(ptr_a2, 0) == 1);
+        assert!(atomic_xchg_seqcst(ptr_a1, 1) == 0);
+        assert!(atomic_xchg_seqcst(ptr_a1, 0) == 1);
+        assert!(atomic_xchg_acquire(ptr_a2, 1) == 0);
+        assert!(atomic_xchg_acquire(ptr_a2, 0) == 1);
         assert!(atomic_xchg_acqrel(ptr_a3, 1) == 0);
         assert!(atomic_xchg_acqrel(ptr_a3, 0) == 1);
-        assert!(atomic_xchg_rel(ptr_a4, 1) == 0);
-        assert!(atomic_xchg_rel(ptr_a4, 0) == 1);
+        assert!(atomic_xchg_release(ptr_a4, 1) == 0);
+        assert!(atomic_xchg_release(ptr_a4, 0) == 1);
         assert!(atomic_xchg_relaxed(ptr_a5, 1) == 0);
         assert!(atomic_xchg_relaxed(ptr_a5, 0) == 1);
     }
diff --git a/tests/kani/Intrinsics/Atomic/Unstable/AtomicXor/main.rs b/tests/kani/Intrinsics/Atomic/Unstable/AtomicXor/main.rs
index 2ca0f05760ce..e9953aa7852d 100644
--- a/tests/kani/Intrinsics/Atomic/Unstable/AtomicXor/main.rs
+++ b/tests/kani/Intrinsics/Atomic/Unstable/AtomicXor/main.rs
@@ -1,12 +1,13 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-// Check that `atomic_xor` and other variants (unstable version) return the
+// Check that `atomic_xor_seqcst` and other variants (unstable version) return the
 // expected result.
 
 #![feature(core_intrinsics)]
 use std::intrinsics::{
-    atomic_xor, atomic_xor_acq, atomic_xor_acqrel, atomic_xor_rel, atomic_xor_relaxed,
+    atomic_xor_acqrel, atomic_xor_acquire, atomic_xor_relaxed, atomic_xor_release,
+    atomic_xor_seqcst,
 };
 
 #[kani::proof]
@@ -26,10 +27,10 @@ fn main() {
     let b = 1 as u8;
 
     unsafe {
-        let x1 = atomic_xor(ptr_a1, b);
-        let x2 = atomic_xor_acq(ptr_a2, b);
+        let x1 = atomic_xor_seqcst(ptr_a1, b);
+        let x2 = atomic_xor_acquire(ptr_a2, b);
         let x3 = atomic_xor_acqrel(ptr_a3, b);
-        let x4 = atomic_xor_rel(ptr_a4, b);
+        let x4 = atomic_xor_release(ptr_a4, b);
         let x5 = atomic_xor_relaxed(ptr_a5, b);
 
         assert!(x1 == 1);
diff --git a/tests/kani/Intrinsics/Copy/copy_nonoverlapping_append.rs b/tests/kani/Intrinsics/Copy/copy_nonoverlapping_append.rs
index a9c0d3a5eb9a..047c6bc2de60 100644
--- a/tests/kani/Intrinsics/Copy/copy_nonoverlapping_append.rs
+++ b/tests/kani/Intrinsics/Copy/copy_nonoverlapping_append.rs
@@ -6,6 +6,7 @@
 use std::ptr;
 
 #[kani::proof]
+#[kani::unwind(17)]
 fn test_append() {
     let mut a = vec!['r'];
     let mut b = vec!['u', 's', 't'];
diff --git a/tests/kani/Refs/main.rs b/tests/kani/Refs/main.rs
index a93e3f40f082..bfac8efb4aef 100644
--- a/tests/kani/Refs/main.rs
+++ b/tests/kani/Refs/main.rs
@@ -80,6 +80,7 @@ impl<'a> ArgParser<'a> {
 }
 
 #[kani::proof]
+#[kani::unwind(2)]
 fn main() {
     let a: ArgParser = ArgParser { arguments: BTreeMap::new() };
     a.format_arguments();
diff --git a/tests/ui/code-location/expected b/tests/ui/code-location/expected
index 6179fa7c8d96..3dc32e899534 100644
--- a/tests/ui/code-location/expected
+++ b/tests/ui/code-location/expected
@@ -1,7 +1,7 @@
 module/mod.rs:10:5 in function module::not_empty
 main.rs:13:5 in function same_file
 /toolchains/
-alloc/src/vec/mod.rs:2888:81 in function <std::vec::Vec<T, A> as std::ops::Drop>::drop
+alloc/src/vec/mod.rs:2920:81 in function <std::vec::Vec<T, A> as std::ops::Drop>::drop
 
 VERIFICATION:- SUCCESSFUL