Commit 9ef61cea authored by Andrei Paskevich's avatar Andrei Paskevich

Ity: correct reads in cty_tuple

parent 787ad277
......@@ -1339,7 +1339,8 @@ let cty_tuple args =
let post = create_post vs (t_equ (t_var vs) (t_tuple tl)) in
let mask = mask_reduce (MaskTuple ( mask_of_pv args)) in
let res = ity_tuple ( (fun v -> v.pv_ity) args) in
let eff = eff_ghostify (mask = MaskGhost) eff_empty in
let eff = eff_read (Spv.of_list args) in
let eff = eff_ghostify (mask = MaskGhost) eff in
let frz = List.fold_right freeze_pv args isb_empty in
cty_unsafe [] [] [post] Mexn.empty Mpv.empty eff res mask frz
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment