Merge branch 'upgrade_proofs_coq_8_11_to_8_16' into 'master'

[why3.git] / bench / check-ce / int32.mlw

module Ce_int32

  use mach.int.Int32

  let dummy_update (ref r : int32)
    requires { int32'int r = 22}
    ensures { int32'int r = 42} =
    r <- (42:int32);
    r <- r + r;

end