From 65b89a6b06b5ff2e26883800702cda19d2d980df Mon Sep 17 00:00:00 2001
From: Frédéric Besson
Date: Tue, 17 Sep 2019 18:09:06 +0200
Subject: 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
---
 plugins/micromega/persistent_cache.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins/micromega/persistent_cache.ml')

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] ;
-- 
cgit v1.2.3