New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

unknown parameter 'model_partial' #3

Closed

k4rtik opened this issue Jan 11, 2023 · 3 comments

k4rtik commented Jan 11, 2023

Hi @ranjitjhala

Thanks for this tutorial introduction to refinement types. When I try to run the example in README, I get the following error:

✗ stack exec -- sprite 8 test/L8/pos/listSet.re
Crash!: :1:1-1:1: 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"

I am using the fork I made at https://github.com/k4rtik/sprite-lang to be able to run the code on my M1 machine. Specifically, I am on ghc 8.10.7, Z3 version 4.11.2, and liquid-fixpoint commit: 92e434da5653c5d75e1f6f1bd687bc0dc9d8acdf

Author

k4rtik commented Jan 11, 2023

I see this is also reported at ucsd-progsys/liquid-fixpoint#622

Author

k4rtik commented Jan 11, 2023

Fixed by updating liquid-fixpoint, see k4rtik@69f32f0#diff-0de01f189d384bfbe69e806ef70b1a425b27394dbe2a9d0e62ffd010dda86c03

k4rtik closed this as completed

Owner

ranjitjhala commented Jan 11, 2023 via email

Thanks Kartik - I just bumped the stack/cabal to update so this should go away!

On Wed, Jan 11, 2023 at 9:23 AM Kartik Singhal ***@***.***> wrote: Closed #3 <https://urldefense.com/v3/__https://github.com/ranjitjhala/sprite-lang/issues/3__;!!Mih3wA!Ho_gWTPK07ajLLIfM_yEY0V9d1p_2rKLtPLYwFJz9zPOtIU-QBXlR9cPnrDjMEuSS_KZpwH_2f817KPnpFFWMBMy$> as completed. — Reply to this email directly, view it on GitHub <https://urldefense.com/v3/__https://github.com/ranjitjhala/sprite-lang/issues/3*event-8203891069__;Iw!!Mih3wA!Ho_gWTPK07ajLLIfM_yEY0V9d1p_2rKLtPLYwFJz9zPOtIU-QBXlR9cPnrDjMEuSS_KZpwH_2f817KPnpJa8Q79_$>, or unsubscribe <https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/AAMS4OGXSUYNPJLZPV4GCOTWR3UCJANCNFSM6AAAAAATXO5KHY__;!!Mih3wA!Ho_gWTPK07ajLLIfM_yEY0V9d1p_2rKLtPLYwFJz9zPOtIU-QBXlR9cPnrDjMEuSS_KZpwH_2f817KPnpJlZ8pbD$> . You are receiving this because you were mentioned.Message ID: ***@***.***>

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment