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

[facundominguez]

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]

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.