Make minor modifications

2 files changed, 11 insertions, 1 deletions

diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml
index 4e05dda7..9a78e77a 100644
--- a/compiler/InterpreterBorrows.ml
+++ b/compiler/InterpreterBorrows.ml
@@ -2405,7 +2405,13 @@ let ctx_merge_regions (ctx : C.eval_ctx) (rid : T.RegionId.id)
       List.map (Substitute.typed_avalue_subst_rids rsubst) abs.V.avalues
     in
     let regions = T.RegionId.Set.diff abs.V.regions rids in
-    let ancestors_regions = T.RegionId.Set.diff abs.V.ancestors_regions rids in
+    let ancestors_regions =
+      if T.RegionId.Set.disjoint abs.V.ancestors_regions rids then
+        abs.V.ancestors_regions
+      else
+        T.RegionId.Set.add rid
+          (T.RegionId.Set.diff abs.V.ancestors_regions rids)
+    in
     { abs with V.avalues; regions; ancestors_regions }
   in
 
diff --git a/compiler/InterpreterBorrows.mli b/compiler/InterpreterBorrows.mli
index 53297bc7..51c6c592 100644
--- a/compiler/InterpreterBorrows.mli
+++ b/compiler/InterpreterBorrows.mli
@@ -203,6 +203,10 @@ type merge_duplicates_funcs = {
 
 (** Merge two abstractions together.
 
+    We insert the result of the merge in place of the first abstraction (this
+    helps preserving the structure of the environment, when computing loop
+    fixed points for instance).
+
     When we merge two abstractions together, we remove the loans/borrows
     which appear in one and whose associated loans/borrows appear in the
     other. For instance: