Update the projectors to ignore values when they don't contain regions

of interest

1 files changed, 2 insertions, 2 deletions

diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml
index d172d1b7..3eb7322b 100644
--- a/src/InterpreterStatements.ml
+++ b/src/InterpreterStatements.ml
@@ -883,7 +883,7 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config)
   let ret_sv_ty = inst_sg.A.output in
   let ret_spc = mk_fresh_symbolic_value ret_sv_ty in
   let ret_value = mk_typed_value_from_symbolic_value ret_spc in
-  let ret_av = mk_aproj_loans_from_symbolic_value ret_spc in
+  let ret_av regions = mk_aproj_loans_from_symbolic_value regions ret_spc in
   (* Evaluate the input operands *)
   let ctx, args = eval_operands config ctx args in
   let args_with_rtypes = List.combine args inst_sg.A.inputs in
@@ -908,7 +908,7 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config)
         ctx args_with_rtypes
     in
     (* Group the input and output values *)
-    let avalues = List.append args_projs [ ret_av ] in
+    let avalues = List.append args_projs [ ret_av abs.regions ] in
     (* Add the avalues to the abstraction *)
     let abs = { abs with avalues } in
     (* Insert the abstraction in the context *)