diff --git a/src/plugins/e-acsl/src/libraries/misc.ml b/src/plugins/e-acsl/src/libraries/misc.ml
index 839b26676fdf56b33b4c4b0fd58f62755f2e762a..e1ea93a8e4b694429e13b6f8980df08e7b9b5e1a 100644
--- a/src/plugins/e-acsl/src/libraries/misc.ml
+++ b/src/plugins/e-acsl/src/libraries/misc.ml
@@ -217,8 +217,9 @@ module Id_term =
     (struct
       include Cil_datatype.Term
       let name = "E_ACSL.Id_term"
-      let compare (t1:term) t2 =
-        if t1 == t2 then 0 else Cil_datatype.Term.compare t1 t2
+      let compare _ _ =
+        (* There is no sound comparison based on physical identity. *)
+        Kernel.fatal "Id_term: comparison undefined (and undefinable)"
       let equal (t1:term) t2 = t1 == t2
       let structural_descr = Structural_descr.t_abstract
       let rehash = Datatype.identity
diff --git a/src/plugins/e-acsl/src/libraries/misc.mli b/src/plugins/e-acsl/src/libraries/misc.mli
index 16706184a7f1a478815d49234773f5ae1defedc2..b1bff7698f6d4a770e6b006247363b17e599d369 100644
--- a/src/plugins/e-acsl/src/libraries/misc.mli
+++ b/src/plugins/e-acsl/src/libraries/misc.mli
@@ -82,7 +82,10 @@ val finite_min_and_max: Ival.t -> Integer.t * Integer.t
 (** [finite_min_and_max i] takes the finite ival [i] and returns its bounds. *)
 
 module Id_term: Datatype.S_with_collections with type t = term
-(** Datatype for terms that relies on physical equality. *)
+(** Datatype for terms that relies on physical equality.
+    Note that of its collections only [Hashtbl] can be used.
+    Using [Map] and [Set] raises a fatal error as they require a comparison
+    function, which cannot be defined in a sound way for physical equality. *)
 
 val extract_uncoerced_lval: exp -> exp option
 (** Unroll the [CastE] part of the expression until an [Lval] is found, and