From b1105c75ea54f38155ca86c62711082ce0bc325d Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 26 Jan 2022 23:20:54 +0100
Subject: Fix various issues

---
 src/InterpreterBorrows.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'src/InterpreterBorrows.ml')

diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml
index b231722d..d2964c90 100644
--- a/src/InterpreterBorrows.ml
+++ b/src/InterpreterBorrows.ml
@@ -454,6 +454,7 @@ let give_back_symbolic_value (_config : C.config)
           V.AProjBorrows (nsv, sv.V.sv_ty)
       | _ -> failwith "Unreachable"
     in
+    (* TODO: this actually doesn't work, or at least there is something subtle... *)
     V.AProjLoans (sv, (mv, child_proj) :: local_given_back)
   in
   update_intersecting_aproj_loans proj_regions proj_ty sv subst ctx
-- 
cgit v1.2.3