Use equal_idx function

src/dynarray/stm_tests.ml

@@ -36,6 +36,8 @@ module Dynarray_spec (Elem : Elem) = struct
 
   type idx = I of int [@@unboxed]
 
+  let equal_idx (I i1) (I i2) = Int.equal i1 i2
+
   type cmd =
     | Create
     | Make of int * elem
@@ -354,7 +356,12 @@ module Dynarray_spec (Elem : Elem) = struct
     | Append_list (arr_i, l) ->
         update_model arr_i (fun arr -> arr @ l) state
     | Append (arr_i1, arr_i2) ->
-        update_model arr_i1 (fun arr -> arr @ get_model arr_i2 state) state
+      (* "Warning: append a a is a programming error because it iterates on a and
+          adds elements to it at the same time [...] It fails with Invalid_argument." *)
+      update_model arr_i1 (fun arr -> arr @ get_model arr_i2 state) state
+      (* In practice:
+         Invalid_argument "Dynarray.append: a length change from 3 to 6 occurred during iteration"
+         and the state change happens *)
     | Append_seq (arr_i, arr') ->
         update_model arr_i (fun arr -> arr @ Array.to_list arr') state
     | Append_iter (arr_i, arr') ->
@@ -452,7 +459,7 @@ module Dynarray_spec (Elem : Elem) = struct
       valid_arr_idx i state &&  valid_arr_idx j state &&
       (match res with
        | Ok () -> true
-       | Error (Invalid_argument _) -> i=j
+       | Error (Invalid_argument _) -> equal_idx i j
        | Error _ -> false)
     | Append_seq (i,_), Res ((Result (Unit, Exn), _), res) -> valid_arr_idx i state && res = Ok ()
     | Append_iter (i,_), Res ((Result (Unit, Exn), _), res) -> valid_arr_idx i state && res = Ok ()