liquid-fixpoint-8.10.7: tests/pos/bool00.fq
qualif Zog(v:a) : (10 <= v)
qualif Bog(v:a, x:a) : (x <= v)
bind 0 a : {v: int | $k0}
bind 1 tt : {v: bool | v}
constraint:
env [ ]
lhs {v : int | v = 10}
rhs {v : int | $k0}
id 1 tag []
constraint:
env [ ]
lhs {v : int | v = 20}
rhs {v : int | $k0}
id 2 tag []
constraint:
env [ 0 ]
lhs {v : int | v = a}
rhs {v : int | 10 <= v}
id 3 tag []
wf:
env [ ]
reft {v: int | $k0}