diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
index 88f4763be49e..bf3671bb3a16 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
@@ -299,7 +299,7 @@ impl GotocCtx<'_> {
             Intrinsic::Assume => self.codegen_assert_assume(
                 fargs.remove(0).cast_to(Type::bool()),
                 PropertyClass::Assume,
-                "assumption failed",
+                "Rust intrinsic assumption failed",
                 loc,
             ),
             Intrinsic::AtomicAnd(_) => codegen_atomic_binop!(bitand),
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
index 0ffa893056be..788e5f6ec31d 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
@@ -151,12 +151,15 @@ impl GotocCtx<'_> {
                 let farg_types = operands.map(|op| self.operand_ty_stable(&op));
                 self.codegen_copy("copy_nonoverlapping", true, fargs, &farg_types, None, location)
             }
+            // https://doc.rust-lang.org/beta/nightly-rustc/rustc_middle/mir/enum.NonDivergingIntrinsic.html#variant.Assume
+            // Informs the optimizer that a condition is always true.
+            // If the condition is false, the behavior is undefined.
             StatementKind::Intrinsic(NonDivergingIntrinsic::Assume(ref op)) => {
                 let cond = self.codegen_operand_stable(op).cast_to(Type::bool());
                 self.codegen_assert_assume(
                     cond,
                     PropertyClass::Assume,
-                    "assumption failed",
+                    "Rust intrinsic assumption failed",
                     location,
                 )
             }
diff --git a/tests/expected/any_vec/exact_length.expected b/tests/expected/any_vec/exact_length.expected
index f64d2830a7b8..7191e2175f0a 100644
--- a/tests/expected/any_vec/exact_length.expected
+++ b/tests/expected/any_vec/exact_length.expected
@@ -1,11 +1,11 @@
 Checking harness check_access_length_17...
 
-Failed Checks: assumption failed\
+Failed Checks: Rust intrinsic assumption failed\
 in <usize as std::slice::SliceIndex<[u8]>>::get_unchecked
 
 Checking harness check_access_length_zero...
 
-Failed Checks: assumption failed\
+Failed Checks: Rust intrinsic assumption failed\
 in <usize as std::slice::SliceIndex<[u8]>>::get_unchecked
 
 Verification failed for - check_access_length_17
diff --git a/tests/expected/any_vec/out_bounds.expected b/tests/expected/any_vec/out_bounds.expected
index 24121aee4ee8..b457127fec4c 100644
--- a/tests/expected/any_vec/out_bounds.expected
+++ b/tests/expected/any_vec/out_bounds.expected
@@ -1,6 +1,6 @@
 Checking harness check_always_out_bounds...
 
-Failed Checks: assumption failed
+Failed Checks: Rust intrinsic assumption failed
 in <usize as std::slice::SliceIndex<[u8]>>::get_unchecked
 
 Verification failed for - check_always_out_bounds