diff --git a/src/test/cbmc/DynTrait/vtable_size_align_drop_fail.rs b/src/test/cbmc/DynTrait/vtable_size_align_drop_fail.rs
index 7af61f34b3a0..ed87c0fa3ba8 100644
--- a/src/test/cbmc/DynTrait/vtable_size_align_drop_fail.rs
+++ b/src/test/cbmc/DynTrait/vtable_size_align_drop_fail.rs
@@ -13,6 +13,7 @@
 #![allow(deprecated)]
 
 use std::intrinsics::size_of;
+use std::ptr::drop_in_place;
 
 include!("../Helpers/vtable_utils_ignore.rs");
 include!("../../rmc-prelude.rs");
@@ -68,7 +69,7 @@ fn main() {
 
     // Check layout/values for Sheep
     unsafe {
-        let animal_sheep = random_animal(1);
+        let animal_sheep = &*random_animal(1);
 
         // Check that the struct's data is what we expect
         let data_ptr = data!(animal_sheep);
@@ -90,15 +91,15 @@ fn main() {
     }
     // Check layout/values for Cow
     unsafe {
-        let animal_sheep = random_animal(1);
+        let animal_cow = &*random_animal(6);
 
         // Check that the struct's data is what we expect
-        let data_ptr = data!(animal_sheep);
+        let data_ptr = data!(animal_cow);
 
         // Note: i8 ptr cast
         __VERIFIER_expect_fail(*(data_ptr as *mut i8) != 9, "Wrong data"); // From Cow
 
-        let vtable_ptr = vtable!(animal_sheep);
+        let vtable_ptr = vtable!(animal_cow);
 
         // Drop pointer
         __VERIFIER_expect_fail(
diff --git a/src/tools/compiletest/src/runtest.rs b/src/tools/compiletest/src/runtest.rs
index 3163dd8d8cb2..8f86c79500b6 100644
--- a/src/tools/compiletest/src/runtest.rs
+++ b/src/tools/compiletest/src/runtest.rs
@@ -2406,18 +2406,56 @@ impl<'test> TestCx<'test> {
             .args(&self.props.cbmc_flags);
         self.add_rmc_dir_to_path(&mut rmc);
         let proc_res = self.compose_and_run_compiler(rmc, None);
-        // 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 the test file contains expected failures in some locations, ensure
+        // that verification does indeed fail in those locations
+        if proc_res.stdout.contains("EXPECTED FAIL") {
+            let lines = TestCx::verify_expect_fail(&proc_res.stdout);
+            if !lines.is_empty() {
+                self.fatal_proc_rec(
+                    &format!("test failed: expected failure in lines {:?}, got success", lines),
+                    &proc_res,
+                )
             }
         } else {
-            if proc_res.status.success() {
-                self.fatal_proc_rec("test failed: expected failure, got success", &proc_res);
+            // The code above depends too much on the exact string output of
+            // RMC. If the output of RMC changes in the future, the check below
+            // will (hopefully) force some tests to fail and remind us to
+            // update the code above as well.
+            if fs::read_to_string(&self.testpaths.file).unwrap().contains("__VERIFIER_expect_fail")
+            {
+                self.fatal_proc_rec(
+                    "found call to `__VERIFIER_expect_fail` with no corresponding \
+                 \"EXPECTED FAIL\" in RMC's output",
+                    &proc_res,
+                )
+            }
+            // 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);
+                }
+            } else {
+                if proc_res.status.success() {
+                    self.fatal_proc_rec("test failed: expected failure, got success", &proc_res);
+                }
             }
         }
     }
 
+    /// 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> {
+        let re = Regex::new(r"line [0-9]+ EXPECTED FAIL: SUCCESS").unwrap();
+        let mut lines = vec![];
+        for m in re.find_iter(str) {
+            let splits = m.as_str().split_ascii_whitespace();
+            let num_str = splits.skip(1).next().unwrap();
+            let num = num_str.parse().unwrap();
+            lines.push(num);
+        }
+        lines
+    }
+
     /// Runs cargo-rmc on the function specified by the stem of `self.testpaths.file`.
     /// An error message is printed to stdout if verification output does not
     /// contain the expected output in `self.testpaths.file`.