diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 3d2fc0f9896cdda68b2e27eca1e5c9642d8e9b26..65dc019e650c436f6e781a36215d59a4f1218070 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -25,6 +25,8 @@
 Plugin E-ACSL <next-release>
 ############################
 
+-* E-ACSL       [2021-12-03] Fix crash when creating an axiomatic with an
+                existing name in E-ACSL's RTL (frama-c/e-acsl#161).
 -* E-ACSL       [2021-12-01] Fix crash when binding a lambda-abstraction to a
                 local variable (frama-c/e-acsl#189).
 -* e-acsl-gcc   [2021-11-30] Fix e-acsl-gcc.sh bash autocompletion script and
diff --git a/src/plugins/e-acsl/src/project_initializer/rtl.ml b/src/plugins/e-acsl/src/project_initializer/rtl.ml
index abdaad68f4529b167f64e23160b52e1ffffe2a84..671e517c3f12456093f38f4e994f203da23a2213 100644
--- a/src/plugins/e-acsl/src/project_initializer/rtl.ml
+++ b/src/plugins/e-acsl/src/project_initializer/rtl.ml
@@ -232,7 +232,7 @@ let lookup_rtl_globals rtl_ast =
         Assocs.add_kf g kf
       in
       do_it ~add ~assoc (fun _ -> Globals.Functions.mem_name vi.vname) acc l g
-    | GAnnot (Daxiomatic (name, galist, _, _), _) as g :: l ->
+    | GAnnot (Daxiomatic (name, galist, _, _) as ga, _) as g :: l ->
       (* processing axiomatics *)
       let fun_or_preds =
         (* extract the functions and predicates from the axiomatic *)
@@ -264,19 +264,43 @@ let lookup_rtl_globals rtl_ast =
            all its functions and predicates are in the user's project. If only
            some of them are in it then it is an error, and if none of them are
            then the axiomatic is not in the user's project. *)
-        if exists && not forall then
-          Options.abort
-            "@[The following logic functions or predicates@ \
-             are in conflict with logic functions or predicates from the@ \
-             axiomatic '%s' in the E-ACSL runtime library, please rename@ \
-             them:@ %a@]"
-            name
-            (Pretty_utils.pp_list
-               ~sep:",@ "
-               Printer.pp_logic_info)
-            conflicting_lis
-        else
-          forall
+        let in_user_prj =
+          if exists && not forall then
+            Options.abort
+              "@[The following logic functions or predicates@ \
+               are in conflict with logic functions or predicates from the@ \
+               axiomatic '%s' in the E-ACSL runtime library, please rename@ \
+               them:@ %a@]"
+              name
+              (Pretty_utils.pp_list
+                 ~sep:",@ "
+                 Printer.pp_logic_info)
+              conflicting_lis
+          else
+            forall
+        in
+        (* If the axiomatic is not "in the user's project", check if a different
+           axiomatic with the same name is in it. *)
+        if not in_user_prj then begin
+          let ip_from_ga = Property.ip_of_global_annotation ga in
+          let found =
+            try
+              Property_status.iter
+                (fun ppt ->
+                   if List.exists (Property.equal ppt) ip_from_ga
+                   then raise Exit);
+              false
+            with Exit ->
+              true
+          in
+          if found then
+            Options.abort
+              "@[The axiomatic '%s' is in conflict with an@ \
+               axiomatic with the same name in the E-ACSL runtime library,@ \
+               please rename it.@]"
+              name
+        end;
+        in_user_prj
       in
       let assoc _g =
         List.iter