search

ucsd-progsys / liquid-fixpoint

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

Fail gracefully when SMT returns EOF #625

Closed gabrielhdt closed 1 year ago

gabrielhdt commented 1 year ago

Fixes #231 Whenever the SMT command returns EOF (typically when the SMT command is not found), the program stops with message "SMT returned End of File".

To test it,

$ command -v z3
$ echo $?
1
$ stack exec fixpoint -- tests/pos/adt.fq
[...]
Working   0% [.................................................................]
fixpoint: 
**** ERROR *********************************************************************
**** ERROR *********************************************************************
**** ERROR *********************************************************************
SMT returned End of File
**** ERROR *********************************************************************
**** ERROR *********************************************************************
**** ERROR *********************************************************************

CallStack (from HasCallStack):
  error, called at src/Language/Fixpoint/Misc.hs:156:14 in liquid-fixpoint-0.8.10.7.1-6wSG354KhckBRT3ofw9cCu:Language.Fixpoint.Misc
  errorstar, called at src/Language/Fixpoint/Smt/Interface.hs:269:15 in liquid-fixpoint-0.8.10.7.1-6wSG354KhckBRT3ofw9cCu:Language.Fixpoint.Smt.Interface
ranjitjhala commented 1 year ago

Super thanks so much!!! (I’ll merge once CI gives the green light!)