diff --git a/src/plugins/aorai/aorai_utils.ml b/src/plugins/aorai/aorai_utils.ml
index 077cc38480e28e1258dddc52da8e8a90c8f34608..ca4ed6893bbdcbca3bdb9730b07960e9c79bb71f 100644
--- a/src/plugins/aorai/aorai_utils.ml
+++ b/src/plugins/aorai/aorai_utils.ml
@@ -679,7 +679,6 @@ let add_global glob = globals_queue := glob :: !globals_queue
 (* Utilities for global variables *)
 let add_gvar ?init vi =
   let initinfo = {Cil_types.init} in
-  vi.vghost <- true;
   vi.vstorage <- NoStorage;
   add_global (GVar(vi,initinfo,vi.vdecl));
   Globals.Vars.add vi initinfo;
@@ -700,7 +699,7 @@ let mk_gvar ?init ~ty name =
       Globals.Vars.remove vi;
       vi
     with Not_found ->
-      Cil.makeGlobalVar name ty
+      Cil.makeGlobalVar ~ghost:true name ty
   in
   add_gvar ?init vi
 
diff --git a/src/plugins/aorai/data_for_aorai.ml b/src/plugins/aorai/data_for_aorai.ml
index 14d19b1b0859e3d71be9a323212c2af3d35c030d..272897682ca8d26ffb9b90e7fddda8d2f9087900 100644
--- a/src/plugins/aorai/data_for_aorai.ml
+++ b/src/plugins/aorai/data_for_aorai.ml
@@ -99,7 +99,7 @@ module State_var =
     end)
 
 let get_state_var =
-  let add_var state = Cil.makeVarinfo true false state.name Cil.intType in
+  let add_var state = Cil.makeGlobalVar ~ghost:true state.name Cil.intType in
   State_var.memo add_var
 
 let get_state_logic_var state = Cil.cvar_to_lvar (get_state_var state)
@@ -339,7 +339,9 @@ let pebble_set_at li lab =
 let memo_multi_state st =
   match st.multi_state with
   | None ->
-    let aux = Cil.makeGlobalVar (get_fresh "aorai_aux") Cil.intType in
+    let aux =
+      Cil.makeGlobalVar ~ghost:true (get_fresh "aorai_aux") Cil.intType
+    in
     let laux = Cil.cvar_to_lvar aux in
     let set = Cil_const.make_logic_info (get_fresh (st.name ^ "_pebble")) in
     let typ = Logic_const.make_set_type (Ctype Cil.intType) in
@@ -572,7 +574,7 @@ let memo_aux_variable tr counter used_prms vi =
       | Some _ -> TArray(vi.vtype,None,[])
     in
     let my_var =
-      Cil.makeGlobalVar (get_fresh ("aorai_" ^ vi.vname)) my_type
+      Cil.makeGlobalVar ~ghost:true (get_fresh ("aorai_" ^ vi.vname)) my_type
     in
     add_aux_variable my_var;
     let my_lvar = Cil.cvar_to_lvar my_var in
@@ -1156,7 +1158,9 @@ let rec type_seq default_state tr metaenv env needs_pebble curr_start curr_end s
           else Cil.intType
         in (* We won't always need a counter *)
         lazy (
-          let vi = Cil.makeGlobalVar (get_fresh "aorai_counter") ty in
+          let
+            vi = Cil.makeGlobalVar ~ghost:true (get_fresh "aorai_counter") ty
+          in
           add_aux_variable vi;
           vi
         )
@@ -1358,6 +1362,7 @@ let type_trans auto metaenv env tr =
         let start = tr.start in
         let count = (* TODO: make it an integer. *)
           Cil.makeGlobalVar
+            ~ghost:true
             (get_fresh ("aorai_cnt_" ^ start.name)) Cil.intType
         in
         add_aux_variable count;
diff --git a/src/plugins/aorai/yaparser.mly b/src/plugins/aorai/yaparser.mly
index fc6ea315e04c259d37ef20639c793b83b4678547..3e715519933eb404e1717b8df32f463215d07175 100644
--- a/src/plugins/aorai/yaparser.mly
+++ b/src/plugins/aorai/yaparser.mly
@@ -100,7 +100,10 @@ let add_metavariable map (name,typename) =
   in
   if Datatype.String.Map.mem name map then
     Aorai_option.abort "The metavariable %s is declared twice" name;
-  let vi = Cil.makeGlobalVar (Data_for_aorai.get_fresh ("aorai_" ^ name)) ty in
+  let vi =
+    Cil.makeGlobalVar
+      ~ghost:true (Data_for_aorai.get_fresh ("aorai_" ^ name)) ty
+  in
   Datatype.String.Map.add name vi map
 
 let check_state st =