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

Function as argument #67

Closed BenjaminCosman closed 9 years ago

BenjaminCosman commented 9 years ago

See:

https://github.com/ucsd-progsys/liquid-fixpoint/blob/cutsolver/tests/todo/func-arg.fq

external/fixpoint/fixpoint.native returns SAT, but the haskell solver throws an error

ranjitjhala commented 9 years ago

thanks for the super minimal example! will look into this asap.

ranjitjhala commented 9 years ago

Which is the benchmark from which this is from?

ranjitjhala commented 9 years ago

Pushed an edit that filters out Higher Order binders, works for this (and other tests) so closing.

see febb09f0cdda32ca8359437670566c1d67bc622f fc9ce8d6c6494c80d89fc6ba84a1a29727e49e75