Revision 445254861f733c4d5a0c852383bdf9a5058086bd authored by Anish Tondwalkar on 02 May 2019, 21:18:18 UTC, committed by Anish Tondwalkar on 02 May 2019, 21:18:18 UTC
1 parent 097f354
test00a.fq
// This qualifier saves the day; solve constraints WITHOUT IT
// qualif Zog(v:a) : (10 <= v)
bind 0 x : {v : int | true}
bind 1 y : {v : int | true}
bind 2 z : {v : int | true}
constraint:
env [0]
lhs {v : int | (x = 10)}
rhs {v : int | $k0[v:=x]}
id 1 tag []
constraint:
env [1]
lhs {v : int | y = 20}
rhs {v : int | $k0[v:=y]}
id 2 tag []
constraint:
env [2]
lhs {v : int | $k0[v:=z]}
rhs {v : int | 10 <= z}
id 3 tag []
wf:
env [ ]
reft {v: int | $k0}
Computing file changes ...
