diff --git a/src/plugins/obfuscator/obfuscate.ml b/src/plugins/obfuscator/obfuscate.ml
index 3decde3ce5cfa10d312011200841cf9c4f6412f4..ce98d74285882c360f909fe8a7951d699b74ae68 100644
--- a/src/plugins/obfuscator/obfuscate.ml
+++ b/src/plugins/obfuscator/obfuscate.ml
@@ -166,12 +166,13 @@ class visitor = object
     Cil.DoChildren
 
   method! vannotation = function
-    | Daxiomatic(str, _, _, _) ->
-      warn "axiomatic" str;
-      Cil.DoChildren
-    | Dlemma(str, _, _, { tp_kind }, _, _) ->
-      warn (Cil_printer.string_of_lemma tp_kind) str;
-      Cil.DoChildren
+    | Daxiomatic(str, globs, attrs, loc) ->
+      let str' = Dictionary.fresh Obfuscator_kind.Axiomatic str in
+      Cil.ChangeDoChildrenPost(Daxiomatic(str',globs,attrs,loc),Extlib.id)
+    | Dlemma(str, labs, typs, pred, attrs, loc) ->
+      let str' = Dictionary.fresh Obfuscator_kind.Lemma str in
+      Cil.ChangeDoChildrenPost(
+        Dlemma(str',labs,typs, pred, attrs, loc),Extlib.id)
     | _ ->
       Cil.DoChildren
 
diff --git a/src/plugins/obfuscator/obfuscator_kind.ml b/src/plugins/obfuscator/obfuscator_kind.ml
index e1f1513784abd71faf1fb5af430a702c31b49a48..1e5c410045b8fd8c67c8c95098d316f57969e921 100644
--- a/src/plugins/obfuscator/obfuscator_kind.ml
+++ b/src/plugins/obfuscator/obfuscator_kind.ml
@@ -36,6 +36,8 @@ type k =
   | Type
   | Logic_type
   | Logic_constructor
+  | Axiomatic
+  | Lemma
 
 let name_of_kind = function
   | Behavior -> "behavior"
@@ -53,6 +55,8 @@ let name_of_kind = function
   | Type -> "type"
   | Logic_type -> "logic type"
   | Logic_constructor -> "logic constructor"
+  | Axiomatic -> "axiomatic"
+  | Lemma -> "lemma"
 
 let prefix = function
   | Behavior -> "B"
@@ -70,6 +74,8 @@ let prefix = function
   | Type -> "T"
   | Logic_type -> "LT"
   | Logic_constructor -> "LC"
+  | Axiomatic -> "A"
+  | Lemma -> "LE"
 
 include Datatype.Make_with_collections
     (struct
diff --git a/src/plugins/obfuscator/obfuscator_kind.mli b/src/plugins/obfuscator/obfuscator_kind.mli
index 75fd6bb8af5a3a00662520b265423f5bbab6a2e2..8eee3ce7ad4b63c5894a2fc93f257f1dfce7d219 100644
--- a/src/plugins/obfuscator/obfuscator_kind.mli
+++ b/src/plugins/obfuscator/obfuscator_kind.mli
@@ -36,6 +36,8 @@ type k =
   | Type
   | Logic_type
   | Logic_constructor
+  | Axiomatic
+  | Lemma
 
 include Datatype.S_with_collections with type t = k
 val prefix: t -> string
diff --git a/tests/misc/oracle/obfuscate.res.oracle b/tests/misc/oracle/obfuscate.res.oracle
index e36f5683039a52a8e2255c55ac546ff4fac23d02..2f53420c9b5f02ce608dcda753a9e54dfc6c90d3 100644
--- a/tests/misc/oracle/obfuscate.res.oracle
+++ b/tests/misc/oracle/obfuscate.res.oracle
@@ -2,12 +2,12 @@
 [obfuscator] Warning: unobfuscated attribute name `fc_stdlib'
 [obfuscator] Warning: unobfuscated attribute parameter name `stdint.h'
 [obfuscator] Warning: unobfuscated attribute name `missingproto'
-[obfuscator] Warning: unobfuscated axiomatic name `A'
-[obfuscator] Warning: unobfuscated axiomatic name `A1'
-[obfuscator] Warning: unobfuscated lemma name `OK'
 /* *********************************** */
 /* start of dictionary for obfuscation */
 /* *********************************** */
+// axiomatics
+#define A1 A
+#define A2 A1
 // behaviors
 #define B1 bhv
 // enums
@@ -31,6 +31,8 @@
 // logic constructors
 #define LC1 T
 #define LC2 F
+// lemmas
+#define LE1 OK
 // logic types
 #define LT1 t
 // logic variables
@@ -172,12 +174,12 @@ void F6(struct T2 *f6)
   return;
 }
 
-/*@ axiomatic A {
+/*@ axiomatic A1 {
       predicate LV3(void (*LV4)()) ;
       
       }
  */
-/*@ axiomatic A1 {
+/*@ axiomatic A2 {
       predicate LV5(void (*LV6)()) ;
       
       }
@@ -188,7 +190,7 @@ void F7(void)
   return;
 }
 
-/*@ lemma OK{L}: LV3((void (*)())(&F7)) ∧ LV5((void (*)())(&F7));
+/*@ lemma LE1{L}: LV3((void (*)())(&F7)) ∧ LV5((void (*)())(&F7));
 
 */