Skip to content

Avoid comparing unreachable constructor deployments - #1249

Open
dajiaohuang wants to merge 1 commit into
argotorg:mainfrom
dajiaohuang:w8/fix-create-path-overlap
Open

dajiaohuang wants to merge 1 commit into
argotorg:mainfrom
dajiaohuang:w8/fix-create-path-overlap

Conversation

@dajiaohuang

@dajiaohuang dajiaohuang commented Oct 27, 2026 •

Copy link
Copy Markdown

Description

Fix false --create counterexamples from comparing concrete deployed runtimes on mutually exclusive constructor paths. Before nested runtime equivalence, check satisfiability of the combined constructor path constraints. If the solver cannot decide overlap, report that uncertainty rather than claiming a runtime counterexample. Adds the exact bytecode regression from #1179.

Fixes #1179.

Checklist

  • tested locally — not run; this Windows environment has no nix, cabal, or ghc. cabal run test failed before starting because cabal is unavailable; the README development flow requires a Nix shell.
  • added automated tests
  • updated the docs (not needed for this behavioral fix)
  • updated the changelog (not required by the repository PR template)

git diff --check passed.

This branch has not been deployed

No deployments
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

hevm equivalence --create compares deployed code from constructor paths that cannot both happen

1 participant