search

ucsd-progsys / liquid-fixpoint

Horn Clause Constraint Solving for Liquid Types
BSD 3-Clause "New" or "Revised" License
132 stars 59 forks source link

Disallow bogus substitutions? #68

Closed BenjaminCosman closed 9 years ago

BenjaminCosman commented 9 years ago

See:

https://github.com/ucsd-progsys/liquid-fixpoint/blob/cutsolver/tests/weird/bogus.fq

Note that this isn't just a hand-crafted edge-case - you can find a similar bogus substitution if you run liquid on https://github.com/ucsd-progsys/liquidhaskell/blob/master/tests/pos/TopLevel.hs and then search for tmp_x_185

ranjitjhala commented 9 years ago

Ok let's discuss right now?

On May 27, 2015, at 2:27 PM, bmcfluff notifications@github.com wrote:

See:

https://github.com/ucsd-progsys/liquid-fixpoint/blob/cutsolver/tests/weird/bogus.fq

Note that this isn't just a hand-crafted edge-case - you can find a similar bogus substitution if you run liquid on https://github.com/ucsd-progsys/liquidhaskell/blob/master/tests/pos/TopLevel.hs and then search for tmp_x_185

— Reply to this email directly or view it on GitHub.

ranjitjhala commented 9 years ago

This is fine, because in $k__0[q:=r] the q is not in the domain of k__0 so we can just eliminate the substitution entirely...

BenjaminCosman commented 9 years ago

Eliminate.hs now handles this correctly