Fix compilation errors

2 files changed, 6 insertions, 6 deletions

diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml
index c4c090e3..029a2f1e 100644
--- a/src/InterpreterBorrows.ml
+++ b/src/InterpreterBorrows.ml
@@ -746,7 +746,7 @@ let give_back (config : C.config) (l : V.BorrowId.id) (bc : g_borrow_content)
     a reference whose region has already ended).
  *)
 let convert_avalue_to_value (av : V.typed_avalue) : V.typed_value =
-  mk_fresh_symbolic_typed_value av.V.sv_ty
+  mk_fresh_symbolic_typed_value av.V.ty
 
 (** End a borrow identified by its borrow id in a context
     
@@ -1136,11 +1136,11 @@ and end_abstraction_borrows (config : C.config) (abs_id : V.AbstractionId.id)
   | FoundAProjBorrows (sv, proj_ty) ->
       (* Replace the proj_borrows - there should be exactly one *)
       let ctx =
-        update_intersecting_aproj_borrows_non_shared regions sv
+        update_intersecting_aproj_borrows_non_shared abs.regions sv
           V.AEndedProjBorrows ctx
       in
       (* Give back a fresh symbolic value *)
-      let nsv = mk_fresh_symbolic_typed_value proj_ty in
+      let nsv = mk_fresh_symbolic_value proj_ty in
       let ctx = give_back_symbolic_value config sv nsv ctx in
       (* Reexplore *)
       end_abstraction_borrows config abs_id ctx
diff --git a/src/InterpreterUtils.ml b/src/InterpreterUtils.ml
index 2886f642..b76ae28c 100644
--- a/src/InterpreterUtils.ml
+++ b/src/InterpreterUtils.ml
@@ -59,11 +59,11 @@ let mk_fresh_symbolic_value (ty : T.rty) : V.symbolic_value =
   svalue
 
 (** Create a fresh symbolic value *)
-let mk_fresh_symbolic_value (rty : T.rty) : V.symbolic_value =
-  let ty = Subst.erase_regions ty in
+let mk_fresh_symbolic_typed_value (rty : T.rty) : V.typed_value =
+  let ty = Subst.erase_regions rty in
   (* Generate the fresh a symbolic value *)
   let value = mk_fresh_symbolic_value rty in
-  let value = V.Symbolic svalue in
+  let value = V.Symbolic value in
   { V.value; V.ty }
 
 (** Create a typed value from a symbolic value. *)