From 7bd3b03e28ac8591aad130b52376f0827af69e91 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 17 Dec 2021 18:55:06 +0100
Subject: Update give_back

---
 src/Interpreter.ml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index cb883768..3101ebaf 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -1507,7 +1507,11 @@ let give_back (config : C.config) (l : V.BorrowId.id) (bc : g_borrow_content)
       assert (Option.is_some (lookup_loan_opt sanity_ek l ctx));
       (* Update the context *)
       give_back_shared config l ctx
-  | Abstract (V.AIgnoredSharedBorrow _) -> raise Unimplemented
+  | Abstract (V.AIgnoredSharedBorrow asb) ->
+      (* Sanity check *)
+      assert (borrow_in_asb l asb);
+      (* Update the context *)
+      give_back_shared config l ctx
   | Abstract (V.AIgnoredMutBorrow _) -> failwith "Unreachable"
 
 (** End a borrow identified by its borrow id in a context
-- 
cgit v1.2.3