-
Notifications
You must be signed in to change notification settings - Fork 42
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Simplification rule with symbolic
attribute applied on concrete input
#3644
Comments
Perhaps the rule introducing fresh variables can be rewritten now that we're not needing ot commute the mulitplication in the first place?
Then we don't get the "race" condition on the rules? @lucasmt can you try it? |
For now we can work around this by using less general lemmas instead of
So we are not blocked by this issue. |
I've pushed a branch with a minimal reproducible example here: https://github.com/runtimeverification/evm-semantics/tree/reproduce-fresh-uint The example can be reproduced by running the |
I have some problems reproducing this via the given branch |
For the record: After commenting out all Investigation revealed that it is in fact not The error can be triggered by running this execute request which calls freshUInt, taking a single rewrite step .
Next steps:
|
|
As mentioned, this wrong simplification happens inside A run with
I.e., the rule that introduces Postponing this for now, as we can avoid falling back to |
The issue is reported by @lucasmt pn Slack, see the thread. I'm quoting the message here:
The text was updated successfully, but these errors were encountered: