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
test2.fq
// This qualifier saves the day; solve constraints WITHOUT IT
qualif Zog(v:a): (10 <= v)
// But you may use this one
qualif Pog(v:a): (0 <= v)
bind 0 x: {v: int | v = 10}
bind 1 a: {v: int | $k1 }
bind 2 y: {v: int | v = 20}
bind 3 b: {v: int | $k1 }
bind 4 c: {v: int | $k0 }
constraint:
env [ ]
lhs {v : int | v = 0}
rhs {v : int | $k1 }
id 0 tag []
constraint:
env [0; 1]
lhs {v : int | v = x + a}
rhs {v : int | $k0}
id 1 tag []
constraint:
env [2; 3]
lhs {v : int | v = y + b}
rhs {v : int | $k0}
id 2 tag []
constraint:
env [ ]
lhs {v : int | $k0}
rhs {v : int | $k1}
id 3 tag []
constraint:
env [4]
lhs {v : int | v = c }
rhs {v : int | 10 <= v}
id 4 tag []
wf:
env [ ]
reft {v: int | $k0}
wf:
env [ ]
reft {v: int | $k1}
Computing file changes ...
