Fix position invalidation in unroll_for

Author: Gustavo2622

src/phl/ecPhlLoopTx.ml

@@ -362,7 +362,11 @@ let process_unroll_for ~cfold side cpos tc =
   let tcenv = FApi.t_onalli doi tcenv in
 
   if cfold then begin
-    let cpos = EcMatching.Position.Notations.(cpos <+| 1) in
+    (* Use normalized position: pos - 1 is the loop counter initialization
+       assignment that immediately precedes the while loop at pos.
+       We cannot reuse the original match-based cpos here because t_doit
+       has transformed the code, potentially invalidating the match. *)
+    let cpos = ([], EcMatching.Position.cpos1 (pos - 1)) in
     let clen = blen * (List.length zs - 1) in
 
     FApi.t_last (EcPhlCodeTx.t_cfold ~eager:false side cpos (Some clen)) tcenv