change z3 version to 4.13.3

[karthikbhargavan]

I am sure there may be a better place to put the --z3version but with this change, KaRaMeL works with the latest F* and Z3 4.13.3

[msprotz]

@mtzguido can you remind me what's up with using the most recent z3 version?

what I'd like to understand is what happens to people like @R1kM and I for whom z3 is z3 4.8.5 and who presumably don't have z3 4.13.3 installed -- can everything be handled with ./everest z3? just want to make sure before merging this in!

[prosecco]

warning: valecrypt does not seem to like 4.13.3

…

On Thu, Dec 26, 2024, 16:23 Jonathan Protzenko ***@***.***> wrote: @mtzguido <https://github.com/mtzguido> can you remind me what's up with using the most recent z3 version? what I'd like to understand is what happens to people like @R1kM <https://github.com/R1kM> and I for whom z3 is z3 4.8.5 and who presumably don't have z3 4.13.3 installed -- can everything be handled with ./everest z3? just want to make sure before merging this in! — Reply to this email directly, view it on GitHub <#510 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ABDABHVCX6RT7FBRKD7PFB32HQUPJAVCNFSM6AAAAABUF2CFFSVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDKNRSHEZDQNRTGI> . You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>

[mtzguido]

Yes running ./everest z3 should install both versions as z3-4.8.5 and z3-4.13.3 so F* can find them automatically. project-everest/everest#119

[msprotz]

@karthikbhargavan can you recall if you upgraded something else in your setup then? could it be that you now have z3 resolve to 4.13.3 instead of the old 4.8.5? F* expects 4.8.5 by default

[mtzguido]

(btw, I think karamel should work as it is now with 4.8.5 as long as F* can find it, but the idea is to gradually move to 4.13.3, so I'd be happy seeing this PR merged if it works for everyone)

[msprotz]

yeah I'm roughly in favor of merging (modulo putting the flag directly in $(FSTAR)), with the caveat that some users may not realize that the right thing to do is to create aliases, and thus will end up with z3 being 4.13.3 which will then make their build of HACL* fail (which is what I suspect happened to Karthik)

maybe the error message should clearly say "please create an alias" (if it doesn't already?)

[mtzguido]

The error should be something like this:

$ ./bin/fstar.exe ulib/Prims.fst -f
* Error 357 at ulib/Prims.fst(498,0-498,68):
  - Unexpected Z3 version for 'z3': expected '4.8.5', got '4.13.3'.
  - Please download version 4.8.5 of Z3 from
        https://github.com/Z3Prover/z3/releases
    and install it into your $PATH as 'z3-4.8.5'.

1 error was reported (see above)