Repository navigation
Upgrade to Z3 5.1 - #340
Merged
Merged
Conversation
EVERPARSE_Z3_VERSION now defaults to 5.1.0, F*'s default Z3 version. The 3D test-generation Makefiles and the adapter tests follow EVERPARSE_Z3_VERSION instead of hardcoding z3-4.13.3, and so does the binary package. Olympus-Change: minimal Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: f536a3f7-4be1-44ba-ba6c-992c94e5e517
Olympus-Change: minimal Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: f536a3f7-4be1-44ba-ba6c-992c94e5e517
3D: use (check-sat-using smt) in Z3 test generation, since Z3 5.1.0's default incremental solver may not terminate on these push/pop sessions; add an F# realization of Hashing.Op.t for hashchk (now required by F*). Olympus-Change: minimal Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: f536a3f7-4be1-44ba-ba6c-992c94e5e517
CBOR/CDDL Pulse: avoid non-linear real arithmetic on permissions (on which Z3 5.1.0 may not terminate) and prune a quantifier cascade from array_group_concat_unique_strong in cddl_array_iterator_next. Olympus-Change: minimal Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: f536a3f7-4be1-44ba-ba6c-992c94e5e517
CBOR.Pulse.Raw.Match: exclude CBOR.Pulse.Raw.Util.perm_mul_assoc, whose SMT patterns cause a matching loop with Z3 5.1.0 on permission products. Olympus-Change: minimal Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: f536a3f7-4be1-44ba-ba6c-992c94e5e517
The pinned F* fb6ea91 does not know about Z3 5.1.0, so CI's get_fstar_z3.sh never downloads z3-5.1.0 and F* reports 'Z3 solver not found'. Move to the F* commit that adds 5.1.0 (FStarLang/FStar#4654 merged with master, plus an rlimit cap). Olympus-Change: minimal Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: f536a3f7-4be1-44ba-ba6c-992c94e5e517
The Z3 5.1.0 release binary bundled in the package requires glibc 2.38, which Ubuntu 22.04 lacks. Olympus-Change: minimal Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: f536a3f7-4be1-44ba-ba6c-992c94e5e517
Make three proofs that failed in GitHub CI (Z3 5.1.0 release) robust, so that they succeed on the first attempt with large rlimit margin: - CBOR.Spec.API.Format: split cbor_det_serialize_map_length_union_disjoint_eq into helper lemmas (snoc length, cons preconditions, cons serialization length, linear arithmetic step); it no longer needs --z3rlimit 32. Also make cbor_parse_prefix succeed without the ifuel retry. - CBOR.Pulse.Raw.EverParse.Serialized.Base: in the tagged/array/map intro_aux ghost functions, state the perm_mul 1.0R and Array?.v/Map?.v equalities as small lemmas before the rewrites. - EverParse3d.Actions.Base (validate_list_up_to): move the suffix reasoning after a leaf read and the list_up_to loop-invariant step into separate lemmas (leaf_read_is_suffix_of, list_up_to_step). Checked with --query_stats on seeds 0-3 with both Z3 master and the Z3 5.1.0 release: no failed/retried queries in these modules. Olympus-Change: minimal Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: f536a3f7-4be1-44ba-ba6c-992c94e5e517
tahina-pro
requested changes
Oct 15, 2026
Move the default EVERPARSE_Z3_VERSION and the package's bundled Z3 to 5.3.0, and the pinned F* to olympus_z3upgrade, which now has FStarLang/FStar#4654 with Z3 5.3.0. On Linux x86_64 F* bundles the Z3 executable of the official manylinux wheel, which runs on Ubuntu 22.04, so the package tests go back to ubuntu-22.04. Olympus-Change: minimal Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: f536a3f7-4be1-44ba-ba6c-992c94e5e517
tahina-pro
requested changes
Oct 17, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.