Short circuit for `or` operator is not respected in smt checker counterexample
- Dominant language
- C++
- Stars
- 25.7k
- Forks
- 6.2k
- Avg merge
- 2d 19h
- Merged PRs (30d)
- 29
Description
in `test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_fail.sol`
we have:
```
contract c {
uint x;
function f() internal returns (uint) {
x = x + 1;
return x;
}
function g() public returns (bool) {
x = 0;
bool b = (f() > 0) || (f() > 0);
assert(x == 1);
assert(!b);
return b;
}
}
```
smt checker prints the following warning
```
Warning 6328: (192-202): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n = false\nb = true\n\nTransaction trace:\nc.constructor()\nState: x = 0\nc.g()\n c.f() -- internal call\n c.f() -- internal call
```
which is invalid - function `f` is called only once, because of short circuit in `or` operator.
Contributor guide
Assessment
This issue has not been assessed yet.