nits

src/ecCircuits.ml

@@ -1137,7 +1137,7 @@ let instrs_equiv
   if not (List.for_all (EcTypes.is_loc |- fst) (rd @ wr)) then
     raise (CircError "the statements should not read/write global variables");
 
-  let pstate = List.map (fun (pv, ty) -> { v_name = EcTypes.get_loc pv; v_type = ty; }) wr in
+  let pstate = List.map (fun (pv, ty) -> { v_name = EcTypes.get_loc pv; v_type = ty; }) (rd @ wr) in
   let pstate, inputs = pstate_of_variables env pstate in
 
   let pstate1 = List.fold_left (process_instr hyps mem) pstate s1 in

src/phl/ecPhlRwPrgm.ml

@@ -11,10 +11,9 @@ type change_t = pcodepos * int * pstmt
 let process_change ((cpos, i, s) : change_t) (tc : tcenv1) =
   let env = FApi.tc1_env tc in
   let hs = EcLowPhlGoal.tc1_as_hoareS tc in
+  let env = EcEnv.Memory.push_active hs.hs_m env in
 
-  let cpos =
-    let env = EcEnv.Memory.push_active hs.hs_m env in
-    EcTyping.trans_codepos env cpos in
+  let cpos = EcTyping.trans_codepos env cpos in
 
   let s =
     let ue = EcProofTyping.unienv_of_hyps (FApi.tc1_hyps tc) in