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

Produce an intelligible error message when the z3 version is not the expected one #622

Open facundominguez opened 2 years ago

facundominguez commented 2 years ago

Our CI is using z3 as SMT solver, and new users usually try that when first installing LH. However, LF doesn't work with any z3 version, leading to errors like

crash: SMTLIB2 respSat = Error "line 4 column 27: unknown parameter 'model_partial', this is an old parameter name, invoke 'z3 -p' to obtain the new parameter list"

It would help users if LF checked the z3 version being used and produced an error if the version is not one of the expected ones.

At this point I don't know which z3 versions are supported, but we could start by demanding the specific version used in CI, and maybe adding a flag to disable the check if the user wants to run LF with whatever version she has instead.

ranjitjhala commented 2 years ago

Yes this would be good — that error (the person reporting on slack?) surprised me — as LH has been mostly very stable since we use the SMTLIB interface which hasn’t changed in awhile.