module Ce_int32

  use ref.Ref
  use export mach.int.Int32

  meta "meta_incremental" ""

  let dummy_update (r: ref int32)
    requires { to_int !r = 22}
    ensures {to_int !r = 42} =
    r := of_int 42;
    r := !r + !r;

end


module Ce_interesting

  use int.Int
  use ref.Ref
  use export mach.int.Int32

  meta "meta_incremental" ""

  let dummy_update (r: ref int32)
    requires { to_int !r > 22}
    ensures {to_int !r <= 42} =
    r := of_int 42;
    r := !r + !r;

end