Make the symbolic, borrow, region and abstration counters global and

stateful

1 files changed, 1 insertions, 7 deletions

diff --git a/src/InterpreterProjectors.ml b/src/InterpreterProjectors.ml
index 21c9e034..3fa824ab 100644
--- a/src/InterpreterProjectors.ml
+++ b/src/InterpreterProjectors.ml
@@ -475,12 +475,10 @@ let prepare_reborrows (config : C.config) (allow_reborrows : bool)
     (ctx : C.eval_ctx) :
     (V.BorrowId.id -> V.BorrowId.id) * (C.eval_ctx -> C.eval_ctx) =
   let reborrows : (V.BorrowId.id * V.BorrowId.id) list ref = ref [] in
-  let borrow_counter = ref ctx.C.borrow_counter in
   (* The function to generate and register fresh reborrows *)
   let fresh_reborrow (bid : V.BorrowId.id) : V.BorrowId.id =
     if allow_reborrows then (
-      let bid', cnt' = V.BorrowId.fresh !borrow_counter in
-      borrow_counter := cnt';
+      let bid' = C.fresh_borrow_id () in
       reborrows := (bid, bid') :: !reborrows;
       bid')
     else failwith "Unexpected reborrow"
@@ -489,13 +487,9 @@ let prepare_reborrows (config : C.config) (allow_reborrows : bool)
   let apply_registered_reborrows (ctx : C.eval_ctx) : C.eval_ctx =
     match config.C.mode with
     | C.ConcreteMode ->
-        (* Reborrows are introduced when applying projections in symbolic mode *)
-        assert (!borrow_counter = ctx.C.borrow_counter);
         assert (!reborrows = []);
         ctx
     | C.SymbolicMode ->
-        (* Update the borrow counter *)
-        let ctx = { ctx with C.borrow_counter = !borrow_counter } in
         (* Apply the reborrows *)
         apply_reborrows !reborrows ctx
   in