Open
Conversation
mtzguido
reviewed
Mar 31, 2026
Member
There was a problem hiding this comment.
Maybe these two guards can be removed now?
Add explicit SMT hints and split_queries to fix regressions caused by the structural Universe encoding change (U_zero/U_succ datatype instead of Univ wrapping Int). - FStar.UInt128: add non-negativity assertions for k1*k2, k1*m, n+k1*m to help Z3 with subtyping checks; remove z3rlimit_factor bump - PulseCore.Preorder: explicit case-split match in assoc_l/assoc_r with split_queries always (each case is trivial individually) - Pulse.Lib.FractionalAnchoredPreorder: add split_queries always for update_anchored_hist - AlgHeap: add split_queries always for interp_morph - RBTreeIntrinsic: add split_queries always for balance sort proofs Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Z3 4.13.3 has a bug in its LP solver (lar_solver.cpp assertion violation / segfault) triggered by the 2-constructor Universe algebraic datatype (U_zero | U_succ) during incremental solving. The crash occurs on the 19th query when Z3 evaluates labels after an unknown result. Using --z3refresh (fresh Z3 per query) avoids the accumulated state that triggers the crash. Z3 4.15.3 does not have this bug. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
- Change Universe from algebraic datatype to (declare-sort Universe) with uninterpreted U_zero/U_succ functions and no :weight annotations - Fix FStar.Int.rotate_right_left_inverse: add explicit modular arithmetic lemma (rotate_mod_lemma) to guide Z3 through ((i+s)%n + n - s%n) % n = i - Remove --z3refresh from AlgForAll: uninterpreted sort avoids the Z3 4.13.3 incremental segfault that the algebraic datatype encoding triggered Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
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.