Revision ae9f5b95ebf7b36577861434e2099b638540d730 authored by Anish Tondwalkar on 20 October 2019, 06:45:47 UTC, committed by Anish Tondwalkar on 20 October 2019, 06:45:47 UTC
1 parent eba2590
num00.fq
// This qualifier saves the day; solve constraints WITHOUT IT
qualif Zog(v:a) : (0 <= v)
qualif Bog(v:a) : (0 <= 1)
bind 0 zog : {v : int | true}
constraint:
env [0]
lhs {v : alpha | (v = 10)}
rhs {v : alpha | $k0}
id 1 tag []
constraint:
env [0]
lhs {v : alpha | $k0}
rhs {v : alpha | $k0}
id 2 tag []
constraint:
env [0]
lhs {v : alpha | $k0}
rhs {v : alpha | 0 <= v}
id 3 tag []
wf:
env [0]
reft {v: alpha | $k0}
Computing file changes ...