diff --git a/compiler/rustc_codegen_rmc/src/codegen/statement.rs b/compiler/rustc_codegen_rmc/src/codegen/statement.rs
index 3dd73220d369..e9f8f9b3d855 100644
--- a/compiler/rustc_codegen_rmc/src/codegen/statement.rs
+++ b/compiler/rustc_codegen_rmc/src/codegen/statement.rs
@@ -3,7 +3,7 @@
 use super::typ::TypeExt;
 use super::typ::FN_RETURN_VOID_VAR_NAME;
 use crate::GotocCtx;
-use cbmc::goto_program::{BuiltinFn, Expr, Location, Stmt, Type};
+use cbmc::goto_program::{BuiltinFn, Expr, ExprValue, Location, Stmt, Type};
 use rustc_hir::def_id::DefId;
 use rustc_middle::mir;
 use rustc_middle::mir::{
@@ -472,11 +472,14 @@ impl<'tcx> GotocCtx<'tcx> {
         // CBMC requires that the argument to the assertion must be a string constant.
         // If there is one in the MIR, use it; otherwise, explain that we can't.
         // TODO: give a better message here.
-        let arg = match fargs[0].struct_expr_values() {
-            Some(values) => values[0].clone(),
-            _ => Expr::string_constant(
+
+        // Rewrite panic string depending on "assertion failed" prefix being present or not
+        let arg = if let Some(s) = rewrite_panic_string(fargs) {
+            Expr::string_constant(&s)
+        } else {
+            Expr::string_constant(
                 "This is a placeholder assertion message; the rust message requires dynamic string formatting, which is not supported by CBMC",
-            ),
+            )
         };
 
         let loc = self.codegen_span_option(span);
@@ -647,3 +650,47 @@ impl<'tcx> GotocCtx<'tcx> {
         .with_location(self.codegen_span(&stmt.source_info.span))
     }
 }
+
+/// Assertions, regardless of failing or being proven true are printed as "assertion failed". For example, "assertion failed 1==2: SUCCESS".
+/// This is due to the rustc builtin macros formatting the panic string with "assertion failed" prefix inside expressions. This function rewrites the panic string.
+fn rewrite_panic_string(fargs: Vec<Expr>) -> Option<String> {
+    // Extract the StringConstant from the Expr Struct
+    let extracted_string =
+        if let Some(s) = extract_panic_string(&fargs[0]) { s } else { return None };
+
+    // Rewrite the String only in the case of the prefix being "assertion failed"
+    // If there are changes to be made in the future, different helper functions can be called based on the prefix
+    let rewritten_string = if let Some(stripped) = extracted_string.strip_prefix("assertion failed")
+    {
+        rewrite_assertion_failed(stripped)
+    } else {
+        extracted_string.to_string()
+    };
+
+    Some(rewritten_string)
+}
+
+/// Helper function to extract the panic string from the Expr and return only the StringConstant that is wrapped inside
+fn extract_panic_string(e: &Expr) -> Option<&str> {
+    // The goto needs the translation to be represented as `&"constant"[0]`. The Rust Str type needs to be represented as a struct for CBMC
+    let extracted_string: &str = match e.struct_expr_values().unwrap()[0].value() {
+        ExprValue::AddressOf(expr) => match expr.value() {
+            ExprValue::Index { array, .. } => match array.value() {
+                ExprValue::StringConstant { s } => s,
+                _ => return None,
+            },
+            _ => return None,
+        },
+        ExprValue::StringConstant { s } => s,
+        _ => return None,
+    };
+
+    Some(extracted_string)
+}
+
+/// Micro helper function that specifically handles the case of "assertion failed" StringConstants
+/// If the prefix is changed or the handling needs to be changed, only this function needs to be rewritten
+fn rewrite_assertion_failed(stripped_string: &str) -> String {
+    let rewritten_string = format!("assertion{}", stripped_string);
+    rewritten_string
+}
diff --git a/src/test/cargo-rmc/simple-config-toml/test_one_plus_two.expected b/src/test/cargo-rmc/simple-config-toml/test_one_plus_two.expected
index 4495f0272208..35c113e4b9f1 100644
--- a/src/test/cargo-rmc/simple-config-toml/test_one_plus_two.expected
+++ b/src/test/cargo-rmc/simple-config-toml/test_one_plus_two.expected
@@ -1 +1 @@
-[pair::rmc_tests::test_one_plus_two.assertion.1] line 31 assertion failed: p.sum() == 3: SUCCESS
+[pair::rmc_tests::test_one_plus_two.assertion.1] line 31 assertion: p.sum() == 3: SUCCESS
diff --git a/src/test/cargo-rmc/simple-config-toml/test_sum.expected b/src/test/cargo-rmc/simple-config-toml/test_sum.expected
index 874dde7ec188..5d53ee50c582 100644
--- a/src/test/cargo-rmc/simple-config-toml/test_sum.expected
+++ b/src/test/cargo-rmc/simple-config-toml/test_sum.expected
@@ -1 +1 @@
-[rmc_tests::test_sum.assertion.1] line 27 assertion failed: p.sum() == a.wrapping_add(b): SUCCESS
+[rmc_tests::test_sum.assertion.1] line 27 assertion: p.sum() == a.wrapping_add(b): SUCCESS
diff --git a/src/test/cargo-rmc/simple-lib/test_one_plus_two.expected b/src/test/cargo-rmc/simple-lib/test_one_plus_two.expected
index 4495f0272208..35c113e4b9f1 100644
--- a/src/test/cargo-rmc/simple-lib/test_one_plus_two.expected
+++ b/src/test/cargo-rmc/simple-lib/test_one_plus_two.expected
@@ -1 +1 @@
-[pair::rmc_tests::test_one_plus_two.assertion.1] line 31 assertion failed: p.sum() == 3: SUCCESS
+[pair::rmc_tests::test_one_plus_two.assertion.1] line 31 assertion: p.sum() == 3: SUCCESS
diff --git a/src/test/cargo-rmc/simple-lib/test_sum.expected b/src/test/cargo-rmc/simple-lib/test_sum.expected
index 874dde7ec188..5d53ee50c582 100644
--- a/src/test/cargo-rmc/simple-lib/test_sum.expected
+++ b/src/test/cargo-rmc/simple-lib/test_sum.expected
@@ -1 +1 @@
-[rmc_tests::test_sum.assertion.1] line 27 assertion failed: p.sum() == a.wrapping_add(b): SUCCESS
+[rmc_tests::test_sum.assertion.1] line 27 assertion: p.sum() == a.wrapping_add(b): SUCCESS
diff --git a/src/test/cargo-rmc/simple-main/main.expected b/src/test/cargo-rmc/simple-main/main.expected
index 4253bc716933..8a9917939457 100644
--- a/src/test/cargo-rmc/simple-main/main.expected
+++ b/src/test/cargo-rmc/simple-main/main.expected
@@ -1,2 +1,2 @@
-[main.assertion.1] line 4 assertion failed: 1 == 2: FAILURE
+[main.assertion.1] line 4 assertion: 1 == 2: FAILURE
 VERIFICATION FAILED
diff --git a/src/test/expected/allocation/expected b/src/test/expected/allocation/expected
index 37c016ff5300..51e3ca6785c9 100644
--- a/src/test/expected/allocation/expected
+++ b/src/test/expected/allocation/expected
@@ -1,2 +1,2 @@
-line 8 assertion failed: foo() == None: SUCCESS
-line 11 assertion failed: foo() == y: SUCCESS
+line 8 assertion: foo() == None: SUCCESS
+line 11 assertion: foo() == y: SUCCESS
diff --git a/src/test/expected/array/expected b/src/test/expected/array/expected
index 70152d4c1d60..185544e86aa3 100644
--- a/src/test/expected/array/expected
+++ b/src/test/expected/array/expected
@@ -3,7 +3,7 @@ array 'y'.0 upper bound in y.0[var_12]: SUCCESS
 array 'y'.0 upper bound in y.0[var_16]: FAILURE
 array 'x'.0 upper bound in x.0[var_3]: SUCCESS
 array 'x'.0 upper bound in x.0[var_5]: SUCCESS
-line 12 assertion failed: y[0] == 1: SUCCESS
-line 13 assertion failed: y[1] == 2: SUCCESS
+line 12 assertion: y[0] == 1: SUCCESS
+line 13 assertion: y[1] == 2: SUCCESS
 line 14 index out of bounds: the length is move _17 but the index is _16: FAILURE
-line 14 assertion failed: y[z] == 3: FAILURE
+line 14 assertion: y[z] == 3: FAILURE
diff --git a/src/test/expected/assertion-without-failed/expected b/src/test/expected/assertion-without-failed/expected
new file mode 100644
index 000000000000..8010163c96b2
--- /dev/null
+++ b/src/test/expected/assertion-without-failed/expected
@@ -0,0 +1 @@
+line 4 assertion: 1 == 2: FAILURE
\ No newline at end of file
diff --git a/src/test/expected/assertion-without-failed/main.rs b/src/test/expected/assertion-without-failed/main.rs
new file mode 100644
index 000000000000..3f1fa2b4f1d1
--- /dev/null
+++ b/src/test/expected/assertion-without-failed/main.rs
@@ -0,0 +1,5 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+pub fn main() {
+    assert!(1 == 2);
+}
diff --git a/src/test/expected/binop/expected b/src/test/expected/binop/expected
index 7dd221b5e40e..e58bdcbd16ea 100644
--- a/src/test/expected/binop/expected
+++ b/src/test/expected/binop/expected
@@ -1,42 +1,42 @@
 line 4 attempt to compute `move _8 + move _9`, which would overflow: SUCCESS
-line 4 assertion failed: a + b == correct: SUCCESS
+line 4 assertion: a + b == correct: SUCCESS
 line 5 attempt to compute `move _15 + move _16`, which would overflow: SUCCESS
-line 5 assertion failed: a + b == wrong: FAILURE
+line 5 assertion: a + b == wrong: FAILURE
 line 9 attempt to compute `move _8 - move _9`, which would overflow: SUCCESS
-line 9 assertion failed: a - b == correct: SUCCESS
+line 9 assertion: a - b == correct: SUCCESS
 line 10 attempt to compute `move _15 - move _16`, which would overflow: SUCCESS
-line 10 assertion failed: a - b == wrong: FAILURE
+line 10 assertion: a - b == wrong: FAILURE
 line 14 attempt to compute `move _8 * move _9`, which would overflow: SUCCESS
-line 14 assertion failed: a * b == correct: SUCCESS
+line 14 assertion: a * b == correct: SUCCESS
 line 15 attempt to compute `move _15 * move _16`, which would overflow: SUCCESS
-line 15 assertion failed: a * b == wrong: FAILURE
+line 15 assertion: a * b == wrong: FAILURE
 line 19 attempt to divide `_8` by zero: SUCCESS
 line 19 attempt to compute `_8 / _9`, which would overflow: SUCCESS
-line 19 assertion failed: a / b == correct: SUCCESS
+line 19 assertion: a / b == correct: SUCCESS
 line 20 attempt to divide `_18` by zero: SUCCESS
 line 20 attempt to compute `_18 / _19`, which would overflow: SUCCESS
-line 20 assertion failed: a / b == wrong: FAILURE
+line 20 assertion: a / b == wrong: FAILURE
 line 24 attempt to calculate the remainder of `_8` with a divisor of zero: SUCCESS
 line 24 attempt to compute the remainder of `_8 % _9`, which would overflow: SUCCESS
-line 24 assertion failed: a % b == correct: SUCCESS
+line 24 assertion: a % b == correct: SUCCESS
 line 25 attempt to calculate the remainder of `_18` with a divisor of zero: SUCCESS
 line 25 attempt to compute the remainder of `_18 % _19`, which would overflow: SUCCESS
-line 25 assertion failed: a % b == wrong: FAILURE
+line 25 assertion: a % b == wrong: FAILURE
 line 29 attempt to shift left by `move _9`, which would overflow: SUCCESS
-line 29 assertion failed: a << b == correct: SUCCESS
+line 29 assertion: a << b == correct: SUCCESS
 line 30 attempt to shift left by `move _16`, which would overflow: SUCCESS
-line 30 assertion failed: a << b == wrong: FAILURE
+line 30 assertion: a << b == wrong: FAILURE
 line 34 attempt to shift right by `move _9`, which would overflow: SUCCESS
-line 34 assertion failed: a >> b == correct: SUCCESS
+line 34 assertion: a >> b == correct: SUCCESS
 line 35 attempt to shift right by `move _16`, which would overflow: SUCCESS
-line 35 assertion failed: a >> b == wrong: FAILURE
+line 35 assertion: a >> b == wrong: FAILURE
 line 39 attempt to shift right by `move _9`, which would overflow: SUCCESS
-line 39 assertion failed: a >> b == correct: SUCCESS
+line 39 assertion: a >> b == correct: SUCCESS
 line 40 attempt to shift right by `move _16`, which would overflow: SUCCESS
-line 40 assertion failed: a >> b == wrong: FAILURE
-line 44 assertion failed: a & b == correct: SUCCESS
-line 45 assertion failed: a & b == wrong: FAILURE
-line 49 assertion failed: a | b == correct: SUCCESS
-line 50 assertion failed: a | b == wrong: FAILURE
-line 54 assertion failed: a ^ b == correct: SUCCESS
-line 55 assertion failed: a ^ b == wrong: FAILURE
+line 40 assertion: a >> b == wrong: FAILURE
+line 44 assertion: a & b == correct: SUCCESS
+line 45 assertion: a & b == wrong: FAILURE
+line 49 assertion: a | b == correct: SUCCESS
+line 50 assertion: a | b == wrong: FAILURE
+line 54 assertion: a ^ b == correct: SUCCESS
+line 55 assertion: a ^ b == wrong: FAILURE
diff --git a/src/test/expected/closure/expected b/src/test/expected/closure/expected
index 5a70cc7ef769..291f478f0bae 100644
--- a/src/test/expected/closure/expected
+++ b/src/test/expected/closure/expected
@@ -3,5 +3,5 @@ line 20 attempt to compute `move _8 + move _9`, which would overflow: SUCCESS
 line 20 attempt to compute `move _5 + move _6`, which would overflow: SUCCESS
 line 20 attempt to compute `(*((*_1).0: &mut i32)) + move _4`, which would overflow: SUCCESS
 line 25 attempt to compute `move _18 + const 12_i32`, which would overflow: SUCCESS
-line 25 assertion failed: original_num + 12 == num: SUCCESS
+line 25 assertion: original_num + 12 == num: SUCCESS
 line 25 arithmetic overflow on signed + in var_18 + 12: SUCCESS
diff --git a/src/test/expected/closure2/expected b/src/test/expected/closure2/expected
index 81c45ac28f7f..6c9b3a8440b5 100644
--- a/src/test/expected/closure2/expected
+++ b/src/test/expected/closure2/expected
@@ -1,4 +1,4 @@
 line 5 attempt to compute `move _3 + move _4`, which would overflow: SUCCESS
 line 7 attempt to compute `move _3 + move _4`, which would overflow: SUCCESS
-line 8 assertion failed: z == 102: SUCCESS
-line 9 assertion failed: g(z) == 206: SUCCESS
+line 8 assertion: z == 102: SUCCESS
+line 9 assertion: g(z) == 206: SUCCESS
diff --git a/src/test/expected/closure3/expected b/src/test/expected/closure3/expected
index ccc0abde64a1..99dc9e71824f 100644
--- a/src/test/expected/closure3/expected
+++ b/src/test/expected/closure3/expected
@@ -1,3 +1,3 @@
 line 16 attempt to compute `move _3 + move _4`, which would overflow: SUCCESS
 line 17 attempt to compute `move _11 + const 10_i64`, which would overflow: SUCCESS
-line 17 assertion failed: num + 10 == y: SUCCESS
+line 17 assertion: num + 10 == y: SUCCESS
diff --git a/src/test/expected/comp/expected b/src/test/expected/comp/expected
index c54dfd655287..05ca26e66da9 100644
--- a/src/test/expected/comp/expected
+++ b/src/test/expected/comp/expected
@@ -1,11 +1,11 @@
 line 5 attempt to compute `move _6 + move _7`, which would overflow: SUCCESS
 line 5 attempt to compute `move _10 + move _11`, which would overflow: SUCCESS
-line 5 assertion failed: a + b == b + a: SUCCESS
+line 5 assertion: a + b == b + a: SUCCESS
 line 6 attempt to compute `move _16 + move _17`, which would overflow: SUCCESS
 line 6 attempt to compute `move _21 + move _22`, which would overflow: SUCCESS
 line 6 attempt to compute `move _20 + const 1_i32`, which would overflow: SUCCESS
-line 6 assertion failed: a + b != a + b + 1: SUCCESS
+line 6 assertion: a + b != a + b + 1: SUCCESS
 line 11 attempt to compute `move _6 + move _7`, which would overflow: SUCCESS
-line 11 assertion failed: a + b > a: SUCCESS
+line 11 assertion: a + b > a: SUCCESS
 line 12 attempt to compute `move _13 - move _14`, which would overflow: SUCCESS
-line 12 assertion failed: a - b < a: SUCCESS
+line 12 assertion: a - b < a: SUCCESS
diff --git a/src/test/expected/copy/expected b/src/test/expected/copy/expected
index 4d218431fb4a..271c96661c4e 100644
--- a/src/test/expected/copy/expected
+++ b/src/test/expected/copy/expected
@@ -1,3 +1,3 @@
 memmove source region readable: SUCCESS
 memmove destination region writeable: SUCCESS
-assertion failed: *dst == expected_val: SUCCESS
+assertion: *dst == expected_val: SUCCESS
diff --git a/src/test/expected/dynamic-error-trait/expected b/src/test/expected/dynamic-error-trait/expected
index eb72d9c5cf94..b939ae9cf61b 100644
--- a/src/test/expected/dynamic-error-trait/expected
+++ b/src/test/expected/dynamic-error-trait/expected
@@ -1,2 +1,2 @@
-assertion failed: mm.size == 2: SUCCESS
-assertion failed: mm.size == 3: FAILURE
+assertion: mm.size == 2: SUCCESS
+assertion: mm.size == 3: FAILURE
diff --git a/src/test/expected/dynamic-trait-static-dispatch/expected b/src/test/expected/dynamic-trait-static-dispatch/expected
index 936d70bfc4f3..401bdc31c7d8 100644
--- a/src/test/expected/dynamic-trait-static-dispatch/expected
+++ b/src/test/expected/dynamic-trait-static-dispatch/expected
@@ -1,2 +1,2 @@
-line 25 assertion failed: bar.a() == 3: SUCCESS
-line 26 assertion failed: bar.b() == 5: SUCCESS
+line 25 assertion: bar.a() == 3: SUCCESS
+line 26 assertion: bar.b() == 5: SUCCESS
diff --git a/src/test/expected/dynamic-trait/expected b/src/test/expected/dynamic-trait/expected
index 91d2bca953cf..069316ea0670 100644
--- a/src/test/expected/dynamic-trait/expected
+++ b/src/test/expected/dynamic-trait/expected
@@ -4,13 +4,13 @@ line 26 attempt to compute `move _3 * move _7`, which would overflow: SUCCESS
 line 32 attempt to compute `move _2 * move _3`, which would overflow: SUCCESS
 line 35 attempt to compute `move _4 * move _5`, which would overflow: SUCCESS
 line 35 attempt to compute `move _3 * move _7`, which would overflow: SUCCESS
-line 52 assertion failed: rec.vol(3) == 150: SUCCESS
-line 53 assertion failed: impl_area(rec.clone()) == 50: SUCCESS
-line 56 assertion failed: vol == 100: SUCCESS
-line 59 assertion failed: square.vol(3) == 27: SUCCESS
-line 60 assertion failed: do_vol(&square, 2) == 18: SUCCESS
-line 61 assertion failed: impl_area(square.clone()) == 9: SUCCESS
-line 63 assertion failed: !square.compare_area(&square): SUCCESS
-line 64 assertion failed: !square.compare_area(&rec): SUCCESS
-line 65 assertion failed: rec.compare_area(&square): SUCCESS
-line 66 assertion failed: !rec.compare_area(&rec): SUCCESS
+line 52 assertion: rec.vol(3) == 150: SUCCESS
+line 53 assertion: impl_area(rec.clone()) == 50: SUCCESS
+line 56 assertion: vol == 100: SUCCESS
+line 59 assertion: square.vol(3) == 27: SUCCESS
+line 60 assertion: do_vol(&square, 2) == 18: SUCCESS
+line 61 assertion: impl_area(square.clone()) == 9: SUCCESS
+line 63 assertion: !square.compare_area(&square): SUCCESS
+line 64 assertion: !square.compare_area(&rec): SUCCESS
+line 65 assertion: rec.compare_area(&square): SUCCESS
+line 66 assertion: !rec.compare_area(&rec): SUCCESS
diff --git a/src/test/expected/enum/expected b/src/test/expected/enum/expected
index 22b2f6a67841..926b7a7c2ebc 100644
--- a/src/test/expected/enum/expected
+++ b/src/test/expected/enum/expected
@@ -1,7 +1,7 @@
 line 18 unreachable code: SUCCESS
-line 18 assertion failed: false: SUCCESS
-line 19 assertion failed: x == 10: SUCCESS
+line 18 assertion: false: SUCCESS
+line 19 assertion: x == 10: SUCCESS
 line 22 unreachable code: SUCCESS
-line 22 assertion failed: false: SUCCESS
-line 25 assertion failed: x == 30 && y == 60.0: SUCCESS
-line 26 assertion failed: x == 31: FAILURE
+line 22 assertion: false: SUCCESS
+line 25 assertion: x == 30 && y == 60.0: SUCCESS
+line 26 assertion: x == 31: FAILURE
diff --git a/src/test/expected/float-nan/expected b/src/test/expected/float-nan/expected
index f1db04b782d1..b8f88af3d980 100644
--- a/src/test/expected/float-nan/expected
+++ b/src/test/expected/float-nan/expected
@@ -1,5 +1,5 @@
-line 11 assertion failed: 1.0 / f != 0.0 / f: SUCCESS
-line 13 assertion failed: !(1.0 / f == 0.0 / f): SUCCESS
-line 15 assertion failed: 1.0 / f == 0.0 / f: FAILURE
-line 17 assertion failed: 0.0 / f == 0.0 / f: FAILURE
-line 19 assertion failed: 0.0 / f != 0.0 / f: SUCCESS
+line 11 assertion: 1.0 / f != 0.0 / f: SUCCESS
+line 13 assertion: !(1.0 / f == 0.0 / f): SUCCESS
+line 15 assertion: 1.0 / f == 0.0 / f: FAILURE
+line 17 assertion: 0.0 / f == 0.0 / f: FAILURE
+line 19 assertion: 0.0 / f != 0.0 / f: SUCCESS
diff --git a/src/test/expected/generics/expected b/src/test/expected/generics/expected
index b778feee4fe4..3a417edfb517 100644
--- a/src/test/expected/generics/expected
+++ b/src/test/expected/generics/expected
@@ -1,2 +1,2 @@
-line 21 assertion failed: x == y.data: SUCCESS
-line 22 assertion failed: z == w.data: SUCCESS
+line 21 assertion: x == y.data: SUCCESS
+line 22 assertion: z == w.data: SUCCESS
diff --git a/src/test/expected/iterator/expected b/src/test/expected/iterator/expected
index 03d7525a7728..a66f4f19099c 100644
--- a/src/test/expected/iterator/expected
+++ b/src/test/expected/iterator/expected
@@ -1,3 +1,3 @@
 line 5 unreachable code: SUCCESS
 line 6 attempt to compute `_1 * move _13`, which would overflow: SUCCESS
-line 8 assertion failed: z == 6: SUCCESS
+line 8 assertion: z == 6: SUCCESS
diff --git a/src/test/expected/niche/expected b/src/test/expected/niche/expected
index ce8e04bf66c4..38bf5632d469 100644
--- a/src/test/expected/niche/expected
+++ b/src/test/expected/niche/expected
@@ -1,5 +1,5 @@
-line 20 assertion failed: false: SUCCESS
+line 20 assertion: false: SUCCESS
 line 20 unreachable code: SUCCESS
 line 25 unreachable code: SUCCESS
-line 25 assertion failed: false: SUCCESS
-line 27 assertion failed: a == *b: SUCCESS
+line 25 assertion: false: SUCCESS
+line 27 assertion: a == *b: SUCCESS
diff --git a/src/test/expected/niche2/expected b/src/test/expected/niche2/expected
index 1d3eafe2aaf5..6e6af4193ec9 100644
--- a/src/test/expected/niche2/expected
+++ b/src/test/expected/niche2/expected
@@ -1,5 +1,5 @@
-line 21 assertion failed: false: SUCCESS
+line 21 assertion: false: SUCCESS
 line 21 unreachable code: SUCCESS
-line 27 assertion failed: x == 10: SUCCESS
-line 28 assertion failed: false: SUCCESS
-line 33 assertion failed: false: SUCCESS
+line 27 assertion: x == 10: SUCCESS
+line 28 assertion: false: SUCCESS
+line 33 assertion: false: SUCCESS
diff --git a/src/test/expected/nondet/expected b/src/test/expected/nondet/expected
index 1c5430c0e112..ac207b6ab028 100644
--- a/src/test/expected/nondet/expected
+++ b/src/test/expected/nondet/expected
@@ -2,4 +2,4 @@ line 9 attempt to compute `move _12 * move _13`, which would overflow: SUCCESS
 line 9 attempt to compute `const 2_i32 * move _16`, which would overflow: SUCCESS
 line 9 attempt to compute `move _11 - move _15`, which would overflow: SUCCESS
 line 9 attempt to compute `move _10 + const 1_i32`, which would overflow: SUCCESS
-line 9 assertion failed: x * x - 2 * x + 1 != 4 || (x == -1 || x == 3): SUCCESS
+line 9 assertion: x * x - 2 * x + 1 != 4 || (x == -1 || x == 3): SUCCESS
diff --git a/src/test/expected/references/expected b/src/test/expected/references/expected
index 4781758d73f1..2bd75c252156 100644
--- a/src/test/expected/references/expected
+++ b/src/test/expected/references/expected
@@ -1 +1 @@
-line 17 assertion failed: z == 2: SUCCESS
+line 17 assertion: z == 2: SUCCESS
diff --git a/src/test/expected/replace-hashmap/expected b/src/test/expected/replace-hashmap/expected
index 835bdfb4723a..054fb50e29cd 100644
--- a/src/test/expected/replace-hashmap/expected
+++ b/src/test/expected/replace-hashmap/expected
@@ -1,6 +1,6 @@
 line 31 attempt to compute `((*_1).0: usize) + const 1_usize`, which would overflow: SUCCESS
 line 31 arithmetic overflow on unsigned + in self->len + 1: SUCCESS
-line 56 assertion failed: a.is_some(): FAILURE
-line 57 assertion failed: a.is_none(): FAILURE
-line 59 assertion failed: b.is_some(): SUCCESS
-line 60 assertion failed: b.is_none(): FAILURE
+line 56 assertion: a.is_some(): FAILURE
+line 57 assertion: a.is_none(): FAILURE
+line 59 assertion: b.is_some(): SUCCESS
+line 60 assertion: b.is_none(): FAILURE
diff --git a/src/test/expected/replace-vec/expected b/src/test/expected/replace-vec/expected
index 7a98f73b07a9..7b29f6509686 100644
--- a/src/test/expected/replace-vec/expected
+++ b/src/test/expected/replace-vec/expected
@@ -1,8 +1,8 @@
 line 25 attempt to compute `((*_1).0: usize) + const 1_usize`, which would overflow: SUCCESS
 line 35 attempt to compute `((*_1).0: usize) - const 1_usize`, which would overflow: SUCCESS
-line 53 assertion failed: v.len() == 1: SUCCESS
-line 54 assertion failed: v.len() == 11: FAILURE
-line 56 assertion failed: p != None: SUCCESS
-line 57 assertion failed: p == None: FAILURE
-line 58 assertion failed: p == Some(to_push): SUCCESS
-line 59 assertion failed: p == Some(not_pushed): FAILURE
+line 53 assertion: v.len() == 1: SUCCESS
+line 54 assertion: v.len() == 11: FAILURE
+line 56 assertion: p != None: SUCCESS
+line 57 assertion: p == None: FAILURE
+line 58 assertion: p == Some(to_push): SUCCESS
+line 59 assertion: p == Some(not_pushed): FAILURE
diff --git a/src/test/expected/slice/expected b/src/test/expected/slice/expected
index dd4501277b2b..0b5eee120fba 100644
--- a/src/test/expected/slice/expected
+++ b/src/test/expected/slice/expected
@@ -1,4 +1,4 @@
-line 15 assertion failed: y.len() == 5: SUCCESS
+line 15 assertion: y.len() == 5: SUCCESS
 line 16 index out of bounds: the length is move _16 but the index is _15: SUCCESS
-line 16 assertion failed: y[1] == 2: SUCCESS
-line 17 assertion failed: z.len() == 3: SUCCESS
+line 16 assertion: y[1] == 2: SUCCESS
+line 17 assertion: z.len() == 3: SUCCESS
diff --git a/src/test/expected/static-mutable-struct/expected b/src/test/expected/static-mutable-struct/expected
index 2ce4276890b6..443bdce0f74d 100644
--- a/src/test/expected/static-mutable-struct/expected
+++ b/src/test/expected/static-mutable-struct/expected
@@ -1,12 +1,12 @@
-line 23 assertion failed: foo().x == 12: SUCCESS
-line 24 assertion failed: foo().y == 12: FAILURE
-line 25 assertion failed: foo().x == 14: FAILURE
-line 26 assertion failed: foo().y == 14: SUCCESS
-line 29 assertion failed: foo().x == 1: SUCCESS
-line 30 assertion failed: foo().y == 1: FAILURE
-line 31 assertion failed: foo().x == 2: FAILURE
-line 32 assertion failed: foo().y == 2: SUCCESS
-line 35 assertion failed: foo().x == 1 << 62: SUCCESS
-line 36 assertion failed: foo().x == 1 << 31: FAILURE
-line 37 assertion failed: foo().y == 1 << 31: SUCCESS
+line 23 assertion: foo().x == 12: SUCCESS
+line 24 assertion: foo().y == 12: FAILURE
+line 25 assertion: foo().x == 14: FAILURE
+line 26 assertion: foo().y == 14: SUCCESS
+line 29 assertion: foo().x == 1: SUCCESS
+line 30 assertion: foo().y == 1: FAILURE
+line 31 assertion: foo().x == 2: FAILURE
+line 32 assertion: foo().y == 2: SUCCESS
+line 35 assertion: foo().x == 1 << 62: SUCCESS
+line 36 assertion: foo().x == 1 << 31: FAILURE
+line 37 assertion: foo().y == 1 << 31: SUCCESS
 
diff --git a/src/test/expected/static-mutable/expected b/src/test/expected/static-mutable/expected
index 1e47840833bb..97e1428acc7b 100644
--- a/src/test/expected/static-mutable/expected
+++ b/src/test/expected/static-mutable/expected
@@ -1,4 +1,4 @@
-line 16 assertion failed: 10 == foo(): FAILURE
-line 17 assertion failed: 12 == foo(): SUCCESS
-line 19 assertion failed: 10 == foo(): SUCCESS
-line 20 assertion failed: 12 == foo(): FAILURE
+line 16 assertion: 10 == foo(): FAILURE
+line 17 assertion: 12 == foo(): SUCCESS
+line 19 assertion: 10 == foo(): SUCCESS
+line 20 assertion: 12 == foo(): FAILURE
diff --git a/src/test/expected/static/expected b/src/test/expected/static/expected
index 93b76a5cc863..c31a9ac0c1a6 100644
--- a/src/test/expected/static/expected
+++ b/src/test/expected/static/expected
@@ -1,2 +1,2 @@
-line 10 assertion failed: 10 == foo(): FAILURE
-line 11 assertion failed: 12 == foo(): SUCCESS
+line 10 assertion: 10 == foo(): FAILURE
+line 11 assertion: 12 == foo(): SUCCESS
diff --git a/src/test/expected/test1/expected b/src/test/expected/test1/expected
index 726f39612293..b1c5e7ea6530 100644
--- a/src/test/expected/test1/expected
+++ b/src/test/expected/test1/expected
@@ -1,5 +1,5 @@
 line 7 attempt to compute `_1 + move _4`, which would overflow: SUCCESS
 line 8 attempt to compute `_2 - const 1_i32`, which would overflow: SUCCESS
-line 12 assertion failed: a == 54: FAILURE
-line 14 assertion failed: a == 55: SUCCESS
-line 16 assertion failed: a >= 55: SUCCESS
+line 12 assertion: a == 54: FAILURE
+line 14 assertion: a == 55: SUCCESS
+line 16 assertion: a >= 55: SUCCESS
diff --git a/src/test/expected/test2/expected b/src/test/expected/test2/expected
index 6560754671f4..8c2f32124be5 100644
--- a/src/test/expected/test2/expected
+++ b/src/test/expected/test2/expected
@@ -1,5 +1,5 @@
 line 7 attempt to shift right by `const 1_i32`, which would overflow: SUCCESS
 line 8 attempt to compute `_2 + const 1_i32`, which would overflow: SUCCESS
-line 13 assertion failed: i == 3: FAILURE
-line 15 assertion failed: i == 2: SUCCESS
-line 17 assertion failed: i == 2 || i == 3: SUCCESS
+line 13 assertion: i == 3: FAILURE
+line 15 assertion: i == 2: SUCCESS
+line 17 assertion: i == 2 || i == 3: SUCCESS
diff --git a/src/test/expected/test3/expected b/src/test/expected/test3/expected
index 1c9045ad231b..ca72b0649b42 100644
--- a/src/test/expected/test3/expected
+++ b/src/test/expected/test3/expected
@@ -1,9 +1,9 @@
 line 9 attempt to compute `_2 - const 1_i32`, which would overflow: SUCCESS
-line 14 assertion failed: a == 10.0 && i == 1: FAILURE
-line 16 assertion failed: a == 9.0 && i == 0: FAILURE
-line 18 assertion failed: a == 9.0 && i == 1: FAILURE
-line 20 assertion failed: a == 10.0 && i == 0: SUCCESS
-line 23 assertion failed: a == 9.0 || i == 0: SUCCESS
-line 25 assertion failed: a == 10.0 || i == 1: SUCCESS
-line 27 assertion failed: a == 9.0 || i == 1: FAILURE
-line 29 assertion failed: a == 10.0 || i == 0: SUCCESS
+line 14 assertion: a == 10.0 && i == 1: FAILURE
+line 16 assertion: a == 9.0 && i == 0: FAILURE
+line 18 assertion: a == 9.0 && i == 1: FAILURE
+line 20 assertion: a == 10.0 && i == 0: SUCCESS
+line 23 assertion: a == 9.0 || i == 0: SUCCESS
+line 25 assertion: a == 10.0 || i == 1: SUCCESS
+line 27 assertion: a == 9.0 || i == 1: FAILURE
+line 29 assertion: a == 10.0 || i == 0: SUCCESS
diff --git a/src/test/expected/test4/expected b/src/test/expected/test4/expected
index 4415a6f38323..b3361bbd556f 100644
--- a/src/test/expected/test4/expected
+++ b/src/test/expected/test4/expected
@@ -1,6 +1,6 @@
 line 8 attempt to compute `_2 + const 1_i32`, which would overflow: SUCCESS
-line 13 assertion failed: i == 3: FAILURE
-line 15 assertion failed: i == 2: SUCCESS
-line 17 assertion failed: i == 2 || i == 3: SUCCESS
+line 13 assertion: i == 3: FAILURE
+line 15 assertion: i == 2: SUCCESS
+line 17 assertion: i == 2 || i == 3: SUCCESS
 line 21 attempt to divide `_3` by zero: SUCCESS
 line 21 attempt to compute `_3 / _4`, which would overflow: SUCCESS
diff --git a/src/test/expected/test5/expected b/src/test/expected/test5/expected
index 221409f3c327..8888ada624f9 100644
--- a/src/test/expected/test5/expected
+++ b/src/test/expected/test5/expected
@@ -1,4 +1,4 @@
-line 5 assertion failed: div(4, 2) == 2: SUCCESS
-line 7 assertion failed: div(6, 2) == 2: FAILURE
+line 5 assertion: div(4, 2) == 2: SUCCESS
+line 7 assertion: div(6, 2) == 2: FAILURE
 line 11 attempt to divide `_3` by zero: SUCCESS
 line 11 attempt to compute `_3 / _4`, which would overflow: SUCCESS
diff --git a/src/test/expected/test6/expected b/src/test/expected/test6/expected
index 416610f2ed91..0e327f6f9394 100644
--- a/src/test/expected/test6/expected
+++ b/src/test/expected/test6/expected
@@ -1,2 +1,2 @@
-line 9 assertion failed: add2(1, 1) == 2.0: SUCCESS
-line 11 assertion failed: add2(2, 1) == 2.0: FAILURE
+line 9 assertion: add2(1, 1) == 2.0: SUCCESS
+line 11 assertion: add2(2, 1) == 2.0: FAILURE
diff --git a/src/test/expected/transmute/expected b/src/test/expected/transmute/expected
index 43617fc39881..082026f6bdc5 100644
--- a/src/test/expected/transmute/expected
+++ b/src/test/expected/transmute/expected
@@ -1,2 +1,2 @@
-line 5 assertion failed: bitpattern == 0x3F800000: SUCCESS
-line 11 assertion failed: f == 1.0: SUCCESS
+line 5 assertion: bitpattern == 0x3F800000: SUCCESS
+line 11 assertion: f == 1.0: SUCCESS
diff --git a/src/test/expected/vec/expected b/src/test/expected/vec/expected
index 9ba2d3790e35..839987da1944 100644
--- a/src/test/expected/vec/expected
+++ b/src/test/expected/vec/expected
@@ -12,6 +12,6 @@
 [realloc.precondition_instance.10] line 30 double free: SUCCESS
 [realloc.precondition_instance.11] line 30 free called for new[] object: SUCCESS
 [realloc.precondition_instance.12] line 30 free called for stack-allocated object: SUCCESS
-line 6 assertion failed: x[0] == 10: SUCCESS
-line 8 assertion failed: y == 10: SUCCESS
-line 9 assertion failed: y != 10: FAILURE
+line 6 assertion: x[0] == 10: SUCCESS
+line 8 assertion: y == 10: SUCCESS
+line 9 assertion: y != 10: FAILURE
diff --git a/src/test/expected/vecdq/expected b/src/test/expected/vecdq/expected
index 36e8d9827acc..cc95712bf141 100644
--- a/src/test/expected/vecdq/expected
+++ b/src/test/expected/vecdq/expected
@@ -1,6 +1,6 @@
-assertion failed: q.len() == 2: SUCCESS
-assertion failed: q.pop_front().unwrap() == x: SUCCESS
-assertion failed: q.pop_front().unwrap() == y: SUCCESS
+assertion: q.len() == 2: SUCCESS
+assertion: q.pop_front().unwrap() == x: SUCCESS
+assertion: q.pop_front().unwrap() == y: SUCCESS
 max allocation size exceeded: SUCCESS
 max allocation may fail: SUCCESS
 max allocation size exceeded: SUCCESS