The typing of this code raises Invalid_argument("Ity.eff_reset")

theory Effect

  use ref.Ref

   type t = { mutable a: ref int }

  let resize (h: t) : unit
    =
     let r = ! (h.a) in
     h.a <- ref r

  let set (h: t) : unit
    =
      resize h;
      h.a := 0

end

theory Clone

       clone Effect

end

By looking at the code it seems that an invariant is broken (writes and resets are not disjoint?). The cty that fails:

(h:t) : ()
writes { (h.a:ref int @rho).contents, (h:t <ref int @rho> @rho1).a }
covers { h:t <ref int @rho> @rho1 }
resets { h.a:ref int @rho }

@paskevyc @filliatr