search

ucsd-progsys / liquid-fixpoint

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

Support the newest Z3 version (z3-4.11.2) #626

Closed Alf0nso closed 2 years ago

Alf0nso commented 2 years ago

Running Liquid Haskell with newer versions of z3 causes this error:

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"

Mentioned in this issue: https://github.com/ucsd-progsys/liquid-fixpoint/issues/622 In this pr we removed the z3 "model.partial false". On older versions of z3 the default option was already false. Invoke z3 -p and we get:

[module] model
    ...
    partial (bool) (default: false)
nikivazou commented 2 years ago

Thanks @Alf0nso!!!!!! Can we have a pull request in LH too that links to this change?

oquechy commented 2 years ago

Thanks @Alf0nso!!!!!! Can we have a pull request in LH too that links to this change?

@nikivazou do you think we can do this before merging the new change into fixpoint?

nikivazou commented 2 years ago

yes, lets make sure nothing breaks in LH before merging this in fixpoint!