diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 6d268f2117d9547ae03dcc531a3a88e49859d816..c0aa7ec4d8c4dc503bfcacd4540d6b9f8817bb79 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -1130,10 +1130,21 @@ let alphaConvertVarAndAddToEnv addtoenv vi =
                 vi.vname newname Cil_printer.pp_location oldloc;
           end
       end else begin
-        (* We have changed the name of a local variable. Can we try to detect
-         * if the other variable was also local in the same scope? Not for
-         * now. *)
-        copyVarinfo vi newname
+        (* favor renaming ghost variables over non-ghost ones *)
+        if not vi.vghost then begin
+          let siblings =
+            fst @@ List.split @@
+            Datatype.String.Hashtbl.find_all ghost_env vi.vname
+          in
+          let check = function
+            | EnvVar vi' -> vi!=vi' && vi.vname = vi'.vname
+            | _ -> false
+          in
+          match List.find_opt check siblings with
+          | Some (EnvVar ({ vghost = true } as oldvi)) ->
+            oldvi.vname <- newname; vi
+          | _ -> copyVarinfo vi newname
+        end else copyVarinfo vi newname
       end
     end
   in
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 14b0d96135b65de457a9533562071955a50e374b..d52be341225739de126ccc744555a101393a6d96 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -6450,12 +6450,15 @@ let uniqueVarNames (f: file) : unit =
                 newname Location.pretty oldloc ;
             v.vname <- newname
           in
-          (* Do the formals first *)
-          List.iter processLocal fdec.sformals;
+          let ghost vi = vi.vghost in
+          let formals_ghost, formals = List.partition ghost fdec.sformals in
+          let locals_ghost, locals = List.partition ghost fdec.slocals in
+          List.iter processLocal formals;
+          List.iter processLocal locals;
+          List.iter processLocal formals_ghost;
+          List.iter processLocal locals_ghost;
           (* Fix the type again *)
           setFormals fdec fdec.sformals;
-          (* And now the locals *)
-          List.iter processLocal fdec.slocals;
           (* Undo the changes to the global table *)
           Alpha.undoAlphaChanges gAlphaTable !undolist;
           ()
diff --git a/tests/syntax/oracle/ghost_local_capture.res.oracle b/tests/syntax/oracle/ghost_local_capture.res.oracle
index 648e40245cd0098fbd3a8d9b7dd52e785ef84979..9ec3c5e8a407511204a83f21caa661beb0f7c832 100644
--- a/tests/syntax/oracle/ghost_local_capture.res.oracle
+++ b/tests/syntax/oracle/ghost_local_capture.res.oracle
@@ -18,17 +18,17 @@ void titi(void)
 
 void toto(void)
 {
-  /*@ ghost int c = 1; */
+  /*@ ghost int c_0 = 1; */
   {
     L0: ;
-    int c_0 = 0;
+    int c = 0;
     L1: ;
-    c_0 = 2;
-    /*@ assert c_0 ≡ 2; */ ;
-    /*@ assert \at(c,L0) ≡ 1; */ ;
-    /*@ assert \at(c_0,L1) ≡ 0; */ ;
+    c = 2;
+    /*@ assert c ≡ 2; */ ;
+    /*@ assert \at(c_0,L0) ≡ 1; */ ;
+    /*@ assert \at(c,L1) ≡ 0; */ ;
   }
-  /*@ assert c ≡ 1; */ ;
+  /*@ assert c_0 ≡ 1; */ ;
   return;
 }