Improved handling of micromega caches

- Specialised hash and equality functions.
  Avoid collisions in extreme scenarios.
- Flags to disable the use of the caches.

fixes #10772

1 files changed, 2 insertions, 2 deletions

diff --git a/plugins/micromega/persistent_cache.ml b/plugins/micromega/persistent_cache.ml
index 14a1bc9712..14e2e40846 100644
--- a/plugins/micromega/persistent_cache.ml
+++ b/plugins/micromega/persistent_cache.ml
@@ -127,7 +127,7 @@ let open_in f =
     match read_key_elem inch with
       | None -> ()
       | Some (key,elem) ->
-          Table.replace htbl key elem ;
+          Table.add htbl key elem ;
 	  xload () in
     try
       (* Locking of the (whole) file while reading *)
@@ -164,7 +164,7 @@ let add t k e =
     else
       let fd = descr_of_out_channel outch in
       begin
-       Table.replace tbl k e ;
+       Table.add tbl k e ;
        do_under_lock Write fd 
         (fun _ -> 
          Marshal.to_channel outch (k,e) [Marshal.No_sharing] ;