Skip to content

Fall back to checking equality of expressions in sim#997

Open
oskgo wants to merge 1 commit into
mainfrom
fix-990-2
Open

Fall back to checking equality of expressions in sim#997
oskgo wants to merge 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.

Co-authored-by: Copilot <copilot@github.com>
@oskgo oskgo marked this pull request as ready for review June 19, 2026 12:42
@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.

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

1 participant