Revision e782f4a589aa38c100ec34f2a390d35247e3653b authored by Anish Tondwalkar on 19 August 2019, 08:43:17 UTC, committed by Anish Tondwalkar on 19 August 2019, 08:43:17 UTC
1 parent fe737ea
test3.fq
qualif Zog(v:a, z:b) : (v = z)
bind 0 x : {v : int | true}
bind 1 q : {v : int | true}
bind 2 y : {v : int | v = 42}
constraint:
env [1]
lhs {v : int | v = q}
rhs {v : int | $k0[x:=q] }
id 1 tag []
constraint:
env [2]
lhs {v : int | $k0[x:=y]}
rhs {v : int | v = 10}
id 2 tag []
wf:
env [0]
reft {v : int | $k0}
Computing file changes ...
