diff --git a/prusti-viper/src/encoder/procedure_encoder.rs b/prusti-viper/src/encoder/procedure_encoder.rs
index bceb6bc06b1..2dfade294fb 100644
--- a/prusti-viper/src/encoder/procedure_encoder.rs
+++ b/prusti-viper/src/encoder/procedure_encoder.rs
@@ -2158,14 +2158,8 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                 };
 
                 // Check or assume the assertion
-                let assert_msg = if let AssertKind::BoundsCheck{ .. } = msg {
-                    // Use the debug impl for BoundsCheck, as it is supposed to be handled before
-                    // calling display() according to the docs
-                    // TODO: use fmt_assert_args once https://github.com/rust-lang/rust/pull/84392 is merged
-                    format!("{:?}", msg)
-                } else {
-                    msg.description().to_string()
-                };
+                let mut assert_msg = String::new();
+                msg.fmt_assert_args(&mut assert_msg).unwrap();
 
                 stmts.push(vir::Stmt::comment(format!("Rust assertion: {}", assert_msg)));
                 if self.check_panics {
diff --git a/prusti-viper/src/encoder/pure_function_encoder.rs b/prusti-viper/src/encoder/pure_function_encoder.rs
index 12ddcf21b9d..ddde6fe8f06 100644
--- a/prusti-viper/src/encoder/pure_function_encoder.rs
+++ b/prusti-viper/src/encoder/pure_function_encoder.rs
@@ -948,14 +948,9 @@ impl<'p, 'v: 'p, 'tcx: 'v> BackwardMirInterpreter<'tcx>
                     vir::Expr::not(cond_val)
                 };
 
-                let assert_msg = if let mir::AssertKind::BoundsCheck{ .. } = msg {
-                    // Use the debug impl for BoundsCheck, as it is supposed to be handled before
-                    // calling display() according to the docs
-                    // TODO: use fmt_assert_args once https://github.com/rust-lang/rust/pull/84392 is merged
-                    format!("{:?}", msg)
-                } else {
-                    msg.description().to_string()
-                };
+                let mut assert_msg = String::new();
+                msg.fmt_assert_args(&mut assert_msg).unwrap();
+
                 let pos = self.encoder.error_manager().register(
                     term.source_info.span,
                     ErrorCtxt::PureFunctionAssertTerminator(assert_msg),