From b2d5671516b60ae83778b26867a8e5b6060f519d Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 27 Jan 2022 11:43:59 +0100
Subject: Introduce AEndedSharedBorrow so as not to introduce ABottom when
 ending shared aborrows

---
 src/InterpreterBorrowsCore.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'src/InterpreterBorrowsCore.ml')

diff --git a/src/InterpreterBorrowsCore.ml b/src/InterpreterBorrowsCore.ml
index b4ab7706..941ac140 100644
--- a/src/InterpreterBorrowsCore.ml
+++ b/src/InterpreterBorrowsCore.ml
@@ -434,7 +434,8 @@ let lookup_borrow_opt (ek : exploration_kind) (l : V.BorrowId.id)
         | V.AIgnoredMutBorrow (_, _)
         | V.AEndedMutBorrow _
         | V.AEndedIgnoredMutBorrow
-            { given_back_loans_proj = _; child = _; given_back_meta = _ } ->
+            { given_back_loans_proj = _; child = _; given_back_meta = _ }
+        | V.AEndedSharedBorrow ->
             super#visit_aborrow_content env bc
         | V.AProjSharedBorrow asb ->
             if borrow_in_asb l asb then
@@ -548,7 +549,7 @@ let update_aborrow (ek : exploration_kind) (l : V.BorrowId.id) (nv : V.avalue)
         | V.ASharedBorrow bid ->
             if bid = l then update ()
             else V.ABorrow (super#visit_ASharedBorrow env bid)
-        | V.AIgnoredMutBorrow _ | V.AEndedMutBorrow _
+        | V.AIgnoredMutBorrow _ | V.AEndedMutBorrow _ | V.AEndedSharedBorrow
         | V.AEndedIgnoredMutBorrow _ ->
             super#visit_ABorrow env bc
         | V.AProjSharedBorrow asb ->
-- 
cgit v1.2.3