diff --git a/src/test/cbmc/Assert/UninitValid/fixme_main_fail.rs b/src/test/cbmc/Assert/UninitValid/fixme_main.rs
similarity index 97%
rename from src/test/cbmc/Assert/UninitValid/fixme_main_fail.rs
rename to src/test/cbmc/Assert/UninitValid/fixme_main.rs
index 38541c2d355b..06c24dee9d53 100644
--- a/src/test/cbmc/Assert/UninitValid/fixme_main_fail.rs
+++ b/src/test/cbmc/Assert/UninitValid/fixme_main.rs
@@ -1,5 +1,7 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+// rmc-verify-fail
+
 use std::mem::{self, MaybeUninit};
 
 fn main() {
diff --git a/src/test/cbmc/Assert/ZeroValid/fixme_main_fail.rs b/src/test/cbmc/Assert/ZeroValid/fixme_main.rs
similarity index 96%
rename from src/test/cbmc/Assert/ZeroValid/fixme_main_fail.rs
rename to src/test/cbmc/Assert/ZeroValid/fixme_main.rs
index 435cfd18f1a7..805173c08f7d 100644
--- a/src/test/cbmc/Assert/ZeroValid/fixme_main_fail.rs
+++ b/src/test/cbmc/Assert/ZeroValid/fixme_main.rs
@@ -1,5 +1,7 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+// rmc-verify-fail
+
 // The function zeroed() calls assert_zero_valid to mark that it is only defined to assign an
 // all-zero bit pattern to a type T if this is a valid value. So the following is undefined.
 
diff --git a/src/test/cbmc/BinOp_Offset/main_fail.rs b/src/test/cbmc/BinOp_Offset/main_fail.rs
index 57014c62b0b1..49d4c3ea20aa 100644
--- a/src/test/cbmc/BinOp_Offset/main_fail.rs
+++ b/src/test/cbmc/BinOp_Offset/main_fail.rs
@@ -1,5 +1,7 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+// rmc-verify-fail
+
 include!("../../rmc-prelude.rs");
 
 pub fn test_offset_in_double_array() {
diff --git a/src/test/cbmc/BitManipulation/Stable/fixme_main_fail.rs b/src/test/cbmc/BitManipulation/Stable/fixme_main.rs
similarity index 97%
rename from src/test/cbmc/BitManipulation/Stable/fixme_main_fail.rs
rename to src/test/cbmc/BitManipulation/Stable/fixme_main.rs
index c1a9bee0a280..928572cc1c2c 100644
--- a/src/test/cbmc/BitManipulation/Stable/fixme_main_fail.rs
+++ b/src/test/cbmc/BitManipulation/Stable/fixme_main.rs
@@ -1,5 +1,7 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+// rmc-verify-fail
+
 fn main() {
     // Intrinsics implemented as integer primitives
     // https://doc.rust-lang.org/core/intrinsics/fn.cttz.html
diff --git a/src/test/cbmc/BitManipulation/Unstable/fixme_main_fail.rs b/src/test/cbmc/BitManipulation/Unstable/fixme_main.rs
similarity index 97%
rename from src/test/cbmc/BitManipulation/Unstable/fixme_main_fail.rs
rename to src/test/cbmc/BitManipulation/Unstable/fixme_main.rs
index 75e6331cea21..b892b70121e0 100644
--- a/src/test/cbmc/BitManipulation/Unstable/fixme_main_fail.rs
+++ b/src/test/cbmc/BitManipulation/Unstable/fixme_main.rs
@@ -1,5 +1,7 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+// rmc-verify-fail
+
 #![feature(core_intrinsics)]
 use std::intrinsics::{ctlz, cttz, cttz_nonzero};
 
diff --git a/src/test/cbmc/Count/Unstable/Ctlz/bounds_fail.rs b/src/test/cbmc/Count/Unstable/Ctlz/bounds.rs
similarity index 97%
rename from src/test/cbmc/Count/Unstable/Ctlz/bounds_fail.rs
rename to src/test/cbmc/Count/Unstable/Ctlz/bounds.rs
index deb91a6646e7..7db52aa63ab6 100644
--- a/src/test/cbmc/Count/Unstable/Ctlz/bounds_fail.rs
+++ b/src/test/cbmc/Count/Unstable/Ctlz/bounds.rs
@@ -1,6 +1,6 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-
+// rmc-verify-fail
 // cbmc-flags: --bounds-check
 
 #![feature(core_intrinsics)]
diff --git a/src/test/cbmc/Count/Unstable/Cttz/bounds_fail.rs b/src/test/cbmc/Count/Unstable/Cttz/bounds.rs
similarity index 97%
rename from src/test/cbmc/Count/Unstable/Cttz/bounds_fail.rs
rename to src/test/cbmc/Count/Unstable/Cttz/bounds.rs
index 5fa791853c05..0327087efa1a 100644
--- a/src/test/cbmc/Count/Unstable/Cttz/bounds_fail.rs
+++ b/src/test/cbmc/Count/Unstable/Cttz/bounds.rs
@@ -1,6 +1,6 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-
+// rmc-verify-fail
 // cbmc-flags: --bounds-check
 
 #![feature(core_intrinsics)]
diff --git a/src/test/cbmc/DynTrait/boxed_closure_fail_fixme.rs b/src/test/cbmc/DynTrait/boxed_closure_fail_fixme.rs
index c3a7f2cf90ef..54d8523b6945 100644
--- a/src/test/cbmc/DynTrait/boxed_closure_fail_fixme.rs
+++ b/src/test/cbmc/DynTrait/boxed_closure_fail_fixme.rs
@@ -1,10 +1,11 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+// rmc-verify-fail
 
 // Check that we can codegen a boxed dyn closure and fail an inner assertion
 
 // This current verifies "successfully" because the closure is not actually
-// called in the resulting CotoC code.
+// called in the resulting GotoC code.
 // https://github.com/model-checking/rmc/issues/240
 
 include!("../../rmc-prelude.rs");
diff --git a/src/test/cbmc/DynTrait/boxed_trait_fail.rs b/src/test/cbmc/DynTrait/boxed_trait_fail.rs
index b1d9de112430..9e690ef063eb 100644
--- a/src/test/cbmc/DynTrait/boxed_trait_fail.rs
+++ b/src/test/cbmc/DynTrait/boxed_trait_fail.rs
@@ -1,5 +1,6 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+// rmc-verify-fail
 
 // Dynamic traits should work when used through a box
 // _fail test; all assertions inverted.
diff --git a/src/test/cbmc/DynTrait/different_crates_fail.rs b/src/test/cbmc/DynTrait/different_crates_fail.rs
index 2a8211b4da97..3b7c47fe2338 100644
--- a/src/test/cbmc/DynTrait/different_crates_fail.rs
+++ b/src/test/cbmc/DynTrait/different_crates_fail.rs
@@ -1,5 +1,6 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+// rmc-verify-fail
 
 // This test uses a trait defined in a different crate (the standard library)
 // and a test defined in the local crate. The goal is to test vtable resolution
diff --git a/src/test/cbmc/DynTrait/nested_boxes_fail.rs b/src/test/cbmc/DynTrait/nested_boxes_fail.rs
index d3001ddb8053..fd6a6332a35f 100644
--- a/src/test/cbmc/DynTrait/nested_boxes_fail.rs
+++ b/src/test/cbmc/DynTrait/nested_boxes_fail.rs
@@ -1,5 +1,6 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+// rmc-verify-fail
 
 // This test checks the size and align fields for 3-deep nested trait pointers. The
 // outter 2 dynamic trait objects have fat pointers as their backing data.
diff --git a/src/test/cbmc/FatPointers/boxmuttrait_fail.rs b/src/test/cbmc/FatPointers/boxmuttrait_fail.rs
index 51a621cc56c4..63233d093455 100644
--- a/src/test/cbmc/FatPointers/boxmuttrait_fail.rs
+++ b/src/test/cbmc/FatPointers/boxmuttrait_fail.rs
@@ -1,5 +1,6 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+// rmc-verify-fail
 
 use std::io::{sink, Write};
 
diff --git a/src/test/cbmc/FatPointers/boxslice1.rs b/src/test/cbmc/FatPointers/boxslice1.rs
index eaca29c49e01..91e29de5ceaf 100644
--- a/src/test/cbmc/FatPointers/boxslice1.rs
+++ b/src/test/cbmc/FatPointers/boxslice1.rs
@@ -11,5 +11,5 @@ fn main() {
     // This transformer produces a Box<[u8]>
     let _sparkle_heart_str = str::from_utf8(&sparkle_heart_vec);
 
-    // see boxslice2_fail.rs for an attempt to test sparkle_heart_str
+    // see boxslice2.rs for an attempt to test sparkle_heart_str
 }
diff --git a/src/test/cbmc/FatPointers/boxslice2_fail.rs b/src/test/cbmc/FatPointers/boxslice2.rs
similarity index 97%
rename from src/test/cbmc/FatPointers/boxslice2_fail.rs
rename to src/test/cbmc/FatPointers/boxslice2.rs
index 7e809e1606e9..c5c103e36213 100644
--- a/src/test/cbmc/FatPointers/boxslice2_fail.rs
+++ b/src/test/cbmc/FatPointers/boxslice2.rs
@@ -1,5 +1,6 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+// rmc-verify-fail
 
 // Casts boxed array to boxed slice (example taken from rust documentation)
 use std::str;
diff --git a/src/test/cbmc/FatPointers/boxtrait_fail.rs b/src/test/cbmc/FatPointers/boxtrait_fail.rs
index de5947149011..05d650bb8bc3 100644
--- a/src/test/cbmc/FatPointers/boxtrait_fail.rs
+++ b/src/test/cbmc/FatPointers/boxtrait_fail.rs
@@ -1,5 +1,6 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+// rmc-verify-fail
 
 // This is handled by the box to box case of unsized pointers
 
diff --git a/src/test/cbmc/FatPointers/trait1_fail.rs b/src/test/cbmc/FatPointers/trait1_fail.rs
index 05fd76a2df04..1cb23c38f0c4 100644
--- a/src/test/cbmc/FatPointers/trait1_fail.rs
+++ b/src/test/cbmc/FatPointers/trait1_fail.rs
@@ -1,5 +1,6 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+// rmc-verify-fail
 
 // Cast a concrete ref to a trait ref.
 
diff --git a/src/test/cbmc/FatPointers/trait2_fail.rs b/src/test/cbmc/FatPointers/trait2_fail.rs
index d7f535bc0890..50de1a127e0a 100644
--- a/src/test/cbmc/FatPointers/trait2_fail.rs
+++ b/src/test/cbmc/FatPointers/trait2_fail.rs
@@ -1,5 +1,6 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+// rmc-verify-fail
 
 // Cast a concrete ref to a trait raw pointer.
 
diff --git a/src/test/cbmc/FatPointers/trait3_fail.rs b/src/test/cbmc/FatPointers/trait3_fail.rs
index 04898500e7d8..5a1fca792443 100644
--- a/src/test/cbmc/FatPointers/trait3_fail.rs
+++ b/src/test/cbmc/FatPointers/trait3_fail.rs
@@ -1,5 +1,6 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+// rmc-verify-fail
 
 // Cast a concrete ref to
 //   concrete raw pointer
diff --git a/src/test/cbmc/Intrinsics/abort_fail.rs b/src/test/cbmc/Intrinsics/abort.rs
similarity index 91%
rename from src/test/cbmc/Intrinsics/abort_fail.rs
rename to src/test/cbmc/Intrinsics/abort.rs
index c45a069b7a5f..fc445524774d 100644
--- a/src/test/cbmc/Intrinsics/abort_fail.rs
+++ b/src/test/cbmc/Intrinsics/abort.rs
@@ -1,5 +1,7 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+// rmc-verify-fail
+
 #![feature(core_intrinsics)]
 use std::intrinsics;
 fn main() {
diff --git a/src/test/cbmc/PointerOffset/Unstable/main_fail.rs b/src/test/cbmc/PointerOffset/Unstable/main_fail.rs
index 1579b97c1e75..a7ced6f3510b 100644
--- a/src/test/cbmc/PointerOffset/Unstable/main_fail.rs
+++ b/src/test/cbmc/PointerOffset/Unstable/main_fail.rs
@@ -1,5 +1,7 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+// rmc-verify-fail
+
 #![feature(core_intrinsics)]
 use std::intrinsics::ptr_offset_from;
 
diff --git a/src/test/cbmc/Pointers_Basic/fixme_from_raw_fail.rs b/src/test/cbmc/Pointers_Basic/fixme_from_raw.rs
similarity index 95%
rename from src/test/cbmc/Pointers_Basic/fixme_from_raw_fail.rs
rename to src/test/cbmc/Pointers_Basic/fixme_from_raw.rs
index b3a25e21e58f..ea8d8c3271ca 100644
--- a/src/test/cbmc/Pointers_Basic/fixme_from_raw_fail.rs
+++ b/src/test/cbmc/Pointers_Basic/fixme_from_raw.rs
@@ -1,5 +1,6 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+// rmc-verify-fail
 
 fn main() {
     let address = 0x01234usize;
diff --git a/src/test/cbmc/Pointers_OutOfScopeFail/fixme_main_fail.rs b/src/test/cbmc/Pointers_OutOfScopeFail/fixme_main.rs
similarity index 96%
rename from src/test/cbmc/Pointers_OutOfScopeFail/fixme_main_fail.rs
rename to src/test/cbmc/Pointers_OutOfScopeFail/fixme_main.rs
index 43c97aef82bd..744213ee8767 100644
--- a/src/test/cbmc/Pointers_OutOfScopeFail/fixme_main_fail.rs
+++ b/src/test/cbmc/Pointers_OutOfScopeFail/fixme_main.rs
@@ -1,5 +1,7 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+// rmc-verify-fail
+
 fn main() {
     // declare pointer to integer
     let p_subscoped: *const u32;
diff --git a/src/test/cbmc/SIMD/Compare/main_fail.rs b/src/test/cbmc/SIMD/Compare/main.rs
similarity index 98%
rename from src/test/cbmc/SIMD/Compare/main_fail.rs
rename to src/test/cbmc/SIMD/Compare/main.rs
index 2e45f0b6f327..adfd84cc1376 100644
--- a/src/test/cbmc/SIMD/Compare/main_fail.rs
+++ b/src/test/cbmc/SIMD/Compare/main.rs
@@ -1,5 +1,7 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+// rmc-verify-fail
+
 #![feature(repr_simd, platform_intrinsics)]
 
 #[repr(simd)]
diff --git a/src/test/cbmc/Serde/main_fail.rs b/src/test/cbmc/Serde/main.rs
similarity index 96%
rename from src/test/cbmc/Serde/main_fail.rs
rename to src/test/cbmc/Serde/main.rs
index 688f430ae39d..acd38b53b2e7 100644
--- a/src/test/cbmc/Serde/main_fail.rs
+++ b/src/test/cbmc/Serde/main.rs
@@ -1,5 +1,7 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+// rmc-check-fail
+
 // We currently assert(false) for reify function pointer.
 // So this codegens but fails model checking.
 
diff --git a/src/test/cbmc/SizeAndAlignOfDst/main_fail.rs b/src/test/cbmc/SizeAndAlignOfDst/main_fail.rs
index 700a5477f3b7..2fffc98fc27f 100644
--- a/src/test/cbmc/SizeAndAlignOfDst/main_fail.rs
+++ b/src/test/cbmc/SizeAndAlignOfDst/main_fail.rs
@@ -5,6 +5,7 @@
 // Arc<Mutex<dyn Subscriber>>.
 // This test still fails with a final coercion error for
 // DummySubscriber to dyn Subscriber.
+// rmc-verify-fail
 
 use std::sync::Arc;
 use std::sync::Mutex;
diff --git a/src/test/cbmc/Slice/drop_in_place_fail.rs b/src/test/cbmc/Slice/drop_in_place.rs
similarity index 95%
rename from src/test/cbmc/Slice/drop_in_place_fail.rs
rename to src/test/cbmc/Slice/drop_in_place.rs
index 6157653dcd6f..d02a9c473b0f 100644
--- a/src/test/cbmc/Slice/drop_in_place_fail.rs
+++ b/src/test/cbmc/Slice/drop_in_place.rs
@@ -1,5 +1,7 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+// rmc-check-fail
+
 #[allow(unconditional_recursion)]
 pub unsafe fn drop_in_place<T: ?Sized>(to_drop: *mut T) {
     // Code here does not matter - this is replaced by the
diff --git a/src/test/cbmc/Slice/pathbuf_fail.rs b/src/test/cbmc/Slice/pathbuf.rs
similarity index 92%
rename from src/test/cbmc/Slice/pathbuf_fail.rs
rename to src/test/cbmc/Slice/pathbuf.rs
index 76dc80fd2a9a..d7c886914369 100644
--- a/src/test/cbmc/Slice/pathbuf_fail.rs
+++ b/src/test/cbmc/Slice/pathbuf.rs
@@ -1,5 +1,7 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+// rmc-verify-fail
+
 use std::fs;
 use std::path::PathBuf;
 pub fn main() {
diff --git a/src/test/cbmc/Slice/slice_from_raw_fail.rs b/src/test/cbmc/Slice/slice_from_raw.rs
similarity index 96%
rename from src/test/cbmc/Slice/slice_from_raw_fail.rs
rename to src/test/cbmc/Slice/slice_from_raw.rs
index 4d180f461ef6..49cf8257c204 100644
--- a/src/test/cbmc/Slice/slice_from_raw_fail.rs
+++ b/src/test/cbmc/Slice/slice_from_raw.rs
@@ -1,5 +1,7 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+// rmc-verify-fail
+
 use std::slice;
 
 include!("../../rmc-prelude.rs");
diff --git a/src/test/cbmc/VolatileIntrinsics/core_intrinsics.rs b/src/test/cbmc/VolatileIntrinsics/core_intrinsics.rs
new file mode 100644
index 000000000000..31f019a03b37
--- /dev/null
+++ b/src/test/cbmc/VolatileIntrinsics/core_intrinsics.rs
@@ -0,0 +1,21 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// rmc-codegen-fail
+
+#![feature(core_intrinsics)]
+
+use std::intrinsics::*;
+
+pub fn main() {
+    let mut a: Box<u8> = Box::new(0);
+    unsafe {
+        let x = volatile_load(&*a);
+        assert!(x == *a);
+        volatile_store(&mut *a, 1);
+        assert!(*a == 1);
+        unaligned_volatile_store(&mut *a, 2);
+        assert!(*a == 2);
+        volatile_set_memory(&mut *a, 3, 1);
+        assert!(*a == 3);
+    }
+}
diff --git a/src/test/prusti/Binary_search_fail.rs b/src/test/prusti/Binary_search.rs
similarity index 96%
rename from src/test/prusti/Binary_search_fail.rs
rename to src/test/prusti/Binary_search.rs
index 40223377b0ac..f6c3c2ef49f3 100644
--- a/src/test/prusti/Binary_search_fail.rs
+++ b/src/test/prusti/Binary_search.rs
@@ -1,6 +1,6 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-
+// rmc-verify-fail
 // cbmc-flags: --unwind 4
 
 use std::cmp::Ordering::*;
@@ -43,7 +43,7 @@ fn binary_search<T: Ord>(arr: &[T], elem: &T) -> Option<usize> {
     None
 }
 
-include!("../../rmc-prelude.rs");
+include!("../rmc-prelude.rs");
 
 fn get() -> [i32; 11] {
     [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11]
diff --git a/src/test/smack/basic/add_fail.rs b/src/test/smack/basic/add.rs
similarity index 91%
rename from src/test/smack/basic/add_fail.rs
rename to src/test/smack/basic/add.rs
index a826ffbb3506..dab1e8ad1ae7 100644
--- a/src/test/smack/basic/add_fail.rs
+++ b/src/test/smack/basic/add.rs
@@ -1,6 +1,7 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // @expect error
+// rmc-verify-fail
 
 pub fn main() {
     let a = 2;
diff --git a/src/test/smack/basic/arith_assume_fail.rs b/src/test/smack/basic/arith_assume3.rs
similarity index 97%
rename from src/test/smack/basic/arith_assume_fail.rs
rename to src/test/smack/basic/arith_assume3.rs
index 7277374fd299..b279588af7de 100644
--- a/src/test/smack/basic/arith_assume_fail.rs
+++ b/src/test/smack/basic/arith_assume3.rs
@@ -1,6 +1,7 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // @expect error
+// rmc-verify-fail
 
 include!("../../rmc-prelude.rs");
 
diff --git a/src/test/smack/basic/div_fail.rs b/src/test/smack/basic/div.rs
similarity index 91%
rename from src/test/smack/basic/div_fail.rs
rename to src/test/smack/basic/div.rs
index 7a389fc0d288..4dfd34404679 100644
--- a/src/test/smack/basic/div_fail.rs
+++ b/src/test/smack/basic/div.rs
@@ -1,6 +1,7 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // @expect error
+// rmc-verify-fail
 
 pub fn main() {
     let a = 2;
diff --git a/src/test/smack/basic/mod_fail.rs b/src/test/smack/basic/mod.rs
similarity index 91%
rename from src/test/smack/basic/mod_fail.rs
rename to src/test/smack/basic/mod.rs
index 6b09f95769d2..e586bc34092d 100644
--- a/src/test/smack/basic/mod_fail.rs
+++ b/src/test/smack/basic/mod.rs
@@ -1,6 +1,7 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // @expect error
+// rmc-verify-fail
 
 pub fn main() {
     let a = 2;
diff --git a/src/test/smack/basic/mul_fail.rs b/src/test/smack/basic/mul.rs
similarity index 91%
rename from src/test/smack/basic/mul_fail.rs
rename to src/test/smack/basic/mul.rs
index fb1e73e40daf..1b9cbcc10ce0 100644
--- a/src/test/smack/basic/mul_fail.rs
+++ b/src/test/smack/basic/mul.rs
@@ -1,6 +1,7 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // @expect error
+// rmc-verify-fail
 
 pub fn main() {
     let a = 2;
diff --git a/src/test/smack/basic/sub_fail.rs b/src/test/smack/basic/sub.rs
similarity index 91%
rename from src/test/smack/basic/sub_fail.rs
rename to src/test/smack/basic/sub.rs
index be2b46a4d82e..aa79dadd0209 100644
--- a/src/test/smack/basic/sub_fail.rs
+++ b/src/test/smack/basic/sub.rs
@@ -1,6 +1,7 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // @expect error
+// rmc-verify-fail
 
 pub fn main() {
     let a = 2;
diff --git a/src/test/smack/functions/closure_fail.rs b/src/test/smack/functions/closure_fail.rs
index 975be573a716..e858e3c87858 100644
--- a/src/test/smack/functions/closure_fail.rs
+++ b/src/test/smack/functions/closure_fail.rs
@@ -2,6 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // @flag --no-memory-splitting
 // @expect verified
+// rmc-verify-fail
 
 fn call_with_one<F>(mut some_closure: F) -> ()
 where
diff --git a/src/test/smack/functions/double_fail.rs b/src/test/smack/functions/double_fail.rs
index df39e066f7f7..3e3d9597d007 100644
--- a/src/test/smack/functions/double_fail.rs
+++ b/src/test/smack/functions/double_fail.rs
@@ -1,6 +1,7 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // @expect error
+// rmc-verify-fail
 
 fn double(a: u32) -> u32 {
     a * 2
diff --git a/src/test/smack/generics/generic_function_fail1.rs b/src/test/smack/generics/generic_function1.rs
similarity index 98%
rename from src/test/smack/generics/generic_function_fail1.rs
rename to src/test/smack/generics/generic_function1.rs
index cc1c80489620..d97897373533 100644
--- a/src/test/smack/generics/generic_function_fail1.rs
+++ b/src/test/smack/generics/generic_function1.rs
@@ -1,6 +1,7 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // @expect error
+// rmc-verify-fail
 
 struct Point<T> {
     pub x: T,
diff --git a/src/test/smack/generics/generic_function_fail2.rs b/src/test/smack/generics/generic_function2.rs
similarity index 98%
rename from src/test/smack/generics/generic_function_fail2.rs
rename to src/test/smack/generics/generic_function2.rs
index b4d1cdee484d..a45f5d17a328 100644
--- a/src/test/smack/generics/generic_function_fail2.rs
+++ b/src/test/smack/generics/generic_function2.rs
@@ -1,6 +1,7 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // @expect error
+// rmc-verify-fail
 
 struct Point<T> {
     pub x: T,
diff --git a/src/test/smack/generics/generic_function_fail3.rs b/src/test/smack/generics/generic_function3.rs
similarity index 98%
rename from src/test/smack/generics/generic_function_fail3.rs
rename to src/test/smack/generics/generic_function3.rs
index 7156b3fd35f4..c2f7f742be1c 100644
--- a/src/test/smack/generics/generic_function_fail3.rs
+++ b/src/test/smack/generics/generic_function3.rs
@@ -1,6 +1,7 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // @expect error
+// rmc-verify-fail
 
 struct Point<T> {
     pub x: T,
diff --git a/src/test/smack/generics/generic_function_fail4.rs b/src/test/smack/generics/generic_function4.rs
similarity index 98%
rename from src/test/smack/generics/generic_function_fail4.rs
rename to src/test/smack/generics/generic_function4.rs
index ae3dfeb72cd6..52f4f5d3b4fd 100644
--- a/src/test/smack/generics/generic_function_fail4.rs
+++ b/src/test/smack/generics/generic_function4.rs
@@ -1,6 +1,7 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // @expect verified
+// rmc-verify-fail
 
 struct Point<T> {
     pub x: T,
diff --git a/src/test/smack/generics/generic_function_fail5.rs b/src/test/smack/generics/generic_function5.rs
similarity index 98%
rename from src/test/smack/generics/generic_function_fail5.rs
rename to src/test/smack/generics/generic_function5.rs
index 2cac16cda9af..1f9369510df5 100644
--- a/src/test/smack/generics/generic_function_fail5.rs
+++ b/src/test/smack/generics/generic_function5.rs
@@ -1,6 +1,7 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // @expect verified
+// rmc-verify-fail
 
 struct Point<T> {
     pub x: T,
diff --git a/src/test/smack/loops/gauss_sum_nondet.rs b/src/test/smack/loops/gauss_sum_nondet.rs
index 33c70312017f..6f57722d8ea0 100644
--- a/src/test/smack/loops/gauss_sum_nondet.rs
+++ b/src/test/smack/loops/gauss_sum_nondet.rs
@@ -2,7 +2,6 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // @flag --no-memory-splitting --unroll=4
 // @expect verified
-
 // cbmc-flags: --unwind 5
 
 include!("../../rmc-prelude.rs");
diff --git a/src/test/smack/loops/gauss_sum_nondet_fail.rs b/src/test/smack/loops/gauss_sum_nondet_fail.rs
index d29f31dc2d50..43045d2f1566 100644
--- a/src/test/smack/loops/gauss_sum_nondet_fail.rs
+++ b/src/test/smack/loops/gauss_sum_nondet_fail.rs
@@ -2,7 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // @flag --no-memory-splitting --unroll=10
 // @expect error
-
+// rmc-verify-fail
 // cbmc-flags: --unwind 5
 
 include!("../../rmc-prelude.rs");
diff --git a/src/test/smack/loops/iterator_fail.rs b/src/test/smack/loops/iterator_fail.rs
index 72fca0cf5134..4a5b537d8582 100644
--- a/src/test/smack/loops/iterator_fail.rs
+++ b/src/test/smack/loops/iterator_fail.rs
@@ -2,7 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // @flag --no-memory-splitting --unroll=10
 // @expect error
-
+// rmc-verify-fail
 // cbmc-flags: --unwind 5
 
 fn fac(n: u64) -> u64 {
diff --git a/src/test/smack/overflow/add_overflow_fail.rs b/src/test/smack/overflow/add_overflow.rs
similarity index 93%
rename from src/test/smack/overflow/add_overflow_fail.rs
rename to src/test/smack/overflow/add_overflow.rs
index 3ba735e6c281..e9f8d3f5774c 100644
--- a/src/test/smack/overflow/add_overflow_fail.rs
+++ b/src/test/smack/overflow/add_overflow.rs
@@ -2,6 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // @flag --integer-overflow
 // @expect overflow
+// rmc-verify-fail
 
 pub fn get128() -> u8 {
     128
diff --git a/src/test/smack/overflow/mul_overflow_fail.rs b/src/test/smack/overflow/mul_overflow.rs
similarity index 93%
rename from src/test/smack/overflow/mul_overflow_fail.rs
rename to src/test/smack/overflow/mul_overflow.rs
index 7fc95268c842..a89509d7e611 100644
--- a/src/test/smack/overflow/mul_overflow_fail.rs
+++ b/src/test/smack/overflow/mul_overflow.rs
@@ -2,6 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // @flag --integer-overflow
 // @expect overflow
+// rmc-verify-fail
 
 fn get128() -> u8 {
     128
diff --git a/src/test/smack/overflow/sub_overflow_fail.rs b/src/test/smack/overflow/sub_overflow.rs
similarity index 93%
rename from src/test/smack/overflow/sub_overflow_fail.rs
rename to src/test/smack/overflow/sub_overflow.rs
index 557968972608..fce508a36ab6 100644
--- a/src/test/smack/overflow/sub_overflow_fail.rs
+++ b/src/test/smack/overflow/sub_overflow.rs
@@ -2,6 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // @flag --integer-overflow
 // @expect overflow
+// rmc-verify-fail
 
 fn get128() -> u8 {
     128
diff --git a/src/test/smack/recursion/fac_fail.rs b/src/test/smack/recursion/fac_fail.rs
index 8da67d48ed9e..47ab6439cfbc 100644
--- a/src/test/smack/recursion/fac_fail.rs
+++ b/src/test/smack/recursion/fac_fail.rs
@@ -2,6 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // @flag --unroll=10
 // @expect error
+// rmc-verify-fail
 
 fn fac(n: u64, acc: u64) -> u64 {
     match n {
diff --git a/src/test/smack/recursion/fib_fail.rs b/src/test/smack/recursion/fib_fail.rs
index 14cba9bb9ee4..537203831b4a 100644
--- a/src/test/smack/recursion/fib_fail.rs
+++ b/src/test/smack/recursion/fib_fail.rs
@@ -2,6 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // @flag --unroll=10
 // @expect error
+// rmc-verify-fail
 
 fn fib(x: u64) -> u64 {
     match x {
diff --git a/src/test/smack/structures/option_fail.rs b/src/test/smack/structures/option_fail.rs
index 5e2bfe77348f..70a835f62f07 100644
--- a/src/test/smack/structures/option_fail.rs
+++ b/src/test/smack/structures/option_fail.rs
@@ -1,6 +1,7 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // @expect reachable
+// rmc-verify-fail
 
 fn safe_div(x: u32, y: u32) -> Option<u32> {
     if y != 0 { Some(x / y) } else { None }
diff --git a/src/test/smack/structures/point_fail.rs b/src/test/smack/structures/point_fail.rs
index 4361f98bcbb7..8d6895a9b0c7 100644
--- a/src/test/smack/structures/point_fail.rs
+++ b/src/test/smack/structures/point_fail.rs
@@ -1,6 +1,7 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // @expect error
+// rmc-verify-fail
 
 use std::ops::{Add, AddAssign};
 
diff --git a/src/test/smack/vector/vec1_fail1.rs b/src/test/smack/vector/vec11.rs
similarity index 95%
rename from src/test/smack/vector/vec1_fail1.rs
rename to src/test/smack/vector/vec11.rs
index bf164d34d4ca..858c17a1a08c 100644
--- a/src/test/smack/vector/vec1_fail1.rs
+++ b/src/test/smack/vector/vec11.rs
@@ -2,6 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // @flag --no-memory-splitting
 // @expect error
+// rmc-verify-fail
 
 pub fn main() {
     let mut v: Vec<u64> = Vec::new();
diff --git a/src/test/smack/vector/vec1_fail2.rs b/src/test/smack/vector/vec12.rs
similarity index 95%
rename from src/test/smack/vector/vec1_fail2.rs
rename to src/test/smack/vector/vec12.rs
index dd7b910164d4..4c5d8ce96614 100644
--- a/src/test/smack/vector/vec1_fail2.rs
+++ b/src/test/smack/vector/vec12.rs
@@ -2,6 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // @flag --no-memory-splitting
 // @expect error
+// rmc-verify-fail
 
 pub fn main() {
     let mut v: Vec<u64> = Vec::new();
diff --git a/src/test/smack/vector/vec1_fail3.rs b/src/test/smack/vector/vec13.rs
similarity index 95%
rename from src/test/smack/vector/vec1_fail3.rs
rename to src/test/smack/vector/vec13.rs
index 7843d004179d..0ce12dcfcae4 100644
--- a/src/test/smack/vector/vec1_fail3.rs
+++ b/src/test/smack/vector/vec13.rs
@@ -2,6 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // @flag --no-memory-splitting
 // @expect error
+// rmc-verify-fail
 
 pub fn main() {
     let mut v: Vec<u64> = Vec::new();
diff --git a/src/test/smack/vector/vec_resize_fail.rs b/src/test/smack/vector/vec_resize_fail.rs
index 07377c1a5973..ca7ae526ee66 100644
--- a/src/test/smack/vector/vec_resize_fail.rs
+++ b/src/test/smack/vector/vec_resize_fail.rs
@@ -2,6 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // @flag --no-memory-splitting --unroll=3
 // @expect error
+// rmc-verify-fail
 
 pub fn main() {
     let mut v1: Vec<u64> = vec![0];
diff --git a/src/tools/compiletest/src/common.rs b/src/tools/compiletest/src/common.rs
index 0108b66f05b8..240f4cf30694 100644
--- a/src/tools/compiletest/src/common.rs
+++ b/src/tools/compiletest/src/common.rs
@@ -118,6 +118,21 @@ impl fmt::Display for PassMode {
     }
 }
 
+/// Step at which RMC test should fail.
+#[derive(Copy, Clone, Debug, PartialEq, PartialOrd)]
+pub enum RMCFailStep {
+    /// RMC panics before the codegen step (up to MIR generation). This step
+    /// runs the same checks on the test code as `cargo check` including syntax,
+    /// type, name resolution, and borrow checks.
+    Check,
+    /// RMC panics at the codegen step because the test code uses unimplemented
+    /// and/or unsupported features.
+    Codegen,
+    /// RMC panics after the codegen step because of verification failures or
+    /// other CBMC errors.
+    Verify,
+}
+
 #[derive(Copy, Clone, Debug, PartialEq, PartialOrd)]
 pub enum FailMode {
     Check,
diff --git a/src/tools/compiletest/src/header.rs b/src/tools/compiletest/src/header.rs
index 40c13a7b4144..4704a240c97b 100644
--- a/src/tools/compiletest/src/header.rs
+++ b/src/tools/compiletest/src/header.rs
@@ -7,7 +7,9 @@ use std::path::{Path, PathBuf};
 
 use tracing::*;
 
-use crate::common::{CompareMode, Config, Debugger, FailMode, Mode, PanicStrategy, PassMode};
+use crate::common::{
+    CompareMode, Config, Debugger, FailMode, Mode, PanicStrategy, PassMode, RMCFailStep,
+};
 use crate::util;
 use crate::{extract_cdb_version, extract_gdb_version};
 
@@ -121,6 +123,8 @@ pub struct TestProps {
     pass_mode: Option<PassMode>,
     // Ignore `--pass` overrides from the command line for this test.
     ignore_pass: bool,
+    // At which step is the RMC test expected to fail.
+    pub rmc_panic_step: Option<RMCFailStep>,
     // How far this test should proceed to start failing.
     pub fail_mode: Option<FailMode>,
     // rustdoc will test the output of the `--test` option
@@ -170,6 +174,7 @@ impl TestProps {
             forbid_output: vec![],
             incremental_dir: None,
             pass_mode: None,
+            rmc_panic_step: None,
             fail_mode: None,
             ignore_pass: false,
             check_test_line_numbers_match: false,
@@ -331,6 +336,7 @@ impl TestProps {
                 }
 
                 self.update_pass_mode(ln, cfg, config);
+                self.update_rmc_fail_mode(ln, config);
                 self.update_fail_mode(ln, config);
 
                 if !self.ignore_pass {
@@ -383,6 +389,17 @@ impl TestProps {
         }
     }
 
+    /// Checks if `ln` specifies which stage the test should fail on and updates
+    /// RMC fail mode accordingly.
+    fn update_rmc_fail_mode(&mut self, ln: &str, config: &Config) {
+        let rmc_fail_step = config.parse_rmc_step_fail_directive(ln);
+        match (self.rmc_panic_step, rmc_fail_step) {
+            (None, Some(_)) => self.rmc_panic_step = rmc_fail_step,
+            (Some(_), Some(_)) => panic!("multiple `rmc-*-fail` headers in a single test"),
+            (_, None) => {}
+        }
+    }
+
     fn update_fail_mode(&mut self, ln: &str, config: &Config) {
         let check_ui = |mode: &str| {
             if config.mode != Mode::Ui {
@@ -526,6 +543,28 @@ impl Config {
         self.parse_name_value_directive(line, "compile-flags")
     }
 
+    /// Parses strings of the form `rmc-*-fail` and returns the step at which
+    /// RMC is expected to panic.
+    fn parse_rmc_step_fail_directive(&self, line: &str) -> Option<RMCFailStep> {
+        let check_rmc = |mode: &str| {
+            if self.mode != Mode::RMC {
+                panic!("`rmc-{}-fail` header is only supported in RMC tests", mode);
+            }
+        };
+        if self.parse_name_directive(line, "rmc-check-fail") {
+            check_rmc("check");
+            Some(RMCFailStep::Check)
+        } else if self.parse_name_directive(line, "rmc-codegen-fail") {
+            check_rmc("codegen");
+            Some(RMCFailStep::Codegen)
+        } else if self.parse_name_directive(line, "rmc-verify-fail") {
+            check_rmc("verify");
+            Some(RMCFailStep::Verify)
+        } else {
+            None
+        }
+    }
+
     /// Parses strings of the form `// rmc-flags: ...` and returns the options listed after `rmc-flags:`
     fn parse_rmc_flags(&self, line: &str) -> Option<String> {
         self.parse_name_value_directive(line, "rmc-flags")
diff --git a/src/tools/compiletest/src/runtest.rs b/src/tools/compiletest/src/runtest.rs
index 9635f0929cbe..417310e9a59b 100644
--- a/src/tools/compiletest/src/runtest.rs
+++ b/src/tools/compiletest/src/runtest.rs
@@ -1,6 +1,8 @@
 // ignore-tidy-filelength
 
-use crate::common::{expected_output_path, UI_EXTENSIONS, UI_FIXED, UI_STDERR, UI_STDOUT};
+use crate::common::{
+    expected_output_path, RMCFailStep, UI_EXTENSIONS, UI_FIXED, UI_STDERR, UI_STDOUT,
+};
 use crate::common::{output_base_dir, output_base_name, output_testname_unique};
 use crate::common::{
     Assembly, CargoRMC, Expected, Incremental, JsDocTest, MirOpt, RunMake, RustdocJson, Ui, RMC,
@@ -400,7 +402,6 @@ impl<'test> TestCx<'test> {
                     panic!("revision name must begin with rpass, rfail, or cfail");
                 }
             }
-            RMC => !self.testpaths.file.to_str().unwrap().contains("fail"),
             mode => panic!("unimplemented for mode {:?}", mode),
         }
     }
@@ -2392,20 +2393,69 @@ impl<'test> TestCx<'test> {
     }
 
     /// Adds rmc scripts directory to the `PATH` environment variable.
-    fn add_rmc_dir_to_path(&self, rmc: &mut Command) {
+    fn add_rmc_dir_to_path(&self, command: &mut Command) {
         // If the PATH enviornment variable is already defined,
         if let Some((key, val)) = env::vars().find(|(key, _)| key == "PATH") {
             // Add the RMC scripts directory to the PATH.
-            rmc.env(key, format!("{}:{}", self.config.rmc_dir_path.to_str().unwrap(), val));
+            command.env(key, format!("{}:{}", self.config.rmc_dir_path.to_str().unwrap(), val));
         } else {
             // Otherwise, insert PATH as a new enviornment variable and set its value to the RMC scripts directory.
-            rmc.env(String::from("PATH"), String::from(self.config.rmc_dir_path.to_str().unwrap()));
+            command.env(
+                String::from("PATH"),
+                String::from(self.config.rmc_dir_path.to_str().unwrap()),
+            );
+        }
+    }
+
+    /// Runs `rmc-rustc` on the test file specified by `self.testpaths.file`. An
+    /// error message is printed to stdout if the check result is not expected.
+    fn check(&self) {
+        let mut rustc = Command::new("rmc-rustc");
+        rustc.args(["-Z", "no-codegen"]).arg(&self.testpaths.file);
+        self.add_rmc_dir_to_path(&mut rustc);
+        let proc_res = self.compose_and_run_compiler(rustc, None);
+        if self.props.rmc_panic_step == Some(RMCFailStep::Check) {
+            if proc_res.status.success() {
+                self.fatal_proc_rec("test failed: expected check failure, got success", &proc_res);
+            }
+        } else {
+            if !proc_res.status.success() {
+                self.fatal_proc_rec("test failed: expected check success, got failure", &proc_res);
+            }
+        }
+    }
+
+    /// Runs `rmc-rustc` on the test file specified by `self.testpaths.file`. An
+    /// error message is printed to stdout if the codegen result is not
+    /// expected.
+    fn codegen(&self) {
+        let mut rustc = Command::new("rmc-rustc");
+        rustc
+            .args(["-Z", "codegen-backend=gotoc", "--cfg=rmc", "--out-dir"])
+            .arg(self.output_base_dir())
+            .arg(&self.testpaths.file);
+        self.add_rmc_dir_to_path(&mut rustc);
+        let proc_res = self.compose_and_run_compiler(rustc, None);
+        if self.props.rmc_panic_step == Some(RMCFailStep::Codegen) {
+            if proc_res.status.success() {
+                self.fatal_proc_rec(
+                    "test failed: expected codegen failure, got success",
+                    &proc_res,
+                );
+            }
+        } else {
+            if !proc_res.status.success() {
+                self.fatal_proc_rec(
+                    "test failed: expected codegen success, got failure",
+                    &proc_res,
+                );
+            }
         }
     }
 
     /// Runs RMC on the test file specified by `self.testpaths.file`. An error
-    /// message is printed to stdout if verification result is not expected.
-    fn run_rmc_test(&self) {
+    /// message is printed to stdout if the verification result is not expected.
+    fn verify(&self) {
         // Other modes call self.compile_test(...). However, we cannot call it here for two reasons:
         // 1. It calls rustc instead of RMC
         // 2. It may pass some options that do not make sense for RMC
@@ -2443,18 +2493,39 @@ impl<'test> TestCx<'test> {
                 )
             }
             // Print an error if the verification result is not expected.
-            if self.should_compile_successfully(self.pass_mode()) {
-                if !proc_res.status.success() {
-                    self.fatal_proc_rec("test failed: expected success, got failure", &proc_res);
+            if self.props.rmc_panic_step == Some(RMCFailStep::Verify) {
+                if proc_res.status.success() {
+                    self.fatal_proc_rec(
+                        "test failed: expected verification failure, got success",
+                        &proc_res,
+                    );
                 }
             } else {
-                if proc_res.status.success() {
-                    self.fatal_proc_rec("test failed: expected failure, got success", &proc_res);
+                if !proc_res.status.success() {
+                    self.fatal_proc_rec(
+                        "test failed: expected verification success, got failure",
+                        &proc_res,
+                    );
                 }
             }
         }
     }
 
+    /// Checks, codegens, and verifies the test file specified by
+    /// `self.testpaths.file`. An error message is printed to stdout if a result
+    /// is not expected.
+    fn run_rmc_test(&self) {
+        self.check();
+        if self.props.rmc_panic_step == Some(RMCFailStep::Check) {
+            return;
+        }
+        self.codegen();
+        if self.props.rmc_panic_step == Some(RMCFailStep::Codegen) {
+            return;
+        }
+        self.verify();
+    }
+
     /// If the test file contains expected failures in some locations, ensure
     /// that verification does not succeed in those locations.
     fn verify_expect_fail(str: &str) -> Vec<usize> {