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

[cutsolver] Deleting constraint causes UNSAT #85

Closed BenjaminCosman closed 9 years ago

BenjaminCosman commented 9 years ago

See:

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

Native solver says SAT, but if you delete constraint 13 then it says UNSAT?

BenjaminCosman commented 9 years ago

Fixed by dfd4eda1397cb26c3b22c071ad4d9e0d0d93ac64