Skip to content

Fall back to checking equality of expressions in sim#997

Merged
fdupress merged 1 commit into
mainfrom
fix-990-2
Jul 10, 2026
Merged

Fall back to checking equality of expressions in sim#997
fdupress merged 1 commit into
mainfrom
fix-990-2

Conversation

@oskgo

@oskgo oskgo commented May 7, 2026

Copy link
Copy Markdown
Contributor

Fixes #990.

Maybe this should be fixed by making the equality check in pretty printing stronger instead. I'm not sure what's right here.

Blocked by #996.

@oskgo

oskgo commented Jun 19, 2026

Copy link
Copy Markdown
Contributor Author

The breakage in sha3 is expected breakage. A goal that was not solved by sim before is now solved. We get an anomaly due to #1054.

The fix is to prune the branch of the proof after the sim at the offending location.

@oskgo oskgo requested a review from strub June 22, 2026 11:26
@strub strub self-assigned this Jul 3, 2026
@strub strub added this pull request to the merge queue Jul 3, 2026
@github-merge-queue github-merge-queue Bot removed this pull request from the merge queue due to failed status checks Jul 3, 2026
Comment thread src/ecPV.ml
@oskgo oskgo added this pull request to the merge queue Jul 10, 2026
@github-merge-queue github-merge-queue Bot removed this pull request from the merge queue due to failed status checks Jul 10, 2026
@fdupress fdupress added this pull request to the merge queue Jul 10, 2026
Merged via the queue into main with commit 6ea6bdc Jul 10, 2026
19 checks passed
@fdupress fdupress deleted the fix-990-2 branch July 10, 2026 15:05
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

sim less robust

4 participants