Fix HC collisions.

When hashing formulas, consider the type. This ensures consistency
with formula equality checks and reduces collision rates, enhancing
performance, especially with OCaml 5.

See ocaml/ocaml#13849 for more information.

Author: strub

src/ecAst.ml

@@ -999,8 +999,8 @@ module Hsform = Why3.Hashcons.Make (struct
        ty_equal f1.f_ty f2.f_ty
     && equal_node f1.f_node f2.f_node
 
-  let hash f =
-    match f.f_node with
+  let hash_node (f : f_node) =
+    match f with
     | Fquant(q, b, f) ->
         Why3.Hashcons.combine2 (f_hash f) (b_hash b) (qt_hash q)
 
@@ -1047,6 +1047,9 @@ module Hsform = Why3.Hashcons.Make (struct
     | FeagerF     eg   -> eg_hash eg
     | Fpr         pr   -> pr_hash pr
 
+  let hash (f : form) =
+    Why3.Hashcons.combine (ty_hash f.f_ty) (hash_node f.f_node)
+
   let fv_mlr = Sid.add mleft (Sid.singleton mright)
 
   let fv_node f =