From 0658739222a23474c5453eb32f282587ae8eb95e Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 13 Jan 2022 21:56:36 +0100
Subject: Update the projectors to ignore values when they don't contain
 regions of interest

---
 src/InterpreterBorrows.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'src/InterpreterBorrows.ml')

diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml
index ebfd87c7..d8c2f3a8 100644
--- a/src/InterpreterBorrows.ml
+++ b/src/InterpreterBorrows.ml
@@ -316,9 +316,10 @@ let give_back_value (config : C.config) (bid : V.BorrowId.id)
                * and the given back value is thus a symbolic value *)
               match nv.V.value with
               | V.Symbolic sv ->
+                  let abs = Option.get opt_abs in
                   (* The loan projector *)
                   let given_back_loans_proj =
-                    mk_aproj_loans_from_symbolic_value sv
+                    mk_aproj_loans_from_symbolic_value abs.regions sv
                   in
                   (* Continue giving back in the child value *)
                   let child = super#visit_typed_avalue opt_abs child in
-- 
cgit v1.2.3