search

ucsd-progsys / liquidhaskell

Liquid Types For Haskell
BSD 3-Clause "New" or "Revised" License
1.19k stars 137 forks source link

Useless source span in smtlib crash #564

Open gridaphobe opened 8 years ago

gridaphobe commented 8 years ago 
:1:1-1:1: Error: crash: SMTLIB2 respSat = Error "line 123 column 42: invalid function application, wrong number of arguments"

The :1:1-1:1: bit is meaningless. We should either provide the source span that gave rise to the constraint, or elide the location entirely.

@nikivazou can you post the file that caused this error?

nikivazou commented 8 years ago

Well, it is quite difficult to reproduce the error in master, because hacked prover/fixpoint and liquidhaskell to get this error!

ranjitjhala commented 8 years ago

You can run with "--save" and put the FQ file somewhere NOT IN THE REPO! :)

On Fri, Jan 8, 2016 at 12:54 PM, Niki Vazou notifications@github.com wrote:

Well, it is quite difficult to reproduce the error in master, because hacked prover/fixpoint and liquidhaskell to get this error!

— Reply to this email directly or view it on GitHub https://github.com/ucsd-progsys/liquidhaskell/issues/564#issuecomment-170121185 .

ranjitjhala commented 8 years ago

Is there a file hs or fq that triggers this? Hard to fix otherwise ...