diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 213647c8ba91c50ab951092ce331de6163edaf9b..0a6d498f7f95a20564a6dfc4e768a4d66bfc7fbe 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -2749,14 +2749,18 @@ let makeGlobalVarinfo (isadef: bool) (vi: varinfo) : varinfo * bool =
          prototypes. Logic specifications refer to the varinfo in this table. *)
       begin
         match vi.vtype with
-        | TFun (_,Some formals , _, _) ->
+        | TFun (_, Some formals , _, _) ->
           (try
              let old_formals_env = getFormalsDecl oldvi in
              List.iter2
                (fun old ((name,typ,attr) as decl) ->
                   let new_ghost = Cil.isGhostFormalVarDecl decl in
                   if old.vghost <> new_ghost then
-                    raise (Invalid_argument "Incompatible ghost status")
+                    abort_context
+                      "Function %a redeclared with incompatible ghost status \
+                       in formals (original declaration was at %a)"
+                      Cil_datatype.Varinfo.pretty vi
+                      Cil_datatype.Location.pretty oldloc
                   else if name <> "" then begin
                     Kernel.debug ~dkey:Kernel.dkey_typing_global
                       "replacing formal %s with %s" old.vname name;
@@ -2765,24 +2769,15 @@ let makeGlobalVarinfo (isadef: bool) (vi: varinfo) : varinfo * bool =
                       Cil.update_var_type old typ;
                       old.vattr <- attr;
                     end;
-                    (match old.vlogic_var_assoc with
-                     | None -> ()
-                     | Some old_lv -> old_lv.lv_name <- name)
+                    match old.vlogic_var_assoc with
+                    | None -> ()
+                    | Some old_lv -> old_lv.lv_name <- name
                   end)
                old_formals_env
-               formals;
-           with
-           | Invalid_argument _ ->
-             abort_context
-               "Function %a redeclared with incompatible formals \
-                (original declaration was at %a)"
-               Cil_datatype.Varinfo.pretty vi
-               Cil_datatype.Location.pretty oldloc
-             ;
-           | Not_found ->
-             Cil.setFormalsDecl oldvi vi.vtype)
+               formals
+           with Not_found -> Cil.setFormalsDecl oldvi vi.vtype)
         | _ -> ()
-      end ;
+      end;
       (* if [isadef] is true, [vi] is a definition.  *)
       if isadef then begin
         (* always favor the location of the definition.*)
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 0b407312c002d8a823f6676a417178926cca7a28..5948613d72cea59c2d6f277f02477c2c95866b81 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -760,7 +760,6 @@ let setFormals (f: fundec) (forms: varinfo list) =
   unsafeSetFormalsDecl f.svar forms;
   List.iter (fun v -> v.vformal <- true) forms;
   f.sformals <- forms; (* Set the formals *)
-  assert (getFormalsDecl f.svar == f.sformals);
   match unrollType f.svar.vtype with
     TFun(rt, _, isva, fa) ->
     update_var_type f.svar