allow renaming variables named 'set' in ghost declarations

src/backends/C/c_backend_spec.ml

@@ -1928,7 +1928,9 @@ let sanitize_expr = function
 let sanitize_predicate = function
   | Transition (st, f, inst, i, vs, r, mf, mfinsts) ->
     Transition (st, f, inst, i, List.map sanitize_expr vs, r, mf, mfinsts)
-  | p ->
+  | GhostAssign (x, v) ->
+    GhostAssign (sanitize_var_decl x, sanitize_value v)
+  | (Reset _ | MemoryPack _ | MemoryPackBase _) as p ->
     p
 
 let rec sanitize_formula = function
@@ -1954,7 +1956,7 @@ let rec sanitize_formula = function
     ExistsMem (m, sanitize_formula f1, sanitize_formula f2)
   | Value v ->
     Value (sanitize_value v)
-  | f ->
+  | (True | False | StateVarPack _ | MemoryPackToplevel _) as f ->
     f
 
 and sanitize_formulae fs = List.map (fun spec -> sanitize_formula spec) fs