bind 1 pig : {v: int | []}
bind 3 argAlice : {v: int | v = 10}
bind 4 alice : {v: int | [$k0[vk01 := argAlice][vk02 := v]] }
bind 5 argBob : {v: int | v = 20}
bind 6 bob : {v: int | [$k1[vk11 := argBob][vk12 := v]] }
bind 10 vk01 : {v: int | []}
bind 11 vk11 : {v: int | []}
// This is a version of the UNSAFE pack00.fq + the pack annotations,
// which shouldn't magically make it safe.
pack $k0 : 1
pack $k1 : 1
constraint:
env [1]
lhs {v1 : int | [v1 = pig + 1]}
rhs {v1 : int | [$k0[vk01 := pig][vk02 := v1]]}
id 1 tag [2]
constraint:
env [1]
lhs {v2 : int | [v2 = pig + 1]}
rhs {v2 : int | [$k1[vk11 := pig][vk12 := v2]]}
id 2 tag [2]
constraint:
env [3; 4; 5; 6]
lhs {v3 : int | [v3 = alice + bob]}
rhs {v3 : int | [v3 = 0]}
id 3 tag [2]
wf:
env [10]
reft {vk02: int | [$k0]}
wf:
env [11]
reft {vk12: int | [$k1]}