From 0f2ce5dd56dc1001d5ba7128e6f0ac83ea499267 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 21 Apr 2022 12:50:37 +0200
Subject: Cleanup and update comments

---
 src/SymbolicToPure.ml | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

(limited to 'src/SymbolicToPure.ml')

diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
index 65bdcf9c..e32e28d6 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -640,7 +640,7 @@ let rec typed_value_to_rvalue (ctx : bs_ctx) (v : V.typed_value) : typed_rvalue
             (translate mv).value
         | V.InactivatedMutBorrow (mv, _) ->
             (* Same as for shared borrows. However, note that we use inactivated borrows
-             * only in meta-data: a value actually used in the translation can't come
+             * only in meta-data: a value actually *used in the translation* can't come
              * from an unpromoted inactivated borrow *)
             (translate mv).value
         | V.MutBorrow (_, v) ->
@@ -1451,8 +1451,6 @@ and translate_meta (config : config) (meta : S.meta) (e : S.expression)
 
 let translate_fun_decl (config : config) (ctx : bs_ctx)
     (body : S.expression option) : fun_decl =
-  (* Reset the counters *)
-  reset_pure_counters ();
   (* Translate *)
   let def = ctx.fun_decl in
   let bid = ctx.bid in
-- 
cgit v1.2.3