diff --git a/source/rust_verify/src/lifetime_ast.rs b/source/rust_verify/src/lifetime_ast.rs
index 02a510d22b..269c8554c8 100644
--- a/source/rust_verify/src/lifetime_ast.rs
+++ b/source/rust_verify/src/lifetime_ast.rs
@@ -176,7 +176,7 @@ pub(crate) struct FunDecl {
     pub(crate) name_span: Span,
     pub(crate) name: Id,
     pub(crate) generics: Vec<GenericParam>,
-    pub(crate) params: Vec<(Option<Span>, Id, Typ)>,
+    pub(crate) params: Vec<(Option<Span>, Id, Typ, bool)>,
     pub(crate) ret: Option<(Option<Span>, Typ)>,
     pub(crate) body: Exp,
 }
diff --git a/source/rust_verify/src/lifetime_emit.rs b/source/rust_verify/src/lifetime_emit.rs
index f7cd341294..8b754aa1a4 100644
--- a/source/rust_verify/src/lifetime_emit.rs
+++ b/source/rust_verify/src/lifetime_emit.rs
@@ -692,13 +692,11 @@ pub(crate) fn emit_fun_decl(state: &mut EmitState, f: &FunDecl) {
     emit_generic_params(state, &f.generics);
     state.write("(");
     state.push_indent();
-    for (span, x, typ) in f.params.iter() {
+    for (span, x, typ, is_mut_var) in f.params.iter() {
         state.newline();
-        // For checking lifetimes, we make all function parameters mutable.
-        // This way, we do not have to closely track which parameters are
-        // mutable and which are not. This should not have an impact on
-        // the result of the lifetime analysis.
-        state.write("mut ");
+        if *is_mut_var {
+            state.write("mut ");
+        }
         if let Some(span) = span {
             state.write_spanned(x.to_string(), *span);
         } else {
diff --git a/source/rust_verify/src/lifetime_generate.rs b/source/rust_verify/src/lifetime_generate.rs
index 1489d313c7..a44049e824 100644
--- a/source/rust_verify/src/lifetime_generate.rs
+++ b/source/rust_verify/src/lifetime_generate.rs
@@ -1600,11 +1600,22 @@ fn erase_fn_common<'tcx>(
         let name = state.fun_name(&fun_name);
         let inputs = &fn_sig.inputs();
         assert!(inputs.len() == f_vir.x.params.len());
-        let p_spans: Vec<Option<Span>> = if let Some(body) = body {
+        let params_info: Vec<(Option<Span>, bool)> = if let Some(body) = body {
             assert!(inputs.len() == body.params.len());
-            body.params.iter().map(|p| Some(p.pat.span)).collect()
+            body.params
+                .iter()
+                .map(|p| {
+                    let is_mut_var = match p.pat.kind {
+                        PatKind::Binding(rustc_hir::BindingAnnotation(_, mutability), _, _, _) => {
+                            mutability == rustc_hir::Mutability::Mut
+                        }
+                        _ => panic!("unexpected pat"),
+                    };
+                    (Some(p.pat.span), is_mut_var)
+                })
+                .collect()
         } else {
-            inputs.iter().map(|_| None).collect()
+            inputs.iter().map(|_| (None, false)).collect()
         };
         let mut lifetimes: Vec<GenericParam> = Vec::new();
         let mut typ_params: Vec<GenericParam> = Vec::new();
@@ -1612,20 +1623,24 @@ fn erase_fn_common<'tcx>(
             erase_mir_generics(ctxt, state, impl_id, false, &mut lifetimes, &mut typ_params);
         }
         erase_mir_generics(ctxt, state, id, true, &mut lifetimes, &mut typ_params);
-        let mut params: Vec<(Option<Span>, Id, Typ)> = Vec::new();
-        for ((input, param), sp) in inputs.iter().zip(f_vir.x.params.iter()).zip(p_spans.iter()) {
+        let mut params: Vec<(Option<Span>, Id, Typ, bool)> = Vec::new();
+        for ((input, param), param_info) in
+            inputs.iter().zip(f_vir.x.params.iter()).zip(params_info.iter())
+        {
             let name = if let Some((_, name)) = &param.x.unwrapped_info {
                 name.to_string()
             } else {
                 param.x.name.to_string()
             };
+            let is_mut_var = param_info.1;
+            let span = param_info.0;
             let x = state.local(name);
             let typ = if param.x.mode == Mode::Spec {
                 TypX::mk_unit()
             } else {
                 erase_ty(ctxt, state, input)
             };
-            params.push((*sp, x, typ));
+            params.push((span, x, typ, is_mut_var));
         }
         let ret = if let Some(sig) = sig {
             match sig.decl.output {