ucsd-progsys/liquid-fixpoint — pull request #33 by nikivazou (2014-05-03 04:26:49+00:00)
Title: Simplification

external/fixpoint/tests/bad.fq should be SAT but was UNSAT and the bug was in the simplification of the solution....

We have two qualifiers:
~~~
qualif Cmp1(v:a,~A:a) : v <= ~A
qualif Auto3(VV : t_a16R, ~A0 : t_a16R): (VV < ~A0)
~~~

`predAbs.def_leq s (Cmp1(v, k)) (Auto3(v, l))` used to be True, because the arguments in the definition of the qualifiers are different. Note that the arguments `k` and `l` are **different**.

So, previously, the qualifier `Auto3(v, l)` was lost from the `k_411` (in `bad.fq`)
and with that every information that relates `v` with `l` was lost.