diff --git a/src/kernel_services/ast_queries/acsl_extension.mli b/src/kernel_services/ast_queries/acsl_extension.mli
index d5c76f546f301125f799cebf67634b592d1c27e9..a8889b0899e2f56278e39f9966aa9245bf18aa82 100644
--- a/src/kernel_services/ast_queries/acsl_extension.mli
+++ b/src/kernel_services/ast_queries/acsl_extension.mli
@@ -173,7 +173,7 @@ val register_code_annot_next_both: register_extension
 
    New type and function symbols shall be created with `Cil.make_xxx` functions.
    The registered symbols {i will} be automatically prefixed with the name of
-   the imported module.
+   the imported module if necessary.
 
    The register module importer function might be invoked several times,
    typically when a given module is imported from several files. Although
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index f2158c1dc0b543ef55aa170dfdfeb08d9acd0edb..22360e6fe582f10b98ea8bdecadcd3dd33548905 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -854,7 +854,9 @@ struct
         end
 
   let make_module_builder (decls : global_annotation list ref) moduleId =
-    let wrap = Printf.sprintf "%s::%s" moduleId in
+    let prefix = moduleId ^ "::" in
+    let wrap s =
+      if String.starts_with ~prefix s then s else prefix ^ s in
     let add_logic_ctor loc ct =
       ct.ctor_name <- wrap ct.ctor_name ;
       add_logic_ctor loc ct in