diff --git a/src/kernel_services/ast_queries/logic_utils.ml b/src/kernel_services/ast_queries/logic_utils.ml
index d7e5d704db6d2a83a7466a157c835b1eb66b64e9..347c154d719146a0232ab1256ce35a79843b1cd0 100644
--- a/src/kernel_services/ast_queries/logic_utils.ml
+++ b/src/kernel_services/ast_queries/logic_utils.ml
@@ -2349,6 +2349,15 @@ class complete_types =
              not (isLogicType Cil.isCompleteType t.term_type) ->
         ChangeDoChildrenPost({ t with term_type = v.lv_type }, fun x -> x)
       | _ -> DoChildrenPost self#insert_cast_term
+
+    method! vinst = function
+      | Code_annot _ -> Cil.DoChildren
+      | _ -> Cil.SkipChildren
+
+    method! vexpr _ = Cil.SkipChildren
+    method! vlval _ = Cil.SkipChildren
+    method! vtype _ = Cil.SkipChildren
+    method! vinit _ _ _ = Cil.SkipChildren
   end
 
 let complete_types f = Cil.visitCilFile (new complete_types) f