From 4c30e381a96a4d1a0d2dab20fbcc08bd91cad0ec Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 1 Dec 2022 00:36:12 +0100
Subject: Make minor modifications

---
 compiler/InterpreterBorrows.ml  | 8 +++++++-
 compiler/InterpreterBorrows.mli | 4 ++++
 2 files changed, 11 insertions(+), 1 deletion(-)

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