Skip to content
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

Unnamed return variable is displayed incorrectly in counter example #15423

Open
lum7na opened this issue Sep 10, 2024 · 0 comments
Open

Unnamed return variable is displayed incorrectly in counter example #15423

lum7na opened this issue Sep 10, 2024 · 0 comments

Comments

@lum7na
Copy link

lum7na commented Sep 10, 2024

Description

When the return value is unnamed, the left side of the equality sign in the counterexample appears empty.

contract C {
  function f(uint256 value) public payable returns(bool) {
    value = value / value;
  }
}

Compiled with solc --model-checker-engine all a.sol:

Warning: CHC: Division by zero happens here.
Counterexample:

value = 0
 = false // The left side of the equality sign here is empty.

Transaction trace:
C.constructor()
C.f(0){ msg.value: 19 }
 --> out.sol:3:13:
  |
3 |     value = value / value;
  |             ^^^^^^^^^^^^^

Environment

  • Compiler version: 0.8.26
@cameel cameel added the smt label Sep 10, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

2 participants