diff options
| -rw-r--r-- | src/Interpreter.ml | 6 |
1 files changed, 5 insertions, 1 deletions
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 |