liquid-fixpoint-0.7.0.3: tests/minimize/two-cores.fq
qualif Cmp(v:a): (v = 10)
qualif Cmp(v:a): (v = 12)
constraint:
env []
lhs {v : int | [v = 10]}
rhs {v : int | [$k_0]}
id 1 tag [3]
constraint:
env []
lhs {v : int | [$k_0]}
rhs {v : int | [v != 10]}
id 4 tag [4]
constraint:
env []
lhs {v : int | [v = 12]}
rhs {v : int | [$k_0]}
id 2 tag [5]
constraint:
env []
lhs {v : int | [$k_0]}
rhs {v : int | [v != 12]}
id 3 tag [6]
wf:
env []
reft {v : int | [$k_0]}