Repository navigation
Conversation
`loop_header_of` took the first dominator of the marker block that has a back edge, but a dominating loop header need not contain the marker. An invariant written in an outer loop body after an inner loop was installed at the inner loop's header, and one written after a loop outside every loop was silently attached to that loop. Require the marker to lie in the natural loop of one of the header's back edges. Fixes #352 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01JTZrVqVEqBgdyunsY7yQ5P
Codex Review SummaryThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
This branch has not been deployed
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
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.
Fixes #352.
loop_header_ofwalked up the dominator tree from the marker block and took the first block with a back edge. A header that dominates the marker does not have to contain it, which caused two problems:Unsat.The fix keeps the dominator walk but accepts a header only when the marker lies in the natural loop of one of its back edges
p -> header. That means the marker reachespwithout passing through the header, whichnatural_loop_containschecks with a backward search fromp.Added
tests/ui/{pass,fail}/loop_invariant_after_inner_loop.rs. The pass file wasUnsatbefore this change. The fail file breaks the invariant (3 * i→2 * i).cargo fmt --check,cargo clippy -- -D warningsandcargo test(with PCSat) all pass.Generated by Claude Code